From: vijay_ganesh Date: Wed, 2 Sep 2009 22:32:47 +0000 (+0000) Subject: Removed lots of useless code. The FOR loop code is still being written X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5b27e55ac23d4d19412d6f29997415a22996a58c;p=francis%2Fstp.git Removed lots of useless code. The FOR loop code is still being written git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@168 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/README b/README index 5e619d2..4463d6e 100644 --- a/README +++ b/README @@ -21,6 +21,11 @@ See LICENSE file in the home dir of this program WEBSITE ------- +http://sites.google.com/site/stpfastprover + + +SOURCEFORGE REPOSITORY +---------------------- http://sourceforge.net/projects/stp-fast-prover diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 9260e42..04c7af5 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -3,14 +3,11 @@ #information always use full screen mode to view/edit this file in #emacs -#do not edit -#OPTIONS1 = -DNATIVE_C_ARITH - #OPTIMIZE = -g -pg # Debugging and gprof-style profiling #OPTIMIZE = -g # Debugging OPTIMIZE = -O3 -DNDEBUG # Maximum optimization -CFLAGS_BASE = $(OPTIMIZE) $(OPTIONS1) +CFLAGS_BASE = $(OPTIMIZE) # You can compile using make STATIC=true to compile a statically linked executable # Note that you should execute liblinks.sh first. ifdef STATIC diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index ec02c4f..4ecef9d 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -390,7 +390,6 @@ ASTNode BeevMgr::CreateSymbol(const char * const name) return n; } -#ifndef NATIVE_C_ARITH //Create a ASTBVConst node ASTNode BeevMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst) { @@ -588,121 +587,6 @@ CBV const ASTNode::GetBVConst() const FatalError("GetBVConst: non bitvector-constant: ", *this); return ((ASTBVConst *) _int_node_ptr)->GetBVConst(); } -#else -//Create a ASTBVConst node -ASTNode BeevMgr::CreateBVConst(const unsigned int width, - const unsigned long long int bvconst) -{ - if(width > 64 || width <= 0) - FatalError("Fatal Error: CreateBVConst: trying to create a bvconst of width:", ASTUndefined, width); - - //64 bit mask - unsigned long long int mask = 0xffffffffffffffffLL; - mask = mask >> (64 - width); - - unsigned long long int bv = bvconst; - bv = bv & mask; - - ASTBVConst temp_bvconst(bv, *this); - temp_bvconst._value_width = width; - ASTNode n(LookupOrCreateBVConst(temp_bvconst)); - n.SetValueWidth(width); - n.SetIndexWidth(0); - return n; -} -//Create a ASTBVConst node from std::string -ASTNode BeevMgr::CreateBVConst(const char* strval, int base) -{ - if(!(base == 2 || base == 16 || base == 10)) - FatalError("CreateBVConst: This base is not supported: ", ASTUndefined, base); - - if(10 != base) - { - unsigned int width = (base == 2) ? strlen(strval) : strlen(strval)*4; - unsigned long long int val = strtoull(strval, NULL, base); - ASTNode bvcon = CreateBVConst(width, val); - return bvcon; - } - else - { - //this is an ugly hack to accomodate SMTLIB format - //restrictions. SMTLIB format represents bitvector - //constants in base 10 (what a terrible idea, but i - //have no choice but to support it), and make an - //implicit assumption that the length is 32 (another - //terrible idea). - unsigned width = 32; - unsigned long long int val = strtoull(strval, NULL, base); - ASTNode bvcon = CreateBVConst(width, val); - return bvcon; - } -} - -//To ensure unique BVConst nodes, lookup the node in unique-table -//before creating a new one. -ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) -{ - ASTBVConst *s_ptr = &s; // it's a temporary key. - - // Do an explicit lookup to see if we need to create a copy of the - // string. - ASTBVConstSet::const_iterator it; - if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) - { - // Make a new ASTBVConst. Can cast the iterator to non-const -- - // carefully. - unsigned int width = s_ptr->_value_width; - ASTBVConst * s_ptr1 = new ASTBVConst(s_ptr->GetBVConst(), *this); - s_ptr1->SetNodeNum(NewNodeNum()); - s_ptr1->_value_width = width; - pair p = _bvconst_unique_table.insert(s_ptr1); - return *p.first; - } - else - // return BVConst found in table. - return *it; -} - -// Inline because we need to wait until unique_table is defined -void ASTBVConst::CleanUp() -{ - // cout << "Deleting node " << this->GetNodeNum() << endl; - _bm._bvconst_unique_table.erase(this); - delete this; -} - -// Get the value of bvconst from a bvconst. It's an error if kind -// != BVCONST -unsigned long long int ASTNode::GetBVConst() const -{ - if(GetKind() != BVCONST) - FatalError("GetBVConst: non bitvector-constant: ", *this); - return ((ASTBVConstTmp *) _int_node_ptr)->GetBVConst(); -} - -ASTNode BeevMgr::CreateZeroConst(unsigned width) -{ - return CreateBVConst(width,0); -} - -ASTNode BeevMgr::CreateOneConst(unsigned width) -{ - return CreateBVConst(width,1); -} - -ASTNode BeevMgr::CreateTwoConst(unsigned width) -{ - return CreateBVConst(width,2); -} - -ASTNode BeevMgr::CreateMaxConst(unsigned width) -{ - std::string s; - s.insert(s.end(),width,'1'); - return CreateBVConst(s.c_str(),2); -} - -#endif // FIXME: _name is now a constant field, and this assigns to it // because it tries not to copy the string unless it needs to. How diff --git a/src/AST/AST.h b/src/AST/AST.h index 58602ab..dc315ca 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -38,9 +38,7 @@ //#include "../sat/unsound/UnsoundSimpSolver.h" #include "../sat/core/SolverTypes.h" #include -#ifndef NATIVE_C_ARITH #include "../constantbv/constantbv.h" -#endif /***************************************************************************** * LIST OF CLASSES DECLARED IN THIS FILE: @@ -91,8 +89,12 @@ class ASTNode friend class ASTInterior; friend class vector ; //Print the arguments in lisp format. - friend ostream &LispPrintVec(ostream &os, const ASTVec &v, int indentation = 0); - friend ostream &LispPrintVecSpecial(ostream &os, const vector &v, int indentation = 0); + friend ostream &LispPrintVec(ostream &os, + const ASTVec &v, + int indentation = 0); + friend ostream &LispPrintVecSpecial(ostream &os, + const vector &v, + int indentation = 0); private: // FIXME: make this into a reference? @@ -267,11 +269,7 @@ public: const char * const GetName() const; //Get the BVCONST value -#ifndef NATIVE_C_ARITH const CBV GetBVConst() const; -#else - unsigned long long int GetBVConst() const; -#endif /*ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0)) * @@ -675,9 +673,6 @@ public: /***************************************************************************/ /* Class ASTBVConst: Class to represent internals of a bitvectorconst */ /***************************************************************************/ - -#ifndef NATIVE_C_ARITH - class ASTBVConst: public ASTInternal { friend class BeevMgr; @@ -802,233 +797,21 @@ public: } }; //End of ASTBVConst - -//FIXME This function is DEPRECATED -//Do not use in the future -inline unsigned int GetUnsignedConst(const ASTNode n) -{ - if (sizeof(unsigned int) * 8 <= n.GetValueWidth()) - { - // It may only contain a small value in a bit type, which fits nicely into an unsigned int. - // This is common for functions like: bvshl(bv1[128], bv1[128]) - // where both operands have the same type. - signed long maxBit = CONSTANTBV::Set_Max(n.GetBVConst()); - if (maxBit >= ((signed long) sizeof(unsigned int)) * 8) - { - n.LispPrint(cerr); //print the node so they can find it. - FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int"); - } - } - return (unsigned int) *((unsigned int *) n.GetBVConst()); -} -#else -class ASTBVConst : public ASTInternal -{ - friend class BeevMgr; - friend class ASTNode; - friend class ASTNodeHasher; - friend class ASTNodeEqual; - -private: - // the bitvector contents. bitvector contents will be in two - // modes. one mode where all bitvectors are NATIVE and in this - // mode we use native unsigned long long int to represent the - // 32/64 bitvectors. The other for arbitrary length bitvector - // operations. - const unsigned long long int _bvconst; - - class ASTBVConstHasher - { - public: - size_t operator() (const ASTBVConst * bvc) const - { - //Thomas Wang's 64 bit Mix Function - unsigned long long int key(bvc->_bvconst); - key += ~(key << 32); - key ^= (key >> 22); - key += ~(key << 13); - key ^= (key >> 8); - key += (key << 3); - key ^= (key >> 15); - key += ~(key << 27); - key ^= (key >> 31); - - size_t return_key = key; - return return_key; - }; - }; - - class ASTBVConstEqual - { - public: - bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const - { - return ((bvc1->_bvconst == bvc2->_bvconst) - && (bvc1->_value_width == bvc2->_value_width)); - } - }; - - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); -public: - // Default constructor - ASTBVConst(const unsigned long long int bv, BeevMgr &bm) : - ASTInternal(BVCONST, bm), _bvconst(bv) - { - } - - // Copy constructor. FIXME: figure out how this is supposed to - // work. - ASTBVConst(const ASTBVConst &sym) : - ASTInternal(sym._kind, sym._children, sym._bm), - _bvconst(sym._bvconst) - { - _value_width = sym._value_width; - } - - // Destructor (does nothing, but is declared virtual here) - virtual ~ASTBVConst() - {} - - friend bool operator==(const ASTBVConst &sym1, const ASTBVConst &sym2) - { - return ((sym1._bvconst == sym2._bvconst) && - (sym1._value_width == sym2._value_width)); - } - - // Print function for bvconst -- return _bvconst value in binary format - virtual void nodeprint(ostream& os, bool c_friendly = false) - { - string s = "0bin"; - unsigned long long int bitmask = 0x8000000000000000LL; - bitmask = bitmask >> (64-_value_width); - - for (; bitmask > 0; bitmask >>= 1) - s += (_bvconst & bitmask) ? '1' : '0'; - os << s; - } - - unsigned long long int GetBVConst() const - { return _bvconst;} -}; //End of ASTBVConst - -//return value of bvconst -inline unsigned int GetUnsignedConst(const ASTNode n) -{ - if(32 < n.GetValueWidth()) - FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:"); - return (unsigned int)n.GetBVConst(); -} -#endif -/* - #else - // the bitvector contents. bitvector contents will be in two - // modes. one mode where all bitvectors are NATIVE and in this mode - // we use native unsigned long long int to represent the 32/64 - // bitvectors. The other for arbitrary length bitvector operations. - - //BVCONST defined for arbitrary length bitvectors - class ASTBVConst : public ASTInternal{ - friend class BeevMgr; - friend class ASTNode; - friend class ASTNodeHasher; - friend class ASTNodeEqual; - - private: - const char * const _bvconst; - - class ASTBVConstHasher{ - public: - size_t operator() (const ASTBVConst * bvc) const{ - hash h; - return h(bvc->_bvconst); - }; - }; - - class ASTBVConstEqual{ - public: - bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const { - if(bvc1->_value_width != bvc2->_value_width) - return false; - return (0 == strncmp(bvc1->_bvconst,bvc2->_bvconst,bvc1->_value_width)); - } - }; - - ASTBVConst(const char * bv, BeevMgr &bm) : - ASTInternal(BVCONST, bm), _bvconst(bv) { - //_value_width = strlen(bv); - } - - friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){ - if(bvc1._value_width != bvc2._value_width) - return false; - return (0 == strncmp(bvc1._bvconst,bvc2._bvconst,bvc1._value_width)); - } - - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); - - // Print function for bvconst -- return _bvconst value in binary format - virtual void nodeprint(ostream& os) { - if(_value_width%4 == 0) { - unsigned int * iii = CONSTANTBV::BitVector_Create(_value_width,true); - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_from_Bin(iii,(unsigned char*)_bvconst); - //error printing - if(0 != e) { - os << "nodeprint: BVCONST : wrong hex value: " << BitVector_Error(e); - FatalError(""); - } - unsigned char * ccc = CONSTANTBV::BitVector_to_Hex(iii); - os << "0hex" << ccc; - CONSTANTBV::BitVector_Destroy(iii); - } - else { - std::string s(_bvconst,_value_width); - s = "0bin" + s; - os << s; - } - } - - // Copy constructor. - ASTBVConst(const ASTBVConst &sym) : ASTInternal(sym._kind, sym._children, sym._bm),_bvconst(sym._bvconst) { - //checking if the input is in the correct format - for(unsigned int jj=0;jj ASTNodeMap; +typedef hash_map ASTNodeMap; -typedef hash_map ASTNodeCountMap; +typedef hash_map ASTNodeCountMap; // Function to dump contents of ASTNodeMap @@ -1038,9 +821,13 @@ ostream &operator<<(ostream &os, const ASTNodeMap &nmap); Typedef ASTNodeSet: This is a hash set of ASTNodes. Very useful for representing things like "visited nodes" ***************************************************************************/ -typedef hash_set ASTNodeSet; +typedef hash_set ASTNodeSet; -typedef hash_multiset ASTNodeMultiSet; +typedef hash_multiset ASTNodeMultiSet; //external parser table for declared symbols. //FIXME: move to a more appropriate place @@ -1529,12 +1316,12 @@ public: return n; } - ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg); + ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL); ASTNode SimplifyFormula_TopLevel(const ASTNode& a, bool pushNeg); - ASTNode SimplifyFormula(const ASTNode& a, bool pushNeg); ASTNode SimplifyTerm_TopLevel(const ASTNode& b); - ASTNode SimplifyTerm(const ASTNode& a); - ASTNode SimplifyTermAux(const ASTNode& a); + + ASTNode SimplifyFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyTerm(const ASTNode& inputterm, ASTNodeMap* VarConstMap=NULL); void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); void BuildReferenceCountMap(const ASTNode& b); @@ -1547,32 +1334,35 @@ private: ASTNodeMap MultInverseMap; - // 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. + // 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; public: - ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL); ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2); - ASTNode ITEOpt_InEqs(const ASTNode& in1); + ASTNode ITEOpt_InEqs(const ASTNode& in1, ASTNodeMap* VarConstMap=NULL); ASTNode PullUpITE(const ASTNode& in); ASTNode RemoveContradictionsFromAND(const ASTNode& in); ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3); ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2); ASTNode CreateSimplifiedINEQ(Kind k, const ASTNode& a0, const ASTNode& a1, bool pushNeg); - ASTNode SimplifyNotFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyAndOrFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyXorFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyNandFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyNorFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyImpliesFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyIffFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyIteFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyForFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyNotFormula(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 SimplifyNandFormula(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 SimplifyIffFormula(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 FlattenOneLevel(const ASTNode& a); ASTNode FlattenAndOr(const ASTNode& a); ASTNode CombineLikeTerms(const ASTNode& a); @@ -1590,10 +1380,17 @@ public: int CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input); int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input); int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); - //creates array write axiom only for the input term or formula, if + + int SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input); + int Expand_A_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap); + ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody, + ASTNodeMap* VarConstMap); + + //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); + ASTNode Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, + const ASTNode& array_newname); ASTVec ArrayWrite_RemainingAxioms; //variable indicates that counterexample will now be checked by //the counterexample checker, and hence simplifyterm must switch @@ -1771,8 +1568,8 @@ private: //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); - ASTNode ReadOverWrite_To_ITE(const ASTNode& term); + ASTNode SimplifyWrites_InPlace(const ASTNode& term, ASTNodeMap* VarConstMap=NULL); + ASTNode ReadOverWrite_To_ITE(const ASTNode& term, ASTNodeMap* VarConstMap=NULL); ASTNode NewArrayVar(unsigned int index, unsigned int value); ASTNode NewVar(unsigned int valuewidth); @@ -1783,6 +1580,10 @@ private: //terms ASTNodeMap NewName_ReadOverWrite_Map; + //For finiteloop construct + // + //A list of all finiteloop constructs in the input formula + ASTVec List_Of_FiniteLoops; public: //print the STP solver output void PrintOutput(bool true_iff_valid); @@ -1885,6 +1686,10 @@ public: //prints statistics for the ASTNode. can add a prefix string c void ASTNodeStats(const char * c, const ASTNode& a); + //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); @@ -1989,6 +1794,30 @@ public: } }; -} -; // end namespace BEEV +//Return the unsigned constant value of the input 'n' +inline unsigned int GetUnsignedConst(const ASTNode n) +{ + if(BVCONST != n.GetKind()){ + FatalError("GetUnsignedConst: cannot extract an "\ + "unsigned value from a non-bvconst"); + } + + if (sizeof(unsigned int) * 8 <= n.GetValueWidth()) + { + // It may only contain a small value in a bit type, + // which fits nicely into an unsigned int. This is + // common for functions like: bvshl(bv1[128], + // bv1[128]) where both operands have the same type. + signed long maxBit = CONSTANTBV::Set_Max(n.GetBVConst()); + if (maxBit >= ((signed long) sizeof(unsigned int)) * 8) + { + n.LispPrint(cerr); //print the node so they can find it. + FatalError("GetUnsignedConst: cannot convert bvconst "\ + "of length greater than 32 to unsigned int"); + } + } + return (unsigned int) *((unsigned int *) n.GetBVConst()); +} //end of GetUnsignedConst + +}; // end namespace BEEV #endif diff --git a/src/AST/BitBlast.cpp b/src/AST/BitBlast.cpp index 4816064..ad882b6 100644 --- a/src/AST/BitBlast.cpp +++ b/src/AST/BitBlast.cpp @@ -549,18 +549,12 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) case BVCONST: { ASTVec tmp_res(num_bits); -#ifndef NATIVE_C_ARITH CBV bv = term.GetBVConst(); for (unsigned int i = 0; i < num_bits; i++) { - tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv, i) ? ASTTrue : ASTFalse; + tmp_res[i] = + CONSTANTBV::BitVector_bit_test(bv, i) ? ASTTrue : ASTFalse; } -#else - const unsigned long long int c = term.GetBVConst(); - unsigned long long int bitmask = 0x00000000000000001LL; - for (unsigned int i = 0; i < num_bits; i++, bitmask <<= 1) - tmp_res[i] = ((c & (bitmask)) ? ASTTrue : ASTFalse); -#endif result = CreateNode(BOOLVEC, tmp_res); break; } diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp index eb1f24f..4045087 100644 --- a/src/AST/ToCNF.cpp +++ b/src/AST/ToCNF.cpp @@ -1780,7 +1780,8 @@ void BeevMgr::DeleteClauseList(BeevMgr::ClauseList *cllp) delete cllp; } -int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input) +int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, + const ASTNode& q, const ASTNode& orig_input) { ASTNode BBFormula = BBForm(q); CNFMgr* cm = new CNFMgr(this); diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index 84bdde3..8615ece 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -1421,114 +1421,104 @@ int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& return 2; } //end of SATBased_ArrayWriteRefinement -#ifdef PHONY -//Check result after calling SAT FIXME: Document arguments in -//comments, and give them meaningful names. How is anyone supposed -//to know what "q" is? -int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, - const ASTNode& q, const ASTNode& orig_input) +//Expands all finite-for-loops using counterexample-guided +//abstraction-refinement. +int BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, + const ASTNode& orig_input) { - //Bitblast, CNF, call SAT now - ASTNode BBFormula = BBForm(q); - //ASTNodeStats("after bitblasting", BBFormula); - //ClauseList *cllp = ToCNF(BBFormula); - // if(stats && print_nodes) { - // cout << "\nClause list" << endl; - // PrintClauseList(cout, *cllp); - // cerr << "\n finished printing clauselist\n"; - // } - - //**************************************** - // TOCNF CONVERSION - //**************************************** - CNFMgr *cm = new CNFMgr(this); - - ClauseList* cllp = new ClauseList(); - cm->NOCOPY_INPLACE_UNION(cllp, cm->SINGLETON(cm->dummy_true_var)); - cm->CountSharesPos(BBFormula); - cm->ToCNFModRenamingPos(BBFormula); - cm->INPLACE_UNION(cllp, *((cm->ClausesPos)[BBFormula])); - cm->AddDefs(cllp); - //**************************************** - // TOCNF CONVERSION - //**************************************** - - bool sat = toSATandSolve(newS,*cllp); - // Temporary debugging call. - // CheckBBandCNF(newS, BBFormula); - - //**************************************** - // TOCNF CLEANUP - //**************************************** - cm->CLEAR(); - cm->DELETE(cllp); - delete cm; - //**************************************** - // TOCNF CLEANUP - //**************************************** + /* + * For each 'finiteloop' in the global list 'List_Of_FiniteLoops' + * + * Expand_A_FiniteLoop(finiteloop); + * + * The 'Expand_A_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. + */ +} - if(!sat) - { - PrintOutput(true); - return 1; - } - else if(newS.okay()) - { - CounterExampleMap.clear(); - ConstructCounterExample(newS); - if (stats && print_nodes) - { - PrintSATModel(newS); - } - //check if the counterexample is good or not - ComputeFormulaMap.clear(); - if(counterexample_checking_during_refinement) - bvdiv_exception_occured = false; - ASTNode orig_result = ComputeFormulaUsingModel(orig_input); - if(!(ASTTrue == orig_result || ASTFalse == orig_result)) - FatalError("TopLevelSat: Original input must compute to true or false against model"); - - // if(!arrayread_refinement && !(ASTTrue == orig_result)) { - // print_counterexample = true; - // PrintCounterExample(true); - // FatalError("counterexample bogus : arrayread_refinement is switched off: " - // "EITHER all LA axioms have not been added OR bitblaster() or ToCNF()" - // "or satsolver() or counterexamplechecker() have a bug"); - // } - - // if the counterexample is indeed a good one, then return - // invalid - if(ASTTrue == orig_result) - { - CheckCounterExample(newS.okay()); - PrintOutput(false); - PrintCounterExample(newS.okay()); - PrintCounterExample_InOrder(newS.okay()); - return 0; - } - // counterexample is bogus: flag it +int BeevMgr::Expand_A_FiniteLoop(const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap) { + /* + * 'finiteloop' is the finite loop to be expanded + * + * Every finiteloop has three parts: + * + * 1) Parameter initialization + * + * 2) Parameter limit value + * + * 3) Formula Body (This can be a NESTED for loop) + * + * 4) Increment formula + * + * Each entry of the parameter_stack contains the following: + * + * 1. Current parameter name + * + * 2. Initial value of the parameter + * + * 3. Limit value of the parameter + * + * 4. Increment value + * + * If parameter_stack is empty then it means that we are at the + * start of expanding this finite loop + * + * Nested FORs are allowed, but only the innermost loop can have a + * formula in it + * + * STEPS: + * + * 0. Populate the top of the parameter stack with 'finiteloop' + * parameter initial, limit and increment values + * + * 1. If formulabody in 'finiteloop' is another for loop, then + * recurse + * + * 2. Else if current parameter value is less than limit value then + * + * Instantiate a singleformula + * + * Check if the formula is true in the current model + * + * If true, discard it + * + * If false, add it to the SAT solver to get a new model. Make + * sure to update array index tables to facilitate array + * read refinement later. + * + * 3. If control reaches here, it means one of the following + * possibilities (We have instantiated all relevant formulas by + * now): + * + * 3.1: We have UNSAT. Return UNSAT + * + * 3.2: We have SAT, and it is indeed a satisfying model + */ + + //0th element of FOR-construct stores the initial parameter value + int paramInitValue = finiteloop[0].GetUnsignedConst(); +} - else - { - if(stats && print_nodes) - { - cout << "Supposedly bogus one: \n"; - bool tmp = print_counterexample; - print_counterexample = true; - PrintCounterExample(true); - print_counterexample = tmp; - } +ASTNode BeevMgr::FiniteLoop_Extract_SingleFormula(const ASTNode& formulabody, + ASTNodeMap* VarToConstantMap) +{ + /* + * Takes a formula 'formulabody', and simplifies it against + * variable-to-constant map 'VarToConstantMap' + */ + return SimplifyFormula(formulabody, VarToConstantMap); +} - return 2; - } - } - else - { - PrintOutput(true); - return -100; - } -} //end of CALLSAT_ResultCheck -#endif //FUNCTION: this function accepts a boolvector and returns a BVConst ASTNode BeevMgr::BoolVectoBVConst(hash_map * w, unsigned int l) @@ -1549,55 +1539,6 @@ ASTNode BeevMgr::BoolVectoBVConst(hash_map * w, unsigned int l) return CreateBVConst(cc.c_str(), 2); } -/* - void BeevMgr::PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS) { - if(!print_sat_varorder) - return; - - ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin(); - ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end(); - - cout << init_msg; - cout << ": Printing activity levels of variables\n"; - for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){ - cout << (it->second) << " : "; - (it->first).PL_Print(cout,0); - cout << " : "; - cout << newS.returnActivity(it->second) << endl; - } - } - - //this function biases the activity levels of MINISAT variables. - void BeevMgr::ChangeActivityLevels_Of_SATVars(MINISAT::Solver& newS) { - if(!variable_activity_optimize) - return; - - ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin(); - ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end(); - - unsigned int index=1; - double base = 2; - for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){ - ASTNode n = it->first; - - if(BVGETBIT == n.GetKind() || NOT == n.GetKind()) { - if(BVGETBIT == n.GetKind()) - index = GetUnsignedConst(n[1]); - else if (NOT == n.GetKind() && BVGETBIT == n[0].GetKind()) - index = GetUnsignedConst(n[0][1]); - else - index = 0; - double initial_activity = pow(base,(double)index); - newS.updateInitialActivity(it->second,initial_activity); - } - else { - double initial_activity = pow(base,pow(base,(double)index)); - newS.updateInitialActivity(it->second,initial_activity); - } - } - } - */ - //This function prints the output of the STP solver void BeevMgr::PrintOutput(bool true_iff_valid) { diff --git a/src/bitvec/consteval.cpp b/src/bitvec/consteval.cpp index 12860c9..2a54a80 100644 --- a/src/bitvec/consteval.cpp +++ b/src/bitvec/consteval.cpp @@ -20,7 +20,6 @@ static void BVConstEvaluatorError(CONSTANTBV::ErrCode e, const ASTNode& t) FatalError(ss.c_str(), t); } -#ifndef NATIVE_C_ARITH ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) { ASTNode OutputNode; @@ -567,763 +566,5 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) UpdateSolverMap(t, OutputNode); //UpdateSimplifyMap(t,OutputNode,false); return OutputNode; -} -#else -//accepts 64 bit BVConst and sign extends it -static unsigned long long int SXBVConst64(const ASTNode& t) -{ - unsigned long long int c = t.GetBVConst(); - unsigned int len = t.GetValueWidth(); - - unsigned long long int mask = 1; - mask = mask << len-1; - - bool TopBit = (c & mask) ? true : false; - if(!TopBit) return c; - - unsigned long long int sign = 0xffffffffffffffffLL; - sign = sign << len-1; - - return (c | sign); -} - -//FIXME: Ideally I would like the ASTNodes to be able to operate on -//themselves (add, sub, concat, etc.) rather than doing a -//GetBVConst() and then do the operation externally. For now, -//this is the fastest path to completion. -ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) -{ - //cerr << "inside begin bcconstevaluator: " << t << endl; - - ASTNode OutputNode; - if(CheckSolverMap(t,OutputNode)) - return OutputNode; - OutputNode = ASTUndefined; - - Kind k = t.GetKind(); - unsigned long long int output = 0; - unsigned inputwidth = t.GetValueWidth(); - ASTNode t0 = ASTUndefined; - ASTNode t1 = ASTUndefined; - if(2 == t.Degree()) - { - t0 = BVConstEvaluator(t[0]); - t1 = BVConstEvaluator(t[1]); - } - switch(k) - { - case READ: - case UNDEFINED: - case WRITE: - case SYMBOL: - cerr << t; - FatalError("BVConstEvaluator: term is not a constant-term",t); - break; - case BVCONST: - return t; - break; - case BVNEG: - //compute bitwise negation in C - output = ~(BVConstEvaluator(t[0]).GetBVConst()); - break; - case BVSX: - output = SXBVConst64(BVConstEvaluator(t[0])); - break; - case BVAND: - output = t0.GetBVConst() & t1.GetBVConst(); - break; - case BVOR: - output = t0.GetBVConst() | t1.GetBVConst(); - break; - case BVXOR: - output = t0.GetBVConst() ^ t1.GetBVConst(); - break; - case BVSUB: - output = t0.GetBVConst() - t1.GetBVConst(); - break; - case BVUMINUS: - output = ~(BVConstEvaluator(t[0]).GetBVConst()) + 1; - break; - case BVEXTRACT: - { - unsigned long long int val = BVConstEvaluator(t[0]).GetBVConst(); - unsigned int hi = GetUnsignedConst(BVConstEvaluator(t[1])); - unsigned int low = GetUnsignedConst(BVConstEvaluator(t[2])); - - if(!(0 <= hi <= 64)) - FatalError("ConstantEvaluator: hi bit in BVEXTRACT is > 32bits",t); - if(!(0 <= low <= hi <= 64)) - FatalError("ConstantEvaluator: low bit in BVEXTRACT is > 32bits or hi",t); - - //64 bit mask. - unsigned long long int mask1 = 0xffffffffffffffffLL; - mask1 >>= 64-(hi+1); - - //extract val[hi:0] - val &= mask1; - //extract val[hi:low] - val >>= low; - output = val; - break; - } - case BVCONCAT: - { - unsigned long long int q = BVConstEvaluator(t0).GetBVConst(); - unsigned long long int r = BVConstEvaluator(t1).GetBVConst(); - - unsigned int qlen = t[0].GetValueWidth(); - unsigned int rlen = t[1].GetValueWidth(); - unsigned int slen = t.GetValueWidth(); - if(!(0 < qlen + rlen <= 64)) - FatalError("BVConstEvaluator:" - "lengths of childnodes of BVCONCAT are > 64:",t); - - //64 bit mask for q - unsigned long long int qmask = 0xffffffffffffffffLL; - qmask >>= 64-qlen; - //zero the useless bits of q - q &= qmask; - - //64 bit mask for r - unsigned long long int rmask = 0xffffffffffffffffLL; - rmask >>= 64-rlen; - //zero the useless bits of r - r &= rmask; - - //concatenate - q <<= rlen; - q |= r; - - //64 bit mask for output s - unsigned long long int smask = 0xffffffffffffffffLL; - smask >>= 64-slen; - - //currently q has the output - output = q; - output &= smask; - break; - } - case BVMULT: - { - output = t0.GetBVConst() * t1.GetBVConst(); - - //64 bit mask - unsigned long long int mask = 0xffffffffffffffffLL; - mask = mask >> (64 - inputwidth); - output &= mask; - break; - } - case BVPLUS: - { - ASTVec c = t.GetChildren(); - for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) - output += BVConstEvaluator(*it).GetBVConst(); - - //64 bit mask - unsigned long long int mask = 0xffffffffffffffffLL; - mask = mask >> (64 -inputwidth); - output &= mask; - break; - } - case SBVDIV: - case SBVREM: - { - output = BVConstEvaluator(TranslateSignedDivMod(t)).GetBVConst(); - break; - } - case BVDIV: - { - if(0 == t1.GetBVConst()) - { - //if denominator is 0 then - // (if refinement is ON then output is set to 0) - // (else produce a fatal error) - if(counterexample_checking_during_refinement) - { - output = 0; - bvdiv_exception_occured = true; - break; - } - else - { - FatalError("BVConstEvaluator: divide by zero not allowed:",t); - } - } - - output = t0.GetBVConst() / t1.GetBVConst(); - //64 bit mask - unsigned long long int mask = 0xffffffffffffffffLL; - mask = mask >> (64 - inputwidth); - output &= mask; - break; - } - case BVMOD: - { - if(0 == t1.GetBVConst()) - { - //if denominator is 0 then - // (if refinement is ON then output is set to 0) - // (else produce a fatal error) - if(counterexample_checking_during_refinement) - { - output = 0; - bvdiv_exception_occured = true; - break; - } - else - { - FatalError("BVConstEvaluator: divide by zero not allowed:",t); - } - } - - output = t0.GetBVConst() % t1.GetBVConst(); - //64 bit mask - unsigned long long int mask = 0xffffffffffffffffLL; - mask = mask >> (64 - inputwidth); - output &= mask; - break; - } - case ITE: - if(ASTTrue == t[0]) - OutputNode = BVConstEvaluator(t[1]); - else if(ASTFalse == t[0]) - OutputNode = BVConstEvaluator(t[2]); - else - FatalError("BVConstEvaluator:" - "ITE condiional must be either TRUE or FALSE:",t); - break; - case EQ: - if(t0.GetBVConst() == t1.GetBVConst()) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case NEQ: - if(t0.GetBVConst() != t1.GetBVConst()) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - break; - case BVLT: - { - unsigned long long n0 = t0.GetBVConst(); - unsigned long long n1 = t1.GetBVConst(); - if(n0 < n1) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - case BVLE: - if(t0.GetBVConst() <= t1.GetBVConst()) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVGT: - if(t0.GetBVConst() > t1.GetBVConst()) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVGE: - if(t0.GetBVConst() >= t1.GetBVConst()) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVSLT: - { - signed long long int n0 = SXBVConst64(t0); - signed long long int n1 = SXBVConst64(t1); - if(n0 < n1) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - case BVSLE: - { - signed long long int n0 = SXBVConst64(t0); - signed long long int n1 = SXBVConst64(t1); - if(n0 <= n1) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - case BVSGT: - { - signed long long int n0 = SXBVConst64(t0); - signed long long int n1 = SXBVConst64(t1); - if(n0 > n1) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - case BVSGE: - { - signed long long int n0 = SXBVConst64(t0); - signed long long int n1 = SXBVConst64(t1); - if(n0 >= n1) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - default: - FatalError("BVConstEvaluator: The input kind is not supported yet:",t); - break; - } - - if(ASTTrue != OutputNode && ASTFalse != OutputNode) - OutputNode = CreateBVConst(inputwidth, output); - UpdateSolverMap(t,OutputNode); - //UpdateSimplifyMap(t,OutputNode,false); - return OutputNode; } //End of BVConstEvaluator -#endif -//In the block below is the old string based version -//It is included here as an easy reference while the current code is being worked on. - -/* - ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) { - ASTNode OutputNode; - Kind k = t.GetKind(); - - if(CheckSolverMap(t,OutputNode)) - return OutputNode; - OutputNode = t; - - unsigned int inputwidth = t.GetValueWidth(); - unsigned * output = CONSTANTBV::BitVector_Create(inputwidth,true); - unsigned * One = CONSTANTBV::BitVector_Create(inputwidth,true); - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_from_Bin(One, (unsigned char*)"1"); - //error printing - if(0 != e) { - std::string ss("BVConstEvaluator:"); - ss += (const char*)BitVector_Error(e); - FatalError(ss.c_str(), t); - } - - unsigned * Zero = CONSTANTBV::BitVector_Create(inputwidth,true); - unsigned int * iii = One; - unsigned int * jjj = Zero; - - //saving some typing. BVPLUS does not use these variables. if the - //input BVPLUS has two nodes, then we want to avoid setting these - //variables. - if(2 == t.Degree() && k != BVPLUS && k != BVCONCAT) { - iii = ConvertToCONSTANTBV(BVConstEvaluator(t[0]).GetBVConst()); - jjj = ConvertToCONSTANTBV(BVConstEvaluator(t[1]).GetBVConst()); - } - - char * cccc; - switch(k) { - case UNDEFINED: - case READ: - case WRITE: - case SYMBOL: - FatalError("BVConstEvaluator: term is not a constant-term",t); - break; - case BVCONST: - OutputNode = t; - break; - case BVNEG:{ - //AARON - if (iii != One) free(iii); - //AARON - - iii = ConvertToCONSTANTBV(BVConstEvaluator(t[0]).GetBVConst()); - CONSTANTBV::Set_Complement(output,iii); - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - break; - } - case BVSX: { - unsigned * out0 = ConvertToCONSTANTBV(BVConstEvaluator(t[0]).GetBVConst()); - unsigned t0_width = t[0].GetValueWidth(); - if(inputwidth == t0_width) { - cccc = (char *)CONSTANTBV::BitVector_to_Bin(out0); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - CONSTANTBV::BitVector_Destroy(out0); - } - else { - // FIXME: (Dill) I'm guessing that BitVector sign returns 1 if the - // number is positive, 0 if 0, and -1 if negative. But I'm only - // guessing. - signed int topbit_sign = (CONSTANTBV::BitVector_Sign(out0) < 0); - //out1 is the sign-extension bits - unsigned * out1 = CONSTANTBV::BitVector_Create(inputwidth-t0_width,true); - if(topbit_sign) - CONSTANTBV::BitVector_Fill(out1); - - //AARON - CONSTANTBV::BitVector_Destroy(output); - //AARON - - output = CONSTANTBV::BitVector_Concat(out1,out0); - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - CONSTANTBV::BitVector_Destroy(out0); - CONSTANTBV::BitVector_Destroy(out1); - } - break; - } - case BVAND: { - CONSTANTBV::Set_Intersection(output,iii,jjj); - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - break; - } - case BVOR: { - CONSTANTBV::Set_Union(output,iii,jjj); - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - break; - } - case BVXOR: { - CONSTANTBV::Set_ExclusiveOr(output,iii,jjj); - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - break; - } - case BVSUB: { - bool carry = false; - CONSTANTBV::BitVector_sub(output,iii,jjj,&carry); - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - break; - } - case BVUMINUS: { - bool carry = false; - - //AARON - if (iii != One) free(iii); - //AARON - - iii = ConvertToCONSTANTBV(BVConstEvaluator(t[0]).GetBVConst()); - CONSTANTBV::Set_Complement(output,iii); - CONSTANTBV::BitVector_add(output,output,One,&carry); - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - break; - } - case BVEXTRACT: { - string s(BVConstEvaluator(t[0]).GetBVConst()); - unsigned int hi = GetUnsignedConst(BVConstEvaluator(t[1])); - unsigned int low = GetUnsignedConst(BVConstEvaluator(t[2])); - - //length of substr to chop - unsigned int len = hi-low+1; - //distance from MSB - hi = s.size()-1 - hi; - string ss = s.substr(hi,len); - OutputNode = CreateBVConst(ss.c_str(),2); - break; - } - case BVCONCAT: { - string s(BVConstEvaluator(t[0]).GetBVConst()); - string r(BVConstEvaluator(t[1]).GetBVConst()); - - string q(s+r); - OutputNode = CreateBVConst(q.c_str(),2); - break; - } - case BVMULT: { - unsigned * output1 = CONSTANTBV::BitVector_Create(2*inputwidth,true); - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Multiply(output1,iii,jjj); - //error printing - if(0 != e) { - std::string ss("BVConstEvaluator:"); - ss += (const char*)BitVector_Error(e); - //destroy all the CONSTANTBV bitvectors - CONSTANTBV::BitVector_Destroy(iii); - CONSTANTBV::BitVector_Destroy(jjj); - CONSTANTBV::BitVector_Destroy(One); - CONSTANTBV::BitVector_Destroy(Zero); - FatalError(ss.c_str(), t); - } - - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output1); - std::string s(cccc); - - //AARON - free(cccc); - //AARON - - s = s.substr(inputwidth,inputwidth); - OutputNode = CreateBVConst(s.c_str(),2); - CONSTANTBV::BitVector_Destroy(output1); - break; - } - case BVPLUS: { - bool carry = false; - ASTVec c = t.GetChildren(); - for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) { - unsigned int * kk = ConvertToCONSTANTBV(BVConstEvaluator(*it).GetBVConst()); - CONSTANTBV::BitVector_add(output,output,kk,&carry); - carry = false; - CONSTANTBV::BitVector_Destroy(kk); - } - cccc = (char *)CONSTANTBV::BitVector_to_Bin(output); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - //AARON - - break; - } - case SBVDIV: - case SBVREM: { - OutputNode = BVConstEvaluator(TranslateSignedDivMod(t)); - break; - } - case BVDIV: { - unsigned * quotient = CONSTANTBV::BitVector_Create(inputwidth,true); - unsigned * remainder = CONSTANTBV::BitVector_Create(inputwidth,true); - // iii is dividend, jjj is the divisor - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient,iii,jjj,remainder); - - if(0 != e) { - //error printing - if(counterexample_checking_during_refinement) { - OutputNode = CreateZeroConst(inputwidth); - bvdiv_exception_occured = true; - break; - } - else { - std::string ss("BVConstEvaluator:"); - ss += (const char*)BitVector_Error(e); - //destroy all the CONSTANTBV bitvectors - CONSTANTBV::BitVector_Destroy(iii); - CONSTANTBV::BitVector_Destroy(jjj); - CONSTANTBV::BitVector_Destroy(One); - CONSTANTBV::BitVector_Destroy(Zero); - - //AARON - iii = jjj = One = Zero = NULL; - //AARON - - FatalError(ss.c_str(), t); - } - } //end of error printing - - cccc = (char *)CONSTANTBV::BitVector_to_Bin(quotient); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - CONSTANTBV::BitVector_Destroy(quotient); - CONSTANTBV::BitVector_Destroy(remainder); - //AARON - - break; - } - case BVMOD: { - unsigned * quotient = CONSTANTBV::BitVector_Create(inputwidth,true); - unsigned * remainder = CONSTANTBV::BitVector_Create(inputwidth,true); - // iii is dividend, jjj is the divisor - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient,iii,jjj,remainder); - - if(0 != e) { - //error printing - if(counterexample_checking_during_refinement) { - OutputNode = CreateZeroConst(inputwidth); - bvdiv_exception_occured = true; - break; - } - else { - std::string ss("BVConstEvaluator:"); - ss += (const char*)BitVector_Error(e); - //destroy all the CONSTANTBV bitvectors - CONSTANTBV::BitVector_Destroy(iii); - CONSTANTBV::BitVector_Destroy(jjj); - CONSTANTBV::BitVector_Destroy(One); - CONSTANTBV::BitVector_Destroy(Zero); - - //AARON - iii = jjj = One = Zero = NULL; - //AARON - - FatalError(ss.c_str(), t); - } - } //end of errory printing - - cccc = (char *)CONSTANTBV::BitVector_to_Bin(remainder); - OutputNode = CreateBVConst(cccc,2); - - //AARON - free(cccc); - CONSTANTBV::BitVector_Destroy(quotient); - CONSTANTBV::BitVector_Destroy(remainder); - //AARON - - break; - } - case ITE: - if(ASTTrue == t[0]) - OutputNode = BVConstEvaluator(t[1]); - else if(ASTFalse == t[0]) - OutputNode = BVConstEvaluator(t[2]); - else - FatalError("BVConstEvaluator: ITE condiional must be either TRUE or FALSE:",t); - break; - case EQ: - if(CONSTANTBV::BitVector_equal(iii,jjj)) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case NEQ: - if(!CONSTANTBV::BitVector_equal(iii,jjj)) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVLT: - if(-1 == CONSTANTBV::BitVector_Lexicompare(iii,jjj)) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVLE: { - int comp = CONSTANTBV::BitVector_Lexicompare(iii,jjj); - if(comp <= 0) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - case BVGT: - if(1 == CONSTANTBV::BitVector_Lexicompare(iii,jjj)) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVGE: { - int comp = CONSTANTBV::BitVector_Lexicompare(iii,jjj); - if(comp >= 0) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - case BVSLT: - if(-1 == CONSTANTBV::BitVector_Compare(iii,jjj)) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVSLE: { - signed int comp = CONSTANTBV::BitVector_Compare(iii,jjj); - if(comp <= 0) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - case BVSGT: - if(1 == CONSTANTBV::BitVector_Compare(iii,jjj)) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - case BVSGE: { - int comp = CONSTANTBV::BitVector_Compare(iii,jjj); - if(comp >= 0) - OutputNode = ASTTrue; - else - OutputNode = ASTFalse; - break; - } - default: - FatalError("BVConstEvaluator: The input kind is not supported yet:",t); - break; - } - - - - // //destroy all the CONSTANTBV bitvectors - // CONSTANTBV::BitVector_Destroy(iii); - // CONSTANTBV::BitVector_Destroy(jjj); - // CONSTANTBV::BitVector_Destroy(output); - - // if(k == BVNEG || k == BVUMINUS) - // CONSTANTBV::BitVector_Destroy(One); - // else if(k == BVAND || k == BVOR || k == BVXOR || k == BVSUB || - // k == BVMULT || k == EQ || k == NEQ || k == BVLT || - // k == BVLE || k == BVGT || k == BVGE || k == BVSLT || - // k == BVSLE || k == BVSGT || k == BVSGE) { - // CONSTANTBV::BitVector_Destroy(One); - // CONSTANTBV::BitVector_Destroy(Zero); - // } - - //AARON - if (output != NULL) CONSTANTBV::BitVector_Destroy(output); - if (One != NULL) CONSTANTBV::BitVector_Destroy(One); - if (Zero != NULL) CONSTANTBV::BitVector_Destroy(Zero); - if (iii != NULL && iii != One) CONSTANTBV::BitVector_Destroy(iii); - if (jjj != NULL && jjj != Zero) CONSTANTBV::BitVector_Destroy(jjj); - //AARON - - UpdateSolverMap(t,OutputNode); - //UpdateSimplifyMap(t,OutputNode,false); - return OutputNode; - } - - - unsigned int * ConvertToCONSTANTBV(const char * s) { - unsigned int length = strlen(s); - unsigned char * ccc = (unsigned char *)s; - unsigned * iii = CONSTANTBV::BitVector_Create(length,true); - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_from_Bin(iii,ccc); - //error printing - if(0 != e) { - cerr << "ConverToCONSTANTBV: wrong bin value: " << BitVector_Error(e); - FatalError(""); - } - - return iii; - } - */ -} -; //end of namespace BEEV +}; //end of namespace BEEV diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 5606f71..3d48dfd 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -1324,17 +1324,14 @@ unsigned long long int getBVUnsignedLongLong(Expr e) { nodestar a = (nodestar)e; if(BEEV::BVCONST != a->GetKind()) - BEEV::FatalError("getBVUnsigned: Attempting to extract int value from a NON-constant BITVECTOR: ",*a); -#ifdef NATIVE_C_ARITH - return (unsigned long long int)a->GetBVConst(); -#else + BEEV::FatalError("getBVUnsigned: Attempting to extract int value"\ + "from a NON-constant BITVECTOR: ",*a); unsigned* bv = a->GetBVConst(); char * str_bv = (char *)CONSTANTBV::BitVector_to_Bin(bv); unsigned long long int tmp = strtoull(str_bv,NULL,2); CONSTANTBV::BitVector_Dispose((unsigned char *)str_bv); return tmp; -#endif } diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 0264f64..44e5237 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -12,6 +12,23 @@ namespace BEEV { +bool BeevMgr::CheckMap(ASTNodeMap* VarConstMap, + const ASTNode& key, ASTNode& output) +{ + if(NULL == VarConstMap) + { + return false; + } + ASTNodeMap::iterator it; + if ((it = VarConstMap->find(key)) != VarConstMap->end()) + { + output = it->second; + return true; + } + return false; +} + + bool BeevMgr::CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg) { ASTNodeMap::iterator it, itend; @@ -205,10 +222,10 @@ void BeevMgr::FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1) } } -ASTNode BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg) +ASTNode BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { Begin_RemoveWrites = false; - ASTNode out = SimplifyFormula(b, pushNeg); + ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); return out; } @@ -248,7 +265,7 @@ ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg) return out; } -ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) +ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { if (!optimize_flag) return b; @@ -316,12 +333,12 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) return output; } -ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg) { +ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { //FIXME: Code this up properly later. Mainly pushing the negation down return a; } -ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { if (!optimize_flag) return a; @@ -595,7 +612,7 @@ ASTNode BeevMgr::PullUpITE(const ASTNode& in) } //takes care of some simple ITE Optimizations in the context of equations -ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in) +ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in, ASTNodeMap* VarConstMap) { CountersAndStats("ITEOpts_InEqs"); @@ -645,7 +662,7 @@ ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in) } else if (in1[2] == in2) { - cond = SimplifyFormula(cond, true); + cond = SimplifyFormula(cond, true, VarConstMap); output = cond; } else @@ -664,7 +681,7 @@ ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in) } else if (in2[2] == in1) { - cond = SimplifyFormula(cond, true); + cond = SimplifyFormula(cond, true, VarConstMap); output = cond; } else @@ -778,7 +795,7 @@ ASTNode BeevMgr::CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& i return result; } -ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; //cerr << "input:\n" << a << endl; @@ -807,7 +824,7 @@ ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) next_it = i + 1; bool nextexists = (next_it < iend); - aaa = SimplifyFormula(aaa, pushNeg); + aaa = SimplifyFormula(aaa, pushNeg, VarConstMap); if (annihilator == aaa) { //memoize @@ -819,7 +836,7 @@ ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) ASTNode bbb = ASTFalse; if (nextexists) { - bbb = SimplifyFormula(*next_it, pushNeg); + bbb = SimplifyFormula(*next_it, pushNeg, VarConstMap); } if (nextexists && bbb == aaa) { @@ -860,7 +877,7 @@ ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) } case 1: { - output = SimplifyFormula(outvec[0], false); + output = SimplifyFormula(outvec[0], false, VarConstMap); break; } default: @@ -883,7 +900,7 @@ ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) } //end of SimplifyAndOrFormula -ASTNode BeevMgr::SimplifyNotFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyNotFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg)) @@ -926,7 +943,7 @@ ASTNode BeevMgr::SimplifyNotFormula(const ASTNode& a, bool pushNeg) } else { - output = SimplifyFormula(o, pn); + output = SimplifyFormula(o, pn, VarConstMap); } //memoize UpdateSimplifyMap(o, output, pn); @@ -934,7 +951,7 @@ ASTNode BeevMgr::SimplifyNotFormula(const ASTNode& a, bool pushNeg) return output; } -ASTNode BeevMgr::SimplifyXorFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyXorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg)) @@ -945,8 +962,8 @@ ASTNode BeevMgr::SimplifyXorFormula(const ASTNode& a, bool pushNeg) FatalError("Simplify got an XOR with more than two children."); } - ASTNode a0 = SimplifyFormula(a[0], false); - ASTNode a1 = SimplifyFormula(a[1], false); + ASTNode a0 = SimplifyFormula(a[0], false, VarConstMap); + ASTNode a1 = SimplifyFormula(a[1], false, VarConstMap); output = pushNeg ? CreateNode(IFF, a0, a1) : CreateNode(XOR, a0, a1); if (XOR == output.GetKind()) @@ -964,7 +981,7 @@ ASTNode BeevMgr::SimplifyXorFormula(const ASTNode& a, bool pushNeg) return output; } -ASTNode BeevMgr::SimplifyNandFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyNandFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output, a0, a1; if (CheckSimplifyMap(a, output, pushNeg)) @@ -973,15 +990,15 @@ ASTNode BeevMgr::SimplifyNandFormula(const ASTNode& a, bool pushNeg) //the two NOTs cancel out if (pushNeg) { - a0 = SimplifyFormula(a[0], false); - a1 = SimplifyFormula(a[1], false); + a0 = SimplifyFormula(a[0], false, VarConstMap); + a1 = SimplifyFormula(a[1], false, VarConstMap); output = CreateNode(AND, a0, a1); } else { //push the NOT implicit in the NAND - a0 = SimplifyFormula(a[0], true); - a1 = SimplifyFormula(a[1], true); + a0 = SimplifyFormula(a[0], true, VarConstMap); + a1 = SimplifyFormula(a[1], true, VarConstMap); output = CreateNode(OR, a0, a1); } @@ -990,7 +1007,7 @@ ASTNode BeevMgr::SimplifyNandFormula(const ASTNode& a, bool pushNeg) return output; } -ASTNode BeevMgr::SimplifyNorFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyNorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output, a0, a1; if (CheckSimplifyMap(a, output, pushNeg)) @@ -1000,14 +1017,14 @@ ASTNode BeevMgr::SimplifyNorFormula(const ASTNode& a, bool pushNeg) if (pushNeg) { a0 = SimplifyFormula(a[0], false); - a1 = SimplifyFormula(a[1], false); + a1 = SimplifyFormula(a[1], false, VarConstMap); output = CreateNode(OR, a0, a1); } else { //push the NOT implicit in the NAND - a0 = SimplifyFormula(a[0], true); - a1 = SimplifyFormula(a[1], true); + a0 = SimplifyFormula(a[0], true, VarConstMap); + a1 = SimplifyFormula(a[1], true, VarConstMap); output = CreateNode(AND, a0, a1); } @@ -1016,7 +1033,7 @@ ASTNode BeevMgr::SimplifyNorFormula(const ASTNode& a, bool pushNeg) return output; } -ASTNode BeevMgr::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg)) @@ -1028,14 +1045,14 @@ ASTNode BeevMgr::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg) ASTNode c0, c1; if (pushNeg) { - c0 = SimplifyFormula(a[0], false); - c1 = SimplifyFormula(a[1], true); + c0 = SimplifyFormula(a[0], false, VarConstMap); + c1 = SimplifyFormula(a[1], true, VarConstMap); output = CreateNode(AND, c0, c1); } else { - c0 = SimplifyFormula(a[0], false); - c1 = SimplifyFormula(a[1], false); + c0 = SimplifyFormula(a[0], false, VarConstMap); + c1 = SimplifyFormula(a[1], false, VarConstMap); if (ASTFalse == c0) { output = ASTTrue; @@ -1086,7 +1103,7 @@ ASTNode BeevMgr::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg) return output; } -ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) +ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg)) @@ -1096,12 +1113,12 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) FatalError("SimplifyIffFormula: vector with wrong num of nodes", ASTUndefined); ASTNode c0 = a[0]; - ASTNode c1 = SimplifyFormula(a[1], false); + ASTNode c1 = SimplifyFormula(a[1], false, VarConstMap); if (pushNeg) - c0 = SimplifyFormula(c0, true); + c0 = SimplifyFormula(c0, true, VarConstMap); else - c0 = SimplifyFormula(c0, false); + c0 = SimplifyFormula(c0, false, VarConstMap); if (ASTTrue == c0) { @@ -1109,7 +1126,7 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) } else if (ASTFalse == c0) { - output = SimplifyFormula(c1, true); + output = SimplifyFormula(c1, true, VarConstMap); } else if (ASTTrue == c1) { @@ -1117,7 +1134,7 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) } else if (ASTFalse == c1) { - output = SimplifyFormula(c0, true); + output = SimplifyFormula(c0, true, VarConstMap); } else if (c0 == c1) { @@ -1153,7 +1170,7 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) return output; } -ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg) +ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { if (!optimize_flag) return b; @@ -1166,17 +1183,17 @@ ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg) FatalError("SimplifyIteFormula: vector with wrong num of nodes", ASTUndefined); ASTNode a = b; - ASTNode t0 = SimplifyFormula(a[0], false); + ASTNode t0 = SimplifyFormula(a[0], false, VarConstMap); ASTNode t1, t2; if (pushNeg) { - t1 = SimplifyFormula(a[1], true); - t2 = SimplifyFormula(a[2], true); + t1 = SimplifyFormula(a[1], true, VarConstMap); + t2 = SimplifyFormula(a[2], true, VarConstMap); } else { - t1 = SimplifyFormula(a[1], false); - t2 = SimplifyFormula(a[2], false); + t1 = SimplifyFormula(a[1], false, VarConstMap); + t2 = SimplifyFormula(a[2], false, VarConstMap); } if (ASTTrue == t0) @@ -1197,7 +1214,7 @@ ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg) } else if (ASTFalse == t1 && ASTTrue == t2) { - output = SimplifyFormula(t0, true); + output = SimplifyFormula(t0, true, VarConstMap); } else if (ASTTrue == t1) { @@ -1285,7 +1302,7 @@ ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b) } //This function simplifies terms based on their kind -ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) +ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap) { ASTNode inputterm(actualInputterm); // mutable local copy. @@ -1297,6 +1314,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) ASTNode output; assert(BVTypeCheck(inputterm)); + //######################################## //######################################## @@ -1331,9 +1349,13 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) output = inputterm; break; case SYMBOL: + if(CheckMap(VarConstMap, inputterm, output)) + { + return output; + } if (CheckSolverMap(inputterm, output)) { - return SimplifyTerm(output); + return SimplifyTerm(output); } output = inputterm; break; @@ -1341,7 +1363,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) { if (2 != inputterm.Degree()) { - FatalError("SimplifyTerm: We assume that BVMULT is binary", inputterm); + FatalError("SimplifyTerm: We assume that BVMULT is binary", inputterm); } // Described nicely by Warren, Hacker's Delight pg 135. @@ -1993,7 +2015,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) } else if (ITE == inputterm[0].GetKind()) { - ASTNode cond = SimplifyFormula(inputterm[0][0], false); + ASTNode cond = SimplifyFormula(inputterm[0][0], false, VarConstMap); ASTNode index = SimplifyTerm(inputterm[1]); ASTNode read1 = CreateTerm(READ, inputValueWidth, inputterm[0][1], index); @@ -2020,7 +2042,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) } case ITE: { - ASTNode t0 = SimplifyFormula(inputterm[0], false); + ASTNode t0 = SimplifyFormula(inputterm[0], false, VarConstMap); ASTNode t1 = SimplifyTerm(inputterm[1]); ASTNode t2 = SimplifyTerm(inputterm[2]); output = CreateSimplifiedTermITE(t0, t1, t2); @@ -2535,7 +2557,7 @@ ASTNode BeevMgr::RemoveWrites_TopLevel(const ASTNode& term) } } //end of RemoveWrites_TopLevel() -ASTNode BeevMgr::SimplifyWrites_InPlace(const ASTNode& term) +ASTNode BeevMgr::SimplifyWrites_InPlace(const ASTNode& term, ASTNodeMap* VarConstMap) { ASTNodeMultiSet WriteIndicesSeenSoFar; bool SeenNonConstWriteIndex = false; @@ -2564,7 +2586,7 @@ ASTNode BeevMgr::SimplifyWrites_InPlace(const ASTNode& term) //compare the readIndex and the current writeIndex and see if they //simplify to TRUE or FALSE or UNDETERMINABLE at this stage - ASTNode compare_readwrite_indices = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false); + ASTNode compare_readwrite_indices = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false, VarConstMap); //if readIndex and writeIndex are equal if (ASTTrue == compare_readwrite_indices && !SeenNonConstWriteIndex) @@ -2660,7 +2682,7 @@ ASTNode BeevMgr::RemoveWrites(const ASTNode& input) return output; } //end of RemoveWrites() -ASTNode BeevMgr::ReadOverWrite_To_ITE(const ASTNode& term) +ASTNode BeevMgr::ReadOverWrite_To_ITE(const ASTNode& term, ASTNodeMap* VarConstMap) { unsigned int width = term.GetValueWidth(); ASTNode input = term; @@ -2689,7 +2711,7 @@ ASTNode BeevMgr::ReadOverWrite_To_ITE(const ASTNode& term) ASTNode writeIndex = SimplifyTerm(write[1]); ASTNode writeVal = SimplifyTerm(write[2]); - ASTNode cond = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false); + ASTNode cond = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false, VarConstMap); ASTNode newRead = CreateTerm(READ, width, writeA, readIndex); ASTNode newRead_memoized = newRead; if (CheckSimplifyMap(newRead, newRead_memoized, false)) @@ -2769,16 +2791,6 @@ ASTNode BeevMgr::MultiplicativeInverse(const ASTNode& d) inverse = c; unsigned inputwidth = c.GetValueWidth(); -#ifdef NATIVE_C_ARITH - ASTNode one = CreateOneConst(inputwidth); - while(c != one) - { - //c = c*c - c = BVConstEvaluator(CreateTerm(BVMULT,inputwidth,c,c)); - //inverse = invsere*c - inverse = BVConstEvaluator(CreateTerm(BVMULT,inputwidth,inverse,c)); - } -#else //Compute the multiplicative inverse of c using the extended //euclidian algorithm // @@ -2834,7 +2846,6 @@ ASTNode BeevMgr::MultiplicativeInverse(const ASTNode& d) ASTNode low = CreateZeroConst(32); inverse = CreateTerm(BVEXTRACT, inputwidth, x2, hi, low); inverse = BVConstEvaluator(inverse); -#endif UpdateMultInverseMap(d, inverse); //cerr << "output of multinverse function is: " << inverse << endl;