diff options
Diffstat (limited to 'stp/AST/AST.h')
| -rw-r--r-- | stp/AST/AST.h | 1806 |
1 files changed, 0 insertions, 1806 deletions
diff --git a/stp/AST/AST.h b/stp/AST/AST.h deleted file mode 100644 index 3052107f..00000000 --- a/stp/AST/AST.h +++ /dev/null @@ -1,1806 +0,0 @@ -// -*- 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> -#include <stdint.h> -#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 *GetName() const; - - //Get the BVCONST value -#ifndef NATIVE_C_ARITH - 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. - 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 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 *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. - 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 |