From: vijay_ganesh Date: Wed, 14 Oct 2009 17:05:17 +0000 (+0000) Subject: code indented using emacs X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c126604703f0aeb26d014e9df44cb9291060a3bd;p=francis%2Fstp.git code indented using emacs git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@302 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/emacs-format.sh b/scripts/emacs-format.sh index 7a5a6fa..ea7c016 100755 --- a/scripts/emacs-format.sh +++ b/scripts/emacs-format.sh @@ -1,36 +1,37 @@ -#!/bin/sh -# File: my-indent -# Opens a set of files in emacs and executes the emacs-format-function. -# Assumes the function named emacs-format-function is defined in the -# file named emacs-format-file. + #!/bin/sh -loadpath=`pwd` -if [ $# == 0 ] -then - echo "my-indent requires at least one argument." 1>&2 - echo "Usage: my-indent files-to-indent" 1>&2 - exit 1 -fi + # File: my-indent Opens a set of files in emacs and executes the + # emacs-format-function. Assumes the function named + # emacs-format-function is defined in the file named + # emacs-format-file. -while [ $# -ge 1 ] -do - if [ -d $1 ] + loadpath=`pwd` + if [ $# == 0 ] then - echo "Argument of my-indent $1 cannot be a directory." 1>&2 - exit 1 + echo "my-indent requires at least one argument." 1>&2 + echo "Usage: my-indent files-to-indent" 1>&2 + exit 1 fi - # Check for existence of file: - ls $1 2> /dev/null | grep $1 > /dev/null - if [ $? != 0 ] - then - echo "my-indent: $1 not found." 1>&2 - exit 1 - fi - echo "Indenting $1 with emacs in batch mode" - emacs -batch $1 -l $loadpath/scripts/emacs-format-file -f emacs-format-function - echo - shift 1 -done -exit 0 + while [ $# -ge 1 ] + do + if [ -d $1 ] + then + echo "Argument of my-indent $1 cannot be a directory." 1>&2 + exit 1 + fi + + # Check for existence of file: + ls $1 2> /dev/null | grep $1 > /dev/null + if [ $? != 0 ] + then + echo "my-indent: $1 not found." 1>&2 + exit 1 + fi + echo "Indenting $1 with emacs in batch mode" + emacs -batch $1 -l $loadpath/scripts/emacs-format-file -f emacs-format-function + echo + shift 1 + done + exit 0 diff --git a/src/AST/ASTBVConst.cpp b/src/AST/ASTBVConst.cpp index 31296f0..903928b 100644 --- a/src/AST/ASTBVConst.cpp +++ b/src/AST/ASTBVConst.cpp @@ -50,42 +50,42 @@ namespace BEEV if(print_binary_flag) { res = CONSTANTBV::BitVector_to_Bin(_bvconst); if (c_friendly) - { - prefix = "0b"; - } + { + prefix = "0b"; + } else - { - prefix = "0bin"; - } + { + prefix = "0bin"; + } } else if (_value_width % 4 == 0) { - res = CONSTANTBV::BitVector_to_Hex(_bvconst); - if (c_friendly) - { - prefix = "0x"; - } - else - { - prefix = "0hex"; - } + res = CONSTANTBV::BitVector_to_Hex(_bvconst); + if (c_friendly) + { + prefix = "0x"; + } + else + { + prefix = "0hex"; + } } else { - res = CONSTANTBV::BitVector_to_Bin(_bvconst); - if (c_friendly) - { - prefix = "0b"; - } - else - { - prefix = "0bin"; - } + res = CONSTANTBV::BitVector_to_Bin(_bvconst); + if (c_friendly) + { + prefix = "0b"; + } + else + { + prefix = "0bin"; + } } if (NULL == res) { - os << "nodeprint: BVCONST : could not convert to string" << _bvconst; - FatalError(""); + os << "nodeprint: BVCONST : could not convert to string" << _bvconst; + FatalError(""); } os << prefix << res; CONSTANTBV::BitVector_Dispose(res); @@ -108,15 +108,15 @@ namespace BEEV bool ASTBVConst::ASTBVConstEqual::operator()(const ASTBVConst * bvc1, - const ASTBVConst * bvc2) const + const ASTBVConst * bvc2) const { if (bvc1->_value_width != bvc2->_value_width) { - return false; + return false; } return (0 == - CONSTANTBV::BitVector_Compare(bvc1->_bvconst, - bvc2->_bvconst)); + CONSTANTBV::BitVector_Compare(bvc1->_bvconst, + bvc2->_bvconst)); } //End of ASTBVConstEqual operator };//End of namespace diff --git a/src/AST/ASTBVConst.h b/src/AST/ASTBVConst.h index 093c1ce..3f29dd7 100644 --- a/src/AST/ASTBVConst.h +++ b/src/AST/ASTBVConst.h @@ -55,7 +55,7 @@ namespace BEEV { public: bool operator()(const ASTBVConst * bvc1, - const ASTBVConst * bvc2) const; + const ASTBVConst * bvc2) const; }; //End of class ASTBVConstEqual /**************************************************************** @@ -73,7 +73,7 @@ namespace BEEV if (bvc1._value_width != bvc2._value_width) return false; return (0 == CONSTANTBV::BitVector_Compare(bvc1._bvconst, - bvc2._bvconst)); + bvc2._bvconst)); } //End of operator== // Call this when deleting a node that has been stored in the the diff --git a/src/AST/ASTInterior.cpp b/src/AST/ASTInterior.cpp index 0302786..cc8c2a5 100644 --- a/src/AST/ASTInterior.cpp +++ b/src/AST/ASTInterior.cpp @@ -45,22 +45,22 @@ namespace BEEV ASTVec::const_iterator iend = ch.end(); for (ASTVec::const_iterator i = ch.begin(); i != iend; i++) { - hashval += i->Hash(); - hashval += (hashval << 10); - hashval ^= (hashval >> 6); + hashval += i->Hash(); + hashval += (hashval << 10); + hashval ^= (hashval >> 6); } hashval += (hashval << 3); hashval ^= (hashval >> 11); hashval += (hashval << 15); - return hashval; + return hashval; } //End of ASTInteriorHasher operator() //ASTInteriorEqual operator() bool ASTInterior::ASTInteriorEqual:: operator()(const ASTInterior *int_node_ptr1, - const ASTInterior *int_node_ptr2) const + const ASTInterior *int_node_ptr2) const { return (*int_node_ptr1 == *int_node_ptr2); } ///End of ASTInteriorEqual operator() diff --git a/src/AST/ASTInterior.h b/src/AST/ASTInterior.h index 4db901a..b003959 100644 --- a/src/AST/ASTInterior.h +++ b/src/AST/ASTInterior.h @@ -55,15 +55,15 @@ namespace BEEV { public: bool operator()(const ASTInterior *int_node_ptr1, - const ASTInterior *int_node_ptr2) const; + const ASTInterior *int_node_ptr2) const; }; //End of class ASTInteriorEqual // Used in Equality class for hash tables friend bool operator==(const ASTInterior &int_node1, - const ASTInterior &int_node2) + const ASTInterior &int_node2) { return ((int_node1._kind == int_node2._kind) - && (int_node1._children == int_node2._children)); + && (int_node1._children == int_node2._children)); } //End of operator== // Call this when deleting a node that has been stored in the diff --git a/src/AST/ASTInternal.h b/src/AST/ASTInternal.h index 4cc565c..1843c1e 100644 --- a/src/AST/ASTInternal.h +++ b/src/AST/ASTInternal.h @@ -186,10 +186,10 @@ namespace BEEV void DecRef() { if (--_ref_count == 0) - { - // Delete node from unique table and kill it. - CleanUp(); - } + { + // Delete node from unique table and kill it. + CleanUp(); + } }//End of DecRef() int GetNodeNum() const diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp index a87ca49..fe1dc41 100644 --- a/src/AST/ASTNode.cpp +++ b/src/AST/ASTNode.cpp @@ -18,12 +18,12 @@ namespace BEEV // Constructor; // // creates a new pointer, increments refcount of pointed-to object. - ASTNode::ASTNode(ASTInternal *in) : + ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { if (in) { - in->IncRef(); + in->IncRef(); } } //End of Constructor @@ -38,40 +38,40 @@ namespace BEEV } //End of Copy Constructor for ASTNode // ASTNode accessor function. - Kind ASTNode::GetKind() const + Kind ASTNode::GetKind() const { //cout << "GetKind: " << _int_node_ptr; return _int_node_ptr->GetKind(); } //End of GetKind() // Declared here because of same ordering problem as GetKind. - const ASTVec &ASTNode::GetChildren() const + const ASTVec &ASTNode::GetChildren() const { return _int_node_ptr->GetChildren(); } //End of GetChildren() // Access node number - int ASTNode::GetNodeNum() const + int ASTNode::GetNodeNum() const { return _int_node_ptr->_node_num; } //End of GetNodeNum() - unsigned int ASTNode::GetIndexWidth() const + unsigned int ASTNode::GetIndexWidth() const { return _int_node_ptr->_index_width; } //End of GetIndexWidth() - void ASTNode::SetIndexWidth(unsigned int iw) const + void ASTNode::SetIndexWidth(unsigned int iw) const { _int_node_ptr->_index_width = iw; } //End of SetIndexWidth() - unsigned int ASTNode::GetValueWidth() const + unsigned int ASTNode::GetValueWidth() const { return _int_node_ptr->_value_width; } //End of GetValueWidth() - void ASTNode::SetValueWidth(unsigned int vw) const + void ASTNode::SetValueWidth(unsigned int vw) const { _int_node_ptr->_value_width = vw; } //End of SetValueWidth() @@ -79,7 +79,7 @@ namespace BEEV //return the type of the ASTNode: // // 0 iff BOOLEAN; 1 iff BITVECTOR; 2 iff ARRAY; 3 iff UNKNOWN; - types ASTNode::GetType() const + types ASTNode::GetType() const { if ((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN return BOOLEAN_TYPE; @@ -91,7 +91,7 @@ namespace BEEV } //End of GetType() // Assignment - ASTNode& ASTNode::operator=(const ASTNode& n) + ASTNode& ASTNode::operator=(const ASTNode& n) { if (n._int_node_ptr) { @@ -114,7 +114,7 @@ namespace BEEV } } //End of Destructor() - STPMgr* ASTNode::GetSTPMgr() const + STPMgr* ASTNode::GetSTPMgr() const { return GlobalSTP->bm; } //End of GetSTPMgr() @@ -124,7 +124,7 @@ namespace BEEV { STPMgr * bm = GetSTPMgr(); return (bm->AlreadyPrintedSet.find(*this) != - bm->AlreadyPrintedSet.end()); + bm->AlreadyPrintedSet.end()); } //End of IsAlreadyPrinted() // Mark the node as printed if it has been already printed diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h index 87509a3..c0ecbc6 100644 --- a/src/AST/ASTNode.h +++ b/src/AST/ASTNode.h @@ -47,8 +47,8 @@ namespace BEEV friend bool operator==(const ASTNode node1, const ASTNode node2) { return - ((size_t) node1._int_node_ptr) == - ((size_t) node2._int_node_ptr); + ((size_t) node1._int_node_ptr) == + ((size_t) node2._int_node_ptr); } friend bool operator!=(const ASTNode node1, const ASTNode node2) @@ -59,8 +59,8 @@ namespace BEEV friend bool operator<(const ASTNode node1, const ASTNode node2) { return - ((size_t) node1._int_node_ptr) < - ((size_t) node2._int_node_ptr); + ((size_t) node1._int_node_ptr) < + ((size_t) node2._int_node_ptr); } public: diff --git a/src/AST/ASTSymbol.h b/src/AST/ASTSymbol.h index e166799..e779c61 100644 --- a/src/AST/ASTSymbol.h +++ b/src/AST/ASTSymbol.h @@ -47,11 +47,11 @@ namespace BEEV #ifdef TR1_UNORDERED_MAP tr1::hash h; #else - //hash h; + //hash h; #endif - //return h(sym_ptr->_name); - //cerr << "ASTSymbol hasher recieved name: " - //<< sym_ptr->_name << endl; + //return h(sym_ptr->_name); + //cerr << "ASTSymbol hasher recieved name: " + //<< sym_ptr->_name << endl; return (size_t)hash((unsigned char*)(sym_ptr->_name)); }; }; // End of class ASTSymbolHasher @@ -65,7 +65,7 @@ namespace BEEV { public: bool operator()(const ASTSymbol *sym_ptr1, - const ASTSymbol *sym_ptr2) const + const ASTSymbol *sym_ptr2) const { return (*sym_ptr1 == *sym_ptr2); } @@ -73,7 +73,7 @@ namespace BEEV // comparator friend bool operator==(const ASTSymbol &sym1, - const ASTSymbol &sym2) + const ASTSymbol &sym2) { return (strcmp(sym1._name, sym2._name) == 0); } diff --git a/src/AST/ASTUtil.cpp b/src/AST/ASTUtil.cpp index 0989802..a3be1d0 100644 --- a/src/AST/ASTUtil.cpp +++ b/src/AST/ASTUtil.cpp @@ -41,12 +41,12 @@ namespace BEEV { cout << endl; for (function_counters::iterator - it = s.begin(), itend = s.end(); - it != itend; it++) + it = s.begin(), itend = s.end(); + it != itend; it++) cout << "Number of times the function: " - << it->first - << ": is called: " - << it->second << endl; + << it->first + << ": is called: " + << it->second << endl; return; } s[functionname] += 1; diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp index d8e1343..cc41bfd 100644 --- a/src/AST/ASTmisc.cpp +++ b/src/AST/ASTmisc.cpp @@ -218,8 +218,8 @@ namespace BEEV FatalError("BVTypeCheck: indices should be BVCONST\n", n); if (n.GetValueWidth() != GetUnsignedConst(n[1]) - GetUnsignedConst(n[2]) + 1) FatalError("BVTypeCheck: length mismatch\n", n); - if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth()) - FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n); + if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth()) + FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n); break; case BVLEFTSHIFT: case BVRIGHTSHIFT: @@ -243,10 +243,10 @@ namespace BEEV case FALSE: case SYMBOL: return true; - case PARAMBOOL: - if(2 != n.Degree()) - FatalError("BVTypeCheck: PARAMBOOL formula can have exactly two childNodes", n); - break; + case PARAMBOOL: + if(2 != n.Degree()) + FatalError("BVTypeCheck: PARAMBOOL formula can have exactly two childNodes", n); + break; case EQ: if (!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth())) { @@ -297,7 +297,7 @@ namespace BEEV //FIXME: Todo break; default: - + FatalError("BVTypeCheck: Unrecognized kind: "); break; } @@ -342,9 +342,9 @@ namespace BEEV //a is of the form READ(Arr,const), and b is const, or //a is of the form var, and b is const if ((k1 == READ - && a[0].GetKind() == SYMBOL - && a[1].GetKind() == BVCONST - && (k2 == BVCONST))) + && a[0].GetKind() == SYMBOL + && a[1].GetKind() == BVCONST + && (k2 == BVCONST))) // || k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() // == BVCONST))) return 1; @@ -355,15 +355,15 @@ namespace BEEV //b is of the form READ(Arr,const), and a is const, or //b is of the form var, and a is const if ((k1 == BVCONST) - && ((k2 == READ - && b[0].GetKind() == SYMBOL - && b[1].GetKind() == BVCONST))) + && ((k2 == READ + && b[0].GetKind() == SYMBOL + && b[1].GetKind() == BVCONST))) return -1; if (SYMBOL == k2 - && (BVCONST == k1 - || TRUE == k1 - || FALSE == k1)) + && (BVCONST == k1 + || TRUE == k1 + || FALSE == k1)) return -1; return 0; diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 6616d37..2c14837 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -17,8 +17,8 @@ namespace BEEV { - // NB: This is the only function that should be called externally. It sets - // up the cache that the others use. + // NB: This is the only function that should be called + // externally. It sets up the cache that the others use. ASTNode ArrayTransformer::TransformFormula_TopLevel(const ASTNode& form) { runTimes->start(RunTimes::Transforming); @@ -54,7 +54,8 @@ namespace BEEV 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)); + bm->CreateNode(EQ, one, + bm->CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1)); if (SBVREM == in.GetKind()) { @@ -63,15 +64,27 @@ namespace BEEV //Take absolute value. ASTNode pos_dividend = - bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), 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); + 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 simp->SimplifyTerm_TopLevel(n); @@ -93,17 +106,36 @@ 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 simp->SimplifyTerm_TopLevel(n); } @@ -125,19 +157,34 @@ 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 simp->SimplifyTerm_TopLevel(n); } - FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in); + FatalError("TranslateSignedDivModRem:"\ + "input must be signed DIV/MOD/REM", in); return bm->CreateNode(UNDEFINED); }//end of TranslateSignedDivModRem() @@ -187,7 +234,8 @@ namespace BEEV if (!(is_Form_kind(k) && BOOLEAN_TYPE == simpleForm.GetType())) { //FIXME: "You have inputted a NON-formula"? - FatalError("TransformFormula: You have input a NON-formula", simpleForm); + FatalError("TransformFormula:"\ + "You have input a NON-formula", simpleForm); } ASTNodeMap::iterator iter; @@ -242,7 +290,9 @@ namespace BEEV { ASTVec vec; ASTNode o; - for (ASTVec::const_iterator it = simpleForm.begin(), itend = simpleForm.end(); it != itend; it++) + for (ASTVec::const_iterator + it = simpleForm.begin(), + itend = simpleForm.end(); it != itend; it++) { o = TransformFormula(*it); vec.push_back(o); @@ -252,42 +302,45 @@ namespace BEEV break; } case FOR: - { - //Insert in a global list of FOR constructs. Return TRUE now - //GlobalList_Of_FiniteLoops.push_back(simpleForm); - return bm->CreateNode(TRUE); - break; - } + { + //Insert in a global list of FOR constructs. Return TRUE now + //GlobalList_Of_FiniteLoops.push_back(simpleForm); + return bm->CreateNode(TRUE); + break; + } case PARAMBOOL: - { - //If the parameteric boolean variable is of the form - //VAR(const), then convert it into a Boolean variable of the - //form "VAR(const)". - // - //Else if the paramteric boolean variable is of the form - //VAR(expression), then simply return it - if(BVCONST == simpleForm[1].GetKind()) - { - result = bm->NewParameterized_BooleanVar(simpleForm[0],simpleForm[1]); - } - else - { - result = simpleForm; - } - break; - } + { + //If the parameteric boolean variable is of the form + //VAR(const), then convert it into a Boolean variable of the + //form "VAR(const)". + // + //Else if the paramteric boolean variable is of the form + //VAR(expression), then simply return it + if(BVCONST == simpleForm[1].GetKind()) + { + result = + bm->NewParameterized_BooleanVar(simpleForm[0],simpleForm[1]); + } + else + { + result = simpleForm; + } + break; + } default: - { - if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType()) - result = simpleForm; - else - { - FatalError("TransformFormula: Illegal kind: ", bm->CreateNode(UNDEFINED), k); - cerr << "The input is: " << simpleForm << endl; - cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl; - } - break; - } + { + if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType()) + result = simpleForm; + else + { + FatalError("TransformFormula: Illegal kind: ", + bm->CreateNode(UNDEFINED), k); + cerr << "The input is: " << simpleForm << endl; + cerr << "The valuewidth of input is : " + << simpleForm.GetValueWidth() << endl; + } + break; + } } //end of Switch if (simpleForm.GetChildren().size() > 0) @@ -304,7 +357,8 @@ namespace BEEV ASTNode term = inputterm; Kind k = term.GetKind(); if (!is_Term_kind(k)) - FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k); + FatalError("TransformTerm: Illegal kind: You have input a nonterm:", + inputterm, k); ASTNodeMap::iterator iter; if ((iter = TransformMap->find(term)) != TransformMap->end()) return iter->second; @@ -312,9 +366,9 @@ namespace BEEV { case SYMBOL: { - // ASTNodeMap::iterator itsym; - // if((itsym = CounterExampleMap.find(term)) != CounterExampleMap.end()) - // result = itsym->second; + // ASTNodeMap::iterator itsym; if((itsym = + // CounterExampleMap.find(term)) != + // CounterExampleMap.end()) result = itsym->second; // else result = term; break; @@ -358,41 +412,50 @@ namespace BEEV Kind k = result.GetKind(); - if (BVDIV == k || BVMOD == k || SBVDIV == k || SBVREM == k || SBVMOD == k) + if (BVDIV == k + || BVMOD == k + || SBVDIV == k + || SBVREM == k + || SBVMOD == k) { ASTNode bottom = result[1]; - if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind()) + if (SBVDIV == result.GetKind() + || SBVREM == result.GetKind() + || SBVMOD == result.GetKind()) { result = TranslateSignedDivModRem(result); } if (division_by_zero_returns_one) { - // This is a difficult rule to introduce in other places because it's recursive. i.e. - // result is embedded unchanged inside the result. + // This is a difficult rule to introduce in other + // places because it's recursive. i.e. 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); + result = + bm->CreateTerm(ITE, inputValueWidth, + bm->CreateNode(EQ, zero, bottom), + one, result); } } } - //////////////////////////////////////////////////////////////////////////////////// - - break; } if (term.GetChildren().size() > 0) (*TransformMap)[term] = result; if (term.GetValueWidth() != result.GetValueWidth()) - FatalError("TransformTerm: result and input terms are of different length", result); + FatalError("TransformTerm: "\ + "result and input terms are of different length", result); if (term.GetIndexWidth() != result.GetIndexWidth()) { cerr << "TransformTerm: input term is : " << term << endl; - FatalError("TransformTerm: result and input terms have different index length", result); + FatalError("TransformTerm: "\ + "result & input terms have different index length", result); } return result; } //End of TransformTerm @@ -417,7 +480,8 @@ namespace BEEV const unsigned int width = term.GetValueWidth(); if (READ != term.GetKind()) - FatalError("TransformArray: input term is of wrong kind: ", ASTUndefined); + FatalError("TransformArray: input term is of wrong kind: ", + ASTUndefined); ASTNodeMap::iterator iter; if ((iter = TransformMap->find(term)) != TransformMap->end()) @@ -441,12 +505,14 @@ namespace BEEV */ // Recursively transform read index, which may also contain reads. - ASTNode processedTerm = bm->CreateTerm(READ, width, arrName, readIndex); + ASTNode processedTerm = + bm->CreateTerm(READ, width, arrName, readIndex); //check if the 'processedTerm' has a corresponding ITE construct //already. if so, return it. else continue processing. ASTNodeMap::iterator it; - if ((it = Arrayread_IteMap->find(processedTerm)) != Arrayread_IteMap->end()) + if ((it = Arrayread_IteMap->find(processedTerm)) + != Arrayread_IteMap->end()) { result = it->second; break; @@ -454,23 +520,25 @@ namespace BEEV //Constructing Symbolic variable corresponding to 'processedTerm' ASTNode CurrentSymbol; ASTNodeMap::iterator it1; - // First, check if read index is constant and it has a constant value in the substitution map. + // First, check if read index is constant and it has a + // constant value in the substitution map. if (simp->CheckSubstitutionMap(processedTerm, CurrentSymbol)) { Arrayread_SymbolMap[processedTerm] = CurrentSymbol; } // Check if it already has an abstract variable. - else if ((it1 = Arrayread_SymbolMap.find(processedTerm)) != Arrayread_SymbolMap.end()) + else if ((it1 = Arrayread_SymbolMap.find(processedTerm)) + != Arrayread_SymbolMap.end()) { CurrentSymbol = it1->second; } else { - // Make up a new abstract variable. - // FIXME: Make this into a method (there already may BE a method) and - // get rid of the fixed-length buffer! - //build symbolic name corresponding to array read. The symbolic - //name has 2 components: stringname, and a count + // Make up a new abstract variable. FIXME: Make this + // into a method (there already may BE a method) and get + // rid of the fixed-length buffer! build symbolic name + // corresponding to array read. The symbolic name has 2 + // components: stringname, and a count const char * b = arrName.GetName(); std::string c(b); char d[32]; @@ -507,18 +575,24 @@ namespace BEEV ASTVec::const_reverse_iterator it2end = readIndices.rend(); for (; it2 != it2end; it2++) { - ASTNode cond = simp->CreateSimplifiedEQ(readIndex, *it2); + ASTNode cond = + simp->CreateSimplifiedEQ(readIndex, *it2); if (ASTFalse == cond) continue; - ASTNode arrRead = bm->CreateTerm(READ, width, arrName, *it2); + ASTNode arrRead = + bm->CreateTerm(READ, width, arrName, *it2); assert(BVTypeCheck(arrRead)); ASTNode arrayreadSymbol = Arrayread_SymbolMap[arrRead]; if (arrayreadSymbol.IsNull()) - FatalError("TransformArray:symbolic variable for processedTerm, p," - "does not exist:p = ", arrRead); - ite = simp->CreateSimplifiedTermITE(cond, arrayreadSymbol, ite); + { + FatalError("TransformArray:"\ + "symbolic variable for processedTerm, p,"\ + "does not exist:p = ", arrRead); + } + ite = + simp->CreateSimplifiedTermITE(cond, arrayreadSymbol, ite); } result = ite; //} @@ -553,42 +627,54 @@ namespace BEEV ASTNode writeVal = TransformTerm(arrName[2]); if (ARRAY_TYPE != arrName[0].GetType()) - FatalError("TransformArray: An array write is being attempted on a non-array:", term); + FatalError("TransformArray: "\ + "An array write is being attempted on a non-array:", + term); - if ((SYMBOL == arrName[0].GetKind() || WRITE == arrName[0].GetKind())) + if ((SYMBOL == arrName[0].GetKind() + || WRITE == arrName[0].GetKind())) { - ASTNode cond = simp->CreateSimplifiedEQ(writeIndex, readIndex); + ASTNode cond = + simp->CreateSimplifiedEQ(writeIndex, readIndex); BVTypeCheck(cond); - ASTNode readTerm = bm->CreateTerm(READ, width, arrName[0], readIndex); + ASTNode readTerm = + bm->CreateTerm(READ, width, arrName[0], readIndex); BVTypeCheck(readTerm); ASTNode readPushedIn = TransformArray(readTerm); BVTypeCheck(readPushedIn); - result = simp->CreateSimplifiedTermITE(cond, writeVal, readPushedIn); - + result = + simp->CreateSimplifiedTermITE(cond, writeVal, readPushedIn); BVTypeCheck(result); } else if (ITE == arrName[0].GetKind()) { - // pull out the ite from the write // pushes the write through. - ASTNode writeTrue = bm->CreateNode(WRITE, (arrName[0][1]), writeIndex, writeVal); + // pull out the ite from the write // pushes the write + // through. + ASTNode writeTrue = + bm->CreateNode(WRITE, (arrName[0][1]), writeIndex, writeVal); writeTrue.SetIndexWidth(writeIndex.GetValueWidth()); writeTrue.SetValueWidth(writeVal.GetValueWidth()); assert(ARRAY_TYPE == writeTrue.GetType()); - ASTNode writeFalse = bm->CreateNode(WRITE, (arrName[0][2]), writeIndex, writeVal); + ASTNode writeFalse = + bm->CreateNode(WRITE, (arrName[0][2]), writeIndex, writeVal); writeFalse.SetIndexWidth(writeIndex.GetValueWidth()); writeFalse.SetValueWidth(writeVal.GetValueWidth()); assert(ARRAY_TYPE == writeFalse.GetType()); - result = simp->CreateSimplifiedTermITE(TransformFormula(arrName[0][0]), writeTrue, writeFalse); + result = + simp->CreateSimplifiedTermITE(TransformFormula(arrName[0][0]), + writeTrue, writeFalse); result.SetIndexWidth(writeIndex.GetValueWidth()); result.SetValueWidth(writeVal.GetValueWidth()); assert(ARRAY_TYPE == result.GetType()); - result = bm->CreateTerm(READ, writeVal.GetValueWidth(), result, readIndex); + result = + bm->CreateTerm(READ, writeVal.GetValueWidth(), + result, readIndex); BVTypeCheck(result); result = TransformArray(result); } @@ -631,7 +717,8 @@ namespace BEEV break; } default: - FatalError("TransformArray: The READ is NOT over SYMBOL/WRITE/ITE", term); + FatalError("TransformArray: "\ + "The READ is NOT over SYMBOL/WRITE/ITE", term); break; } @@ -670,13 +757,14 @@ namespace BEEV ASTVec c = a.GetChildren(); SortByArith(c); if (SYMBOL != c[0].GetKind() || - bm->VarSeenInTerm(c[0], - simp->SimplifyFormula_NoRemoveWrites(c[1], false))) + bm->VarSeenInTerm(c[0], + simp->SimplifyFormula_NoRemoveWrites(c[1], false))) { return a; } bool updated = - simp->UpdateSubstitutionMap(c[0], simp->SimplifyFormula(c[1], false)); + simp->UpdateSubstitutionMap(c[0], + simp->SimplifyFormula(c[1], false)); output = updated ? ASTTrue : a; return output; } @@ -691,14 +779,14 @@ namespace BEEV ASTNode c1 = simp->SimplifyTerm(c[1]); if (SYMBOL == c[0].GetKind() - && bm->VarSeenInTerm(c[0], c1)) + && bm->VarSeenInTerm(c[0], c1)) { return a; } if (1 == TermOrder(c[0], c[1]) - && READ == c[0].GetKind() - && bm->VarSeenInTerm(c[0][1], c1)) + && READ == c[0].GetKind() + && bm->VarSeenInTerm(c[0][1], c1)) { return a; } @@ -711,7 +799,9 @@ namespace BEEV { ASTVec o; ASTVec c = a.GetChildren(); - for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) + for (ASTVec::iterator + it = c.begin(), itend = c.end(); + it != itend; it++) { simp->UpdateAlwaysTrueFormMap(*it); ASTNode aaa = CreateSubstitutionMap(*it); @@ -750,15 +840,15 @@ namespace BEEV //by a BVCONST (e1). This is necessary for later Leibnitz Axiom //generation void ArrayTransformer::FillUp_ArrReadIndex_Vec(const ASTNode& e0, - const ASTNode& e1) + const ASTNode& e1) { int i = TermOrder(e0, e1); if (0 == i) return; if (1 == i - && e0.GetKind() != SYMBOL - && !simp->CheckSubstitutionMap(e0)) + && e0.GetKind() != SYMBOL + && !simp->CheckSubstitutionMap(e0)) { (*Arrayname_ReadindicesMap)[e0[0]].push_back(e0[1]); //e0 is the array read : READ(A,i) and e1 is a bvconst @@ -766,8 +856,8 @@ namespace BEEV return; } if (-1 == i - && e1.GetKind() != SYMBOL - && !simp->CheckSubstitutionMap(e1)) + && e1.GetKind() != SYMBOL + && !simp->CheckSubstitutionMap(e1)) { (*Arrayname_ReadindicesMap)[e1[0]].push_back(e1[1]); //e0 is the array read : READ(A,i) and e1 is a bvconst diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index 8ae199d..b3fd4d7 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -169,9 +169,9 @@ namespace BEEV bool FoundIntroducedSymbolSet(const ASTNode& in) { if(Introduced_SymbolsSet.find(in) != Introduced_SymbolsSet.end()) - { - return true; - } + { + return true; + } return false; } // End of IntroduceSymbolSet @@ -179,12 +179,12 @@ namespace BEEV { for (ASTNodeToVecMap::iterator - iset = Arrayname_ReadindicesMap->begin(), - iset_end = Arrayname_ReadindicesMap->end(); - iset != iset_end; iset++) - { - iset->second.clear(); - } + iset = Arrayname_ReadindicesMap->begin(), + iset_end = Arrayname_ReadindicesMap->end(); + iset != iset_end; iset++) + { + iset->second.clear(); + } Arrayname_ReadindicesMap->clear(); Arrayread_SymbolMap.clear(); diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index 666d07e..cd7f727 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -19,82 +19,82 @@ std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsin namespace BEEV { - void FatalError(const char * str); + void FatalError(const char * str); } long RunTimes::getCurrentTime() { - timeval t; - gettimeofday(&t, NULL); - return (1000 * t.tv_sec) + (t.tv_usec / 1000); + timeval t; + gettimeofday(&t, NULL); + return (1000 * t.tv_sec) + (t.tv_usec / 1000); } void RunTimes::print() { - if (0 != category_stack.size()) - BEEV::FatalError("category stack is not yet emptuy"); + if (0 != category_stack.size()) + BEEV::FatalError("category stack is not yet emptuy"); - std::ostringstream result; - result << "statistics\n"; - std::map::const_iterator it1 = counts.begin(); - std::map::const_iterator it2 = times.begin(); + std::ostringstream result; + result << "statistics\n"; + std::map::const_iterator it1 = counts.begin(); + std::map::const_iterator it2 = times.begin(); - while (it1 != counts.end()) - { - result << " " << CategoryNames[it1->first] << ": " << it1->second; - if ((it2 = times.find(it1->first)) != times.end()) - result << " [" << it2->second << "ms]"; - result << std::endl; - it1++; - } + while (it1 != counts.end()) + { + result << " " << CategoryNames[it1->first] << ": " << it1->second; + if ((it2 = times.find(it1->first)) != times.end()) + result << " [" << it2->second << "ms]"; + result << std::endl; + it1++; + } - std::cerr << result.str(); - // iterator + std::cerr << result.str(); + // iterator } void RunTimes::addTime(Category c, long milliseconds) { - std::map::iterator it; - if ((it = times.find(c)) == times.end()) - { - times[c] = milliseconds; - } - else - { - it->second += milliseconds; - } + std::map::iterator it; + if ((it = times.find(c)) == times.end()) + { + times[c] = milliseconds; + } + else + { + it->second += milliseconds; + } } void RunTimes::addCount(Category c) { - std::map::iterator it; - if ((it = counts.find(c)) == counts.end()) - { - counts[c] = 1; - } - else - { - it->second++; - } + std::map::iterator it; + if ((it = counts.find(c)) == counts.end()) + { + counts[c] = 1; + } + else + { + it->second++; + } } void RunTimes::stop(Category c) { - Element e = category_stack.top(); - category_stack.pop(); - if (e.first != c) - { - std::cerr << e.first; - std::cerr << c; - BEEV::FatalError("Don't match"); - } - addTime(c, getCurrentTime() - e.second); - addCount(c); + Element e = category_stack.top(); + category_stack.pop(); + if (e.first != c) + { + std::cerr << e.first; + std::cerr << c; + BEEV::FatalError("Don't match"); + } + addTime(c, getCurrentTime() - e.second); + addCount(c); } void RunTimes::start(Category c) { - category_stack.push(std::make_pair(c, getCurrentTime())); + category_stack.push(std::make_pair(c, getCurrentTime())); } diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index e1bcb63..9f1ff00 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -34,7 +34,7 @@ public: typedef std::pair Element; - private: +private: RunTimes& operator =(const RunTimes&); RunTimes(const RunTimes& other); @@ -46,7 +46,7 @@ public: long getCurrentTime(); void addTime(Category c, long milliseconds); - public: +public: void addCount(Category c); void start(Category c); @@ -56,11 +56,11 @@ public: RunTimes(){} void clear() - { - counts.clear(); - times.clear(); - category_stack.empty(); - } + { + counts.clear(); + times.clear(); + category_stack.empty(); + } }; #endif diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h index cd51bb7..8a942b6 100644 --- a/src/AST/UsefulDefs.h +++ b/src/AST/UsefulDefs.h @@ -27,17 +27,17 @@ #include "RunTimes.h" #ifdef EXT_HASH_MAP - #include - #include +#include +#include #elif defined(TR1_UNORDERED_MAP) - #include - #include - #define hash_map tr1::unordered_map - #define hash_set tr1::unordered_set - #define hash_multiset tr1::unordered_multiset +#include +#include +#define hash_map tr1::unordered_map +#define hash_set tr1::unordered_set +#define hash_multiset tr1::unordered_multiset #else - #include - #include +#include +#include #endif #define HASHMAP hash_map @@ -115,9 +115,9 @@ namespace BEEV { eqstr> function_counters; #else typedef HASHMAP, - eqstr> function_counters; + int, + hash, + eqstr> function_counters; #endif // Function that computes various kinds of statistics for the phases diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index abc58a4..5d7023a 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -32,35 +32,35 @@ namespace BEEV { { inputToSAT = simplified_solved_InputToSAT; - if(optimize_flag) - { + if(optimize_flag) + { - bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); - simplified_solved_InputToSAT = - arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT); - bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); - //printf("##################################################\n"); - bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); + simplified_solved_InputToSAT = + arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT); + bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); + //printf("##################################################\n"); + bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); - simplified_solved_InputToSAT = - simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); + simplified_solved_InputToSAT = + simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); - bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); - } + bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); + } - if(wordlevel_solve_flag) - { - simplified_solved_InputToSAT = - bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); - bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT); - } + if(wordlevel_solve_flag) + { + simplified_solved_InputToSAT = + bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); + bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT); + } } while (inputToSAT != simplified_solved_InputToSAT); bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", - simplified_solved_InputToSAT); + simplified_solved_InputToSAT); bm->SimplifyWrites_InPlace_Flag = true; bm->Begin_RemoveWrites = false; @@ -70,29 +70,29 @@ namespace BEEV { { inputToSAT = simplified_solved_InputToSAT; - if(optimize_flag) - { - bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); - simplified_solved_InputToSAT = - arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT); - bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); - bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); - - simplified_solved_InputToSAT = - simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); - bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); - } - - if(wordlevel_solve_flag) - { - simplified_solved_InputToSAT = - bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); - bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT); - } + if(optimize_flag) + { + bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); + simplified_solved_InputToSAT = + arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT); + bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); + bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + + simplified_solved_InputToSAT = + simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); + bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); + } + + if(wordlevel_solve_flag) + { + simplified_solved_InputToSAT = + bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); + bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT); + } } while (inputToSAT != simplified_solved_InputToSAT); bm->ASTNodeStats("After SimplifyWrites_Inplace: ", - simplified_solved_InputToSAT); + simplified_solved_InputToSAT); bm->start_abstracting = (arraywrite_refinement_flag) ? true : false; bm->SimplifyWrites_InPlace_Flag = false; @@ -100,7 +100,7 @@ namespace BEEV { if (bm->start_abstracting) { bm->ASTNodeStats("before abstraction round begins: ", - simplified_solved_InputToSAT); + simplified_solved_InputToSAT); } bm->TermsAlreadySeenMap_Clear(); @@ -129,8 +129,8 @@ namespace BEEV { res = Ctr_Example->CallSAT_ResultCheck(newS, - simplified_solved_InputToSAT, - orig_input); + simplified_solved_InputToSAT, + orig_input); if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); @@ -140,14 +140,14 @@ namespace BEEV { // res = SATBased_AllFiniteLoops_Refinement(newS, orig_input); // if (SOLVER_UNDECIDED != res) // { - // CountersAndStats("print_func_stats"); + // CountersAndStats("print_func_stats"); // return res; // } res = Ctr_Example->SATBased_ArrayReadRefinement(newS, - simplified_solved_InputToSAT, - orig_input); + simplified_solved_InputToSAT, + orig_input); if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); @@ -164,8 +164,8 @@ namespace BEEV { res = Ctr_Example->SATBased_ArrayReadRefinement(newS, - simplified_solved_InputToSAT, - orig_input); + simplified_solved_InputToSAT, + orig_input); if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); @@ -178,92 +178,92 @@ namespace BEEV { return SOLVER_ERROR; } //End of TopLevelSTPAux -// void STP::ClearAllTables(void) -// { -// // //Clear STPManager caches - -// // //Clear ArrayTransformer caches - -// // //Clear Simplifier caches - -// // //Clear BVSolver caches - -// // //Clear AbsRefine_CounterExample caches - -// // //clear all tables before calling toplevelsat -// // //_ASTNode_to_SATVar.clear(); -// // //_SATVar_to_AST.clear(); - -// // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), -// // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) -// // // { -// // // (it->second)->clear(); -// // // delete (it->second); -// // // } -// // // _ASTNode_to_Bitvector.clear(); - -// // NodeLetVarMap.clear(); -// // NodeLetVarMap1.clear(); -// // PLPrintNodeSet.clear(); -// // AlreadyPrintedSet.clear(); -// // //ReferenceCount->clear(); -// // //_arrayread_ite.clear(); -// // //_introduced_symbols.clear(); -// // //CounterExampleMap.clear(); -// // //ComputeFormulaMap.clear(); -// // StatInfoSet.clear(); - -// // _asserts.clear(); - -// // // for (ASTNodeToVecMap::iterator iset = -// // // _arrayname_readindices.begin(), iset_end = -// // // _arrayname_readindices.end(); iset != iset_end; iset++) { -// // // iset->second.clear(); } -// // // _arrayname_readindices.clear(); - -// // _interior_unique_table.clear(); -// // _symbol_unique_table->clear(); -// // _bvconst_unique_table.clear(); -// } - -// void STP::ClearAllCaches(void) -// { -// // //clear all tables before calling toplevelsat -// // //_ASTNode_to_SATVar.clear(); -// // //_SATVar_to_AST.clear(); - -// // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), -// // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) -// // // { -// // // (it->second)->clear(); -// // // delete (it->second); -// // // } -// // // _ASTNode_to_Bitvector.clear(); + // void STP::ClearAllTables(void) + // { + // // //Clear STPManager caches + + // // //Clear ArrayTransformer caches + + // // //Clear Simplifier caches + + // // //Clear BVSolver caches + + // // //Clear AbsRefine_CounterExample caches + + // // //clear all tables before calling toplevelsat + // // //_ASTNode_to_SATVar.clear(); + // // //_SATVar_to_AST.clear(); + + // // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), + // // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) + // // // { + // // // (it->second)->clear(); + // // // delete (it->second); + // // // } + // // // _ASTNode_to_Bitvector.clear(); + + // // NodeLetVarMap.clear(); + // // NodeLetVarMap1.clear(); + // // PLPrintNodeSet.clear(); + // // AlreadyPrintedSet.clear(); + // // //ReferenceCount->clear(); + // // //_arrayread_ite.clear(); + // // //_introduced_symbols.clear(); + // // //CounterExampleMap.clear(); + // // //ComputeFormulaMap.clear(); + // // StatInfoSet.clear(); + + // // _asserts.clear(); + + // // // for (ASTNodeToVecMap::iterator iset = + // // // _arrayname_readindices.begin(), iset_end = + // // // _arrayname_readindices.end(); iset != iset_end; iset++) { + // // // iset->second.clear(); } + // // // _arrayname_readindices.clear(); + + // // _interior_unique_table.clear(); + // // _symbol_unique_table->clear(); + // // _bvconst_unique_table.clear(); + // } + + // void STP::ClearAllCaches(void) + // { + // // //clear all tables before calling toplevelsat + // // //_ASTNode_to_SATVar.clear(); + // // //_SATVar_to_AST.clear(); + + // // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), + // // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) + // // // { + // // // (it->second)->clear(); + // // // delete (it->second); + // // // } + // // // _ASTNode_to_Bitvector.clear(); -// // NodeLetVarMap.clear(); -// // NodeLetVarMap1.clear(); -// // PLPrintNodeSet.clear(); -// // AlreadyPrintedSet.clear(); -// // // SimplifyMap->clear(); -// // // SimplifyNegMap->clear(); -// // // ReferenceCount->clear(); -// // // SolverMap.clear(); -// // //AlwaysTrueFormMap.clear(); -// // //_arrayread_ite.clear(); -// // //_arrayread_symbol.clear(); -// // //_introduced_symbols.clear(); -// // //CounterExampleMap.clear(); -// // //ComputeFormulaMap.clear(); -// // StatInfoSet.clear(); - -// // // for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++) -// // // { -// // // iset->second.clear(); -// // // } + // // NodeLetVarMap.clear(); + // // NodeLetVarMap1.clear(); + // // PLPrintNodeSet.clear(); + // // AlreadyPrintedSet.clear(); + // // // SimplifyMap->clear(); + // // // SimplifyNegMap->clear(); + // // // ReferenceCount->clear(); + // // // SolverMap.clear(); + // // //AlwaysTrueFormMap.clear(); + // // //_arrayread_ite.clear(); + // // //_arrayread_symbol.clear(); + // // //_introduced_symbols.clear(); + // // //CounterExampleMap.clear(); + // // //ComputeFormulaMap.clear(); + // // StatInfoSet.clear(); + + // // // for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++) + // // // { + // // // iset->second.clear(); + // // // } -// // // _arrayname_readindices.clear(); -// // //_interior_unique_table.clear(); -// // //_symbol_unique_table.clear(); -// // //_bvconst_unique_table.clear(); -// } + // // // _arrayname_readindices.clear(); + // // //_interior_unique_table.clear(); + // // //_symbol_unique_table.clear(); + // // //_bvconst_unique_table.clear(); + // } }; //end of namespace diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h index 5929778..efd58b0 100644 --- a/src/STPManager/STP.h +++ b/src/STPManager/STP.h @@ -45,11 +45,11 @@ namespace BEEV //Constructor STP(STPMgr* b, - Simplifier* s, - BVSolver* bsolv, - ArrayTransformer * a, - ToSAT * ts, - AbsRefine_CounterExample * ce) + Simplifier* s, + BVSolver* bsolv, + ArrayTransformer * a, + ToSAT * ts, + AbsRefine_CounterExample * ce) { bm = b; simp = s; @@ -61,7 +61,7 @@ namespace BEEV ~STP() { - ClearAllTables(); + ClearAllTables(); } /**************************************************************** @@ -71,11 +71,11 @@ namespace BEEV // The absolute TopLevel function that invokes STP on the input // formula SOLVER_RETURN_TYPE TopLevelSTP(const ASTNode& inputasserts, - const ASTNode& query) + const ASTNode& query) { ASTNode q = bm->CreateNode(AND, - inputasserts, - bm->CreateNode(NOT, query)); + inputasserts, + bm->CreateNode(NOT, query)); return TopLevelSTPAux(q); } //End of TopLevelSTP() diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index bade332..eef71a3 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -32,7 +32,7 @@ namespace BEEV n_ptr->SetNodeNum(NewNodeNum()); } pair p = - _interior_unique_table.insert(n_ptr); + _interior_unique_table.insert(n_ptr); return *(p.first); } else @@ -57,8 +57,8 @@ namespace BEEV } ASTNode STPMgr::CreateNode(Kind kind, - const ASTNode& child0, - const ASTVec & back_children) + const ASTNode& child0, + const ASTVec & back_children) { ASTInterior *n_ptr = new ASTInterior(kind); @@ -69,9 +69,9 @@ namespace BEEV } ASTNode STPMgr::CreateNode(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTVec & back_children) + const ASTNode& child0, + const ASTNode& child1, + const ASTVec & back_children) { ASTInterior *n_ptr = new ASTInterior(kind); ASTVec &front_children = n_ptr->_children; @@ -82,10 +82,10 @@ namespace BEEV } ASTNode STPMgr::CreateNode(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2, - const ASTVec & back_children) + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec & back_children) { ASTInterior *n_ptr = new ASTInterior(kind); ASTVec &front_children = n_ptr->_children; @@ -97,28 +97,28 @@ namespace BEEV } ASTInterior *STPMgr::CreateInteriorNode(Kind kind, - // children array of this node will be modified. - ASTInterior *n_ptr, - const ASTVec & back_children) + // children array of this node will be modified. + ASTInterior *n_ptr, + const ASTVec & back_children) { // insert back_children at end of front_children ASTVec &front_children = n_ptr->_children; front_children.insert(front_children.end(), - back_children.begin(), - back_children.end()); + back_children.begin(), + back_children.end()); // check for undefined nodes. ASTVec::const_iterator it_end = front_children.end(); for (ASTVec::const_iterator it = front_children.begin(); it != it_end; it++) { if (it->IsNull()) - { - FatalError("CreateInteriorNode:"\ - "Undefined childnode in CreateInteriorNode: ", - ASTUndefined); - } + { + FatalError("CreateInteriorNode:"\ + "Undefined childnode in CreateInteriorNode: ", + ASTUndefined); + } } return LookupOrCreateInterior(n_ptr); @@ -174,13 +174,13 @@ namespace BEEV s_ptr1->SetNodeNum(NewNodeNum()); s_ptr1->_value_width = s_ptr->_value_width; pair p = - _symbol_unique_table.insert(s_ptr1); + _symbol_unique_table.insert(s_ptr1); return *p.first; } else { - // return symbol found in table. - return *it; + // return symbol found in table. + return *it; } } // End of LookupOrCreateSymbol @@ -189,7 +189,7 @@ namespace BEEV ASTSymbol* s_ptr = &s; // it's a temporary key. if (_symbol_unique_table.find(s_ptr) == - _symbol_unique_table.end()) + _symbol_unique_table.end()) return false; else return true; @@ -200,8 +200,8 @@ namespace BEEV { if (width > (sizeof(unsigned long long int) << 3) || width <= 0) FatalError("CreateBVConst: "\ - "trying to create a bvconst using unsigned long long of width: ", - ASTUndefined, width); + "trying to create a bvconst using unsigned long long of width: ", + ASTUndefined, width); CBV bv = CONSTANTBV::BitVector_Create(width, true); unsigned long c_val = (~((unsigned long) 0)) & bvconst; @@ -231,8 +231,8 @@ namespace BEEV ASTNode STPMgr::CreateBVConst(string*& strval, int base, int bit_width) { - if (bit_width <= 0) - FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, bit_width); + if (bit_width <= 0) + FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, bit_width); if (!(2 == base || 10 == base || 16 == base)) @@ -385,12 +385,12 @@ namespace BEEV // Create and return an ASTNode for a term ASTNode STPMgr::CreateTerm(Kind kind, - unsigned int width, - const ASTVec &children) + unsigned int width, + const ASTVec &children) { if (!is_Term_kind(kind)) FatalError("CreateTerm: Illegal kind to CreateTerm:", - ASTUndefined, kind); + ASTUndefined, kind); ASTNode n = CreateNode(kind, children); n.SetValueWidth(width); @@ -401,23 +401,23 @@ namespace BEEV } ASTNode STPMgr::CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTVec &children) + unsigned int width, + const ASTNode& child0, + const ASTVec &children) { if (!is_Term_kind(kind)) FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind); - ASTNode n = CreateNode(kind, child0, children); - n.SetValueWidth(width); - BVTypeCheck(n); - return n; + ASTNode n = CreateNode(kind, child0, children); + n.SetValueWidth(width); + BVTypeCheck(n); + return n; } ASTNode STPMgr::CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTNode& child1, - const ASTVec &children) + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec &children) { if (!is_Term_kind(kind)) FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind); @@ -427,11 +427,11 @@ namespace BEEV } ASTNode STPMgr::CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2, - const ASTVec &children) + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec &children) { if (!is_Term_kind(kind)) FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind); @@ -557,19 +557,19 @@ namespace BEEV } // //Create a new variable of ValueWidth 'n' -// ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value) -// { -// std::string c("v"); -// char d[32]; -// sprintf(d, "%d", _symbol_count++); -// std::string ccc(d); -// c += "_writearray_" + ccc; - -// ASTNode CurrentSymbol = CreateSymbol(c.c_str()); -// CurrentSymbol.SetValueWidth(value); -// CurrentSymbol.SetIndexWidth(index); -// return CurrentSymbol; -// } //end of NewArrayVar() + // ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value) + // { + // std::string c("v"); + // char d[32]; + // sprintf(d, "%d", _symbol_count++); + // std::string ccc(d); + // c += "_writearray_" + ccc; + + // ASTNode CurrentSymbol = CreateSymbol(c.c_str()); + // CurrentSymbol.SetValueWidth(value); + // CurrentSymbol.SetIndexWidth(index); + // return CurrentSymbol; + // } //end of NewArrayVar() //prints statistics for the ASTNode void STPMgr::ASTNodeStats(const char * c, const ASTNode& a) @@ -658,15 +658,15 @@ namespace BEEV bool STPMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term) { if (READ == term.GetKind() - && WRITE == term[0].GetKind() - && !GetRemoveWritesFlag()) + && WRITE == term[0].GetKind() + && !GetRemoveWritesFlag()) { return false; } if (READ == term.GetKind() - && WRITE == term[0].GetKind() - && GetRemoveWritesFlag()) + && WRITE == term[0].GetKind() + && GetRemoveWritesFlag()) { return true; } @@ -703,7 +703,7 @@ namespace BEEV ASTNode STPMgr::NewParameterized_BooleanVar(const ASTNode& var, - const ASTNode& constant) + const ASTNode& constant) { ostringstream outVar; ostringstream outNum; diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 337b707..74cb639 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -33,9 +33,9 @@ namespace BEEV // Typedef for unique Interior node table. typedef HASHSET< - ASTInterior *, - ASTInterior::ASTInteriorHasher, - ASTInterior::ASTInteriorEqual> ASTInteriorSet; + ASTInterior *, + ASTInterior::ASTInteriorHasher, + ASTInterior::ASTInteriorEqual> ASTInteriorSet; // Typedef for unique Symbol node (leaf) table. typedef HASHSET< @@ -104,9 +104,9 @@ namespace BEEV // nodes are not modified. Then it returns the hashed copy of the // node, which is created if necessary. ASTInterior *CreateInteriorNode(Kind kind, - ASTInterior *new_node, + ASTInterior *new_node, const ASTVec & back_children = - _empty_ASTVec); + _empty_ASTVec); // Create unique ASTInterior node. ASTInterior *LookupOrCreateInterior(ASTInterior *n); @@ -220,29 +220,29 @@ namespace BEEV // Simplifying create functions ASTNode CreateSimpForm(Kind kind, - ASTVec &children); + ASTVec &children); ASTNode CreateSimpForm(Kind kind, - const ASTNode& child0); + const ASTNode& child0); ASTNode CreateSimpForm(Kind kind, - const ASTNode& child0, - const ASTNode& child1); + const ASTNode& child0, + const ASTNode& child1); ASTNode CreateSimpForm(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2); + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2); ASTNode CreateSimpNot (const ASTNode& form); ASTNode CreateSimpXor(const ASTNode& form1, - const ASTNode& form2); + const ASTNode& form2); ASTNode CreateSimpXor(ASTVec &children); ASTNode CreateSimpAndOr(bool isAnd, - const ASTNode& form1, - const ASTNode& form2); + const ASTNode& form1, + const ASTNode& form2); ASTNode CreateSimpAndOr(bool IsAnd, - ASTVec &children); + ASTVec &children); ASTNode CreateSimpFormITE(const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2); + const ASTNode& child1, + const ASTNode& child2); /**************************************************************** * Create Symbol and BVConst functions * @@ -268,19 +268,19 @@ namespace BEEV // Create and return an interior ASTNode ASTNode CreateNode(Kind kind, - const ASTVec &children = _empty_ASTVec); + const ASTVec &children = _empty_ASTVec); ASTNode CreateNode(Kind kind, - const ASTNode& child0, - const ASTVec &children = _empty_ASTVec); + const ASTNode& child0, + const ASTVec &children = _empty_ASTVec); ASTNode CreateNode(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTVec &children = _empty_ASTVec); + 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); + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec &children = _empty_ASTVec); /**************************************************************** * Create Term functions * @@ -288,23 +288,23 @@ namespace BEEV // Create and return an ASTNode for a term ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTVec &children = _empty_ASTVec); + unsigned int width, + const ASTVec &children = _empty_ASTVec); ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTVec &children = _empty_ASTVec); + unsigned int width, + const ASTNode& child0, + const ASTVec &children = _empty_ASTVec); ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTNode& child1, - const ASTVec &children = _empty_ASTVec); + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec &children = _empty_ASTVec); ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2, - const ASTVec &children = _empty_ASTVec); + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec &children = _empty_ASTVec); /**************************************************************** @@ -362,7 +362,7 @@ namespace BEEV bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); ASTNode NewParameterized_BooleanVar(const ASTNode& var, - const ASTNode& constant); + const ASTNode& constant); void TermsAlreadySeenMap_Clear(void) { diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index 10f4c91..b03cf11 100644 --- a/src/absrefine_counterexample/AbsRefine_CounterExample.h +++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h @@ -19,209 +19,209 @@ namespace BEEV { class AbsRefine_CounterExample - { - private: + { + private: - // Handy defs - ASTNode ASTTrue, ASTFalse, ASTUndefined; + // Handy defs + ASTNode ASTTrue, ASTFalse, ASTUndefined; - // Data structure that holds the counterexample - ASTNodeMap CounterExampleMap; + // Data structure that holds the counterexample + ASTNodeMap CounterExampleMap; - // This map for building/printing counterexamples. MINISAT - // returns values for each bit (a BVGETBIT Node), and this maps - // allows us to assemble the bits into bitvectors. - typedef HASHMAP< - ASTNode, - HASHMAP *, - ASTNode::ASTNodeHasher, - ASTNode::ASTNodeEqual> ASTtoBitvectorMap; - - ASTtoBitvectorMap _ASTNode_to_BitvectorMap; - - // This memo map is used by the ComputeFormulaUsingModel() - ASTNodeMap ComputeFormulaMap; + // This map for building/printing counterexamples. MINISAT + // returns values for each bit (a BVGETBIT Node), and this maps + // allows us to assemble the bits into bitvectors. + typedef HASHMAP< + ASTNode, + HASHMAP *, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTtoBitvectorMap; + + ASTtoBitvectorMap _ASTNode_to_BitvectorMap; + + // This memo map is used by the ComputeFormulaUsingModel() + ASTNodeMap ComputeFormulaMap; - // Ptr to STPManager - STPMgr * bm; + // Ptr to STPManager + STPMgr * bm; - // Ptr to Simplifier - Simplifier * simp; + // Ptr to Simplifier + Simplifier * simp; - // Ptr to ArrayTransformer - ArrayTransformer * ArrayTransform; + // Ptr to ArrayTransformer + ArrayTransformer * ArrayTransform; - // Ptr to ToSAT - ToSAT * tosat; - - // Checks if the counterexample is good. In order for the - // counterexample to be ok, every assert must evaluate to true - // w.r.t couner_example, and the query must evaluate to - // false. Otherwise we know that the counter_example is bogus. - void CheckCounterExample(bool t); - - // Accepts a term and turns it into a constant-term w.r.t - // counter_example - ASTNode TermToConstTermUsingModel(const ASTNode& term, - bool ArrayReadFlag = true); - - ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term, - bool ArrayReadFlag = true); - - void CopySolverMap_To_CounterExample(void); - - //Converts a vector of bools to a BVConst - ASTNode BoolVectoBVConst(HASHMAP * w, unsigned int l); - - public: - - // Constructor - AbsRefine_CounterExample(STPMgr * b, - Simplifier * s, - ArrayTransformer * at, - ToSAT * t) : - bm(b), simp(s), ArrayTransform(at), tosat(t) - { - ASTTrue = bm->CreateNode(TRUE); - ASTFalse = bm->CreateNode(FALSE); - ASTUndefined = bm->CreateNode(UNDEFINED); - } - - void ClearCounterExampleMap(void) - { - CounterExampleMap.clear(); - } - - void ClearComputeFormulaMap(void) - { - ComputeFormulaMap.clear(); - } - - //Converts MINISAT counterexample into an AST memotable (i.e. the - //function populates the datastructure CounterExampleMap) - void ConstructCounterExample(MINISAT::Solver& S); + // Ptr to ToSAT + ToSAT * tosat; + + // Checks if the counterexample is good. In order for the + // counterexample to be ok, every assert must evaluate to true + // w.r.t couner_example, and the query must evaluate to + // false. Otherwise we know that the counter_example is bogus. + void CheckCounterExample(bool t); + + // Accepts a term and turns it into a constant-term w.r.t + // counter_example + ASTNode TermToConstTermUsingModel(const ASTNode& term, + bool ArrayReadFlag = true); + + ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term, + bool ArrayReadFlag = true); + + void CopySolverMap_To_CounterExample(void); + + //Converts a vector of bools to a BVConst + ASTNode BoolVectoBVConst(HASHMAP * w, unsigned int l); + + public: + + // Constructor + AbsRefine_CounterExample(STPMgr * b, + Simplifier * s, + ArrayTransformer * at, + ToSAT * t) : + bm(b), simp(s), ArrayTransform(at), tosat(t) + { + ASTTrue = bm->CreateNode(TRUE); + ASTFalse = bm->CreateNode(FALSE); + ASTUndefined = bm->CreateNode(UNDEFINED); + } + + void ClearCounterExampleMap(void) + { + CounterExampleMap.clear(); + } + + void ClearComputeFormulaMap(void) + { + ComputeFormulaMap.clear(); + } + + //Converts MINISAT counterexample into an AST memotable (i.e. the + //function populates the datastructure CounterExampleMap) + void ConstructCounterExample(MINISAT::Solver& S); - //Prints the counterexample to stdout - void PrintCounterExample(bool t, std::ostream& os = cout); + //Prints the counterexample to stdout + void PrintCounterExample(bool t, std::ostream& os = cout); - //Prints the counterexample to stdout - void PrintCounterExample_InOrder(bool t); + //Prints the counterexample to stdout + void PrintCounterExample_InOrder(bool t); - //queries the counterexample, and returns the value corresponding - //to e - ASTNode GetCounterExample(bool t, const ASTNode& e); + //queries the counterexample, and returns the value corresponding + //to e + ASTNode GetCounterExample(bool t, const ASTNode& e); - int CounterExampleSize(void) const - { - return CounterExampleMap.size(); - } - - //FIXME: This is bloody dangerous function. Hack attack to take - //care of requests from users who want to store complete - //counter-examples in their own data structures. - ASTNodeMap GetCompleteCounterExample() - { - return CounterExampleMap; - } + int CounterExampleSize(void) const + { + return CounterExampleMap.size(); + } + + //FIXME: This is bloody dangerous function. Hack attack to take + //care of requests from users who want to store complete + //counter-examples in their own data structures. + ASTNodeMap GetCompleteCounterExample() + { + return CounterExampleMap; + } - //Computes the truth value of a formula w.r.t counter_example - ASTNode ComputeFormulaUsingModel(const ASTNode& form); - - - // Prints MINISAT assigment one bit at a time, for debugging. - void PrintSATModel(MINISAT::Solver& S); - - /**************************************************************** - * Array Refinement functions * - ****************************************************************/ - SOLVER_RETURN_TYPE - CallSAT_ResultCheck(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input); - //creates array write axiom only for the input term or formula, if - //necessary. If there are no axioms to produce then it simply - //generates TRUE - ASTNode - Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, - const ASTNode& array_newname); + //Computes the truth value of a formula w.r.t counter_example + ASTNode ComputeFormulaUsingModel(const ASTNode& form); + + + // Prints MINISAT assigment one bit at a time, for debugging. + void PrintSATModel(MINISAT::Solver& S); + + /**************************************************************** + * Array Refinement functions * + ****************************************************************/ + SOLVER_RETURN_TYPE + CallSAT_ResultCheck(MINISAT::Solver& SatSolver, + const ASTNode& modified_input, + const ASTNode& original_input); + //creates array write axiom only for the input term or formula, if + //necessary. If there are no axioms to produce then it simply + //generates TRUE + ASTNode + Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, + const ASTNode& array_newname); - SOLVER_RETURN_TYPE - SATBased_ArrayReadRefinement(MINISAT::Solver& newS, - const ASTNode& modified_input, - const ASTNode& original_input); - - SOLVER_RETURN_TYPE - SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, - const ASTNode& orig_input); + SOLVER_RETURN_TYPE + SATBased_ArrayReadRefinement(MINISAT::Solver& newS, + const ASTNode& modified_input, + const ASTNode& original_input); + + SOLVER_RETURN_TYPE + SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, + const ASTNode& orig_input); - // SOLVER_RETURN_TYPE - // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS, - // const ASTNode& orig_input); + // SOLVER_RETURN_TYPE + // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS, + // const ASTNode& orig_input); - // ASTVec SATBased_FiniteLoop_Refinement(MINISAT::Solver& - // SatSolver, const ASTNode& original_input, const ASTNode& - // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool - // absrefine_flag=false); + // ASTVec SATBased_FiniteLoop_Refinement(MINISAT::Solver& + // SatSolver, const ASTNode& original_input, const ASTNode& + // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool + // absrefine_flag=false); - // ASTNode Check_FiniteLoop_UsingModel(const ASTNode& - // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool - // CheckUsingModel_Or_Expand); - // - // ASTNode Expand_FiniteLoop_TopLevel(const ASTNode& - // finiteloop); ASTNode Check_FiniteLoop_UsingModel(const - // ASTNode& finiteloop); - - void ClearAllTables(void) - { - CounterExampleMap.clear(); - for (ASTtoBitvectorMap::iterator - it = _ASTNode_to_BitvectorMap.begin(), - itend = _ASTNode_to_BitvectorMap.end(); - it != itend; it++) - { - (it->second)->clear(); - delete (it->second); - } - _ASTNode_to_BitvectorMap.clear(); - ComputeFormulaMap.clear(); - } //End of ClearAllTables() - };//End of Class CounterExample + // ASTNode Check_FiniteLoop_UsingModel(const ASTNode& + // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool + // CheckUsingModel_Or_Expand); + // + // ASTNode Expand_FiniteLoop_TopLevel(const ASTNode& + // finiteloop); ASTNode Check_FiniteLoop_UsingModel(const + // ASTNode& finiteloop); + + void ClearAllTables(void) + { + CounterExampleMap.clear(); + for (ASTtoBitvectorMap::iterator + it = _ASTNode_to_BitvectorMap.begin(), + itend = _ASTNode_to_BitvectorMap.end(); + it != itend; it++) + { + (it->second)->clear(); + delete (it->second); + } + _ASTNode_to_BitvectorMap.clear(); + ComputeFormulaMap.clear(); + } //End of ClearAllTables() + };//End of Class CounterExample class CompleteCounterExample + { + ASTNodeMap counterexample; + STPMgr * bv; + public: + CompleteCounterExample(ASTNodeMap a, STPMgr* beev) : + counterexample(a), bv(beev) + { + } + ASTNode GetCounterExample(ASTNode e) { - ASTNodeMap counterexample; - STPMgr * bv; - public: - CompleteCounterExample(ASTNodeMap a, STPMgr* beev) : - counterexample(a), bv(beev) - { - } - ASTNode GetCounterExample(ASTNode e) - { - if (BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind()) - { - FatalError("You must input a term or propositional variables\n", e); - } - if (counterexample.find(e) != counterexample.end()) - { - return counterexample[e]; - } - else - { - if (SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType()) - { - return bv->CreateNode(BEEV::FALSE); - } - - if (SYMBOL == e.GetKind()) - { - ASTNode z = bv->CreateZeroConst(e.GetValueWidth()); - return z; - } - - return e; - } - } - };//end of Class CompleteCounterExample + if (BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind()) + { + FatalError("You must input a term or propositional variables\n", e); + } + if (counterexample.find(e) != counterexample.end()) + { + return counterexample[e]; + } + else + { + if (SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType()) + { + return bv->CreateNode(BEEV::FALSE); + } + + if (SYMBOL == e.GetKind()) + { + ASTNode z = bv->CreateZeroConst(e.GetValueWidth()); + return z; + } + + return e; + } + } + };//end of Class CompleteCounterExample };//end of namespace #endif diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index 838cba7..7e11b7f 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -41,8 +41,8 @@ namespace BEEV *****************************************************************/ SOLVER_RETURN_TYPE AbsRefine_CounterExample::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, - const ASTNode& inputAlreadyInSAT, - const ASTNode& original_input) { + const ASTNode& inputAlreadyInSAT, + const ASTNode& original_input) { //printf("doing array read refinement\n"); if (!arrayread_refinement_flag) FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); @@ -59,9 +59,9 @@ namespace BEEV // //for each array, fetch its list of indices seen so far for (ASTNodeToVecMap::const_iterator - iset = ArrayTransform->ArrayName_ReadIndicesMap()->begin(), + iset = ArrayTransform->ArrayName_ReadIndicesMap()->begin(), iset_end = ArrayTransform->ArrayName_ReadIndicesMap()->end(); - iset != iset_end; iset++) + iset != iset_end; iset++) { ASTVec listOfIndices = iset->second; //loop over the list of indices for the array and create LA, @@ -79,9 +79,9 @@ namespace BEEV ASTNode ArrName = iset->first; // if(SYMBOL != ArrName.GetKind()) // FatalError("SATBased_ArrayReadRefinement: "\ - // "arrname is not a SYMBOL",ArrName); + // "arrname is not a SYMBOL",ArrName); ASTNode arr_read1 = - bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index); + bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index); //get the variable corresponding to the array_read1 //ASTNode arrsym1 = _arrayread_symbol[arr_read1]; ASTNode arrsym1 = ArrayTransform->ArrayRead_SymbolMap(arr_read1); @@ -104,13 +104,13 @@ namespace BEEV ASTNode eqOfIndices = (exprless(the_index, compare_index)) ? simp->CreateSimplifiedEQ(the_index, compare_index) : - simp->CreateSimplifiedEQ(compare_index, the_index); + simp->CreateSimplifiedEQ(compare_index, the_index); ASTNode arr_read2 = - bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index); + bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index); //get the variable corresponding to the array_read2 //ASTNode arrsym2 = _arrayread_symbol[arr_read2]; - ASTNode arrsym2 = ArrayTransform->ArrayRead_SymbolMap(arr_read2); + ASTNode arrsym2 = ArrayTransform->ArrayRead_SymbolMap(arr_read2); if (!(SYMBOL == arrsym2.GetKind() || BVCONST == arrsym2.GetKind())) FatalError("TopLevelSAT: refinement loop:" "term arrsym2 corresponding to READ must be a var", arrsym2); @@ -135,9 +135,9 @@ namespace BEEV if (FalseAxiomsVec.size() > oldFalseAxiomsSize) { res2 = - CallSAT_ResultCheck(SatSolver, - FalseAxioms, - original_input); + CallSAT_ResultCheck(SatSolver, + FalseAxioms, + original_input); oldFalseAxiomsSize = FalseAxiomsVec.size(); } //printf("spot 02, res2 = %d\n", res2); @@ -152,8 +152,8 @@ namespace BEEV bm->CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0]; bm->ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms); return CallSAT_ResultCheck(SatSolver, - RemainingAxioms, - original_input); + RemainingAxioms, + original_input); } //end of SATBased_ArrayReadRefinement @@ -165,7 +165,7 @@ namespace BEEV SOLVER_RETURN_TYPE AbsRefine_CounterExample:: SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + const ASTNode& original_input) { ASTNode writeAxiom; ASTNodeMap::const_iterator it = simp->ReadOverWriteMap()->begin(); @@ -202,8 +202,8 @@ namespace BEEV if (FalseAxioms.size() > oldFalseAxiomsSize) { res2 = CallSAT_ResultCheck(SatSolver, - writeAxiom, - original_input); + writeAxiom, + original_input); oldFalseAxiomsSize = FalseAxioms.size(); } if (SOLVER_UNDECIDED != res2) @@ -216,8 +216,8 @@ namespace BEEV bm->CreateNode(AND, RemainingAxioms) : RemainingAxioms[0]; bm->ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom); res2 = CallSAT_ResultCheck(SatSolver, - writeAxiom, - original_input); + writeAxiom, + original_input); if (SOLVER_UNDECIDED != res2) { return res2; @@ -228,12 +228,12 @@ namespace BEEV //bm->Creates Array Write Axioms ASTNode AbsRefine_CounterExample::Create_ArrayWriteAxioms(const ASTNode& term, - const ASTNode& newvar) + const ASTNode& newvar) { if (READ != term.GetKind() && WRITE != term[0].GetKind()) { FatalError("Create_ArrayWriteAxioms: "\ - "Input must be a READ over a WRITE", term); + "Input must be a READ over a WRITE", term); } ASTNode lhs = newvar; @@ -243,407 +243,407 @@ namespace BEEV }//end of Create_ArrayWriteAxioms() -// static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, -// const ASTNode& key, const ASTNode& value) -// { -// ASTNodeMap::iterator it = VarToConstMap->find(key); -// if(it != VarToConstMap->end()) -// { -// VarToConstMap->erase(it); -// } - -// (*VarToConstMap)[key] = value; -// return; -// } - - -// /****************************************************************** -// * FINITE FORLOOP ABSTRACTION REFINEMENT -// * -// * For each 'finiteloop' in the list 'GlobalList_Of_FiniteLoops' -// * -// * Expand_FiniteLoop(finiteloop); -// * -// * The 'Expand_FiniteLoop' function expands the 'finiteloop' in a -// * counterexample-guided refinement fashion -// * -// * Once all the finiteloops have been expanded, we need to go back -// * and recheck that every discarded constraint is true with the -// * final model. A flag 'done' is set to false if atleast one -// * constraint is false during model-check, and is set to true if all -// * constraints are true during model-check. -// * -// * if the 'done' flag is true, then we terminate this refinement -// * loop. -// *****************************************************************/ -// SOLVER_RETURN_TYPE -// AbsRefine_CounterExample::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, -// const ASTNode& original_input) -// { -// //cout << "The number of abs-refinement limit is " << num_absrefine << endl; -// for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) -// { -// ASTVec Allretvec0; -// Allretvec0.push_back(ASTTrue); -// SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; -// for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), -// iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) -// { -// ASTVec retvec; -// ASTNodeMap ParamToCurrentValMap; -// retvec = SATBased_FiniteLoop_Refinement(SatSolver, -// original_input, -// *i, -// &ParamToCurrentValMap, -// true); //absrefine flag - -// for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++) -// { -// Allretvec0.push_back(*j); -// } -// //Allretvec0.(Allretvec0.end(),retvec.begin(),retvec.end()); -// } //End of For - -// ASTNode retformula = -// (Allretvec0.size() == 1) ? -// Allretvec0[0] : bm->CreateNode(AND,Allretvec0); -// retformula = TransformFormula_TopLevel(retformula); - -// //Add the return value of all loops to the SAT Solver -// res = -// CallSAT_ResultCheck(SatSolver, retformula, original_input); -// if(SOLVER_UNDECIDED != res) -// { -// return res; -// } -// } //end of absrefine count + // static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, + // const ASTNode& key, const ASTNode& value) + // { + // ASTNodeMap::iterator it = VarToConstMap->find(key); + // if(it != VarToConstMap->end()) + // { + // VarToConstMap->erase(it); + // } + + // (*VarToConstMap)[key] = value; + // return; + // } + + + // /****************************************************************** + // * FINITE FORLOOP ABSTRACTION REFINEMENT + // * + // * For each 'finiteloop' in the list 'GlobalList_Of_FiniteLoops' + // * + // * Expand_FiniteLoop(finiteloop); + // * + // * The 'Expand_FiniteLoop' function expands the 'finiteloop' in a + // * counterexample-guided refinement fashion + // * + // * Once all the finiteloops have been expanded, we need to go back + // * and recheck that every discarded constraint is true with the + // * final model. A flag 'done' is set to false if atleast one + // * constraint is false during model-check, and is set to true if all + // * constraints are true during model-check. + // * + // * if the 'done' flag is true, then we terminate this refinement + // * loop. + // *****************************************************************/ + // SOLVER_RETURN_TYPE + // AbsRefine_CounterExample::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, + // const ASTNode& original_input) + // { + // //cout << "The number of abs-refinement limit is " << num_absrefine << endl; + // for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) + // { + // ASTVec Allretvec0; + // Allretvec0.push_back(ASTTrue); + // SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; + // for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), + // iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) + // { + // ASTVec retvec; + // ASTNodeMap ParamToCurrentValMap; + // retvec = SATBased_FiniteLoop_Refinement(SatSolver, + // original_input, + // *i, + // &ParamToCurrentValMap, + // true); //absrefine flag + + // for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++) + // { + // Allretvec0.push_back(*j); + // } + // //Allretvec0.(Allretvec0.end(),retvec.begin(),retvec.end()); + // } //End of For + + // ASTNode retformula = + // (Allretvec0.size() == 1) ? + // Allretvec0[0] : bm->CreateNode(AND,Allretvec0); + // retformula = TransformFormula_TopLevel(retformula); + + // //Add the return value of all loops to the SAT Solver + // res = + // CallSAT_ResultCheck(SatSolver, retformula, original_input); + // if(SOLVER_UNDECIDED != res) + // { + // return res; + // } + // } //end of absrefine count -// ASTVec Allretvec1; -// Allretvec1.push_back(ASTTrue); -// SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; -// for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), -// iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) -// { -// //cout << "The abs-refine didn't finish the job. Add the remaining formulas\n"; -// ASTNodeMap ParamToCurrentValMap; -// ASTVec retvec; -// retvec = SATBased_FiniteLoop_Refinement(SatSolver, -// original_input, -// *i, -// &ParamToCurrentValMap, -// false); //absrefine flag -// for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++) -// { -// Allretvec1.push_back(*j); -// } -// } //End of For - -// ASTNode retformula = -// (Allretvec1.size() == 1) ? -// Allretvec1[0] : bm->CreateNode(AND,Allretvec1); -// retformula = TransformFormula_TopLevel(retformula); -// //Add the return value of all loops to the SAT Solver -// res = CallSAT_ResultCheck(SatSolver, retformula, original_input); -// return res; -// } //end of SATBased_AllFiniteLoops_Refinement() + // ASTVec Allretvec1; + // Allretvec1.push_back(ASTTrue); + // SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; + // for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), + // iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) + // { + // //cout << "The abs-refine didn't finish the job. Add the remaining formulas\n"; + // ASTNodeMap ParamToCurrentValMap; + // ASTVec retvec; + // retvec = SATBased_FiniteLoop_Refinement(SatSolver, + // original_input, + // *i, + // &ParamToCurrentValMap, + // false); //absrefine flag + // for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++) + // { + // Allretvec1.push_back(*j); + // } + // } //End of For + + // ASTNode retformula = + // (Allretvec1.size() == 1) ? + // Allretvec1[0] : bm->CreateNode(AND,Allretvec1); + // retformula = TransformFormula_TopLevel(retformula); + // //Add the return value of all loops to the SAT Solver + // res = CallSAT_ResultCheck(SatSolver, retformula, original_input); + // return res; + // } //end of SATBased_AllFiniteLoops_Refinement() -// /***************************************************************** -// * SATBased_FiniteLoop_Refinement -// * -// * 'finiteloop' is the finite loop to be expanded -// * Every finiteloop has three parts: -// * 0) Parameter Name -// * 1) Parameter initialization -// * 2) Parameter limit value -// * 3) Increment formula -// * 4) Formula Body -// * -// * ParamToCurrentValMap contains a map from parameters to their -// * current values in the recursion -// * -// * Nested FORs are allowed, but only the innermost loop can have a -// * formula in it -// *****************************************************************/ -// //SATBased_FiniteLoop_Refinement -// // -// //Expand the finite loop, check against model, and add false -// //formulas to the SAT solver -// ASTVec -// AbsRefine_CounterExample::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, -// const ASTNode& original_input, -// const ASTNode& finiteloop, -// ASTNodeMap* ParamToCurrentValMap, -// bool absrefine_flag) -// { -// //BVTypeCheck should have already checked the sanity of the input -// //FOR-formula -// ASTNode parameter = finiteloop[0]; -// int paramInit = GetUnsignedConst(finiteloop[1]); -// int paramLimit = GetUnsignedConst(finiteloop[2]); -// int paramIncrement = GetUnsignedConst(finiteloop[3]); -// ASTNode exceptFormula = finiteloop[4]; -// ASTNode formulabody = finiteloop[5]; -// int paramCurrentValue = paramInit; -// int width = finiteloop[1].GetValueWidth(); - -// //Update ParamToCurrentValMap with parameter and its current -// //value. Here paramCurrentValue is the initial value -// ASTNode value = -// bm->CreateBVConst(width,paramCurrentValue); -// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); + // /***************************************************************** + // * SATBased_FiniteLoop_Refinement + // * + // * 'finiteloop' is the finite loop to be expanded + // * Every finiteloop has three parts: + // * 0) Parameter Name + // * 1) Parameter initialization + // * 2) Parameter limit value + // * 3) Increment formula + // * 4) Formula Body + // * + // * ParamToCurrentValMap contains a map from parameters to their + // * current values in the recursion + // * + // * Nested FORs are allowed, but only the innermost loop can have a + // * formula in it + // *****************************************************************/ + // //SATBased_FiniteLoop_Refinement + // // + // //Expand the finite loop, check against model, and add false + // //formulas to the SAT solver + // ASTVec + // AbsRefine_CounterExample::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, + // const ASTNode& original_input, + // const ASTNode& finiteloop, + // ASTNodeMap* ParamToCurrentValMap, + // bool absrefine_flag) + // { + // //BVTypeCheck should have already checked the sanity of the input + // //FOR-formula + // ASTNode parameter = finiteloop[0]; + // int paramInit = GetUnsignedConst(finiteloop[1]); + // int paramLimit = GetUnsignedConst(finiteloop[2]); + // int paramIncrement = GetUnsignedConst(finiteloop[3]); + // ASTNode exceptFormula = finiteloop[4]; + // ASTNode formulabody = finiteloop[5]; + // int paramCurrentValue = paramInit; + // int width = finiteloop[1].GetValueWidth(); + + // //Update ParamToCurrentValMap with parameter and its current + // //value. Here paramCurrentValue is the initial value + // ASTNode value = + // bm->CreateBVConst(width,paramCurrentValue); + // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); -// //Go recursively thru' all the FOR-constructs. -// if(FOR == formulabody.GetKind()) -// { -// ASTVec retvec; -// ASTVec retvec_innerfor; -// retvec.push_back(ASTTrue); -// while(paramCurrentValue < paramLimit) -// { -// retvec_innerfor = -// SATBased_FiniteLoop_Refinement(SatSolver, -// original_input, -// formulabody, -// ParamToCurrentValMap, -// absrefine_flag); - -// for(ASTVec::iterator i=retvec_innerfor.begin(), -// iend=retvec_innerfor.end();i!=iend;i++) -// { -// retvec.push_back(*i); -// } - -// //Update ParamToCurrentValMap with parameter and its -// //current value. -// paramCurrentValue = paramCurrentValue + paramIncrement; -// value = bm->CreateTerm(BVPLUS, -// width, -// (*ParamToCurrentValMap)[parameter], -// bm->CreateOneConst(width)); -// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); -// } //end of While - -// return retvec; -// } //end of recursion FORs - -// //Expand the leaf level FOR-construct completely -// //increment of paramCurrentValue done inside loop -// int ThisForLoopAllTrue = 0; -// ASTVec ForloopVec; -// ForloopVec.push_back(ASTTrue); -// for(;paramCurrentValue < paramLimit;) -// { -// ASTNode currentFormula; -// ASTNode currentExceptFormula = exceptFormula; -// currentExceptFormula = -// SimplifyFormula(exceptFormula, false, ParamToCurrentValMap); -// if(ASTTrue == currentExceptFormula) -// { -// currentFormula = ASTTrue; -// } -// else -// { -// currentFormula = -// SimplifyFormula(formulabody, false, ParamToCurrentValMap); -// } - -// //Check the currentformula against the model, and add it to the -// //SAT solver if it is false against the model -// if(absrefine_flag -// && -// ASTFalse == ComputeFormulaUsingModel(currentFormula) -// ) -// { -// ForloopVec.push_back(currentFormula); -// } -// else -// { -// if(ASTTrue != currentFormula) -// { -// ForloopVec.push_back(currentFormula); -// } -// if(ASTFalse == currentFormula) -// { -// ForloopVec.push_back(ASTFalse); -// return ForloopVec; -// } -// } + // //Go recursively thru' all the FOR-constructs. + // if(FOR == formulabody.GetKind()) + // { + // ASTVec retvec; + // ASTVec retvec_innerfor; + // retvec.push_back(ASTTrue); + // while(paramCurrentValue < paramLimit) + // { + // retvec_innerfor = + // SATBased_FiniteLoop_Refinement(SatSolver, + // original_input, + // formulabody, + // ParamToCurrentValMap, + // absrefine_flag); + + // for(ASTVec::iterator i=retvec_innerfor.begin(), + // iend=retvec_innerfor.end();i!=iend;i++) + // { + // retvec.push_back(*i); + // } + + // //Update ParamToCurrentValMap with parameter and its + // //current value. + // paramCurrentValue = paramCurrentValue + paramIncrement; + // value = bm->CreateTerm(BVPLUS, + // width, + // (*ParamToCurrentValMap)[parameter], + // bm->CreateOneConst(width)); + // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); + // } //end of While + + // return retvec; + // } //end of recursion FORs + + // //Expand the leaf level FOR-construct completely + // //increment of paramCurrentValue done inside loop + // int ThisForLoopAllTrue = 0; + // ASTVec ForloopVec; + // ForloopVec.push_back(ASTTrue); + // for(;paramCurrentValue < paramLimit;) + // { + // ASTNode currentFormula; + // ASTNode currentExceptFormula = exceptFormula; + // currentExceptFormula = + // SimplifyFormula(exceptFormula, false, ParamToCurrentValMap); + // if(ASTTrue == currentExceptFormula) + // { + // currentFormula = ASTTrue; + // } + // else + // { + // currentFormula = + // SimplifyFormula(formulabody, false, ParamToCurrentValMap); + // } + + // //Check the currentformula against the model, and add it to the + // //SAT solver if it is false against the model + // if(absrefine_flag + // && + // ASTFalse == ComputeFormulaUsingModel(currentFormula) + // ) + // { + // ForloopVec.push_back(currentFormula); + // } + // else + // { + // if(ASTTrue != currentFormula) + // { + // ForloopVec.push_back(currentFormula); + // } + // if(ASTFalse == currentFormula) + // { + // ForloopVec.push_back(ASTFalse); + // return ForloopVec; + // } + // } -// //Update ParamToCurrentValMap with parameter and its current -// //value. -// paramCurrentValue = paramCurrentValue + paramIncrement; -// value = bm->CreateTerm(BVPLUS, -// width, -// (*ParamToCurrentValMap)[parameter], -// bm->CreateOneConst(width)); -// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); -// } //end of expanding the FOR loop + // //Update ParamToCurrentValMap with parameter and its current + // //value. + // paramCurrentValue = paramCurrentValue + paramIncrement; + // value = bm->CreateTerm(BVPLUS, + // width, + // (*ParamToCurrentValMap)[parameter], + // bm->CreateOneConst(width)); + // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); + // } //end of expanding the FOR loop -// return ForloopVec; -// } //end of the SATBased_FiniteLoop_Refinement() - -// //SATBased_FiniteLoop_Refinement_UsingModel(). Expand the finite -// //loop, check against model -// ASTNode -// AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, -// ASTNodeMap* ParamToCurrentValMap, -// bool checkusingmodel_flag = true) -// { -// /* -// * 'finiteloop' is the finite loop to be expanded -// * Every finiteloop has three parts: -// * 0) Parameter Name -// * 1) Parameter initialization -// * 2) Parameter limit value -// * 3) Increment formula -// * 4) Formula Body -// * -// * ParamToCurrentValMap contains a map from parameters to their -// * current values in the recursion -// * -// * Nested FORs are allowed, but only the innermost loop can have a -// * formula in it -// */ - -// //BVTypeCheck should have already checked the sanity of the input -// //FOR-formula -// ASTNode parameter = finiteloop[0]; -// int paramInit = GetUnsignedConst(finiteloop[1]); -// int paramLimit = GetUnsignedConst(finiteloop[2]); -// int paramIncrement = GetUnsignedConst(finiteloop[3]); -// ASTNode exceptFormula = finiteloop[4]; -// ASTNode formulabody = finiteloop[5]; -// int paramCurrentValue = paramInit; -// int width = finiteloop[1].GetValueWidth(); - -// //Update ParamToCurrentValMap with parameter and its current -// //value. Here paramCurrentValue is the initial value -// ASTNode value = -// bm->CreateBVConst(width,paramCurrentValue); -// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); - -// ASTNode ret = ASTTrue; -// ASTVec returnVec; -// //Go recursively thru' all the FOR-constructs. -// if(FOR == formulabody.GetKind()) -// { -// while(paramCurrentValue < paramLimit) -// { -// ret = Check_FiniteLoop_UsingModel(formulabody, -// ParamToCurrentValMap, -// checkusingmodel_flag); -// if(ASTFalse == ret) -// { -// //no more expansion needed. Return immediately -// return ret; -// } -// else -// { -// returnVec.push_back(ret); -// } - -// //Update ParamToCurrentValMap with parameter and its -// //current value. -// paramCurrentValue = paramCurrentValue + paramIncrement; -// value = bm->CreateTerm(BVPLUS, -// width, -// (*ParamToCurrentValMap)[parameter], -// bm->CreateOneConst(width)); -// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); -// } //end of While - -// ASTNode retFormula = -// (returnVec.size() > 1) ? -// bm->CreateNode(AND, returnVec) : -// (returnVec.size() == 1) ? -// returnVec[0] : -// ASTTrue; -// return retFormula; -// } - -// ASTVec forloopFormulaVector; -// //Expand the leaf level FOR-construct completely -// //incrementing of paramCurrentValue is done inside loop -// for(;paramCurrentValue < paramLimit;) -// { -// ASTNode currentFormula; - -// ASTNode currentExceptFormula = exceptFormula; -// currentExceptFormula = -// SimplifyFormula(exceptFormula, false, ParamToCurrentValMap); -// if(ASTTrue == currentExceptFormula) -// { -// currentFormula = ASTTrue; -// //continue; -// } -// else -// { -// currentFormula = -// SimplifyFormula(formulabody, false, ParamToCurrentValMap); -// } - -// if(checkusingmodel_flag) -// { -// //Check the currentformula against the model, and return -// //immediately -// //cout << "Printing current Formula: " << currentFormula << "\n"; -// ASTNode computedForm = ComputeFormulaUsingModel(currentFormula); -// //cout << "Printing computed Formula: " << computedForm << "\n"; -// if(ASTFalse == computedForm) -// { -// return ASTFalse; -// } -// } -// else -// { -// if(ASTTrue != currentFormula) -// { -// forloopFormulaVector.push_back(currentFormula); -// } -// } + // return ForloopVec; + // } //end of the SATBased_FiniteLoop_Refinement() + + // //SATBased_FiniteLoop_Refinement_UsingModel(). Expand the finite + // //loop, check against model + // ASTNode + // AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, + // ASTNodeMap* ParamToCurrentValMap, + // bool checkusingmodel_flag = true) + // { + // /* + // * 'finiteloop' is the finite loop to be expanded + // * Every finiteloop has three parts: + // * 0) Parameter Name + // * 1) Parameter initialization + // * 2) Parameter limit value + // * 3) Increment formula + // * 4) Formula Body + // * + // * ParamToCurrentValMap contains a map from parameters to their + // * current values in the recursion + // * + // * Nested FORs are allowed, but only the innermost loop can have a + // * formula in it + // */ + + // //BVTypeCheck should have already checked the sanity of the input + // //FOR-formula + // ASTNode parameter = finiteloop[0]; + // int paramInit = GetUnsignedConst(finiteloop[1]); + // int paramLimit = GetUnsignedConst(finiteloop[2]); + // int paramIncrement = GetUnsignedConst(finiteloop[3]); + // ASTNode exceptFormula = finiteloop[4]; + // ASTNode formulabody = finiteloop[5]; + // int paramCurrentValue = paramInit; + // int width = finiteloop[1].GetValueWidth(); + + // //Update ParamToCurrentValMap with parameter and its current + // //value. Here paramCurrentValue is the initial value + // ASTNode value = + // bm->CreateBVConst(width,paramCurrentValue); + // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); + + // ASTNode ret = ASTTrue; + // ASTVec returnVec; + // //Go recursively thru' all the FOR-constructs. + // if(FOR == formulabody.GetKind()) + // { + // while(paramCurrentValue < paramLimit) + // { + // ret = Check_FiniteLoop_UsingModel(formulabody, + // ParamToCurrentValMap, + // checkusingmodel_flag); + // if(ASTFalse == ret) + // { + // //no more expansion needed. Return immediately + // return ret; + // } + // else + // { + // returnVec.push_back(ret); + // } + + // //Update ParamToCurrentValMap with parameter and its + // //current value. + // paramCurrentValue = paramCurrentValue + paramIncrement; + // value = bm->CreateTerm(BVPLUS, + // width, + // (*ParamToCurrentValMap)[parameter], + // bm->CreateOneConst(width)); + // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); + // } //end of While + + // ASTNode retFormula = + // (returnVec.size() > 1) ? + // bm->CreateNode(AND, returnVec) : + // (returnVec.size() == 1) ? + // returnVec[0] : + // ASTTrue; + // return retFormula; + // } + + // ASTVec forloopFormulaVector; + // //Expand the leaf level FOR-construct completely + // //incrementing of paramCurrentValue is done inside loop + // for(;paramCurrentValue < paramLimit;) + // { + // ASTNode currentFormula; + + // ASTNode currentExceptFormula = exceptFormula; + // currentExceptFormula = + // SimplifyFormula(exceptFormula, false, ParamToCurrentValMap); + // if(ASTTrue == currentExceptFormula) + // { + // currentFormula = ASTTrue; + // //continue; + // } + // else + // { + // currentFormula = + // SimplifyFormula(formulabody, false, ParamToCurrentValMap); + // } + + // if(checkusingmodel_flag) + // { + // //Check the currentformula against the model, and return + // //immediately + // //cout << "Printing current Formula: " << currentFormula << "\n"; + // ASTNode computedForm = ComputeFormulaUsingModel(currentFormula); + // //cout << "Printing computed Formula: " << computedForm << "\n"; + // if(ASTFalse == computedForm) + // { + // return ASTFalse; + // } + // } + // else + // { + // if(ASTTrue != currentFormula) + // { + // forloopFormulaVector.push_back(currentFormula); + // } + // } -// //Update ParamToCurrentValMap with parameter and its current -// //value -// paramCurrentValue = paramCurrentValue + paramIncrement; -// value = bm->CreateTerm(BVPLUS, -// width, -// (*ParamToCurrentValMap)[parameter], -// bm->CreateOneConst(width)); -// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); -// } //end of For - -// if(checkusingmodel_flag) -// { -// return ASTTrue; -// } -// else -// { -// ASTNode retFormula = -// (forloopFormulaVector.size() > 1) ? -// bm->CreateNode(AND, forloopFormulaVector) : -// (forloopFormulaVector.size() == 1) ? -// forloopFormulaVector[0] : -// ASTTrue; -// return retFormula; -// } -// } //end of the Check_FiniteLoop_UsingModel() + // //Update ParamToCurrentValMap with parameter and its current + // //value + // paramCurrentValue = paramCurrentValue + paramIncrement; + // value = bm->CreateTerm(BVPLUS, + // width, + // (*ParamToCurrentValMap)[parameter], + // bm->CreateOneConst(width)); + // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); + // } //end of For + + // if(checkusingmodel_flag) + // { + // return ASTTrue; + // } + // else + // { + // ASTNode retFormula = + // (forloopFormulaVector.size() > 1) ? + // bm->CreateNode(AND, forloopFormulaVector) : + // (forloopFormulaVector.size() == 1) ? + // forloopFormulaVector[0] : + // ASTTrue; + // return retFormula; + // } + // } //end of the Check_FiniteLoop_UsingModel() -// //Expand_FiniteLoop_For_ModelCheck -// ASTNode -// AbsRefine_CounterExample::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop) -// { -// ASTNodeMap ParamToCurrentValMap; -// return Check_FiniteLoop_UsingModel(finiteloop, -// &ParamToCurrentValMap, false); -// } //end of Expand_FiniteLoop_TopLevel() - -// ASTNode -// AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop) -// { -// ASTNodeMap ParamToCurrentValMap; -// return Check_FiniteLoop_UsingModel(finiteloop, -// &ParamToCurrentValMap, true); -// } //end of Check_FiniteLoop_UsingModel + // //Expand_FiniteLoop_For_ModelCheck + // ASTNode + // AbsRefine_CounterExample::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop) + // { + // ASTNodeMap ParamToCurrentValMap; + // return Check_FiniteLoop_UsingModel(finiteloop, + // &ParamToCurrentValMap, false); + // } //end of Expand_FiniteLoop_TopLevel() + + // ASTNode + // AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop) + // { + // ASTNodeMap ParamToCurrentValMap; + // return Check_FiniteLoop_UsingModel(finiteloop, + // &ParamToCurrentValMap, true); + // } //end of Check_FiniteLoop_UsingModel };// end of namespace BEEV diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 7b4c9cf..c429f21 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -54,11 +54,11 @@ namespace BEEV //'v' is the map from bit-index to bit-value HASHMAP * v; if (_ASTNode_to_BitvectorMap.find(symbol) == - _ASTNode_to_BitvectorMap.end()) - { - _ASTNode_to_BitvectorMap[symbol] = - new HASHMAP (symbolWidth); - } + _ASTNode_to_BitvectorMap.end()) + { + _ASTNode_to_BitvectorMap[symbol] = + new HASHMAP (symbolWidth); + } //v holds the map from bit-index to bit-value v = _ASTNode_to_BitvectorMap[symbol]; @@ -100,16 +100,16 @@ namespace BEEV //the the aggregate value of the bitvector, and populate the //CounterExampleMap datastructure for (ASTtoBitvectorMap::iterator it = _ASTNode_to_BitvectorMap.begin(), - itend = _ASTNode_to_BitvectorMap.end(); it != itend; it++) + itend = _ASTNode_to_BitvectorMap.end(); it != itend; it++) { ASTNode var = it->first; //debugging //cerr << var; if (SYMBOL != var.GetKind()) - { - FatalError("ConstructCounterExample:"\ - "error while constructing counterexample: not a variable: ", var); - } + { + FatalError("ConstructCounterExample:"\ + "error while constructing counterexample: not a variable: ", var); + } //construct the bitvector value HASHMAP * w = it->second; ASTNode value = BoolVectoBVConst(w, var.GetValueWidth()); @@ -125,9 +125,9 @@ namespace BEEV //In this loop, we compute the value of each array read, the //corresponding ITE against the counterexample generated above. for (ASTNodeMap::const_iterator - it = ArrayTransform->ArrayRead_IteMap()->begin(), - itend = ArrayTransform->ArrayRead_IteMap()->end(); - it != itend; it++) + it = ArrayTransform->ArrayRead_IteMap()->begin(), + itend = ArrayTransform->ArrayRead_IteMap()->end(); + it != itend; it++) { //the array read ASTNode arrayread = it->first; @@ -139,8 +139,8 @@ namespace BEEV //counterexample ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1]); ASTNode key = bm->CreateTerm(READ, - arrayread.GetValueWidth(), - arrayread[0], arrayread_index); + arrayread.GetValueWidth(), + arrayread[0], arrayread_index); //Get the ITE corresponding to the array-read and convert it //to a constant against the model @@ -427,7 +427,7 @@ namespace BEEV ASTNode writeVal = TermToConstTermUsingModel(write[2], false); ASTNode cond = - ComputeFormulaUsingModel(simp->CreateSimplifiedEQ(writeIndex, readIndex)); + ComputeFormulaUsingModel(simp->CreateSimplifiedEQ(writeIndex, readIndex)); if (ASTTrue == cond) { //found the write-value. return it @@ -497,10 +497,10 @@ namespace BEEV } } else - { - CounterExampleMap[form] = ASTFalse; - output = ASTFalse; - } + { + CounterExampleMap[form] = ASTFalse; + output = ASTFalse; + } break; case EQ: case BVLT: @@ -520,7 +520,7 @@ namespace BEEV //evaluate formula to false if bvdiv execption occurs while //counterexample is being checked during refinement. if (bm->bvdiv_exception_occured - && bm->counterexample_checking_during_refinement) + && bm->counterexample_checking_during_refinement) { output = ASTFalse; } @@ -609,19 +609,19 @@ namespace BEEV output = ComputeFormulaUsingModel(form[2]); else FatalError("ComputeFormulaUsingModel: ITE: "\ - "something is wrong with the formula: ", form); + "something is wrong with the formula: ", form); break; case PARAMBOOL: - output = bm->NewParameterized_BooleanVar(form[0],form[1]); - output = ComputeFormulaUsingModel(output); - break; + output = bm->NewParameterized_BooleanVar(form[0],form[1]); + output = ComputeFormulaUsingModel(output); + break; case FOR: - //output = Check_FiniteLoop_UsingModel(form); - output = ASTTrue; - break; + //output = Check_FiniteLoop_UsingModel(form); + output = ASTTrue; + break; default: FatalError(" ComputeFormulaUsingModel: "\ - "the kind has not been implemented", ASTUndefined); + "the kind has not been implemented", ASTUndefined); break; } @@ -733,30 +733,30 @@ namespace BEEV if (ARRAY_TYPE == se.GetType()) { FatalError("TermToConstTermUsingModel: "\ - "entry in counterexample is an arraytype. bogus:", se); + "entry in counterexample is an arraytype. bogus:", se); } //skip over introduced variables if (f.GetKind() == SYMBOL && - (ArrayTransform->FoundIntroducedSymbolSet(f))) - { - continue; - } + (ArrayTransform->FoundIntroducedSymbolSet(f))) + { + continue; + } if (f.GetKind() == SYMBOL || - (f.GetKind() == READ && - f[0].GetKind() == SYMBOL && - f[1].GetKind() == BVCONST)) + (f.GetKind() == READ && + f[0].GetKind() == SYMBOL && + f[1].GetKind() == BVCONST)) { os << "ASSERT( "; f.PL_Print(os,0); - if(BOOLEAN_TYPE == f.GetType()) - { - os << "<=>"; - } - else - { - os << " = "; - } + if(BOOLEAN_TYPE == f.GetType()) + { + os << "<=>"; + } + else + { + os << " = "; + } if (BITVECTOR_TYPE == se.GetType()) { TermToConstTermUsingModel(se, false).PL_Print(os, 0); @@ -809,7 +809,7 @@ namespace BEEV std::vector out_int; cout << "% "; for (ASTVec::iterator it = bm->ListOfDeclaredVars.begin(), - itend = bm->ListOfDeclaredVars.end(); it != itend; it++) + itend = bm->ListOfDeclaredVars.end(); it != itend; it++) { if (ARRAY_TYPE == it->GetType()) { @@ -902,20 +902,20 @@ namespace BEEV if (!simp->Return_SolverMap()->empty()) { - CounterExampleMap.insert(simp->Return_SolverMap()->begin(), - simp->Return_SolverMap()->end()); + CounterExampleMap.insert(simp->Return_SolverMap()->begin(), + simp->Return_SolverMap()->end()); } } -SOLVER_RETURN_TYPE + SOLVER_RETURN_TYPE AbsRefine_CounterExample:: CallSAT_ResultCheck(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input) + const ASTNode& modified_input, + const ASTNode& original_input) { bool sat = tosat->CallSAT(SatSolver, - modified_input, - original_input); + modified_input, + original_input); if (!sat) { //PrintOutput(true); diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 6c93812..8165b9e 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -140,8 +140,8 @@ VC vc_createValidityChecker(void) { BEEV::ParserBM = bm; stpstar stp = new BEEV::STP(bm, simp, - bvsolver, arrayTransformer, - tosat, Ctr_Example); + bvsolver, arrayTransformer, + tosat, Ctr_Example); BEEV::GlobalSTP = stp; decls = new BEEV::ASTVec(); @@ -893,7 +893,7 @@ Expr vc_bvConstExprFromInt(VC vc, //printf("%ull", max_n_bits); if(v > max_n_bits) { printf("CInterface: vc_bvConstExprFromInt: "\ - "You are trying to construct a constant %llu >= %d,\n", v, max_n_bits); + "You are trying to construct a constant %llu >= %d,\n", v, max_n_bits); BEEV::FatalError("FatalError"); } node n = b->CreateBVConst(n_bits, v); diff --git a/src/extlib-constbv/constantbv.cpp b/src/extlib-constbv/constantbv.cpp index cd05ed3..cdae9c6 100644 --- a/src/extlib-constbv/constantbv.cpp +++ b/src/extlib-constbv/constantbv.cpp @@ -85,38 +85,38 @@ namespace CONSTANTBV { /* global macro definitions: */ /*****************************/ -#define BIT_VECTOR_ZERO_WORDS(target,count) \ - while (count-- > 0) *target++ = 0; +#define BIT_VECTOR_ZERO_WORDS(target,count) \ + while (count-- > 0) *target++ = 0; -#define BIT_VECTOR_FILL_WORDS(target,fill,count) \ - while (count-- > 0) *target++ = fill; +#define BIT_VECTOR_FILL_WORDS(target,fill,count) \ + while (count-- > 0) *target++ = fill; -#define BIT_VECTOR_FLIP_WORDS(target,flip,count) \ - while (count-- > 0) *target++ ^= flip; +#define BIT_VECTOR_FLIP_WORDS(target,flip,count) \ + while (count-- > 0) *target++ ^= flip; -#define BIT_VECTOR_COPY_WORDS(target,source,count) \ - while (count-- > 0) *target++ = *source++; +#define BIT_VECTOR_COPY_WORDS(target,source,count) \ + while (count-- > 0) *target++ = *source++; -#define BIT_VECTOR_BACK_WORDS(target,source,count) \ - { target += count; source += count; while (count-- > 0) *--target = *--source; } +#define BIT_VECTOR_BACK_WORDS(target,source,count) \ + { target += count; source += count; while (count-- > 0) *--target = *--source; } -#define BIT_VECTOR_CLR_BIT(address,index) \ - *(address+(index>>LOGBITS)) &= ~ BITMASKTAB[index & MODMASK]; +#define BIT_VECTOR_CLR_BIT(address,index) \ + *(address+(index>>LOGBITS)) &= ~ BITMASKTAB[index & MODMASK]; -#define BIT_VECTOR_SET_BIT(address,index) \ - *(address+(index>>LOGBITS)) |= BITMASKTAB[index & MODMASK]; +#define BIT_VECTOR_SET_BIT(address,index) \ + *(address+(index>>LOGBITS)) |= BITMASKTAB[index & MODMASK]; -#define BIT_VECTOR_TST_BIT(address,index) \ - ((*(address+(index>>LOGBITS)) & BITMASKTAB[index & MODMASK]) != 0) +#define BIT_VECTOR_TST_BIT(address,index) \ + ((*(address+(index>>LOGBITS)) & BITMASKTAB[index & MODMASK]) != 0) -#define BIT_VECTOR_FLP_BIT(address,index,mask) \ - (mask = BITMASKTAB[index & MODMASK]), \ +#define BIT_VECTOR_FLP_BIT(address,index,mask) \ + (mask = BITMASKTAB[index & MODMASK]), \ (((*(addr+(index>>LOGBITS)) ^= mask) & mask) != 0) -#define BIT_VECTOR_DIGITIZE(type,value,digit) \ - value = (type) ((digit = value) / 10); \ - digit -= value * 10; \ - digit += (type) '0'; +#define BIT_VECTOR_DIGITIZE(type,value,digit) \ + value = (type) ((digit = value) / 10); \ + digit -= value * 10; \ + digit += (type) '0'; /*********************************************************/ /* private low-level functions (potentially dangerous!): */ @@ -142,8 +142,8 @@ namespace CONSTANTBV { unsigned int * source, unsigned int count) { if (target != source) { if (target < source) BIT_VECTOR_COPY_WORDS(target,source,count) - else BIT_VECTOR_BACK_WORDS(target,source,count) - } + else BIT_VECTOR_BACK_WORDS(target,source,count) + } } static void BIT_VECTOR_ins_words(unsigned int * addr, @@ -1537,7 +1537,7 @@ namespace CONSTANTBV { break; case (int) '1': value |= BITMASKTAB[count]; - break; + break; default: ok = false; break; @@ -1907,10 +1907,10 @@ namespace CONSTANTBV { { case (unsigned int) '0': state = 2; - break; + break; case (unsigned int) '\0': state = 0; - break; + break; default: error = ErrCode_Pars; break; @@ -1921,16 +1921,16 @@ namespace CONSTANTBV { { case (unsigned int) '-': start = index; - state = 3; - break; + state = 3; + break; case (unsigned int) ',': BIT_VECTOR_SET_BIT(addr,index) - state = 5; - break; + state = 5; + break; case (unsigned int) '\0': BIT_VECTOR_SET_BIT(addr,index) - state = 0; - break; + state = 0; + break; default: error = ErrCode_Pars; break; @@ -1944,9 +1944,9 @@ namespace CONSTANTBV { BitVector_Interval_Fill(addr,start,index); else if (start == index) BIT_VECTOR_SET_BIT(addr,index) - else error = ErrCode_Ordr; - state = 4; - break; + else error = ErrCode_Ordr; + state = 4; + break; default: error = ErrCode_Pars; break; @@ -1957,10 +1957,10 @@ namespace CONSTANTBV { { case (unsigned int) ',': state = 5; - break; + break; case (unsigned int) '\0': state = 0; - break; + break; default: error = ErrCode_Pars; break; @@ -1971,7 +1971,7 @@ namespace CONSTANTBV { { case (unsigned int) '0': state = 2; - break; + break; default: error = ErrCode_Pars; break; @@ -2012,8 +2012,8 @@ namespace CONSTANTBV { if (index < bits_(addr)) { if (bit) BIT_VECTOR_SET_BIT(addr,index) - else BIT_VECTOR_CLR_BIT(addr,index) - } + else BIT_VECTOR_CLR_BIT(addr,index) + } } void BitVector_LSB(unsigned int * addr, boolean bit) @@ -3398,8 +3398,8 @@ namespace CONSTANTBV { BIT_VECTOR_TST_BIT(Z,indxZ) ) sum ^= 1; } if (sum) BIT_VECTOR_SET_BIT(X,indxX) - else BIT_VECTOR_CLR_BIT(X,indxX) - } + else BIT_VECTOR_CLR_BIT(X,indxX) + } } } } @@ -3439,8 +3439,8 @@ namespace CONSTANTBV { BIT_VECTOR_TST_BIT(Z,indxZ) ) sum |= 1; } if (sum) BIT_VECTOR_SET_BIT(X,indxX) - else BIT_VECTOR_CLR_BIT(X,indxX) - } + else BIT_VECTOR_CLR_BIT(X,indxX) + } } } } diff --git a/src/main/Globals.h b/src/main/Globals.h index eaae76d..33892fc 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -22,8 +22,8 @@ namespace MINISAT { - class Solver; - typedef int Var; + class Solver; + typedef int Var; } namespace BEEV diff --git a/src/main/main.cpp b/src/main/main.cpp index 518d1bf..35b8d9c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -56,11 +56,11 @@ int main(int argc, char ** argv) { ParserBM = bm; GlobalSTP = new STP(bm, - simp, - bvsolver, - arrayTransformer, - tosat, - Ctr_Example); + simp, + bvsolver, + arrayTransformer, + tosat, + Ctr_Example); //populate the help string helpstring += "STP version: " + version + "\n\n"; @@ -107,13 +107,13 @@ int main(int argc, char ** argv) { construct_counterexample_flag = true; check_counterexample_flag = true; break; - case 'e': - expand_finitefor_flag = true; - break; - case 'f': - num_absrefine_flag = true; - num_absrefine = atoi(argv[++i]); - break; + case 'e': + expand_finitefor_flag = true; + break; + case 'f': + num_absrefine_flag = true; + num_absrefine = atoi(argv[++i]); + break; case 'h': fprintf(stderr,usage,prog); cout << helpstring; @@ -139,8 +139,8 @@ int main(int argc, char ** argv) { stats_flag = true; break; case 't': - quick_statistics_flag = true; - break; + quick_statistics_flag = true; + break; case 'u': arraywrite_refinement_flag = false; break; @@ -153,7 +153,7 @@ int main(int argc, char ** argv) { case 'x': xor_flatten_flag = true; break; - case 'y': + case 'y': print_binary_flag = true; break; case 'z': @@ -166,27 +166,27 @@ int main(int argc, char ** argv) { return -1; break; } - } else { - infile = argv[i]; - if (smtlib_parser_flag) - { - smtin = fopen(infile,"r"); - if(smtin == NULL) - { - fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); - FatalError(""); - } - } - else - { - cvcin = fopen(infile,"r"); - if(cvcin == NULL) - { - fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); - FatalError(""); - } - } - } + } else { + infile = argv[i]; + if (smtlib_parser_flag) + { + smtin = fopen(infile,"r"); + if(smtin == NULL) + { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + FatalError(""); + } + } + else + { + cvcin = fopen(infile,"r"); + if(cvcin == NULL) + { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + FatalError(""); + } + } + } } //want to print the output always from the commandline. @@ -215,9 +215,9 @@ int main(int argc, char ** argv) { { if(smtlib_parser_flag) { - // don't pass the query. It's not returned by the smtlib - // parser. - printer::SMTLIB_PrintBack(cout, asserts); + // don't pass the query. It's not returned by the smtlib + // parser. + printer::SMTLIB_PrintBack(cout, asserts); } else { diff --git a/src/parser/let-funcs.h b/src/parser/let-funcs.h index 8a04544..fad5b9b 100644 --- a/src/parser/let-funcs.h +++ b/src/parser/let-funcs.h @@ -15,37 +15,37 @@ namespace BEEV { //LET Management class LETMgr - { - private: + { + private: - // MAP: This map is from bound IDs that occur in LETs to - // expression. The map is useful in checking replacing the IDs - // with the corresponding expressions. - ASTNodeMap *_letid_expr_map; - ASTNode ASTUndefined; + // MAP: This map is from bound IDs that occur in LETs to + // expression. The map is useful in checking replacing the IDs + // with the corresponding expressions. + ASTNodeMap *_letid_expr_map; + ASTNode ASTUndefined; - public: + public: - LETMgr(ASTNode undefined) - { - _letid_expr_map = new ASTNodeMap(); - ASTUndefined = undefined; - } + LETMgr(ASTNode undefined) + { + _letid_expr_map = new ASTNodeMap(); + ASTUndefined = undefined; + } - ASTNode ResolveID(const ASTNode& var); + ASTNode ResolveID(const ASTNode& var); - //Functions that are used to manage LET expressions - void LetExprMgr(const ASTNode& var, const ASTNode& letExpr); + //Functions that are used to manage LET expressions + void LetExprMgr(const ASTNode& var, const ASTNode& letExpr); - //Delete Letid Map - void CleanupLetIDMap(void); + //Delete Letid Map + void CleanupLetIDMap(void); - //Allocate LetID map - void InitializeLetIDMap(void); + //Allocate LetID map + void InitializeLetIDMap(void); - //Substitute Let-vars with LetExprs - ASTNode SubstituteLetExpr(ASTNode inExpr); - };// End of class LETMgr + //Substitute Let-vars with LetExprs + ASTNode SubstituteLetExpr(ASTNode inExpr); + };// End of class LETMgr }; //end of namespace #endif diff --git a/src/printer/AssortedPrinters.cpp b/src/printer/AssortedPrinters.cpp index 1c50b88..a47a967 100644 --- a/src/printer/AssortedPrinters.cpp +++ b/src/printer/AssortedPrinters.cpp @@ -82,11 +82,11 @@ namespace BEEV // } // } //end of PrintClauseList() - // //Variable Order Printer: A global function which converts a MINISAT + // //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) + // int decision_level, int polarity) // { // BEEV::ASTNode vv = BEEV::GlobalSTPMgr->_SATVar_to_AST[minisat_var]; // cout << spaces(decision_level); @@ -103,21 +103,21 @@ namespace BEEV BEEV::ASTNode a = *i; switch(a.GetType()) { case BEEV::BITVECTOR_TYPE: - a.PL_Print(os); - os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl; - break; + a.PL_Print(os); + os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl; + break; case BEEV::ARRAY_TYPE: - a.PL_Print(os); - os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF "; - os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl; - break; + a.PL_Print(os); + os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF "; + os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl; + break; case BEEV::BOOLEAN_TYPE: - a.PL_Print(os); - os << " : BOOLEAN;" << endl; - break; + a.PL_Print(os); + os << " : BOOLEAN;" << endl; + break; default: - BEEV::FatalError("vc_printDeclsToStream: Unsupported type",a); - break; + BEEV::FatalError("vc_printDeclsToStream: Unsupported type",a); + break; } } } //printVarDeclsToStream @@ -125,18 +125,18 @@ namespace BEEV void STPMgr::printAssertsToStream(ostream &os, int simplify_print) { - ASTVec v = GetAsserts(); - for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) { - //Begin_RemoveWrites = true; - //ASTNode q = (simplify_print == 1) ? SimplifyFormula_TopLevel(*i,false) : *i; - //q = (simplify_print == 1) ? SimplifyFormula_TopLevel(q,false) : q; - ASTNode q = *i; - //Begin_RemoveWrites = false; - os << "ASSERT( "; - q.PL_Print(os); - os << ");" << endl; + ASTVec v = GetAsserts(); + for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) { + //Begin_RemoveWrites = true; + //ASTNode q = (simplify_print == 1) ? SimplifyFormula_TopLevel(*i,false) : *i; + //q = (simplify_print == 1) ? SimplifyFormula_TopLevel(q,false) : q; + ASTNode q = *i; + //Begin_RemoveWrites = false; + os << "ASSERT( "; + q.PL_Print(os); + os << ");" << endl; + } } -} void print_STPInput_Back(const ASTNode& asserts, const ASTNode& query) { (BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout); diff --git a/src/printer/PLPrinter.cpp b/src/printer/PLPrinter.cpp index dcc8318..7b6b917 100644 --- a/src/printer/PLPrinter.cpp +++ b/src/printer/PLPrinter.cpp @@ -174,35 +174,35 @@ namespace printer os << endl << "ENDIF"; break; case PARAMBOOL: - PL_Print1(os, c[0], indentation, letize); - os << "("; - PL_Print1(os, c[1], indentation, letize); - os << ")"; - break; + PL_Print1(os, c[0], indentation, letize); + os << "("; + PL_Print1(os, c[1], indentation, letize); + os << ")"; + break; case FOR: - // if(expand_finitefor_flag) - // { - // ASTNode expandedfor = bm->Expand_FiniteLoop_TopLevel(n); - // PL_Print1(os, expandedfor, indentation, letize); - // } - // else - { - os << "FOR("; - PL_Print1(os, c[0], indentation, letize); - os << ";"; - PL_Print1(os, c[1], indentation, letize); - os << ";"; - PL_Print1(os, c[2], indentation, letize); - os << ";"; - PL_Print1(os, c[3], indentation, letize); - os << ";"; - os << "EXCEPT "; - PL_Print1(os, c[4], indentation, letize); - os << "){ \n"; - PL_Print1(os, c[5], indentation, letize); - os << "} \n"; - } - break; + // if(expand_finitefor_flag) + // { + // ASTNode expandedfor = bm->Expand_FiniteLoop_TopLevel(n); + // PL_Print1(os, expandedfor, indentation, letize); + // } + // else + { + os << "FOR("; + PL_Print1(os, c[0], indentation, letize); + os << ";"; + PL_Print1(os, c[1], indentation, letize); + os << ";"; + PL_Print1(os, c[2], indentation, letize); + os << ";"; + PL_Print1(os, c[3], indentation, letize); + os << ";"; + os << "EXCEPT "; + PL_Print1(os, c[4], indentation, letize); + os << "){ \n"; + PL_Print1(os, c[5], indentation, letize); + os << "} \n"; + } + break; case BVLT: case BVLE: case BVGT: diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index 215f37d..485c665 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -12,7 +12,7 @@ // todo : fix lets. // : Finish mapping function names from internal names to SMTLIB names. -// : build proper headers for PrintBack +// : build proper headers for PrintBack // : Letize code for each printer should be merged. namespace printer @@ -27,48 +27,48 @@ namespace printer // Initial version intended to print the whole thing back. void SMTLIB_PrintBack(ostream &os, const ASTNode& n) { - // need to add fake headers into here. - os << "(" << endl; - os << "benchmark blah" << endl; - printVarDeclsToStream(n.GetSTPMgr(),os); - SMTLIB_Print(os, n, 0); - os << ")" << endl; + // need to add fake headers into here. + os << "(" << endl; + os << "benchmark blah" << endl; + printVarDeclsToStream(n.GetSTPMgr(),os); + SMTLIB_Print(os, n, 0); + os << ")" << endl; } void printVarDeclsToStream( const STPMgr* 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. - assert(a.GetKind()== SYMBOL); - - switch(a.GetType()) { - case BEEV::BITVECTOR_TYPE: - - os << ":extrafuns (( "; - a.nodeprint(os); - os << " bv[" << a.GetValueWidth() << "]"; - os << " ))" << endl; - break; - - case BEEV::ARRAY_TYPE: - os << ":extrafuns (( "; - a.nodeprint(os); - os << " Array[" << a.GetIndexWidth(); - os << ":" << a.GetValueWidth() << "] ))" << endl; - break; - case BEEV::BOOLEAN_TYPE: - os << ":extrapred (( "; - a.nodeprint(os); - os << "))" << endl; - break; - default: - BEEV::FatalError("printVarDeclsToStream: Unsupported type",a); - break; - } + for(ASTVec::const_iterator i = mgr->ListOfDeclaredVars.begin(), + iend=mgr->ListOfDeclaredVars.end();i!=iend;i++) { + const BEEV::ASTNode& a = *i; + + // Should be a symbol. + assert(a.GetKind()== SYMBOL); + + switch(a.GetType()) { + case BEEV::BITVECTOR_TYPE: + + os << ":extrafuns (( "; + a.nodeprint(os); + os << " bv[" << a.GetValueWidth() << "]"; + os << " ))" << endl; + break; + + case BEEV::ARRAY_TYPE: + os << ":extrafuns (( "; + a.nodeprint(os); + os << " Array[" << a.GetIndexWidth(); + os << ":" << a.GetValueWidth() << "] ))" << endl; + break; + case BEEV::BOOLEAN_TYPE: + os << ":extrapred (( "; + a.nodeprint(os); + os << "))" << endl; + break; + default: + BEEV::FatalError("printVarDeclsToStream: Unsupported type",a); + break; } - } //printVarDeclsToStream + } + } //printVarDeclsToStream void outputBitVec(const ASTNode n, ostream& os) { diff --git a/src/printer/printers.h b/src/printer/printers.h index b448033..8230bef 100644 --- a/src/printer/printers.h +++ b/src/printer/printers.h @@ -23,18 +23,18 @@ namespace printer ostream& Dot_Print(ostream &os, const BEEV::ASTNode n); ostream& SMTLIB_Print(ostream &os, - const BEEV::ASTNode n, const int indentation = 0); + const BEEV::ASTNode n, const int indentation = 0); ostream& C_Print(ostream &os, - const BEEV::ASTNode n, const int indentation = 0); + const BEEV::ASTNode n, const int indentation = 0); ostream& PL_Print(ostream &os, - const BEEV::ASTNode& n, int indentation=0); + const BEEV::ASTNode& n, int indentation=0); ostream& Lisp_Print(ostream &os, - const BEEV::ASTNode& n, int indentation=0); + const BEEV::ASTNode& n, int indentation=0); ostream& Lisp_Print_indent(ostream &os, - const BEEV::ASTNode& n,int indentation=0); + const BEEV::ASTNode& n,int indentation=0); void SMTLIB_PrintBack(ostream &os, - const BEEV::ASTNode& n ); + const BEEV::ASTNode& n ); } diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index ca8e19b..e9bde34 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -260,19 +260,19 @@ namespace BEEV { ASTNode monom = *it; if (SYMBOL == monom.GetKind() - && Vars.count(monom) == 1 - && !VarSeenInTerm(monom, rhs) - && !DoNotSolveThis(monom) && !chosen_symbol) + && Vars.count(monom) == 1 + && !VarSeenInTerm(monom, rhs) + && !DoNotSolveThis(monom) && !chosen_symbol) { outmonom = monom; chosen_symbol = true; } else if (BVUMINUS == monom.GetKind() - && SYMBOL == monom[0].GetKind() - && Vars.count(monom[0]) == 1 - && !DoNotSolveThis(monom[0]) + && SYMBOL == monom[0].GetKind() + && Vars.count(monom[0]) == 1 + && !DoNotSolveThis(monom[0]) && !VarSeenInTerm(monom[0], rhs) - && !chosen_symbol) + && !chosen_symbol) { //cerr << "Chosen Monom: " << monom << endl; outmonom = monom; @@ -292,23 +292,23 @@ namespace BEEV { ASTNode monom = *it; ASTNode var = - (BVMULT == monom.GetKind()) ? - monom[1] : - _bm->CreateNode(UNDEFINED); + (BVMULT == monom.GetKind()) ? + monom[1] : + _bm->CreateNode(UNDEFINED); if (BVMULT == monom.GetKind() - && BVCONST == monom[0].GetKind() - && _simp->BVConstIsOdd(monom[0]) - && ((SYMBOL == var.GetKind() - && Vars.count(var) == 1) - || (BVEXTRACT == var.GetKind() - && SYMBOL == var[0].GetKind() - && BVCONST == var[1].GetKind() - && zero == var[2] - && !VarSeenInTerm(var[0], rhs) - && !DoNotSolveThis(var[0]))) - && !DoNotSolveThis(var) - && !VarSeenInTerm(var, rhs) + && BVCONST == monom[0].GetKind() + && _simp->BVConstIsOdd(monom[0]) + && ((SYMBOL == var.GetKind() + && Vars.count(var) == 1) + || (BVEXTRACT == var.GetKind() + && SYMBOL == var[0].GetKind() + && BVCONST == var[1].GetKind() + && zero == var[2] + && !VarSeenInTerm(var[0], rhs) + && !DoNotSolveThis(var[0]))) + && !DoNotSolveThis(var) + && !VarSeenInTerm(var, rhs) && !chosen_odd) { //monom[0] is odd. @@ -367,9 +367,9 @@ namespace BEEV //construct: rhs - (lhs without the chosen monom) unsigned int len = lhs.GetValueWidth(); leftover_lhs = - _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS, len, leftover_lhs)); + _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS, len, leftover_lhs)); ASTNode newrhs = - _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs)); + _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs)); lhs = chosen_monom; rhs = newrhs; } //end of if(BVPLUS ...) @@ -435,10 +435,10 @@ namespace BEEV ASTNode zero = _bm->CreateZeroConst(32); if (!(SYMBOL == lhs[0].GetKind() - && BVCONST == lhs[1].GetKind() - && zero == lhs[2] - && !VarSeenInTerm(lhs[0], rhs) - && !DoNotSolveThis(lhs[0]))) + && BVCONST == lhs[1].GetKind() + && zero == lhs[2] + && !VarSeenInTerm(lhs[0], rhs) + && !DoNotSolveThis(lhs[0]))) { return eq; } @@ -459,9 +459,9 @@ namespace BEEV //then also add another entry for x = x1@t ASTNode var = lhs[0]; ASTNode newvar = - _bm->NewVar(var.GetValueWidth() - lhs.GetValueWidth()); + _bm->NewVar(var.GetValueWidth() - lhs.GetValueWidth()); newvar = - _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs); + _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs); _simp->UpdateSolverMap(var, newvar); output = ASTTrue; break; @@ -493,7 +493,7 @@ namespace BEEV ASTNode a = _simp->MultiplicativeInverse(lhs[0]); ASTNode chosenvar = (BVEXTRACT == lhs[1].GetKind()) ? lhs[1][0] : lhs[1]; ASTNode chosenvar_value = - _simp->SimplifyTerm(_bm->CreateTerm(BVMULT, rhs.GetValueWidth(), a, rhs)); + _simp->SimplifyTerm(_bm->CreateTerm(BVMULT, rhs.GetValueWidth(), a, rhs)); //if chosenvar is seen in chosenvar_value then abort if (VarSeenInTerm(chosenvar, chosenvar_value)) @@ -521,11 +521,11 @@ namespace BEEV { ASTNode var = lhs[1][0]; ASTNode newvar = - _bm->NewVar(var.GetValueWidth() - lhs[1].GetValueWidth()); + _bm->NewVar(var.GetValueWidth() - lhs[1].GetValueWidth()); newvar = - _bm->CreateTerm(BVCONCAT, - var.GetValueWidth(), - newvar, chosenvar_value); + _bm->CreateTerm(BVCONCAT, + var.GetValueWidth(), + newvar, chosenvar_value); _simp->UpdateSolverMap(var, newvar); } output = ASTTrue; @@ -727,7 +727,7 @@ namespace BEEV ASTNode aaa = *it; Kind itk = aaa.GetKind(); if (!(BVCONST == itk && !_simp->BVConstIsOdd(aaa)) && !(BVMULT == itk && BVCONST == aaa[0].GetKind() && SYMBOL == aaa[1].GetKind() - && !_simp->BVConstIsOdd(aaa[0]))) + && !_simp->BVConstIsOdd(aaa[0]))) { //If the monomials of the lhs are NOT of the form 'a*x' or 'a' //where 'a' is even, then return the eqn @@ -816,15 +816,15 @@ namespace BEEV bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term) { if (READ == term.GetKind() - && WRITE == term[0].GetKind() - && !_bm->GetRemoveWritesFlag()) + && WRITE == term[0].GetKind() + && !_bm->GetRemoveWritesFlag()) { return false; } if (READ == term.GetKind() - && WRITE == term[0].GetKind() - && _bm->GetRemoveWritesFlag()) + && WRITE == term[0].GetKind() + && _bm->GetRemoveWritesFlag()) { return true; } diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 91048b5..91bd87d 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -39,124 +39,124 @@ namespace BEEV ******************************************************************/ class BVSolver - { - private: - // Ptr to toplevel manager that manages bit-vector expressions - // (i.e. construct various kinds of expressions), and also has - // member functions that simplify bit-vector expressions - STPMgr * _bm; + { + private: + // Ptr to toplevel manager that manages bit-vector expressions + // (i.e. construct various kinds of expressions), and also has + // member functions that simplify bit-vector expressions + STPMgr * _bm; - // Ptr to Simplifier - Simplifier * _simp; - - // - ASTNode ASTTrue, ASTFalse, ASTUndefined; - - //Those formulas which have already been solved. If the same - //formula occurs twice then do not solve the second occurence, and - //instead drop it - ASTNodeMap FormulasAlreadySolvedMap; - - //this map is useful while traversing terms and uniquely - //identifying variables in the those terms. Prevents double - //counting. - ASTNodeMap TermsAlreadySeenMap; - ASTNodeMap TermsAlreadySeenMap_ForArrays; - - //solved variables list: If a variable has been solved for then do - //not solve for it again - ASTNodeSet DoNotSolve_TheseVars; - - //checks if var has been solved for or not. if yes, then return - //true else return false - bool DoNotSolveThis(const ASTNode& var); - - //traverses a term, and creates a multiset of all variables in the - //term. Does memoization to avoid double counting. - void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v); - void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v); - - //choose a suitable var from the term - ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm); - //accepts an equation and solves for a variable or a monom in it - ASTNode BVSolve_Odd(const ASTNode& eq); - - //solves equations of the form a*x=t where 'a' is even. Has a - //return value, unlike the normal BVSolve() - ASTNode BVSolve_Even(const ASTNode& eq); - ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag); - - //Checks for arrayreads in a term. if yes then returns true, else - //return false - bool CheckForArrayReads(const ASTNode& term); - bool CheckForArrayReads_TopLevel(const ASTNode& term); - - //Creates new variables used in solving - ASTNode NewVar(unsigned int n); - - //this function return true if the var occurs in term, else the - //function returns false - bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); - - //takes an even number "in" as input, and returns an odd number - //(return value) and a power of 2 (as number_shifts by reference), - //such that in = (odd_number * power_of_2). - // - //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on - //bit-vector arithmetic published in DAC 1998) paper for precise - //understanding of the algorithm - ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, - unsigned int& number_shifts); - - //Once a formula has been solved, then update the alreadysolvedmap - //with the formula, and the solved value. The solved value can be - //described using the following example: Suppose input to the - //solver is - // - // input key: x = 2 AND y = x + t - // - // output value: y = 2 + t - void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value); - - //This function checks if the key (formula) has already been - //solved for. - // - //If yes it returns TRUE and fills the "output" with the - //solved-value (call by reference argument), - // - //else returns FALSE - bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output); - - public: - //constructor - BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp) - { - ASTTrue = _bm->CreateNode(TRUE); - ASTFalse = _bm->CreateNode(FALSE); - ASTUndefined = _bm->CreateNode(UNDEFINED); - } - ; - - //Destructor - ~BVSolver() - { - TermsAlreadySeenMap.clear(); - DoNotSolve_TheseVars.clear(); - FormulasAlreadySolvedMap.clear(); - TermsAlreadySeenMap_ForArrays.clear(); - } - - //Top Level Solver: Goes over the input DAG, identifies the - //equation to be solved, solves them, - ASTNode TopLevelBVSolve(const ASTNode& a); - - void ClearAllTables(void) - { - DoNotSolve_TheseVars.clear(); - FormulasAlreadySolvedMap.clear(); - TermsAlreadySeenMap_ForArrays.clear(); - } //End of ClearAllTables() - - }; //end of class bvsolver + // Ptr to Simplifier + Simplifier * _simp; + + // + ASTNode ASTTrue, ASTFalse, ASTUndefined; + + //Those formulas which have already been solved. If the same + //formula occurs twice then do not solve the second occurence, and + //instead drop it + ASTNodeMap FormulasAlreadySolvedMap; + + //this map is useful while traversing terms and uniquely + //identifying variables in the those terms. Prevents double + //counting. + ASTNodeMap TermsAlreadySeenMap; + ASTNodeMap TermsAlreadySeenMap_ForArrays; + + //solved variables list: If a variable has been solved for then do + //not solve for it again + ASTNodeSet DoNotSolve_TheseVars; + + //checks if var has been solved for or not. if yes, then return + //true else return false + bool DoNotSolveThis(const ASTNode& var); + + //traverses a term, and creates a multiset of all variables in the + //term. Does memoization to avoid double counting. + void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v); + void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v); + + //choose a suitable var from the term + ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm); + //accepts an equation and solves for a variable or a monom in it + ASTNode BVSolve_Odd(const ASTNode& eq); + + //solves equations of the form a*x=t where 'a' is even. Has a + //return value, unlike the normal BVSolve() + ASTNode BVSolve_Even(const ASTNode& eq); + ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag); + + //Checks for arrayreads in a term. if yes then returns true, else + //return false + bool CheckForArrayReads(const ASTNode& term); + bool CheckForArrayReads_TopLevel(const ASTNode& term); + + //Creates new variables used in solving + ASTNode NewVar(unsigned int n); + + //this function return true if the var occurs in term, else the + //function returns false + bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); + + //takes an even number "in" as input, and returns an odd number + //(return value) and a power of 2 (as number_shifts by reference), + //such that in = (odd_number * power_of_2). + // + //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on + //bit-vector arithmetic published in DAC 1998) paper for precise + //understanding of the algorithm + ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, + unsigned int& number_shifts); + + //Once a formula has been solved, then update the alreadysolvedmap + //with the formula, and the solved value. The solved value can be + //described using the following example: Suppose input to the + //solver is + // + // input key: x = 2 AND y = x + t + // + // output value: y = 2 + t + void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value); + + //This function checks if the key (formula) has already been + //solved for. + // + //If yes it returns TRUE and fills the "output" with the + //solved-value (call by reference argument), + // + //else returns FALSE + bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output); + + public: + //constructor + BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp) + { + ASTTrue = _bm->CreateNode(TRUE); + ASTFalse = _bm->CreateNode(FALSE); + ASTUndefined = _bm->CreateNode(UNDEFINED); + } + ; + + //Destructor + ~BVSolver() + { + TermsAlreadySeenMap.clear(); + DoNotSolve_TheseVars.clear(); + FormulasAlreadySolvedMap.clear(); + TermsAlreadySeenMap_ForArrays.clear(); + } + + //Top Level Solver: Goes over the input DAG, identifies the + //equation to be solved, solves them, + ASTNode TopLevelBVSolve(const ASTNode& a); + + void ClearAllTables(void) + { + DoNotSolve_TheseVars.clear(); + FormulasAlreadySolvedMap.clear(); + TermsAlreadySeenMap_ForArrays.clear(); + } //End of ClearAllTables() + + }; //end of class bvsolver };//end of namespace BEEV #endif diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp index 3779060..6574b2c 100644 --- a/src/simplifier/consteval.cpp +++ b/src/simplifier/consteval.cpp @@ -93,58 +93,58 @@ namespace BEEV break; } - case BVLEFTSHIFT: - case BVRIGHTSHIFT: - case BVSRSHIFT: - { - // load in the bitWidth. - CBV width = CONSTANTBV::BitVector_Create(inputwidth, true); - for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++) - if ((inputwidth & (0x1 << i)) != 0) - CONSTANTBV::BitVector_Bit_On(width, i); - - output = CONSTANTBV::BitVector_Create(inputwidth, true); - - // Number of bits to shift it. - ASTNode shiftNode = BVConstEvaluator(t[1]); - - bool msb = CONSTANTBV::BitVector_msb_(tmp0); - - // If this shift is greater than the bitWidth, make it zero. - if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0) - { - if (k == BVSRSHIFT && msb) - CONSTANTBV::Set_Complement(output, output); - } - else - { - // the shift is destructive, get a copy. - CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth); - - unsigned int shift = GetUnsignedConst(shiftNode); - - if (k == BVLEFTSHIFT) - CONSTANTBV::BitVector_Move_Left(output, shift); - else - CONSTANTBV::BitVector_Move_Right(output, shift); - - if (k == BVSRSHIFT && msb) - { - // signed shift, and the number was originally negative. - // Shift may be larger than the inputwidth. - for (unsigned int i = 0; i < min(shift, inputwidth); i++) - { - CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i)); - } - assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative. - } - } - - OutputNode = _bm->CreateBVConst(output, outputwidth); - - CONSTANTBV::BitVector_Destroy(width); - break; - } + case BVLEFTSHIFT: + case BVRIGHTSHIFT: + case BVSRSHIFT: + { + // load in the bitWidth. + CBV width = CONSTANTBV::BitVector_Create(inputwidth, true); + for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++) + if ((inputwidth & (0x1 << i)) != 0) + CONSTANTBV::BitVector_Bit_On(width, i); + + output = CONSTANTBV::BitVector_Create(inputwidth, true); + + // Number of bits to shift it. + ASTNode shiftNode = BVConstEvaluator(t[1]); + + bool msb = CONSTANTBV::BitVector_msb_(tmp0); + + // If this shift is greater than the bitWidth, make it zero. + if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0) + { + if (k == BVSRSHIFT && msb) + CONSTANTBV::Set_Complement(output, output); + } + else + { + // the shift is destructive, get a copy. + CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth); + + unsigned int shift = GetUnsignedConst(shiftNode); + + if (k == BVLEFTSHIFT) + CONSTANTBV::BitVector_Move_Left(output, shift); + else + CONSTANTBV::BitVector_Move_Right(output, shift); + + if (k == BVSRSHIFT && msb) + { + // signed shift, and the number was originally negative. + // Shift may be larger than the inputwidth. + for (unsigned int i = 0; i < min(shift, inputwidth); i++) + { + CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i)); + } + assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative. + } + } + + OutputNode = _bm->CreateBVConst(output, outputwidth); + + CONSTANTBV::BitVector_Destroy(width); + break; + } case BVAND: diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 2f16073..6d2c29a 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -16,22 +16,22 @@ namespace BEEV ASTNode Simplifier::Flatten(const ASTNode& a) { - ASTNode n = a; - while (true) - { - ASTNode& nold = n; - n = FlattenOneLevel(n); - if ((n == nold)) - break; - } - - return n; + ASTNode n = a; + while (true) + { + ASTNode& nold = n; + n = FlattenOneLevel(n); + if ((n == nold)) + break; + } + + return n; } bool Simplifier::CheckMap(ASTNodeMap* VarConstMap, - const ASTNode& key, ASTNode& output) + const ASTNode& key, ASTNode& output) { if(NULL == VarConstMap) { @@ -48,12 +48,12 @@ namespace BEEV bool Simplifier::CheckSimplifyMap(const ASTNode& key, - ASTNode& output, - bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode& output, + bool pushNeg, ASTNodeMap* VarConstMap) { if(NULL != VarConstMap) { - return false; + return false; } ASTNodeMap::iterator it, itend; it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key); @@ -82,12 +82,12 @@ namespace BEEV // Push any reference count used by the key to the value. void Simplifier::UpdateSimplifyMap(const ASTNode& key, - const ASTNode& value, - bool pushNeg, ASTNodeMap* VarConstMap) + const ASTNode& value, + bool pushNeg, ASTNodeMap* VarConstMap) { if(NULL != VarConstMap) { - return; + return; } // Don't add leaves. Leaves are easy to recalculate, no need @@ -147,8 +147,8 @@ namespace BEEV if (1 == i && !CheckSubstitutionMap(e0)) { assert((e1.GetKind() == TRUE) || - (e1.GetKind() == FALSE) || - (e1.GetKind() == BVCONST)); + (e1.GetKind() == FALSE) || + (e1.GetKind() == BVCONST)); (*SolverMap)[e0] = e1; return true; } @@ -158,8 +158,8 @@ namespace BEEV if (-1 == i && !CheckSubstitutionMap(e1)) { assert((e0.GetKind() == TRUE) || - (e0.GetKind() == FALSE) || - (e0.GetKind() == BVCONST)); + (e0.GetKind() == FALSE) || + (e0.GetKind() == BVCONST)); (*SolverMap)[e1] = e0; return true; } @@ -205,7 +205,7 @@ namespace BEEV ASTNode Simplifier::SimplifyFormula_NoRemoveWrites(const ASTNode& b, - bool pushNeg, ASTNodeMap* VarConstMap) + bool pushNeg, ASTNodeMap* VarConstMap) { _bm->Begin_RemoveWrites = false; ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); @@ -242,48 +242,48 @@ namespace BEEV // The SimplifyMaps on entry to the topLevel functions may contain useful entries. // E.g. The BVSolver calls SimplifyTerm() ASTNode Simplifier::SimplifyFormula_TopLevel(const ASTNode& b, - bool pushNeg, ASTNodeMap* VarConstMap) + bool pushNeg, ASTNodeMap* VarConstMap) { _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); if (smtlib_parser_flag) - BuildReferenceCountMap(b); + BuildReferenceCountMap(b); ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); ResetSimplifyMaps(); _bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel); return out; } -ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) -{ - _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); - ASTNode out = SimplifyTerm(b); - ResetSimplifyMaps(); - _bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel); - return out; -} + ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) + { + _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); + ASTNode out = SimplifyTerm(b); + ResetSimplifyMaps(); + _bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel); + return out; + } ASTNode Simplifier::SimplifyFormula(const ASTNode& b, - bool pushNeg, ASTNodeMap* VarConstMap) + bool pushNeg, ASTNodeMap* VarConstMap) { -// if (!optimize_flag) -// return b; + // if (!optimize_flag) + // return b; Kind kind = b.GetKind(); if (BOOLEAN_TYPE != b.GetType()) { FatalError(" SimplifyFormula: "\ - "You have input a nonformula kind: ", ASTUndefined, kind); + "You have input a nonformula kind: ", ASTUndefined, kind); } ASTNode a = b; ASTVec ca = a.GetChildren(); if (!(IMPLIES == kind || - ITE == kind || - FOR == kind || - PARAMBOOL==kind || - isAtomic(kind))) + ITE == kind || + FOR == kind || + PARAMBOOL==kind || + isAtomic(kind))) { SortByArith(ca); a = _bm->CreateNode(kind, ca); @@ -340,7 +340,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) ASTNode Simplifier::SimplifyForFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap) + bool pushNeg, ASTNodeMap* VarConstMap) { //FIXME: Code this up properly later. Mainly pushing the negation //down @@ -349,10 +349,10 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) ASTNode Simplifier::SimplifyAtomicFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap) + bool pushNeg, ASTNodeMap* VarConstMap) { -// if (!optimize_flag) -// return a; + // if (!optimize_flag) + // return a; ASTNode output; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) @@ -388,12 +388,12 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) output = pushNeg ? _bm->CreateNode(NOT, output) : output; break; case PARAMBOOL: - { - ASTNode term = SimplifyTerm(a[1], VarConstMap); - output = _bm->CreateNode(PARAMBOOL, a[0], term); - output = pushNeg ? _bm->CreateNode(NOT, output) : output; - break; - } + { + ASTNode term = SimplifyTerm(a[1], VarConstMap); + output = _bm->CreateNode(PARAMBOOL, a[0], term); + output = pushNeg ? _bm->CreateNode(NOT, output) : output; + break; + } case BVGETBIT: { ASTNode term = SimplifyTerm(a[0], VarConstMap); @@ -401,7 +401,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) ASTNode zero = _bm->CreateZeroConst(1); ASTNode one = _bm->CreateOneConst(1); ASTNode getthebit = - SimplifyTerm(_bm->CreateTerm(BVEXTRACT, 1, term, thebit, thebit), VarConstMap); + SimplifyTerm(_bm->CreateTerm(BVEXTRACT, 1, term, thebit, thebit), VarConstMap); if (getthebit == zero) output = pushNeg ? ASTTrue : ASTFalse; else if (getthebit == one) @@ -442,7 +442,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) } default: FatalError("SimplifyAtomicFormula: "\ - "NO atomic formula of the kind: ", ASTUndefined, kind); + "NO atomic formula of the kind: ", ASTUndefined, kind); break; } @@ -452,8 +452,8 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) } //end of SimplifyAtomicFormula() ASTNode Simplifier::CreateSimplifiedINEQ(Kind k, - const ASTNode& left, - const ASTNode& right, bool pushNeg) + const ASTNode& left, + const ASTNode& right, bool pushNeg) { ASTNode output; if (BVCONST == left.GetKind() && BVCONST == right.GetKind()) @@ -486,9 +486,9 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) else { output = - pushNeg ? - _bm->CreateNode(BVLE, right, left) : - _bm->CreateNode(BVLT, left, right); + pushNeg ? + _bm->CreateNode(BVLE, right, left) : + _bm->CreateNode(BVLT, left, right); } break; case BVLE: @@ -512,9 +512,9 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) else { output = - pushNeg ? - _bm->CreateNode(BVLT, right, left) : - _bm->CreateNode(BVLE, left, right); + pushNeg ? + _bm->CreateNode(BVLT, right, left) : + _bm->CreateNode(BVLE, left, right); } break; case BVGT: @@ -529,9 +529,9 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) else { output = - pushNeg ? - _bm->CreateNode(BVLE, left, right) : - _bm->CreateNode(BVLT, right, left); + pushNeg ? + _bm->CreateNode(BVLE, left, right) : + _bm->CreateNode(BVLT, right, left); } break; case BVGE: @@ -546,9 +546,9 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) else { output = - pushNeg ? - _bm->CreateNode(BVLT, left, right) : - _bm->CreateNode(BVLE, right, left); + pushNeg ? + _bm->CreateNode(BVLT, left, right) : + _bm->CreateNode(BVLE, right, left); } break; case BVSLT: @@ -584,7 +584,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) { if (BVLT != in[j].GetKind()) continue; - // parameters are swapped. + // parameters are swapped. if (in[i][0] == in[j][1] && in[i][1] == in[j][0]) return ASTFalse; } @@ -667,8 +667,8 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) output = ASTFalse; } else if (ITE == k1 && - BVCONST == in1[1].GetKind() && - BVCONST == in1[2].GetKind() && BVCONST == k2) + BVCONST == in1[1].GetKind() && + BVCONST == in1[2].GetKind() && BVCONST == k2) { //if one side is a BVCONST and the other side is an ITE over //BVCONST then we can do the following optimization: @@ -698,8 +698,8 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) } } else if (ITE == k2 && - BVCONST == in2[1].GetKind() && - BVCONST == in2[2].GetKind() && BVCONST == k1) + BVCONST == in2[1].GetKind() && + BVCONST == in2[2].GetKind() && BVCONST == k1) { ASTNode cond = in2[0]; if (in2[1] == in1) @@ -756,8 +756,8 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) //accepts cond == t1, then part is t2, and else part is t3 ASTNode Simplifier::CreateSimplifiedTermITE(const ASTNode& in0, - const ASTNode& in1, - const ASTNode& in2) + const ASTNode& in1, + const ASTNode& in2) { ASTNode t0 = in0; ASTNode t1 = in1; @@ -769,13 +769,13 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) { cerr << "t2 is : = " << t2; FatalError("CreateSimplifiedTermITE: "\ - "the lengths of the two branches don't match", t1); + "the lengths of the two branches don't match", t1); } if (t1.GetIndexWidth() != t2.GetIndexWidth()) { cerr << "t2 is : = " << t2; FatalError("CreateSimplifiedTermITE: "\ - "the lengths of the two branches don't match", t1); + "the lengths of the two branches don't match", t1); } return _bm->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2); } @@ -915,10 +915,10 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) default: { output = - (isAnd) ? (pushNeg ? - _bm->CreateNode(OR, outvec) : - _bm->CreateNode(AND, outvec)) : - (pushNeg ? _bm->CreateNode(AND, outvec) : _bm->CreateNode(OR,outvec)); + (isAnd) ? (pushNeg ? + _bm->CreateNode(OR, outvec) : + _bm->CreateNode(AND, outvec)) : + (pushNeg ? _bm->CreateNode(AND, outvec) : _bm->CreateNode(OR,outvec)); //output = FlattenOneLevel(output); break; } @@ -937,7 +937,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) ASTNode Simplifier::SimplifyNotFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap) + bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) @@ -1110,8 +1110,8 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) output = c1; } else if (CheckAlwaysTrueFormMap(c1) || - CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, c0)) || - (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0]))) + CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, c0)) || + (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0]))) { //(~c0 AND (~c0 OR c1)) <==> TRUE // @@ -1119,7 +1119,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) output = ASTTrue; } else if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, c1)) || - (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0]))) + (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0]))) { //(~c1 AND c0->c1) <==> (~c1 AND ~c1->~c0) <==> ~c0 //(c1 AND c0->~c1) <==> (c1 AND c1->~c0) <==> ~c0 @@ -1212,8 +1212,8 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) ASTNode Simplifier::SimplifyIteFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { - // if (!optimize_flag) -// return b; + // if (!optimize_flag) + // return b; ASTNode output; if (CheckSimplifyMap(b, output, pushNeg, VarConstMap)) @@ -1277,7 +1277,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) output = t1; } else if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, t0)) || - (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) + (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) { output = t2; } @@ -1444,8 +1444,8 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) } CONSTANTBV::BitVector_increment(maskedPlusOne); ASTNode temp = - _bm->CreateTerm(BVMULT, inputValueWidth, - _bm->CreateBVConst(maskedPlusOne, inputValueWidth), other); + _bm->CreateTerm(BVMULT, inputValueWidth, + _bm->CreateBVConst(maskedPlusOne, inputValueWidth), other); output = _bm->CreateTerm(BVNEG, inputValueWidth, temp); } } @@ -1552,27 +1552,27 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) // propagate bvuminus upwards through multiplies. if (BVMULT == output.GetKind()) - { - ASTVec d = output.GetChildren(); - int uminus = 0; - for (unsigned i = 0; i < d.size(); i++) - { - if (d[i].GetKind() == BVUMINUS) - { - d[i] = d[i][0]; - uminus++; - } - } - if (uminus != 0) - { - SortByArith(d); - output = _bm->CreateTerm(BVMULT, output.GetValueWidth(), d); - if ((uminus & 0x1) != 0) // odd, pull up the uminus. - { - output = _bm->CreateTerm(BVUMINUS, output.GetValueWidth(), output); - } - } - } + { + ASTVec d = output.GetChildren(); + int uminus = 0; + for (unsigned i = 0; i < d.size(); i++) + { + if (d[i].GetKind() == BVUMINUS) + { + d[i] = d[i][0]; + uminus++; + } + } + if (uminus != 0) + { + SortByArith(d); + output = _bm->CreateTerm(BVMULT, output.GetValueWidth(), d); + if ((uminus & 0x1) != 0) // odd, pull up the uminus. + { + output = _bm->CreateTerm(BVUMINUS, output.GetValueWidth(), output); + } + } + } @@ -1644,17 +1644,17 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) } else { - // If the first argument to the multiply is a constant, push it through. - // Without regard for the splitting of nodes (hmm.) - // This is necessary because the bitvector solver can process -3*x, but - // not -(3*x). - if (BVCONST == a0[0].GetKind()) - { - ASTNode a00 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[0]), VarConstMap); - output = _bm->CreateTerm(BVMULT, l, a00, a0[1]); - } - else - output = _bm->CreateTerm(BVUMINUS, l, a0); + // If the first argument to the multiply is a constant, push it through. + // Without regard for the splitting of nodes (hmm.) + // This is necessary because the bitvector solver can process -3*x, but + // not -(3*x). + if (BVCONST == a0[0].GetKind()) + { + ASTNode a00 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[0]), VarConstMap); + output = _bm->CreateTerm(BVMULT, l, a00, a0[1]); + } + else + output = _bm->CreateTerm(BVUMINUS, l, a0); } break; } @@ -2042,62 +2042,62 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) case BVLEFTSHIFT: - case BVRIGHTSHIFT: - - { // If the shift amount is known. Then replace it by an extract. - ASTNode a = SimplifyTerm(inputterm[0], VarConstMap); - ASTNode b = SimplifyTerm(inputterm[1], VarConstMap); - const unsigned int width = a.GetValueWidth(); - if (BVCONST == b.GetKind()) // known shift amount. - { - if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) - { - // Intended to remove shifts by very large amounts that don't fit into the unsigned. - // at thhe start of the "else" branch. - output = _bm->CreateZeroConst(width); - } - else - { - const unsigned int shift = GetUnsignedConst(b); - if (shift > width) - { - output = _bm->CreateZeroConst(width); - } - else if (shift == 0) - { - output = a; // unchanged. - } - else - { - if (k == BVLEFTSHIFT) - { - ASTNode zero = _bm->CreateZeroConst(shift); - ASTNode hi = _bm->CreateBVConst(32, width - shift -1); - ASTNode low = _bm->CreateBVConst(32, 0); - ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low); - BVTypeCheck(extract); - output = _bm->CreateTerm(BVCONCAT, width, extract, zero); - BVTypeCheck(output); - } - else if (k == BVRIGHTSHIFT) - { - ASTNode zero = _bm->CreateZeroConst(shift); - ASTNode hi = _bm->CreateBVConst(32, width -1); - ASTNode low = _bm->CreateBVConst(32, shift); - ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low); - BVTypeCheck(extract); - output = _bm->CreateTerm(BVCONCAT, width, zero, extract); - BVTypeCheck(output); - } - else - FatalError("herasdf"); - } - } - } - else - output = _bm->CreateTerm(k, width, a, b); - } - break; + case BVRIGHTSHIFT: + + { // If the shift amount is known. Then replace it by an extract. + ASTNode a = SimplifyTerm(inputterm[0], VarConstMap); + ASTNode b = SimplifyTerm(inputterm[1], VarConstMap); + const unsigned int width = a.GetValueWidth(); + if (BVCONST == b.GetKind()) // known shift amount. + { + if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) + { + // Intended to remove shifts by very large amounts that don't fit into the unsigned. + // at thhe start of the "else" branch. + output = _bm->CreateZeroConst(width); + } + else + { + const unsigned int shift = GetUnsignedConst(b); + if (shift > width) + { + output = _bm->CreateZeroConst(width); + } + else if (shift == 0) + { + output = a; // unchanged. + } + else + { + if (k == BVLEFTSHIFT) + { + ASTNode zero = _bm->CreateZeroConst(shift); + ASTNode hi = _bm->CreateBVConst(32, width - shift -1); + ASTNode low = _bm->CreateBVConst(32, 0); + ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low); + BVTypeCheck(extract); + output = _bm->CreateTerm(BVCONCAT, width, extract, zero); + BVTypeCheck(output); + } + else if (k == BVRIGHTSHIFT) + { + ASTNode zero = _bm->CreateZeroConst(shift); + ASTNode hi = _bm->CreateBVConst(32, width -1); + ASTNode low = _bm->CreateBVConst(32, shift); + ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low); + BVTypeCheck(extract); + output = _bm->CreateTerm(BVCONCAT, width, zero, extract); + BVTypeCheck(output); + } + else + FatalError("herasdf"); + } + } + } + else + output = _bm->CreateTerm(k, width, a, b); + } + break; case BVXOR: @@ -2669,14 +2669,14 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) } if (!_bm->Begin_RemoveWrites - && !_bm->SimplifyWrites_InPlace_Flag - && !_bm->start_abstracting) + && !_bm->SimplifyWrites_InPlace_Flag + && !_bm->start_abstracting) { return term; } else if (!_bm->Begin_RemoveWrites - && _bm->SimplifyWrites_InPlace_Flag - && !_bm->start_abstracting) + && _bm->SimplifyWrites_InPlace_Flag + && !_bm->start_abstracting) { //return term; return SimplifyWrites_InPlace(term); @@ -2788,7 +2788,7 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) } if (!_bm->start_abstracting - && _bm->Begin_RemoveWrites) + && _bm->Begin_RemoveWrites) { output = ReadOverWrite_To_ITE(input); } @@ -3032,16 +3032,16 @@ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) ReferenceCount = new ASTNodeCountMap(); } -void Simplifier::printCacheStatus() -{ - cerr << SimplifyMap->size() << endl; - cerr << SimplifyNegMap->size() << endl; - cerr << ReferenceCount->size() << endl; - //cerr << TermsAlreadySeenMap.size() << endl; + void Simplifier::printCacheStatus() + { + cerr << SimplifyMap->size() << endl; + cerr << SimplifyNegMap->size() << endl; + cerr << ReferenceCount->size() << endl; + //cerr << TermsAlreadySeenMap.size() << endl; - cerr << SimplifyMap->bucket_count() << endl; - cerr << SimplifyNegMap->bucket_count() << endl; - cerr << ReferenceCount->bucket_count() << endl; - //cerr << TermsAlreadySeenMap.bucket_count() << endl; -} //printCacheStatus() + cerr << SimplifyMap->bucket_count() << endl; + cerr << SimplifyNegMap->bucket_count() << endl; + cerr << ReferenceCount->bucket_count() << endl; + //cerr << TermsAlreadySeenMap.bucket_count() << endl; + } //printCacheStatus() };//end of namespace diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 9e602db..be35163 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -16,243 +16,243 @@ namespace BEEV { class Simplifier - { - friend class counterexample; - private: - - /**************************************************************** - * Private Data and TypeDefs * - ****************************************************************/ - - // Handy defs - ASTNode ASTTrue, ASTFalse, ASTUndefined; - - // Memo table for simplifcation. Key is unsimplified node, and - // value is simplified node. - ASTNodeMap * SimplifyMap; - ASTNodeMap * SimplifyNegMap; - ASTNodeMap * SolverMap; - ASTNodeSet AlwaysTrueFormMap; - ASTNodeMap MultInverseMap; - - // For ArrayWrite Abstraction: map from read-over-write term to - // newname. - ASTNodeMap * ReadOverWrite_NewName_Map; + { + friend class counterexample; + private: + + /**************************************************************** + * Private Data and TypeDefs * + ****************************************************************/ + + // Handy defs + ASTNode ASTTrue, ASTFalse, ASTUndefined; + + // Memo table for simplifcation. Key is unsimplified node, and + // value is simplified node. + ASTNodeMap * SimplifyMap; + ASTNodeMap * SimplifyNegMap; + ASTNodeMap * SolverMap; + ASTNodeSet AlwaysTrueFormMap; + ASTNodeMap MultInverseMap; + + // For ArrayWrite Abstraction: map from read-over-write term to + // newname. + ASTNodeMap * ReadOverWrite_NewName_Map; - // For ArrayWrite Refinement: Map new arraynames to - // Read-Over-Write terms - ASTNodeMap NewName_ReadOverWrite_Map; + // For ArrayWrite Refinement: Map new arraynames to + // Read-Over-Write terms + ASTNodeMap NewName_ReadOverWrite_Map; - // The number of direct parents of each node. i.e. the number - // of times the pointer is in "children". When we simplify we - // want to be careful sometimes about using the context of a - // node. For example, given ((x + 23) = 2), the obvious - // simplification is to join the constants. However, if there - // are lots of references to the plus node. Then each time we - // simplify, we'll create an additional plus. - // nextpoweroftwo064.smt is the motivating benchmark. The - // splitting increased the number of pluses from 1 to 65. - ASTNodeCountMap *ReferenceCount; + // The number of direct parents of each node. i.e. the number + // of times the pointer is in "children". When we simplify we + // want to be careful sometimes about using the context of a + // node. For example, given ((x + 23) = 2), the obvious + // simplification is to join the constants. However, if there + // are lots of references to the plus node. Then each time we + // simplify, we'll create an additional plus. + // nextpoweroftwo064.smt is the motivating benchmark. The + // splitting increased the number of pluses from 1 to 65. + ASTNodeCountMap *ReferenceCount; - //Ptr to STP Manager - STPMgr * _bm; + //Ptr to STP Manager + STPMgr * _bm; - public: + public: - /**************************************************************** - * Public Member Functions * - ****************************************************************/ - Simplifier(STPMgr * bm) : _bm(bm) - { - SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - ReadOverWrite_NewName_Map = new ASTNodeMap(INITIAL_TABLE_SIZE); - ReferenceCount = new ASTNodeCountMap(INITIAL_TABLE_SIZE); - - ASTTrue = bm->CreateNode(TRUE); - ASTFalse = bm->CreateNode(FALSE); - ASTUndefined = bm->CreateNode(UNDEFINED); - } + /**************************************************************** + * Public Member Functions * + ****************************************************************/ + Simplifier(STPMgr * bm) : _bm(bm) + { + SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE); + SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE); + SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); + ReadOverWrite_NewName_Map = new ASTNodeMap(INITIAL_TABLE_SIZE); + ReferenceCount = new ASTNodeCountMap(INITIAL_TABLE_SIZE); + + ASTTrue = bm->CreateNode(TRUE); + ASTFalse = bm->CreateNode(FALSE); + ASTUndefined = bm->CreateNode(UNDEFINED); + } - ~Simplifier() - { - delete SimplifyMap; - delete SimplifyNegMap; - delete ReferenceCount; - } - - /**************************************************************** - * Functions to check and update various Maps * - ****************************************************************/ + ~Simplifier() + { + delete SimplifyMap; + delete SimplifyNegMap; + delete ReferenceCount; + } + + /**************************************************************** + * Functions to check and update various Maps * + ****************************************************************/ - //Check the map passed to SimplifyTerm - bool CheckMap(ASTNodeMap* VarConstMap, - const ASTNode& key, ASTNode& output); - - //substitution - bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); - bool CheckSubstitutionMap(const ASTNode& a); - bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); + //Check the map passed to SimplifyTerm + bool CheckMap(ASTNodeMap* VarConstMap, + const ASTNode& key, ASTNode& output); + + //substitution + bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); + bool CheckSubstitutionMap(const ASTNode& a); + bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); - //functions for checking and updating simplifcation map - bool CheckSimplifyMap(const ASTNode& key, - ASTNode& output, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); - void UpdateSimplifyMap(const ASTNode& key, - const ASTNode& value, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); - bool CheckAlwaysTrueFormMap(const ASTNode& key); - void UpdateAlwaysTrueFormMap(const ASTNode& val); - bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); - void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); + //functions for checking and updating simplifcation map + bool CheckSimplifyMap(const ASTNode& key, + ASTNode& output, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); + void UpdateSimplifyMap(const ASTNode& key, + const ASTNode& value, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); + bool CheckAlwaysTrueFormMap(const ASTNode& key); + void UpdateAlwaysTrueFormMap(const ASTNode& val); + bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); + void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); - //Map for solved variables - bool CheckSolverMap(const ASTNode& a, ASTNode& output); - bool CheckSolverMap(const ASTNode& a); - bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); + //Map for solved variables + bool CheckSolverMap(const ASTNode& a, ASTNode& output); + bool CheckSolverMap(const ASTNode& a); + bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); - void ResetSimplifyMaps(void); + void ResetSimplifyMaps(void); - /**************************************************************** - * Simplification functions * - ****************************************************************/ + /**************************************************************** + * Simplification functions * + ****************************************************************/ - ASTNode SimplifyFormula_TopLevel(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyFormula_TopLevel(const ASTNode& a, + bool pushNeg, + ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyTerm_TopLevel(const ASTNode& b); + ASTNode SimplifyTerm_TopLevel(const ASTNode& b); - ASTNode SimplifyFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyFormula(const ASTNode& a, + bool pushNeg, + ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyTerm(const ASTNode& inputterm, - ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyTerm(const ASTNode& inputterm, + ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, + bool pushNeg, + ASTNodeMap* VarConstMap=NULL); - void CheckSimplifyInvariant(const ASTNode& a, - const ASTNode& output); + void CheckSimplifyInvariant(const ASTNode& a, + const ASTNode& output); - void BuildReferenceCountMap(const ASTNode& b); + void BuildReferenceCountMap(const ASTNode& b); - ASTNode SimplifyAtomicFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyAtomicFormula(const ASTNode& a, + bool pushNeg, + ASTNodeMap* VarConstMap=NULL); - ASTNode CreateSimplifiedEQ(const ASTNode& t1, - const ASTNode& t2); + ASTNode CreateSimplifiedEQ(const ASTNode& t1, + const ASTNode& t2); - ASTNode ITEOpt_InEqs(const ASTNode& in1, - ASTNodeMap* VarConstMap=NULL); + ASTNode ITEOpt_InEqs(const ASTNode& in1, + ASTNodeMap* VarConstMap=NULL); - ASTNode PullUpITE(const ASTNode& in); + ASTNode PullUpITE(const ASTNode& in); - ASTNode RemoveContradictionsFromAND(const ASTNode& in); + ASTNode RemoveContradictionsFromAND(const ASTNode& in); - ASTNode CreateSimplifiedTermITE(const ASTNode& t1, - const ASTNode& t2, - const ASTNode& t3); + ASTNode CreateSimplifiedTermITE(const ASTNode& t1, + const ASTNode& t2, + const ASTNode& t3); - ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0, - const ASTNode& in1, - const ASTNode& in2); + ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0, + const ASTNode& in1, + const ASTNode& in2); - ASTNode CreateSimplifiedINEQ(Kind k, - const ASTNode& a0, - const ASTNode& a1, bool pushNeg); + ASTNode CreateSimplifiedINEQ(Kind k, + const ASTNode& a0, + const ASTNode& a1, bool pushNeg); - ASTNode SimplifyNotFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyNotFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyAndOrFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyAndOrFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyXorFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyXorFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyNandFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyNandFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyNorFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyNorFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyImpliesFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyImpliesFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyIffFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyIffFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyIteFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyIteFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyForFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyForFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode Flatten(const ASTNode& a); + ASTNode Flatten(const ASTNode& a); - ASTNode FlattenOneLevel(const ASTNode& a); + ASTNode FlattenOneLevel(const ASTNode& a); - ASTNode FlattenAndOr(const ASTNode& a); + ASTNode FlattenAndOr(const ASTNode& a); - ASTNode CombineLikeTerms(const ASTNode& a); + ASTNode CombineLikeTerms(const ASTNode& a); - ASTNode LhsMinusRhs(const ASTNode& eq); + ASTNode LhsMinusRhs(const ASTNode& eq); - ASTNode DistributeMultOverPlus(const ASTNode& a, - bool startdistribution = false); + ASTNode DistributeMultOverPlus(const ASTNode& a, + bool startdistribution = false); - ASTNode ConvertBVSXToITE(const ASTNode& a); + ASTNode ConvertBVSXToITE(const ASTNode& a); - //accepts constant term and simplifies it to a bvconst - ASTNode BVConstEvaluator(const ASTNode& t); + //accepts constant term and simplifies it to a bvconst + ASTNode BVConstEvaluator(const ASTNode& t); - //checks if the input constant is odd or not - bool BVConstIsOdd(const ASTNode& c); + //checks if the input constant is odd or not + bool BVConstIsOdd(const ASTNode& c); - //computes the multiplicatve inverse of the input - ASTNode MultiplicativeInverse(const ASTNode& c); + //computes the multiplicatve inverse of the input + ASTNode MultiplicativeInverse(const ASTNode& c); - //Replaces WRITE(Arr,i,val) with ITE(j=i, val, READ(Arr,j)) - ASTNode RemoveWrites_TopLevel(const ASTNode& term); - ASTNode RemoveWrites(const ASTNode& term); - ASTNode SimplifyWrites_InPlace(const ASTNode& term, - ASTNodeMap* VarConstMap=NULL); - ASTNode ReadOverWrite_To_ITE(const ASTNode& term, - ASTNodeMap* VarConstMap=NULL); + //Replaces WRITE(Arr,i,val) with ITE(j=i, val, READ(Arr,j)) + ASTNode RemoveWrites_TopLevel(const ASTNode& term); + ASTNode RemoveWrites(const ASTNode& term); + ASTNode SimplifyWrites_InPlace(const ASTNode& term, + ASTNodeMap* VarConstMap=NULL); + ASTNode ReadOverWrite_To_ITE(const ASTNode& term, + ASTNodeMap* VarConstMap=NULL); - void printCacheStatus(); + void printCacheStatus(); - //FIXME: Get rid of this horrible function - const ASTNodeMap * ReadOverWriteMap() - { - return ReadOverWrite_NewName_Map; - } // End of ReadOverWriteMap() + //FIXME: Get rid of this horrible function + const ASTNodeMap * ReadOverWriteMap() + { + return ReadOverWrite_NewName_Map; + } // End of ReadOverWriteMap() - const ASTNodeMap * Return_SolverMap() - { - return SolverMap; - } // End of SolverMap() - - void ClearAllTables(void) - { - SimplifyMap->clear(); - SimplifyNegMap->clear(); - SolverMap->clear(); - ReadOverWrite_NewName_Map->clear(); - NewName_ReadOverWrite_Map.clear(); - AlwaysTrueFormMap.clear(); - MultInverseMap.clear(); - ReferenceCount->clear(); - } - };//end of class Simplifier + const ASTNodeMap * Return_SolverMap() + { + return SolverMap; + } // End of SolverMap() + + void ClearAllTables(void) + { + SimplifyMap->clear(); + SimplifyNegMap->clear(); + SolverMap->clear(); + ReadOverWrite_NewName_Map->clear(); + NewName_ReadOverWrite_Map.clear(); + AlwaysTrueFormMap.clear(); + MultInverseMap.clear(); + ReferenceCount->clear(); + } + };//end of class Simplifier }; //end of namespace #endif diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index 974ed67..6f96c17 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -61,78 +61,78 @@ namespace BEEV break; } - case BVRIGHTSHIFT: - case BVSRSHIFT: - case BVLEFTSHIFT: - { - // Barrel shifter - const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren(); - const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren(); - - // Signed right shift, need to copy the sign bit. - ASTNode toFill; - if (BVSRSHIFT == k) - toFill = bbarg1.back(); - else - toFill = ASTFalse; - - ASTVec temp_result(bbarg1); - // if any bit is set in bbarg2 higher than log2Width, then we know that the result is zero. - // Add one to make allowance for rounding down. For example, given 300 bits, the log2 is about - // 8.2 so round up to 9. - - const unsigned width = bbarg1.size(); - unsigned log2Width = (unsigned)log2(width) + 1; - - - if (k == BVSRSHIFT || k == BVRIGHTSHIFT) - for (unsigned int i = 0; i < log2Width; i++) - { - if (bbarg2[i] == ASTFalse) - continue; // Not shifting by anything. - - unsigned int shift_amount = 1 << i; - - for (unsigned int j = 0; j < width; j++) - { - if (j + shift_amount >= width) - temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); - else - temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]); - } - } - else - for (unsigned int i = 0; i < log2Width; i++) - { - if (bbarg2[i] == ASTFalse) - continue; // Not shifting by anything. - - int shift_amount = 1 << i; - - for (signed int j = width - 1; j > 0; j--) - { - if (j < shift_amount) - temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); - else - temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]); - } - } - - // If any of the remainder are true. Then the whole thing gets the fill value. - ASTNode remainder = ASTFalse; - for (unsigned int i = log2Width; i < width; i++) - { - remainder = _bm->CreateNode(OR, remainder, bbarg2[i]); - } - - for (unsigned int i = 0; i < width; i++) - { - temp_result[i] = _bm->CreateSimpForm(ITE, remainder, toFill, temp_result[i]); - } - - result = _bm->CreateNode(BOOLVEC, temp_result); - } - break; + case BVRIGHTSHIFT: + case BVSRSHIFT: + case BVLEFTSHIFT: + { + // Barrel shifter + const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren(); + const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren(); + + // Signed right shift, need to copy the sign bit. + ASTNode toFill; + if (BVSRSHIFT == k) + toFill = bbarg1.back(); + else + toFill = ASTFalse; + + ASTVec temp_result(bbarg1); + // if any bit is set in bbarg2 higher than log2Width, then we know that the result is zero. + // Add one to make allowance for rounding down. For example, given 300 bits, the log2 is about + // 8.2 so round up to 9. + + const unsigned width = bbarg1.size(); + unsigned log2Width = (unsigned)log2(width) + 1; + + + if (k == BVSRSHIFT || k == BVRIGHTSHIFT) + for (unsigned int i = 0; i < log2Width; i++) + { + if (bbarg2[i] == ASTFalse) + continue; // Not shifting by anything. + + unsigned int shift_amount = 1 << i; + + for (unsigned int j = 0; j < width; j++) + { + if (j + shift_amount >= width) + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); + else + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]); + } + } + else + for (unsigned int i = 0; i < log2Width; i++) + { + if (bbarg2[i] == ASTFalse) + continue; // Not shifting by anything. + + int shift_amount = 1 << i; + + for (signed int j = width - 1; j > 0; j--) + { + if (j < shift_amount) + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); + else + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]); + } + } + + // If any of the remainder are true. Then the whole thing gets the fill value. + ASTNode remainder = ASTFalse; + for (unsigned int i = log2Width; i < width; i++) + { + remainder = _bm->CreateNode(OR, remainder, bbarg2[i]); + } + + for (unsigned int i = 0; i < width; i++) + { + temp_result[i] = _bm->CreateSimpForm(ITE, remainder, toFill, temp_result[i]); + } + + result = _bm->CreateNode(BOOLVEC, temp_result); + } + break; case BVVARSHIFT: FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term); break; @@ -163,7 +163,7 @@ namespace BEEV if (result_width == arg_width) { //nothing to sign extend - result = arg; + result = arg; break; } else @@ -846,8 +846,8 @@ namespace BEEV { ASTNode neglit = _bm->CreateSimpNot(*lit); ASTNode thisbit = _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglit, *rit), // TRUE if l < r - _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglit, *rit), // false if not equal - prevbit)); // else prevbit + _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglit, *rit), // false if not equal + prevbit)); // else prevbit prevbit = thisbit; } @@ -863,8 +863,8 @@ namespace BEEV ASTNode neglmsb = _bm->CreateSimpNot(lmsb); ASTNode msb = _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb), // TRUE if l < r - _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglmsb, rmsb), // false if not equal - prevbit)); // else prevbit + _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglmsb, rmsb), // false if not equal + prevbit)); // else prevbit return msb; } diff --git a/src/to-sat/BitBlast.h b/src/to-sat/BitBlast.h index 21fea95..2c0b912 100644 --- a/src/to-sat/BitBlast.h +++ b/src/to-sat/BitBlast.h @@ -78,7 +78,7 @@ namespace BEEV // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. Unsigned only, for now. void BBDivMod(const ASTVec &y, const ASTVec &x, - ASTVec &q, ASTVec &r, unsigned int rwidth); + ASTVec &q, ASTVec &r, unsigned int rwidth); // Return formula for majority function of three formulas. ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c); diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index 3018db8..7769b54 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -15,8 +15,8 @@ namespace BEEV //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or //SOLVER_UNDECIDED bool ToSAT::CallSAT(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input) + const ASTNode& modified_input, + const ASTNode& original_input) { bm->GetRunTimes()->start(RunTimes::BitBlasting); BitBlaster BB(bm); @@ -53,12 +53,12 @@ namespace BEEV if (smtlib_parser_flag) { if (true_iff_valid && - (input_status == TO_BE_SATISFIABLE)) + (input_status == TO_BE_SATISFIABLE)) { cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl; } else if (!true_iff_valid && - (input_status == TO_BE_UNSATISFIABLE)) + (input_status == TO_BE_UNSATISFIABLE)) { cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; } diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 8e984bb..afcf25f 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -34,30 +34,30 @@ namespace BEEV switch (k) { case TRUE: - { - result = true; - break; - } + { + result = true; + break; + } case FALSE: - { - result = true; - break; - } + { + result = true; + break; + } case SYMBOL: - { - result = true; - break; - } + { + result = true; + break; + } case BVCONST: - { - result = true; - break; - } + { + result = true; + break; + } default: - { - result = false; - break; - } + { + result = false; + break; + } } return result; @@ -71,55 +71,55 @@ namespace BEEV switch (k) { case BVLT: - { - result = true; - break; - } + { + result = true; + break; + } case BVLE: - { - result = true; - break; - } + { + result = true; + break; + } case BVGT: - { - result = true; - break; - } + { + result = true; + break; + } case BVGE: - { - result = true; - break; - } + { + result = true; + break; + } case BVSLT: - { - result = true; - break; - } + { + result = true; + break; + } case BVSLE: - { - result = true; - break; - } + { + result = true; + break; + } case BVSGT: - { - result = true; - break; - } + { + result = true; + break; + } case BVSGE: - { - result = true; - break; - } + { + result = true; + break; + } case EQ: - { - result = true; - break; - } + { + result = true; + break; + } default: - { - result = false; - break; - } + { + result = false; + break; + } } return result; @@ -133,15 +133,15 @@ namespace BEEV switch (k) { case ITE: - { - result = true; - break; - } + { + result = true; + break; + } default: - { - result = false; - break; - } + { + result = false; + break; + } } return result; @@ -155,32 +155,32 @@ namespace BEEV switch (k) { case NOT: - { - result = false; - break; - } + { + result = false; + break; + } case NAND: - { - result = false; - break; - } + { + result = false; + break; + } case NOR: - { - result = false; - break; - } + { + result = false; + break; + } case IMPLIES: - { - if (idx == 0) - { - result = false; - } - break; - } + { + if (idx == 0) + { + result = false; + } + break; + } default: - { - break; - } + { + break; + } } return result; @@ -194,50 +194,50 @@ namespace BEEV switch (k) { case NOT: - { - result = true; - break; - } + { + result = true; + break; + } case NAND: - { - result = true; - break; - } + { + result = true; + break; + } case NOR: - { - result = true; - break; - } + { + result = true; + break; + } case XOR: - { - result = true; - break; - } + { + result = true; + break; + } case IFF: - { - result = true; - break; - } + { + result = true; + break; + } case IMPLIES: - { - if (idx == 0) - { - result = true; - } - break; - } + { + if (idx == 0) + { + result = true; + } + break; + } case ITE: - { - if (idx == 0) - { - result = true; - } - break; - } + { + if (idx == 0) + { + result = true; + } + break; + } default: - { - break; - } + { + break; + } } return result; @@ -284,8 +284,8 @@ namespace BEEV bool result = false; if (x.control & (1 << idx)) - { - result = true; + { + result = true; } return result; @@ -383,7 +383,7 @@ namespace BEEV ClauseList::const_iterator it = varphi.begin(); for (; it != varphi.end(); it++) { - psi->push_back(new vector (**it)); + psi->push_back(new vector (**it)); } return psi; @@ -421,7 +421,7 @@ namespace BEEV void CNFMgr::NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2) { varphi1->insert(varphi1->end(), varphi2->begin(), varphi2->end()); - delete varphi2; + delete varphi2; } //End of NOCOPY_INPLACE_UNION ClauseList* CNFMgr::PRODUCT(const ClauseList& varphi1, const ClauseList& varphi2) @@ -432,17 +432,17 @@ namespace BEEV ClauseList::const_iterator it1 = varphi1.begin(); for (; it1 != varphi1.end(); it1++) { - ClausePtr clause1 = *it1; - ClauseList::const_iterator it2 = varphi2.begin(); - for (; it2 != varphi2.end(); it2++) - { - ClausePtr clause2 = *it2; - ClausePtr clause = new vector (); - clause->reserve(clause1->size() + clause2->size()); - clause->insert(clause->end(), clause1->begin(), clause1->end()); - clause->insert(clause->end(), clause2->begin(), clause2->end()); - psi->push_back(clause); - } + ClausePtr clause1 = *it1; + ClauseList::const_iterator it2 = varphi2.begin(); + for (; it2 != varphi2.end(); it2++) + { + ClausePtr clause2 = *it2; + ClausePtr clause = new vector (); + clause->reserve(clause1->size() + clause2->size()); + clause->insert(clause->end(), clause1->begin(), clause1->end()); + clause->insert(clause->end(), clause2->begin(), clause2->end()); + psi->push_back(clause); + } } return psi; @@ -462,13 +462,13 @@ namespace BEEV if (info.find(varphi) == info.end()) { - x = new CNFInfo(); - initializeCNFInfo(*x); - info[varphi] = x; + x = new CNFInfo(); + initializeCNFInfo(*x); + info[varphi] = x; } else { - x = info[varphi]; + x = info[varphi]; } //######################################## @@ -477,12 +477,12 @@ namespace BEEV if (isPos && sharesPos(*x) == 2) { - return; + return; } if (!isPos && sharesNeg(*x) == 2) { - return; + return; } //######################################## @@ -491,12 +491,12 @@ namespace BEEV if (isPos) { - incrementSharesPos(*x); + incrementSharesPos(*x); } if (!isPos) { - incrementSharesNeg(*x); + incrementSharesNeg(*x); } //######################################## @@ -505,28 +505,28 @@ namespace BEEV if (isAtom(varphi)) { - return; + return; } else if (isPred(varphi)) { - for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) - { - scanTerm(varphi[i]); - } + for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) + { + scanTerm(varphi[i]); + } } else { - for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) - { - if (onChildDoPos(varphi, i)) - { - scanFormula(varphi[i], isPos); - } - if (onChildDoNeg(varphi, i)) - { - scanFormula(varphi[i], !isPos); - } - } + for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) + { + if (onChildDoPos(varphi, i)) + { + scanFormula(varphi[i], isPos); + } + if (onChildDoNeg(varphi, i)) + { + scanFormula(varphi[i], !isPos); + } + } } } //End of ScanFormula() @@ -541,13 +541,13 @@ namespace BEEV if (info.find(varphi) == info.end()) { - x = new CNFInfo(); - initializeCNFInfo(*x); - info[varphi] = x; + x = new CNFInfo(); + initializeCNFInfo(*x); + info[varphi] = x; } else { - x = info[varphi]; + x = info[varphi]; } //######################################## @@ -556,7 +556,7 @@ namespace BEEV if (sharesPos(*x) == 2) { - return; + return; } //######################################## @@ -573,27 +573,27 @@ namespace BEEV if (isAtom(varphi)) { - return; + return; } else if (isITE(varphi)) { - scanFormula(varphi[0], true); - scanFormula(varphi[0], false); - scanTerm(varphi[1]); - scanTerm(varphi[2]); + scanFormula(varphi[0], true); + scanFormula(varphi[0], false); + scanTerm(varphi[1]); + scanTerm(varphi[2]); } else { - for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) - { - scanTerm(varphi[i]); - } + for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) + { + scanTerm(varphi[i]); + } } }//End of scanterm() - //######################################## - //######################################## - // main cnf conversion function + //######################################## + //######################################## + // main cnf conversion function void CNFMgr::convertFormulaToCNF(const ASTNode& varphi, ClauseList* defs) { @@ -604,9 +604,9 @@ namespace BEEV if (isTerm(*x)) { - convertTermForCNF(varphi, defs); - setWasVisited(*x); - return; + convertTermForCNF(varphi, defs); + setWasVisited(*x); + return; } //######################################## @@ -614,28 +614,28 @@ namespace BEEV if (sharesPos(*x) > 0 && !wasVisited(*x)) { - convertFormulaToCNFPosCases(varphi, defs); + convertFormulaToCNFPosCases(varphi, defs); } if (x->clausespos != NULL && x->clausespos->size() > 1) { - if (doSibRenamingPos(*x) || sharesPos(*x) > 1) - { - doRenamingPos(varphi, defs); - } + if (doSibRenamingPos(*x) || sharesPos(*x) > 1) + { + doRenamingPos(varphi, defs); + } } if (sharesNeg(*x) > 0 && !wasVisited(*x)) { - convertFormulaToCNFNegCases(varphi, defs); + convertFormulaToCNFNegCases(varphi, defs); } if (x->clausesneg != NULL && x->clausesneg->size() > 1) { - if (doSibRenamingNeg(*x) || sharesNeg(*x) > 1) - { - doRenamingNeg(varphi, defs); - } + if (doSibRenamingNeg(*x) || sharesNeg(*x) > 1) + { + doRenamingNeg(varphi, defs); + } } //######################################## @@ -654,7 +654,7 @@ namespace BEEV if (x->termforcnf != NULL) { - return; + return; } //######################################## @@ -663,29 +663,29 @@ namespace BEEV if (isITE(varphi)) { - x->termforcnf = doRenameITE(varphi, defs); - reduceMemoryFootprintPos(varphi[0]); - reduceMemoryFootprintNeg(varphi[0]); - + x->termforcnf = doRenameITE(varphi, defs); + reduceMemoryFootprintPos(varphi[0]); + reduceMemoryFootprintNeg(varphi[0]); + } else if (isAtom(varphi)) { - x->termforcnf = ASTNodeToASTNodePtr(varphi); + x->termforcnf = ASTNodeToASTNodePtr(varphi); } else - { - ASTVec psis; - ASTVec::const_iterator it = varphi.GetChildren().begin(); - for (; it != varphi.GetChildren().end(); it++) - { - convertTermForCNF(*it, defs); - psis.push_back(*(info[*it]->termforcnf)); - } - - ASTNode psi = bm->CreateNode(varphi.GetKind(), psis); - psi.SetValueWidth(varphi.GetValueWidth()); - psi.SetIndexWidth(varphi.GetIndexWidth()); - x->termforcnf = ASTNodeToASTNodePtr(psi); + { + ASTVec psis; + ASTVec::const_iterator it = varphi.GetChildren().begin(); + for (; it != varphi.GetChildren().end(); it++) + { + convertTermForCNF(*it, defs); + psis.push_back(*(info[*it]->termforcnf)); + } + + ASTNode psi = bm->CreateNode(varphi.GetKind(), psis); + psi.SetValueWidth(varphi.GetValueWidth()); + psi.SetIndexWidth(varphi.GetIndexWidth()); + x->termforcnf = ASTNodeToASTNodePtr(psi); } } //End of convertTermForCNF() @@ -777,7 +777,7 @@ namespace BEEV //######################################## // step 2, calc new variable - //######################################## + //######################################## ostringstream oss; oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; @@ -811,894 +811,894 @@ namespace BEEV { if (isPred(varphi)) { - convertFormulaToCNFPosPred(varphi, defs); - return; + convertFormulaToCNFPosPred(varphi, defs); + return; } Kind k = varphi.GetKind(); switch (k) { case FALSE: - { - convertFormulaToCNFPosFALSE(varphi, defs); - break; - } - case TRUE: - { - convertFormulaToCNFPosTRUE(varphi, defs); - break; - } + { + convertFormulaToCNFPosFALSE(varphi, defs); + break; + } + case TRUE: + { + convertFormulaToCNFPosTRUE(varphi, defs); + break; + } case BVGETBIT: - { - convertFormulaToCNFPosBVGETBIT(varphi, defs); - break; - } + { + convertFormulaToCNFPosBVGETBIT(varphi, defs); + break; + } case SYMBOL: - { - convertFormulaToCNFPosSYMBOL(varphi, defs); - break; - } + { + convertFormulaToCNFPosSYMBOL(varphi, defs); + break; + } case NOT: - { - convertFormulaToCNFPosNOT(varphi, defs); - break; - } + { + convertFormulaToCNFPosNOT(varphi, defs); + break; + } case AND: - { - convertFormulaToCNFPosAND(varphi, defs); - break; - } + { + convertFormulaToCNFPosAND(varphi, defs); + break; + } case NAND: - { - convertFormulaToCNFPosNAND(varphi, defs); - break; - } + { + convertFormulaToCNFPosNAND(varphi, defs); + break; + } case OR: - { - convertFormulaToCNFPosOR(varphi, defs); - break; - } + { + convertFormulaToCNFPosOR(varphi, defs); + break; + } case NOR: - { - convertFormulaToCNFPosNOR(varphi, defs); - break; - } - case XOR: - { - convertFormulaToCNFPosXOR(varphi, defs); - break; - } - case IMPLIES: - { - convertFormulaToCNFPosIMPLIES(varphi, defs); - break; - } - case ITE: - { - convertFormulaToCNFPosITE(varphi, defs); - break; - } - default: - { - fprintf(stderr, "convertFormulaToCNFPosCases: doesn't handle kind %d\n", k); - FatalError(""); - } + { + convertFormulaToCNFPosNOR(varphi, defs); + break; + } + case XOR: + { + convertFormulaToCNFPosXOR(varphi, defs); + break; } + case IMPLIES: + { + convertFormulaToCNFPosIMPLIES(varphi, defs); + break; + } + case ITE: + { + convertFormulaToCNFPosITE(varphi, defs); + break; + } + default: + { + fprintf(stderr, "convertFormulaToCNFPosCases: doesn't handle kind %d\n", k); + FatalError(""); + } + } } //End of convertFormulaToCNFPosCases() void CNFMgr::convertFormulaToCNFNegCases(const ASTNode& varphi, ClauseList* defs) - { + { + + if (isPred(varphi)) + { + convertFormulaToCNFNegPred(varphi, defs); + return; + } - if (isPred(varphi)) + Kind k = varphi.GetKind(); + switch (k) + { + case FALSE: { - convertFormulaToCNFNegPred(varphi, defs); - return; + convertFormulaToCNFNegFALSE(varphi, defs); + break; } - - Kind k = varphi.GetKind(); - switch (k) + case TRUE: { - case FALSE: - { - convertFormulaToCNFNegFALSE(varphi, defs); - break; - } - case TRUE: - { - convertFormulaToCNFNegTRUE(varphi, defs); - break; - } - case BVGETBIT: - { - convertFormulaToCNFNegBVGETBIT(varphi, defs); - break; - } - case SYMBOL: - { - convertFormulaToCNFNegSYMBOL(varphi, defs); - break; - } - case NOT: - { - convertFormulaToCNFNegNOT(varphi, defs); - break; - } - case AND: - { - convertFormulaToCNFNegAND(varphi, defs); - break; - } - case NAND: - { - convertFormulaToCNFNegNAND(varphi, defs); - break; - } - case OR: - { - convertFormulaToCNFNegOR(varphi, defs); - break; - } - case NOR: - { - convertFormulaToCNFNegNOR(varphi, defs); - break; - } - case XOR: - { - convertFormulaToCNFNegXOR(varphi, defs); - break; - } - case IMPLIES: - { - convertFormulaToCNFNegIMPLIES(varphi, defs); - break; - } - case ITE: - { - convertFormulaToCNFNegITE(varphi, defs); - break; - } - default: - { - fprintf(stderr, "convertFormulaToCNFNegCases: doesn't handle kind %d\n", k); - FatalError(""); - } + convertFormulaToCNFNegTRUE(varphi, defs); + break; } - } //convertFormulaToCNFNegCases() - - //######################################## - //######################################## - // individual cnf conversion cases - - void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs) - { - ASTVec psis; - - ASTVec::const_iterator it = varphi.GetChildren().begin(); - for (; it != varphi.GetChildren().end(); it++) + case BVGETBIT: { - convertTermForCNF(*it, defs); - psis.push_back(*(info[*it]->termforcnf)); + convertFormulaToCNFNegBVGETBIT(varphi, defs); + break; } - - info[varphi]->clausespos = SINGLETON(bm->CreateNode(varphi.GetKind(), psis)); - } //End of convertFormulaToCNFPosPred() - - void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs) - { - ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); - info[varphi]->clausespos = SINGLETON(dummy_false_var); - } //End of convertFormulaToCNFPosFALSE() - - void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs) - { - ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); - info[varphi]->clausespos = SINGLETON(dummy_true_var); - } //End of convertFormulaToCNFPosTRUE - - void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs) - { - info[varphi]->clausespos = SINGLETON(varphi); - }//End of convertFormulaToCNFPosBVGETBIT() - - void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs) - { - info[varphi]->clausespos = SINGLETON(varphi); - } //End of convertFormulaToCNFPosSYMBOL() - - void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs) - { - convertFormulaToCNF(varphi[0], defs); - info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg)); - reduceMemoryFootprintNeg(varphi[0]); - } //End of convertFormulaToCNFPosNOT() - - void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (pos) AND ~> UNION - //**************************************** - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - ClauseList* psi = COPY(*(info[*it]->clausespos)); - for (it++; it != varphi.GetChildren().end(); it++) + case SYMBOL: { - convertFormulaToCNF(*it, defs); - INPLACE_UNION(psi, *(info[*it]->clausespos)); - reduceMemoryFootprintPos(*it); + convertFormulaToCNFNegSYMBOL(varphi, defs); + break; } - - info[varphi]->clausespos = psi; - } //End of convertFormulaToCNFPosAND() - - void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs) - { - bool renamesibs = false; - ClauseList* clauses; - ClauseList* psi; - ClauseList* oldpsi; - - //**************************************** - // (pos) NAND ~> PRODUCT NOT - //**************************************** - - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausesneg; - if (clauses->size() > 1) + case NOT: { - renamesibs = true; + convertFormulaToCNFNegNOT(varphi, defs); + break; } - psi = COPY(*clauses); - reduceMemoryFootprintNeg(*it); - - for (it++; it != varphi.GetChildren().end(); it++) + case AND: { - if (renamesibs) - { - setDoSibRenamingNeg(*(info[*it])); - } - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausesneg; - if (clauses->size() > 1) - { - renamesibs = true; - } - oldpsi = psi; - psi = PRODUCT(*psi, *clauses); - reduceMemoryFootprintNeg(*it); - DELETE(oldpsi); + convertFormulaToCNFNegAND(varphi, defs); + break; } - - info[varphi]->clausespos = psi; - } //End of convertFormulaToCNFPosNAND() - - void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs) - { - bool renamesibs = false; - ClauseList* clauses; - ClauseList* psi; - ClauseList* oldpsi; - - //**************************************** - // (pos) OR ~> PRODUCT - //**************************************** - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausespos; - if (clauses->size() > 1) + case NAND: { - renamesibs = true; + convertFormulaToCNFNegNAND(varphi, defs); + break; } - psi = COPY(*clauses); - reduceMemoryFootprintPos(*it); - - for (it++; it != varphi.GetChildren().end(); it++) + case OR: { - if (renamesibs) - { - setDoSibRenamingPos(*(info[*it])); - } - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausespos; - if (clauses->size() > 1) - { - renamesibs = true; - } - oldpsi = psi; - psi = PRODUCT(*psi, *clauses); - reduceMemoryFootprintPos(*it); - DELETE(oldpsi); + convertFormulaToCNFNegOR(varphi, defs); + break; } - - info[varphi]->clausespos = psi; - } //End of convertFormulaToCNFPosOR() - - void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (pos) NOR ~> UNION NOT - //**************************************** - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - ClauseList* psi = COPY(*(info[*it]->clausesneg)); - reduceMemoryFootprintNeg(*it); - for (it++; it != varphi.GetChildren().end(); it++) + case NOR: { - convertFormulaToCNF(*it, defs); - INPLACE_UNION(psi, *(info[*it]->clausesneg)); - reduceMemoryFootprintNeg(*it); + convertFormulaToCNFNegNOR(varphi, defs); + break; } - - info[varphi]->clausespos = psi; - } //End of convertFormulaToCNFPosNOR() - - void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (pos) IMPLIES ~> PRODUCT NOT [0] ; [1] - //**************************************** - CNFInfo* x0 = info[varphi[0]]; - CNFInfo* x1 = info[varphi[1]]; - convertFormulaToCNF(varphi[0], defs); - if (x0->clausesneg->size() > 1) + case XOR: { - setDoSibRenamingPos(*x1); + convertFormulaToCNFNegXOR(varphi, defs); + break; } - convertFormulaToCNF(varphi[1], defs); - ClauseList* psi = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); - reduceMemoryFootprintNeg(varphi[0]); - reduceMemoryFootprintPos(varphi[1]); - info[varphi]->clausespos = psi; - } //End of convertFormulaToCNFPosIMPLIES() - - void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1]) - // ; (PRODUCT [0] ; [2]) - //**************************************** - CNFInfo* x0 = info[varphi[0]]; - CNFInfo* x1 = info[varphi[1]]; - CNFInfo* x2 = info[varphi[2]]; - convertFormulaToCNF(varphi[0], defs); - if (x0->clausesneg->size() > 1) + case IMPLIES: { - setDoSibRenamingPos(*x1); + convertFormulaToCNFNegIMPLIES(varphi, defs); + break; } - convertFormulaToCNF(varphi[1], defs); - if (x0->clausespos->size() > 1) + case ITE: { - setDoSibRenamingPos(*x2); + convertFormulaToCNFNegITE(varphi, defs); + break; } - convertFormulaToCNF(varphi[2], defs); - ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); - ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausespos)); - NOCOPY_INPLACE_UNION(psi1, psi2); - reduceMemoryFootprintNeg(varphi[0]); - reduceMemoryFootprintPos(varphi[1]); - reduceMemoryFootprintPos(varphi[0]); - reduceMemoryFootprintPos(varphi[2]); - - info[varphi]->clausespos = psi1; - } //End of convertFormulaToCNFPosITE() - - void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs) - { - ASTVec::const_iterator it = varphi.GetChildren().begin(); - for (; it != varphi.GetChildren().end(); it++) + default: { - convertFormulaToCNF(*it, defs); // make pos and neg clause sets + fprintf(stderr, "convertFormulaToCNFNegCases: doesn't handle kind %d\n", k); + FatalError(""); } - ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); - info[varphi]->clausespos = psi; - ASTVec::const_iterator it2 = varphi.GetChildren().begin(); - for (; it2 != varphi.GetChildren().end(); it2++){ - reduceMemoryFootprintPos(*it2); - reduceMemoryFootprintNeg(*it2); } - } //End of convertFormulaToCNFPosXOR() + } //convertFormulaToCNFNegCases() - ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs) - { + //######################################## + //######################################## + // individual cnf conversion cases - bool renamesibs; - ClauseList* psi; - ClauseList* psi1; - ClauseList* psi2; + void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs) + { + ASTVec psis; - if (idx == varphi.GetChildren().size() - 2) - { - //**************************************** - // (pos) XOR ~> UNION - // (PRODUCT [idx] ; [idx+1]) - // ; (PRODUCT NOT [idx] ; NOT [idx+1]) - //**************************************** - renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingPos(*info[varphi[idx + 1]]); - } - renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingNeg(*info[varphi[idx + 1]]); - } + ASTVec::const_iterator it = varphi.GetChildren().begin(); + for (; it != varphi.GetChildren().end(); it++) + { + convertTermForCNF(*it, defs); + psis.push_back(*(info[*it]->termforcnf)); + } - psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausespos)); - psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausesneg)); - NOCOPY_INPLACE_UNION(psi1, psi2); + info[varphi]->clausespos = SINGLETON(bm->CreateNode(varphi.GetKind(), psis)); + } //End of convertFormulaToCNFPosPred() - psi = psi1; - } - else - { - //**************************************** - // (pos) XOR ~> UNION - // (PRODUCT [idx] ; XOR [idx+1..]) - // ; (PRODUCT NOT [idx] ; NOT XOR [idx+1..]) - //**************************************** - ClauseList* theta1; - theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs); - renamesibs = theta1->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingPos(*info[varphi[idx]]); - } - ClauseList* theta2; - theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs); - renamesibs = theta2->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingNeg(*info[varphi[idx]]); - } + void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs) + { + ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); + info[varphi]->clausespos = SINGLETON(dummy_false_var); + } //End of convertFormulaToCNFPosFALSE() - psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta1); - psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta2); - DELETE(theta1); - DELETE(theta2); - NOCOPY_INPLACE_UNION(psi1, psi2); + void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs) + { + ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); + info[varphi]->clausespos = SINGLETON(dummy_true_var); + } //End of convertFormulaToCNFPosTRUE - psi = psi1; - } + void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs) + { + info[varphi]->clausespos = SINGLETON(varphi); + }//End of convertFormulaToCNFPosBVGETBIT() - return psi; - } //End of convertFormulaToCNFPosXORAux() + void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs) + { + info[varphi]->clausespos = SINGLETON(varphi); + } //End of convertFormulaToCNFPosSYMBOL() - void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs) - { + void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs) + { + convertFormulaToCNF(varphi[0], defs); + info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg)); + reduceMemoryFootprintNeg(varphi[0]); + } //End of convertFormulaToCNFPosNOT() - ASTVec psis; + void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (pos) AND ~> UNION + //**************************************** + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + ClauseList* psi = COPY(*(info[*it]->clausespos)); + for (it++; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); + INPLACE_UNION(psi, *(info[*it]->clausespos)); + reduceMemoryFootprintPos(*it); + } - ASTVec::const_iterator it = varphi.GetChildren().begin(); - for (; it != varphi.GetChildren().end(); it++) - { - convertFormulaToCNF(*it, defs); - psis.push_back(*(info[*it]->termforcnf)); - } + info[varphi]->clausespos = psi; + } //End of convertFormulaToCNFPosAND() - info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, bm->CreateNode(varphi.GetKind(), psis))); - } //End of convertFormulaToCNFNegPred() - - void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs) - { - ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); - info[varphi]->clausesneg = SINGLETON(dummy_true_var); - } //End of convertFormulaToCNFNegFALSE() - - void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs) - { - ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); - info[varphi]->clausesneg = SINGLETON(dummy_false_var); - } //End of convertFormulaToCNFNegTRUE() - - void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs) - { - ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi)); - info[varphi]->clausesneg = psi; - } //End of convertFormulaToCNFNegBVGETBIT() - - void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs) - { - info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, varphi)); - } //End of convertFormulaToCNFNegSYMBOL() - - void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs) - { - convertFormulaToCNF(varphi[0], defs); - info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos)); - reduceMemoryFootprintPos(varphi[0]); - } //End of convertFormulaToCNFNegNOT() - - void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs) - { - bool renamesibs = false; - ClauseList* clauses; - ClauseList* psi; - ClauseList* oldpsi; - - //**************************************** - // (neg) AND ~> PRODUCT NOT - //**************************************** - - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausesneg; - if (clauses->size() > 1) - { - renamesibs = true; - } - psi = COPY(*clauses); - reduceMemoryFootprintNeg(*it); + void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs) + { + bool renamesibs = false; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; + + //**************************************** + // (pos) NAND ~> PRODUCT NOT + //**************************************** + + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausesneg; + if (clauses->size() > 1) + { + renamesibs = true; + } + psi = COPY(*clauses); + reduceMemoryFootprintNeg(*it); - for (it++; it != varphi.GetChildren().end(); it++) - { - if (renamesibs) - { - setDoSibRenamingNeg(*(info[*it])); - } - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausesneg; - if (clauses->size() > 1) - { - renamesibs = true; - } - oldpsi = psi; - psi = PRODUCT(*psi, *clauses); - reduceMemoryFootprintNeg(*it); - DELETE(oldpsi); - } + for (it++; it != varphi.GetChildren().end(); it++) + { + if (renamesibs) + { + setDoSibRenamingNeg(*(info[*it])); + } + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausesneg; + if (clauses->size() > 1) + { + renamesibs = true; + } + oldpsi = psi; + psi = PRODUCT(*psi, *clauses); + reduceMemoryFootprintNeg(*it); + DELETE(oldpsi); + } - info[varphi]->clausesneg = psi; - } //End of convertFormulaToCNFNegAND() - - void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (neg) NAND ~> UNION - //**************************************** - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - ClauseList* psi = COPY(*(info[*it]->clausespos)); - reduceMemoryFootprintPos(*it); - for (it++; it != varphi.GetChildren().end(); it++) - { - convertFormulaToCNF(*it, defs); - INPLACE_UNION(psi, *(info[*it]->clausespos)); - reduceMemoryFootprintPos(*it); - } + info[varphi]->clausespos = psi; + } //End of convertFormulaToCNFPosNAND() - info[varphi]->clausespos = psi; - } //End of convertFormulaToCNFNegNAND() - - void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (neg) OR ~> UNION NOT - //**************************************** - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - ClauseList* psi = COPY(*(info[*it]->clausesneg)); - reduceMemoryFootprintNeg(*it); - for (it++; it != varphi.GetChildren().end(); it++) - { - convertFormulaToCNF(*it, defs); - INPLACE_UNION(psi, *(info[*it]->clausesneg)); - reduceMemoryFootprintNeg(*it); - } + void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs) + { + bool renamesibs = false; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; + + //**************************************** + // (pos) OR ~> PRODUCT + //**************************************** + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausespos; + if (clauses->size() > 1) + { + renamesibs = true; + } + psi = COPY(*clauses); + reduceMemoryFootprintPos(*it); - info[varphi]->clausesneg = psi; - } //End of convertFormulaToCNFNegOR() - - void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs) - { - bool renamesibs = false; - ClauseList* clauses; - ClauseList* psi; - ClauseList* oldpsi; - - //**************************************** - // (neg) NOR ~> PRODUCT - //**************************************** - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausespos; - if (clauses->size() > 1) - { - renamesibs = true; - } - psi = COPY(*clauses); - reduceMemoryFootprintPos(*it); + for (it++; it != varphi.GetChildren().end(); it++) + { + if (renamesibs) + { + setDoSibRenamingPos(*(info[*it])); + } + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausespos; + if (clauses->size() > 1) + { + renamesibs = true; + } + oldpsi = psi; + psi = PRODUCT(*psi, *clauses); + reduceMemoryFootprintPos(*it); + DELETE(oldpsi); + } - for (it++; it != varphi.GetChildren().end(); it++) - { - if (renamesibs) - { - setDoSibRenamingPos(*(info[*it])); - } - convertFormulaToCNF(*it, defs); - clauses = info[*it]->clausespos; - if (clauses->size() > 1) - { - renamesibs = true; - } - oldpsi = psi; - psi = PRODUCT(*psi, *clauses); - reduceMemoryFootprintPos(*it); - DELETE(oldpsi); - } + info[varphi]->clausespos = psi; + } //End of convertFormulaToCNFPosOR() - info[varphi]->clausesneg = psi; - } //End of convertFormulaToCNFNegNOR() - - void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (neg) IMPLIES ~> UNION [0] ; NOT [1] - //**************************************** - CNFInfo* x0 = info[varphi[0]]; - CNFInfo* x1 = info[varphi[1]]; - convertFormulaToCNF(varphi[0], defs); - convertFormulaToCNF(varphi[1], defs); - ClauseList* psi = UNION(*(x0->clausespos), *(x1->clausesneg)); - info[varphi]->clausesneg = psi; - reduceMemoryFootprintPos(varphi[0]); - reduceMemoryFootprintNeg(varphi[1]); - } //End of convertFormulaToCNFNegIMPLIES() - - void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs) - { - //**************************************** - // (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1]) - // ; (PRODUCT [0] ; NOT [2]) - //**************************************** - CNFInfo* x0 = info[varphi[0]]; - CNFInfo* x1 = info[varphi[1]]; - CNFInfo* x2 = info[varphi[2]]; - convertFormulaToCNF(varphi[0], defs); - if (x0->clausesneg->size() > 1) - { - setDoSibRenamingNeg(*x1); - } - convertFormulaToCNF(varphi[1], defs); - if (x0->clausespos->size() > 1) - { - setDoSibRenamingNeg(*x2); - } - convertFormulaToCNF(varphi[2], defs); - ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausesneg)); - ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausesneg)); - NOCOPY_INPLACE_UNION(psi1, psi2); - reduceMemoryFootprintNeg(varphi[0]); - reduceMemoryFootprintNeg(varphi[1]); - reduceMemoryFootprintPos(varphi[0]); - reduceMemoryFootprintNeg(varphi[2]); - - info[varphi]->clausesneg = psi1; - } //End of convertFormulaToCNFNegITE() - - void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs) - { - ASTVec::const_iterator it = varphi.GetChildren().begin(); - for (; it != varphi.GetChildren().end(); it++) - { - convertFormulaToCNF(*it, defs); // make pos and neg clause sets - } - ClauseList* psi = convertFormulaToCNFNegXORAux(varphi, 0, defs); - info[varphi]->clausesneg = psi; - ASTVec::const_iterator it2 = varphi.GetChildren().begin(); - for (; it2 != varphi.GetChildren().end(); it2++){ - reduceMemoryFootprintPos(*it2); - reduceMemoryFootprintNeg(*it2); - } - } //End of convertFormulaToCNFNegXOR() - - ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs) - { - bool renamesibs; - ClauseList* psi; - ClauseList* psi1; - ClauseList* psi2; - - if (idx == varphi.GetChildren().size() - 2) - { + void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (pos) NOR ~> UNION NOT + //**************************************** + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + ClauseList* psi = COPY(*(info[*it]->clausesneg)); + reduceMemoryFootprintNeg(*it); + for (it++; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); + INPLACE_UNION(psi, *(info[*it]->clausesneg)); + reduceMemoryFootprintNeg(*it); + } - //**************************************** - // (neg) XOR ~> UNION - // (PRODUCT NOT [idx] ; [idx+1]) - // ; (PRODUCT [idx] ; NOT [idx+1]) - //**************************************** - convertFormulaToCNF(varphi[idx], defs); - renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingPos(*info[varphi[idx + 1]]); - } + info[varphi]->clausespos = psi; + } //End of convertFormulaToCNFPosNOR() - convertFormulaToCNF(varphi[idx], defs); - renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingNeg(*info[varphi[idx + 1]]); - } + void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (pos) IMPLIES ~> PRODUCT NOT [0] ; [1] + //**************************************** + CNFInfo* x0 = info[varphi[0]]; + CNFInfo* x1 = info[varphi[1]]; + convertFormulaToCNF(varphi[0], defs); + if (x0->clausesneg->size() > 1) + { + setDoSibRenamingPos(*x1); + } + convertFormulaToCNF(varphi[1], defs); + ClauseList* psi = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); + reduceMemoryFootprintNeg(varphi[0]); + reduceMemoryFootprintPos(varphi[1]); + info[varphi]->clausespos = psi; + } //End of convertFormulaToCNFPosIMPLIES() + + void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1]) + // ; (PRODUCT [0] ; [2]) + //**************************************** + CNFInfo* x0 = info[varphi[0]]; + CNFInfo* x1 = info[varphi[1]]; + CNFInfo* x2 = info[varphi[2]]; + convertFormulaToCNF(varphi[0], defs); + if (x0->clausesneg->size() > 1) + { + setDoSibRenamingPos(*x1); + } + convertFormulaToCNF(varphi[1], defs); + if (x0->clausespos->size() > 1) + { + setDoSibRenamingPos(*x2); + } + convertFormulaToCNF(varphi[2], defs); + ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); + ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausespos)); + NOCOPY_INPLACE_UNION(psi1, psi2); + reduceMemoryFootprintNeg(varphi[0]); + reduceMemoryFootprintPos(varphi[1]); + reduceMemoryFootprintPos(varphi[0]); + reduceMemoryFootprintPos(varphi[2]); + + info[varphi]->clausespos = psi1; + } //End of convertFormulaToCNFPosITE() + + void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs) + { + ASTVec::const_iterator it = varphi.GetChildren().begin(); + for (; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); // make pos and neg clause sets + } + ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); + info[varphi]->clausespos = psi; + ASTVec::const_iterator it2 = varphi.GetChildren().begin(); + for (; it2 != varphi.GetChildren().end(); it2++){ + reduceMemoryFootprintPos(*it2); + reduceMemoryFootprintNeg(*it2); + } + } //End of convertFormulaToCNFPosXOR() - psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausespos)); - psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausesneg)); - NOCOPY_INPLACE_UNION(psi1, psi2); + ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs) + { - psi = psi1; - } - else - { - //**************************************** - // (neg) XOR ~> UNION - // (PRODUCT NOT [idx] ; XOR [idx+1..]) - // ; (PRODUCT [idx] ; NOT XOR [idx+1..]) - //**************************************** - ClauseList* theta1; - theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs); - renamesibs = theta1->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingNeg(*info[varphi[idx]]); - } - convertFormulaToCNF(varphi[idx], defs); + bool renamesibs; + ClauseList* psi; + ClauseList* psi1; + ClauseList* psi2; - ClauseList* theta2; - theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs); - renamesibs = theta2->size() > 1 ? true : false; - if (renamesibs) - { - setDoSibRenamingPos(*info[varphi[idx]]); - } + if (idx == varphi.GetChildren().size() - 2) + { + //**************************************** + // (pos) XOR ~> UNION + // (PRODUCT [idx] ; [idx+1]) + // ; (PRODUCT NOT [idx] ; NOT [idx+1]) + //**************************************** + renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingPos(*info[varphi[idx + 1]]); + } + renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingNeg(*info[varphi[idx + 1]]); + } - psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta1); - psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta2); - DELETE(theta1); - DELETE(theta2); - NOCOPY_INPLACE_UNION(psi1, psi2); + psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausespos)); + psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausesneg)); + NOCOPY_INPLACE_UNION(psi1, psi2); - psi = psi1; - } + psi = psi1; + } + else + { + //**************************************** + // (pos) XOR ~> UNION + // (PRODUCT [idx] ; XOR [idx+1..]) + // ; (PRODUCT NOT [idx] ; NOT XOR [idx+1..]) + //**************************************** + ClauseList* theta1; + theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs); + renamesibs = theta1->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingPos(*info[varphi[idx]]); + } + ClauseList* theta2; + theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs); + renamesibs = theta2->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingNeg(*info[varphi[idx]]); + } + + psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta1); + psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta2); + DELETE(theta1); + DELETE(theta2); + NOCOPY_INPLACE_UNION(psi1, psi2); + + psi = psi1; + } + + return psi; + } //End of convertFormulaToCNFPosXORAux() + + void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs) + { + + ASTVec psis; + + ASTVec::const_iterator it = varphi.GetChildren().begin(); + for (; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); + psis.push_back(*(info[*it]->termforcnf)); + } + + info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, bm->CreateNode(varphi.GetKind(), psis))); + } //End of convertFormulaToCNFNegPred() + + void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs) + { + ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); + info[varphi]->clausesneg = SINGLETON(dummy_true_var); + } //End of convertFormulaToCNFNegFALSE() + + void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs) + { + ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); + info[varphi]->clausesneg = SINGLETON(dummy_false_var); + } //End of convertFormulaToCNFNegTRUE() + + void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs) + { + ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi)); + info[varphi]->clausesneg = psi; + } //End of convertFormulaToCNFNegBVGETBIT() + + void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs) + { + info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, varphi)); + } //End of convertFormulaToCNFNegSYMBOL() + + void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs) + { + convertFormulaToCNF(varphi[0], defs); + info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos)); + reduceMemoryFootprintPos(varphi[0]); + } //End of convertFormulaToCNFNegNOT() + + void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs) + { + bool renamesibs = false; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; + + //**************************************** + // (neg) AND ~> PRODUCT NOT + //**************************************** + + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausesneg; + if (clauses->size() > 1) + { + renamesibs = true; + } + psi = COPY(*clauses); + reduceMemoryFootprintNeg(*it); + + for (it++; it != varphi.GetChildren().end(); it++) + { + if (renamesibs) + { + setDoSibRenamingNeg(*(info[*it])); + } + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausesneg; + if (clauses->size() > 1) + { + renamesibs = true; + } + oldpsi = psi; + psi = PRODUCT(*psi, *clauses); + reduceMemoryFootprintNeg(*it); + DELETE(oldpsi); + } + + info[varphi]->clausesneg = psi; + } //End of convertFormulaToCNFNegAND() + + void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (neg) NAND ~> UNION + //**************************************** + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + ClauseList* psi = COPY(*(info[*it]->clausespos)); + reduceMemoryFootprintPos(*it); + for (it++; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); + INPLACE_UNION(psi, *(info[*it]->clausespos)); + reduceMemoryFootprintPos(*it); + } - return psi; - } //End of convertFormulaToCNFNegXORAux() + info[varphi]->clausespos = psi; + } //End of convertFormulaToCNFNegNAND() + + void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (neg) OR ~> UNION NOT + //**************************************** + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + ClauseList* psi = COPY(*(info[*it]->clausesneg)); + reduceMemoryFootprintNeg(*it); + for (it++; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); + INPLACE_UNION(psi, *(info[*it]->clausesneg)); + reduceMemoryFootprintNeg(*it); + } + + info[varphi]->clausesneg = psi; + } //End of convertFormulaToCNFNegOR() + + void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs) + { + bool renamesibs = false; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; + + //**************************************** + // (neg) NOR ~> PRODUCT + //**************************************** + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausespos; + if (clauses->size() > 1) + { + renamesibs = true; + } + psi = COPY(*clauses); + reduceMemoryFootprintPos(*it); + + for (it++; it != varphi.GetChildren().end(); it++) + { + if (renamesibs) + { + setDoSibRenamingPos(*(info[*it])); + } + convertFormulaToCNF(*it, defs); + clauses = info[*it]->clausespos; + if (clauses->size() > 1) + { + renamesibs = true; + } + oldpsi = psi; + psi = PRODUCT(*psi, *clauses); + reduceMemoryFootprintPos(*it); + DELETE(oldpsi); + } + + info[varphi]->clausesneg = psi; + } //End of convertFormulaToCNFNegNOR() + + void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (neg) IMPLIES ~> UNION [0] ; NOT [1] + //**************************************** + CNFInfo* x0 = info[varphi[0]]; + CNFInfo* x1 = info[varphi[1]]; + convertFormulaToCNF(varphi[0], defs); + convertFormulaToCNF(varphi[1], defs); + ClauseList* psi = UNION(*(x0->clausespos), *(x1->clausesneg)); + info[varphi]->clausesneg = psi; + reduceMemoryFootprintPos(varphi[0]); + reduceMemoryFootprintNeg(varphi[1]); + } //End of convertFormulaToCNFNegIMPLIES() + + void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs) + { + //**************************************** + // (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1]) + // ; (PRODUCT [0] ; NOT [2]) + //**************************************** + CNFInfo* x0 = info[varphi[0]]; + CNFInfo* x1 = info[varphi[1]]; + CNFInfo* x2 = info[varphi[2]]; + convertFormulaToCNF(varphi[0], defs); + if (x0->clausesneg->size() > 1) + { + setDoSibRenamingNeg(*x1); + } + convertFormulaToCNF(varphi[1], defs); + if (x0->clausespos->size() > 1) + { + setDoSibRenamingNeg(*x2); + } + convertFormulaToCNF(varphi[2], defs); + ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausesneg)); + ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausesneg)); + NOCOPY_INPLACE_UNION(psi1, psi2); + reduceMemoryFootprintNeg(varphi[0]); + reduceMemoryFootprintNeg(varphi[1]); + reduceMemoryFootprintPos(varphi[0]); + reduceMemoryFootprintNeg(varphi[2]); + + info[varphi]->clausesneg = psi1; + } //End of convertFormulaToCNFNegITE() + + void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs) + { + ASTVec::const_iterator it = varphi.GetChildren().begin(); + for (; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); // make pos and neg clause sets + } + ClauseList* psi = convertFormulaToCNFNegXORAux(varphi, 0, defs); + info[varphi]->clausesneg = psi; + ASTVec::const_iterator it2 = varphi.GetChildren().begin(); + for (; it2 != varphi.GetChildren().end(); it2++){ + reduceMemoryFootprintPos(*it2); + reduceMemoryFootprintNeg(*it2); + } + } //End of convertFormulaToCNFNegXOR() + + ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs) + { + bool renamesibs; + ClauseList* psi; + ClauseList* psi1; + ClauseList* psi2; + + if (idx == varphi.GetChildren().size() - 2) + { + + //**************************************** + // (neg) XOR ~> UNION + // (PRODUCT NOT [idx] ; [idx+1]) + // ; (PRODUCT [idx] ; NOT [idx+1]) + //**************************************** + convertFormulaToCNF(varphi[idx], defs); + renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingPos(*info[varphi[idx + 1]]); + } + + convertFormulaToCNF(varphi[idx], defs); + renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingNeg(*info[varphi[idx + 1]]); + } + + psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausespos)); + psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausesneg)); + NOCOPY_INPLACE_UNION(psi1, psi2); + + psi = psi1; + } + else + { + //**************************************** + // (neg) XOR ~> UNION + // (PRODUCT NOT [idx] ; XOR [idx+1..]) + // ; (PRODUCT [idx] ; NOT XOR [idx+1..]) + //**************************************** + ClauseList* theta1; + theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs); + renamesibs = theta1->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingNeg(*info[varphi[idx]]); + } + convertFormulaToCNF(varphi[idx], defs); + + ClauseList* theta2; + theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs); + renamesibs = theta2->size() > 1 ? true : false; + if (renamesibs) + { + setDoSibRenamingPos(*info[varphi[idx]]); + } + + psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta1); + psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta2); + DELETE(theta1); + DELETE(theta2); + NOCOPY_INPLACE_UNION(psi1, psi2); + + psi = psi1; + } + + return psi; + } //End of convertFormulaToCNFNegXORAux() //######################################## //######################################## // utilities for reclaiming memory. - void CNFMgr::reduceMemoryFootprintPos(const ASTNode& varphi) - { - CNFInfo* x = info[varphi]; - if (sharesPos(*x) == 1) - { - DELETE(x->clausespos); - x->clausespos = NULL; - if (x->clausesneg == NULL) - { - delete x; - info.erase(varphi); - } - } - } //End of reduceMemoryFootprintPos() + void CNFMgr::reduceMemoryFootprintPos(const ASTNode& varphi) + { + CNFInfo* x = info[varphi]; + if (sharesPos(*x) == 1) + { + DELETE(x->clausespos); + x->clausespos = NULL; + if (x->clausesneg == NULL) + { + delete x; + info.erase(varphi); + } + } + } //End of reduceMemoryFootprintPos() - void CNFMgr::reduceMemoryFootprintNeg(const ASTNode& varphi) - { - CNFInfo* x = info[varphi]; - if (sharesNeg(*x) == 1) - { - DELETE(x->clausesneg); - x->clausesneg = NULL; - if (x->clausespos == NULL) - { - delete x; - info.erase(varphi); - } - } - } //End of reduceMemoryFootprintNeg() + void CNFMgr::reduceMemoryFootprintNeg(const ASTNode& varphi) + { + CNFInfo* x = info[varphi]; + if (sharesNeg(*x) == 1) + { + DELETE(x->clausesneg); + x->clausesneg = NULL; + if (x->clausespos == NULL) + { + delete x; + info.erase(varphi); + } + } + } //End of reduceMemoryFootprintNeg() //######################################## //######################################## - ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi) - { - ASTNode* psi; + ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi) + { + ASTNode* psi; - if (store.find(varphi) != store.end()) - { - psi = store[varphi]; - } - else - { - psi = new ASTNode(varphi); - store[varphi] = psi; - } + if (store.find(varphi) != store.end()) + { + psi = store[varphi]; + } + else + { + psi = new ASTNode(varphi); + store[varphi] = psi; + } - return psi; - } //End of ASTNodeToASTNodePtr() + return psi; + } //End of ASTNodeToASTNodePtr() //######################################## //######################################## - void CNFMgr::cleanup(const ASTNode& varphi) - { - delete info[varphi]->clausespos; - CNFInfo* toDelete = info[varphi]; // get the thing to delete. - info.erase(varphi); // remove it from the hashtable - delete toDelete; + void CNFMgr::cleanup(const ASTNode& varphi) + { + delete info[varphi]->clausespos; + CNFInfo* toDelete = info[varphi]; // get the thing to delete. + info.erase(varphi); // remove it from the hashtable + delete toDelete; - ASTNodeToCNFInfoMap::const_iterator it1 = info.begin(); - for (; it1 != info.end(); it1++) - { - CNFInfo* x = it1->second; - if (x->clausespos != NULL) - { - DELETE(x->clausespos); - } - if (x->clausesneg != NULL) - { - if (!isTerm(*x)) - { - DELETE(x->clausesneg); - } - } - delete x; - } + ASTNodeToCNFInfoMap::const_iterator it1 = info.begin(); + for (; it1 != info.end(); it1++) + { + CNFInfo* x = it1->second; + if (x->clausespos != NULL) + { + DELETE(x->clausespos); + } + if (x->clausesneg != NULL) + { + if (!isTerm(*x)) + { + DELETE(x->clausesneg); + } + } + delete x; + } - info.clear(); - } //End of cleanup() + info.clear(); + } //End of cleanup() //######################################## //######################################## // constructor - CNFMgr::CNFMgr(STPMgr *bmgr) - { - bm = bmgr; - } + CNFMgr::CNFMgr(STPMgr *bmgr) + { + bm = bmgr; + } - //######################################## - //######################################## - // destructor + //######################################## + //######################################## + // destructor CNFMgr::~CNFMgr() { ASTNodeToASTNodePtrMap::const_iterator it1 = store.begin(); for (; it1 != store.end(); it1++) { - delete it1->second; + delete it1->second; } store.clear(); } - //######################################## - //######################################## - // top-level conversion function - - ClauseList* CNFMgr::convertToCNF(const ASTNode& varphi) - { - bm->GetRunTimes()->start(RunTimes::CNFConversion); - scanFormula(varphi, true); - ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); - ClauseList* defs = SINGLETON(dummy_true_var); - convertFormulaToCNF(varphi, defs); - ClauseList* top = info[varphi]->clausespos; - defs->insert(defs->begin() + 1, top->begin(), top->end()); - - cleanup(varphi); - bm->GetRunTimes()->stop(RunTimes::CNFConversion); - return defs; - }//End of convertToCNF() - - void CNFMgr::DELETE(ClauseList* varphi) - { - ClauseList::const_iterator it = varphi->begin(); - for (; it != varphi->end(); it++) - { - delete *it; - } + //######################################## + //######################################## + // top-level conversion function + + ClauseList* CNFMgr::convertToCNF(const ASTNode& varphi) + { + bm->GetRunTimes()->start(RunTimes::CNFConversion); + scanFormula(varphi, true); + ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); + ClauseList* defs = SINGLETON(dummy_true_var); + convertFormulaToCNF(varphi, defs); + ClauseList* top = info[varphi]->clausespos; + defs->insert(defs->begin() + 1, top->begin(), top->end()); + + cleanup(varphi); + bm->GetRunTimes()->stop(RunTimes::CNFConversion); + return defs; + }//End of convertToCNF() + + void CNFMgr::DELETE(ClauseList* varphi) + { + ClauseList::const_iterator it = varphi->begin(); + for (; it != varphi->end(); it++) + { + delete *it; + } - delete varphi; - } //End of DELETE() + delete varphi; + } //End of DELETE() } // end namespace BEEV diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 57d6a3a..993b09b 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -76,7 +76,9 @@ namespace BEEV satSolverClause.capacity((*i)->size()); //now iterate through the internals of the ASTclause itself - vector::const_iterator j = (*i)->begin(), jend = (*i)->end(); + vector::const_iterator j = (*i)->begin(); + vector::const_iterator jend = (*i)->end(); + //j is a disjunct in the ASTclause (*i) for (; j != jend; j++) { @@ -107,7 +109,7 @@ namespace BEEV bm->GetRunTimes()->stop(RunTimes::SendingToSAT); return false; } - } + } bm->GetRunTimes()->stop(RunTimes::SendingToSAT); @@ -120,8 +122,8 @@ namespace BEEV //PrintActivityLevels_Of_SATVars("Before SAT:",newS); //ChangeActivityLevels_Of_SATVars(newS); - //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS); - //newS.solve(); + //PrintActivityLevels_Of_SATVars("Before SAT and after initial + //bias:",newS); newS.solve(); bm->GetRunTimes()->start(RunTimes::Solving); newS.solve(); @@ -136,8 +138,9 @@ namespace BEEV return false; } //end of toSATandSolve() - // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying assignment. - // Returns ASTTrue if true, ASTFalse if false or undefined. + // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying + // assignment. Returns ASTTrue if true, ASTFalse if false or + // undefined. ASTNode ToSAT::SymbolTruthValue(MINISAT::Solver &newS, ASTNode form) { MINISAT::Var satvar = _ASTNode_to_SATVar_Map[form]; diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index 92a7ad4..05e9ed0 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -36,10 +36,10 @@ namespace BEEV // variable in ASTClause a new MINISAT::Var is created (these vars // typedefs for ints) typedef HASHMAP< - ASTNode, - MINISAT::Var, - ASTNode::ASTNodeHasher, - ASTNode::ASTNodeEqual> ASTtoSATMap; + ASTNode, + MINISAT::Var, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTtoSATMap; ASTtoSATMap _ASTNode_to_SATVar_Map; // MAP: This is a map from MINISAT::Vars to ASTNodes @@ -71,7 +71,7 @@ namespace BEEV //looksup a MINISAT var from the minisat-var memo-table. if none //exists, then creates one. Treat the result as const. MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, - const ASTNode& n); + const ASTNode& n); // Evaluates bitblasted formula in satisfying assignment ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form); @@ -98,8 +98,8 @@ namespace BEEV // Bitblasts, CNF conversion and calls toSATandSolve() bool CallSAT(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input); + const ASTNode& modified_input, + const ASTNode& original_input); // Converts the clause to SAT and calls SAT solver bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll);