From 8eb41135be1054f2cb46ba9875e60f86649f59a7 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 21 Aug 2009 22:27:18 +0000 Subject: [PATCH] git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@138 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile | 153 ++++++++++++++++++++++++++++++++ scripts/Makefile.in | 2 +- scripts/run_smt_tests.pl | 4 +- src/AST/AST.cpp | 44 ++++----- src/AST/AST.h | 2 +- src/AST/ASTUtil.cpp | 2 +- src/AST/ASTUtil.h | 41 ++++----- src/AST/SimpBool.cpp | 4 +- src/AST/ToCNF.cpp | 12 +-- src/AST/ToSAT.cpp | 65 +++++++------- src/AST/Transform.cpp | 2 +- src/c_interface/c_interface.cpp | 56 +++++------- src/parser/CVC.y | 2 +- src/parser/main.cpp | 59 +++++------- src/simplifier/bvsolver.cpp | 36 ++++++-- src/simplifier/simplifier.cpp | 36 ++++---- 16 files changed, 329 insertions(+), 191 deletions(-) create mode 100644 Makefile diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..f7d8638 --- /dev/null +++ b/Makefile @@ -0,0 +1,153 @@ + # STP (Simple Theorem Prover) top level makefile + # + # To make in debug mode, type 'make "OPTIMIZE=-g" + # To make in optimized mode, type 'make "OPTIMIZE=-O3" + + +include scripts/Makefile.common scripts/config.info + +BIN_DIR=$(PREFIX)/bin +LIB_DIR=$(PREFIX)/lib +INCLUDE_DIR=$(PREFIX)/include/stp + +SRC=src +BINARIES=bin/stp +LIBRARIES=lib/libstp.a +HEADERS=$(SRC)/c_interface/*.h + +.PHONY: all +all: + $(MAKE) -C $(SRC)/AST + $(MAKE) -C $(SRC)/sat core + $(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 \ + $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o + $(RANLIB) libstp.a + @mkdir -p lib + @mv libstp.a lib/ + @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 bin/stp + rm -rf *.log + #rm -rf Makefile + #rm -rf config.info + rm -f TAGS + $(MAKE) clean -C $(SRC)/AST + $(MAKE) clean -C $(SRC)/sat + $(MAKE) clean -C $(SRC)/simplifier + $(MAKE) clean -C $(SRC)/bitvec + $(MAKE) clean -C $(SRC)/parser + $(MAKE) clean -C $(SRC)/c_interface + $(MAKE) clean -C $(SRC)/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_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: regress +regress: + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + scripts/run_cvc_tests.pl $(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) + +# The higher the level, the more tests are run (3 = all) +REGRESS_LEVEL=4 +REGRESS_TESTS=$(REGRESS_TESTS0) +#REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log" +PROGNAME=bin/stp +ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) + +.PHONY: regressbigarray +regressbigarray: + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + scripts/run_bigarray_tests.pl $(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) + +.PHONY: regress_smt +regress_smt: + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + scripts/run_smt_tests.pl $(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) + + +.PHONY: regressall +regressall: + $(MAKE) regress + +GRIND_LOG = `date +%Y-%m-%d`"-grind.log" +GRINDPROG = valgrind --leak-check=full --undef-value-errors=no +GRIND_TAR = $(BIN_DIR)/stp -d +GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" +GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS) + + +.PHONY: grind +grind: + + $(MAKE) install CFLAGS="-ggdb -pg -g" + @echo "*********************************************************" \ + | tee -a $(GRIND_LOG) + @echo "Starting tests at" `date` | tee -a $(GRIND_LOG) + @echo "*********************************************************" \ + | tee -a $(GRIND_LOG) + scripts/run_cvc_tests.pl $(GRIND_OPTIONS) 2>&1 | tee -a $(GRIND_LOG); [ $${PIPESTATUS[0]} -eq 0 ] + @echo "*********************************************************" \ + | tee -a $(GRIND_LOG) + @echo "Output is saved in $(GRIND_LOG)" | tee -a $(GRIND_LOG) + @echo "*********************************************************" \ + | tee -a $(GRIND_LOG) \ No newline at end of file diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 9b84ae4..f7d8638 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -18,7 +18,7 @@ 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)/simplifier $(MAKE) -C $(SRC)/bitvec $(MAKE) -C $(SRC)/c_interface diff --git a/scripts/run_smt_tests.pl b/scripts/run_smt_tests.pl index 386c367..c686c91 100755 --- a/scripts/run_smt_tests.pl +++ b/scripts/run_smt_tests.pl @@ -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 -m", # Program names + "vc" => $pwd . "/bin/stp -d -m", # Program names #"vc" => "valgrind --leak-check=full /home/vganesh/stp/bin/stp", # Program names "pfc" => "true", "stptestpath" => "stp/smt_tests", @@ -82,7 +82,7 @@ my %optionsDefault = ("level" => 4, # Runtime limit; 0 = no limit "time" => 60, # Additional command line options to stp - "stpOptions" => "-d -f"); + "stpOptions" => "-d"); # Database of command line options. Initially, they are undefined my %options = (); diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 12bd650..e3a52a6 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -18,47 +18,41 @@ namespace BEEV //here // //collect statistics on certain functions -bool stats = false; +bool stats_flag = false; //print DAG nodes -bool print_nodes = false; -//tentative global var to allow for variable activity optimization -//in the SAT solver. deprecated. -bool variable_activity_optimize = false; +bool print_nodes_flag = false; //run STP in optimized mode -bool optimize = true; +bool optimize_flag = true; //do sat refinement, i.e. underconstraint the problem, and feed to //SAT. if this works, great. else, add a set of suitable constraints //to re-constraint the problem correctly, and call SAT again, until //all constraints have been added. -bool arrayread_refinement = true; +bool arrayread_refinement_flag = true; //flag to control write refinement -bool arraywrite_refinement = true; +bool arraywrite_refinement_flag = true; //check the counterexample against the original input to STP -bool check_counterexample = false; +bool check_counterexample_flag = false; //construct the counterexample in terms of original variable based //on the counterexample returned by SAT solver -bool construct_counterexample = true; -bool print_counterexample = false; -bool print_binary = false; +bool construct_counterexample_flag = true; +bool print_counterexample_flag = false; +bool print_binary_flag = false; //if this option is true then print the way dawson wants using a //different printer. do not use this printer. -bool print_arrayval_declaredorder = false; +bool print_arrayval_declaredorder_flag = false; //flag to decide whether to print "valid/invalid" or not -bool print_output = false; -//do linear search in the array values of an input array. experimental -bool linear_search = false; +bool print_output_flag = false; //print the variable order chosen by the sat solver while it is //solving. -bool print_sat_varorder = false; +bool print_sat_varorder_flag = false; //turn on word level bitvector solver -bool wordlevel_solve = true; +bool wordlevel_solve_flag = true; //turn off XOR flattening -bool xor_flatten = false; - -//the smtlib parser has been turned on -bool smtlib_parser_enable = false; +bool xor_flatten_flag = false; +//Flag to switch on the smtlib parser +bool smtlib_parser_flag = false; //print the input back -bool print_STPinput_back = false; +bool print_STPinput_back_flag = false; enum inputStatus input_status = NOT_DECLARED; @@ -1606,13 +1600,13 @@ ASTNode BeevMgr::NewVar(unsigned int value) //prints statistics for the ASTNode void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a) { - if (!stats) + if (!stats_flag) return; StatInfoSet.clear(); //print node size: cout << endl << "Printing: " << c; - if (print_nodes) + if (print_nodes_flag) { //a.PL_Print(cout,0); //cout << endl; diff --git a/src/AST/AST.h b/src/AST/AST.h index 3fe3b3b..773406c 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -743,7 +743,7 @@ private: unsigned char *res; const char *prefix; - if(print_binary) { + if(print_binary_flag) { res = CONSTANTBV::BitVector_to_Bin(_bvconst); if (c_friendly) { diff --git a/src/AST/ASTUtil.cpp b/src/AST/ASTUtil.cpp index 7fd98e6..435c8e0 100644 --- a/src/AST/ASTUtil.cpp +++ b/src/AST/ASTUtil.cpp @@ -33,7 +33,7 @@ void CountersAndStats(const char * functionname) { static function_counters s; - if (stats) + if (stats_flag) { if (!strcmp(functionname, "print_func_stats")) diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h index bfa8932..8e0cf13 100644 --- a/src/AST/ASTUtil.h +++ b/src/AST/ASTUtil.h @@ -35,48 +35,43 @@ namespace BEEV { //here // //collect statistics on certain functions - extern bool stats; + extern bool stats_flag; //print DAG nodes - extern bool print_nodes; - //tentative global var to allow for variable activity optimization - //in the SAT solver. deprecated. - extern bool variable_activity_optimize; + extern bool print_nodes_flag; //run STP in optimized mode - extern bool optimize; + extern bool optimize_flag; //do sat refinement, i.e. underconstraint the problem, and feed to //SAT. if this works, great. else, add a set of suitable constraints //to re-constraint the problem correctly, and call SAT again, until //all constraints have been added. - extern bool arrayread_refinement; + extern bool arrayread_refinement_flag; //switch to control write refinements - extern bool arraywrite_refinement; + extern bool arraywrite_refinement_flag; //check the counterexample against the original input to STP - extern bool check_counterexample; + extern bool check_counterexample_flag; //construct the counterexample in terms of original variable based //on the counterexample returned by SAT solver - extern bool construct_counterexample; - extern bool print_counterexample; - extern bool print_binary; + extern bool construct_counterexample_flag; + extern bool print_counterexample_flag; + extern bool print_binary_flag; //if this option is true then print the way dawson wants using a //different printer. do not use this printer. - extern bool print_arrayval_declaredorder; + extern bool print_arrayval_declaredorder_flag; //flag to decide whether to print "valid/invalid" or not - extern bool print_output; - //do linear search in the array values of an input array. experimental - extern bool linear_search; + extern bool print_output_flag; //print the variable order chosen by the sat solver while it is //solving. - extern bool print_sat_varorder; + extern bool print_sat_varorder_flag; //turn on word level bitvector solver - extern bool wordlevel_solve; + extern bool wordlevel_solve_flag; //XOR flattening optimizations. - extern bool xor_flatten; + extern bool xor_flatten_flag; //this flag indicates that the BVSolver() succeeded - extern bool toplevel_solved; - //the smtlib parser has been turned on - extern bool smtlib_parser_enable; + extern bool toplevel_solved_flag; //print the input back - extern bool print_STPinput_back; + extern bool print_STPinput_back_flag; + //Flag to switch on the smtlib parser + extern bool smtlib_parser_flag; enum inputStatus { diff --git a/src/AST/SimpBool.cpp b/src/AST/SimpBool.cpp index 85e1916..1e06da0 100644 --- a/src/AST/SimpBool.cpp +++ b/src/AST/SimpBool.cpp @@ -230,7 +230,7 @@ ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, ASTVec &children) ASTVec new_children; ASTVec flat_children; - if (xor_flatten) + if (xor_flatten_flag) { flat_children = FlattenKind(k, children); } @@ -331,7 +331,7 @@ ASTNode BeevMgr::CreateSimpXor(ASTVec &children) ASTVec flat_children; // empty vector ASTVec::const_iterator it_end = children.end(); - if (xor_flatten) + if (xor_flatten_flag) { flat_children = FlattenKind(XOR, children); } diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp index 672fd40..76daf4f 100644 --- a/src/AST/ToCNF.cpp +++ b/src/AST/ToCNF.cpp @@ -1778,7 +1778,7 @@ int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode BBFormula = BBForm(q); CNFMgr* cm = new CNFMgr(this); ClauseList* cl = cm->convertToCNF(BBFormula); - if (stats) + if (stats_flag) cerr << "Number of clauses:" << cl->size() << endl; //PrintClauseList(cout, *cl); bool sat = toSATandSolve(newS, *cl); @@ -1794,7 +1794,7 @@ int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const { CounterExampleMap.clear(); ConstructCounterExample(newS); - if (stats && print_nodes) + if (stats_flag && print_nodes_flag) { PrintSATModel(newS); } @@ -1827,13 +1827,13 @@ int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const // counterexample is bogus: flag it else { - if (stats && print_nodes) + if (stats_flag && print_nodes_flag) { cout << "Supposedly bogus one: \n"; - bool tmp = print_counterexample; - print_counterexample = true; + bool tmp = print_counterexample_flag; + print_counterexample_flag = true; PrintCounterExample(true); - print_counterexample = tmp; + print_counterexample_flag = tmp; } return 2; diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index c1a78b7..3cecef5 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -134,7 +134,7 @@ bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll) // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver void BeevMgr::PrintStats(MINISAT::Solver& s) { - if (!stats) + if (!stats_flag) return; double cpu_time = MINISAT::cpuTime(); uint64_t mem_used = MINISAT::memUsed(); @@ -157,7 +157,7 @@ void BeevMgr::PrintSATModel(MINISAT::Solver& newS) // FIXME: Don't put tests like this in the print functions. The print functions // should print unconditionally. Put a conditional around the call if you don't // want them to print - if (!(stats && print_nodes)) + if (!(stats_flag && print_nodes_flag)) return; int num_vars = newS.nVars(); @@ -320,7 +320,7 @@ void BeevMgr::ConstructCounterExample(MINISAT::Solver& newS) if (!newS.okay()) return; - if (!construct_counterexample) + if (!construct_counterexample_flag) return; CopySolverMap_To_CounterExample(); @@ -900,7 +900,7 @@ void BeevMgr::CheckCounterExample(bool t) // the flag in order to make it actualy happen! printf("checking counterexample\n"); - if (!check_counterexample) + if (!check_counterexample_flag) { return; } @@ -932,7 +932,7 @@ void BeevMgr::PrintCounterExample(bool t, std::ostream& os) //global command-line option // FIXME: This should always print the counterexample. If you want // to turn it off, check the switch at the point of call. - if (!print_counterexample) + if (!print_counterexample_flag) { return; } @@ -945,7 +945,7 @@ void BeevMgr::PrintCounterExample(bool t, std::ostream& os) //if this option is true then print the way dawson wants using a //different printer. do not use this printer. - if (print_arrayval_declaredorder) + if (print_arrayval_declaredorder_flag) { return; } @@ -1006,7 +1006,7 @@ void BeevMgr::PrintCounterExample_InOrder(bool t) //want both counterexample printers to print at the sametime. // FIXME: This should always print the counterexample. If you want // to turn it off, check the switch at the point of call. - if (print_counterexample) + if (print_counterexample_flag) return; //input is valid, no counterexample to print @@ -1015,7 +1015,7 @@ void BeevMgr::PrintCounterExample_InOrder(bool t) //print if the commandline option is '-q'. allows printing the //counterexample in order. - if (!print_arrayval_declaredorder) + if (!print_arrayval_declaredorder_flag) return; //t is true if SAT solver generated a counterexample, else it is @@ -1125,11 +1125,11 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) q = newq; newq = CreateSubstitutionMap(newq); //printf("##################################################\n"); - //ASTNodeStats("after pure substitution: ", newq); + ASTNodeStats("after pure substitution: ", newq); newq = SimplifyFormula_TopLevel(newq, false); - //ASTNodeStats("after simplification: ", newq); + ASTNodeStats("after simplification: ", newq); newq = bvsolver.TopLevelBVSolve(newq); - //ASTNodeStats("after solving: ", newq); + ASTNodeStats("after solving: ", newq); } while (q != newq); ASTNodeStats("Before SimplifyWrites_Inplace begins: ", newq); @@ -1141,15 +1141,15 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) { q = newq; newq = CreateSubstitutionMap(newq); - //ASTNodeStats("after pure substitution: ", newq); + ASTNodeStats("after pure substitution: ", newq); newq = SimplifyFormula_TopLevel(newq, false); - //ASTNodeStats("after simplification: ", newq); + ASTNodeStats("after simplification: ", newq); newq = bvsolver.TopLevelBVSolve(newq); - //ASTNodeStats("after solving: ", newq); + ASTNodeStats("after solving: ", newq); } while (q != newq); ASTNodeStats("After SimplifyWrites_Inplace: ", newq); - start_abstracting = (arraywrite_refinement) ? true : false; + start_abstracting = (arraywrite_refinement_flag) ? true : false; SimplifyWrites_InPlace_Flag = false; Begin_RemoveWrites = (start_abstracting) ? false : true; if (start_abstracting) @@ -1186,8 +1186,8 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) int res; //solver instantiated here - MINISAT::SimpSolver newS; - if (arrayread_refinement) + MINISAT::Solver newS; + if (arrayread_refinement_flag) { counterexample_checking_during_refinement = true; } @@ -1244,7 +1244,7 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) // all the false axioms each time). int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input) { //printf("doing array read refinement\n"); - if (!arrayread_refinement) + if (!arrayread_refinement_flag) FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); ASTVec FalseAxiomsVec, RemainingAxiomsVec; @@ -1580,28 +1580,27 @@ ASTNode BeevMgr::BoolVectoBVConst(hash_map * w, unsigned int l) //This function prints the output of the STP solver void BeevMgr::PrintOutput(bool true_iff_valid) { - //self-explanatory - if (print_output) + if (print_output_flag) { - if (smtlib_parser_enable) + if (smtlib_parser_flag) { - if (true_iff_valid && (BEEV::input_status == TO_BE_SATISFIABLE)) - { - cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl; - } - else if (!true_iff_valid && (BEEV::input_status == TO_BE_UNSATISFIABLE)) - { - cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; - } + if (true_iff_valid && (BEEV::input_status == TO_BE_SATISFIABLE)) + { + cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl; + } + else if (!true_iff_valid && (BEEV::input_status == TO_BE_UNSATISFIABLE)) + { + cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; + } } } if (true_iff_valid) { ValidFlag = true; - if (print_output) + if (print_output_flag) { - if (smtlib_parser_enable) + if (smtlib_parser_flag) cout << "unsat\n"; else cout << "Valid.\n"; @@ -1610,9 +1609,9 @@ void BeevMgr::PrintOutput(bool true_iff_valid) else { ValidFlag = false; - if (print_output) + if (print_output_flag) { - if (smtlib_parser_enable) + if (smtlib_parser_flag) cout << "sat\n"; else cout << "Invalid.\n"; diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index 41db3c0..771e25c 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -449,7 +449,7 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term) _introduced_symbols.insert(CurrentSymbol); assert(BVTypeCheck(ite)); - if (arrayread_refinement) + if (arrayread_refinement_flag) { // ite is really a variable here; it is an ite in the // else-branch diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 2dc0a54..8fc74d1 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -23,7 +23,7 @@ typedef BEEV::ASTVec nodelist; typedef BEEV::CompleteCounterExample* CompleteCEStar; BEEV::ASTVec *decls = NULL; //vector created_exprs; -bool cinterface_exprdelete_on = false; +bool cinterface_exprdelete_on_flag = false; /* GLOBAL FUNCTION: parser */ @@ -39,65 +39,60 @@ void vc_setFlags(char c) { helpstring += "-c : construct counterexample\n"; helpstring += "-d : check counterexample\n"; helpstring += "-p : print counterexample\n"; + helpstring += "-y : print counterexample in binary\n"; + helpstring += "-b : STP input read back\n"; + helpstring += "-x : flatten nested XORs\n"; helpstring += "-h : help\n"; + helpstring += "-m : use the SMTLIB parser\n"; switch(c) { case 'a' : - BEEV::optimize = false; - BEEV::wordlevel_solve = false; + BEEV::optimize_flag = false; + BEEV::wordlevel_solve_flag = false; break; case 'b': - BEEV::print_STPinput_back = true; + BEEV::print_STPinput_back_flag = true; break; case 'c': - BEEV::construct_counterexample = true; + BEEV::construct_counterexample_flag = true; break; case 'd': - BEEV::construct_counterexample = true; - BEEV::check_counterexample = true; - break; - case 'e': - BEEV::variable_activity_optimize = true; - break; - case 'f': - BEEV::smtlib_parser_enable = true; + BEEV::construct_counterexample_flag = true; + BEEV::check_counterexample_flag = true; break; case 'h': cout << helpstring; BEEV::FatalError(""); break; - case 'l' : - BEEV::linear_search = true; - break; case 'n': - BEEV::print_output = true; + BEEV::print_output_flag = true; break; case 'p': - BEEV::print_counterexample = true; + BEEV::print_counterexample_flag = true; break; case 'q': - BEEV::print_arrayval_declaredorder = true; + BEEV::print_arrayval_declaredorder_flag = true; break; case 'r': - BEEV::arrayread_refinement = false; + BEEV::arrayread_refinement_flag = false; break; case 's' : - BEEV::stats = true; + BEEV::stats_flag = true; break; case 'u': - BEEV::arraywrite_refinement = true; + BEEV::arraywrite_refinement_flag = true; break; case 'v' : - BEEV::print_nodes = true; + BEEV::print_nodes_flag = true; break; case 'w': - BEEV::wordlevel_solve = false; + BEEV::wordlevel_solve_flag = false; break; case 'x': - cinterface_exprdelete_on = true; + cinterface_exprdelete_on_flag = true; break; case 'z': - BEEV::print_sat_varorder = true; + BEEV::print_sat_varorder_flag = true; break; default: std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n"; @@ -110,14 +105,11 @@ void vc_setFlags(char c) { //Create a validity Checker. This is the global BeevMgr VC vc_createValidityChecker(void) { vc_setFlags('d'); -#ifdef NATIVE_C_ARITH -#else CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); if(0 != c) { cout << CONSTANTBV::BitVector_Error(c) << endl; return 0; } -#endif bmstar bm = new BEEV::BeevMgr(); decls = new BEEV::ASTVec(); //created_exprs.clear(); @@ -266,7 +258,7 @@ void vc_printCounterExampleToBuffer(VC vc, char **buf, unsigned long *len) { // formate the state of the query std::ostringstream os; - BEEV::print_counterexample = true; + BEEV::print_counterexample_flag = true; os << "COUNTEREXAMPLE BEGIN: \n"; b->PrintCounterExample(true,os); os << "COUNTEREXAMPLE END: \n"; @@ -426,7 +418,7 @@ void vc_pop(VC vc) { void vc_printCounterExample(VC vc) { bmstar b = (bmstar)vc; - BEEV::print_counterexample = true; + BEEV::print_counterexample_flag = true; cout << "COUNTEREXAMPLE BEGIN: \n"; b->PrintCounterExample(true); cout << "COUNTEREXAMPLE END: \n"; @@ -1629,7 +1621,7 @@ int getIWidth (Expr ex) { void vc_printCounterExampleFile(VC vc, int fd) { fdostream os(fd); bmstar b = (bmstar)vc; - BEEV::print_counterexample = true; + BEEV::print_counterexample_flag = true; os << "COUNTEREXAMPLE BEGIN: \n"; b->PrintCounterExample(true, os); os << "COUNTEREXAMPLE END: \n"; diff --git a/src/parser/CVC.y b/src/parser/CVC.y index 1be1066..c58e175 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -169,7 +169,7 @@ cmd : other_cmd counterexample : COUNTEREXAMPLE_TOK ';' { - BEEV::print_counterexample = true; + BEEV::print_counterexample_flag = true; BEEV::globalBeevMgr_for_parser->PrintCounterExample(true); } ; diff --git a/src/parser/main.cpp b/src/parser/main.cpp index 6b69cf7..9b2b656 100644 --- a/src/parser/main.cpp +++ b/src/parser/main.cpp @@ -92,31 +92,21 @@ int main(int argc, char ** argv) { 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] == '-') { switch(argv[i][1]) { case 'a' : - BEEV::optimize = false; - BEEV::wordlevel_solve = false; + BEEV::optimize_flag = false; break; case 'b': - BEEV::print_STPinput_back = true; + BEEV::print_STPinput_back_flag = true; break; case 'c': - BEEV::construct_counterexample = true; + BEEV::construct_counterexample_flag = true; break; case 'd': - BEEV::construct_counterexample = true; - BEEV::check_counterexample = true; - break; - case 'e': - BEEV::variable_activity_optimize = true; - break; - case 'f': - BEEV::smtlib_parser_enable = true; + BEEV::construct_counterexample_flag = true; + BEEV::check_counterexample_flag = true; break; case 'h': fprintf(stderr,usage,prog); @@ -124,44 +114,41 @@ int main(int argc, char ** argv) { //BEEV::FatalError(""); return -1; break; - case 'l' : - BEEV::linear_search = true; - break; case 'n': - BEEV::print_output = true; + BEEV::print_output_flag = true; break; case 'm': - smtlibParser=true; + BEEV::smtlib_parser_flag=true; break; case 'p': - BEEV::print_counterexample = true; + BEEV::print_counterexample_flag = true; break; case 'y': - BEEV::print_binary = true; + BEEV::print_binary_flag = true; break; case 'q': - BEEV::print_arrayval_declaredorder = true; + BEEV::print_arrayval_declaredorder_flag = true; break; case 'r': - BEEV::arrayread_refinement = false; + BEEV::arrayread_refinement_flag = false; break; case 's' : - BEEV::stats = true; + BEEV::stats_flag = true; break; case 'u': - BEEV::arraywrite_refinement = false; + BEEV::arraywrite_refinement_flag = false; break; case 'v' : - BEEV::print_nodes = true; + BEEV::print_nodes_flag = true; break; case 'w': - BEEV::wordlevel_solve = false; + BEEV::wordlevel_solve_flag = false; break; case 'x': - BEEV::xor_flatten = true; + BEEV::xor_flatten_flag = true; break; case 'z': - BEEV::print_sat_varorder = true; + BEEV::print_sat_varorder_flag = true; break; default: fprintf(stderr,usage,prog); @@ -180,7 +167,7 @@ int main(int argc, char ** argv) { } else { infile = argv[i]; - if (smtlibParser) + if (BEEV::smtlib_parser_flag) { smtin = fopen(infile,"r"); if(smtin == NULL) @@ -201,24 +188,20 @@ int main(int argc, char ** argv) { } } -#ifdef NATIVE_C_ARITH -#else CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); if(0 != c) { cout << CONSTANTBV::BitVector_Error(c) << endl; return 0; } -#endif //want to print the output always from the commandline. - BEEV::print_output = true; + BEEV::print_output_flag = true; BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr(); BEEV::SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); BEEV::SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); - //BEEV::smtlib_parser_enable = true; - - if (smtlibParser) + + if (BEEV::smtlib_parser_flag) smtparse(); else cvcparse(); diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index 2447789..cd1ff6c 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -310,7 +310,7 @@ ASTNode BVSolver::BVSolve_Odd(const ASTNode& input) { ASTNode eq = input; //cerr << "Input to BVSolve_Odd()" << eq << endl; - if (!(wordlevel_solve && EQ == eq.GetKind())) + if (!(wordlevel_solve_flag && EQ == eq.GetKind())) { return input; } @@ -385,12 +385,31 @@ ASTNode BVSolver::BVSolve_Odd(const ASTNode& input) output = ASTTrue; break; } +// case READ: +// { +// if(BVCONST != lhs[1].GetKind() || READ != rhs.GetKind() || +// BVCONST != rhs[1].GetKind() || lhs == rhs) +// { +// return eq; +// } +// else +// { +// DoNotSolve_TheseVars.insert(lhs); +// if (!_bm->UpdateSolverMap(lhs, rhs)) +// { +// return eq; +// } + +// output = ASTTrue; +// break; +// } +// } case BVEXTRACT: { ASTNode zero = _bm->CreateZeroConst(32); - if (!(SYMBOL == lhs[0].GetKind() && BVCONST == lhs[1].GetKind() && zero == lhs[2] && !_bm->VarSeenInTerm(lhs[0], rhs) && !DoNotSolveThis( - lhs[0]))) + if (!(SYMBOL == lhs[0].GetKind() && BVCONST == lhs[1].GetKind() && + zero == lhs[2] && !_bm->VarSeenInTerm(lhs[0], rhs) && !DoNotSolveThis(lhs[0]))) { return eq; } @@ -505,7 +524,7 @@ ASTNode BVSolver::NewVar(unsigned int n) //the formula ASTNode BVSolver::TopLevelBVSolve(const ASTNode& input) { - if (!wordlevel_solve) + if (!wordlevel_solve_flag) { return input; } @@ -532,9 +551,8 @@ ASTNode BVSolver::TopLevelBVSolve(const ASTNode& input) ASTNode solved = ASTFalse; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { - //_bm->ASTNodeStats("Printing before calling simplifyformula inside the solver:", *it); - ASTNode aaa = (ASTTrue == solved && EQ == it->GetKind()) ? _bm->SimplifyFormula(*it, false) : *it; - //ASTNode aaa = *it; + //_bm->ASTNodeStats("Printing before calling simplifyformula inside the solver:", *it); + ASTNode aaa = (ASTTrue == solved && EQ == it->GetKind()) ? _bm->SimplifyFormula(*it, false) : *it; //_bm->ASTNodeStats("Printing after calling simplifyformula inside the solver:", aaa); aaa = BVSolve_Odd(aaa); //_bm->ASTNodeStats("Printing after oddsolver:", aaa); @@ -578,7 +596,7 @@ ASTNode BVSolver::CheckEvenEqn(const ASTNode& input, bool& evenflag) { ASTNode eq = input; //cerr << "Input to BVSolve_Odd()" << eq << endl; - if (!(wordlevel_solve && EQ == eq.GetKind())) + if (!(wordlevel_solve_flag && EQ == eq.GetKind())) { evenflag = false; return eq; @@ -634,7 +652,7 @@ ASTNode BVSolver::CheckEvenEqn(const ASTNode& input, bool& evenflag) //solve an eqn whose monomials have only even coefficients ASTNode BVSolver::BVSolve_Even(const ASTNode& input) { - if (!wordlevel_solve) + if (!wordlevel_solve_flag) { return input; } diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 9f94bd2..9ad8664 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -138,7 +138,10 @@ int BeevMgr::TermOrder(const ASTNode& a, const ASTNode& b) //a is of the form READ(Arr,const), and b is const, or //a is of the form var, and b is const - if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST) && (k2 == BVCONST)) + 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; if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2)) @@ -206,7 +209,7 @@ ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg) ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) { - if (!optimize) + if (!optimize_flag) return b; Kind kind = b.GetKind(); @@ -271,7 +274,7 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg) { - if (!optimize) + if (!optimize_flag) { return a; } @@ -550,7 +553,7 @@ ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in) { CountersAndStats("ITEOpts_InEqs"); - if (!(EQ == in.GetKind() && optimize)) + if (!(EQ == in.GetKind() && optimize_flag)) { return in; } @@ -642,7 +645,7 @@ ASTNode BeevMgr::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2) Kind k1 = in1.GetKind(); Kind k2 = in2.GetKind(); - if (!optimize) + if (!optimize_flag) { return CreateNode(EQ, in1, in2); } @@ -667,7 +670,7 @@ ASTNode BeevMgr::CreateSimplifiedTermITE(const ASTNode& in0, const ASTNode& in1, ASTNode t1 = in1; ASTNode t2 = in2; CountersAndStats("CreateSimplifiedITE"); - if (!optimize) + if (!optimize_flag) { if (t1.GetValueWidth() != t2.GetValueWidth()) { @@ -707,7 +710,7 @@ ASTNode BeevMgr::CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& i ASTNode t2 = in2; CountersAndStats("CreateSimplifiedFormulaITE"); - if (optimize) + if (optimize_flag) { if (t0 == ASTTrue) return t1; @@ -1106,7 +1109,7 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg) { - if (!optimize) + if (!optimize_flag) return b; ASTNode output; @@ -1241,7 +1244,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) ASTNode inputterm(actualInputterm); // mutable local copy. //cout << "SimplifyTerm: input: " << a << endl; - if (!optimize) + if (!optimize_flag) { return inputterm; } @@ -2011,7 +2014,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) ASTNode BeevMgr::SimplifyTermAux(const ASTNode& inputterm) { //cout << "SimplifyTerm: input: " << a << endl; - if (!optimize) + if (!optimize_flag) { return inputterm; } @@ -2022,7 +2025,7 @@ ASTNode BeevMgr::SimplifyTermAux(const ASTNode& inputterm) //######################################## //######################################## - if (wordlevel_solve && CheckSolverMap(inputterm, output)) + if (wordlevel_solve_flag && CheckSolverMap(inputterm, output)) { return SimplifyTermAux(output); } @@ -3508,8 +3511,8 @@ bool BeevMgr::BVConstIsOdd(const ASTNode& c) //The big substitution function ASTNode BeevMgr::CreateSubstitutionMap(const ASTNode& a) { - if (!optimize) - return a; + if (!wordlevel_solve_flag) + return a; ASTNode output = a; //if the variable has been solved for, then simply return it @@ -3552,16 +3555,17 @@ ASTNode BeevMgr::CreateSubstitutionMap(const ASTNode& a) SortByArith(c); FillUp_ArrReadIndex_Vec(c[0], c[1]); - if (SYMBOL == c[0].GetKind() && VarSeenInTerm(c[0], SimplifyTermAux(c[1]))) + ASTNode c1 = SimplifyTermAux(c[1]); + if (SYMBOL == c[0].GetKind() && VarSeenInTerm(c[0], c1)) { return a; } - if (1 == TermOrder(c[0], c[1]) && READ == c[0].GetKind() && VarSeenInTerm(c[0][0], SimplifyTermAux(c[1]))) + if (1 == TermOrder(c[0], c[1]) && READ == c[0].GetKind() && VarSeenInTerm(c[0][1], c1)) { return a; } - bool updated = UpdateSubstitutionMap(c[0], SimplifyTermAux(c[1])); + bool updated = UpdateSubstitutionMap(c[0], c1); output = updated ? ASTTrue : a; return output; } -- 2.47.3