.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
$(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
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
.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
$(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
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
#include "AST.h"
#include <assert.h>
-#include "printer/printers.h"
-#include "printer/AssortedPrinters.h"
+//#include "../printer/printers.h"
+//#include "../printer/AssortedPrinters.h"
namespace BEEV
{
#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 <vector>
-#ifdef EXT_HASH_MAP
-#include <ext/hash_set>
-#include <ext/hash_map>
-#elif defined(TR1_UNORDERED_MAP)
-#include <tr1/unordered_map>
-#include <tr1/unordered_set>
-#define hash_map tr1::unordered_map
-#define hash_set tr1::unordered_set
-#define hash_multiset tr1::unordered_multiset
-#else
-#include <hash_set>
-#include <hash_map>
-#endif
-#include <iostream>
-#include <sstream>
-#include <string>
-#include <map>
-#include <set>
-#include <algorithm>
-#include "../main/Globals.h"
-#include "ASTUtil.h"
-#include "ASTKind.h"
-#include <stdint.h>
-#include <stdlib.h>
-#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 <class E, class T>
- struct enumeration
- {
- typedef T type;
- typedef E enum_type;
-
- enumeration()
- : e_(E())
- {}
-
- enumeration(E e)
- : e_(static_cast<T>(e))
- {}
-
- operator E() const
- { return static_cast<E>(e_); }
-
- private:
- T e_;
- };
-
- //Useful typedefs: Vector of ASTNodes, used for child nodes among
- //other things.
- typedef vector<ASTNode> 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<ASTNode>;
- //Print the arguments in lisp format.
- friend ostream &LispPrintVec(ostream &os,
- const ASTVec &v,
- int indentation = 0);
- friend ostream &LispPrintVecSpecial(ostream &os,
- const vector<const ASTNode*> &v,
- int indentation = 0);
-
- 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);
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,unsigned char> _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<ASTInterior, ...>" 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<string> h;
-#else
- hash<char*> 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.
--- /dev/null
+// -*- 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
--- /dev/null
+// -*- 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
--- /dev/null
+// -*- 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,unsigned char> _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
--- /dev/null
+// -*- 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<ASTNode>;
+
+ 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<const ASTNode*> &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
--- /dev/null
+// -*- 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<string> h;
+#else
+ hash<char*> 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
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
.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) > $@
--- /dev/null
+// -*- 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 <vector>
+#ifdef EXT_HASH_MAP
+#include <ext/hash_set>
+#include <ext/hash_map>
+#elif defined(TR1_UNORDERED_MAP)
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
+#define hash_map tr1::unordered_map
+#define hash_set tr1::unordered_set
+#define hash_multiset tr1::unordered_multiset
+#else
+#include <hash_set>
+#include <hash_map>
+#endif
+#include <iostream>
+#include <sstream>
+#include <string>
+#include <map>
+#include <set>
+#include <algorithm>
+#include "../main/Globals.h"
+#include "ASTUtil.h"
+#include "ASTKind.h"
+#include <stdint.h>
+#include <stdlib.h>
+#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 <class E, class T>
+ struct enumeration
+ {
+ typedef T type;
+ typedef E enum_type;
+
+ enumeration() : e_(E())
+ {}
+
+ enumeration(E e) : e_(static_cast<T>(e))
+ {}
+
+ operator E() const
+ { return static_cast<E>(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<ASTNode> ASTVec;
+ typedef unsigned int * CBV;
+#define HASHMAP hash_map;
+#define HASHSET hash_set;
+ extern ASTVec _empty_ASTVec;
+
+}; //end of namespace
+
+#endif
#include <iostream>
#include <sstream>
#include "AST.h"
-#include "printer/printers.h"
+//#include "../printer/printers.h"
namespace BEEV
{
#include <assert.h>
#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)
LIBS = -L../to-sat -ltosat \
-L../AST -last \
+ -L../printer -lprinter \
-L../abstraction-refinement -labstractionrefinement \
-L../sat -lminisat \
-L../simplifier -lsimplifier \
********************************************************************/
// -*- 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;
********************************************************************/
// -*- 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
#ifndef PRINTER_H
#define PRINTER_H
-#include "../AST.h"
-
+#include "../AST/AST.h"
namespace BEEV
{
using namespace std;
#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
{
projects / francis / stp.git / commitdiff