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.
+++ /dev/null
- # 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)
-
-
"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",
********************************************************************/
#include <iostream>
#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
[\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;}
<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */}
// 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."); }
%%
// 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 */
};
+
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 .#*
+
+++ /dev/null
-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 .#*
//#include <zlib.h>
#include <stdio.h>
#include "../AST/AST.h"
-#include "parsePL_defs.h"
#include "../sat/core/Solver.h"
#include "../sat/core/SolverTypes.h"
//#include "../sat/VarOrder.h"
/* GLOBAL FUNCTION: parser
*/
-extern int yyparse();
-//extern int smtlibparse();
+extern int smtparse();
+extern int cvcparse();
+
/* GLOBAL VARS: Some global vars for the Main function.
*
******************************************************************************/
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
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] == '-') {
break;
case 'n':
BEEV::print_output = true;
+ break;
+ case 'm':
+ smtlibParser=true;
break;
case 'p':
BEEV::print_counterexample = true;
}
} 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("");
+ }
+ }
}
}
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
// -*- c++ -*-
#include <iostream>
#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;
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;} */
%}
%%
[ \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;
};
_string_lit.end()); }
<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */
_string_lit.insert(_string_lit.end(),
- escapeChar(yytext[1])); }
+ escapeChar(smttext[1])); }
<STRING_LITERAL>"\"" { BEGIN INITIAL; /* return to normal mode */
- yylval.str = new std::string(_string_lit);
+ smtlval.str = new std::string(_string_lit);
return STRING_TOK; }
-<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*yytext); }
+<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*smttext); }
<INITIAL>"{" { BEGIN USER_VALUE;
_string_lit.erase(_string_lit.begin(),
_string_lit.end()); }
<USER_VALUE>"\\"[{}] { /* escape characters */
- _string_lit.insert(_string_lit.end(),yytext[1]); }
+ _string_lit.insert(_string_lit.end(),smttext[1]); }
<USER_VALUE>"}" { BEGIN INITIAL; /* return to normal mode */
- yylval.str = new std::string(_string_lit);
+ smtlval.str = new std::string(_string_lit);
return USER_VAL_TOK; }
<USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n');}
-<USER_VALUE>. { _string_lit.insert(_string_lit.end(),*yytext); }
+<USER_VALUE>. { _string_lit.insert(_string_lit.end(),*smttext); }
"BitVec" { return BITVEC_TOK;}
"Array" { return ARRAY_TOK;}
"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."); }
%%
// 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;
}
projects / francis / stp.git / commitdiff