From: vijay_ganesh Date: Fri, 28 Aug 2009 18:24:24 +0000 (+0000) Subject: Minor changes to make scripts. Since files got moved around, the libstp.a was broken... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1539b287e7351e43d67c6929f6ec1a6f0b0fbe0e;p=francis%2Fstp.git Minor changes to make scripts. Since files got moved around, the libstp.a was broken. The c-api-tests were failing. everything seems to work now git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@148 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/Makefile b/Makefile index 9b84ae4..8f9931e 100644 --- a/Makefile +++ b/Makefile @@ -18,13 +18,15 @@ HEADERS=$(SRC)/c_interface/*.h .PHONY: all all: $(MAKE) -C $(SRC)/AST - $(MAKE) -C $(SRC)/sat simp + $(MAKE) -C $(SRC)/sat core +# $(MAKE) -C $(SRC)/sat simp +# $(MAKE) -C $(SRC)/sat unsound $(MAKE) -C $(SRC)/simplifier $(MAKE) -C $(SRC)/bitvec $(MAKE) -C $(SRC)/c_interface $(MAKE) -C $(SRC)/constantbv $(MAKE) -C $(SRC)/parser - $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/sat/*.a $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \ + $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \ $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(RANLIB) libstp.a @mkdir -p lib diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 9b84ae4..8f9931e 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -18,13 +18,15 @@ HEADERS=$(SRC)/c_interface/*.h .PHONY: all all: $(MAKE) -C $(SRC)/AST - $(MAKE) -C $(SRC)/sat simp + $(MAKE) -C $(SRC)/sat core +# $(MAKE) -C $(SRC)/sat simp +# $(MAKE) -C $(SRC)/sat unsound $(MAKE) -C $(SRC)/simplifier $(MAKE) -C $(SRC)/bitvec $(MAKE) -C $(SRC)/c_interface $(MAKE) -C $(SRC)/constantbv $(MAKE) -C $(SRC)/parser - $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/sat/*.a $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \ + $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \ $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(RANLIB) libstp.a @mkdir -p lib diff --git a/src/AST/AST.h b/src/AST/AST.h index 3274657..fb446ad 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -32,8 +32,9 @@ #include #include "ASTUtil.h" #include "ASTKind.h" -//#include "../sat/core/Solver.h" -#include "../sat/simp/SimpSolver.h" +#include "../sat/core/Solver.h" +//#include "../sat/simp/SimpSolver.h" +//#include "../sat/unsound/UnsoundSimpSolver.h" #include "../sat/core/SolverTypes.h" #include #ifndef NATIVE_C_ARITH diff --git a/src/AST/ASTKind.kinds b/src/AST/ASTKind.kinds index 985ee62..0257e96 100644 --- a/src/AST/ASTKind.kinds +++ b/src/AST/ASTKind.kinds @@ -1,5 +1,5 @@ #Please refer LICENSE FILE in the home directory for licensing information -# name minkids maxkids cat1 cat2 ... +# name minkids maxkids category1 category2 Categories: Term Form # Leaf nodes. @@ -60,6 +60,7 @@ NOR 1 - Form XOR 1 - Form IFF 1 - Form IMPLIES 2 2 Form +FOR 4 4 Form # array operations READ 2 2 Term diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index 94eaa58..5d1d0bc 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -121,6 +121,7 @@ bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll) //PrintActivityLevels_Of_SATVars("Before SAT:",newS); //ChangeActivityLevels_Of_SATVars(newS); //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS); + //newS.solve(); newS.solve(); //PrintActivityLevels_Of_SATVars("After SAT",newS); @@ -1186,7 +1187,9 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) int res; //solver instantiated here - MINISAT::SimpSolver newS; + MINISAT::Solver newS; + //MINISAT::SimpSolver newS; + //MINISAT::UnsoundSimpSolver newS; if (arrayread_refinement_flag) { counterexample_checking_during_refinement = true; diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex index de7f851..c515708 100644 --- a/src/parser/CVC.lex +++ b/src/parser/CVC.lex @@ -50,6 +50,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "NAND" { return NAND_TOK;} "NOR" { return NOR_TOK;} "NOT" { return NOT_TOK; } +"FOR" { return FOR_TOK; } "OR" { return OR_TOK; } "/=" { return NEQ_TOK; } ":=" { return ASSIGN_TOK;} diff --git a/src/parser/CVC.y b/src/parser/CVC.y index c58e175..c5801a3 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -56,6 +56,7 @@ using namespace std; %token AND_TOK "AND" %token OR_TOK "OR" %token NOT_TOK "NOT" +%token FOR_TOK "FOR" %token XOR_TOK "XOR" %token NAND_TOK "NAND" %token NOR_TOK "NOR" @@ -440,6 +441,22 @@ Formula : '(' Formula ')' { $$ = $2; } delete $1; delete $3; } + | FOR_TOK '(' Formula ';' Formula ';' Formula ')' '{' Formula '}' + { + //Allows a compact representation of + //parameterized set of formulas + // + //$1 is the initialization (this is an AND of + //formulas of the form var = constant) + // + //$2 is the constant bounding (this is an AND + //of formulas of the form var < constant). + // + //$3 is the increment (this is an AND of + //formulas of the form var = var + constant). + // + //$4 is the parameterized formula + } | NOT_TOK Formula { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$2)); diff --git a/src/parser/Makefile b/src/parser/Makefile index 43d99ee..e3e086a 100644 --- a/src/parser/Makefile +++ b/src/parser/Makefile @@ -5,8 +5,9 @@ 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 +LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv +#CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp +CFLAGS += -I../sat/mtl -I../sat/core -I../sat/unsound all: parseSMT.cpp lexSMT.cpp parseCVC.cpp lexCVC.cpp let-funcs.cpp parser parseCVC.o lexCVC.o let-funcs.o diff --git a/src/sat/Makefile b/src/sat/Makefile index a6aa9e6..d270dc8 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -4,7 +4,6 @@ core: .PHONY: simp simp: $(MAKE) -C simp lib all - .PHONY: unsound unsound: $(MAKE) -C unsound lib all @@ -14,4 +13,4 @@ clean: rm -rf *~ libminisat.a $(MAKE) -C core clean $(MAKE) -C simp clean - #$(MAKE) -C unsound clean + $(MAKE) -C unsound clean diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile index ea85050..aa15002 100644 --- a/src/sat/core/Makefile +++ b/src/sat/core/Makefile @@ -7,4 +7,6 @@ LFLAGS = -lz include ../mtl/template.mk all: + ranlib libminisat.a + cp *.or ../ cp libminisat.a ../ \ No newline at end of file diff --git a/src/sat/mtl/template.mk b/src/sat/mtl/template.mk index e60f2fb..4c27893 100644 --- a/src/sat/mtl/template.mk +++ b/src/sat/mtl/template.mk @@ -72,7 +72,7 @@ $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static: lib$(LIB).a lib$(LIB)d.a lib$(LIB)p.a: @echo Library: "$@ ( $^ )" @rm -f $@ - @ar cq $@ $^ + @ar cq $@ $^ ## Clean rule clean: diff --git a/src/sat/simp/Makefile b/src/sat/simp/Makefile index 26974d1..78c93ec 100644 --- a/src/sat/simp/Makefile +++ b/src/sat/simp/Makefile @@ -10,4 +10,6 @@ COBJS = $(addsuffix .o, $(basename $(CSRCS))) $(CORE)/Solver.o include ../mtl/template.mk all: - cp libminisat.a ../ \ No newline at end of file + ranlib libminisat.a + cp *.o ../ + cp libminisat.a ../ diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 5d75708..d6e9ea9 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -140,7 +140,7 @@ int BeevMgr::TermOrder(const ASTNode& a, const ASTNode& b) //a is of the form var, and b is const if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && (k2 == BVCONST))) -// || + // || // k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST))) return 1; diff --git a/tests/c-api-tests/array-cvcl-02.c b/tests/c-api-tests/array-cvcl-02.c index 2855671..18d4d24 100644 --- a/tests/c-api-tests/array-cvcl-02.c +++ b/tests/c-api-tests/array-cvcl-02.c @@ -27,8 +27,9 @@ int main() { Expr a_of_i = vc_bvSignExtend(vc, vc_readExpr(vc,cvcl_array,i32), 32); - Expr a_of_i_eq_11 = vc_eqExpr(vc, a_of_i, - vc_bvConstExprFromInt(vc, 32, 11)); + Expr a_of_i_eq_11 = vc_eqExpr(vc, + vc_bvConcatExpr(vc,i32,a_of_i), + vc_bvConstExprFromInt(vc, 64, 11)); vc_assertFormula(vc, in_bounds); vc_assertFormula(vc, a_of_i_eq_11);