diff options
Diffstat (limited to 'stp/AST/AST.h')
| -rw-r--r-- | stp/AST/AST.h | 1805 |
1 files changed, 1805 insertions, 0 deletions
diff --git a/stp/AST/AST.h b/stp/AST/AST.h new file mode 100644 index 00000000..53ed7016 --- /dev/null +++ b/stp/AST/AST.h @@ -0,0 +1,1805 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef AST_H +#define AST_H +#include <vector> +#ifdef EXT_HASH_MAP +#include <ext/hash_set> +#include <ext/hash_map> +#else +#include <hash_set> +#include <hash_map> +#endif +#include <iostream> +#include <sstream> +#include <string> +#include <map> +#include <set> +#include "ASTUtil.h" +#include "ASTKind.h" +#include "../sat/Solver.h" +#include "../sat/SolverTypes.h" +#include <cstdlib> +#ifndef NATIVE_C_ARITH +#include "../constantbv/constantbv.h" +#endif +/***************************************************************************** + * LIST OF CLASSES DECLARED IN THIS FILE: + * + * class BeevMgr; + * class ASTNode; + * class ASTInternal; + * class ASTInterior; + * class ASTSymbol; + * class ASTBVConst; + *****************************************************************************/ +namespace BEEV { + using namespace std; + using namespace MINISAT; +#ifdef EXT_HASH_MAP + using namespace __gnu_cxx; +#endif + + //return types for the GetType() function in ASTNode class + enum types { + BOOLEAN_TYPE = 0, + BITVECTOR_TYPE, + ARRAY_TYPE, + UNKNOWN_TYPE + }; + + class BeevMgr; + class ASTNode; + class ASTInternal; + class ASTInterior; + class ASTSymbol; + class ASTBVConst; + class BVSolver; + + //Vector of ASTNodes, used for child nodes among other things. + typedef vector<ASTNode> ASTVec; + extern ASTVec _empty_ASTVec; + extern BeevMgr * globalBeevMgr_for_parser; + + typedef unsigned int * CBV; + + /***************************************************************************/ + /* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */ + /***************************************************************************/ + class ASTNode { + friend class BeevMgr; + friend class vector<ASTNode>; + //Print the arguments in lisp format. + friend ostream &LispPrintVec(ostream &os, + const ASTVec &v, int indentation = 0); + + private: + // FIXME: make this into a reference? + ASTInternal * _int_node_ptr; // The real data. + + // Usual constructor. + ASTNode(ASTInternal *in); + + //Check if it points to a null node + bool IsNull () const { return _int_node_ptr == NULL; } + + //Equal iff ASTIntNode pointers are the same. + friend bool operator==(const ASTNode node1, const ASTNode node2){ + return ((size_t) node1._int_node_ptr) == ((size_t) node2._int_node_ptr); + } + + /* FIXME: Nondeterministic code *** */ + /** questionable pointer comparison function */ + friend bool operator<(const ASTNode node1, const ASTNode node2){ + return ((size_t) node1._int_node_ptr) < ((size_t) node2._int_node_ptr); + } + + public: + // This is for sorting by expression number (used in Boolean + //optimization) + friend bool exprless(const ASTNode n1, const ASTNode n2) { + Kind k1 = n1.GetKind(); + Kind k2 = n2.GetKind(); + + if(BVCONST == k1 && BVCONST != k2){ + return true; + } + if(BVCONST != k1 && BVCONST == k2){ + return false; + } + + if(SYMBOL == k1 && SYMBOL != k2) { + return true; + } + + if(SYMBOL != k1 && SYMBOL == k2) { + return false; + } + + return (n1.GetNodeNum() < n2.GetNodeNum()); + }//end of exprless + + // Internal lisp-form printer that does not clear _node_print_table + ostream &LispPrint1(ostream &os, int indentation) const; + + ostream &LispPrint_indent(ostream &os, int indentation) const; + + // For lisp DAG printing. Has it been printed already, so we can + // just print the node number? + bool IsAlreadyPrinted() const; + void MarkAlreadyPrinted() const; + + public: + // Default constructor. This gets used when declaring an ASTVec + // of a given size, in the hash table, etc. For faster + // refcounting, create a symbol node for NULL. Give it a big + // initial refcount. Never free it. also check, for ref-count + // overflow? + ASTNode() : _int_node_ptr(NULL) { }; + + // Copy constructor + ASTNode(const ASTNode &n); + + // Destructor + ~ASTNode(); + + // Assignment (for ref counting) + ASTNode& operator=(const ASTNode& n); + + BeevMgr &GetBeevMgr() const; + + // Access node number + int GetNodeNum() const; + + // Access kind. Inlined later because of declaration ordering problems. + Kind GetKind() const; + + // access Children + const ASTVec &GetChildren() const; + + // Return the number of child nodes + size_t Degree() const{ + return GetChildren().size(); + }; + + // Get indexth childNode. + const ASTNode operator[](size_t index) const { + return GetChildren()[index]; + }; + + // Get begin() iterator for child nodes + ASTVec::const_iterator begin() const{ + return GetChildren().begin(); + }; + + // Get end() iterator for child nodes + ASTVec::const_iterator end() const{ + return GetChildren().end(); + }; + + //Get back() element for child nodes + const ASTNode back() const{ + return GetChildren().back(); + }; + + // Get the name from a symbol (char *). It's an error if kind != SYMBOL + 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)) + * + *ASTNode is of type ARRAY <==> ((indexwidth>0)&&(valuewidth>0)) + * + *ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0)) + * + *both indexwidth and valuewidth should never be less than 0 + */ + unsigned int GetIndexWidth () const; + + // FIXME: This function is dangerous. Try to eliminate it's use. + void SetIndexWidth (unsigned int iw) const; + + unsigned int GetValueWidth () const; + + // FIXME: This function is dangerous. Try to eliminate it's use. + void SetValueWidth (unsigned int vw) const; + + //return the type of the ASTNode + //0 iff BOOLEAN + //1 iff BITVECTOR + //2 iff ARRAY + + /*ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0)) + * + *ASTNode is of type ARRAY <==> ((indexwidth>0)&&(valuewidth>0)) + * + *ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0)) + * + *both indexwidth and valuewidth should never be less than 0 + */ + types GetType(void) const; + + // Hash is pointer value of _int_node_ptr. + const size_t Hash() const{ + return (size_t) _int_node_ptr; + //return GetNodeNum(); + } + + // lisp-form printer + ostream& LispPrint(ostream &os, int indentation = 0) const; + + //Presentation Language Printer + ostream& PL_Print(ostream &os, int indentation = 0) const; + + void PL_Print1(ostream &os, int indentation = 0, bool b = false) const; + + //Construct let variables for shared subterms + void LetizeNode(void) const; + + // Attempt to define something that will work in the gdb + friend void lp(ASTNode &node); + friend void lpvec(const ASTVec &vec); + + friend ostream &operator<<(ostream &os, const ASTNode &node) { + node.LispPrint(os, 0); + return os; + }; + + // Check whether the ASTNode points to anything. Undefined nodes + // are created by the default constructor. In binding table (for + // lambda args, etc.), undefined nodes are used to represent + // deleted entries. + bool IsDefined() const { return _int_node_ptr != NULL; } + + /* Hasher class for STL hash_maps and hash_sets that use ASTNodes + * as keys. Needs to be public so people can define hash tables + * (and use ASTNodeMap class)*/ + class ASTNodeHasher { + public: + size_t operator() (const ASTNode& n) const{ + return (size_t) n._int_node_ptr; + //return (size_t)n.GetNodeNum(); + }; + }; //End of ASTNodeHasher + + /* Equality for ASTNode hash_set and hash_map. Returns true iff + * internal pointers are the same. Needs to be public so people + * can define hash tables (and use ASTNodeSet class)*/ + class ASTNodeEqual { + public: + bool operator()(const ASTNode& n1, const ASTNode& n2) const{ + return (n1._int_node_ptr == n2._int_node_ptr); + } + }; //End of ASTNodeEqual + }; //End of Class ASTNode + + void FatalError(const char * str, const ASTNode& a, int w = 0); + void FatalError(const char * str); + void SortByExprNum(ASTVec& c); + bool exprless(const ASTNode n1, const ASTNode n2); + bool isAtomic(Kind k); + + /***************************************************************************/ + /* Class ASTInternal:Abstract base class for internal node representation.*/ + /* Requires Kind and ChildNodes so same traversal works */ + /* on all nodes. */ + /***************************************************************************/ + class ASTInternal { + + friend class ASTNode; + + protected: + + // reference count. + int _ref_count; + + // Kind. It's a type tag and the operator. + Kind _kind; + + // The vector of children (*** should this be in ASTInterior? ***) + ASTVec _children; + + // Manager object. Having this backpointer means it's easy to + // find the manager when we need it. + BeevMgr &_bm; + + //Nodenum is a unique positive integer for the node. The nodenum + //of a node should always be greater than its descendents (which + //is easily achieved by incrementing the number each time a new + //node is created). + int _node_num; + + // Length of bitvector type for array index. The term is an + // array iff this is positive. Otherwise, the term is a bitvector + // or a bit. + unsigned int _index_width; + + // Length of bitvector type for scalar value or array element. + // If this is one, the term represents a single bit (same as a bitvector + // of length 1). It must be 1 or greater. + unsigned int _value_width; + + // Increment refcount. +#ifndef SMTLIB + void IncRef() { ++_ref_count; } +#else + void IncRef() { } +#endif + + // DecRef is a potentially expensive, because it has to delete + // the node from the unique table, in addition to freeing it. + // FIXME: Consider putting in a backpointer (iterator) to the hash + // table entry so it can be deleted without looking it up again. + void DecRef(); + + virtual const Kind GetKind() const { return _kind; } + + virtual ASTVec const &GetChildren() const { return _children; } + + int GetNodeNum() const { return _node_num; } + + void SetNodeNum(int nn) { _node_num = nn; }; + + // Constructor (bm only) + ASTInternal(BeevMgr &bm, int nodenum = 0) : + _ref_count(0), + _kind(UNDEFINED), + _bm(bm), + _node_num(nodenum), + _index_width(0), + _value_width(0) { } + + // Constructor (kind only, empty children, int nodenum) + ASTInternal(Kind kind, BeevMgr &bm, int nodenum = 0) : + _ref_count(0), + _kind(kind), + _bm(bm), + _node_num(nodenum), + _index_width(0), + _value_width(0) { } + + // Constructor (kind and children). This copies the contents of + // the child nodes. + // FIXME: is there a way to avoid repeating these? + ASTInternal(Kind kind, const ASTVec &children, BeevMgr &bm, int nodenum = 0) : + _ref_count(0), + _kind(kind), + _children(children), + _bm(bm), + _node_num(nodenum), + _index_width(0), + _value_width(0) { } + + // Copy constructor. This copies the contents of the child nodes + // array, along with everything else. Assigning the smart pointer, + // ASTNode, does NOT invoke this; This should only be used for + // temporary hash keys before uniquefication. + // FIXME: I don't think children need to be copied. + ASTInternal(const ASTInternal &int_node, int nodenum = 0) : + _ref_count(0), + _kind(int_node._kind), + _children(int_node._children), + _bm(int_node._bm), + _node_num(int_node._node_num), + _index_width(int_node._index_width), + _value_width(int_node._value_width) { } + + // Copying assign operator. Also copies contents of children. + ASTInternal& operator=(const ASTInternal &int_node); + + // Cleanup function for removing from hash table + virtual void CleanUp() = 0; + + // Destructor (does nothing, but is declared virtual here. + virtual ~ASTInternal(); + + // Abstract virtual print function for internal node. + virtual void nodeprint(ostream& os) { os << "*"; }; + }; //End of Class ASTInternal + + // FIXME: Should children be only in interior node type? + /*************************************************************************** + Class ASTInterior: Internal representation of an interior + ASTNode. Generally, these nodes should have at least one + child + ***************************************************************************/ + class ASTInterior : public ASTInternal { + + friend class BeevMgr; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + + // Hasher for ASTInterior pointer nodes + class ASTInteriorHasher { + public: + size_t operator()(const ASTInterior *int_node_ptr) const; + }; + + // Equality for ASTInterior nodes + class ASTInteriorEqual { + public: + bool operator()(const ASTInterior *int_node_ptr1, + const ASTInterior *int_node_ptr2) const{ + return (*int_node_ptr1 == *int_node_ptr2); + } + }; + + // Used in Equality class for hash tables + friend bool operator==(const ASTInterior &int_node1, + const ASTInterior &int_node2){ + return (int_node1._kind == int_node2._kind) && + (int_node1._children == int_node2._children); + } + + // Call this when deleting a node that has been stored in the + // the unique table + virtual void CleanUp(); + + // Returns kinds. "lispprinter" handles printing of parenthesis + // and childnodes. + virtual void nodeprint(ostream& os) { + os << _kind_names[_kind]; + } + public: + + // FIXME: This should not be public, but has to be because the + // ASTInterior hash table insists on it. I can't seem to make the + // private destructor visible to hash_set. It does not even work + // to put "friend class hash_set<ASTInterior, ...>" in here. + + // Basic constructors + ASTInterior(Kind kind, BeevMgr &bm) : + ASTInternal(kind, bm) { } + + ASTInterior(Kind kind, ASTVec &children, BeevMgr &bm) : + ASTInternal(kind, children, bm) { } + + //Copy constructor. This copies the contents of the child nodes + //array, along with everything else. Assigning the smart pointer, + //ASTNode, does NOT invoke this. + ASTInterior(const ASTInterior &int_node) : ASTInternal(int_node) { } + + // Destructor (does nothing, but is declared virtual here. + virtual ~ASTInterior(); + + }; //End of ASTNodeInterior + + + /***************************************************************************/ + /* Class ASTSymbol: Class to represent internals of Symbol node. */ + /***************************************************************************/ + class ASTSymbol : public ASTInternal{ + friend class BeevMgr; + friend class ASTNode; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + // The name of the symbol + const char * const _name; + + class ASTSymbolHasher{ + public: + size_t operator() (const ASTSymbol *sym_ptr) const{ + hash<char*> h; + return h(sym_ptr->_name); + }; + }; + + // Equality for ASTInternal nodes + class ASTSymbolEqual{ + public: + bool operator()(const ASTSymbol *sym_ptr1, const ASTSymbol *sym_ptr2) const{ + return (*sym_ptr1 == *sym_ptr2); + } + }; + + friend bool operator==(const ASTSymbol &sym1, const ASTSymbol &sym2){ + return (strcmp(sym1._name, sym2._name) == 0); + } + + const char * const GetName() const{return _name;} + + // Print function for symbol -- return name */ + virtual void nodeprint(ostream& os) { os << _name;} + + // Call this when deleting a node that has been stored in the + // the unique table + virtual void CleanUp(); + + public: + + // Default constructor + ASTSymbol(BeevMgr &bm) : ASTInternal(bm), _name(NULL) { } + + // Constructor. This does NOT copy its argument. + ASTSymbol(const char * const name, BeevMgr &bm) : ASTInternal(SYMBOL, bm), + _name(name) { } + + // Destructor (does nothing, but is declared virtual here. + virtual ~ASTSymbol(); + + // Copy constructor + // FIXME: seems to be calling default constructor for astinternal + ASTSymbol(const ASTSymbol &sym) : + ASTInternal(sym._kind, sym._children, sym._bm), + _name(sym._name) { } + }; //End of ASTSymbol + + + /***************************************************************************/ + /* Class ASTBVConst: Class to represent internals of a bitvectorconst */ + /***************************************************************************/ + +#ifndef NATIVE_C_ARITH + + class ASTBVConst : public ASTInternal { + friend class BeevMgr; + friend class ASTNode; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + //This is the private copy of a bvconst currently + //This should not be changed at any point + CBV _bvconst; + + class ASTBVConstHasher{ + public: + size_t operator() (const ASTBVConst * bvc) const { + return CONSTANTBV::BitVector_Hash(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==CONSTANTBV::BitVector_Compare(bvc1->_bvconst,bvc2->_bvconst)); + } + }; + + //FIXME Keep an eye on this function + ASTBVConst(CBV bv, unsigned int width, BeevMgr &bm) : + ASTInternal(BVCONST, bm) + { + _bvconst = CONSTANTBV::BitVector_Clone(bv); + _value_width = width; + } + + friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){ + if(bvc1._value_width != bvc2._value_width) + return false; + return (0==CONSTANTBV::BitVector_Compare(bvc1._bvconst,bvc2._bvconst)); + } + // 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 bin format + virtual void nodeprint(ostream& os) { + unsigned char *res; + const char *prefix; + + if (_value_width%4 == 0) { + res = CONSTANTBV::BitVector_to_Hex(_bvconst); + prefix = "0hex"; + } else { + res = CONSTANTBV::BitVector_to_Bin(_bvconst); + prefix = "0bin"; + } + if (NULL == res) { + os << "nodeprint: BVCONST : could not convert to string" << _bvconst; + FatalError(""); + } + os << prefix << res; + CONSTANTBV::BitVector_Dispose(res); + } + + // Copy constructor. + ASTBVConst(const ASTBVConst &sym) : + ASTInternal(sym._kind, sym._children, sym._bm) + { + _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst); + _value_width = sym._value_width; + } + + public: + virtual ~ASTBVConst(){ + CONSTANTBV::BitVector_Destroy(_bvconst); + } + + CBV GetBVConst() const {return _bvconst;} + }; //End of ASTBVConst + + //FIXME This function is DEPRICATED + //Do not use in the future + 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) *((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) { + 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; + + // Function to dump contents of ASTNodeMap + 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<ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeSet; + + typedef hash_multiset<ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeMultiSet; + + //external parser table for declared symbols. + //FIXME: move to a more appropriate place + extern ASTNodeSet _parser_symbol_table; + + /*************************************************************************** + Class LispPrinter: iomanipulator for printing ASTNode or ASTVec + ***************************************************************************/ + class LispPrinter { + + public: + ASTNode _node; + + // number of spaces to print before first real character of + // object. + int _indentation; + + // FIXME: pass ASTNode by reference + // Constructor to build the LispPrinter object + LispPrinter(ASTNode node, int indentation): _node(node), _indentation(indentation) { } + + friend ostream &operator<<(ostream &os, const LispPrinter &lp){ + return lp._node.LispPrint(os, lp._indentation); + }; + + }; //End of ListPrinter + + //This is the IO manipulator. It builds an object of class + //"LispPrinter" that has a special overloaded "<<" operator. + inline LispPrinter lisp(const ASTNode &node, int indentation = 0){ + LispPrinter lp(node, indentation); + return lp; + } + + /***************************************************************************/ + /* Class LispVecPrinter:iomanipulator for printing vector of ASTNodes */ + /***************************************************************************/ + class LispVecPrinter { + + public: + const ASTVec * _vec; + // number of spaces to print before first real + // character of object. + int _indentation; + + // Constructor to build the LispPrinter object + LispVecPrinter(const ASTVec &vec, int indentation){ + _vec = &vec; _indentation = indentation; + } + + friend ostream &operator<<(ostream &os, const LispVecPrinter &lvp){ + LispPrintVec(os, *lvp._vec, lvp._indentation); + return os; + }; + }; //End of Class ListVecPrinter + + //iomanipulator. builds an object of class "LisPrinter" that has a + //special overloaded "<<" operator. + inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0){ + LispVecPrinter lvp(vec, indentation); + return lvp; + } + + + /***************************************************************** + * INLINE METHODS from various classed, declared here because of + * dependencies on classes that are declared later. + *****************************************************************/ + // ASTNode accessor function. + inline Kind ASTNode::GetKind() const { + //cout << "GetKind: " << _int_node_ptr; + return _int_node_ptr->GetKind(); + } + + // FIXME: should be const ASTVec const? + // Declared here because of same ordering problem as GetKind. + inline const ASTVec &ASTNode::GetChildren() const { + return _int_node_ptr->GetChildren(); + } + + // Access node number + inline int ASTNode::GetNodeNum() const { + return _int_node_ptr->_node_num; + } + + inline unsigned int ASTNode::GetIndexWidth () const { + return _int_node_ptr->_index_width; + } + + inline void ASTNode::SetIndexWidth (unsigned int iw) const { + _int_node_ptr->_index_width = iw; + } + + inline unsigned int ASTNode::GetValueWidth () const { + return _int_node_ptr->_value_width; + } + + inline void ASTNode::SetValueWidth (unsigned int vw) const { + _int_node_ptr->_value_width = vw; + } + + //return the type of the ASTNode: 0 iff BOOLEAN; 1 iff BITVECTOR; 2 + //iff ARRAY; 3 iff UNKNOWN; + inline types ASTNode::GetType() const { + if((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN + return BOOLEAN_TYPE; + if((GetIndexWidth() == 0) && (GetValueWidth() > 0)) //BITVECTOR + return BITVECTOR_TYPE; + if((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY + return ARRAY_TYPE; + return UNKNOWN_TYPE; + } + + // Constructor; creates a new pointer, increments refcount of + // pointed-to object. +#ifndef SMTLIB + inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { + if (in) in->IncRef(); + } +#else + inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { }; +#endif + + // Assignment. Increment refcount of new value, decrement refcount + // of old value and destroy if this was the last pointer. FIXME: + // accelerate this by creating an intnode with a ref counter instead + // of pointing to NULL. Need a special check in CleanUp to make + // sure the null node never gets freed. + +#ifndef SMTLIB + inline ASTNode& ASTNode::operator=(const ASTNode& n) { + if (n._int_node_ptr) { + n._int_node_ptr->IncRef(); + } + if (_int_node_ptr) { + _int_node_ptr->DecRef(); + } + _int_node_ptr = n._int_node_ptr; + return *this; + } +#else + inline ASTNode& ASTNode::operator=(const ASTNode& n) { + _int_node_ptr = n._int_node_ptr; + return *this; + } +#endif + +#ifndef SMTLIB + inline void ASTInternal::DecRef() + { + if (--_ref_count == 0) { + // Delete node from unique table and kill it. + CleanUp(); + } + } + + // Destructor + inline ASTNode::~ASTNode() + { + if (_int_node_ptr) { + _int_node_ptr->DecRef(); + } + }; +#else + // No refcounting + inline void ASTInternal::DecRef() + { + } + + // Destructor + inline ASTNode::~ASTNode() + { + }; +#endif + + inline BeevMgr& ASTNode::GetBeevMgr() const { return _int_node_ptr->_bm; } + + /*************************************************************************** + * Class BeevMgr. This holds all "global" variables for the system, such as + * unique tables for the various kinds of nodes. + ***************************************************************************/ + class BeevMgr { + friend class ASTNode; // ASTNode modifies AlreadyPrintedSet + // in BeevMgr + friend class ASTInterior; + friend class ASTBVConst; + friend class ASTSymbol; + + // FIXME: The values appear to be the same regardless of the value of SMTLIB + // initial hash table sizes, to save time on resizing. +#ifdef SMTLIB + static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100; + static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100; + + static const int INITIAL_SIMPLIFY_MAP_SIZE = 100; + static const int INITIAL_SOLVER_MAP_SIZE = 100; + static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; + static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; +#else + // these are the STL defaults + static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100; + static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100; + + static const int INITIAL_SIMPLIFY_MAP_SIZE = 100; + static const int INITIAL_SOLVER_MAP_SIZE = 100; + static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; + static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; +#endif + + private: + // Typedef for unique Interior node table. + typedef hash_set<ASTInterior *, + ASTInterior::ASTInteriorHasher, + ASTInterior::ASTInteriorEqual> ASTInteriorSet; + + // Typedef for unique Symbol node (leaf) table. + typedef hash_set<ASTSymbol *, + ASTSymbol::ASTSymbolHasher, + ASTSymbol::ASTSymbolEqual> ASTSymbolSet; + + // Unique tables to share nodes whenever possible. + ASTInteriorSet _interior_unique_table; + //The _symbol_unique_table is also the symbol table to be used + //during parsing/semantic analysis + ASTSymbolSet _symbol_unique_table; + + //Typedef for unique BVConst node (leaf) table. + typedef hash_set<ASTBVConst *, + ASTBVConst::ASTBVConstHasher, + ASTBVConst::ASTBVConstEqual> ASTBVConstSet; + + //table to uniquefy bvconst + ASTBVConstSet _bvconst_unique_table; + + // type of memo table. + typedef hash_map<ASTNode, ASTVec, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToVecMap; + + typedef hash_map<ASTNode,ASTNodeSet, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToSetMap; + + // Memo table for bit blasted terms. If a node has already been + // bitblasted, it is mapped to a vector of Boolean formulas for + // the bits. + + //OLD: ASTNodeToVecMap BBTermMemo; + ASTNodeMap BBTermMemo; + + // Memo table for bit blasted formulas. If a node has already + // been bitblasted, it is mapped to a node representing the + // bitblasted equivalent + ASTNodeMap BBFormMemo; + + //public: + // Get vector of Boolean formulas for sum of two + // vectors of Boolean formulas + void BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin); + // Increment + ASTVec BBInc(ASTVec& x); + // Add one bit to a vector of bits. + ASTVec BBAddOneBit(ASTVec& x, ASTNode cin); + // Bitwise complement + ASTVec BBNeg(const ASTVec& x); + // Unary minus + ASTVec BBUminus(const ASTVec& x); + // Multiply. + ASTVec BBMult(const ASTVec& x, const ASTVec& y); + // AND each bit of vector y with single bit b and return the result. + // (used in BBMult) + ASTVec BBAndBit(const ASTVec& y, ASTNode b); + // Returns ASTVec for result - y. This destroys "result". + void BBSub(ASTVec& result, const ASTVec& y); + // build ITE's (ITE cond then[i] else[i]) for each i. + ASTVec BBITE(const ASTNode& cond, + const ASTVec& thn, const ASTVec& els); + // Build a vector of zeros. + ASTVec BBfill(unsigned int width, ASTNode fillval); + // build an EQ formula + ASTNode BBEQ(const ASTVec& left, const ASTVec& right); + + // This implements a variant of binary long division. + // q and r are "out" parameters. rwidth puts a bound on the + // recursion depth. Unsigned only, for now. + void BBDivMod(const ASTVec &y, + const ASTVec &x, + ASTVec &q, + ASTVec &r, + unsigned int rwidth); + + // Return formula for majority function of three formulas. + ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c); + + // Internal bit blasting routines. + ASTNode BBBVLE(const ASTVec& x, const ASTVec& y, bool is_signed); + + // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. + ASTNode BBcompare(const ASTNode& form); + + // Left and right shift one. Writes into x. + void BBLShift(ASTVec& x); + void BBRShift(ASTVec& x); + + public: + // Simplifying create functions + ASTNode CreateSimpForm(Kind kind, ASTVec &children); + ASTNode CreateSimpForm(Kind kind, const ASTNode& child0); + ASTNode CreateSimpForm(Kind kind, + const ASTNode& child0, + const ASTNode& child1); + ASTNode CreateSimpForm(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2); + + ASTNode CreateSimpNot(const ASTNode& form); + + // These are for internal use only. + // FIXME: Find a way to make this local to SimpBool, so they're + // not in AST.h + ASTNode CreateSimpXor(const ASTNode& form1, + const ASTNode& form2); + ASTNode CreateSimpXor(ASTVec &children); + ASTNode CreateSimpAndOr(bool isAnd, + const ASTNode& form1, + const ASTNode& form2); + ASTNode CreateSimpAndOr(bool IsAnd, ASTVec &children); + ASTNode CreateSimpFormITE(const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2); + + + // Declarations of BitBlaster functions (BitBlast.cpp) + public: + // Adds or removes a NOT as necessary to negate a literal. + ASTNode Negate(const ASTNode& form); + + // Bit blast a bitvector term. The term must have a kind for a + // bitvector term. Result is a ref to a vector of formula nodes + // representing the boolean formula. + const ASTNode BBTerm(const ASTNode& term); + + const ASTNode BBForm(const ASTNode& formula); + + // Declarations of CNF conversion (ToCNF.cpp) + public: + // ToCNF converts a bit-blasted Boolean formula to Conjunctive + // Normal Form, suitable for many SAT solvers. Our CNF representation + // is an STL vector of STL vectors, for independence from any particular + // SAT solver's representation. There needs to be a separate driver to + // convert our clauselist to the representation used by the SAT solver. + // Currently, there is only one such solver and its driver is "ToSAT" + + // Datatype for clauses + typedef ASTVec * ClausePtr; + + // Datatype for Clauselists + typedef vector<ClausePtr> ClauseList; + + // Convert a Boolean formula to an equisatisfiable CNF formula. + ClauseList *ToCNF(const ASTNode& form); + + // Print function for debugging + void PrintClauseList(ostream& os, ClauseList& cll); + + // Free the clause list and all its clauses. + void DeleteClauseList(BeevMgr::ClauseList *cllp); + + // Map from formulas to representative literals, for debugging. + ASTNodeMap RepLitMap; + + private: + // Global for assigning new node numbers. + int _max_node_num; + + const ASTNode ASTFalse, ASTTrue, ASTUndefined; + + // I just did this so I could put it in as a fake return value in + // methods that return a ASTNode &, to make -Wall shut up. + ASTNode dummy_node; + + //BeevMgr Constructor, Destructor and other misc. functions + public: + + int NewNodeNum() { _max_node_num += 2; return _max_node_num; } + + // Table for DAG printing. + ASTNodeSet AlreadyPrintedSet; + + //Tables for Presentation language printing + + //Nodes seen so far + ASTNodeSet PLPrintNodeSet; + + //Map from ASTNodes to LetVars + ASTNodeMap NodeLetVarMap; + + //This is a vector which stores the Node to LetVars pairs. It + //allows for sorted printing, as opposed to NodeLetVarMap + std::vector<pair<ASTNode,ASTNode> > NodeLetVarVec; + + //a partial Map from ASTNodes to LetVars. Needed in order to + //correctly print shared subterms inside the LET itself + ASTNodeMap NodeLetVarMap1; + + //functions to lookup nodes from the memo tables. these should be + //private. + private: + //Destructively appends back_child nodes to front_child nodes. + //If back_child nodes is NULL, no appending is done. back_child + //nodes are not modified. Then it returns the hashed copy of the + //node, which is created if necessary. + ASTInterior *CreateInteriorNode(Kind kind, + ASTInterior *new_node, + // this is destructively modified. + const ASTVec & back_children = _empty_ASTVec); + + // Create unique ASTInterior node. + ASTInterior *LookupOrCreateInterior(ASTInterior *n); + + // Create unique ASTSymbol node. + ASTSymbol *LookupOrCreateSymbol(ASTSymbol& s); + + // Called whenever we want to make sure that the Symbol is + // declared during semantic analysis + bool LookupSymbol(ASTSymbol& s); + + // Called by ASTNode constructors to uniqueify ASTBVConst + ASTBVConst *LookupOrCreateBVConst(ASTBVConst& s); + + //Public functions for CreateNodes and Createterms + public: + // Create and return an ASTNode for a symbol + ASTNode CreateSymbol(const char * const name); + + // Create and return an ASTNode for a symbol + // Width is number of bits. + ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst); + ASTNode CreateZeroConst(unsigned int width); + ASTNode CreateOneConst(unsigned int width); + ASTNode CreateTwoConst(unsigned int width); + ASTNode CreateMaxConst(unsigned int width); + + // Create and return an ASTNode for a symbol + // Optional base was a problem because 0 could be an int or char *, + // so CreateBVConst was ambiguous. + ASTNode CreateBVConst(const char *strval, int base); + + //FIXME This is a dangerous function + ASTNode CreateBVConst(CBV bv, unsigned width); + + // Create and return an interior ASTNode + ASTNode CreateNode(Kind kind, const ASTVec &children = _empty_ASTVec); + + ASTNode CreateNode(Kind kind, + const ASTNode& child0, + const ASTVec &children = _empty_ASTVec); + + ASTNode CreateNode(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec &children = _empty_ASTVec); + + ASTNode CreateNode(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec &children = _empty_ASTVec); + + // Create and return an ASTNode for a term + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, children); + n.SetValueWidth(width); + + //by default we assume that the term is a Bitvector. If + //necessary the indexwidth can be changed later + n.SetIndexWidth(0); + return n; + } + + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTNode& child0, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, child0, children); + n.SetValueWidth(width); + return n; + } + + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, child0, child1, children); + n.SetValueWidth(width); + return n; + } + + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, child0, child1, child2, children); + n.SetValueWidth(width); + return n; + } + + ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg); + 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); + void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); + private: + //memo table for simplifcation + ASTNodeMap SimplifyMap; + ASTNodeMap SimplifyNegMap; + ASTNodeMap SolverMap; + ASTNodeSet AlwaysTrueFormMap; + ASTNodeMap MultInverseMap; + + public: + ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg); + ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2); + ASTNode ITEOpt_InEqs(const ASTNode& in1); + ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3); + 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 FlattenOneLevel(const ASTNode& a); + ASTNode FlattenAndOr(const ASTNode& a); + ASTNode CombineLikeTerms(const ASTNode& a); + ASTNode LhsMinusRhs(const ASTNode& eq); + ASTNode DistributeMultOverPlus(const ASTNode& a, + bool startdistribution=false); + ASTNode ConvertBVSXToITE(const ASTNode& a); + //checks if the input constant is odd or not + bool BVConstIsOdd(const ASTNode& c); + //computes the multiplicatve inverse of the input + ASTNode MultiplicativeInverse(const ASTNode& c); + + void ClearAllTables(void); + void ClearAllCaches(void); + int BeforeSAT_ResultCheck(const ASTNode& q); + int CallSAT_ResultCheck(MINISAT::Solver& newS, + const ASTNode& q, const ASTNode& orig_input); + int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, + const ASTNode& q, const ASTNode& orig_input); + int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); + //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); + ASTVec ArrayWrite_RemainingAxioms; + //variable indicates that counterexample will now be checked by + //the counterexample checker, and hence simplifyterm must switch + //off certain optimizations. In particular, array write + //optimizations + bool start_abstracting; + bool Begin_RemoveWrites; + bool SimplifyWrites_InPlace_Flag; + + void CopySolverMap_To_CounterExample(void); + //int LinearSearch(const ASTNode& orig_input); + //Datastructures and functions needed for counterexample + //generation, and interface with MINISAT + private: + /* MAP: This is a map from ASTNodes to MINISAT::Vars. + * + * The map is populated while ASTclauses are read from the AST + * ClauseList returned by CNF converter. For every new boolean + * variable in ASTClause a new MINISAT::Var is created (these vars + * typedefs for ints) + */ + typedef hash_map<ASTNode, MINISAT::Var, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTtoSATMap; + ASTtoSATMap _ASTNode_to_SATVar; + + public: + //converts the clause to SAT and calls SAT solver + bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll); + + ///print SAT solver statistics + void PrintStats(MINISAT::SolverStats& stats); + + //accepts query and returns the answer. if query is valid, return + //true, else return false. Automatically constructs counterexample + //for invalid queries, and prints them upon request. + int TopLevelSAT(const ASTNode& query, const ASTNode& asserts); + + // Debugging function to find problems in BitBlast and ToCNF. + // See body in ToSAT.cpp for more explanation. + ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form); + + // Internal recursive body of above. + ASTNode CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form); + + // Helper function for CheckBBandCNF + ASTNode SymbolTruthValue(MINISAT::Solver &newS, ASTNode form); + + //looksup a MINISAT var from the minisat-var memo-table. if none + //exists, then creates one. + const MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n); + + // Memo table for CheckBBandCNF debugging function + ASTNodeMap CheckBBandCNFMemo; + + + //Data structures for Array Read Transformations + private: + /* MAP: This is a map from Array Names to list of array-read + * indices in the input. This map is used by the TransformArray() + * function + * + * This map is useful in converting array reads into nested ITE + * constructs. Suppose there are two array reads in the input + * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a + * symbolic constant, say v1, and Read(A,j) is replaced with the + * following ITE: + * + * ITE(i=j,v1,v2) + */ + //CAUTION: I tried using a set instead of vector for + //readindicies. for some odd reason the performance went down + //considerably. this is totally inexplicable. + ASTNodeToVecMap _arrayname_readindices; + + /* MAP: This is a map from Array Names to nested ITE constructs, + * which are built as described below. This map is used by the + * TransformArray() function + * + * This map is useful in converting array reads into nested ITE + * constructs. Suppose there are two array reads in the input + * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a + * symbolic constant, say v1, and Read(A,j) is replaced with the + * following ITE: + * + * ITE(i=j,v1,v2) + */ + ASTNodeMap _arrayread_ite; + + /*MAP: This is a map from array-reads to symbolic constants. This + *map is used by the TransformArray() + */ + ASTNodeMap _arrayread_symbol; + + ASTNodeSet _introduced_symbols; + + /*Memoization map for TransformFormula/TransformTerm/TransformArray function + */ + ASTNodeMap TransformMap; + + //count to keep track of new symbolic constants introduced + //corresponding to Array Reads + unsigned int _symbol_count; + + //Formula/Term Transformers. Let Expr Manager, Type Checker + public: + //Functions that Transform ASTNodes + ASTNode TransformFormula(const ASTNode& query); + ASTNode TransformTerm(const ASTNode& term); + ASTNode TransformArray(const ASTNode& term); + ASTNode TranslateSignedDivMod(const ASTNode& term); + + //LET Management + private: + // MAP: This map is from bound IDs that occur in LETs to + // expression. The map is useful in checking replacing the IDs + // with the corresponding expressions. + ASTNodeMap _letid_expr_map; + public: + + ASTNode ResolveID(const ASTNode& var); + + //Functions that are used to manage LET expressions + void LetExprMgr(const ASTNode& var, const ASTNode& letExpr); + + //Delete Letid Map + void CleanupLetIDMap(void); + + //Allocate LetID map + void InitializeLetIDMap(void); + + //Substitute Let-vars with LetExprs + ASTNode SubstituteLetExpr(ASTNode inExpr); + + /* MAP: This is a map from MINISAT::Vars to ASTNodes + * + * This is a reverse map, useful in constructing + * counterexamples. MINISAT returns a model in terms of MINISAT + * Vars, and this map helps us convert it to a model over ASTNode + * variables. + */ + vector<ASTNode> _SATVar_to_AST; + + private: + /* MAP: This is a map from ASTNodes to vectors of bits + * + * This map is used in constructing and printing + * counterexamples. MINISAT returns values for each bit (a + * BVGETBIT Node), and this maps allows us to assemble the bits + * into bitvectors. + */ + typedef hash_map<ASTNode, hash_map<unsigned int, bool> *, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTtoBitvectorMap; + ASTtoBitvectorMap _ASTNode_to_Bitvector; + + //Data structure that holds the counter-model + ASTNodeMap CounterExampleMap; + + //Checks if the counter_example is ok. In order for the + //counter_example to be ok, Every assert must evaluate to true + //w.r.t couner_example and the query must evaluate to + //false. Otherwise the counter_example is bogus. + void CheckCounterExample(bool t); + + //Converts a vector of bools to a BVConst + ASTNode BoolVectoBVConst(hash_map<unsigned,bool> * w, unsigned int l); + + //accepts a term and turns it into a constant-term w.r.t counter_example + ASTNode TermToConstTermUsingModel(const ASTNode& term, bool ArrayReadFlag = true); + ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool ArrayReadFlag = true); + //Computes the truth value of a formula w.r.t counter_example + ASTNode ComputeFormulaUsingModel(const ASTNode& form); + + //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 NewArrayVar(unsigned int index, unsigned int value); + ASTNode NewVar(unsigned int valuewidth); + //For ArrayWrite Abstraction: map from read-over-write term to + //newname. + ASTNodeMap ReadOverWrite_NewName_Map; + //For ArrayWrite Refinement: Map new arraynames to Read-Over-Write + //terms + ASTNodeMap NewName_ReadOverWrite_Map; + + public: + //print the STP solver output + void PrintOutput(bool true_iff_valid); + + //Converts MINISAT counterexample into an AST memotable (i.e. the + //function populates the datastructure CounterExampleMap) + void ConstructCounterExample(MINISAT::Solver& S); + + //Prints the counterexample to stdout + void PrintCounterExample(bool t,std::ostream& os=cout); + + //Prints the counterexample to stdout + void PrintCounterExample_InOrder(bool t); + + //queries the counterexample, and returns the value corresponding + //to e + ASTNode GetCounterExample(bool t, const ASTNode& e); + + int CounterExampleSize(void) const {return CounterExampleMap.size();} + + //FIXME: This is bloody dangerous function. Hack attack to take + //care of requests from users who want to store complete + //counter-examples in their own data structures. + ASTNodeMap GetCompleteCounterExample() {return CounterExampleMap;} + + // prints MINISAT assigment one bit at a time, for debugging. + void PrintSATModel(MINISAT::Solver& S); + + //accepts constant input and normalizes it. + ASTNode BVConstEvaluator(const ASTNode& t); + + //FUNCTION TypeChecker: Assumes that the immediate Children of the + //input ASTNode have been typechecked. This function is suitable + //in scenarios like where you are building the ASTNode Tree, and + //you typecheck as you go along. It is not suitable as a general + //typechecker + void BVTypeCheck(const ASTNode& n); + + private: + //stack of Logical Context. each entry in the stack is a logical + //context. A logical context is a vector of assertions. The + //logical context is represented by a ptr to a vector of + //assertions in that logical context. Logical contexts are created + //by PUSH/POP + std::vector<ASTVec *> _asserts; + //The query for the current logical context. + ASTNode _current_query; + + //this flag, when true, indicates that counterexample is being + //checked by the counterexample checker + bool counterexample_checking_during_refinement; + + //this flag indicates as to whether the input has been determined to + //be valid or not by this tool + bool ValidFlag; + + //this flag, when true, indicates that a BVDIV divide by zero + //exception occured. However, the program must not exit with a + //fatalerror. Instead, it should evaluate the whole formula (which + //contains the BVDIV term) to be FALSE. + bool bvdiv_exception_occured; + + public: + //set of functions that manipulate Logical Contexts. + // + //add an assertion to the current logical context + void AddAssert(const ASTNode& assert); + void Push(void); + void Pop(void); + void AddQuery(const ASTNode& q); + const ASTNode PopQuery(); + const ASTNode GetQuery(); + const ASTVec GetAsserts(void); + + //reports node size. Second arg is "clearstatinfo", whatever that is. + unsigned int NodeSize(const ASTNode& a, bool t = false); + + private: + //This memo map is used by the ComputeFormulaUsingModel() + ASTNodeMap ComputeFormulaMap; + //Map for statiscal purposes + ASTNodeSet StatInfoSet; + + + ASTNodeMap TermsAlreadySeenMap; + ASTNode CreateSubstitutionMap(const ASTNode& a); + public: + //prints statistics for the ASTNode. can add a prefix string c + void ASTNodeStats(const char * c, const ASTNode& a); + + //substitution + bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); + bool CheckSubstitutionMap(const ASTNode& a); + bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); + //if (a > b) in the termorder, then return 1 + //elseif (a < b) in the termorder, then return -1 + //else return 0 + int TermOrder(const ASTNode& a, const ASTNode& b); + //fill the arrayname_readindices vector if e0 is a READ(Arr,index) + //and index is a BVCONST + void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1); + bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); + + //functions for checking and updating simplifcation map + bool CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg); + void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg); + bool CheckAlwaysTrueFormMap(const ASTNode& key); + void UpdateAlwaysTrueFormMap(const ASTNode& val); + bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); + void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); + + //Map for solved variables + bool CheckSolverMap(const ASTNode& a, ASTNode& output); + bool CheckSolverMap(const ASTNode& a); + bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); + public: + //FIXME: HACK_ATTACK. this vector was hacked into the code to + //support a special request by Dawson' group. They want the + //counterexample to be printed in the order of variables declared. + //TO BE COMMENTED LATER (say by 1st week of march,2006) + ASTVec _special_print_set; + + //prints the initial activity levels of variables + void PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS); + + //this function biases the activity levels of MINISAT variables. + void ChangeActivityLevels_Of_SATVars(MINISAT::Solver& n); + + // Constructor + BeevMgr() : _interior_unique_table(INITIAL_INTERIOR_UNIQUE_TABLE_SIZE), + _symbol_unique_table(INITIAL_SYMBOL_UNIQUE_TABLE_SIZE), + _bvconst_unique_table(INITIAL_BVCONST_UNIQUE_TABLE_SIZE), + BBTermMemo(INITIAL_BBTERM_MEMO_TABLE_SIZE), + BBFormMemo(INITIAL_BBFORM_MEMO_TABLE_SIZE), + _max_node_num(0), + ASTFalse(CreateNode(FALSE)), + ASTTrue(CreateNode(TRUE)), + ASTUndefined(CreateNode(UNDEFINED)), + SimplifyMap(INITIAL_SIMPLIFY_MAP_SIZE), + SimplifyNegMap(INITIAL_SIMPLIFY_MAP_SIZE), + SolverMap(INITIAL_SOLVER_MAP_SIZE), + _arrayread_symbol(INITIAL_ARRAYREAD_SYMBOL_SIZE), + _introduced_symbols(INITIAL_INTRODUCED_SYMBOLS_SIZE), + _symbol_count(0) { + _current_query = ASTUndefined; + ValidFlag = false; + bvdiv_exception_occured = false; + counterexample_checking_during_refinement = false; + start_abstracting = false; + Begin_RemoveWrites = false; + SimplifyWrites_InPlace_Flag = false; + }; + + //destructor + ~BeevMgr(); + }; //End of Class BeevMgr + + + class CompleteCounterExample { + ASTNodeMap counterexample; + BeevMgr * bv; + public: + CompleteCounterExample(ASTNodeMap a, BeevMgr* beev) : counterexample(a), bv(beev){} + ASTNode GetCounterExample(ASTNode e) { + if(BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind()) { + FatalError("You must input a term or propositional variables\n",e); + } + if(counterexample.find(e) != counterexample.end()) { + return counterexample[e]; + } + else { + if(SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType()) { + return bv->CreateNode(BEEV::FALSE); + } + + if(SYMBOL == e.GetKind()) { + ASTNode z = bv->CreateZeroConst(e.GetValueWidth()); + return z; + } + + return e; + } + } + }; + +}; // end namespace BEEV +#endif |