WEBSITE
-------
+http://sites.google.com/site/stpfastprover
+
+
+SOURCEFORGE REPOSITORY
+----------------------
http://sourceforge.net/projects/stp-fast-prover
#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
return n;
}
-#ifndef NATIVE_C_ARITH
//Create a ASTBVConst node
ASTNode BeevMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst)
{
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<ASTBVConstSet::const_iterator, bool> 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
//#include "../sat/unsound/UnsoundSimpSolver.h"
#include "../sat/core/SolverTypes.h"
#include <stdlib.h>
-#ifndef NATIVE_C_ARITH
#include "../constantbv/constantbv.h"
-#endif
/*****************************************************************************
* LIST OF CLASSES DECLARED IN THIS FILE:
friend class ASTInterior;
friend class vector<ASTNode> ;
//Print the arguments in lisp format.
- friend ostream &LispPrintVec(ostream &os, const ASTVec &v, int indentation = 0);
- friend ostream &LispPrintVecSpecial(ostream &os, const vector<const ASTNode*> &v, int indentation = 0);
+ friend ostream &LispPrintVec(ostream &os,
+ const ASTVec &v,
+ int indentation = 0);
+ friend ostream &LispPrintVecSpecial(ostream &os,
+ const vector<const ASTNode*> &v,
+ int indentation = 0);
private:
// FIXME: make this into a reference?
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))
*
/***************************************************************************/
/* Class ASTBVConst: Class to represent internals of a bitvectorconst */
/***************************************************************************/
-
-#ifndef NATIVE_C_ARITH
-
class ASTBVConst: public ASTInternal
{
friend class BeevMgr;
}
}; //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<char*> 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<sym._value_width;jj++)
- if(!(sym._bvconst[jj] == '0' || sym._bvconst[jj] == '1')) {
- cerr << "Fatal Error: wrong input to ASTBVConst copy constructor:" << sym._bvconst << endl;
- FatalError("");
- }
- _value_width = sym._value_width;
- }
- public:
- // Destructor (does nothing, but is declared virtual here)
- virtual ~ASTBVConst(){}
-
- const char * const GetBVConst() const {return _bvconst;}
- }; //End of ASTBVConst
-
- unsigned int * ConvertToCONSTANTBV(const char * s);
-
- //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:");
- std::string s(n.GetBVConst(), n.GetValueWidth());
- unsigned int output = strtoul(s.c_str(),NULL,2);
- return output;
- } //end of ASTBVConst class
- #endif
- */
/***************************************************************************
* Typedef ASTNodeMap: This is a hash table from ASTNodes to ASTNodes.
* It is very convenient for attributes that are not speed-critical
**************************************************************************/
// These are generally useful for storing ASTNodes or attributes thereof
// Hash table from ASTNodes to ASTNodes
-typedef hash_map<ASTNode, ASTNode, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeMap;
+typedef hash_map<ASTNode,
+ ASTNode,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeMap;
-typedef hash_map<ASTNode, int32_t, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeCountMap;
+typedef hash_map<ASTNode,
+ int32_t,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeCountMap;
// Function to dump contents of ASTNodeMap
Typedef ASTNodeSet: This is a hash set of ASTNodes. Very useful
for representing things like "visited nodes"
***************************************************************************/
-typedef hash_set<ASTNode, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeSet;
+typedef hash_set<ASTNode,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeSet;
-typedef hash_multiset<ASTNode, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeMultiSet;
+typedef hash_multiset<ASTNode,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeMultiSet;
//external parser table for declared symbols.
//FIXME: move to a more appropriate place
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);
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);
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
//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);
//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);
//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);
}
};
-}
-; // 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
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;
}
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);
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<unsigned, bool> * 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)
{
FatalError(ss.c_str(), t);
}
-#ifndef NATIVE_C_ARITH
ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
{
ASTNode OutputNode;
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
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
}
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;
}
}
-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;
}
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;
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;
}
//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");
}
else if (in1[2] == in2)
{
- cond = SimplifyFormula(cond, true);
+ cond = SimplifyFormula(cond, true, VarConstMap);
output = cond;
}
else
}
else if (in2[2] == in1)
{
- cond = SimplifyFormula(cond, true);
+ cond = SimplifyFormula(cond, true, VarConstMap);
output = cond;
}
else
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;
next_it = i + 1;
bool nextexists = (next_it < iend);
- aaa = SimplifyFormula(aaa, pushNeg);
+ aaa = SimplifyFormula(aaa, pushNeg, VarConstMap);
if (annihilator == aaa)
{
//memoize
ASTNode bbb = ASTFalse;
if (nextexists)
{
- bbb = SimplifyFormula(*next_it, pushNeg);
+ bbb = SimplifyFormula(*next_it, pushNeg, VarConstMap);
}
if (nextexists && bbb == aaa)
{
}
case 1:
{
- output = SimplifyFormula(outvec[0], false);
+ output = SimplifyFormula(outvec[0], false, VarConstMap);
break;
}
default:
} //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))
}
else
{
- output = SimplifyFormula(o, pn);
+ output = SimplifyFormula(o, pn, VarConstMap);
}
//memoize
UpdateSimplifyMap(o, output, pn);
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))
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())
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))
//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);
}
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))
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);
}
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))
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;
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))
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)
{
}
else if (ASTFalse == c0)
{
- output = SimplifyFormula(c1, true);
+ output = SimplifyFormula(c1, true, VarConstMap);
}
else if (ASTTrue == c1)
{
}
else if (ASTFalse == c1)
{
- output = SimplifyFormula(c0, true);
+ output = SimplifyFormula(c0, true, VarConstMap);
}
else if (c0 == c1)
{
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;
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)
}
else if (ASTFalse == t1 && ASTTrue == t2)
{
- output = SimplifyFormula(t0, true);
+ output = SimplifyFormula(t0, true, VarConstMap);
}
else if (ASTTrue == t1)
{
}
//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.
ASTNode output;
assert(BVTypeCheck(inputterm));
+
//########################################
//########################################
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;
{
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.
}
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);
}
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);
}
} //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;
//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)
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;
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))
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
//
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;
projects / francis / stp.git / commitdiff