From 73ef1a39122cad430bf6a6c65a439abbfe1bddbb Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Thu, 1 Oct 2009 18:08:32 +0000 Subject: [PATCH] massive changes. Added a LESSBYTES_PER_NODE option. Cuts down the bytesize of nodes by more than 20% git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@269 e59a4935-1847-0410-ae03-e826735625c1 --- CODING_GUIDLINES | 7 +++ scripts/Makefile.common | 1 + src/AST/AST.cpp | 44 +++++++-------- src/AST/AST.h | 70 +++++++++++++----------- src/AST/Transform.cpp | 82 ++++++++++++++-------------- src/AST/printer/AssortedPrinters.cpp | 2 +- src/AST/printer/CPrinter.cpp | 32 +++++------ src/AST/printer/LispPrinter.cpp | 4 +- src/AST/printer/PLPrinter.cpp | 36 ++++++------ src/AST/printer/SMTLIBPrinter.cpp | 42 +++++++------- src/c_interface/c_interface.cpp | 38 +------------ src/simplifier/simplifier.cpp | 2 +- src/to-sat/BitBlast.cpp | 17 ------ src/to-sat/ToCNF.cpp | 4 +- 14 files changed, 173 insertions(+), 208 deletions(-) create mode 100644 CODING_GUIDLINES diff --git a/CODING_GUIDLINES b/CODING_GUIDLINES new file mode 100644 index 0000000..1508592 --- /dev/null +++ b/CODING_GUIDLINES @@ -0,0 +1,7 @@ +1. We try to follow the GNU coding guidelines and indentation +standards. Please visit the following website to learn more: + +http://www.gnu.org/prep/standards/standards.html + +2. The code is automatically formatted with the indent tool before +check-in. diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 9f83afe..95f34a5 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -7,6 +7,7 @@ #OPTIMIZE = -g -pg # Debugging and gprof-style profiling OPTIMIZE = -g # Debugging OPTIMIZE = -O3 -DNDEBUG # Maximum optimization +#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE CFLAGS_BASE = $(OPTIMIZE) diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 69b13ab..881c4ee 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -102,7 +102,7 @@ namespace BEEV void ASTInterior::CleanUp() { // cout << "Deleting node " << this->GetNodeNum() << endl; - _bm._interior_unique_table.erase(this); + GlobalBeevMgr->_interior_unique_table.erase(this); delete this; } @@ -112,8 +112,8 @@ namespace BEEV //ASTNode constructors are inlined in AST.h bool ASTNode::IsAlreadyPrinted() const { - BeevMgr &bm = GetBeevMgr(); - return (bm.AlreadyPrintedSet.find(*this) != bm.AlreadyPrintedSet.end()); + BeevMgr * bm = GetBeevMgr(); + return (bm->AlreadyPrintedSet.find(*this) != bm->AlreadyPrintedSet.end()); } void ASTNode::nodeprint(ostream& os, bool c_friendly) const @@ -123,8 +123,8 @@ namespace BEEV void ASTNode::MarkAlreadyPrinted() const { - BeevMgr &bm = GetBeevMgr(); - bm.AlreadyPrintedSet.insert(*this); + BeevMgr * bm = GetBeevMgr(); + bm->AlreadyPrintedSet.insert(*this); } // Get the name from a symbol (char *). It's an error if kind != SYMBOL @@ -180,12 +180,12 @@ namespace BEEV return; //FIXME: this is ugly. - BeevMgr& bm = GetBeevMgr(); + BeevMgr * bm = GetBeevMgr(); const ASTVec &c = this->GetChildren(); for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { ASTNode ccc = *it; - if (bm.PLPrintNodeSet.find(ccc) == bm.PLPrintNodeSet.end()) + if (bm->PLPrintNodeSet.find(ccc) == bm->PLPrintNodeSet.end()) { //If branch: if *it is not in NodeSet then, // @@ -193,7 +193,7 @@ namespace BEEV // //2. Letize its childNodes - bm.PLPrintNodeSet.insert(ccc); + bm->PLPrintNodeSet.insert(ccc); //debugging //cerr << ccc; ccc.LetizeNode(); @@ -211,15 +211,15 @@ namespace BEEV // //2. if no, then create a new var and add it to the //2. NodeLetVarMap - if (bm.NodeLetVarMap.find(ccc) == bm.NodeLetVarMap.end()) + if (bm->NodeLetVarMap.find(ccc) == bm->NodeLetVarMap.end()) { //Create a new symbol. Get some name. if it conflicts with a //declared name, too bad. - int sz = bm.NodeLetVarMap.size(); + int sz = bm->NodeLetVarMap.size(); ostringstream oss; oss << "let_k_" << sz; - ASTNode CurrentSymbol = bm.CreateSymbol(oss.str().c_str()); + ASTNode CurrentSymbol = bm->CreateSymbol(oss.str().c_str()); CurrentSymbol.SetValueWidth(this->GetValueWidth()); CurrentSymbol.SetIndexWidth(this->GetIndexWidth()); /* If for some reason the variable being created here is @@ -228,9 +228,9 @@ namespace BEEV * check for this. [Vijay is the author of this comment.] */ - bm.NodeLetVarMap[ccc] = CurrentSymbol; + bm->NodeLetVarMap[ccc] = CurrentSymbol; std::pair node_letvar_pair(CurrentSymbol, ccc); - bm.NodeLetVarVec.push_back(node_letvar_pair); + bm->NodeLetVarVec.push_back(node_letvar_pair); } } } @@ -244,7 +244,7 @@ namespace BEEV ASTNode BeevMgr::CreateNode(Kind kind, const ASTVec & back_children) { // create a new node. Children will be modified. - ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTInterior *n_ptr = new ASTInterior(kind); // insert all of children at end of new_children. ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); @@ -254,7 +254,7 @@ namespace BEEV ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTVec & back_children) { - ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTInterior *n_ptr = new ASTInterior(kind); ASTVec &front_children = n_ptr->_children; front_children.push_back(child0); ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); @@ -264,7 +264,7 @@ namespace BEEV ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTVec & back_children) { - ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTInterior *n_ptr = new ASTInterior(kind); ASTVec &front_children = n_ptr->_children; front_children.push_back(child0); front_children.push_back(child1); @@ -274,7 +274,7 @@ namespace BEEV ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2, const ASTVec & back_children) { - ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTInterior *n_ptr = new ASTInterior(kind); ASTVec &front_children = n_ptr->_children; front_children.push_back(child0); front_children.push_back(child1); @@ -326,7 +326,7 @@ namespace BEEV //////////////////////////////////////////////////////////////// ASTNode BeevMgr::CreateSymbol(const char * const name) { - ASTSymbol temp_sym(name, *this); + ASTSymbol temp_sym(name); ASTNode n(LookupOrCreateSymbol(temp_sym)); return n; } @@ -451,7 +451,7 @@ namespace BEEV //FIXME Code currently assumes that it will destroy the bitvector passed to it ASTNode BeevMgr::CreateBVConst(CBV bv, unsigned width) { - ASTBVConst temp_bvconst(bv, width, *this); + ASTBVConst temp_bvconst(bv, width); ASTNode n(LookupOrCreateBVConst(temp_bvconst)); CONSTANTBV::BitVector_Destroy(bv); @@ -521,7 +521,7 @@ namespace BEEV void ASTBVConst::CleanUp() { // cout << "Deleting node " << this->GetNodeNum() << endl; - _bm._bvconst_unique_table.erase(this); + GlobalBeevMgr->_bvconst_unique_table.erase(this); delete this; } @@ -557,7 +557,7 @@ namespace BEEV // _name because it's const). Can cast the iterator to // non-const -- carefully. //std::string strname(s_ptr->GetName()); - ASTSymbol * s_ptr1 = new ASTSymbol(strdup(s_ptr->GetName()), *this); + ASTSymbol * s_ptr1 = new ASTSymbol(strdup(s_ptr->GetName())); s_ptr1->SetNodeNum(NewNodeNum()); s_ptr1->_value_width = s_ptr->_value_width; pair p = _symbol_unique_table.insert(s_ptr1); @@ -582,7 +582,7 @@ namespace BEEV void ASTSymbol::CleanUp() { // cout << "Deleting node " << this->GetNodeNum() << endl; - _bm._symbol_unique_table.erase(this); + GlobalBeevMgr->_symbol_unique_table.erase(this); //FIXME This is a HUGE free to invoke. //TEST IT! free((char*) this->_name); diff --git a/src/AST/AST.h b/src/AST/AST.h index e0eb3c7..2615cc9 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -245,7 +245,7 @@ namespace BEEV // Assignment (for ref counting) ASTNode& operator=(const ASTNode& n); - BeevMgr &GetBeevMgr() const; + BeevMgr* GetBeevMgr() const; // Access node number int GetNodeNum() const; @@ -414,36 +414,42 @@ namespace BEEV friend class CNFMgr; protected: - // reference count. - int _ref_count; + //#ifdef LESSBYTES_PERNODE + //unsigned short _ref_count; + //#else + unsigned int _ref_count; + //#endif // Kind. It's a type tag and the operator. - //Kind _kind; enumeration _kind; // The vector of children (*** should this be in ASTInterior? ***) ASTVec _children; - // Manager object. Having this backpointer means it's easy to - // find the manager when we need it. - BeevMgr &_bm; - //Nodenum is a unique positive integer for the node. The nodenum //of a node should always be greater than its descendents (which //is easily achieved by incrementing the number each time a new //node is created). - int _node_num; + unsigned int _node_num; // Length of bitvector type for array index. The term is an // array iff this is positive. Otherwise, the term is a bitvector // or a bit. - unsigned short _index_width; +#ifdef LESSBYTES_PERNODE + unsigned char _index_width; +#else + unsigned int _index_width; +#endif // Length of bitvector type for scalar value or array element. // If this is one, the term represents a single bit (same as a bitvector // of length 1). It must be 1 or greater. - unsigned short _value_width; +#ifdef LESSBYTES_PERNODE + unsigned char _value_width; +#else + unsigned int _value_width; +#endif // Increment refcount. void IncRef() @@ -480,15 +486,15 @@ namespace BEEV ; // Constructor (bm only) - ASTInternal(BeevMgr &bm, int nodenum = 0) : - _ref_count(0), _kind(UNDEFINED), _bm(bm), + ASTInternal(int nodenum = 0) : + _ref_count(0), _kind(UNDEFINED), _node_num(nodenum), _index_width(0), _value_width(0) { } // Constructor (kind only, empty children, int nodenum) - ASTInternal(Kind kind, BeevMgr &bm, int nodenum = 0) : - _ref_count(0), _kind(kind), _bm(bm), + ASTInternal(Kind kind, int nodenum = 0) : + _ref_count(0), _kind(kind), _node_num(nodenum), _index_width(0), _value_width(0) { } @@ -496,9 +502,9 @@ namespace BEEV // Constructor (kind and children). This copies the contents of // the child nodes. // FIXME: is there a way to avoid repeating these? - ASTInternal(Kind kind, const ASTVec &children, BeevMgr &bm, int nodenum = 0) : + ASTInternal(Kind kind, const ASTVec &children, int nodenum = 0) : _ref_count(0), _kind(kind), _children(children), - _bm(bm), _node_num(nodenum), _index_width(0), _value_width(0) + _node_num(nodenum), _index_width(0), _value_width(0) { } @@ -509,7 +515,7 @@ namespace BEEV // FIXME: I don't think children need to be copied. ASTInternal(const ASTInternal &int_node, int nodenum = 0) : _ref_count(0), _kind(int_node._kind), - _children(int_node._children), _bm(int_node._bm), + _children(int_node._children), _node_num(int_node._node_num), _index_width(int_node._index_width), _value_width(int_node._value_width) { @@ -593,13 +599,13 @@ namespace BEEV // to put "friend class hash_set" in here. // Basic constructors - ASTInterior(Kind kind, BeevMgr &bm) : - ASTInternal(kind, bm) + ASTInterior(Kind kind) : + ASTInternal(kind) { } - ASTInterior(Kind kind, ASTVec &children, BeevMgr &bm) : - ASTInternal(kind, children, bm) + ASTInterior(Kind kind, ASTVec &children) : + ASTInternal(kind, children) { } @@ -680,14 +686,14 @@ namespace BEEV public: // Default constructor - ASTSymbol(BeevMgr &bm) : - ASTInternal(bm), _name(NULL) + ASTSymbol() : + ASTInternal(), _name(NULL) { } // Constructor. This does NOT copy its argument. - ASTSymbol(const char * const name, BeevMgr &bm) : - ASTInternal(SYMBOL, bm), _name(name) + ASTSymbol(const char * const name) : + ASTInternal(SYMBOL), _name(name) { } @@ -697,7 +703,7 @@ namespace BEEV // Copy constructor // FIXME: seems to be calling default constructor for astinternal ASTSymbol(const ASTSymbol &sym) : - ASTInternal(sym._kind, sym._children, sym._bm), _name(sym._name) + ASTInternal(sym._kind, sym._children), _name(sym._name) { } }; //End of ASTSymbol @@ -742,8 +748,8 @@ namespace BEEV }; //FIXME Keep an eye on this function - ASTBVConst(CBV bv, unsigned int width, BeevMgr &bm) : - ASTInternal(BVCONST, bm) + ASTBVConst(CBV bv, unsigned int width) : + ASTInternal(BVCONST) { _bvconst = CONSTANTBV::BitVector_Clone(bv); _value_width = width; @@ -812,7 +818,7 @@ namespace BEEV // Copy constructor. ASTBVConst(const ASTBVConst &sym) : - ASTInternal(sym._kind, sym._children, sym._bm) + ASTInternal(sym._kind, sym._children) { _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst); _value_width = sym._value_width; @@ -1804,9 +1810,9 @@ namespace BEEV } } - inline BeevMgr& ASTNode::GetBeevMgr() const + inline BeevMgr* ASTNode::GetBeevMgr() const { - return _int_node_ptr->_bm; + return GlobalBeevMgr; } //Return the unsigned constant value of the input 'n' diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index d89a78f..ba7635e 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -57,37 +57,37 @@ namespace BEEV //Translates signed BVDIV,BVMOD and BVREM into unsigned variety ASTNode TranslateSignedDivModRem(const ASTNode& in) { - BeevMgr& bm = in.GetBeevMgr(); + BeevMgr* bm = GlobalBeevMgr; assert(in.GetChildren().size() ==2); ASTNode dividend = in[0]; ASTNode divisor = in[1]; unsigned len = in.GetValueWidth(); - ASTNode hi1 = bm.CreateBVConst(32, len - 1); - ASTNode one = bm.CreateOneConst(1); - ASTNode zero = bm.CreateZeroConst(1); + ASTNode hi1 = bm->CreateBVConst(32, len - 1); + ASTNode one = bm->CreateOneConst(1); + ASTNode zero = bm->CreateZeroConst(1); // create the condition for the dividend - ASTNode cond_dividend = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)); + ASTNode cond_dividend = bm->CreateNode(EQ, one, bm->CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)); // create the condition for the divisor - ASTNode cond_divisor = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1)); + ASTNode cond_divisor = bm->CreateNode(EQ, one, bm->CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1)); if (SBVREM == in.GetKind()) { //BVMOD is an expensive operation. So have the fewest bvmods possible. Just one. //Take absolute value. - ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend); - ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor); + ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor); //create the modulus term - ASTNode modnode = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor); + ASTNode modnode = bm->CreateTerm(BVMOD, len, pos_dividend, pos_divisor); //If the dividend is <0 take the unary minus. - ASTNode n = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, modnode), modnode); + ASTNode n = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, modnode), modnode); //put everything together, simplify, and return - return bm.SimplifyTerm_TopLevel(n); + return bm->SimplifyTerm_TopLevel(n); } // This is the modulus of dividing rounding to -infinity. @@ -106,19 +106,19 @@ namespace BEEV // (bvneg (bvurem (bvneg s) (bvneg t))))))) //Take absolute value. - ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend); - ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor); + ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor); - ASTNode urem_node = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor); + ASTNode urem_node = bm->CreateTerm(BVMOD, len, pos_dividend, pos_divisor); // If the dividend is <0, then we negate the whole thing. - ASTNode rev_node = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, urem_node), urem_node); + ASTNode rev_node = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, urem_node), urem_node); // if It's XOR <0 then add t (not its absolute value). - ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor); - ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVPLUS, len, rev_node, divisor), rev_node); + ASTNode xor_node = bm->CreateNode(XOR, cond_dividend, cond_divisor); + ASTNode n = bm->CreateTerm(ITE, len, xor_node, bm->CreateTerm(BVPLUS, len, rev_node, divisor), rev_node); - return bm.SimplifyTerm_TopLevel(n); + return bm->SimplifyTerm_TopLevel(n); } else if (SBVDIV == in.GetKind()) { @@ -138,20 +138,20 @@ namespace BEEV //else simply output BVDIV(dividend,divisor) //Take absolute value. - ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend); - ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor); + ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor); - ASTNode divnode = bm.CreateTerm(BVDIV, len, pos_dividend, pos_divisor); + ASTNode divnode = bm->CreateTerm(BVDIV, len, pos_dividend, pos_divisor); // A little confusing. Only negate the result if they are XOR <0. - ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor); - ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVUMINUS, len, divnode), divnode); + ASTNode xor_node = bm->CreateNode(XOR, cond_dividend, cond_divisor); + ASTNode n = bm->CreateTerm(ITE, len, xor_node, bm->CreateTerm(BVUMINUS, len, divnode), divnode); - return bm.SimplifyTerm_TopLevel(n); + return bm->SimplifyTerm_TopLevel(n); } FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in); - return bm.CreateNode(UNDEFINED); + return bm->CreateNode(UNDEFINED); }//end of TranslateSignedDivModRem() @@ -207,7 +207,7 @@ namespace BEEV ********************************************************/ ASTNode TransformFormula(const ASTNode& form) { - BeevMgr& bm = form.GetBeevMgr(); + BeevMgr* bm = form.GetBeevMgr(); assert(TransformMap != NULL); @@ -237,7 +237,7 @@ namespace BEEV { ASTVec c; c.push_back(TransformFormula(simpleForm[0])); - result = bm.CreateNode(NOT, c); + result = bm->CreateNode(NOT, c); break; } case BVLT: @@ -252,14 +252,14 @@ namespace BEEV ASTVec c; c.push_back(TransformTerm(simpleForm[0])); c.push_back(TransformTerm(simpleForm[1])); - result = bm.CreateNode(k, c); + result = bm->CreateNode(k, c); break; } case EQ: { ASTNode term1 = TransformTerm(simpleForm[0]); ASTNode term2 = TransformTerm(simpleForm[1]); - result = bm.CreateSimplifiedEQ(term1, term2); + result = bm->CreateSimplifiedEQ(term1, term2); break; } case AND: @@ -279,14 +279,14 @@ namespace BEEV vec.push_back(o); } - result = bm.CreateNode(k, vec); + result = bm->CreateNode(k, vec); break; } case FOR: { //Insert in a global list of FOR constructs. Return TRUE now - bm.GlobalList_Of_FiniteLoops.push_back(simpleForm); - return bm.CreateNode(TRUE); + bm->GlobalList_Of_FiniteLoops.push_back(simpleForm); + return bm->CreateNode(TRUE); break; } case PARAMBOOL: @@ -299,7 +299,7 @@ namespace BEEV //VAR(expression), then simply return it if(BVCONST == simpleForm[1].GetKind()) { - result = bm.NewBooleanVar(simpleForm[0],simpleForm[1]); + result = bm->NewBooleanVar(simpleForm[0],simpleForm[1]); } else { @@ -313,7 +313,7 @@ namespace BEEV result = simpleForm; else { - FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k); + FatalError("TransformFormula: Illegal kind: ", bm->CreateNode(UNDEFINED), k); cerr << "The input is: " << simpleForm << endl; cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl; } @@ -331,7 +331,7 @@ namespace BEEV { assert(TransformMap != NULL); - BeevMgr& bm = inputterm.GetBeevMgr(); + BeevMgr* bm = inputterm.GetBeevMgr(); ASTNode result; ASTNode term = inputterm; @@ -360,7 +360,7 @@ namespace BEEV FatalError("TransformTerm: this kind is not supported", term); break; case READ: - result = bm.TransformArray(term); + result = bm->TransformArray(term); break; case ITE: { @@ -371,7 +371,7 @@ namespace BEEV thn = TransformTerm(thn); els = TransformTerm(els); //result = CreateTerm(ITE,term.GetValueWidth(),cond,thn,els); - result = bm.CreateSimplifiedTermITE(cond, thn, els); + result = bm->CreateSimplifiedTermITE(cond, thn, els); result.SetIndexWidth(term.GetIndexWidth()); break; } @@ -388,7 +388,7 @@ namespace BEEV o.push_back(TransformTerm(*it)); } - result = bm.CreateTerm(k, width, o); + result = bm->CreateTerm(k, width, o); result.SetIndexWidth(indexwidth); Kind k = result.GetKind(); @@ -408,9 +408,9 @@ namespace BEEV // result is embedded unchanged inside the result. unsigned inputValueWidth = result.GetValueWidth(); - ASTNode zero = bm.CreateZeroConst(inputValueWidth); - ASTNode one = bm.CreateOneConst(inputValueWidth); - result = bm.CreateTerm(ITE, inputValueWidth, bm.CreateNode(EQ, zero, bottom), one, result); + ASTNode zero = bm->CreateZeroConst(inputValueWidth); + ASTNode one = bm->CreateOneConst(inputValueWidth); + result = bm->CreateTerm(ITE, inputValueWidth, bm->CreateNode(EQ, zero, bottom), one, result); } } } diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp index a46d95a..1af9eba 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/AST/printer/AssortedPrinters.cpp @@ -66,7 +66,7 @@ namespace BEEV void lpvec(const ASTVec &vec) { - vec[0].GetBeevMgr().AlreadyPrintedSet.clear(); + (vec[0].GetBeevMgr())->AlreadyPrintedSet.clear(); LispPrintVec(cout, vec, 0); cout << endl; } diff --git a/src/AST/printer/CPrinter.cpp b/src/AST/printer/CPrinter.cpp index dfef1d8..18269a0 100644 --- a/src/AST/printer/CPrinter.cpp +++ b/src/AST/printer/CPrinter.cpp @@ -38,21 +38,21 @@ namespace printer } //if this node is present in the letvar Map, then print the letvar - BeevMgr &bm = n.GetBeevMgr(); + 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) + if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize) { - C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, 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) + if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize) { - C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + C_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize); return; } @@ -434,11 +434,11 @@ namespace printer 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(); + BeevMgr* bm = n.GetBeevMgr(); + bm->PLPrintNodeSet.clear(); + bm->NodeLetVarMap.clear(); + bm->NodeLetVarVec.clear(); + bm->NodeLetVarMap1.clear(); //pass 1: letize the node n.LetizeNode(); @@ -453,12 +453,12 @@ namespace printer //3. Then print the Node itself, replacing every occurence of //3. expr1 with var1, expr2 with var2, ... //os << "("; - if (0 < bm.NodeLetVarMap.size()) + 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(); + //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; @@ -501,7 +501,7 @@ namespace printer } //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; + bm->NodeLetVarMap1[it->second] = it->first; } os << endl << "stp_assert "; diff --git a/src/AST/printer/LispPrinter.cpp b/src/AST/printer/LispPrinter.cpp index ca49afe..8caf9f0 100644 --- a/src/AST/printer/LispPrinter.cpp +++ b/src/AST/printer/LispPrinter.cpp @@ -91,8 +91,8 @@ namespace printer ostream &Lisp_Print(ostream &os, const ASTNode& n, int indentation) { // Clear the PrintMap - BeevMgr& bm = n.GetBeevMgr(); - bm.AlreadyPrintedSet.clear(); + BeevMgr* bm = n.GetBeevMgr(); + bm->AlreadyPrintedSet.clear(); Lisp_Print_indent(os, n, indentation); printf("\n"); return os; diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp index 1d5e7c7..2c5f18f 100644 --- a/src/AST/printer/PLPrinter.cpp +++ b/src/AST/printer/PLPrinter.cpp @@ -26,21 +26,21 @@ namespace printer } //if this node is present in the letvar Map, then print the letvar - BeevMgr &bm = n.GetBeevMgr(); + 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) + if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize) { - PL_Print1(os, (bm.NodeLetVarMap1[n]), indentation, 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) + if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize) { - PL_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + PL_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize); return; } @@ -182,7 +182,7 @@ namespace printer case FOR: if(expand_finitefor_flag) { - ASTNode expandedfor = bm.Expand_FiniteLoop_TopLevel(n); + ASTNode expandedfor = bm->Expand_FiniteLoop_TopLevel(n); PL_Print1(os, expandedfor, indentation, letize); } else @@ -327,11 +327,11 @@ namespace printer 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(); + BeevMgr* bm = n.GetBeevMgr(); + bm->PLPrintNodeSet.clear(); + bm->NodeLetVarMap.clear(); + bm->NodeLetVarVec.clear(); + bm->NodeLetVarMap1.clear(); //pass 1: letize the node n.LetizeNode(); @@ -344,12 +344,12 @@ namespace printer //3. Then print the Node itself, replacing every occurence of //3. expr1 with var1, expr2 with var2, ... //os << "("; - if (0 < bm.NodeLetVarMap.size()) + 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(); + //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 @@ -359,7 +359,7 @@ namespace printer PL_Print1(os, it->second, indentation, false); //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; + bm->NodeLetVarMap1[it->second] = it->first; for (it++; it != itend; it++) { @@ -371,7 +371,7 @@ namespace printer PL_Print1(os, it->second, indentation, false); //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; + bm->NodeLetVarMap1[it->second] = it->first; } os << " IN " << endl; diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp index 5b1fe1f..1313761 100644 --- a/src/AST/printer/SMTLIBPrinter.cpp +++ b/src/AST/printer/SMTLIBPrinter.cpp @@ -23,7 +23,7 @@ namespace printer string functionToSMTLIBName(const BEEV::Kind k); void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); - void printVarDeclsToStream( const BeevMgr& mgr, ostream &os); + void printVarDeclsToStream( const BeevMgr* mgr, ostream &os); // Initial version intended to print the whole thing back. void SMTLIB_PrintBack(ostream &os, const ASTNode& n) { @@ -35,8 +35,8 @@ namespace printer os << ")" << endl; } - void printVarDeclsToStream( const BeevMgr& mgr, ostream &os) { - for(ASTVec::const_iterator i = mgr.ListOfDeclaredVars.begin(),iend=mgr.ListOfDeclaredVars.end();i!=iend;i++) { + void printVarDeclsToStream( const BeevMgr* mgr, ostream &os) { + for(ASTVec::const_iterator i = mgr->ListOfDeclaredVars.begin(),iend=mgr->ListOfDeclaredVars.end();i!=iend;i++) { const BEEV::ASTNode& a = *i; // Should be a symbol. @@ -90,7 +90,7 @@ namespace printer // Prepend with zero to convert to unsigned. os << "bv"; - CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst()); + 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() << "]"; @@ -108,21 +108,21 @@ namespace printer } //if this node is present in the letvar Map, then print the letvar - BeevMgr &bm = n.GetBeevMgr(); + 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) + if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize) { - SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, 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) + if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize) { - SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + SMTLIB_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize); return; } @@ -190,11 +190,11 @@ namespace 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(); + BeevMgr* bm = n.GetBeevMgr(); + bm->PLPrintNodeSet.clear(); + bm->NodeLetVarMap.clear(); + bm->NodeLetVarVec.clear(); + bm->NodeLetVarMap1.clear(); //pass 1: letize the node n.LetizeNode(); @@ -207,12 +207,12 @@ namespace printer //3. Then print the Node itself, replacing every occurence of //3. expr1 with var1, expr2 with var2, ... //os << "("; - if (0 < bm.NodeLetVarMap.size()) + 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(); + //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 @@ -222,7 +222,7 @@ namespace printer SMTLIB_Print1(os, it->second, indentation, false); //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; + bm->NodeLetVarMap1[it->second] = it->first; for (it++; it != itend; it++) { @@ -234,7 +234,7 @@ namespace printer SMTLIB_Print1(os, it->second, indentation, false); //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; + bm->NodeLetVarMap1[it->second] = it->first; } os << " IN " << endl; diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index b4a3426..2473988 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -127,6 +127,7 @@ VC vc_createValidityChecker(void) { return 0; } bmstar bm = new BEEV::BeevMgr(); + BEEV::GlobalBeevMgr = bm; decls = new BEEV::ASTVec(); //created_exprs.clear(); return (VC)bm; @@ -156,9 +157,10 @@ char * vc_printSMTLIB(VC vc, Expr e) // prints Expr 'e' to stdout as C code void vc_printExprCCode(VC vc, Expr e) { BEEV::ASTNode q = (*(nodestar)e); + bmstar b = (bmstar)vc; // print variable declarations - BEEV::ASTVec declsFromParser = (nodelist)BEEV::GlobalBeevMgr->ListOfDeclaredVars; + BEEV::ASTVec declsFromParser = (nodelist)b->ListOfDeclaredVars; for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) { if(BEEV::BITVECTOR_TYPE == it->GetType()) { @@ -1574,40 +1576,6 @@ static char *val_to_binary_str(unsigned nbits, unsigned long long val) { } #endif -// Expr vc_parseExpr(VC vc, char* infile) { -// bmstar b = (bmstar)vc; -// extern FILE* cvcin; -// const char * prog = "stp"; - -// cvcin = fopen(infile,"r"); -// if(cvcin == NULL) { -// fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); -// BEEV::FatalError(""); -// } - -// BEEV::GlobalBeevMgr = b; - -// CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); -// if(0 != c) { -// cout << CONSTANTBV::BitVector_Error(c) << endl; -// return 0; -// } - -// cvcparse(); -// nodelist aaa = b->GetAsserts(); - -// //Don't add the query. It gets added automatically if the input file -// //has QUERY in it -// // -// //node bbb = b->CreateNode(BEEV::NOT,b->GetQuery()); -// node o = b->CreateNode(BEEV::AND,aaa); -// //node o = b->CreateNode(BEEV::AND,oo,bbb); - -// nodestar output = new node(o); -// return output; -// } //end of vc_parseExpr() - - Expr vc_parseExpr(VC vc, const char* infile) { bmstar b = (bmstar)vc; extern FILE* cvcin; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 0f1eb00..fe7dd98 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -21,7 +21,7 @@ ASTNode Flatten(const ASTNode& a) while (true) { ASTNode& nold = n; - n = a.GetBeevMgr().FlattenOneLevel(n); + n = a.GetBeevMgr()->FlattenOneLevel(n); if ((n == nold)) break; } diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index 318eaed..60cd775 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -432,30 +432,13 @@ namespace BEEV // ASSERT: IndexWidth = 0? Semantic analysis should check. //Leaking ASTVec& bbvec = *(new ASTVec); - //FIXME Why is isn't this ASTVEC bbvec(num_bits) ? ASTVec bbvec; - /* - if(term.GetNodeNum() == 17132){ - weregood = true; - } - */ - - /* - if(weregood){ - printf("number of bits for node 17132: %d\n", num_bits); - } - */ for (unsigned int i = 0; i < num_bits; i++) { ASTNode bit_node = CreateNode(BVGETBIT, term, CreateBVConst(32, i)); bbvec.push_back(bit_node); } result = CreateNode(BOOLVEC, bbvec); - /* - if(weregood){ - printf("done\n"); - } - */ break; } case BVCONST: diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 3557c7a..dda2fc5 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -50,7 +50,7 @@ namespace BEEV BeevMgr::ClauseList* convertToCNF(const ASTNode& varphi) { - varphi.GetBeevMgr().runTimes.start(RunTimes::CNFConversion); + varphi.GetBeevMgr()->runTimes.start(RunTimes::CNFConversion); scanFormula(varphi, true); ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); BeevMgr::ClauseList* defs = SINGLETON(dummy_true_var); @@ -59,7 +59,7 @@ namespace BEEV defs->insert(defs->begin() + 1, top->begin(), top->end()); cleanup(varphi); - varphi.GetBeevMgr().runTimes.stop(RunTimes::CNFConversion); + varphi.GetBeevMgr()->runTimes.stop(RunTimes::CNFConversion); return defs; } -- 2.47.3