From: vijay_ganesh Date: Thu, 3 Sep 2009 21:59:12 +0000 (+0000) Subject: more cleanup X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a20226dfe37ef6d6a5841364d1f757e1b0f2454f;p=francis%2Fstp.git more cleanup git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@177 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 79d1545..e0106a5 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -180,7 +180,6 @@ namespace BEEV void ASTNode::MarkAlreadyPrinted() const { - // FIXME: Fetching BeevMgr is annoying. Can we put this in lispprinter class? BeevMgr &bm = GetBeevMgr(); bm.AlreadyPrintedSet.insert(*this); } @@ -251,8 +250,6 @@ namespace BEEV // //2. Letize its childNodes - //FIXME: Fetching BeevMgr is annoying. Can we put this in - //some kind of a printer class bm.PLPrintNodeSet.insert(ccc); //debugging //cerr << ccc; @@ -1238,22 +1235,7 @@ namespace BEEV exit(-1); //assert(0); } - - //Variable Order Printer: A global function which converts a MINISAT - //var into a ASTNODE var. It then prints this var along with - //variable order dcisions taken by MINISAT. - void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision_level, int polarity) - { - BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var]; - cout << spaces(decision_level); - if (polarity) - { - cout << "!"; - } - printer::PL_Print(cout,vv, 0); - cout << endl; - } - + void SortByExprNum(ASTVec& v) { sort(v.begin(), v.end(), exprless); @@ -1266,8 +1248,13 @@ namespace BEEV bool isAtomic(Kind kind) { - if (TRUE == kind || FALSE == kind || EQ == kind || NEQ == kind || BVLT == kind || BVLE == kind || BVGT == kind || BVGE == kind || BVSLT == kind - || BVSLE == kind || BVSGT == kind || BVSGE == kind || SYMBOL == kind || BVGETBIT == kind) + if (TRUE == kind || FALSE == kind || + EQ == kind || NEQ == kind || + BVLT == kind || BVLE == kind || + BVGT == kind || BVGE == kind || + BVSLT == kind || BVSLE == kind || + BVSGT == kind || BVSGE == kind || + SYMBOL == kind || BVGETBIT == kind) return true; return false; } @@ -1282,6 +1269,5 @@ namespace BEEV delete ReferenceCount; } -} -; // end namespace +}; // end namespace beev diff --git a/src/AST/AST.h b/src/AST/AST.h index 2b9e992..cec92f9 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -186,9 +186,6 @@ namespace BEEV } } //end of arithless - // Internal lisp-form printer that does not clear _node_print_table - //ostream &LispPrint1(ostream &os, int indentation) const; - // For lisp DAG printing. Has it been printed already, so we can // just print the node number? bool IsAlreadyPrinted() const; @@ -316,7 +313,6 @@ namespace BEEV ostream& LispPrint(ostream &os, int indentation = 0) const; ostream &LispPrint_indent(ostream &os, int indentation) const; - //Presentation Language Printer ostream& PL_Print(ostream &os, int indentation = 0) const; @@ -528,16 +524,19 @@ namespace BEEV class ASTInteriorEqual { public: - bool operator()(const ASTInterior *int_node_ptr1, const ASTInterior *int_node_ptr2) const + bool operator()(const ASTInterior *int_node_ptr1, + const ASTInterior *int_node_ptr2) const { return (*int_node_ptr1 == *int_node_ptr2); } }; // Used in Equality class for hash tables - friend bool operator==(const ASTInterior &int_node1, const ASTInterior &int_node2) + friend bool operator==(const ASTInterior &int_node1, + const ASTInterior &int_node2) { - return (int_node1._kind == int_node2._kind) && (int_node1._children == int_node2._children); + return (int_node1._kind == int_node2._kind) && + (int_node1._children == int_node2._children); } // Call this when deleting a node that has been stored in the @@ -545,8 +544,8 @@ namespace BEEV virtual void CleanUp(); // Returns kinds. "lispprinter" handles printing of parenthesis - // and childnodes. - // (c_friendly is for printing hex. numbers that C compilers will accept) + // and childnodes. (c_friendly is for printing hex. numbers that C + // compilers will accept) virtual void nodeprint(ostream& os, bool c_friendly = false) { os << _kind_names[_kind]; @@ -857,10 +856,14 @@ namespace BEEV private: // Typedef for unique Interior node table. - typedef hash_set ASTInteriorSet; + typedef hash_set ASTInteriorSet; // Typedef for unique Symbol node (leaf) table. - typedef hash_set ASTSymbolSet; + typedef hash_set ASTSymbolSet; // Unique tables to share nodes whenever possible. ASTInteriorSet _interior_unique_table; @@ -869,15 +872,23 @@ namespace BEEV ASTSymbolSet _symbol_unique_table; //Typedef for unique BVConst node (leaf) table. - typedef hash_set ASTBVConstSet; + typedef hash_set ASTBVConstSet; //table to uniquefy bvconst ASTBVConstSet _bvconst_unique_table; // type of memo table. - typedef hash_map ASTNodeToVecMap; + typedef hash_map ASTNodeToVecMap; - typedef hash_map ASTNodeToSetMap; + typedef hash_map ASTNodeToSetMap; // Memo table for bit blasted terms. If a node has already been // bitblasted, it is mapped to a vector of Boolean formulas for @@ -943,8 +954,10 @@ namespace BEEV // Simplifying create functions ASTNode CreateSimpForm(Kind kind, ASTVec &children); ASTNode CreateSimpForm(Kind kind, const ASTNode& child0); - ASTNode CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1); - ASTNode CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2); + ASTNode CreateSimpForm(Kind kind, + const ASTNode& child0, const ASTNode& child1); + ASTNode CreateSimpForm(Kind kind, const ASTNode& child0, + const ASTNode& child1, const ASTNode& child2); ASTNode CreateSimpNot(const ASTNode& form); @@ -953,9 +966,11 @@ namespace BEEV // not in AST.h ASTNode CreateSimpXor(const ASTNode& form1, const ASTNode& form2); ASTNode CreateSimpXor(ASTVec &children); - ASTNode CreateSimpAndOr(bool isAnd, const ASTNode& form1, const ASTNode& form2); + ASTNode CreateSimpAndOr(bool isAnd, + const ASTNode& form1, const ASTNode& form2); ASTNode CreateSimpAndOr(bool IsAnd, ASTVec &children); - ASTNode CreateSimpFormITE(const ASTNode& child0, const ASTNode& child1, const ASTNode& child2); + ASTNode CreateSimpFormITE(const ASTNode& child0, + const ASTNode& child1, const ASTNode& child2); // Declarations of BitBlaster functions (BitBlast.cpp) public: @@ -1083,11 +1098,15 @@ namespace BEEV // Create and return an interior ASTNode ASTNode CreateNode(Kind kind, const ASTVec &children = _empty_ASTVec); - ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTVec &children = _empty_ASTVec); + ASTNode CreateNode(Kind kind, const ASTNode& child0, + const ASTVec &children = _empty_ASTVec); - ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTVec &children = _empty_ASTVec); + ASTNode CreateNode(Kind kind, const ASTNode& child0, + const ASTNode& child1, const ASTVec &children = _empty_ASTVec); - ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2, const ASTVec &children = _empty_ASTVec); + ASTNode CreateNode(Kind kind, const ASTNode& child0, + const ASTNode& child1, const ASTNode& child2, + const ASTVec &children = _empty_ASTVec); // Create and return an ASTNode for a term inline ASTNode CreateTerm(Kind kind, unsigned int width, const ASTVec &children = _empty_ASTVec) @@ -1103,7 +1122,8 @@ namespace BEEV return n; } - inline ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0, const ASTVec &children = _empty_ASTVec) + inline ASTNode CreateTerm(Kind kind, unsigned int width, + const ASTNode& child0, const ASTVec &children = _empty_ASTVec) { if (!is_Term_kind(kind)) FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind); @@ -1112,7 +1132,9 @@ namespace BEEV return n; } - inline ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0, const ASTNode& child1, const ASTVec &children = _empty_ASTVec) + inline ASTNode CreateTerm(Kind kind, unsigned int width, + const ASTNode& child0, const ASTNode& child1, + const ASTVec &children = _empty_ASTVec) { if (!is_Term_kind(kind)) FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind); @@ -1195,13 +1217,13 @@ namespace BEEV void ClearAllTables(void); void ClearAllCaches(void); - int BeforeSAT_ResultCheck(const ASTNode& q); - int CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input); - int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input); - int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); + int BeforeSAT_ResultCheck(const ASTNode& q); + int CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input); + int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input); + int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); - int SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input); - int Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap); + int SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input); + void Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap); ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody, ASTNodeMap* VarConstMap); diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h index e6df5a5..41f50d1 100644 --- a/src/AST/ASTUtil.h +++ b/src/AST/ASTUtil.h @@ -119,7 +119,7 @@ namespace BEEV { void CountersAndStats(const char * functionname); //global function which accepts an integer and looks up the - //corresponding ASTNode and prints a char* of that ASTNode + //corresponding ASTNode and prints a string of that ASTNode void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision, int polarity=0); }; // end namespace. diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp index e32ada4..63f2dff 100644 --- a/src/AST/AbstractionRefinement.cpp +++ b/src/AST/AbstractionRefinement.cpp @@ -229,7 +229,7 @@ namespace BEEV */ } - int BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop, + void BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap) { /* * 'finiteloop' is the finite loop to be expanded @@ -296,29 +296,39 @@ namespace BEEV (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); //Go recursively thru' all the FOR-constructs. - if(FOR == formulabody.GetKind()) { - while(paramCurrentValue < paramLimit) { - Expand_FiniteLoop(formulabody, ParamToCurrentValMap); - paramCurrentValue = paramCurrentValue + paramIncrement; + if(FOR == formulabody.GetKind()) + { + while(paramCurrentValue < paramLimit) + { + Expand_FiniteLoop(formulabody, ParamToCurrentValMap); + paramCurrentValue = paramCurrentValue + paramIncrement; - //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); - } //end of While - } - else { + //Update ParamToCurrentValMap with parameter and its current + //value + // + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + } //end of While + } + else + { //Expand the leaf level FOR-construct completely for(; paramCurrentValue < paramLimit; - paramCurrentValue = paramCurrentValue + paramIncrement) { - ASTNode currentformula = + paramCurrentValue = paramCurrentValue + paramIncrement) + { + ASTNode currentFormula = FiniteLoop_Extract_SingleFormula(formulabody, ParamToCurrentValMap); //Check the currentformula against the model, and add it to the //SAT solver if it is false against the model + ASTNode formulaInModel = ComputeFormulaUsingModel(currentFormula); + + int result = 0; + if(ASTFalse == formulaInModel) { + //result = CallSAT_ResultCheck(newS, currentFormula, orig_input); + } //Update ParamToCurrentValMap with parameter and its current //value diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp index 7b3b516..1055068 100644 --- a/src/AST/ToCNF.cpp +++ b/src/AST/ToCNF.cpp @@ -1758,18 +1758,6 @@ namespace BEEV //############################################################ - void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll) - { - int num_clauses = cll.size(); - os << "Clauses: " << endl << "=========================================" << endl; - for (int i = 0; i < num_clauses; i++) - { - os << "Clause " << i << endl << "-------------------------------------------" << endl; - LispPrintVecSpecial(os, *cll[i], 0); - os << endl << "-------------------------------------------" << endl; - } - } - void BeevMgr::DeleteClauseList(BeevMgr::ClauseList *cllp) { BeevMgr::ClauseList::const_iterator iend = cllp->end(); @@ -1812,15 +1800,8 @@ namespace BEEV bvdiv_exception_occured = false; ASTNode orig_result = ComputeFormulaUsingModel(orig_input); if (!(ASTTrue == orig_result || ASTFalse == orig_result)) - FatalError("TopLevelSat: Original input must compute to true or false against model"); - - // if(!arrayread_refinement && !(ASTTrue == orig_result)) { - // print_counterexample = true; - // PrintCounterExample(true); - // FatalError("counterexample bogus : arrayread_refinement is switched off: " - // "EITHER all LA axioms have not been added OR bitblaster() or ToCNF()" - // "or satsolver() or counterexamplechecker() have a bug"); - // } + FatalError("TopLevelSat: Original input must compute to "\ + "true or false against model"); // if the counterexample is indeed a good one, then return // invalid diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp index cdca005..42aa67a 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/AST/printer/AssortedPrinters.cpp @@ -182,7 +182,7 @@ namespace BEEV } //End of PrintCounterExample -/* iterate through the CounterExampleMap data structure and print it + /* 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 @@ -313,4 +313,34 @@ namespace BEEV } } } //end of PrintOutput() + + + void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll) + { + int num_clauses = cll.size(); + os << "Clauses: " << endl << "=========================================" << endl; + for (int i = 0; i < num_clauses; i++) + { + os << "Clause " << i << endl << "-------------------------------------------" << endl; + LispPrintVecSpecial(os, *cll[i], 0); + os << endl << "-------------------------------------------" << endl; + } + } //end of PrintClauseList() + + //Variable Order Printer: A global function which converts a MINISAT + //var into a ASTNODE var. It then prints this var along with + //variable order dcisions taken by MINISAT. + void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, + int decision_level, int polarity) + { + BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var]; + cout << spaces(decision_level); + if (polarity) + { + cout << "!"; + } + printer::PL_Print(cout,vv, 0); + cout << endl; + } + };//end of namespace BEEV diff --git a/src/AST/printer/CPrinter.cpp b/src/AST/printer/CPrinter.cpp index 34358bb..2edce1f 100644 --- a/src/AST/printer/CPrinter.cpp +++ b/src/AST/printer/CPrinter.cpp @@ -3,517 +3,517 @@ namespace printer { -using std::string; -using namespace BEEV; - -// printer for C code (copied from PL_Print()) -// TODO: this does not fully implement printing of all of the STP -// language - FatalError calls inserted for unimplemented -// functionality, e.g.,: -// FatalError("C_Print1: printing not implemented for this kind: ",*this); - -// helper function for printing C code (copied from PL_Print1()) -void C_Print1(ostream& os, const ASTNode n, int indentation, bool letize) -{ - - unsigned int upper, lower, num_bytes; - Kind LHSkind, RHSkind; - - //os << spaces(indentation); - //os << endl << spaces(indentation); - if (!n.IsDefined()) - { - os << ""; - return; - } - - //if this node is present in the letvar Map, then print the letvar - BeevMgr &bm = n.GetBeevMgr(); - - //this is to print letvars for shared subterms inside the printing - //of "(LET v0 = term1, v1=term1@term2,... - if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) - { - C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); - return; - } - - //this is to print letvars for shared subterms inside the actual - //term to be printed - if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) - { - C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); - return; - } - - //otherwise print it normally - Kind kind = n.GetKind(); - const ASTVec &c = n.GetChildren(); - switch (kind) - { - case BVGETBIT: - FatalError("C_Print1: printing not implemented for this kind: ", n); - C_Print1(os, c[0], indentation, letize); - os << "{"; - C_Print1(os, c[1], indentation, letize); - os << "}"; - break; - case BITVECTOR: - FatalError("C_Print1: printing not implemented for this kind: ", n); - os << "BITVECTOR("; - unsigned char * str; - str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); - os << str << ")"; - CONSTANTBV::BitVector_Dispose(str); - break; - case BOOLEAN: - FatalError("C_Print1: printing not implemented for this kind: ", n); - os << "BOOLEAN"; - break; - case FALSE: - os << "0"; - break; - case TRUE: - os << "1"; - break; - case BVCONST: - case SYMBOL: - // print in C friendly format: - n.nodeprint(os, true); - break; - case READ: - C_Print1(os, c[0], indentation, letize); - os << "["; - C_Print1(os, c[1], indentation, letize); - os << "]"; - break; - case WRITE: - os << "("; - C_Print1(os, c[0], indentation, letize); - os << " WITH ["; - C_Print1(os, c[1], indentation, letize); - os << "] := "; - C_Print1(os, c[2], indentation, letize); - os << ")"; - os << endl; - break; - case BVUMINUS: - os << kind << "( "; - C_Print1(os, c[0], indentation, letize); - os << ")"; - break; - case NOT: - os << "!("; - C_Print1(os, c[0], indentation, letize); - os << ") " << endl; - break; - case BVNEG: - os << " ~("; - C_Print1(os, c[0], indentation, letize); - os << ")"; - break; - case BVCONCAT: - FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features - os << "("; - C_Print1(os, c[0], indentation, letize); - os << " @ "; - C_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case BVOR: - os << "("; - C_Print1(os, c[0], indentation, letize); - os << " | "; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVAND: - os << "("; - C_Print1(os, c[0], indentation, letize); - os << " & "; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVEXTRACT: - - // we only accept indices that are byte-aligned - // (e.g., [15:8], [23:16]) - // and round down to byte indices rather than bit indices - upper = GetUnsignedConst(c[1]); - lower = GetUnsignedConst(c[2]); - assert(upper > lower); - assert(lower % 8 == 0); - assert((upper + 1) % 8 == 0); - num_bytes = (upper - lower + 1) / 8; - assert (num_bytes > 0); - - // for multi-byte extraction, use the ADDRESS - if (num_bytes > 1) - { - os << "&"; - C_Print1(os, c[0], indentation, letize); - os << "[" << lower / 8 << "]"; - } - // for single-byte extraction, use the VALUE - else - { - C_Print1(os, c[0], indentation, letize); - os << "[" << lower / 8 << "]"; - } - - break; - case BVLEFTSHIFT: - FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features - os << "("; - C_Print1(os, c[0], indentation, letize); - os << " << "; - os << GetUnsignedConst(c[1]); - os << ")"; - break; - case BVRIGHTSHIFT: - FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features - os << "("; - C_Print1(os, c[0], indentation, letize); - os << " >> "; - os << GetUnsignedConst(c[1]); - os << ")"; - break; - case BVMULT: - case BVSUB: - case BVPLUS: - case SBVDIV: - case SBVREM: - case BVDIV: - case BVMOD: - os << kind << "("; - os << n.GetValueWidth(); - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) - { - os << ", " << endl; - C_Print1(os, *it, indentation, letize); - } - os << ")" << endl; - break; - case ITE: - os << "if ("; - C_Print1(os, c[0], indentation, letize); - os << ")" << endl; - os << "{"; - C_Print1(os, c[1], indentation, letize); - os << endl << "} else {"; - C_Print1(os, c[2], indentation, letize); - os << endl << "}"; - break; - case BVLT: - // convert to UNSIGNED before doing comparison! - os << "((unsigned char)"; - C_Print1(os, c[0], indentation, letize); - os << " < "; - os << "(unsigned char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVLE: - // convert to UNSIGNED before doing comparison! - os << "((unsigned char)"; - C_Print1(os, c[0], indentation, letize); - os << " <= "; - os << "(unsigned char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVGT: - // convert to UNSIGNED before doing comparison! - os << "((unsigned char)"; - C_Print1(os, c[0], indentation, letize); - os << " > "; - os << "(unsigned char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVGE: - // convert to UNSIGNED before doing comparison! - os << "((unsigned char)"; - C_Print1(os, c[0], indentation, letize); - os << " >= "; - os << "(unsigned char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVXOR: - case BVNAND: - case BVNOR: - case BVXNOR: - FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features - break; - case BVSLT: - // convert to SIGNED before doing comparison! - os << "((signed char)"; - C_Print1(os, c[0], indentation, letize); - os << " < "; - os << "(signed char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVSLE: - // convert to SIGNED before doing comparison! - os << "((signed char)"; - C_Print1(os, c[0], indentation, letize); - os << " <= "; - os << "(signed char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVSGT: - // convert to SIGNED before doing comparison! - os << "((signed char)"; - C_Print1(os, c[0], indentation, letize); - os << " > "; - os << "(signed char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVSGE: - // convert to SIGNED before doing comparison! - os << "((signed char)"; - C_Print1(os, c[0], indentation, letize); - os << " >= "; - os << "(signed char)"; - C_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case EQ: - // tricky tricky ... if it's a single-byte comparison, - // simply do ==, but if it's multi-byte, must do memcmp - LHSkind = c[0].GetKind(); - RHSkind = c[1].GetKind(); - - num_bytes = 0; - - // try to figure out whether it's a single-byte or multi-byte - // comparison - if (LHSkind == BVEXTRACT) - { - upper = GetUnsignedConst(c[0].GetChildren()[1]); - lower = GetUnsignedConst(c[0].GetChildren()[2]); - num_bytes = (upper - lower + 1) / 8; - } - else if (RHSkind == BVEXTRACT) - { - upper = GetUnsignedConst(c[1].GetChildren()[1]); - lower = GetUnsignedConst(c[1].GetChildren()[2]); - num_bytes = (upper - lower + 1) / 8; - } - - if (num_bytes > 1) - { - os << "(memcmp("; - C_Print1(os, c[0], indentation, letize); - os << ", "; - C_Print1(os, c[1], indentation, letize); - os << ", "; - os << num_bytes; - os << ") == 0)"; - } - else if (num_bytes == 1) - { - os << "("; - C_Print1(os, c[0], indentation, letize); - os << " == "; - C_Print1(os, c[1], indentation, letize); - os << ")"; - } - else - { - FatalError("C_Print1: ugh problem in implementing =="); - } - - break; - case NEQ: - C_Print1(os, c[0], indentation, letize); - os << " != "; - C_Print1(os, c[1], indentation, letize); - os << endl; - break; - case AND: - case OR: - case NAND: - case NOR: - case XOR: - { - os << "("; - C_Print1(os, c[0], indentation, letize); - ASTVec::const_iterator it = c.begin(); - ASTVec::const_iterator itend = c.end(); - - it++; - for (; it != itend; it++) - { - switch (kind) - { - case AND: - os << " && "; - break; - case OR: - os << " || "; - break; - case NAND: - FatalError("unsupported boolean type in C_Print1"); - break; - case NOR: - FatalError("unsupported boolean type in C_Print1"); - break; - case XOR: - FatalError("unsupported boolean type in C_Print1"); - break; - default: - FatalError("unsupported boolean type in C_Print1"); - } - C_Print1(os, *it, indentation, letize); - } - os << ")"; - break; - } - case IFF: - FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features - os << "("; - os << "("; - C_Print1(os, c[0], indentation, letize); - os << ")"; - os << " <=> "; - os << "("; - C_Print1(os, c[1], indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; - case IMPLIES: - FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features - os << "("; - os << "("; - C_Print1(os, c[0], indentation, letize); - os << ")"; - os << " => "; - os << "("; - C_Print1(os, c[1], indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; - case BVSX: - FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features - - os << kind << "("; - C_Print1(os, c[0], indentation, letize); - os << ","; - os << n.GetValueWidth(); - os << ")" << endl; - break; - default: - //remember to use LispPrinter here. Otherwise this function will - //go into an infinite loop. Recall that "<<" is overloaded to - //the lisp printer. FatalError uses lispprinter - FatalError("C_Print1: printing not implemented for this kind: ", n); - break; - } -} //end of C_Print1() - - -//two pass algorithm: -// -//1. In the first pass, letize this Node, N: i.e. if a node -//1. appears more than once in N, then record this fact. -// -//2. In the second pass print a "global let" and then print N -//2. as follows: Every occurence of a node occuring more than -//2. once is replaced with the corresponding let variable. -ostream& C_Print(ostream &os, const ASTNode n, int indentation) -{ - // Clear the PrintMap - BeevMgr& bm = n.GetBeevMgr(); - bm.PLPrintNodeSet.clear(); - bm.NodeLetVarMap.clear(); - bm.NodeLetVarVec.clear(); - bm.NodeLetVarMap1.clear(); - - //pass 1: letize the node - n.LetizeNode(); - - unsigned int lower, upper, num_bytes = 0; - - //pass 2: - // - //2. print all the let variables and their counterpart expressions - //2. as follows (LET var1 = expr1, var2 = expr2, ... - // - //3. Then print the Node itself, replacing every occurence of - //3. expr1 with var1, expr2 with var2, ... - //os << "("; - if (0 < bm.NodeLetVarMap.size()) - { - //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); - //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); - std::vector >::iterator it = bm.NodeLetVarVec.begin(); - std::vector >::iterator itend = bm.NodeLetVarVec.end(); - - // start a new block to create new static scope - os << "{" << endl; - - for (; it != itend; it++) - { - - // see if it's a BVEXTRACT, and if so, whether it's multi-byte - if (it->second.GetKind() == BVEXTRACT) - { - upper = GetUnsignedConst(it->second.GetChildren()[1]); - lower = GetUnsignedConst(it->second.GetChildren()[2]); - num_bytes = (upper - lower + 1) / 8; - assert(num_bytes > 0); - } - - //print the let var first - if (num_bytes > 1) - { - // for multi-byte assignment, use 'memcpy' and array notation - os << "unsigned char "; - C_Print1(os, it->first, indentation, false); - os << "[" << num_bytes << "]; "; - os << "memcpy("; - C_Print1(os, it->first, indentation, false); - os << ", "; - //print the expr - C_Print1(os, it->second, indentation, false); - os << ", " << num_bytes << ");"; - } - else - { - // for single-byte assignment, use '=' - os << "unsigned char "; - C_Print1(os, it->first, indentation, false); - os << " = "; - //print the expr - C_Print1(os, it->second, indentation, false); - os << ";" << endl; - } - - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; - } - - os << endl << "stp_assert "; - C_Print1(os, n, indentation, true); - - os << ";" << endl << "}"; - } - else - { - os << "stp_assert "; - C_Print1(os, n, indentation, false); - os << ";"; - } - //os << " )"; - //os << " "; - - return os; -} //end of C_Print() + using std::string; + using namespace BEEV; + + // printer for C code (copied from PL_Print()) + // TODO: this does not fully implement printing of all of the STP + // language - FatalError calls inserted for unimplemented + // functionality, e.g.,: + // FatalError("C_Print1: printing not implemented for this kind: ",*this); + + // helper function for printing C code (copied from PL_Print1()) + void C_Print1(ostream& os, const ASTNode n, int indentation, bool letize) + { + + unsigned int upper, lower, num_bytes; + Kind LHSkind, RHSkind; + + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) + { + os << ""; + return; + } + + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = n.GetBeevMgr(); + + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) + { + C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) + { + C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + return; + } + + //otherwise print it normally + Kind kind = n.GetKind(); + const ASTVec &c = n.GetChildren(); + switch (kind) + { + case BVGETBIT: + FatalError("C_Print1: printing not implemented for this kind: ", n); + C_Print1(os, c[0], indentation, letize); + os << "{"; + C_Print1(os, c[1], indentation, letize); + os << "}"; + break; + case BITVECTOR: + FatalError("C_Print1: printing not implemented for this kind: ", n); + os << "BITVECTOR("; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); + os << str << ")"; + CONSTANTBV::BitVector_Dispose(str); + break; + case BOOLEAN: + FatalError("C_Print1: printing not implemented for this kind: ", n); + os << "BOOLEAN"; + break; + case FALSE: + os << "0"; + break; + case TRUE: + os << "1"; + break; + case BVCONST: + case SYMBOL: + // print in C friendly format: + n.nodeprint(os, true); + break; + case READ: + C_Print1(os, c[0], indentation, letize); + os << "["; + C_Print1(os, c[1], indentation, letize); + os << "]"; + break; + case WRITE: + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " WITH ["; + C_Print1(os, c[1], indentation, letize); + os << "] := "; + C_Print1(os, c[2], indentation, letize); + os << ")"; + os << endl; + break; + case BVUMINUS: + os << kind << "( "; + C_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case NOT: + os << "!("; + C_Print1(os, c[0], indentation, letize); + os << ") " << endl; + break; + case BVNEG: + os << " ~("; + C_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case BVCONCAT: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " @ "; + C_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVOR: + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " | "; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVAND: + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " & "; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVEXTRACT: + + // we only accept indices that are byte-aligned + // (e.g., [15:8], [23:16]) + // and round down to byte indices rather than bit indices + upper = GetUnsignedConst(c[1]); + lower = GetUnsignedConst(c[2]); + assert(upper > lower); + assert(lower % 8 == 0); + assert((upper + 1) % 8 == 0); + num_bytes = (upper - lower + 1) / 8; + assert (num_bytes > 0); + + // for multi-byte extraction, use the ADDRESS + if (num_bytes > 1) + { + os << "&"; + C_Print1(os, c[0], indentation, letize); + os << "[" << lower / 8 << "]"; + } + // for single-byte extraction, use the VALUE + else + { + C_Print1(os, c[0], indentation, letize); + os << "[" << lower / 8 << "]"; + } + + break; + case BVLEFTSHIFT: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " << "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVRIGHTSHIFT: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " >> "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVMULT: + case BVSUB: + case BVPLUS: + case SBVDIV: + case SBVREM: + case BVDIV: + case BVMOD: + os << kind << "("; + os << n.GetValueWidth(); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + { + os << ", " << endl; + C_Print1(os, *it, indentation, letize); + } + os << ")" << endl; + break; + case ITE: + os << "if ("; + C_Print1(os, c[0], indentation, letize); + os << ")" << endl; + os << "{"; + C_Print1(os, c[1], indentation, letize); + os << endl << "} else {"; + C_Print1(os, c[2], indentation, letize); + os << endl << "}"; + break; + case BVLT: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " < "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVLE: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " <= "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVGT: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " > "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVGE: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " >= "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + break; + case BVSLT: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " < "; + os << "(signed char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVSLE: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " <= "; + os << "(signed char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVSGT: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " > "; + os << "(signed char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVSGE: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " >= "; + os << "(signed char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case EQ: + // tricky tricky ... if it's a single-byte comparison, + // simply do ==, but if it's multi-byte, must do memcmp + LHSkind = c[0].GetKind(); + RHSkind = c[1].GetKind(); + + num_bytes = 0; + + // try to figure out whether it's a single-byte or multi-byte + // comparison + if (LHSkind == BVEXTRACT) + { + upper = GetUnsignedConst(c[0].GetChildren()[1]); + lower = GetUnsignedConst(c[0].GetChildren()[2]); + num_bytes = (upper - lower + 1) / 8; + } + else if (RHSkind == BVEXTRACT) + { + upper = GetUnsignedConst(c[1].GetChildren()[1]); + lower = GetUnsignedConst(c[1].GetChildren()[2]); + num_bytes = (upper - lower + 1) / 8; + } + + if (num_bytes > 1) + { + os << "(memcmp("; + C_Print1(os, c[0], indentation, letize); + os << ", "; + C_Print1(os, c[1], indentation, letize); + os << ", "; + os << num_bytes; + os << ") == 0)"; + } + else if (num_bytes == 1) + { + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " == "; + C_Print1(os, c[1], indentation, letize); + os << ")"; + } + else + { + FatalError("C_Print1: ugh problem in implementing =="); + } + + break; + case NEQ: + C_Print1(os, c[0], indentation, letize); + os << " != "; + C_Print1(os, c[1], indentation, letize); + os << endl; + break; + case AND: + case OR: + case NAND: + case NOR: + case XOR: + { + os << "("; + C_Print1(os, c[0], indentation, letize); + ASTVec::const_iterator it = c.begin(); + ASTVec::const_iterator itend = c.end(); + + it++; + for (; it != itend; it++) + { + switch (kind) + { + case AND: + os << " && "; + break; + case OR: + os << " || "; + break; + case NAND: + FatalError("unsupported boolean type in C_Print1"); + break; + case NOR: + FatalError("unsupported boolean type in C_Print1"); + break; + case XOR: + FatalError("unsupported boolean type in C_Print1"); + break; + default: + FatalError("unsupported boolean type in C_Print1"); + } + C_Print1(os, *it, indentation, letize); + } + os << ")"; + break; + } + case IFF: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + os << "("; + C_Print1(os, c[0], indentation, letize); + os << ")"; + os << " <=> "; + os << "("; + C_Print1(os, c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case IMPLIES: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + os << "("; + C_Print1(os, c[0], indentation, letize); + os << ")"; + os << " => "; + os << "("; + C_Print1(os, c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case BVSX: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + + os << kind << "("; + C_Print1(os, c[0], indentation, letize); + os << ","; + os << n.GetValueWidth(); + os << ")" << endl; + break; + default: + //remember to use LispPrinter here. Otherwise this function will + //go into an infinite loop. Recall that "<<" is overloaded to + //the lisp printer. FatalError uses lispprinter + FatalError("C_Print1: printing not implemented for this kind: ", n); + break; + } + } //end of C_Print1() + + + //two pass algorithm: + // + //1. In the first pass, letize this Node, N: i.e. if a node + //1. appears more than once in N, then record this fact. + // + //2. In the second pass print a "global let" and then print N + //2. as follows: Every occurence of a node occuring more than + //2. once is replaced with the corresponding let variable. + ostream& C_Print(ostream &os, const ASTNode n, int indentation) + { + // Clear the PrintMap + BeevMgr& bm = n.GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); + + //pass 1: letize the node + n.LetizeNode(); + + unsigned int lower, upper, num_bytes = 0; + + //pass 2: + // + //2. print all the let variables and their counterpart expressions + //2. as follows (LET var1 = expr1, var2 = expr2, ... + // + //3. Then print the Node itself, replacing every occurence of + //3. expr1 with var1, expr2 with var2, ... + //os << "("; + if (0 < bm.NodeLetVarMap.size()) + { + //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); + //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); + std::vector >::iterator it = bm.NodeLetVarVec.begin(); + std::vector >::iterator itend = bm.NodeLetVarVec.end(); + + // start a new block to create new static scope + os << "{" << endl; + + for (; it != itend; it++) + { + + // see if it's a BVEXTRACT, and if so, whether it's multi-byte + if (it->second.GetKind() == BVEXTRACT) + { + upper = GetUnsignedConst(it->second.GetChildren()[1]); + lower = GetUnsignedConst(it->second.GetChildren()[2]); + num_bytes = (upper - lower + 1) / 8; + assert(num_bytes > 0); + } + + //print the let var first + if (num_bytes > 1) + { + // for multi-byte assignment, use 'memcpy' and array notation + os << "unsigned char "; + C_Print1(os, it->first, indentation, false); + os << "[" << num_bytes << "]; "; + os << "memcpy("; + C_Print1(os, it->first, indentation, false); + os << ", "; + //print the expr + C_Print1(os, it->second, indentation, false); + os << ", " << num_bytes << ");"; + } + else + { + // for single-byte assignment, use '=' + os << "unsigned char "; + C_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + C_Print1(os, it->second, indentation, false); + os << ";" << endl; + } + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } + + os << endl << "stp_assert "; + C_Print1(os, n, indentation, true); + + os << ";" << endl << "}"; + } + else + { + os << "stp_assert "; + C_Print1(os, n, indentation, false); + os << ";"; + } + //os << " )"; + //os << " "; + + return os; + } //end of C_Print() } diff --git a/src/AST/printer/LispPrinter.cpp b/src/AST/printer/LispPrinter.cpp index 8716be6..51bada5 100644 --- a/src/AST/printer/LispPrinter.cpp +++ b/src/AST/printer/LispPrinter.cpp @@ -3,98 +3,98 @@ namespace printer { -using std::string; -using namespace BEEV; + using std::string; + using namespace BEEV; -ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation); + ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation); -/** Internal function to print in lisp format. Assume newline - and indentation printed already before first line. Recursive - calls will have newline & indent, though */ -ostream &Lisp_Print1(ostream &os, const ASTNode& n, int indentation) -{ - if (!n.IsDefined()) - { - os << ""; - return os; - } - Kind kind = n.GetKind(); - // FIXME: figure out how to avoid symbols with same names as kinds. - // if (kind == READ) { - // const ASTVec &children = GetChildren(); - // children[0].LispPrint1(os, indentation); - // os << "[" << children[1] << "]"; - // } else - if (kind == BVGETBIT) - { - const ASTVec &children = n.GetChildren(); - // child 0 is a symbol. Print without the NodeNum. - os << n.GetNodeNum() << ":"; + /** Internal function to print in lisp format. Assume newline + and indentation printed already before first line. Recursive + calls will have newline & indent, though */ + ostream &Lisp_Print1(ostream &os, const ASTNode& n, int indentation) + { + if (!n.IsDefined()) + { + os << ""; + return os; + } + Kind kind = n.GetKind(); + // FIXME: figure out how to avoid symbols with same names as kinds. + // if (kind == READ) { + // const ASTVec &children = GetChildren(); + // children[0].LispPrint1(os, indentation); + // os << "[" << children[1] << "]"; + // } else + if (kind == BVGETBIT) + { + const ASTVec &children = n.GetChildren(); + // child 0 is a symbol. Print without the NodeNum. + os << n.GetNodeNum() << ":"; - children[0].nodeprint(os,true); - os << "{"; - children[1].nodeprint(os,true); - os << "}"; - } - else if (kind == NOT) - { - const ASTVec &children = n.GetChildren(); - os << n.GetNodeNum() << ":"; - os << "(NOT "; - Lisp_Print1(os,children[0], indentation); - os << ")"; - } - else if (n.Degree() == 0) - { - // Symbol or a kind with no children print as index:NAME if shared, - // even if they have been printed before. - os << n.GetNodeNum() << ":"; - n.nodeprint(os,true); - // os << "(" << _int_node_ptr->_ref_count << ")"; - // os << "{" << GetValueWidth() << "}"; - } - else if (n.IsAlreadyPrinted()) - { - // print non-symbols as "[index]" if seen before. - os << "[" << n.GetNodeNum() << "]"; - // << "(" << _int_node_ptr->_ref_count << ")"; - } - else - { - n.MarkAlreadyPrinted(); - const ASTVec &children = n.GetChildren(); - os << n.GetNodeNum() << ":" - //<< "(" << _int_node_ptr->_ref_count << ")" - << "(" << kind << " "; - // os << "{" << GetValueWidth() << "}"; - ASTVec::const_iterator iend = children.end(); - for (ASTVec::const_iterator i = children.begin(); i != iend; i++) - { - Lisp_Print_indent(os, *i, indentation + 2); - } - os << ")"; - } - return os; -} + children[0].nodeprint(os,true); + os << "{"; + children[1].nodeprint(os,true); + os << "}"; + } + else if (kind == NOT) + { + const ASTVec &children = n.GetChildren(); + os << n.GetNodeNum() << ":"; + os << "(NOT "; + Lisp_Print1(os,children[0], indentation); + os << ")"; + } + else if (n.Degree() == 0) + { + // Symbol or a kind with no children print as index:NAME if shared, + // even if they have been printed before. + os << n.GetNodeNum() << ":"; + n.nodeprint(os,true); + // os << "(" << _int_node_ptr->_ref_count << ")"; + // os << "{" << GetValueWidth() << "}"; + } + else if (n.IsAlreadyPrinted()) + { + // print non-symbols as "[index]" if seen before. + os << "[" << n.GetNodeNum() << "]"; + // << "(" << _int_node_ptr->_ref_count << ")"; + } + else + { + n.MarkAlreadyPrinted(); + const ASTVec &children = n.GetChildren(); + os << n.GetNodeNum() << ":" + //<< "(" << _int_node_ptr->_ref_count << ")" + << "(" << kind << " "; + // os << "{" << GetValueWidth() << "}"; + ASTVec::const_iterator iend = children.end(); + for (ASTVec::const_iterator i = children.begin(); i != iend; i++) + { + Lisp_Print_indent(os, *i, indentation + 2); + } + os << ")"; + } + return os; + } -// Print in lisp format -ostream &Lisp_Print(ostream &os, const ASTNode& n, int indentation) -{ - // Clear the PrintMap - BeevMgr& bm = n.GetBeevMgr(); - bm.AlreadyPrintedSet.clear(); - Lisp_Print_indent(os, n, indentation); - printf("\n"); - return os; -} + // Print in lisp format + ostream &Lisp_Print(ostream &os, const ASTNode& n, int indentation) + { + // Clear the PrintMap + BeevMgr& bm = n.GetBeevMgr(); + bm.AlreadyPrintedSet.clear(); + Lisp_Print_indent(os, n, indentation); + printf("\n"); + return os; + } -// Print newline and indentation, then print the thing. -ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation) -{ - os << endl << spaces(indentation); - Lisp_Print1(os, n, indentation); - return os; -} + // Print newline and indentation, then print the thing. + ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation) + { + os << endl << spaces(indentation); + Lisp_Print1(os, n, indentation); + return os; + } } diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp index 28d23cb..b010506 100644 --- a/src/AST/printer/PLPrinter.cpp +++ b/src/AST/printer/PLPrinter.cpp @@ -3,352 +3,352 @@ namespace printer { -using std::string; -using namespace BEEV; + using std::string; + using namespace BEEV; -void PL_Print1(ostream& os, const ASTNode& n,int indentation, bool letize) -{ - //os << spaces(indentation); - //os << endl << spaces(indentation); - if (!n.IsDefined()) - { - os << ""; - return; - } + void PL_Print1(ostream& os, const ASTNode& n,int indentation, bool letize) + { + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) + { + os << ""; + return; + } - //if this node is present in the letvar Map, then print the letvar - BeevMgr &bm = n.GetBeevMgr(); + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = n.GetBeevMgr(); - //this is to print letvars for shared subterms inside the printing - //of "(LET v0 = term1, v1=term1@term2,... - if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) - { - PL_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); - return; - } + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) + { + PL_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); + return; + } - //this is to print letvars for shared subterms inside the actual - //term to be printed - if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) - { - PL_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); - return; - } + //this is to print letvars for shared subterms inside the actual + //term to be printed + if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) + { + PL_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + return; + } - //otherwise print it normally - Kind kind = n.GetKind(); - const ASTVec &c = n.GetChildren(); - switch (kind) - { - case BVGETBIT: - PL_Print1(os, c[0], indentation, letize); - os << "{"; - PL_Print1(os, c[1],indentation, letize); - os << "}"; - break; - case BITVECTOR: - os << "BITVECTOR("; - unsigned char * str; - str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); - os << str << ")"; - CONSTANTBV::BitVector_Dispose(str); - break; - case BOOLEAN: - os << "BOOLEAN"; - break; - case FALSE: - case TRUE: - os << kind; - break; - case BVCONST: - case SYMBOL: - n.nodeprint(os, true); - break; - case READ: - PL_Print1(os, c[0], indentation, letize); - os << "["; - PL_Print1(os, c[1], indentation, letize); - os << "]"; - break; - case WRITE: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " WITH ["; - PL_Print1(os, c[1], indentation, letize); - os << "] := "; - PL_Print1(os, c[2], indentation, letize); - os << ")"; - os << endl; - break; - case BVUMINUS: - os << kind << "( "; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - break; - case NOT: - os << "NOT("; - PL_Print1(os, c[0], indentation, letize); - os << ") " << endl; - break; - case BVNEG: - os << " ~("; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - break; - case BVCONCAT: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " @ "; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case BVOR: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " | "; - PL_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVAND: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " & "; - PL_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVEXTRACT: - PL_Print1(os, c[0], indentation, letize); - os << "["; - os << GetUnsignedConst(c[1]); - os << ":"; - os << GetUnsignedConst(c[2]); - os << "]"; - break; - case BVLEFTSHIFT: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " << "; - os << GetUnsignedConst(c[1]); - os << ")"; - break; - case BVRIGHTSHIFT: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " >> "; - os << GetUnsignedConst(c[1]); - os << ")"; - break; - case BVMULT: - case BVSUB: - case BVPLUS: - case SBVDIV: - case SBVREM: - case BVDIV: - case BVMOD: - os << kind << "("; - os << n.GetValueWidth(); - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) - { - os << ", " << endl; - PL_Print1(os, *it, indentation, letize); - } - os << ")" << endl; - break; - case ITE: - os << "IF("; - PL_Print1(os, c[0], indentation, letize); - os << ")" << endl; - os << "THEN "; - PL_Print1(os, c[1], indentation, letize); - os << endl << "ELSE "; - PL_Print1(os, c[2], indentation, letize); - os << endl << "ENDIF"; - break; - case BVLT: - case BVLE: - case BVGT: - case BVGE: - case BVXOR: - case BVNAND: - case BVNOR: - case BVXNOR: - os << kind << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case BVSLT: - os << "SBVLT" << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case BVSLE: - os << "SBVLE" << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case BVSGT: - os << "SBVGT" << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case BVSGE: - os << "SBVGE" << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case EQ: - PL_Print1(os,c[0], indentation, letize); - os << " = "; - PL_Print1(os, c[1], indentation, letize); - os << endl; - break; - case NEQ: - PL_Print1(os, c[0], indentation, letize); - os << " /= "; - PL_Print1(os, c[1], indentation, letize); - os << endl; - break; - case AND: - case OR: - case NAND: - case NOR: - case XOR: - { - os << "("; - PL_Print1(os, c[0], indentation, letize); - ASTVec::const_iterator it = c.begin(); - ASTVec::const_iterator itend = c.end(); + //otherwise print it normally + Kind kind = n.GetKind(); + const ASTVec &c = n.GetChildren(); + switch (kind) + { + case BVGETBIT: + PL_Print1(os, c[0], indentation, letize); + os << "{"; + PL_Print1(os, c[1],indentation, letize); + os << "}"; + break; + case BITVECTOR: + os << "BITVECTOR("; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); + os << str << ")"; + CONSTANTBV::BitVector_Dispose(str); + break; + case BOOLEAN: + os << "BOOLEAN"; + break; + case FALSE: + case TRUE: + os << kind; + break; + case BVCONST: + case SYMBOL: + n.nodeprint(os, true); + break; + case READ: + PL_Print1(os, c[0], indentation, letize); + os << "["; + PL_Print1(os, c[1], indentation, letize); + os << "]"; + break; + case WRITE: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " WITH ["; + PL_Print1(os, c[1], indentation, letize); + os << "] := "; + PL_Print1(os, c[2], indentation, letize); + os << ")"; + os << endl; + break; + case BVUMINUS: + os << kind << "( "; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case NOT: + os << "NOT("; + PL_Print1(os, c[0], indentation, letize); + os << ") " << endl; + break; + case BVNEG: + os << " ~("; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case BVCONCAT: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " @ "; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVOR: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " | "; + PL_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVAND: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " & "; + PL_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVEXTRACT: + PL_Print1(os, c[0], indentation, letize); + os << "["; + os << GetUnsignedConst(c[1]); + os << ":"; + os << GetUnsignedConst(c[2]); + os << "]"; + break; + case BVLEFTSHIFT: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " << "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVRIGHTSHIFT: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " >> "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVMULT: + case BVSUB: + case BVPLUS: + case SBVDIV: + case SBVREM: + case BVDIV: + case BVMOD: + os << kind << "("; + os << n.GetValueWidth(); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + { + os << ", " << endl; + PL_Print1(os, *it, indentation, letize); + } + os << ")" << endl; + break; + case ITE: + os << "IF("; + PL_Print1(os, c[0], indentation, letize); + os << ")" << endl; + os << "THEN "; + PL_Print1(os, c[1], indentation, letize); + os << endl << "ELSE "; + PL_Print1(os, c[2], indentation, letize); + os << endl << "ENDIF"; + break; + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + os << kind << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSLT: + os << "SBVLT" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSLE: + os << "SBVLE" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSGT: + os << "SBVGT" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSGE: + os << "SBVGE" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case EQ: + PL_Print1(os,c[0], indentation, letize); + os << " = "; + PL_Print1(os, c[1], indentation, letize); + os << endl; + break; + case NEQ: + PL_Print1(os, c[0], indentation, letize); + os << " /= "; + PL_Print1(os, c[1], indentation, letize); + os << endl; + break; + case AND: + case OR: + case NAND: + case NOR: + case XOR: + { + os << "("; + PL_Print1(os, c[0], indentation, letize); + ASTVec::const_iterator it = c.begin(); + ASTVec::const_iterator itend = c.end(); - it++; - for (; it != itend; it++) - { - os << " " << kind << " "; - PL_Print1(os, *it, indentation, letize); - os << endl; - } - os << ")"; - break; - } - case IFF: - os << "("; - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - os << " <=> "; - os << "("; - PL_Print1(os,c[1], indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; - case IMPLIES: - os << "("; - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - os << " => "; - os << "("; - PL_Print1(os, c[1], indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; - case BVSX: - case BVZX: - os << kind << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - os << n.GetValueWidth(); - os << ")" << endl; - break; - default: - //remember to use LispPrinter here. Otherwise this function will - //go into an infinite loop. Recall that "<<" is overloaded to - //the lisp printer. FatalError uses lispprinter - FatalError("PL_Print1: printing not implemented for this kind: ", n); - break; - } -} //end of PL_Print1() + it++; + for (; it != itend; it++) + { + os << " " << kind << " "; + PL_Print1(os, *it, indentation, letize); + os << endl; + } + os << ")"; + break; + } + case IFF: + os << "("; + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + os << " <=> "; + os << "("; + PL_Print1(os,c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case IMPLIES: + os << "("; + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + os << " => "; + os << "("; + PL_Print1(os, c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case BVSX: + case BVZX: + os << kind << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + os << n.GetValueWidth(); + os << ")" << endl; + break; + default: + //remember to use LispPrinter here. Otherwise this function will + //go into an infinite loop. Recall that "<<" is overloaded to + //the lisp printer. FatalError uses lispprinter + FatalError("PL_Print1: printing not implemented for this kind: ", n); + break; + } + } //end of PL_Print1() -//print in PRESENTATION LANGUAGE -// -//two pass algorithm: -// -//1. In the first pass, letize this Node, N: i.e. if a node -//1. appears more than once in N, then record this fact. -// -//2. In the second pass print a "global let" and then print N -//2. as follows: Every occurence of a node occuring more than -//2. once is replaced with the corresponding let variable. -ostream& PL_Print(ostream &os, const ASTNode& n, int indentation) -{ - // Clear the PrintMap - BeevMgr& bm = n.GetBeevMgr(); - bm.PLPrintNodeSet.clear(); - bm.NodeLetVarMap.clear(); - bm.NodeLetVarVec.clear(); - bm.NodeLetVarMap1.clear(); + //print in PRESENTATION LANGUAGE + // + //two pass algorithm: + // + //1. In the first pass, letize this Node, N: i.e. if a node + //1. appears more than once in N, then record this fact. + // + //2. In the second pass print a "global let" and then print N + //2. as follows: Every occurence of a node occuring more than + //2. once is replaced with the corresponding let variable. + ostream& PL_Print(ostream &os, const ASTNode& n, int indentation) + { + // Clear the PrintMap + BeevMgr& bm = n.GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); - //pass 1: letize the node - n.LetizeNode(); + //pass 1: letize the node + n.LetizeNode(); - //pass 2: - // - //2. print all the let variables and their counterpart expressions - //2. as follows (LET var1 = expr1, var2 = expr2, ... - // - //3. Then print the Node itself, replacing every occurence of - //3. expr1 with var1, expr2 with var2, ... - //os << "("; - if (0 < bm.NodeLetVarMap.size()) - { - //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); - //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); - std::vector >::iterator it = bm.NodeLetVarVec.begin(); - std::vector >::iterator itend = bm.NodeLetVarVec.end(); + //pass 2: + // + //2. print all the let variables and their counterpart expressions + //2. as follows (LET var1 = expr1, var2 = expr2, ... + // + //3. Then print the Node itself, replacing every occurence of + //3. expr1 with var1, expr2 with var2, ... + //os << "("; + if (0 < bm.NodeLetVarMap.size()) + { + //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); + //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); + std::vector >::iterator it = bm.NodeLetVarVec.begin(); + std::vector >::iterator itend = bm.NodeLetVarVec.end(); - os << "(LET "; - //print the let var first - PL_Print1(os, it->first, indentation, false); - os << " = "; - //print the expr - PL_Print1(os, it->second, indentation, false); + os << "(LET "; + //print the let var first + PL_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + PL_Print1(os, it->second, indentation, false); - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; - for (it++; it != itend; it++) - { - os << "," << endl; - //print the let var first - PL_Print1(os, it->first, indentation, false); - os << " = "; - //print the expr - PL_Print1(os, it->second, indentation, false); + for (it++; it != itend; it++) + { + os << "," << endl; + //print the let var first + PL_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + PL_Print1(os, it->second, indentation, false); - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; - } + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } - os << " IN " << endl; - PL_Print1(os, n, indentation, true); - os << ") "; - } - else - PL_Print1(os,n, indentation, false); - //os << " )"; - os << " "; - return os; -} //end of PL_Print() + os << " IN " << endl; + PL_Print1(os, n, indentation, true); + os << ") "; + } + else + PL_Print1(os,n, indentation, false); + //os << " )"; + os << " "; + return os; + } //end of PL_Print() } diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp index d761fe6..1bba628 100644 --- a/src/AST/printer/SMTLIBPrinter.cpp +++ b/src/AST/printer/SMTLIBPrinter.cpp @@ -3,261 +3,261 @@ namespace printer { -using std::string; -using namespace BEEV; + using std::string; + using namespace BEEV; -string functionToSMTLIBName(const BEEV::Kind k); -void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); + string functionToSMTLIBName(const BEEV::Kind k); + void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); -void outputBitVec(const ASTNode n, ostream& os) -{ - Kind k = n.GetKind(); - const ASTVec &c = n.GetChildren(); - ASTNode op; + void outputBitVec(const ASTNode n, ostream& os) + { + Kind k = n.GetKind(); + const ASTVec &c = n.GetChildren(); + ASTNode op; - if (BITVECTOR == k) - { - op = c[0]; - } - else if (BVCONST == k) - { - op = n; - } - else - FatalError("nsadfsdaf"); + if (BITVECTOR == k) + { + op = c[0]; + } + else if (BVCONST == k) + { + op = n; + } + else + FatalError("nsadfsdaf"); - // CONSTANTBV::BitVector_to_Dec returns a signed representation by default. - // Prepend with zero to convert to unsigned. + // CONSTANTBV::BitVector_to_Dec returns a signed representation by default. + // Prepend with zero to convert to unsigned. - os << "bv"; - CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst()); - unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign); - CONSTANTBV::BitVector_Destroy(unsign); - os << str << "[" << op.GetValueWidth() << "]"; - CONSTANTBV::BitVector_Dispose(str); -} + os << "bv"; + CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst()); + unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign); + CONSTANTBV::BitVector_Destroy(unsign); + os << str << "[" << op.GetValueWidth() << "]"; + CONSTANTBV::BitVector_Dispose(str); + } -void SMTLIB_Print1(ostream& os, const ASTNode n, int indentation, bool letize) -{ - //os << spaces(indentation); - //os << endl << spaces(indentation); - if (!n.IsDefined()) - { - os << ""; - return; - } + void SMTLIB_Print1(ostream& os, const ASTNode n, int indentation, bool letize) + { + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) + { + os << ""; + return; + } - //if this node is present in the letvar Map, then print the letvar - BeevMgr &bm = n.GetBeevMgr(); + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = n.GetBeevMgr(); - //this is to print letvars for shared subterms inside the printing - //of "(LET v0 = term1, v1=term1@term2,... - if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) - { - SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); - return; - } + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) + { + SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); + return; + } - //this is to print letvars for shared subterms inside the actual - //term to be printed - if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) - { - SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); - return; - } + //this is to print letvars for shared subterms inside the actual + //term to be printed + if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) + { + SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + return; + } - //otherwise print it normally - Kind kind = n.GetKind(); - const ASTVec &c = n.GetChildren(); - switch (kind) - { - case BITVECTOR: - case BVCONST: - outputBitVec(n, os); - break; + //otherwise print it normally + Kind kind = n.GetKind(); + const ASTVec &c = n.GetChildren(); + switch (kind) + { + case BITVECTOR: + case BVCONST: + outputBitVec(n, os); + break; - case SYMBOL: - n.nodeprint(os); - break; - case FALSE: - os << "false"; - break; - case TRUE: - os << "true"; - break; + case SYMBOL: + n.nodeprint(os); + break; + case FALSE: + os << "false"; + break; + case TRUE: + os << "true"; + break; - case BVSX: - case BVZX: - { - unsigned int amount = GetUnsignedConst(c[1]); - if (BVZX == kind) - os << "(zero_extend["; - else - os << "(sign_extend["; + case BVSX: + case BVZX: + { + unsigned int amount = GetUnsignedConst(c[1]); + if (BVZX == kind) + os << "(zero_extend["; + else + os << "(sign_extend["; - os << amount << "]"; - SMTLIB_Print1(os, c[0], indentation, letize); - os << ")"; - } - break; - case BVEXTRACT: - { - unsigned int upper = GetUnsignedConst(c[1]); - unsigned int lower = GetUnsignedConst(c[2]); - assert(upper >= lower); - os << "(extract[" << upper << ":" << lower << "] "; - SMTLIB_Print1(os, c[0], indentation, letize); - os << ")"; - } - break; - default: - { - os << "(" << functionToSMTLIBName(kind); + os << amount << "]"; + SMTLIB_Print1(os, c[0], indentation, letize); + os << ")"; + } + break; + case BVEXTRACT: + { + unsigned int upper = GetUnsignedConst(c[1]); + unsigned int lower = GetUnsignedConst(c[2]); + assert(upper >= lower); + os << "(extract[" << upper << ":" << lower << "] "; + SMTLIB_Print1(os, c[0], indentation, letize); + os << ")"; + } + break; + default: + { + os << "(" << functionToSMTLIBName(kind); - ASTVec::const_iterator iend = c.end(); - for (ASTVec::const_iterator i = c.begin(); i != iend; i++) - { - os << " "; - SMTLIB_Print1(os, *i, 0, letize); - } + ASTVec::const_iterator iend = c.end(); + for (ASTVec::const_iterator i = c.begin(); i != iend; i++) + { + os << " "; + SMTLIB_Print1(os, *i, 0, letize); + } - os << ")"; - } - } -} + os << ")"; + } + } + } -// copied from Presentation Langauge printer. -ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation) -{ - // Clear the PrintMap - BeevMgr& bm = n.GetBeevMgr(); - bm.PLPrintNodeSet.clear(); - bm.NodeLetVarMap.clear(); - bm.NodeLetVarVec.clear(); - bm.NodeLetVarMap1.clear(); + // copied from Presentation Langauge printer. + ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation) + { + // Clear the PrintMap + BeevMgr& bm = n.GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); - //pass 1: letize the node - n.LetizeNode(); + //pass 1: letize the node + n.LetizeNode(); - //pass 2: - // - //2. print all the let variables and their counterpart expressions - //2. as follows (LET var1 = expr1, var2 = expr2, ... - // - //3. Then print the Node itself, replacing every occurence of - //3. expr1 with var1, expr2 with var2, ... - //os << "("; - if (0 < bm.NodeLetVarMap.size()) - { - //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); - //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); - std::vector >::iterator it = bm.NodeLetVarVec.begin(); - std::vector >::iterator itend = bm.NodeLetVarVec.end(); + //pass 2: + // + //2. print all the let variables and their counterpart expressions + //2. as follows (LET var1 = expr1, var2 = expr2, ... + // + //3. Then print the Node itself, replacing every occurence of + //3. expr1 with var1, expr2 with var2, ... + //os << "("; + if (0 < bm.NodeLetVarMap.size()) + { + //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); + //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); + std::vector >::iterator it = bm.NodeLetVarVec.begin(); + std::vector >::iterator itend = bm.NodeLetVarVec.end(); - os << "(LET "; - //print the let var first - SMTLIB_Print1(os, it->first, indentation, false); - os << " = "; - //print the expr - SMTLIB_Print1(os, it->second, indentation, false); + os << "(LET "; + //print the let var first + SMTLIB_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + SMTLIB_Print1(os, it->second, indentation, false); - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; - for (it++; it != itend; it++) - { - os << "," << endl; - //print the let var first - SMTLIB_Print1(os, it->first, indentation, false); - os << " = "; - //print the expr - SMTLIB_Print1(os, it->second, indentation, false); + for (it++; it != itend; it++) + { + os << "," << endl; + //print the let var first + SMTLIB_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + SMTLIB_Print1(os, it->second, indentation, false); - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; - } + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } - os << " IN " << endl; - SMTLIB_Print1(os, n, indentation, true); - os << ") "; - } - else - SMTLIB_Print1(os, n, indentation, false); + os << " IN " << endl; + SMTLIB_Print1(os, n, indentation, true); + os << ") "; + } + else + SMTLIB_Print1(os, n, indentation, false); - os << endl; - return os; -} + os << endl; + return os; + } -string functionToSMTLIBName(const Kind k) -{ - switch (k) - { - case AND: - case BVAND: - case BVNAND: - case BVNOR: - case BVOR: - case BVSGE: - case BVSGT: - case BVSLE: - case BVSLT: - case BVSUB: - case BVXOR: - case ITE: - case NAND: - case NOR: - case NOT: - case OR: - case XOR: - case IFF: - return _kind_names[k]; + string functionToSMTLIBName(const Kind k) + { + switch (k) + { + case AND: + case BVAND: + case BVNAND: + case BVNOR: + case BVOR: + case BVSGE: + case BVSGT: + case BVSLE: + case BVSLT: + case BVSUB: + case BVXOR: + case ITE: + case NAND: + case NOR: + case NOT: + case OR: + case XOR: + case IFF: + return _kind_names[k]; - case BVCONCAT: - return "concat"; - case BVDIV: - return "bvudiv"; - case BVGT: - return "bvugt"; - case BVGE: - return "bvuge"; - case BVLE: - return "bvule"; - case BVLEFTSHIFT: - return "bvshl"; - case BVLT: - return "bvult"; - case BVMOD: - return "bvurem"; - case BVMULT: - return "bvmul"; - case BVNEG: - return "bvnot"; // CONFUSSSSINNG. (1/2) - case BVPLUS: - return "bvadd"; - case BVRIGHTSHIFT: - return "bvlshr"; // logical - case BVSRSHIFT: - return "bvashr"; // arithmetic. - case BVUMINUS: - return "bvneg"; // CONFUSSSSINNG. (2/2) - case EQ: - return "="; - case READ: - return "select"; - case WRITE: - return "store"; - case SBVDIV: - return "bvsdiv"; - case SBVREM: - return "bvsrem"; + case BVCONCAT: + return "concat"; + case BVDIV: + return "bvudiv"; + case BVGT: + return "bvugt"; + case BVGE: + return "bvuge"; + case BVLE: + return "bvule"; + case BVLEFTSHIFT: + return "bvshl"; + case BVLT: + return "bvult"; + case BVMOD: + return "bvurem"; + case BVMULT: + return "bvmul"; + case BVNEG: + return "bvnot"; // CONFUSSSSINNG. (1/2) + case BVPLUS: + return "bvadd"; + case BVRIGHTSHIFT: + return "bvlshr"; // logical + case BVSRSHIFT: + return "bvashr"; // arithmetic. + case BVUMINUS: + return "bvneg"; // CONFUSSSSINNG. (2/2) + case EQ: + return "="; + case READ: + return "select"; + case WRITE: + return "store"; + case SBVDIV: + return "bvsdiv"; + case SBVREM: + return "bvsrem"; - default: - { - cerr << "Unknown name when outputting:"; - FatalError(_kind_names[k]); - return ""; // to quieten compiler/ - } - } -} + default: + { + cerr << "Unknown name when outputting:"; + FatalError(_kind_names[k]); + return ""; // to quieten compiler/ + } + } + } } diff --git a/src/AST/printer/dotPrinter.cpp b/src/AST/printer/dotPrinter.cpp index 7038567..b2b24a0 100644 --- a/src/AST/printer/dotPrinter.cpp +++ b/src/AST/printer/dotPrinter.cpp @@ -7,67 +7,67 @@ namespace printer { -using std::string; -using namespace BEEV; + using std::string; + using namespace BEEV; -void outputBitVec(const ASTNode n, ostream& os); + void outputBitVec(const ASTNode n, ostream& os); -void Dot_Print1(ostream &os, const ASTNode n, hash_set *alreadyOutput) -{ + void Dot_Print1(ostream &os, const ASTNode n, hash_set *alreadyOutput) + { - // check if this node has already been printed. If so return. - if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end()) - return; - - alreadyOutput->insert(n.GetNodeNum()); - - os << "n" << n.GetNodeNum() << "[label =\""; - switch (n.GetKind()) - { - case SYMBOL: - n.nodeprint(os); - break; - - case BITVECTOR: - case BVCONST: - outputBitVec(n, os); - break; - - default: - os << _kind_names[n.GetKind()]; - } - - os << "\"];" << endl; - - // print the edges to each child. - ASTVec ch = n.GetChildren(); - ASTVec::iterator itend = ch.end(); - int i = 0; - for (ASTVec::iterator it = ch.begin(); it < itend; it++) - { - os << "n" << n.GetNodeNum() << " -> " << "n" << it->GetNodeNum() << "[label=" << i++ << "];" << endl; - } - - // print each of the children. - for (ASTVec::iterator it = ch.begin(); it < itend; it++) - { - Dot_Print1(os, *it, alreadyOutput); - } -} + // check if this node has already been printed. If so return. + if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end()) + return; -ostream& Dot_Print(ostream &os, const ASTNode n) -{ + alreadyOutput->insert(n.GetNodeNum()); - os << "digraph G{" << endl; + os << "n" << n.GetNodeNum() << "[label =\""; + switch (n.GetKind()) + { + case SYMBOL: + n.nodeprint(os); + break; - // create hashmap to hold integers (node numbers). - hash_set alreadyOutput; + case BITVECTOR: + case BVCONST: + outputBitVec(n, os); + break; - Dot_Print1(os, n, &alreadyOutput); + default: + os << _kind_names[n.GetKind()]; + } - os << "}" << endl; + os << "\"];" << endl; - return os; -} + // print the edges to each child. + ASTVec ch = n.GetChildren(); + ASTVec::iterator itend = ch.end(); + int i = 0; + for (ASTVec::iterator it = ch.begin(); it < itend; it++) + { + os << "n" << n.GetNodeNum() << " -> " << "n" << it->GetNodeNum() << "[label=" << i++ << "];" << endl; + } + + // print each of the children. + for (ASTVec::iterator it = ch.begin(); it < itend; it++) + { + Dot_Print1(os, *it, alreadyOutput); + } + } + + ostream& Dot_Print(ostream &os, const ASTNode n) + { + + os << "digraph G{" << endl; + + // create hashmap to hold integers (node numbers). + hash_set alreadyOutput; + + Dot_Print1(os, n, &alreadyOutput); + + os << "}" << endl; + + return os; + } } diff --git a/src/AST/printer/printers.h b/src/AST/printer/printers.h index 19829e9..46c1e4f 100644 --- a/src/AST/printer/printers.h +++ b/src/AST/printer/printers.h @@ -8,14 +8,14 @@ namespace printer { -ostream& Dot_Print(ostream &os, const BEEV::ASTNode n); + ostream& Dot_Print(ostream &os, const BEEV::ASTNode n); -ostream& SMTLIB_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0); -ostream& C_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0); -ostream& PL_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); + ostream& SMTLIB_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0); + ostream& C_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0); + ostream& PL_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); -ostream& Lisp_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); -ostream& Lisp_Print_indent(ostream &os, const BEEV::ASTNode& n,int indentation=0); + ostream& Lisp_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); + ostream& Lisp_Print_indent(ostream &os, const BEEV::ASTNode& n,int indentation=0); }