From: vijay_ganesh Date: Fri, 2 Oct 2009 20:08:29 +0000 (+0000) Subject: massiv code cleanup. Created separate files for ASTNode, ASTInternal, ASTInterior... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=6923293ab1752a6209a9d1c75507f554521d25c4;p=francis%2Fstp.git massiv code cleanup. Created separate files for ASTNode, ASTInternal, ASTInterior, ASTSymbol, ASTBVConst git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@271 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/Makefile b/Makefile index 98832fc..29b31ae 100644 --- a/Makefile +++ b/Makefile @@ -18,6 +18,7 @@ HEADERS=$(SRC)/c_interface/*.h .PHONY: all all: $(MAKE) -C $(SRC)/AST + $(MAKE) -C $(SRC)/printer $(MAKE) -C $(SRC)/abstraction-refinement $(MAKE) -C $(SRC)/to-sat $(MAKE) -C $(SRC)/sat core @@ -29,7 +30,7 @@ all: $(MAKE) -C $(SRC)/extlib-constbv $(MAKE) -C $(SRC)/parser $(MAKE) -C $(SRC)/main - $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/abstraction-refinement/*.o $(SRC)/to-sat/*.o \ + $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/printer/*.o $(SRC)/abstraction-refinement/*.o $(SRC)/to-sat/*.o \ $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/const-evaluator/*.o $(SRC)/extlib-constbv/*.o $(SRC)/c_interface/*.o \ $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o $(RANLIB) libstp.a @@ -58,6 +59,7 @@ clean: rm -rf *.log rm -f TAGS $(MAKE) clean -C $(SRC)/AST + $(MAKE) clean -C $(SRC)/printer $(MAKE) clean -C $(SRC)/abstraction-refinement $(MAKE) clean -C $(SRC)/to-sat $(MAKE) clean -C $(SRC)/sat diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 98832fc..29b31ae 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -18,6 +18,7 @@ HEADERS=$(SRC)/c_interface/*.h .PHONY: all all: $(MAKE) -C $(SRC)/AST + $(MAKE) -C $(SRC)/printer $(MAKE) -C $(SRC)/abstraction-refinement $(MAKE) -C $(SRC)/to-sat $(MAKE) -C $(SRC)/sat core @@ -29,7 +30,7 @@ all: $(MAKE) -C $(SRC)/extlib-constbv $(MAKE) -C $(SRC)/parser $(MAKE) -C $(SRC)/main - $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/abstraction-refinement/*.o $(SRC)/to-sat/*.o \ + $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/printer/*.o $(SRC)/abstraction-refinement/*.o $(SRC)/to-sat/*.o \ $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/const-evaluator/*.o $(SRC)/extlib-constbv/*.o $(SRC)/c_interface/*.o \ $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o $(RANLIB) libstp.a @@ -58,6 +59,7 @@ clean: rm -rf *.log rm -f TAGS $(MAKE) clean -C $(SRC)/AST + $(MAKE) clean -C $(SRC)/printer $(MAKE) clean -C $(SRC)/abstraction-refinement $(MAKE) clean -C $(SRC)/to-sat $(MAKE) clean -C $(SRC)/sat diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 881c4ee..8067f3e 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -9,8 +9,8 @@ #include "AST.h" #include -#include "printer/printers.h" -#include "printer/AssortedPrinters.h" +//#include "../printer/printers.h" +//#include "../printer/AssortedPrinters.h" namespace BEEV { diff --git a/src/AST/AST.h b/src/AST/AST.h index 2615cc9..abf800a 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -9,390 +9,15 @@ #ifndef AST_H #define AST_H +#include "TopLevel.h" +#include "ASTInternal.h" +#include "ASTInterior.h" +#include "ASTNode.h" +#include "ASTSymbol.h" +#include "ASTBVConst.h" -#include -#ifdef EXT_HASH_MAP -#include -#include -#elif defined(TR1_UNORDERED_MAP) -#include -#include -#define hash_map tr1::unordered_map -#define hash_set tr1::unordered_set -#define hash_multiset tr1::unordered_multiset -#else -#include -#include -#endif -#include -#include -#include -#include -#include -#include -#include "../main/Globals.h" -#include "ASTUtil.h" -#include "ASTKind.h" -#include -#include -#include "../extlib-constbv/constantbv.h" -#include "RunTimes.h" - -/***************************************************************************** - * 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 - - class BeevMgr; - class ASTNode; - class ASTInternal; - class ASTInterior; - class ASTSymbol; - class ASTBVConst; - class BVSolver; - - - template - struct enumeration - { - typedef T type; - typedef E enum_type; - - enumeration() - : e_(E()) - {} - - enumeration(E e) - : e_(static_cast(e)) - {} - - operator E() const - { return static_cast(e_); } - - private: - T e_; - }; - - //Useful typedefs: Vector of ASTNodes, used for child nodes among - //other things. - typedef vector ASTVec; - typedef unsigned int * CBV; - extern ASTVec _empty_ASTVec; - /***************************************************************************/ - /* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */ - /***************************************************************************/ - class ASTNode - { - friend class BeevMgr; - friend class CNFMgr; - friend class ASTInterior; - friend class vector; - //Print the arguments in lisp format. - friend ostream &LispPrintVec(ostream &os, - const ASTVec &v, - int indentation = 0); - friend ostream &LispPrintVecSpecial(ostream &os, - const vector &v, - int indentation = 0); - - private: - ASTInternal * _int_node_ptr; // The real data. - - // Usual constructor. - ASTNode(ASTInternal *in); - - //Integer that helps sort the ASTNodes. This sorting is different - //from the sorting based on NodeNum. This is used as a way of - //achieving abstraction-refinement. - //unsigned int _sort_for_absrefine; - - //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); - } - - //MKK: This shouldn't be necessary, but for some inexplicable reason I - //cannot get ToSAT.cpp to compile. The differences between the old files - //(AST.h, ToSAT.cpp) and the new files are very minor, mostly Solver -> - //Solver, and so the compiler errors are difficult to understand. - friend bool operator!=(const ASTNode node1, const ASTNode node2) - { - return !(node1 == 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: - // //Set the sorting integer for abstraction refinement - // void SetAbsRefineInt(unsigned int a) {_sort_for_absrefine = a;} - - // //Get the sorting integer for abstraction refinement - // unsigned int GetAbsRefineInt(void) {return _sort_for_absrefine;} - - // //Compare two ASTNodes based on their abstraction refinement - // //number - // bool CmpAbsRefine(const ASTNode node1, const ASTNode node2) { - // return (node1._sort_for_absrefine < node2._sort_for_absrefine); - // } - - //Check if it points to a null node - bool IsNull() const - { - return _int_node_ptr == NULL; - } - - // This is for sorting by expression number (used in Boolean - //optimization). - // With any ordering operation, the properties of the order - // need to be carefully specified. In this case, we just - // need identical exprs to be consecutive, and (NOT x) to - // follow "x" immediately. For some time, this function was - // "arithless" (below), which separates x and (NOT x) in some - // cases. - // DO NOT MODIFY WITHOUT CHECKING WITH DAVID DILL FIRST! - friend bool exprless(const ASTNode n1, const ASTNode n2) - { - return (n1.GetNodeNum() < n2.GetNodeNum()); - } // end of exprless - - // This is for sorting by arithmetic expressions (for - // combining like terms, etc.) - friend bool arithless(const ASTNode n1, const ASTNode n2) - { - Kind k1 = n1.GetKind(); - Kind k2 = n2.GetKind(); - - if (n1 == n2) - { - // necessary for "strict weak ordering" - return false; - } - else if (BVCONST == k1 && BVCONST != k2) - { - // put consts first - return true; - } - else if (BVCONST != k1 && BVCONST == k2) - { - // put consts first - return false; - } - else if (SYMBOL == k1 && SYMBOL != k2) - { - // put symbols next - return true; - } - else if (SYMBOL != k1 && SYMBOL == k2) - { - // put symbols next - return false; - } - else - { - // otherwise, sort by exprnum (descendents will appear - // before ancestors). - return (n1.GetNodeNum() < n2.GetNodeNum()); - } - } //end of arithless - - // For lisp DAG printing. Has it been printed already, so we can - // just print the node number? - bool IsAlreadyPrinted() const; - void MarkAlreadyPrinted() const; - - // delegates to the ASTInternal node. - void nodeprint(ostream& os, bool c_friendly = false) 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) - { - //_sort_for_absrefine=0; - } - ; - - // 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 - // The result should be treated as const. - const char * /**const**/ GetName() const; - - //Get the BVCONST value - // The result should be treated as const. - /*const*/ CBV GetBVConst() const; - - /*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; - void SetIndexWidth(unsigned int iw) const; - - unsigned int GetValueWidth() const; - 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(); - } - - void NFASTPrint(int l, int max, int prefix) const; - - // lisp-form printer - ostream& LispPrint(ostream &os, int indentation = 0) const; - ostream &LispPrint_indent(ostream &os, int indentation) const; - - //Presentation Language Printer - ostream& PL_Print(ostream &os, int indentation = 0) 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); @@ -402,439 +27,6 @@ namespace BEEV bool arithless(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; - friend class CNFMgr; - - protected: - // reference count. - //#ifdef LESSBYTES_PERNODE - //unsigned short _ref_count; - //#else - unsigned int _ref_count; - //#endif - - // Kind. It's a type tag and the operator. - enumeration _kind; - - // The vector of children (*** should this be in ASTInterior? ***) - ASTVec _children; - - //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). - unsigned 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. -#ifdef LESSBYTES_PERNODE - unsigned char _index_width; -#else - unsigned int _index_width; -#endif - - // 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. -#ifdef LESSBYTES_PERNODE - unsigned char _value_width; -#else - unsigned int _value_width; -#endif - - // Increment refcount. - void IncRef() - { - ++_ref_count; - } - - // 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(); - - // Treat the result as const pleases - 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(int nodenum = 0) : - _ref_count(0), _kind(UNDEFINED), - _node_num(nodenum), _index_width(0), _value_width(0) - { - } - - // Constructor (kind only, empty children, int nodenum) - ASTInternal(Kind kind, int nodenum = 0) : - _ref_count(0), _kind(kind), - _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, int nodenum = 0) : - _ref_count(0), _kind(kind), _children(children), - _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), - _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. - // (c_friendly is for printing hex. numbers that C compilers will accept) - virtual void nodeprint(ostream& os, bool c_friendly = false) - { - 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. (c_friendly is for printing hex. numbers that C - // compilers will accept) - virtual void nodeprint(ostream& os, bool c_friendly = false) - { - 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" in here. - - // Basic constructors - ASTInterior(Kind kind) : - ASTInternal(kind) - { - } - - ASTInterior(Kind kind, ASTVec &children) : - ASTInternal(kind, children) - { - } - - //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 - { -#ifdef TR1_UNORDERED_MAP - tr1::hash h; -#else - hash h; -#endif - 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 */ - // (c_friendly is for printing hex. numbers that C compilers will accept) - virtual void nodeprint(ostream& os, bool c_friendly = false) - { - os << _name; - } - - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); - - public: - - // Default constructor - ASTSymbol() : - ASTInternal(), _name(NULL) - { - } - - // Constructor. This does NOT copy its argument. - ASTSymbol(const char * const name) : - ASTInternal(SYMBOL), _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), _name(sym._name) - { - } - }; //End of ASTSymbol - - - /***************************************************************************/ - /* Class ASTBVConst: Class to represent internals of a bitvectorconst */ - /***************************************************************************/ - 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) : - ASTInternal(BVCONST) - { - _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 - // (c_friendly is for printing hex. numbers that C compilers will accept) - virtual void nodeprint(ostream& os, bool c_friendly = false) - { - unsigned char *res; - const char *prefix; - - if(print_binary_flag) { - res = CONSTANTBV::BitVector_to_Bin(_bvconst); - if (c_friendly) - { - prefix = "0b"; - } - else - { - prefix = "0bin"; - } - } - else if (_value_width % 4 == 0) - { - res = CONSTANTBV::BitVector_to_Hex(_bvconst); - if (c_friendly) - { - prefix = "0x"; - } - else - { - prefix = "0hex"; - } - } - else - { - res = CONSTANTBV::BitVector_to_Bin(_bvconst); - if (c_friendly) - { - prefix = "0b"; - } - else - { - prefix = "0bin"; - } - } - 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) - { - _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 /*************************************************************************** * Typedef ASTNodeMap: This is a hash table from ASTNodes to ASTNodes. diff --git a/src/AST/ASTBVConst.h b/src/AST/ASTBVConst.h new file mode 100644 index 0000000..1f41f17 --- /dev/null +++ b/src/AST/ASTBVConst.h @@ -0,0 +1,175 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef ASTBVCONST_H +#define ASTBVCONST_H +namespace BEEV +{ + void FatalError(const char * str); + + /****************************************************************** + * Class ASTBVConst: * + * * + * Class to represent internals of a bitvector constant * + ******************************************************************/ + class ASTBVConst: public ASTInternal + { + friend class BeevMgr; + friend class ASTNode; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + /**************************************************************** + * Private Data * + ****************************************************************/ + + //CBV is actually an unsigned*. The bitvector constant is + //represented using an external library in extlib-bvconst. + CBV _bvconst; + + /**************************************************************** + * Class ASTBVConstHasher: * + * * + * Hasher for ASTBVConst nodes * + ****************************************************************/ + class ASTBVConstHasher + { + public: + size_t operator()(const ASTBVConst * bvc) const + { + return CONSTANTBV::BitVector_Hash(bvc->_bvconst); + } + ; + }; + + /**************************************************************** + * Class ASTBVConstEqual: * + * * + * Equality for ASTBVConst nodes * + ****************************************************************/ + 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)); + } + }; + + + /**************************************************************** + * Private Functions (virtual defs and friends) * + ****************************************************************/ + ASTBVConst(CBV bv, unsigned int width) : + ASTInternal(BVCONST) + { + _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 (c_friendly is for printing hex. numbers that C + // compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) + { + unsigned char *res; + const char *prefix; + + if(print_binary_flag) { + res = CONSTANTBV::BitVector_to_Bin(_bvconst); + if (c_friendly) + { + prefix = "0b"; + } + else + { + prefix = "0bin"; + } + } + else if (_value_width % 4 == 0) + { + res = CONSTANTBV::BitVector_to_Hex(_bvconst); + if (c_friendly) + { + prefix = "0x"; + } + else + { + prefix = "0hex"; + } + } + else + { + res = CONSTANTBV::BitVector_to_Bin(_bvconst); + if (c_friendly) + { + prefix = "0b"; + } + else + { + prefix = "0bin"; + } + } + 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) + { + _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst); + _value_width = sym._value_width; + } + + public: + + /**************************************************************** + * Public Member Functions * + ****************************************************************/ + + //Destructor. Call the external destructor + virtual ~ASTBVConst() + { + CONSTANTBV::BitVector_Destroy(_bvconst); + } + + // Return the bvconst. It is a const-value + CBV GetBVConst() const + { + return _bvconst; + } + }; //End of ASTBVConst +};//end of namespace +#endif diff --git a/src/AST/ASTInterior.h b/src/AST/ASTInterior.h new file mode 100644 index 0000000..04b0481 --- /dev/null +++ b/src/AST/ASTInterior.h @@ -0,0 +1,105 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef ASTINTERIOR_H +#define ASTINTERIOR_H +namespace BEEV +{ + /****************************************************************** + * 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: + /****************************************************************** + * Private Data and Member Functions * + ******************************************************************/ + + /****************************************************************** + * Class ASTInteriorHasher: * + * * + * Hasher for ASTInterior pointer nodes * + ******************************************************************/ + class ASTInteriorHasher + { + public: + size_t operator()(const ASTInterior *int_node_ptr) const; + }; + + /****************************************************************** + * Class ASTInteriorEqual: * + * * + * 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. (c_friendly is for printing hex. numbers that C + // compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) + { + os << _kind_names[_kind]; + } + public: + /****************************************************************** + * Public Member Functions * + ******************************************************************/ + + // Basic constructors + ASTInterior(Kind kind) : + ASTInternal(kind) + { + } + + ASTInterior(Kind kind, ASTVec &children) : + ASTInternal(kind, children) + { + } + + //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 +}; //end of namespace BEEV +#endif diff --git a/src/AST/ASTInternal.h b/src/AST/ASTInternal.h new file mode 100644 index 0000000..5d9da1b --- /dev/null +++ b/src/AST/ASTInternal.h @@ -0,0 +1,174 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +#ifndef ASTINTERNAL_H +#define ASTINTERNAL_H + +/******************************************************************** + * This file gives the class description of the ASTInternal class * + ********************************************************************/ +namespace BEEV +{ + /****************************************************************** + * 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; + friend class CNFMgr; + + protected: + /**************************************************************** + * Protected Data * + ****************************************************************/ + + //reference counting for garbage collection + unsigned int _ref_count; + + // Kind. It's a type tag and the operator. + enumeration _kind; + + // The vector of children + ASTVec _children; + + //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). + //FIXME: Get rid of this + unsigned int _node_num; + + /******************************************************************* + * 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))* + * * + * Width of the index of an array. Positive for array, 0 otherwise * + *******************************************************************/ +#ifdef LESSBYTES_PERNODE + unsigned char _index_width; +#else + unsigned int _index_width; +#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))* + * * + * Number of bits of bitvector. +ve for array/bitvector,0 otherwise* + *******************************************************************/ +#ifdef LESSBYTES_PERNODE + unsigned char _value_width; +#else + unsigned int _value_width; +#endif + + /**************************************************************** + * Protected Member Functions * + ****************************************************************/ + + // 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. (c_friendly + // is for printing hex. numbers that C compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) + { + os << "*"; + } + ; + + // Treat the result as const pleases + virtual Kind GetKind() const + { + return _kind; + } + + // Get the child nodes of this node + virtual ASTVec const &GetChildren() const + { + return _children; + } + + public: + + /**************************************************************** + * Public Member Functions * + ****************************************************************/ + + // Constructor + ASTInternal(int nodenum = 0) : + _ref_count(0), _kind(UNDEFINED), + _node_num(nodenum), + _index_width(0), _value_width(0) + { + } + + // Constructor (kind only, empty children, int nodenum) + ASTInternal(Kind kind, int nodenum = 0) : + _ref_count(0), _kind(kind), + _node_num(nodenum), + _index_width(0), _value_width(0) + { + } + + // Constructor (kind and children). + ASTInternal(Kind kind, const ASTVec &children, int nodenum = 0) : + _ref_count(0), _kind(kind), _children(children), + _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), + _node_num(int_node._node_num), + _index_width(int_node._index_width), + _value_width(int_node._value_width) + { + } + + // Increment Reference Count + void IncRef() + { + ++_ref_count; + } + + // Decrement Reference Count + void DecRef(); + + int GetNodeNum() const + { + return _node_num; + } + + void SetNodeNum(int nn) + { + _node_num = nn; + } + ; + }; //End of Class ASTInternal + +}; //end of namespace +#endif diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h new file mode 100644 index 0000000..809e665 --- /dev/null +++ b/src/AST/ASTNode.h @@ -0,0 +1,292 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +#ifndef ASTNODE_H +#define ASTNODE_H + +/******************************************************************** + * This file gives the class description of the ASTNode class * + ********************************************************************/ +namespace BEEV +{ + /****************************************************************** + * Class ASTNode: * + * * + * A Kind of Smart pointer to actual ASTInternal datastructure. * + * This class defines the node datastructure for the DAG that * + * captures input formulas to STP. * + ******************************************************************/ + class ASTNode + { + friend class BeevMgr; + friend class CNFMgr; + friend class ASTInterior; + friend class vector; + + private: + /**************************************************************** + * Private Data * + ****************************************************************/ + + // Ptr to the read data + ASTInternal * _int_node_ptr; + + /**************************************************************** + * Private Member Functions * + ****************************************************************/ + + // Constructor. + ASTNode(ASTInternal *in); + + //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); + } + + friend bool operator!=(const ASTNode node1, const ASTNode node2) + { + return !(node1 == node2); + } + + friend bool operator<(const ASTNode node1, const ASTNode node2) + { + //FIXME: Nondeterministic code. Questionable pointer comparison + return + ((size_t) node1._int_node_ptr) < + ((size_t) node2._int_node_ptr); + } + + public: + /**************************************************************** + * Public Member Functions * + ****************************************************************/ + // Default constructor. + ASTNode() :_int_node_ptr(NULL) {}; + + // Copy constructor + ASTNode(const ASTNode &n); + + // Destructor + ~ASTNode(); + + // Print the arguments in lisp format + friend ostream &LispPrintVec(ostream &os, + const ASTVec &v, + int indentation = 0); + + // Print the arguments in lisp format + friend ostream &LispPrintVecSpecial(ostream &os, + const vector &v, + int indentation = 0); + + // Check if it points to a null node + inline bool IsNull() const + { + return _int_node_ptr == NULL; + } + + // Sort ASTNodes by expression numbers + friend bool exprless(const ASTNode n1, const ASTNode n2) + { + return (n1.GetNodeNum() < n2.GetNodeNum()); + } + + // This is for sorting by arithmetic expressions (for + // combining like terms, etc.) + friend bool arithless(const ASTNode n1, const ASTNode n2) + { + Kind k1 = n1.GetKind(); + Kind k2 = n2.GetKind(); + + if (n1 == n2) + { + // necessary for "strict weak ordering" + return false; + } + else if (BVCONST == k1 && BVCONST != k2) + { + // put consts first + return true; + } + else if (BVCONST != k1 && BVCONST == k2) + { + // put consts first + return false; + } + else if (SYMBOL == k1 && SYMBOL != k2) + { + // put symbols next + return true; + } + else if (SYMBOL != k1 && SYMBOL == k2) + { + // put symbols next + return false; + } + else + { + // otherwise, sort by exprnum (descendents will appear + // before ancestors). + return (n1.GetNodeNum() < n2.GetNodeNum()); + } + } //end of arithless + + // For lisp DAG printing. Has it been printed already, so we can + // just print the node number? + bool IsAlreadyPrinted() const; + void MarkAlreadyPrinted() const; + + // delegates to the ASTInternal node. + void nodeprint(ostream& os, bool c_friendly = false) const; + + // Assignment (for ref counting) + ASTNode& operator=(const ASTNode& n); + + //Get the BeevMgr pointer. FIXME: Currently uses a global + //ptr. BAD!! + BeevMgr* GetBeevMgr() const; + + // Access node number + int GetNodeNum() const; + + // Access kind. + Kind GetKind() const; + + // Access Children of this Node + 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. + CBV GetBVConst() const; + + /******************************************************************* + * 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; + unsigned int GetValueWidth() const; + void SetIndexWidth(unsigned int iw) const; + void SetValueWidth(unsigned int vw) const; + types GetType(void) const; + + // Hash using pointer value of _int_node_ptr. + size_t Hash() const + { + return (size_t) _int_node_ptr; + } + + void NFASTPrint(int l, int max, int prefix) const; + + // Lisp-form printer + ostream& LispPrint(ostream &os, int indentation = 0) const; + ostream &LispPrint_indent(ostream &os, int indentation) const; + + // Presentation Language Printer + ostream& PL_Print(ostream &os, int indentation = 0) 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); + + // Printing to stream + friend ostream &operator<<(ostream &os, const ASTNode &node) + { + node.LispPrint(os, 0); + return os; + } + ; + + // Check if NODE really has a good ptr + bool IsDefined() const + { + return _int_node_ptr != NULL; + } + + /***************************************************************** + * Class ASTNodeHahser: * + * * + * 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 + + /***************************************************************** + * Class ASTNodeEqual: * + * * + * 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 +}; //end of namespace +#endif diff --git a/src/AST/ASTSymbol.h b/src/AST/ASTSymbol.h new file mode 100644 index 0000000..f968ccb --- /dev/null +++ b/src/AST/ASTSymbol.h @@ -0,0 +1,122 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef ASTSYMBOL_H +#define ASTSYMBOL_H +namespace BEEV +{ + /****************************************************************** + * 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: + /**************************************************************** + * Private Data * + ****************************************************************/ + + // The name of the symbol + const char * const _name; + + /**************************************************************** + * Class ASTSymbolHasher: * + * * + * Hasher for ASTSymbol nodes * + ****************************************************************/ + class ASTSymbolHasher + { + public: + size_t operator()(const ASTSymbol *sym_ptr) const + { +#ifdef TR1_UNORDERED_MAP + tr1::hash h; +#else + hash h; +#endif + return h(sym_ptr->_name); + } + ; + }; + + /**************************************************************** + * Class ASTSymbolEqual: * + * * + * Equality for ASTSymbol 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; + } + + /**************************************************************** + * Private Member Functions * + ****************************************************************/ + + // Print function for symbol -- return name. (c_friendly is for + // printing hex. numbers that C compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) + { + os << _name; + } + + // Call this when deleting a node that has been stored in the the + // unique table + virtual void CleanUp(); + + public: + + /**************************************************************** + * Public Member Functions * + ****************************************************************/ + + // Default constructor + ASTSymbol() : ASTInternal(), _name(NULL) + { + } + + // Constructor. This does NOT copy its argument. + ASTSymbol(const char * const name) : + ASTInternal(SYMBOL), _name(name) + { + } + + // Destructor (does nothing, but is declared virtual here. + virtual ~ASTSymbol(); + + // Copy constructor + ASTSymbol(const ASTSymbol &sym) : + ASTInternal(sym._kind, sym._children), _name(sym._name) + { + } + }; //End of ASTSymbol +}; //end of namespace +#endif diff --git a/src/AST/Makefile b/src/AST/Makefile index b1279fb..e7b2cb1 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -1,6 +1,6 @@ include ../../scripts/Makefile.common -SRCS=$(wildcard *.cpp printer/*.cpp) +SRCS=$(wildcard *.cpp) OBJS = $(SRCS:.cpp=.o) OBJS+= ASTKind.o CFLAGS += -I../sat/mtl -I../sat/core @@ -18,7 +18,6 @@ ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl .PHONY: clean clean: rm -rf *.o *~ bbtest asttest cnftest *.a ASTKind.cpp ASTKind.h .#* - rm -rf printer/*.o printer/*~ depend: $(SRCS) ASTKind.h ASTKind.cpp @$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@ diff --git a/src/AST/TopLevel.h b/src/AST/TopLevel.h new file mode 100644 index 0000000..a8971db --- /dev/null +++ b/src/AST/TopLevel.h @@ -0,0 +1,99 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +#ifndef TOPLEVEL_H +#define TOPLEVEL_H + +#include +#ifdef EXT_HASH_MAP +#include +#include +#elif defined(TR1_UNORDERED_MAP) +#include +#include +#define hash_map tr1::unordered_map +#define hash_set tr1::unordered_set +#define hash_multiset tr1::unordered_multiset +#else +#include +#include +#endif +#include +#include +#include +#include +#include +#include +#include "../main/Globals.h" +#include "ASTUtil.h" +#include "ASTKind.h" +#include +#include +#include "../extlib-constbv/constantbv.h" +#include "RunTimes.h" + +namespace BEEV { + using namespace std; + using namespace MINISAT; +#ifdef EXT_HASH_MAP + using namespace __gnu_cxx; +#endif + + /****************************************************************** + * struct enumeration: * + * * + * Templated class that allows you to define the number of bytes * + * (using class T below) for the enumerated type class E. * + ******************************************************************/ + template + struct enumeration + { + typedef T type; + typedef E enum_type; + + enumeration() : e_(E()) + {} + + enumeration(E e) : e_(static_cast(e)) + {} + + operator E() const + { return static_cast(e_); } + + private: + T e_; + }; //end of Enumeration struct + + /****************************************************************** + * Important classes declared as part of AST datastructures * + * * + ******************************************************************/ + class BeevMgr; + class ASTNode; + class ASTInternal; + class ASTInterior; + class ASTSymbol; + class ASTBVConst; + class BVSolver; + + /****************************************************************** + * Useful typedefs: * + * * + * Vector of ASTNodes, used for child nodes among other things. * + * It is good to define hash_map and hash_set in case we want to * + * use libraries other than STL. * + ******************************************************************/ + typedef vector ASTVec; + typedef unsigned int * CBV; +#define HASHMAP hash_map; +#define HASHSET hash_set; + extern ASTVec _empty_ASTVec; + +}; //end of namespace + +#endif diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index ba7635e..11b902a 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -20,7 +20,7 @@ #include #include #include "AST.h" -#include "printer/printers.h" +//#include "../printer/printers.h" namespace BEEV { diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 2473988..714b05e 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -12,7 +12,7 @@ #include #include "fdstream.h" #include "../AST/AST.h" -#include "../AST/printer/printers.h" +#include "../printer/printers.h" //These typedefs lower the effort of using the keyboard to type (too //many overloaded meanings of the word type) diff --git a/src/main/Makefile b/src/main/Makefile index b31e490..9b7121a 100644 --- a/src/main/Makefile +++ b/src/main/Makefile @@ -5,6 +5,7 @@ OBJS = $(SRCS:.cpp=.o) LIBS = -L../to-sat -ltosat \ -L../AST -last \ + -L../printer -lprinter \ -L../abstraction-refinement -labstractionrefinement \ -L../sat -lminisat \ -L../simplifier -lsimplifier \ diff --git a/src/main/main.cpp b/src/main/main.cpp index f7bcfa9..e94bef6 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -7,8 +7,8 @@ ********************************************************************/ // -*- c++ -*- #include "../AST/AST.h" -#include "../AST/printer/AssortedPrinters.h" -#include "../AST/printer/printers.h" +#include "../printer/AssortedPrinters.h" +#include "../printer/printers.h" #ifdef EXT_HASH_MAP using namespace __gnu_cxx; diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/printer/AssortedPrinters.cpp similarity index 99% rename from src/AST/printer/AssortedPrinters.cpp rename to src/printer/AssortedPrinters.cpp index 1af9eba..e2600d1 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/printer/AssortedPrinters.cpp @@ -7,10 +7,9 @@ ********************************************************************/ // -*- c++ -*- -#include "../AST.h" -#include "AssortedPrinters.h" #include "printers.h" -#include "../../sat/sat.h" +#include "AssortedPrinters.h" +#include "../sat/sat.h" // to get the PRIu64 macro from inttypes, this needs to be defined. #define __STDC_FORMAT_MACROS diff --git a/src/AST/printer/AssortedPrinters.h b/src/printer/AssortedPrinters.h similarity index 98% rename from src/AST/printer/AssortedPrinters.h rename to src/printer/AssortedPrinters.h index f921db5..3f8f872 100644 --- a/src/AST/printer/AssortedPrinters.h +++ b/src/printer/AssortedPrinters.h @@ -10,8 +10,7 @@ #ifndef PRINTER_H #define PRINTER_H -#include "../AST.h" - +#include "../AST/AST.h" namespace BEEV { using namespace std; diff --git a/src/AST/printer/CPrinter.cpp b/src/printer/CPrinter.cpp similarity index 100% rename from src/AST/printer/CPrinter.cpp rename to src/printer/CPrinter.cpp diff --git a/src/AST/printer/LispPrinter.cpp b/src/printer/LispPrinter.cpp similarity index 100% rename from src/AST/printer/LispPrinter.cpp rename to src/printer/LispPrinter.cpp diff --git a/src/AST/printer/PLPrinter.cpp b/src/printer/PLPrinter.cpp similarity index 100% rename from src/AST/printer/PLPrinter.cpp rename to src/printer/PLPrinter.cpp diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp similarity index 100% rename from src/AST/printer/SMTLIBPrinter.cpp rename to src/printer/SMTLIBPrinter.cpp diff --git a/src/AST/printer/dotPrinter.cpp b/src/printer/dotPrinter.cpp similarity index 100% rename from src/AST/printer/dotPrinter.cpp rename to src/printer/dotPrinter.cpp diff --git a/src/AST/printer/printers.h b/src/printer/printers.h similarity index 91% rename from src/AST/printer/printers.h rename to src/printer/printers.h index 9b15a6d..faa01b1 100644 --- a/src/AST/printer/printers.h +++ b/src/printer/printers.h @@ -10,9 +10,9 @@ #ifndef PRINTERS_H_ #define PRINTERS_H_ -#include "../AST.h" -#include "../ASTUtil.h" -#include "../ASTKind.h" +#include "../AST/AST.h" +#include "../AST/ASTUtil.h" +#include "../AST/ASTKind.h" namespace printer {