From: vijay_ganesh Date: Thu, 3 Sep 2009 20:14:06 +0000 (+0000) Subject: moved many BeevMgr and related classes print functions into a separate file printers... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4a53abd4fb457c12cbe4991e71abee458525c707;p=francis%2Fstp.git moved many BeevMgr and related classes print functions into a separate file printers/AssortedPrinters.cpp git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@175 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 7ecd09c..79d1545 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -11,6 +11,7 @@ #include #include "printer/printers.h" +#include "printer/AssortedPrinters.h" namespace BEEV { @@ -677,19 +678,6 @@ namespace BEEV return os; } - // FIXME: Made non-ref in the hope that it would work better. - void lp(ASTNode node) - { - cout << lisp(node) << endl; - } - - void lpvec(const ASTVec &vec) - { - vec[0].GetBeevMgr().AlreadyPrintedSet.clear(); - LispPrintVec(cout, vec, 0); - cout << endl; - } - // Copy constructor. Maintain _ref_count ASTNode::ASTNode(const ASTNode &n) : _int_node_ptr(n._int_node_ptr) @@ -1078,21 +1066,6 @@ namespace BEEV cout << NodeSize(a) << endl << endl; } - ostream &ASTNode::LispPrint(ostream &os, int indentation) const - { - printer::Lisp_Print(os, *this, indentation); - } - - ostream &ASTNode::LispPrint_indent(ostream &os, int indentation) const - { - printer::Lisp_Print_indent(os, *this, indentation); - } - - ostream& ASTNode::PL_Print(ostream &os, int indentation) const - { - printer::PL_Print(os, *this, indentation); - } - unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo) { if (clearStatInfo) diff --git a/src/AST/AST.h b/src/AST/AST.h index 6caaefe..2b9e992 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -74,11 +74,10 @@ namespace BEEV //Vector of ASTNodes, used for child nodes among other things. typedef vector ASTVec; + typedef unsigned int * CBV; extern ASTVec _empty_ASTVec; extern BeevMgr * globalBeevMgr_for_parser; - typedef unsigned int * CBV; - /***************************************************************************/ /* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */ /***************************************************************************/ @@ -833,77 +832,6 @@ namespace BEEV //FIXME: move to a more appropriate place extern ASTNodeSet _parser_symbol_table; - /*************************************************************************** - Class LispPrinter: iomanipulator for printing ASTNode or ASTVec - ***************************************************************************/ - class LispPrinter - { - - public: - ASTNode _node; - - // number of spaces to print before first real character of - // object. - int _indentation; - - // FIXME: pass ASTNode by reference - // Constructor to build the LispPrinter object - LispPrinter(ASTNode node, int indentation) : - _node(node), _indentation(indentation) - { - } - - friend ostream &operator<<(ostream &os, const LispPrinter &lp) - { - return lp._node.LispPrint(os, lp._indentation); - } - ; - - }; //End of ListPrinter - - //This is the IO manipulator. It builds an object of class - //"LispPrinter" that has a special overloaded "<<" operator. - inline LispPrinter lisp(const ASTNode &node, int indentation = 0) - { - LispPrinter lp(node, indentation); - return lp; - } - - /***************************************************************************/ - /* Class LispVecPrinter:iomanipulator for printing vector of ASTNodes */ - /***************************************************************************/ - class LispVecPrinter - { - - public: - const ASTVec * _vec; - // number of spaces to print before first real - // character of object. - int _indentation; - - // Constructor to build the LispPrinter object - LispVecPrinter(const ASTVec &vec, int indentation) - { - _vec = &vec; - _indentation = indentation; - } - - friend ostream &operator<<(ostream &os, const LispVecPrinter &lvp) - { - LispPrintVec(os, *lvp._vec, lvp._indentation); - return os; - } - ; - }; //End of Class ListVecPrinter - - //iomanipulator. builds an object of class "LisPrinter" that has a - //special overloaded "<<" operator. - inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0) - { - LispVecPrinter lvp(vec, indentation); - return lvp; - } - /*************************************************************************** * Class BeevMgr. This holds all "global" variables for the system, such as * unique tables for the various kinds of nodes. @@ -1819,6 +1747,5 @@ namespace BEEV } return (unsigned int) *((unsigned int *) n.GetBVConst()); } //end of GetUnsignedConst - }; // end namespace BEEV #endif diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp index 02375fe..e32ada4 100644 --- a/src/AST/AbstractionRefinement.cpp +++ b/src/AST/AbstractionRefinement.cpp @@ -51,11 +51,13 @@ namespace BEEV //are no more axioms to add // //for each array, fetch its list of indices seen so far - for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++) + for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), + iset_end = _arrayname_readindices.end(); iset != iset_end; iset++) { ASTVec listOfIndices = iset->second; //loop over the list of indices for the array and create LA, and add to q - for (ASTVec::iterator it = listOfIndices.begin(), itend = listOfIndices.end(); it != itend; it++) + for (ASTVec::iterator it = listOfIndices.begin(), + itend = listOfIndices.end(); it != itend; it++) { if (BVCONST == it->GetKind()) { @@ -76,7 +78,8 @@ namespace BEEV //we have nonconst index here. create Leibnitz axiom for it //w.r.t every index in listOfIndices - for (ASTVec::iterator it1 = listOfIndices.begin(), itend1 = listOfIndices.end(); it1 != itend1; it1++) + for (ASTVec::iterator it1 = listOfIndices.begin(), + itend1 = listOfIndices.end(); it1 != itend1; it1++) { ASTNode compare_index = *it1; //do not compare with yourself @@ -85,8 +88,9 @@ namespace BEEV //prepare for SAT LOOP //first construct the antecedent for the LA axiom - ASTNode eqOfIndices = (exprless(the_index, compare_index)) ? CreateSimplifiedEQ(the_index, compare_index) : CreateSimplifiedEQ( - compare_index, the_index); + ASTNode eqOfIndices = + (exprless(the_index, compare_index)) ? + CreateSimplifiedEQ(the_index, compare_index) : CreateSimplifiedEQ(compare_index, the_index); ASTNode arr_read2 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index); //get the variable corresponding to the array_read2 @@ -105,7 +109,9 @@ namespace BEEV //RemainingAxioms = CreateNode(AND,RemainingAxioms,LeibnitzAxiom); RemainingAxiomsVec.push_back(LeibnitzAxiom); } - ASTNode FalseAxioms = (FalseAxiomsVec.size() > 1) ? CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0]; + ASTNode FalseAxioms = + (FalseAxiomsVec.size() > 1) ? + CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0]; ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms); //printf("spot 01\n"); int res2 = 2; @@ -122,7 +128,9 @@ namespace BEEV } } } - ASTNode RemainingAxioms = (RemainingAxiomsVec.size() > 1) ? CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0]; + ASTNode RemainingAxioms = + (RemainingAxiomsVec.size() > 1) ? + CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0]; ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms); return CallSAT_ResultCheck(newS, RemainingAxioms, orig_input); } //end of SATBased_ArrayReadRefinement @@ -169,7 +177,9 @@ namespace BEEV } } - writeAxiom = (FalseAxioms.size() != 1) ? CreateNode(AND, FalseAxioms) : FalseAxioms[0]; + writeAxiom = + (FalseAxioms.size() != 1) ? + CreateNode(AND, FalseAxioms) : FalseAxioms[0]; ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom); int res2 = 2; if (FalseAxioms.size() > oldFalseAxiomsSize) @@ -182,7 +192,9 @@ namespace BEEV return res2; } - writeAxiom = (RemainingAxioms.size() != 1) ? CreateNode(AND, RemainingAxioms) : RemainingAxioms[0]; + writeAxiom = + (RemainingAxioms.size() != 1) ? + CreateNode(AND, RemainingAxioms) : RemainingAxioms[0]; ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom); res2 = CallSAT_ResultCheck(newS, writeAxiom, orig_input); if (2 != res2) @@ -217,58 +229,60 @@ namespace BEEV */ } - /* - * 'finiteloop' is the finite loop to be expanded - * - * Every finiteloop has three parts: - * - * 0) Parameter Name - * - * 1) Parameter initialization - * - * 2) Parameter limit value - * - * 3) Increment formula - * - * 4) Formula Body - * - * ParamToCurrentValMap contains a map from parameters to their - * current values in the recursion - * - * Nested FORs are allowed, but only the innermost loop can have a - * formula in it - * - * STEPS: - * - * 0. Populate the top of the parameter stack with 'finiteloop' - * parameter initial, limit and increment values - * - * 1. If formulabody in 'finiteloop' is another for loop, then - * recurse - * - * 2. Else if current parameter value is less than limit value then - * - * Instantiate a singleformula - * - * Check if the formula is true in the current model - * - * If true, discard it - * - * If false, add it to the SAT solver to get a new model. Make - * sure to update array index tables to facilitate array - * read refinement later. - * - * 3. If control reaches here, it means one of the following - * possibilities (We have instantiated all relevant formulas by - * now): - * - * 3.1: We have UNSAT. Return UNSAT - * - * 3.2: We have SAT, and it is indeed a satisfying model - */ int BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap) { - //Make sure that the parameter is a variable + /* + * 'finiteloop' is the finite loop to be expanded + * + * Every finiteloop has three parts: + * + * 0) Parameter Name + * + * 1) Parameter initialization + * + * 2) Parameter limit value + * + * 3) Increment formula + * + * 4) Formula Body + * + * ParamToCurrentValMap contains a map from parameters to their + * current values in the recursion + * + * Nested FORs are allowed, but only the innermost loop can have a + * formula in it + * + * STEPS: + * + * 0. Populate the top of the parameter stack with 'finiteloop' + * parameter initial, limit and increment values + * + * 1. If formulabody in 'finiteloop' is another for loop, then + * recurse + * + * 2. Else if current parameter value is less than limit value then + * + * Instantiate a singleformula + * + * Check if the formula is true in the current model + * + * If true, discard it + * + * If false, add it to the SAT solver to get a new model. Make + * sure to update array index tables to facilitate array + * read refinement later. + * + * 3. If control reaches here, it means one of the following + * possibilities (We have instantiated all relevant formulas by + * now): + * + * 3.1: We have UNSAT. Return UNSAT + * + * 3.2: We have SAT, and it is indeed a satisfying model + */ + + //BVTypeCheck should have already checked the sanity of the input + //FOR-formula ASTNode parameter = finiteloop[0]; int paramInit = GetUnsignedConst(finiteloop[1]); int paramLimit = GetUnsignedConst(finiteloop[2]); diff --git a/src/AST/Makefile b/src/AST/Makefile index 6eb4c8e..fb3ebd1 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -1,7 +1,7 @@ include ../../scripts/Makefile.common #SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp DPLLMgr.cpp ToSAT.cpp Transform.cpp -SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp AbstractionRefinement.cpp printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp printer/PLPrinter.cpp printer/LispPrinter.cpp +SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp AbstractionRefinement.cpp printer/AssortedPrinters.cpp printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp printer/PLPrinter.cpp printer/LispPrinter.cpp OBJS = $(SRCS:.cpp=.o) CFLAGS += -I../sat/mtl -I../sat/core diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index 6d5265d..cd9dbda 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -130,53 +130,7 @@ namespace BEEV return true; else return false; - } - - // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver - void BeevMgr::PrintStats(MINISAT::Solver& s) - { - if (!stats_flag) - return; - double cpu_time = MINISAT::cpuTime(); - uint64_t mem_used = MINISAT::memUsed(); - reportf("restarts : %llu\n", s.starts); - reportf("conflicts : %llu (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); - reportf("decisions : %llu (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); - reportf("propagations : %llu (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); - reportf("conflict literals : %llu (%4.2f %% deleted)\n", s.tot_literals, - (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); - if (mem_used != 0) - reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); - reportf("CPU time : %g s\n", cpu_time); - } - - // Prints Satisfying assignment directly, for debugging. - void BeevMgr::PrintSATModel(MINISAT::Solver& newS) - { - 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)) - return; - - int num_vars = newS.nVars(); - cout << "Satisfying assignment: " << endl; - for (int i = 0; i < num_vars; i++) - { - if (newS.model[i] == MINISAT::l_True) - { - ASTNode s = _SATVar_to_AST[i]; - cout << s << endl; - } - else if (newS.model[i] == MINISAT::l_False) - { - ASTNode s = _SATVar_to_AST[i]; - cout << CreateNode(NOT, s) << endl; - } - } - } + } //end of toSATandSolve() // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying assignment. // Returns ASTTrue if true, ASTFalse if false or undefined. @@ -208,7 +162,7 @@ namespace BEEV CheckBBandCNFMemo.clear(); // Call recursive version that does the work. return CheckBBandCNF_int(newS, form); - } + } //End of CheckBBandCNF() // Recursive body CheckBBandCNF // FIXME: Modify this to just check if result is true, and print mismatch @@ -301,7 +255,7 @@ namespace BEEV } return (CheckBBandCNFMemo[form] = result); - } + } //end of CheckBBandCNF_int() /*FUNCTION: constructs counterexample from MINISAT counterexample * step1 : iterate through MINISAT counterexample and assemble the @@ -924,152 +878,6 @@ namespace BEEV "query evaluates to TRUE under counterexample: NOT OK", _current_query); } - /* FUNCTION: prints a counterexample for INVALID inputs. iterate - * through the CounterExampleMap data structure and print it to - * stdout - */ - 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_flag) - { - return; - } - - //input is valid, no counterexample to print - if (ValidFlag) - { - return; - } - - //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) - { - return; - } - - //t is true if SAT solver generated a counterexample, else it is - //false - if (!t) - { - cerr << "PrintCounterExample: No CounterExample to print: " << endl; - return; - } - - //os << "\nCOUNTEREXAMPLE: \n" << endl; - ASTNodeMap::iterator it = CounterExampleMap.begin(); - ASTNodeMap::iterator itend = CounterExampleMap.end(); - for (; it != itend; it++) - { - ASTNode f = it->first; - ASTNode se = it->second; - - if (ARRAY_TYPE == se.GetType()) - { - FatalError("TermToConstTermUsingModel: entry in counterexample is an arraytype. bogus:", se); - } - - //skip over introduced variables - if (f.GetKind() == SYMBOL && (_introduced_symbols.find(f) != _introduced_symbols.end())) - continue; - if (f.GetKind() == SYMBOL || (f.GetKind() == READ && f[0].GetKind() == SYMBOL && f[1].GetKind() == BVCONST)) - { - os << "ASSERT( "; - f.PL_Print(os,0); - os << " = "; - if (BITVECTOR_TYPE == se.GetType()) - { - TermToConstTermUsingModel(se, false).PL_Print(os, 0); - } - else - { - se.PL_Print(os, 0); - } - os << " );" << endl; - } - } - //os << "\nEND OF COUNTEREXAMPLE" << endl; - } //End of PrintCounterExample - - /* iterate through the CounterExampleMap data structure and print it - * to stdout. this function prints only the declared array variables - * IN the ORDER in which they were declared. It also assumes that - * the variables are of the form 'varname_number'. otherwise it will - * not print anything. This function was specifically written for - * Dawson Engler's group (bug finding research group at Stanford) - */ - void BeevMgr::PrintCounterExample_InOrder(bool t) - { - //global command-line option to print counterexample. we do not - //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) - return; - - //input is valid, no counterexample to print - if (ValidFlag) - return; - - //print if the commandline option is '-q'. allows printing the - //counterexample in order. - if (!print_arrayval_declaredorder_flag) - return; - - //t is true if SAT solver generated a counterexample, else it is - //false - if (!t) - { - cerr << "PrintCounterExample: No CounterExample to print: " << endl; - return; - } - - //vector to store the integer values - std::vector out_int; - cout << "% "; - for (ASTVec::iterator it = _special_print_set.begin(), itend = _special_print_set.end(); it != itend; it++) - { - if (ARRAY_TYPE == it->GetType()) - { - //get the name of the variable - const char * c = it->GetName(); - std::string ss(c); - if (!(0 == strncmp(ss.c_str(), "ini_", 4))) - continue; - reverse(ss.begin(), ss.end()); - - //cout << "debugging: " << ss; - size_t pos = ss.find('_', 0); - if (!((0 < pos) && (pos < ss.size()))) - continue; - - //get the associated length - std::string sss = ss.substr(0, pos); - reverse(sss.begin(), sss.end()); - int n = atoi(sss.c_str()); - - it->PL_Print(cout, 2); - for (int j = 0; j < n; j++) - { - ASTNode index = CreateBVConst(it->GetIndexWidth(), j); - ASTNode readexpr = CreateTerm(READ, it->GetValueWidth(), *it, index); - ASTNode val = GetCounterExample(t, readexpr); - //cout << "ASSERT( "; - //cout << " = "; - out_int.push_back(GetUnsignedConst(val)); - //cout << "\n"; - } - } - } - cout << endl; - for (unsigned int jj = 0; jj < out_int.size(); jj++) - cout << out_int[jj] << endl; - cout << endl; - } //End of PrintCounterExample_InOrder - /* FUNCTION: queries the CounterExampleMap object with 'expr' and * returns the corresponding counterexample value. */ @@ -1101,23 +909,6 @@ namespace BEEV //################################################## //################################################## - - void BeevMgr::printCacheStatus() - { - cerr << SimplifyMap->size() << endl; - cerr << SimplifyNegMap->size() << endl; - cerr << ReferenceCount->size() << endl; - cerr << TermsAlreadySeenMap.size() << endl; - - cerr << SimplifyMap->bucket_count() << endl; - cerr << SimplifyNegMap->bucket_count() << endl; - cerr << ReferenceCount->bucket_count() << endl; - cerr << TermsAlreadySeenMap.bucket_count() << endl; - - - - } - // FIXME: Don't use numeric codes. Use an enum type! //Acceps a query, calls the SAT solver and generates Valid/InValid. //if returned 0 then input is INVALID @@ -1268,48 +1059,5 @@ namespace BEEV cc += '0'; } return CreateBVConst(cc.c_str(), 2); - } - - //This function prints the output of the STP solver - void BeevMgr::PrintOutput(bool true_iff_valid) - { - if (print_output_flag) - { - 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) - { - ValidFlag = true; - if (print_output_flag) - { - if (smtlib_parser_flag) - cout << "unsat\n"; - else - cout << "Valid.\n"; - } - } - else - { - ValidFlag = false; - if (print_output_flag) - { - if (smtlib_parser_flag) - cout << "sat\n"; - else - cout << "Invalid.\n"; - } - } - } -} -; //end of namespace BEEV + } //end of BoolVectoBVConst() +}; //end of namespace BEEV