From: trevor_hansen Date: Fri, 16 Jan 2009 15:28:25 +0000 (+0000) Subject: USER VISIBLE CHANGE: smtlib parser now enabled with "-m" flag. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=60a94185c78c10caaf66eb13de72975c4c1f660a;p=francis%2Fstp.git USER VISIBLE CHANGE: smtlib parser now enabled with "-m" flag. A common makefile builds both parsers. -m is a terrible choice for switch, but at present we only allow one character switches.. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@55 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/INSTALL b/INSTALL index dee6e2e..549df9e 100644 --- a/INSTALL +++ b/INSTALL @@ -9,5 +9,4 @@ make install make regressall NB: -* If you want to compile STP with the parser for the SMT-LIB format, use make -f Makefile.smt instead. * If you want to compile a statically linked version of STP, run ./liblinks.sh after the configure script, and then compile adding STATIC=true to the make commands. diff --git a/Makefile.smt b/Makefile.smt deleted file mode 100644 index 3782cf8..0000000 --- a/Makefile.smt +++ /dev/null @@ -1,92 +0,0 @@ - # STP (Simple Theorem Prover) top level makefile - # - # To make in debug mode, type 'make "CLFAGS=-ggdb" - # To make in optimized mode, type 'make "CFLAGS=-O2" - -include Makefile.common config.info - -BIN_DIR=$(PREFIX)/bin -LIB_DIR=$(PREFIX)/lib -INCLUDE_DIR=$(PREFIX)/include/stp - -BINARIES=bin/stp -LIBRARIES=lib/libstp.a -HEADERS=c_interface/*.h - -# NB: the TAGS target is a hack to get around this recursive make nonsense -# we want all the source and header files generated before we make tags -.PHONY: all -all: - $(MAKE) -C AST - $(MAKE) -C sat/core lib - $(MAKE) -C simplifier - $(MAKE) -C bitvec - $(MAKE) -C c_interface - $(MAKE) -C constantbv - $(MAKE) -C parser -f Makefile.smt - $(AR) rc libstp.a AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o - $(RANLIB) libstp.a - @mkdir -p lib - @mv libstp.a lib/ -# $(MAKE) TAGS - @echo "" - @echo "Compilation successful." - @echo "Type 'make install' to install STP." - -.PHONY: install -install: all - @cp -f $(BINARIES) $(BIN_DIR) - @cp -f $(LIBRARIES) $(LIB_DIR) - @cp -f $(HEADERS) $(INCLUDE_DIR) - @echo "STP installed successfully." - -.PHONY: clean -clean: - rm -rf *~ - rm -rf *.a - rm -rf lib/*.a - rm -rf test/*~ - rm -rf bin/*~ - rm -rf *.log - rm -rf bin/stp - rm -rf Makefile - rm -rf config.info - rm -f TAGS - $(MAKE) clean -C AST - $(MAKE) clean -C sat/core - $(MAKE) clean -C simplifier - $(MAKE) clean -C bitvec - $(MAKE) clean -C parser - $(MAKE) clean -C c_interface - $(MAKE) clean -C constantbv - -# this is make way too difficult because of the recursive Make junk, it -# should be removed -TAGS: FORCE - find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags - - -FORCE: - -# The higher the level, the more tests are run (3 = all) -REGRESS_TESTS0 = egt -REGRESS_LEVEL=4 -REGRESS_TESTS=$(REGRESS_TESTS0) -REGRESS_LOG = `date +%Y-%m-%d`"-regress.log" -PROGNAME=bin/stp -ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) - -.PHONY: regressall -regressall: - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - bin/run_tests.smt $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - - diff --git a/bin/run_tests.smt b/bin/run_tests.smt index eb60723..942cf12 100755 --- a/bin/run_tests.smt +++ b/bin/run_tests.smt @@ -71,7 +71,7 @@ my %optionsDefault = ("level" => 4, "lang" => "all", "stppath" => "stp/bin", #"vc" => $pwd . "/bin/yices -smt", # Program names - "vc" => $pwd . "/bin/stp -d -f", # Program names + "vc" => $pwd . "/bin/stp -d -f -m", # Program names #"vc" => "valgrind --leak-check=full /home/vganesh/stp/bin/stp", # Program names "pfc" => "true", "stptestpath" => "stp/smt_tests", diff --git a/parser/PL.lex b/parser/CVC.lex similarity index 79% rename from parser/PL.lex rename to parser/CVC.lex index e30f198..3dd3320 100644 --- a/parser/PL.lex +++ b/parser/CVC.lex @@ -8,10 +8,10 @@ ********************************************************************/ #include #include "../AST/AST.h" -#include "parsePL_defs.h" +#include "parseCVC_defs.h" extern char *yytext; -extern int yyerror (const char *msg); +extern int cvcerror (const char *msg); %} %option noyywrap @@ -33,11 +33,11 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) [\n] { /*Skip new line */ } [ \t\r\f] { /* skip whitespace */ } -0b{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} -0bin{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} -0h{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} -0hex{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} -{DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;} +0b{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} +0bin{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} +0h{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} +0hex{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} +{DIGIT}+ { cvclval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;} "%" { BEGIN COMMENT;} "\n" { BEGIN INITIAL; /* return to normal mode */} @@ -117,13 +117,13 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) // Check valuesize to see if it's a prop var. I don't like doing // type determination in the lexer, but it's easier than rewriting // the whole grammar to eliminate the term/formula distinction. - yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); - //yylval.node = new BEEV::ASTNode(nptr); - if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE) + cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); + //cvclval.node = new BEEV::ASTNode(nptr); + if ((cvclval.node)->GetType() == BEEV::BOOLEAN_TYPE) return FORMID_TOK; else return TERMID_TOK; } -. { yyerror("Illegal input character."); } +. { cvcerror("Illegal input character."); } %% diff --git a/parser/PL.y b/parser/CVC.y similarity index 99% rename from parser/PL.y rename to parser/CVC.y index 7d15081..d391d77 100644 --- a/parser/PL.y +++ b/parser/CVC.y @@ -15,11 +15,11 @@ using namespace std; // compile error) #undef __GNUC_MINOR__ - extern int yylex(void); + extern int cvclex(void); extern char* yytext; - extern int yylineno; + extern int cvclineno; int yyerror(const char *s) { - cout << "syntax error: line " << yylineno << "\n" << s << endl; + cout << "syntax error: line " << cvclineno << "\n" << s << endl; BEEV::FatalError(""); return 1; /* Dill: don't know what it should return */ }; diff --git a/parser/Makefile b/parser/Makefile index 9d5a917..8ad9a9a 100644 --- a/parser/Makefile +++ b/parser/Makefile @@ -1,24 +1,36 @@ + include ../Makefile.common -SRCS = lexPL.cpp parsePL.cpp let-funcs.cpp main.cpp +LEX=flex +YACC=bison -d -y --debug -v + +SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp let-funcs.cpp main.cpp OBJS = $(SRCS:.cpp=.o) LIBS = -L../AST -last -L../sat/core -L../sat/simp -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp -all: parsePL.cpp lexPL.cpp let-funcs.cpp parser parsePL.o lexPL.o let-funcs.o +all: parseSMT.cpp lexSMT.cpp parseCVC.cpp lexCVC.cpp let-funcs.cpp parser parseCVC.o lexCVC.o let-funcs.o -parser: lexPL.o parsePL.o let-funcs.o main.o parsePL_defs.h - $(CXX) $(CFLAGS) $(LDFLAGS) lexPL.o parsePL.o main.o let-funcs.o $(LIBS) -o parser +parser: lexCVC.o parseCVC.o lexSMT.o parseSMT.o let-funcs.o main.o + $(CXX) $(CFLAGS) $(LDFLAGS) lexCVC.o lexSMT.o parseCVC.o parseSMT.o main.o let-funcs.o $(LIBS) -o parser @mv parser ../bin/stp -lexPL.cpp: PL.lex parsePL_defs.h ../AST/AST.h - $(LEX) PL.lex - @mv lex.yy.c lexPL.cpp +lexCVC.cpp: CVC.lex parseCVC_defs.h ../AST/AST.h + $(LEX) -o lexCVC.cpp --prefix cvc CVC.lex + +parseCVC_defs.h parseCVC.cpp: CVC.y + $(YACC) -p cvc CVC.y + @cp y.tab.c parseCVC.cpp + @cp y.tab.h parseCVC_defs.h -parsePL.cpp: PL.y - $(YACC) PL.y - @cp y.tab.c parsePL.cpp - @cp y.tab.h parsePL_defs.h +lexSMT.cpp: parseSMT_defs.h smtlib.lex ../AST/AST.h + $(LEX) -o lexSMT.cpp --prefix smt smtlib.lex + +parseSMT_defs.h parseSMT.cpp:smtlib.y + $(YACC) -p smt smtlib.y + @cp y.tab.c parseSMT.cpp + @cp y.tab.h parseSMT_defs.h clean: - rm -rf *.o parsePL_defs.h *~ lexPL.cpp parsePL.cpp *.output parser y.tab.* lex.yy.c .#* + rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser y.tab.* lex.yy.c .#* + diff --git a/parser/Makefile.smt b/parser/Makefile.smt deleted file mode 100644 index e55aa7e..0000000 --- a/parser/Makefile.smt +++ /dev/null @@ -1,27 +0,0 @@ -include ../Makefile.common - -LEX=flex -YACC=bison -d -y --debug -v - -SRCS = lexPL.cpp parsePL.cpp let-funcs.cpp main.cpp -OBJS = $(SRCS:.cpp=.o) -LIBS = -L../AST -last -L../sat/core -L../sat/simp -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv -CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp - -all: parsePL.cpp lexPL.cpp let-funcs.cpp parser parsePL.o lexPL.o let-funcs.o - -parser: lexPL.o parsePL.o main.o let-funcs.o parsePL_defs.h - $(CXX) $(CFLAGS) $(LDFLAGS) lexPL.o parsePL.o main.o let-funcs.o $(LIBS) -o parser - @mv parser ../bin/stp - -lexPL.cpp: smtlib.lex parsePL_defs.h ../AST/AST.h - $(LEX) smtlib.lex - @mv lex.yy.c lexPL.cpp - -parsePL.cpp: smtlib.y - $(YACC) smtlib.y - @cp y.tab.c parsePL.cpp - @cp y.tab.h parsePL_defs.h - -clean: - rm -rf *.o parsePL_defs.h *~ lexPL.cpp parsePL.cpp *.output parser y.tab.* lex.yy.c .#* diff --git a/parser/main.cpp b/parser/main.cpp index 3a0f908..547b9df 100644 --- a/parser/main.cpp +++ b/parser/main.cpp @@ -17,7 +17,6 @@ //#include #include #include "../AST/AST.h" -#include "parsePL_defs.h" #include "../sat/core/Solver.h" #include "../sat/core/SolverTypes.h" //#include "../sat/VarOrder.h" @@ -30,8 +29,9 @@ /* GLOBAL FUNCTION: parser */ -extern int yyparse(); -//extern int smtlibparse(); +extern int smtparse(); +extern int cvcparse(); + /* GLOBAL VARS: Some global vars for the Main function. * @@ -60,7 +60,10 @@ BEEV::ASTNode SingleBitZero; ******************************************************************************/ int main(int argc, char ** argv) { char * infile; - extern FILE *yyin; + extern FILE *cvcin; + extern FILE *smtin; + + // Grab some memory from the OS upfront to reduce system time when individual // hash tables are being allocated @@ -81,6 +84,10 @@ int main(int argc, char ** argv) { helpstring += "-p : print counterexample\n"; helpstring += "-x : flatten nested XORs\n"; helpstring += "-h : help\n"; + helpstring += "-m : use the SMTLIB parser\n"; + + + bool smtlibParser = false; for(int i=1; i < argc;i++) { if(argv[i][0] == '-') { @@ -116,6 +123,9 @@ int main(int argc, char ** argv) { break; case 'n': BEEV::print_output = true; + break; + case 'm': + smtlibParser=true; break; case 'p': BEEV::print_counterexample = true; @@ -160,11 +170,25 @@ int main(int argc, char ** argv) { } } else { infile = argv[i]; - yyin = fopen(infile,"r"); - if(yyin == NULL) { - fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); - BEEV::FatalError(""); - } + + if (smtlibParser) + { + smtin = fopen(infile,"r"); + if(smtin == NULL) + { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + BEEV::FatalError(""); + } + } + else + { + cvcin = fopen(infile,"r"); + if(cvcin == NULL) + { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + BEEV::FatalError(""); + } + } } } @@ -184,5 +208,9 @@ int main(int argc, char ** argv) { SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); //BEEV::smtlib_parser_enable = true; - yyparse(); + + if (smtlibParser) + smtparse(); + else + cvcparse(); }//end of Main diff --git a/parser/smtlib.lex b/parser/smtlib.lex index 5d5f1a6..27c2b1f 100644 --- a/parser/smtlib.lex +++ b/parser/smtlib.lex @@ -35,10 +35,10 @@ // -*- c++ -*- #include #include "../AST/AST.h" -#include "parsePL_defs.h" +#include "parseSMT_defs.h" - extern char *yytext; - extern int yyerror (char *msg); + extern char *smttext; + extern int smterror (char *msg); // File-static (local to this file) variables and functions static std::string _string_lit; @@ -55,7 +55,7 @@ extern BEEV::ASTNode SingleBitZero; /* Changed for smtlib speedup */ -/* bv{DIGIT}+ { yylval.node = new BEEV::ASTNode(BEEV::_bm->CreateBVConst(yytext+2, 10)); return BVCONST_TOK;} */ +/* bv{DIGIT}+ { smtlval.node = new BEEV::ASTNode(BEEV::_bm->CreateBVConst(smttext+2, 10)); return BVCONST_TOK;} */ %} @@ -76,18 +76,18 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) %% [ \n\t\r\f] { /* sk'ip whitespace */ } -{DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK; } +{DIGIT}+ { smtlval.uintval = strtoul(smttext, NULL, 10); return NUMERAL_TOK; } - bv{DIGIT}+ { yylval.str = new std::string(yytext+2); return BVCONST_TOK; } + bv{DIGIT}+ { smtlval.str = new std::string(smttext+2); return BVCONST_TOK; } bit{DIGIT}+ { - char c = yytext[3]; + char c = smttext[3]; if (c == '1') { - yylval.node = new BEEV::ASTNode(SingleBitOne); + smtlval.node = new BEEV::ASTNode(SingleBitOne); } else { - yylval.node = new BEEV::ASTNode(SingleBitZero); + smtlval.node = new BEEV::ASTNode(SingleBitZero); } return BITCONST_TOK; }; @@ -102,24 +102,24 @@ bit{DIGIT}+ { _string_lit.end()); } "\\". { /* escape characters (like \n or \") */ _string_lit.insert(_string_lit.end(), - escapeChar(yytext[1])); } + escapeChar(smttext[1])); } "\"" { BEGIN INITIAL; /* return to normal mode */ - yylval.str = new std::string(_string_lit); + smtlval.str = new std::string(_string_lit); return STRING_TOK; } -. { _string_lit.insert(_string_lit.end(),*yytext); } +. { _string_lit.insert(_string_lit.end(),*smttext); } "{" { BEGIN USER_VALUE; _string_lit.erase(_string_lit.begin(), _string_lit.end()); } "\\"[{}] { /* escape characters */ - _string_lit.insert(_string_lit.end(),yytext[1]); } + _string_lit.insert(_string_lit.end(),smttext[1]); } "}" { BEGIN INITIAL; /* return to normal mode */ - yylval.str = new std::string(_string_lit); + smtlval.str = new std::string(_string_lit); return USER_VAL_TOK; } "\n" { _string_lit.insert(_string_lit.end(),'\n');} -. { _string_lit.insert(_string_lit.end(),*yytext); } +. { _string_lit.insert(_string_lit.end(),*smttext); } "BitVec" { return BITVEC_TOK;} "Array" { return ARRAY_TOK;} @@ -221,17 +221,17 @@ bit{DIGIT}+ { "boolbv" { return BOOL_TO_BV_TOK;} (({LETTER})|(_)({ANYTHING}))({ANYTHING})* { - BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); + BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(smttext); // Check valuesize to see if it's a prop var. I don't like doing // type determination in the lexer, but it's easier than rewriting // the whole grammar to eliminate the term/formula distinction. - yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); - //yylval.node = new BEEV::ASTNode(nptr); - if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE) + smtlval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); + //smtlval.node = new BEEV::ASTNode(nptr); + if ((smtlval.node)->GetType() == BEEV::BOOLEAN_TYPE) return FORMID_TOK; else return TERMID_TOK; } -. { yyerror("Illegal input character."); } +. { smterror("Illegal input character."); } %% diff --git a/parser/smtlib.y b/parser/smtlib.y index 3da4090..55fb325 100644 --- a/parser/smtlib.y +++ b/parser/smtlib.y @@ -42,17 +42,14 @@ // compile error) #undef __GNUC_MINOR__ - extern char* yytext; - extern int yylineno; + extern char* smttext; + extern int smtlineno; - //int yylineno; - - extern int yylex(void); + extern int smtlex(void); int yyerror(char *s) { - //yylineno = 0; - cout << "syntax error: line " << yylineno << "\n" << s << endl; - cout << " token: " << yytext << endl; + cout << "syntax error: line " << smtlineno << "\n" << s << endl; + cout << " token: " << smttext << endl; BEEV::FatalError(""); return 1; }