Forgot to remove the actual stp directory.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161056 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 0 insertions, 1806 deletions

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