From: vijay_ganesh Date: Wed, 14 Oct 2009 19:53:48 +0000 (+0000) Subject: All userdefined flags are now local to STPManager. not global anymore X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2a6be219044f950d3b3c9e4ebbd5ed07119e2a15;p=francis%2Fstp.git All userdefined flags are now local to STPManager. not global anymore git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@303 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index ffd597a..ef2b91f 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -6,7 +6,7 @@ #OPTIMIZE = -g -pg # Debugging and gprof-style profiling OPTIMIZE = -g # Debugging -OPTIMIZE = -O3 -DNDEBUG # Maximum optimization +OPTIMIZE = -O3 -DNDEBUG # Maximum optimization #OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE CFLAGS_BASE = $(OPTIMIZE) diff --git a/src/AST/ASTBVConst.cpp b/src/AST/ASTBVConst.cpp index 903928b..71aa8df 100644 --- a/src/AST/ASTBVConst.cpp +++ b/src/AST/ASTBVConst.cpp @@ -47,7 +47,7 @@ namespace BEEV unsigned char *res; const char *prefix; - if(print_binary_flag) { + if((GlobalSTP->bm)->UserFlags.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 a3be1d0..c0b4e88 100644 --- a/src/AST/ASTUtil.cpp +++ b/src/AST/ASTUtil.cpp @@ -8,6 +8,7 @@ // -*- c++ -*- #include "UsefulDefs.h" +#include "../STPManager/STPManager.h" #include "../main/Globals.h" namespace BEEV { @@ -30,11 +31,10 @@ namespace BEEV //this function accepts the name of a function (as a char *), and //records some stats about it. if the input is "print_func_stats", //the function will then print the stats that it has collected. - void CountersAndStats(const char * functionname) + void CountersAndStats(const char * functionname, STPMgr * bm) { static function_counters s; - - if (stats_flag) + if (bm->UserFlags.stats_flag) { if (!strcmp(functionname, "print_func_stats")) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 2c14837..a5af794 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -427,7 +427,7 @@ namespace BEEV result = TranslateSignedDivModRem(result); } - if (division_by_zero_returns_one) + if (bm->UserFlags.division_by_zero_returns_one_flag) { // This is a difficult rule to introduce in other // places because it's recursive. i.e. result is @@ -562,7 +562,7 @@ namespace BEEV Introduced_SymbolsSet.insert(CurrentSymbol); assert(BVTypeCheck(ite)); - if (arrayread_refinement_flag) + if (bm->UserFlags.arrayread_refinement_flag) { // ite is really a variable here; it is an ite in the // else-branch @@ -729,7 +729,7 @@ namespace BEEV //The big substitution function ASTNode ArrayTransformer::CreateSubstitutionMap(const ASTNode& a) { - if (!wordlevel_solve_flag) + if (!bm->UserFlags.wordlevel_solve_flag) return a; ASTNode output = a; diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index b3fd4d7..ce4e2c6 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -116,14 +116,14 @@ namespace BEEV // Constructor ArrayTransformer(STPMgr * bm, Simplifier* s) : - Arrayread_SymbolMap(INITIAL_TABLE_SIZE), - Introduced_SymbolsSet(INITIAL_TABLE_SIZE), + Arrayread_SymbolMap(), + Introduced_SymbolsSet(), bm(bm), simp(s), debug_transform(0) { - Arrayread_IteMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - Arrayname_ReadindicesMap = new ASTNodeToVecMap(INITIAL_TABLE_SIZE); + Arrayread_IteMap = new ASTNodeMap(); + Arrayname_ReadindicesMap = new ASTNodeToVecMap(); runTimes = bm->GetRunTimes(); ASTTrue = bm->CreateNode(TRUE); diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h index 8a942b6..8b42a9a 100644 --- a/src/AST/UsefulDefs.h +++ b/src/AST/UsefulDefs.h @@ -119,10 +119,6 @@ namespace BEEV { hash, eqstr> function_counters; #endif - - // Function that computes various kinds of statistics for the phases - // of STP - void CountersAndStats(const char * functionname); }; //end of namespace #endif diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 5d7023a..f4b5ea4 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -32,7 +32,7 @@ namespace BEEV { { inputToSAT = simplified_solved_InputToSAT; - if(optimize_flag) + if(bm->UserFlags.optimize_flag) { bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); @@ -49,7 +49,7 @@ namespace BEEV { bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); } - if(wordlevel_solve_flag) + if(bm->UserFlags.wordlevel_solve_flag) { simplified_solved_InputToSAT = bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); @@ -70,7 +70,7 @@ namespace BEEV { { inputToSAT = simplified_solved_InputToSAT; - if(optimize_flag) + if(bm->UserFlags.optimize_flag) { bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); simplified_solved_InputToSAT = @@ -83,7 +83,7 @@ namespace BEEV { bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); } - if(wordlevel_solve_flag) + if(bm->UserFlags.wordlevel_solve_flag) { simplified_solved_InputToSAT = bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); @@ -94,7 +94,8 @@ namespace BEEV { bm->ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT); - bm->start_abstracting = (arraywrite_refinement_flag) ? true : false; + bm->start_abstracting = + (bm->UserFlags.arraywrite_refinement_flag) ? true : false; bm->SimplifyWrites_InPlace_Flag = false; bm->Begin_RemoveWrites = (bm->start_abstracting) ? false : true; if (bm->start_abstracting) @@ -122,7 +123,7 @@ namespace BEEV { MINISAT::Solver newS; //MINISAT::SimpSolver newS; //MINISAT::UnsoundSimpSolver newS; - if (arrayread_refinement_flag) + if (bm->UserFlags.arrayread_refinement_flag) { bm->counterexample_checking_during_refinement = true; } @@ -133,7 +134,7 @@ namespace BEEV { orig_input); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats"); + CountersAndStats("print_func_stats", bm); return res; } @@ -150,7 +151,7 @@ namespace BEEV { orig_input); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats"); + CountersAndStats("print_func_stats", bm); return res; } @@ -158,7 +159,7 @@ namespace BEEV { Ctr_Example->SATBased_ArrayWriteRefinement(newS, orig_input); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats"); + CountersAndStats("print_func_stats", bm); return res; } @@ -168,7 +169,7 @@ namespace BEEV { orig_input); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats"); + CountersAndStats("print_func_stats", bm); return res; } diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index eef71a3..2e35d1a 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -574,13 +574,13 @@ namespace BEEV //prints statistics for the ASTNode void STPMgr::ASTNodeStats(const char * c, const ASTNode& a) { - if (!stats_flag) + if (!UserFlags.stats_flag) return; StatInfoSet.clear(); //print node size: cout << endl << "Printing: " << c; - if (print_nodes_flag) + if (UserFlags.print_nodes_flag) { //a.PL_Print(cout,0); //cout << endl; @@ -616,15 +616,10 @@ namespace BEEV return newn; } - STPMgr::~STPMgr() - { - } - - // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver void STPMgr::PrintStats(MINISAT::Solver& s) { - if (!stats_flag) + if (!UserFlags.stats_flag) return; double cpu_time = MINISAT::cpuTime(); uint64_t mem_used = MINISAT::memUsed(); diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 74cb639..8125219 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -10,6 +10,7 @@ #ifndef STPMGR_H #define STPMGR_H +#include "UserDefinedFlags.h" #include "../AST/AST.h" #include "../parser/let-funcs.h" @@ -49,6 +50,12 @@ namespace BEEV ASTBVConst::ASTBVConstHasher, ASTBVConst::ASTBVConstEqual> ASTBVConstSet; + typedef HASHMAP< + ASTNode, + ASTNodeSet, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToSetMap; + // Unique node tables that enables common subexpression sharing ASTInteriorSet _interior_unique_table; @@ -58,12 +65,6 @@ namespace BEEV // Table to uniquefy bvconst ASTBVConstSet _bvconst_unique_table; - typedef HASHMAP< - ASTNode, - ASTNodeSet, - ASTNode::ASTNodeHasher, - ASTNode::ASTNodeEqual> ASTNodeToSetMap; - // Global for assigning new node numbers. int _max_node_num; @@ -94,7 +95,7 @@ namespace BEEV // Ptr to class that reports on the running time of various parts // of the code RunTimes * runTimes; - + /**************************************************************** * Private Member Functions * ****************************************************************/ @@ -125,8 +126,8 @@ namespace BEEV /**************************************************************** * Public Flags * - * FIXME: Make the private. Get rid of this inelegance * - ****************************************************************/ + ****************************************************************/ + UserDefinedFlags UserFlags; // This flag, when true, indicates that counterexample is being // checked by the counterexample checker @@ -158,9 +159,10 @@ namespace BEEV // Constructor STPMgr() : - _symbol_unique_table(INITIAL_TABLE_SIZE), - _bvconst_unique_table(INITIAL_TABLE_SIZE), - _interior_unique_table(INITIAL_TABLE_SIZE), + _symbol_unique_table(), + _bvconst_unique_table(), + _interior_unique_table(), + UserFlags(), _symbol_count(0) { _max_node_num = 0; @@ -180,9 +182,6 @@ namespace BEEV _current_query = ASTUndefined; } - //destructor - ~STPMgr(); - //Return ptr to let-variables manager (see parser/let-funcs.h) LETMgr * GetLetMgr(void) { diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h new file mode 100644 index 0000000..8755b1e --- /dev/null +++ b/src/STPManager/UserDefinedFlags.h @@ -0,0 +1,160 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +#ifndef UDEFFLAGS_H +#define UDEFFLAGS_H + +namespace BEEV +{ + + /****************************************************************** + * Struct UserDefFlags: + * + * Some userdefined variables that are set through commandline + * options. + ******************************************************************/ + + struct UserDefinedFlags { + public: + //collect statistics on certain functions + bool stats_flag; + + //print DAG nodes + bool print_nodes_flag; + + //run STP in optimized mode + 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. + bool arrayread_refinement_flag; + + //switch to control write refinements + bool arraywrite_refinement_flag; + + //check the counterexample against the original input to STP + bool check_counterexample_flag; + + //construct the counterexample in terms of original variable based + //on the counterexample returned by SAT solver + bool construct_counterexample_flag; + bool print_counterexample_flag; + bool print_binary_flag; + + //Expands out the finite for-construct completely + bool expand_finitefor_flag; + + //Determines the number of abstraction-refinement loop count for the + //for-construct + bool num_absrefine_flag; + int num_absrefine; + + //if this option is true then print the way dawson wants using a + //different printer. do not use this printer. + bool print_arrayval_declaredorder_flag; + + //flag to decide whether to print "valid/invalid" or not + bool print_output_flag; + + //print the variable order chosen by the sat solver while it is + //solving. + bool print_sat_varorder_flag; + + //turn on word level bitvector solver + bool wordlevel_solve_flag; + + //XOR flattening optimizations. + bool xor_flatten_flag; + + //this flag indicates that the BVSolver() succeeded + bool toplevel_solved_flag; + + //print the input back + bool print_STPinput_back_flag; + + //Flag to switch on the smtlib parser + bool smtlib_parser_flag; + + bool division_by_zero_returns_one_flag; + + bool quick_statistics_flag; + + //CONSTRUCTOR + UserDefinedFlags() + { + //collect statistics on certain functions + stats_flag = false; + + //print DAG nodes + print_nodes_flag = false; + + //run STP in optimized mode + 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. + arrayread_refinement_flag = true; + + //flag to control write refinement + arraywrite_refinement_flag = true; + + //check the counterexample against the original input to STP + check_counterexample_flag = false; + + //construct the counterexample in terms of original variable based + //on the counterexample returned by SAT solver + construct_counterexample_flag = true; + print_counterexample_flag = false; + print_binary_flag = false; + + //Expands out the finite for-construct completely + expand_finitefor_flag = false; + + //Determines the number of abstraction-refinement loop count for the + //for-construct + num_absrefine_flag = false; + int num_absrefine = 0; + + //if this option is true then print the way dawson wants using a + //different printer. do not use this printer. + print_arrayval_declaredorder_flag = false; + + //flag to decide whether to print "valid/invalid" or not + print_output_flag = false; + + //print the variable order chosen by the sat solver while it is + //solving. + print_sat_varorder_flag = false; + + //turn on word level bitvector solver + wordlevel_solve_flag = true; + + //turn off XOR flattening + xor_flatten_flag = false; + + //Flag to switch on the smtlib parser + smtlib_parser_flag = false; + + //print the input back + print_STPinput_back_flag = false; + + // If enabled. division, mod and remainder by zero will evaluate to + // 1. + division_by_zero_returns_one_flag = false; + + quick_statistics_flag=false; + } //End of constructor for UserDefinedFlags + + }; //End of struct UserDefinedFlags +};//end of namespace + +#endif diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index 7e11b7f..0576d0e 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -40,11 +40,12 @@ namespace BEEV * time or all the false axioms each time). *****************************************************************/ SOLVER_RETURN_TYPE - AbsRefine_CounterExample::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, - const ASTNode& inputAlreadyInSAT, - const ASTNode& original_input) { + AbsRefine_CounterExample:: + SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, + const ASTNode& inputAlreadyInSAT, + const ASTNode& original_input) { //printf("doing array read refinement\n"); - if (!arrayread_refinement_flag) + if (!bm->UserFlags.arrayread_refinement_flag) FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); ASTVec FalseAxiomsVec, RemainingAxiomsVec; diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index c429f21..46a5309 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -31,7 +31,7 @@ namespace BEEV if (!newS.okay()) return; - if (!construct_counterexample_flag) + if (!bm->UserFlags.construct_counterexample_flag) return; CopySolverMap_To_CounterExample(); @@ -632,12 +632,12 @@ namespace BEEV void AbsRefine_CounterExample::CheckCounterExample(bool t) { - // FIXME: Code is more useful if enable flags are check OUTSIDE the method. - // If I want to check a counterexample somewhere, I don't want to have to set - // the flag in order to make it actualy happen! - + // FIXME: Code is more useful if enable flags are check OUTSIDE + // the method. If I want to check a counterexample somewhere, I + // don't want to have to set the flag in order to make it actualy + // happen! printf("checking counterexample\n"); - if (!check_counterexample_flag) + if (!bm->UserFlags.check_counterexample_flag) { return; } @@ -693,10 +693,10 @@ namespace BEEV // stdout void AbsRefine_CounterExample::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_flag) + //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 (!bm->UserFlags.print_counterexample_flag) { return; } @@ -709,7 +709,7 @@ namespace BEEV //if this option is true then print the way dawson wants using a //different printer. do not use this printer. - if (print_arrayval_declaredorder_flag) + if (bm->UserFlags.print_arrayval_declaredorder_flag) { return; } @@ -785,7 +785,7 @@ namespace BEEV //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_flag) + if (bm->UserFlags.print_counterexample_flag) return; //input is valid, no counterexample to print @@ -794,7 +794,7 @@ namespace BEEV //print if the commandline option is '-q'. allows printing the //counterexample in order. - if (!print_arrayval_declaredorder_flag) + if (!bm->UserFlags.print_arrayval_declaredorder_flag) return; //t is true if SAT solver generated a counterexample, else it is @@ -854,10 +854,11 @@ namespace BEEV { if (!newS.okay()) FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT", ASTUndefined); - // 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_flag && print_nodes_flag)) + // 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 (!(bm->UserFlags.stats_flag + && bm->UserFlags.print_nodes_flag)) return; int num_vars = newS.nVars(); @@ -925,7 +926,8 @@ namespace BEEV { CounterExampleMap.clear(); ConstructCounterExample(SatSolver); - if (stats_flag && print_nodes_flag) + if (bm->UserFlags.stats_flag + && bm->UserFlags.print_nodes_flag) { PrintSATModel(SatSolver); } @@ -951,13 +953,14 @@ namespace BEEV // counterexample is bogus: flag it else { - if (stats_flag && print_nodes_flag) + if (bm->UserFlags.stats_flag + && bm->UserFlags.print_nodes_flag) { cout << "Supposedly bogus one: \n"; - bool tmp = print_counterexample_flag; - print_counterexample_flag = true; + bool tmp = bm->UserFlags.print_counterexample_flag; + bm->UserFlags.print_counterexample_flag = true; PrintCounterExample(true); - print_counterexample_flag = tmp; + bm->UserFlags.print_counterexample_flag = tmp; } return SOLVER_UNDECIDED; diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 8165b9e..e6a3065 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -32,41 +32,58 @@ bool cinterface_exprdelete_on_flag = false; */ extern int cvcparse(void*); -void vc_setFlags(char c) { +void vc_setFlags(VC vc, char c) { + bmstar b = (bmstar)(((stpstar)vc)->bm); + std::string helpstring = "Usage: stp [-option] [infile]\n\n"; - helpstring += "STP version: " + BEEV::version + "\n\n"; - helpstring += "-a : switch optimizations off (optimizations are ON by default)\n"; - helpstring += "-c : construct counterexample\n"; - helpstring += "-d : check counterexample\n"; - helpstring += "-e : expand finite-for construct\n"; - helpstring += "-f : number of abstraction-refinement loops\n"; - helpstring += "-h : help\n"; - helpstring += "-m : use the SMTLIB parser\n"; - helpstring += "-p : print counterexample\n"; - helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; - helpstring += "-s : print function statistics\n"; - helpstring += "-v : print nodes \n"; - helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; - helpstring += "-x : flatten nested XORs\n"; - helpstring += "-y : print counterexample in binary\n"; + helpstring += + "STP version: " + BEEV::version + "\n\n"; + helpstring += + "-a : switch optimizations off (optimizations are ON by default)\n"; + helpstring += + "-c : construct counterexample\n"; + helpstring += + "-d : check counterexample\n"; + helpstring += + "-e : expand finite-for construct\n"; + helpstring += + "-f : number of abstraction-refinement loops\n"; + helpstring += + "-h : help\n"; + helpstring += + "-m : use the SMTLIB parser\n"; + helpstring += + "-p : print counterexample\n"; + helpstring += + "-r : switch refinement off (optimizations are ON by default)\n"; + helpstring += + "-s : print function statistics\n"; + helpstring += + "-v : print nodes \n"; + helpstring += + "-w : switch wordlevel solver off (optimizations are ON by default)\n"; + helpstring += + "-x : flatten nested XORs\n"; + helpstring += + "-y : print counterexample in binary\n"; switch(c) { case 'a' : - BEEV::optimize_flag = false; + b->UserFlags.optimize_flag = false; break; case 'c': - BEEV::construct_counterexample_flag = true; + b->UserFlags.construct_counterexample_flag = true; break; case 'd': - BEEV::construct_counterexample_flag = true; - BEEV::check_counterexample_flag = true; + b->UserFlags.construct_counterexample_flag = true; + b->UserFlags.check_counterexample_flag = true; break; case 'e': - BEEV::expand_finitefor_flag = true; + b->UserFlags.expand_finitefor_flag = true; break; case 'f': - BEEV::num_absrefine_flag = true; - //BEEV::num_absrefine = atoi(argv[++i]); + b->UserFlags.num_absrefine_flag = true; + //b->UserFlags.num_absrefine = atoi(argv[++i]); break; case 'h': fprintf(stderr,BEEV::usage,BEEV::prog); @@ -75,41 +92,41 @@ void vc_setFlags(char c) { //return -1; break; case 'n': - BEEV::print_output_flag = true; + b->UserFlags.print_output_flag = true; break; case 'm': - BEEV::smtlib_parser_flag=true; - BEEV::division_by_zero_returns_one = true; + b->UserFlags.smtlib_parser_flag=true; + b->UserFlags.division_by_zero_returns_one_flag = true; break; case 'p': - BEEV::print_counterexample_flag = true; + b->UserFlags.print_counterexample_flag = true; break; case 'q': - BEEV::print_arrayval_declaredorder_flag = true; + b->UserFlags.print_arrayval_declaredorder_flag = true; break; case 'r': - BEEV::arrayread_refinement_flag = false; + b->UserFlags.arrayread_refinement_flag = false; break; case 's' : - BEEV::stats_flag = true; + b->UserFlags.stats_flag = true; break; case 'u': - BEEV::arraywrite_refinement_flag = false; + b->UserFlags.arraywrite_refinement_flag = false; break; case 'v' : - BEEV::print_nodes_flag = true; + b->UserFlags.print_nodes_flag = true; break; case 'w': - BEEV::wordlevel_solve_flag = false; + b->UserFlags.wordlevel_solve_flag = false; break; case 'x': - BEEV::xor_flatten_flag = true; + b->UserFlags.xor_flatten_flag = true; break; case 'y': - BEEV::print_binary_flag = true; + b->UserFlags.print_binary_flag = true; break; case 'z': - BEEV::print_sat_varorder_flag = true; + b->UserFlags.print_sat_varorder_flag = true; break; default: std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n"; @@ -121,7 +138,6 @@ void vc_setFlags(char c) { //Create a validity Checker. This is the global STPMgr VC vc_createValidityChecker(void) { - vc_setFlags('d'); CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); if(0 != c) { cout << CONSTANTBV::BitVector_Error(c) << endl; @@ -146,6 +162,7 @@ VC vc_createValidityChecker(void) { BEEV::GlobalSTP = stp; decls = new BEEV::ASTVec(); //created_exprs.clear(); + vc_setFlags(stp,'d'); return (VC)stp; } @@ -178,7 +195,8 @@ void vc_printExprCCode(VC vc, Expr e) { // print variable declarations BEEV::ASTVec declsFromParser = (nodelist)b->ListOfDeclaredVars; - for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) { + for(BEEV::ASTVec::iterator it=declsFromParser.begin(), + itend=declsFromParser.end(); it!=itend;it++) { if(BEEV::BITVECTOR_TYPE == it->GetType()) { const char* name = it->GetName(); unsigned int bitWidth = it->GetValueWidth(); @@ -206,7 +224,8 @@ void vc_printExprFile(VC vc, Expr e, int fd) { } static void vc_printVarDeclsToStream(VC vc, ostream &os) { - for(BEEV::ASTVec::iterator i = decls->begin(),iend=decls->end();i!=iend;i++) { + for(BEEV::ASTVec::iterator i = decls->begin(), + iend=decls->end();i!=iend;i++) { node a = *i; switch(a.GetType()) { case BEEV::BITVECTOR_TYPE: @@ -239,8 +258,12 @@ static void vc_printAssertsToStream(VC vc, ostream &os, int simplify_print) { BEEV::Simplifier * simp = new BEEV::Simplifier(b); for(BEEV::ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) { b->Begin_RemoveWrites = true; - BEEV::ASTNode q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(*i,false) : *i; - q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(q,false) : q; + BEEV::ASTNode q = + (simplify_print == 1) ? + simp->SimplifyFormula_TopLevel(*i,false) : *i; + q = + (simplify_print == 1) ? + simp->SimplifyFormula_TopLevel(q,false) : q; b->Begin_RemoveWrites = false; os << "ASSERT( "; q.PL_Print(os); @@ -252,7 +275,9 @@ void vc_printAsserts(VC vc, int simplify_print) { vc_printAssertsToStream(vc, cout, simplify_print); } -void vc_printQueryStateToBuffer(VC vc, Expr e, char **buf, unsigned long *len, int simplify_print){ +void vc_printQueryStateToBuffer(VC vc, Expr e, + char **buf, + unsigned long *len, int simplify_print){ assert(vc); assert(e); assert(buf); @@ -298,7 +323,7 @@ void vc_printCounterExampleToBuffer(VC vc, char **buf, unsigned long *len) { // formate the state of the query std::ostringstream os; - BEEV::print_counterexample_flag = true; + b->UserFlags.print_counterexample_flag = true; os << "COUNTEREXAMPLE BEGIN: \n"; ce->PrintCounterExample(true,os); os << "COUNTEREXAMPLE END: \n"; @@ -498,7 +523,7 @@ void vc_printCounterExample(VC vc) { bmstar b = (bmstar)(((stpstar)vc)->bm); ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - BEEV::print_counterexample_flag = true; + b->UserFlags.print_counterexample_flag = true; cout << "COUNTEREXAMPLE BEGIN: \n"; ce->PrintCounterExample(true); cout << "COUNTEREXAMPLE END: \n"; @@ -1629,7 +1654,7 @@ Expr vc_parseExpr(VC vc, const char* infile) { cvcparse((void*)AssertsQuery); BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0]; BEEV::ASTNode query = (*(BEEV::ASTVec*)AssertsQuery)[1]; - //b->TopLevelSTP(asserts, query); + //BEEV::GlobalSTP->TopLevelSTP(asserts, query); node oo = b->CreateNode(BEEV::NOT,query); node o = b->CreateNode(BEEV::AND,asserts,oo); @@ -1782,7 +1807,7 @@ void vc_printCounterExampleFile(VC vc, int fd) { bmstar b = (bmstar)(((stpstar)vc)->bm); ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - BEEV::print_counterexample_flag = true; + b->UserFlags.print_counterexample_flag = true; os << "COUNTEREXAMPLE BEGIN: \n"; ce->PrintCounterExample(true, os); os << "COUNTEREXAMPLE END: \n"; diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index cdc9383..253e1c4 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -15,6 +15,7 @@ * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. ********************************************************************/ // -*- c++ -*- + #ifndef _cvcl__include__c_interface_h_ #define _cvcl__include__c_interface_h_ @@ -41,7 +42,7 @@ extern "C" { // h : help // s : stats // v : print nodes - void vc_setFlags(char c); + void vc_setFlags(VC vc, char c); //! Flags can be NULL VC vc_createValidityChecker(void); diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp index 8f7b998..101f7d3 100644 --- a/src/main/Globals.cpp +++ b/src/main/Globals.cpp @@ -13,75 +13,6 @@ namespace BEEV { - //some global variables that are set through commandline options. it - //is best that these variables remain global. Default values set - //here - // - //collect statistics on certain functions - bool stats_flag = false; - - //print DAG nodes - bool print_nodes_flag = false; - - //run STP in optimized mode - 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_flag = true; - - //flag to control write refinement - bool arraywrite_refinement_flag = true; - - //check the counterexample against the original input to STP - bool check_counterexample_flag = false; - - //construct the counterexample in terms of original variable based - //on the counterexample returned by SAT solver - bool construct_counterexample_flag = true; - bool print_counterexample_flag = false; - bool print_binary_flag = false; - - //Expands out the finite for-construct completely - bool expand_finitefor_flag = false; - - //Determines the number of abstraction-refinement loop count for the - //for-construct - bool num_absrefine_flag = false; - int num_absrefine = 0; - - - //if this option is true then print the way dawson wants using a - //different printer. do not use this printer. - bool print_arrayval_declaredorder_flag = false; - - //flag to decide whether to print "valid/invalid" or not - bool print_output_flag = false; - - //print the variable order chosen by the sat solver while it is - //solving. - bool print_sat_varorder_flag = false; - - //turn on word level bitvector solver - bool wordlevel_solve_flag = true; - - //turn off XOR flattening - 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_flag = false; - - // If enabled. division, mod and remainder by zero will evaluate to - // 1. - bool division_by_zero_returns_one = false; - - bool quick_statistics_flag=false; - enum inputStatus input_status = NOT_DECLARED; //global BEEVMGR for the parser. Use exclusively for parsing @@ -89,11 +20,14 @@ namespace BEEV STPMgr * ParserBM; void (*vc_error_hdlr)(const char* err_msg) = NULL; - /** This is reusable empty vector, for representing empty children - arrays */ + + // This is reusable empty vector, for representing empty children + // arrays ASTVec _empty_ASTVec; - //Some global vars for the Main function. + //Some constant global vars for the Main function. Once they are + //set, these globals will remain constants. These vars are not used + //in the STP library. const char * prog = "stp"; int linenum = 1; const char * usage = "Usage: %s [-option] [infile]\n"; diff --git a/src/main/Globals.h b/src/main/Globals.h index 33892fc..ef22d8d 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -37,74 +37,10 @@ namespace BEEV class BVSolver; class STP; - //some global variables that are set through commandline options. it - //is best that these variables remain global. Default values set - //here - // - //collect statistics on certain functions - extern bool stats_flag; - - //print DAG nodes - extern bool print_nodes_flag; - - //run STP in optimized mode - 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_flag; - - //switch to control write refinements - extern bool arraywrite_refinement_flag; - - //check the counterexample against the original input to STP - 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_flag; - extern bool print_counterexample_flag; - extern bool print_binary_flag; - - //Expands out the finite for-construct completely - extern bool expand_finitefor_flag; - - //Determines the number of abstraction-refinement loop count for the - //for-construct - extern bool num_absrefine_flag; - extern int num_absrefine; - - //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_flag; - - //flag to decide whether to print "valid/invalid" or not - extern bool print_output_flag; - - //print the variable order chosen by the sat solver while it is - //solving. - extern bool print_sat_varorder_flag; - - //turn on word level bitvector solver - extern bool wordlevel_solve_flag; - - //XOR flattening optimizations. - extern bool xor_flatten_flag; - - //this flag indicates that the BVSolver() succeeded - extern bool toplevel_solved_flag; - - //print the input back - extern bool print_STPinput_back_flag; - - //Flag to switch on the smtlib parser - extern bool smtlib_parser_flag; - - extern bool division_by_zero_returns_one; - - extern bool quick_statistics_flag; + /*************************************************************** + * ENUM TYPES + * + ***************************************************************/ enum inputStatus { @@ -113,7 +49,6 @@ namespace BEEV TO_BE_UNSATISFIABLE, TO_BE_UNKNOWN // Specified in the input file as unknown. }; - extern enum inputStatus input_status; //return types for the GetType() function in ASTNode class enum types @@ -132,20 +67,28 @@ namespace BEEV SOLVER_ERROR=-100 }; - //Useful global variables. Use for parsing only - extern STP * GlobalSTP; - extern STPMgr * ParserBM; - //Empty vector. Useful commonly used ASTNodes extern std::vector _empty_ASTVec; extern ASTNode ASTFalse, ASTTrue, ASTUndefined; - //Some global vars for the Main function. + //Useful global variables. Use for parsing only + extern STP * GlobalSTP; + extern STPMgr * ParserBM; + + //Some constant global vars for the Main function. Once they are + //set, these globals will remain constants. These vars are not used + //in the STP library. extern const char * prog; extern int linenum; extern const char * usage; extern std::string helpstring; extern const std::string version; + extern enum inputStatus input_status; + + + // Function that computes various kinds of statistics for the phases + // of STP + void CountersAndStats(const char * functionname, STPMgr * bm); }; //end of namespace BEEV #endif diff --git a/src/main/main.cpp b/src/main/main.cpp index 35b8d9c..32a0212 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -95,24 +95,24 @@ int main(int argc, char ** argv) { switch(argv[i][1]) { case 'a' : - optimize_flag = false; + bm->UserFlags.optimize_flag = false; break; case 'b': - print_STPinput_back_flag = true; + bm->UserFlags.print_STPinput_back_flag = true; break; case 'c': - construct_counterexample_flag = true; + bm->UserFlags.construct_counterexample_flag = true; break; case 'd': - construct_counterexample_flag = true; - check_counterexample_flag = true; + bm->UserFlags.construct_counterexample_flag = true; + bm->UserFlags.check_counterexample_flag = true; break; case 'e': - expand_finitefor_flag = true; + bm->UserFlags.expand_finitefor_flag = true; break; case 'f': - num_absrefine_flag = true; - num_absrefine = atoi(argv[++i]); + bm->UserFlags.num_absrefine_flag = true; + bm->UserFlags.num_absrefine = atoi(argv[++i]); break; case 'h': fprintf(stderr,usage,prog); @@ -120,44 +120,44 @@ int main(int argc, char ** argv) { return -1; break; case 'n': - print_output_flag = true; + bm->UserFlags.print_output_flag = true; break; case 'm': - smtlib_parser_flag=true; - division_by_zero_returns_one = true; + bm->UserFlags.smtlib_parser_flag=true; + bm->UserFlags.division_by_zero_returns_one_flag = true; break; case 'p': - print_counterexample_flag = true; + bm->UserFlags.print_counterexample_flag = true; break; case 'q': - print_arrayval_declaredorder_flag = true; + bm->UserFlags.print_arrayval_declaredorder_flag = true; break; case 'r': - arrayread_refinement_flag = false; + bm->UserFlags.arrayread_refinement_flag = false; break; case 's' : - stats_flag = true; + bm->UserFlags.stats_flag = true; break; case 't': - quick_statistics_flag = true; + bm->UserFlags.quick_statistics_flag = true; break; case 'u': - arraywrite_refinement_flag = false; + bm->UserFlags.arraywrite_refinement_flag = false; break; case 'v' : - print_nodes_flag = true; + bm->UserFlags.print_nodes_flag = true; break; case 'w': - wordlevel_solve_flag = false; + bm->UserFlags.wordlevel_solve_flag = false; break; case 'x': - xor_flatten_flag = true; + bm->UserFlags.xor_flatten_flag = true; break; case 'y': - print_binary_flag = true; + bm->UserFlags.print_binary_flag = true; break; case 'z': - print_sat_varorder_flag = true; + bm->UserFlags.print_sat_varorder_flag = true; break; default: fprintf(stderr,usage,prog); @@ -168,7 +168,7 @@ int main(int argc, char ** argv) { } } else { infile = argv[i]; - if (smtlib_parser_flag) + if (bm->UserFlags.smtlib_parser_flag) { smtin = fopen(infile,"r"); if(smtin == NULL) @@ -190,7 +190,7 @@ int main(int argc, char ** argv) { } //want to print the output always from the commandline. - print_output_flag = true; + bm->UserFlags.print_output_flag = true; ASTVec * AssertsQuery = new ASTVec; CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); if(0 != c) { @@ -199,7 +199,7 @@ int main(int argc, char ** argv) { } bm->GetRunTimes()->start(RunTimes::Parsing); - if (smtlib_parser_flag) + if (bm->UserFlags.smtlib_parser_flag) { smtparse((void*)AssertsQuery); } @@ -211,9 +211,9 @@ int main(int argc, char ** argv) { ASTNode asserts = (*(ASTVec*)AssertsQuery)[0]; ASTNode query = (*(ASTVec*)AssertsQuery)[1]; - if(print_STPinput_back_flag) + if(bm->UserFlags.print_STPinput_back_flag) { - if(smtlib_parser_flag) + if(bm->UserFlags.smtlib_parser_flag) { // don't pass the query. It's not returned by the smtlib // parser. @@ -227,7 +227,7 @@ int main(int argc, char ** argv) { } //end of PrintBack if SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query); - if (quick_statistics_flag) + if (bm->UserFlags.quick_statistics_flag) { bm->GetRunTimes()->print(); } diff --git a/src/parser/CVC.y b/src/parser/CVC.y index 8ca1e74..c658cc2 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -175,7 +175,7 @@ cmd : other_cmd counterexample : COUNTEREXAMPLE_TOK ';' { - print_counterexample_flag = true; + ParserBM->UserFlags.print_counterexample_flag = true; (GlobalSTP->Ctr_Example)->PrintCounterExample(true); } ; diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y index a8c0482..a63fdff 100644 --- a/src/parser/smtlib.y +++ b/src/parser/smtlib.y @@ -416,7 +416,7 @@ var_decl: //var $2->SetIndexWidth($3.indexwidth); $2->SetValueWidth($3.valuewidth); - if(print_STPinput_back_flag) + if(ParserBM->UserFlags.print_STPinput_back_flag) ParserBM->ListOfDeclaredVars.push_back(*$2); } | LPAREN_TOK FORMID_TOK RPAREN_TOK @@ -426,7 +426,7 @@ var_decl: //var $2->SetIndexWidth(0); $2->SetValueWidth(0); - if(print_STPinput_back_flag) + if(ParserBM->UserFlags.print_STPinput_back_flag) ParserBM->ListOfDeclaredVars.push_back(*$2); } ; diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp index 6574b2c..bd09bce 100644 --- a/src/simplifier/consteval.cpp +++ b/src/simplifier/consteval.cpp @@ -246,23 +246,29 @@ namespace BEEV break; } - // SBVREM : Result of rounding the quotient towards zero. i.e. (-10)/3, has a remainder of -1 - // SBVMOD : Result of rounding the quotient towards -infinity. i.e. (-10)/3, has a modulus of 2. - // EXCEPT THAT if it divides exactly and the signs are different, then it's equal to the dividend. + // SBVREM : Result of rounding the quotient towards + // zero. i.e. (-10)/3, has a remainder of -1 + // + // SBVMOD : Result of rounding the quotient towards + // -infinity. i.e. (-10)/3, has a modulus of 2. EXCEPT THAT + // if it divides exactly and the signs are different, then + // it's equal to the dividend. case SBVDIV: case SBVREM: { CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true); CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true); - if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1)) + if (_bm->UserFlags.division_by_zero_returns_one_flag + && CONSTANTBV::BitVector_is_empty(tmp1)) { // Expecting a division by zero. Just return one. OutputNode = _bm->CreateOneConst(outputwidth); } else { - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder); + CONSTANTBV::ErrCode e = + CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder); if (e != 0) { @@ -310,7 +316,8 @@ namespace BEEV tmp0 = CONSTANTBV::BitVector_Clone(tmp0); tmp1 = CONSTANTBV::BitVector_Clone(tmp1); - if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1)) + if (_bm->UserFlags.division_by_zero_returns_one_flag + && CONSTANTBV::BitVector_is_empty(tmp1)) { // Expecting a division by zero. Just return one. OutputNode = _bm->CreateOneConst(outputwidth); @@ -408,7 +415,8 @@ namespace BEEV CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true); CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true); - if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1)) + if (_bm->UserFlags.division_by_zero_returns_one_flag + && CONSTANTBV::BitVector_is_empty(tmp1)) { // Expecting a division by zero. Just return one. OutputNode = _bm->CreateOneConst(outputwidth); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 6d2c29a..249eb47 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -62,7 +62,7 @@ namespace BEEV if (it != itend) { output = it->second; - CountersAndStats("Successful_CheckSimplifyMap"); + CountersAndStats("Successful_CheckSimplifyMap", _bm); return true; } @@ -73,7 +73,7 @@ namespace BEEV ASTTrue : (ASTTrue == it->second) ? ASTFalse : _bm->CreateNode(NOT, it->second); - CountersAndStats("2nd_Successful_CheckSimplifyMap"); + CountersAndStats("2nd_Successful_CheckSimplifyMap", _bm); return true; } @@ -191,7 +191,7 @@ namespace BEEV if (it != itend) { //cerr << "found:" << *it << endl; - CountersAndStats("Successful_CheckAlwaysTrueFormMap"); + CountersAndStats("Successful_CheckAlwaysTrueFormMap", _bm); return true; } @@ -245,7 +245,7 @@ namespace BEEV bool pushNeg, ASTNodeMap* VarConstMap) { _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); - if (smtlib_parser_flag) + if (_bm->UserFlags.smtlib_parser_flag) BuildReferenceCountMap(b); ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); ResetSimplifyMaps(); @@ -638,7 +638,7 @@ namespace BEEV //takes care of some simple ITE Optimizations in the context of equations ASTNode Simplifier::ITEOpt_InEqs(const ASTNode& in, ASTNodeMap* VarConstMap) { - CountersAndStats("ITEOpts_InEqs"); + CountersAndStats("ITEOpts_InEqs", _bm); if (!(EQ == in.GetKind())) { @@ -732,7 +732,7 @@ namespace BEEV //return the constructed equality ASTNode Simplifier::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2) { - CountersAndStats("CreateSimplifiedEQ"); + CountersAndStats("CreateSimplifiedEQ", _bm); Kind k1 = in1.GetKind(); Kind k2 = in2.GetKind(); @@ -762,8 +762,8 @@ namespace BEEV ASTNode t0 = in0; ASTNode t1 = in1; ASTNode t2 = in2; - CountersAndStats("CreateSimplifiedITE"); - if (!optimize_flag) + CountersAndStats("CreateSimplifiedITE", _bm); + if (!_bm->UserFlags.optimize_flag) { if (t1.GetValueWidth() != t2.GetValueWidth()) { @@ -798,14 +798,17 @@ namespace BEEV return _bm->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2); } - ASTNode Simplifier::CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2) + ASTNode + Simplifier:: + CreateSimplifiedFormulaITE(const ASTNode& in0, + const ASTNode& in1, const ASTNode& in2) { ASTNode t0 = in0; ASTNode t1 = in1; ASTNode t2 = in2; - CountersAndStats("CreateSimplifiedFormulaITE"); + CountersAndStats("CreateSimplifiedFormulaITE", _bm); - if (optimize_flag) + if (_bm->UserFlags.optimize_flag) { if (t0 == ASTTrue) return t1; diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index be35163..0dd90fa 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -68,8 +68,8 @@ namespace BEEV SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE); SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE); SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - ReadOverWrite_NewName_Map = new ASTNodeMap(INITIAL_TABLE_SIZE); - ReferenceCount = new ASTNodeCountMap(INITIAL_TABLE_SIZE); + ReadOverWrite_NewName_Map = new ASTNodeMap(); + ReferenceCount = new ASTNodeCountMap(); ASTTrue = bm->CreateNode(TRUE); ASTFalse = bm->CreateNode(FALSE); diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index 7769b54..60bb670 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -25,7 +25,7 @@ namespace BEEV CNFMgr* cm = new CNFMgr(bm); ClauseList* cl = cm->convertToCNF(BBFormula); - if (stats_flag) + if (bm->UserFlags.stats_flag) { cerr << "Number of clauses:" << cl->size() << endl; } @@ -48,19 +48,21 @@ namespace BEEV { bool true_iff_valid = (SOLVER_VALID == ret); - if (print_output_flag) + if (bm->UserFlags.print_output_flag) { - if (smtlib_parser_flag) + if (bm->UserFlags.smtlib_parser_flag) { if (true_iff_valid && (input_status == TO_BE_SATISFIABLE)) { - cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl; + cerr << "Warning. Expected satisfiable,"\ + " FOUND unsatisfiable" << endl; } else if (!true_iff_valid && (input_status == TO_BE_UNSATISFIABLE)) { - cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; + cerr << "Warning. Expected unsatisfiable,"\ + " FOUND satisfiable" << endl; } } } @@ -68,9 +70,9 @@ namespace BEEV if (true_iff_valid) { bm->ValidFlag = true; - if (print_output_flag) + if (bm->UserFlags.print_output_flag) { - if (smtlib_parser_flag) + if (bm->UserFlags.smtlib_parser_flag) cout << "unsat\n"; else cout << "Valid.\n"; @@ -79,9 +81,9 @@ namespace BEEV else { bm->ValidFlag = false; - if (print_output_flag) + if (bm->UserFlags.print_output_flag) { - if (smtlib_parser_flag) + if (bm->UserFlags.smtlib_parser_flag) cout << "sat\n"; else cout << "Invalid.\n"; diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp index b33ab86..dbcfb72 100644 --- a/src/to-sat/SimpBool.cpp +++ b/src/to-sat/SimpBool.cpp @@ -7,12 +7,11 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ -// Simplifying create methods for Boolean operations. -// These are only very simple local simplifications. +// Simplifying create methods for Boolean operations. These are only +// very simple local simplifications. -// This is somewhat redundant with Vijay's simplifier code. They -// need to be merged. -// FIXME: control with optimize flag. +// This is somewhat redundant with Vijay's simplifier code. They need +// to be merged. FIXME: control with optimize flag. static bool _trace_simpbool = 0; static bool _disable_simpbool = 0; @@ -21,8 +20,7 @@ static bool _disable_simpbool = 0; #include "../STPManager/STPManager.h" // SMTLIB experimental hack. Try allocating a single stack here for -// children to reduce growing of vectors. -//BEEV::ASTVec child_stack; +// children to reduce growing of vectors. BEEV::ASTVec child_stack; namespace BEEV { @@ -90,7 +88,8 @@ namespace BEEV //return CreateSimpForm(kind, child_stack); } - ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1) + ASTNode STPMgr::CreateSimpForm(Kind kind, + const ASTNode& child0, const ASTNode& child1) { ASTVec children; //child_stack.clear(); // could just reset top pointer. @@ -102,7 +101,9 @@ namespace BEEV //return CreateSimpForm(kind, child_stack); } - ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2) + ASTNode STPMgr::CreateSimpForm(Kind kind, + const ASTNode& child0, + const ASTNode& child1, const ASTNode& child2) { ASTVec children; //child_stack.clear(); // could just reset top pointer. @@ -183,7 +184,8 @@ namespace BEEV { fflag = 1; // For selective debug printing (below). // append grandchildren to children - flat_children.insert(flat_children.end(), gchildren.begin(), gchildren.end()); + flat_children.insert(flat_children.end(), + gchildren.begin(), gchildren.end()); } else { @@ -206,7 +208,8 @@ namespace BEEV return flat_children; } - ASTNode STPMgr::CreateSimpAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2) + ASTNode STPMgr::CreateSimpAndOr(bool IsAnd, + const ASTNode& form1, const ASTNode& form2) { ASTVec children; children.push_back(form1); @@ -230,7 +233,7 @@ namespace BEEV ASTVec new_children; ASTVec flat_children; - if (xor_flatten_flag) + if (UserFlags.xor_flatten_flag) { flat_children = FlattenKind(k, children); } @@ -250,7 +253,8 @@ namespace BEEV ASTVec::const_iterator it_end = flat_children.end(); ASTVec::const_iterator next_it; - for (ASTVec::const_iterator it = flat_children.begin(); it != it_end; it = next_it) + for (ASTVec::const_iterator it = flat_children.begin(); + it != it_end; it = next_it) { next_it = it + 1; bool nextexists = (next_it < it_end); @@ -273,7 +277,8 @@ namespace BEEV // drop it // cout << "Dropping [" << it->GetNodeNum() << "]" << endl; } - else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) + else if (nextexists && (next_it->GetKind() == NOT) + && ((*next_it)[0] == *it)) { // form and negation -- return FALSE for AND, TRUE for OR. retval = annihilator; @@ -331,7 +336,7 @@ namespace BEEV ASTVec flat_children; // empty vector ASTVec::const_iterator it_end = children.end(); - if (xor_flatten_flag) + if (UserFlags.xor_flatten_flag) { flat_children = FlattenKind(XOR, children); } @@ -373,7 +378,8 @@ namespace BEEV // so that it gets tossed, too. *next_it = ASTFalse; } - else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) + else if (nextexists && (next_it->GetKind() == NOT) + && ((*next_it)[0] == *it)) { // x XOR NOT x = TRUE. Skip current, write "true" into next_it // so that it gets tossed, too. @@ -440,14 +446,18 @@ namespace BEEV } // FIXME: How do I know whether ITE is a formula or not? - ASTNode STPMgr::CreateSimpFormITE(const ASTNode& child0, const ASTNode& child1, const ASTNode& child2) + ASTNode STPMgr::CreateSimpFormITE(const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2) { ASTNode retval; if (_trace_simpbool) { - cout << "========" << endl << "CreateSimpFormITE " << child0 << child1 << child2 << endl; + cout << "========" << endl + << "CreateSimpFormITE " + << child0 << child1 << child2 << endl; } if (ASTTrue == child0) diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 993b09b..47eb0b5 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -38,18 +38,14 @@ namespace BEEV } /* FUNCTION: convert ASTClauses to MINISAT clauses and solve. - * Accepts ASTClauses and converts them to MINISAT clauses. Then adds - * the newly minted MINISAT clauses to the local SAT instance, and - * calls solve(). If solve returns unsat, then stop and return + * Accepts ASTClauses and converts them to MINISAT clauses. Then + * adds the newly minted MINISAT clauses to the local SAT instance, + * and calls solve(). If solve returns unsat, then stop and return * unsat. else continue. */ - // FIXME: Still need to deal with TRUE/FALSE in clauses! - // - //bool ToSAT::toSATandSolve(MINISAT::Solver& newS, - //ClauseList& cll, ASTNodeToIntMap& heuristic) bool ToSAT::toSATandSolve(MINISAT::Solver& newS, ClauseList& cll) { - CountersAndStats("SAT Solver"); + CountersAndStats("SAT Solver", bm); bm->GetRunTimes()->start(RunTimes::SendingToSAT); diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 01e651e..d1da623 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -40,7 +40,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 ./a10.out 11: g++ $(CXXFLAGS) squares-leak.c -lstp -o a11.out - ./a11.out +# ./a11.out 12: g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out ./a12.out diff --git a/tests/c-api-tests/array-cvcl-02.c b/tests/c-api-tests/array-cvcl-02.c index 18d4d24..ce98565 100644 --- a/tests/c-api-tests/array-cvcl-02.c +++ b/tests/c-api-tests/array-cvcl-02.c @@ -7,9 +7,9 @@ g++ -DEXT_HASH_MAP array-cvcl-02.c -I/home/vganesh/stp/c_interface -L/home/vgane #include "c_interface.h" int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); Expr cvcl_array = vc_varExpr1(vc, "a",32,32); Expr i = vc_varExpr1(vc, "i", 0, 8); diff --git a/tests/c-api-tests/b4-c.c b/tests/c-api-tests/b4-c.c index 10e442d..dfaa735 100644 --- a/tests/c-api-tests/b4-c.c +++ b/tests/c-api-tests/b4-c.c @@ -2,13 +2,14 @@ int main() { - vc_setFlags('v'); - vc_setFlags('s'); - vc_setFlags('n'); - //vc_setFlags('a'); - //vc_setFlags('w'); - //vc_setFlags('r'); VC vc = vc_createValidityChecker(); + vc_setFlags(vc,'v'); + vc_setFlags(vc,'s'); + vc_setFlags(vc,'n'); + //vc_setFlags(vc,'a'); + //vc_setFlags(vc,'w'); + //vc_setFlags(vc,'r'); + //vc_push(vc); Expr e12866 = vc_varExpr(vc, "at", vc_bvType(vc, 5)); Expr e12867 = e12866; diff --git a/tests/c-api-tests/b4-c2.c b/tests/c-api-tests/b4-c2.c index f175953..8121d07 100644 --- a/tests/c-api-tests/b4-c2.c +++ b/tests/c-api-tests/b4-c2.c @@ -1,12 +1,13 @@ #include "c_interface.h" #include int main() { - vc_setFlags('w'); - //vc_setFlags('v'); - //vc_setFlags('s'); - //vc_setFlags('a'); - vc_setFlags('n'); VC vc = vc_createValidityChecker(); + vc_setFlags(vc,'w'); + //vc_setFlags(vc,'v'); + //vc_setFlags(vc,'s'); + //vc_setFlags(vc,'a'); + vc_setFlags(vc,'n'); + vc_push(vc); Expr e5283955 = vc_varExpr(vc, "at", vc_bvType(vc, 5)); Expr e5283956 = e5283955; diff --git a/tests/c-api-tests/biosat-rna.cpp b/tests/c-api-tests/biosat-rna.cpp index dd995ca..81a0d52 100644 --- a/tests/c-api-tests/biosat-rna.cpp +++ b/tests/c-api-tests/biosat-rna.cpp @@ -177,13 +177,13 @@ int main(int argc, char** argv) { E_table[35] = 3; - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); - vc_setFlags('r'); - vc_setFlags('a'); - vc_setFlags('w'); - vc_setFlags('y'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); + vc_setFlags(vc,'r'); + vc_setFlags(vc,'a'); + vc_setFlags(vc,'w'); + vc_setFlags(vc,'y'); //Parameteric Boolean X Expr X = vc_varExpr1(vc, "X", 0, 0); diff --git a/tests/c-api-tests/cvc-to-c.cpp b/tests/c-api-tests/cvc-to-c.cpp index 1b0db4f..0da15b0 100644 --- a/tests/c-api-tests/cvc-to-c.cpp +++ b/tests/c-api-tests/cvc-to-c.cpp @@ -14,9 +14,9 @@ using namespace std; int main(int argc, char** argv) { VC vc = vc_createValidityChecker(); - //vc_setFlags('n'); - //vc_setFlags('d'); - //vc_setFlags('p'); + //vc_setFlags(vc,'n'); + //vc_setFlags(vc,'d'); + //vc_setFlags(vc,'p'); Expr c = vc_parseExpr(vc, argv[1]); diff --git a/tests/c-api-tests/getbvunsignedlonglong-check.c b/tests/c-api-tests/getbvunsignedlonglong-check.c index 5041f28..ba9d6e9 100644 --- a/tests/c-api-tests/getbvunsignedlonglong-check.c +++ b/tests/c-api-tests/getbvunsignedlonglong-check.c @@ -9,10 +9,10 @@ int main() { for(int j=0;j < 3; j++) { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); - vc_setFlags('x'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); + vc_setFlags(vc,'x'); Type bv8 = vc_bvType(vc, 8); Expr a = vc_bvCreateMemoryArray(vc, "a"); diff --git a/tests/c-api-tests/multiple-queries.c b/tests/c-api-tests/multiple-queries.c index 877d104..6d72068 100644 --- a/tests/c-api-tests/multiple-queries.c +++ b/tests/c-api-tests/multiple-queries.c @@ -5,10 +5,10 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('c'); - vc_setFlags('d'); - vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'c'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); Type bv8 = vc_bvType(vc, 8); diff --git a/tests/c-api-tests/parsefile-using-cinterface.c b/tests/c-api-tests/parsefile-using-cinterface.c index 7f642c6..b729d65 100644 --- a/tests/c-api-tests/parsefile-using-cinterface.c +++ b/tests/c-api-tests/parsefile-using-cinterface.c @@ -5,9 +5,9 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); Expr c = vc_parseExpr(vc,"./t.cvc"); diff --git a/tests/c-api-tests/print.c b/tests/c-api-tests/print.c index 642eb46..76e3715 100644 --- a/tests/c-api-tests/print.c +++ b/tests/c-api-tests/print.c @@ -5,9 +5,9 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); Expr ct_3 = vc_bvConstExprFromStr(vc, "00000000000000000000000000000011"); diff --git a/tests/c-api-tests/push-pop-1.c b/tests/c-api-tests/push-pop-1.c index b5f129e..2131e39 100644 --- a/tests/c-api-tests/push-pop-1.c +++ b/tests/c-api-tests/push-pop-1.c @@ -5,12 +5,12 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); - vc_setFlags('v'); - vc_setFlags('s'); - vc_setFlags('c'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); + vc_setFlags(vc,'v'); + vc_setFlags(vc,'s'); + vc_setFlags(vc,'c'); vc_push(vc); Type bv8 = vc_bvType(vc, 8); diff --git a/tests/c-api-tests/push-pop.c b/tests/c-api-tests/push-pop.c index 20c4052..097c801 100644 --- a/tests/c-api-tests/push-pop.c +++ b/tests/c-api-tests/push-pop.c @@ -5,11 +5,11 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); - //vc_setFlags('v'); - //vc_setFlags('s'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); + //vc_setFlags(vc,'v'); + //vc_setFlags(vc,'s'); Type bv8 = vc_bvType(vc, 8); diff --git a/tests/c-api-tests/simplify.c b/tests/c-api-tests/simplify.c index 5b14466..423ce12 100644 --- a/tests/c-api-tests/simplify.c +++ b/tests/c-api-tests/simplify.c @@ -8,9 +8,9 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); Type bv8 = vc_bvType(vc, 8); Expr a = vc_bvCreateMemoryArray(vc, "a"); diff --git a/tests/c-api-tests/simplify1.c b/tests/c-api-tests/simplify1.c index c281bc0..e928699 100644 --- a/tests/c-api-tests/simplify1.c +++ b/tests/c-api-tests/simplify1.c @@ -9,10 +9,10 @@ int main() { for(int j=0;j < 3; j++) { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); - vc_setFlags('x'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); + vc_setFlags(vc,'x'); Type bv8 = vc_bvType(vc, 8); Expr a = vc_bvCreateMemoryArray(vc, "a"); diff --git a/tests/c-api-tests/stp-counterex.c b/tests/c-api-tests/stp-counterex.c index 31de727..e6ab393 100644 --- a/tests/c-api-tests/stp-counterex.c +++ b/tests/c-api-tests/stp-counterex.c @@ -6,9 +6,9 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - //vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + //vc_setFlags(vc,'p'); Type bv8 = vc_bvType(vc, 8); diff --git a/tests/c-api-tests/stp-div-001.c b/tests/c-api-tests/stp-div-001.c index 4b4718a..c64d037 100644 --- a/tests/c-api-tests/stp-div-001.c +++ b/tests/c-api-tests/stp-div-001.c @@ -7,9 +7,9 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - //vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + //vc_setFlags(vc,'p'); Type bv8 = vc_bvType(vc, 8); diff --git a/tests/c-api-tests/stpcheck.c b/tests/c-api-tests/stpcheck.c index 6e23e4c..c415363 100644 --- a/tests/c-api-tests/stpcheck.c +++ b/tests/c-api-tests/stpcheck.c @@ -7,8 +7,8 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); // 8-bit variable 'x' Expr x=vc_varExpr(vc,"x",vc_bvType(vc,8)); diff --git a/tests/c-api-tests/x.c b/tests/c-api-tests/x.c index 0060005..b04556b 100644 --- a/tests/c-api-tests/x.c +++ b/tests/c-api-tests/x.c @@ -2,9 +2,9 @@ int main(int argc, char *argv[]) { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); Expr nresp1 = vc_varExpr(vc, "nresp1", vc_bv32Type(vc)); Expr packet_get_int0 = vc_varExpr(vc, "packet_get_int0", vc_bv32Type(vc)); diff --git a/tests/c-api-tests/y.c b/tests/c-api-tests/y.c index db16626..5a43baa 100644 --- a/tests/c-api-tests/y.c +++ b/tests/c-api-tests/y.c @@ -3,9 +3,9 @@ int main(int argc, char *argv[]) { VC vc = vc_createValidityChecker(); - vc_setFlags('n'); - vc_setFlags('d'); - vc_setFlags('p'); + vc_setFlags(vc,'n'); + vc_setFlags(vc,'d'); + vc_setFlags(vc,'p'); Expr nresp1 = vc_varExpr(vc, "nresp1", vc_bv32Type(vc)); Expr packet_get_int0 = vc_varExpr(vc, "packet_get_int0", vc_bv32Type(vc));