+// -*- c++ -*-
/********************************************************************
* AUTHORS: Vijay Ganesh
*
*
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
-// -*- c++ -*-
#include "AST.h"
-#include <assert.h>
-//#include "../printer/printers.h"
-//#include "../printer/AssortedPrinters.h"
-
namespace BEEV
{
- ////////////////////////////////////////////////////////////////
- // ASTInternal members
- ////////////////////////////////////////////////////////////////
- /** Trivial but virtual destructor */
- ASTInternal::~ASTInternal()
- {
- }
-
- ////////////////////////////////////////////////////////////////
- // ASTInterior members
- ////////////////////////////////////////////////////////////////
- /** Copy constructor */
- // ASTInterior::ASTInterior(const ASTInterior &int_node)
- // {
- // _kind = int_node._kind;
- // _children = int_node._children;
- // }
-
- /** Trivial but virtual destructor */
- ASTInterior::~ASTInterior()
- {
- }
-
// FIXME: Darn it! I think this ends up copying the children twice!
/** Either return an old node or create it if it doesn't exist.
Note that nodes are physically allocated in the hash table. */
return *it;
}
- size_t ASTInterior::ASTInteriorHasher::operator()(const ASTInterior *int_node_ptr) const
- {
- //size_t hashval = 0;
- size_t hashval = ((size_t) int_node_ptr->GetKind());
- const ASTVec &ch = int_node_ptr->GetChildren();
- ASTVec::const_iterator iend = ch.end();
- for (ASTVec::const_iterator i = ch.begin(); i != iend; i++)
- {
- //Using "One at a time hash" by Bob Jenkins
- hashval += i->Hash();
- hashval += (hashval << 10);
- hashval ^= (hashval >> 6);
- }
-
- hashval += (hashval << 3);
- hashval ^= (hashval >> 11);
- hashval += (hashval << 15);
- return hashval;
- //return hashval += ((size_t) int_node_ptr->GetKind());
- }
-
- void ASTInterior::CleanUp()
- {
- // cout << "Deleting node " << this->GetNodeNum() << endl;
- GlobalBeevMgr->_interior_unique_table.erase(this);
- delete this;
- }
-
- ////////////////////////////////////////////////////////////////
- // ASTNode members
- ////////////////////////////////////////////////////////////////
- //ASTNode constructors are inlined in AST.h
- bool ASTNode::IsAlreadyPrinted() const
- {
- BeevMgr * bm = GetBeevMgr();
- return (bm->AlreadyPrintedSet.find(*this) != bm->AlreadyPrintedSet.end());
- }
-
- void ASTNode::nodeprint(ostream& os, bool c_friendly) const
- {
- _int_node_ptr->nodeprint(os, c_friendly);
- }
-
- void ASTNode::MarkAlreadyPrinted() const
- {
- BeevMgr * bm = GetBeevMgr();
- bm->AlreadyPrintedSet.insert(*this);
- }
-
- // Get the name from a symbol (char *). It's an error if kind != SYMBOL
- const char * /**const**/ ASTNode::GetName() const
- {
- if (GetKind() != SYMBOL)
- FatalError("GetName: Called GetName on a non-symbol: ", *this);
- return ((ASTSymbol *) _int_node_ptr)->GetName();
- }
-
- void ASTNode::NFASTPrint(int l, int max, int prefix) const
- {
- //****************************************
- // stop
- //****************************************
- if (l > max)
- {
- return;
- }
-
- //****************************************
- // print
- //****************************************
- printf("[%10d]", 0);
- for (int i = 0; i < prefix; i++)
- {
- printf(" ");
- }
- cout << GetKind();
- printf("\n");
-
- //****************************************
- // recurse
- //****************************************
-
- const ASTVec &children = GetChildren();
- ASTVec::const_iterator it = children.begin();
- for (; it != children.end(); it++)
- {
- it->NFASTPrint(l + 1, max, prefix + 1);
- }
- }
-
-
-
- //traverse "*this", and construct "let variables" for terms that
- //occur more than once in "*this".
- void ASTNode::LetizeNode(void) const
- {
- Kind kind = this->GetKind();
-
- if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE)
- return;
-
- //FIXME: this is ugly.
- BeevMgr * bm = GetBeevMgr();
- const ASTVec &c = this->GetChildren();
- for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- ASTNode ccc = *it;
- if (bm->PLPrintNodeSet.find(ccc) == bm->PLPrintNodeSet.end())
- {
- //If branch: if *it is not in NodeSet then,
- //
- //1. add it to NodeSet
- //
- //2. Letize its childNodes
-
- bm->PLPrintNodeSet.insert(ccc);
- //debugging
- //cerr << ccc;
- ccc.LetizeNode();
- }
- else
- {
- Kind k = ccc.GetKind();
- if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE)
- continue;
-
- //0. Else branch: Node has been seen before
- //
- //1. Check if the node has a corresponding letvar in the
- //1. NodeLetVarMap.
- //
- //2. if no, then create a new var and add it to the
- //2. NodeLetVarMap
- if (bm->NodeLetVarMap.find(ccc) == bm->NodeLetVarMap.end())
- {
- //Create a new symbol. Get some name. if it conflicts with a
- //declared name, too bad.
- int sz = bm->NodeLetVarMap.size();
- ostringstream oss;
- oss << "let_k_" << sz;
-
- ASTNode CurrentSymbol = bm->CreateSymbol(oss.str().c_str());
- CurrentSymbol.SetValueWidth(this->GetValueWidth());
- CurrentSymbol.SetIndexWidth(this->GetIndexWidth());
- /* If for some reason the variable being created here is
- * already declared by the user then the printed output will
- * not be a legal input to the system. too bad. I refuse to
- * check for this. [Vijay is the author of this comment.]
- */
-
- bm->NodeLetVarMap[ccc] = CurrentSymbol;
- std::pair<ASTNode, ASTNode> node_letvar_pair(CurrentSymbol, ccc);
- bm->NodeLetVarVec.push_back(node_letvar_pair);
- }
- }
- }
- } //end of LetizeNode()
-
-
-
+
+
////////////////////////////////////////////////////////////////
// BeevMgr members
////////////////////////////////////////////////////////////////
return LookupOrCreateInterior(n_ptr);
}
- /** Trivial but virtual destructor */
- ASTSymbol::~ASTSymbol()
- {
- }
-
ostream &operator<<(ostream &os, const ASTNodeMap &nmap)
{
ASTNodeMap::const_iterator iend = nmap.end();
}
}
- // Inline because we need to wait until unique_table is defined
- void ASTBVConst::CleanUp()
- {
- // cout << "Deleting node " << this->GetNodeNum() << endl;
- GlobalBeevMgr->_bvconst_unique_table.erase(this);
- delete this;
- }
-
- // Get the value of bvconst from a bvconst. It's an error if kind != BVCONST
- // Treat the result as const (the compiler can't enforce it).
- CBV /**const**/ ASTNode::GetBVConst() const
- {
- if (GetKind() != BVCONST)
- FatalError("GetBVConst: non bitvector-constant: ", *this);
- return ((ASTBVConst *) _int_node_ptr)->GetBVConst();
- }
-
// FIXME: _name is now a constant field, and this assigns to it
// because it tries not to copy the string unless it needs to. How
// do I avoid copying children in ASTInterior? Perhaps I don't!
return true;
}
- // Inline because we need to wait until unique_table is defined
- void ASTSymbol::CleanUp()
- {
- // cout << "Deleting node " << this->GetNodeNum() << endl;
- GlobalBeevMgr->_symbol_unique_table.erase(this);
- //FIXME This is a HUGE free to invoke.
- //TEST IT!
- free((char*) this->_name);
- delete this;
- }
-
////////////////////////////////////////////////////////////////
//
// IO manipulators for Lisp format printing of AST.
return os;
}
- // Copy constructor. Maintain _ref_count
- ASTNode::ASTNode(const ASTNode &n) :
- _int_node_ptr(n._int_node_ptr)
- {
- if (n._int_node_ptr)
- {
- n._int_node_ptr->IncRef();
- }
- }
-
// If there is a lot of sharing in the graph, this will take a long
// time. it doesn't mark subgraphs as already having been
// typechecked.
--- /dev/null
+// -*- c++ -*-
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+
+#include "AST.h"
+namespace BEEV
+{
+ /****************************************************************
+ * ASTBVConst Member Function definitions *
+ ****************************************************************/
+
+ //Constructor
+ ASTBVConst::ASTBVConst(CBV bv, unsigned int width) :
+ ASTInternal(BVCONST)
+ {
+ _bvconst = CONSTANTBV::BitVector_Clone(bv);
+ _value_width = width;
+ } //End of ASTBVConst constructor
+
+ // Copy constructor.
+ ASTBVConst::ASTBVConst(const ASTBVConst &sym) :
+ ASTInternal(sym._kind, sym._children)
+ {
+ _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst);
+ _value_width = sym._value_width;
+ } //End of copy constructor()
+
+ // Call this when deleting a node that has been stored in the the
+ // unique table
+ void ASTBVConst::CleanUp()
+ {
+ GlobalBeevMgr->_bvconst_unique_table.erase(this);
+ delete this;
+ } //End of Cleanup()
+
+ // Print function for bvconst -- return _bvconst value in bin
+ // format (c_friendly is for printing hex. numbers that C
+ // compilers will accept)
+ void ASTBVConst::nodeprint(ostream& os, bool c_friendly)
+ {
+ 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);
+ } //End of nodeprint()
+
+ // Return the bvconst. It is a const-value
+ CBV ASTBVConst::GetBVConst() const
+ {
+ return _bvconst;
+ } //End of GetBVConst()
+};//End of namespace
+
#define ASTBVCONST_H
namespace BEEV
{
+ class BeevMgr;
void FatalError(const char * str);
/******************************************************************
return CONSTANTBV::BitVector_Hash(bvc->_bvconst);
}
;
- };
+ }; //End of class ASTBVConstHahser
/****************************************************************
* Class ASTBVConstEqual: *
CONSTANTBV::BitVector_Compare(bvc1->_bvconst,
bvc2->_bvconst));
}
- };
+ }; //End of class ASTBVConstEqual
/****************************************************************
* Private Functions (virtual defs and friends) *
****************************************************************/
- ASTBVConst(CBV bv, unsigned int width) :
- ASTInternal(BVCONST)
- {
- _bvconst = CONSTANTBV::BitVector_Clone(bv);
- _value_width = width;
- }
+ //Constructor
+ ASTBVConst(CBV bv, unsigned int width);
+ // Copy constructor.
+ ASTBVConst(const ASTBVConst &sym);
+
+ //friend equality operator
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));
- }
+ } //End of operator==
// Call this when deleting a node that has been stored in the the
// unique table
// 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;
- }
-
+ virtual void nodeprint(ostream& os, bool c_friendly = false);
+
public:
/****************************************************************
virtual ~ASTBVConst()
{
CONSTANTBV::BitVector_Destroy(_bvconst);
- }
+ } //End of destructor
// Return the bvconst. It is a const-value
- CBV GetBVConst() const
- {
- return _bvconst;
- }
+ CBV GetBVConst() const;
}; //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
+ ********************************************************************/
+
+#include "AST.h"
+namespace BEEV
+{
+ /******************************************************************
+ * ASTInterior Member Functions *
+ ******************************************************************/
+
+ // Call this when deleting a node that has been stored in the
+ // the unique table
+ void ASTInterior::CleanUp()
+ {
+ GlobalBeevMgr->_interior_unique_table.erase(this);
+ delete this;
+ } //End of Cleanup()
+
+ // Returns kinds. "lispprinter" handles printing of parenthesis
+ // and childnodes. (c_friendly is for printing hex. numbers that C
+ // compilers will accept)
+ void ASTInterior::nodeprint(ostream& os, bool c_friendly)
+ {
+ os << _kind_names[_kind];
+ } //end of nodeprint()
+
+ /******************************************************************
+ * ASTInteriorHasher and ASTInteriorEqual Member Functions *
+ ******************************************************************/
+
+ //ASTInteriorHasher operator()
+ size_t
+ ASTInterior::ASTInteriorHasher::
+ operator()(const ASTInterior *int_node_ptr) const
+ {
+ size_t hashval = ((size_t) int_node_ptr->GetKind());
+ const ASTVec &ch = int_node_ptr->GetChildren();
+ ASTVec::const_iterator iend = ch.end();
+ for (ASTVec::const_iterator i = ch.begin(); i != iend; i++)
+ {
+ hashval += i->Hash();
+ hashval += (hashval << 10);
+ hashval ^= (hashval >> 6);
+ }
+
+ hashval += (hashval << 3);
+ hashval ^= (hashval >> 11);
+ hashval += (hashval << 15);
+ return hashval;
+ } //End of ASTInteriorHasher operator()
+
+ //ASTInteriorEqual operator()
+ bool
+ ASTInterior::ASTInteriorEqual::
+ operator()(const ASTInterior *int_node_ptr1,
+ const ASTInterior *int_node_ptr2) const
+ {
+ return (*int_node_ptr1 == *int_node_ptr2);
+ } ///End of ASTInteriorEqual operator()
+
+}; //end of namespace
#ifndef ASTINTERIOR_H
#define ASTINTERIOR_H
+
+#include "TopLevel.h"
namespace BEEV
{
+ class ASTNode;
+ class BeevMgr;
+ typedef vector<ASTNode> ASTVec;
+
/******************************************************************
* Class ASTInterior: *
* *
{
public:
size_t operator()(const ASTInterior *int_node_ptr) const;
- };
+ }; //End of ASTInteriorHasher
/******************************************************************
* Class ASTInteriorEqual: *
{
public:
bool operator()(const ASTInterior *int_node_ptr1,
- const ASTInterior *int_node_ptr2) const
- {
- return (*int_node_ptr1 == *int_node_ptr2);
- }
- };
+ const ASTInterior *int_node_ptr2) const;
+ }; //End of class ASTInteriorEqual
// Used in Equality class for hash tables
friend bool operator==(const ASTInterior &int_node1,
{
return ((int_node1._kind == int_node2._kind)
&& (int_node1._children == int_node2._children));
- }
+ } //End of operator==
// Call this when deleting a node that has been stored in the
// the unique table
// 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];
- }
+ virtual void nodeprint(ostream& os, bool c_friendly = false);
+
public:
/******************************************************************
* Public Member Functions *
******************************************************************/
// Basic constructors
- ASTInterior(Kind kind) :
- ASTInternal(kind)
+ ASTInterior(Kind kind) : ASTInternal(kind)
{
}
- ASTInterior(Kind kind, ASTVec &children) :
- ASTInternal(kind, children)
+ 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)
+ ASTInterior(const ASTInterior &int_node) : ASTInternal(int_node)
{
}
// Destructor (does nothing, but is declared virtual here.
- virtual ~ASTInterior();
+ virtual ~ASTInterior()
+ {
+ }
}; //End of ASTNodeInterior
}; //end of namespace BEEV
#endif
virtual void CleanUp() = 0;
// Destructor (does nothing, but is declared virtual here.
- virtual ~ASTInternal();
+ virtual ~ASTInternal()
+ {
+ }
- // Abstract virtual print function for internal node. (c_friendly
- // is for printing hex. numbers that C compilers will accept)
+ // 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 << "*";
--- /dev/null
+// -*- c++ -*-
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+
+#include "AST.h"
+/********************************************************************
+ * This file gives the class definitions of the ASTNode class *
+ ********************************************************************/
+namespace BEEV
+{
+ // Copy constructor. Maintain _ref_count
+ ASTNode::ASTNode(const ASTNode &n) :
+ _int_node_ptr(n._int_node_ptr)
+ {
+ if (n._int_node_ptr)
+ {
+ n._int_node_ptr->IncRef();
+ }
+ } //End of Copy Constructor for ASTNode
+
+ // Checks if the node has alreadybeen printed or not
+ bool ASTNode::IsAlreadyPrinted() const
+ {
+ BeevMgr * bm = GetBeevMgr();
+ return (bm->AlreadyPrintedSet.find(*this) !=
+ bm->AlreadyPrintedSet.end());
+ } //End of IsAlreadyPrinted()
+
+ // Mark the node as printed if it has been already printed
+ void ASTNode::MarkAlreadyPrinted() const
+ {
+ BeevMgr * bm = GetBeevMgr();
+ bm->AlreadyPrintedSet.insert(*this);
+ } //End of MarkAlreadyPrinted()
+
+ // Print the node
+ void ASTNode::nodeprint(ostream& os, bool c_friendly) const
+ {
+ _int_node_ptr->nodeprint(os, c_friendly);
+ } //End of nodeprint()
+
+ // Get the name from a symbol (char *). It's an error if kind !=
+ // SYMBOL
+ const char * ASTNode::GetName() const
+ {
+ if (GetKind() != SYMBOL)
+ FatalError("GetName: Called GetName on a non-symbol: ", *this);
+ return ((ASTSymbol *) _int_node_ptr)->GetName();
+ } //End of GetName()
+
+ // Get the value of bvconst from a bvconst. It's an error if kind
+ // != BVCONST Treat the result as const (the compiler can't enforce
+ // it).
+ CBV ASTNode::GetBVConst() const
+ {
+ if (GetKind() != BVCONST)
+ FatalError("GetBVConst: non bitvector-constant: ", *this);
+ return ((ASTBVConst *) _int_node_ptr)->GetBVConst();
+ } //End of GetBVConst()
+
+ void ASTNode::NFASTPrint(int l, int max, int prefix) const
+ {
+ //****************************************
+ // stop
+ //****************************************
+ if (l > max)
+ {
+ return;
+ }
+
+ //****************************************
+ // print
+ //****************************************
+ printf("[%10d]", 0);
+ for (int i = 0; i < prefix; i++)
+ {
+ printf(" ");
+ }
+ cout << GetKind();
+ printf("\n");
+
+ //****************************************
+ // recurse
+ //****************************************
+
+ const ASTVec &children = GetChildren();
+ ASTVec::const_iterator it = children.begin();
+ for (; it != children.end(); it++)
+ {
+ it->NFASTPrint(l + 1, max, prefix + 1);
+ }
+ } //End of NFASTPrint()
+
+ //traverse "*this", and construct "let variables" for terms that
+ //occur more than once in "*this".
+ void ASTNode::LetizeNode(void) const
+ {
+ Kind kind = this->GetKind();
+
+ if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE)
+ return;
+
+ //FIXME: this is ugly.
+ BeevMgr * bm = GetBeevMgr();
+ const ASTVec &c = this->GetChildren();
+ for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ {
+ ASTNode ccc = *it;
+ if (bm->PLPrintNodeSet.find(ccc) == bm->PLPrintNodeSet.end())
+ {
+ //If branch: if *it is not in NodeSet then,
+ //
+ //1. add it to NodeSet
+ //
+ //2. Letize its childNodes
+
+ bm->PLPrintNodeSet.insert(ccc);
+ //debugging
+ //cerr << ccc;
+ ccc.LetizeNode();
+ }
+ else
+ {
+ Kind k = ccc.GetKind();
+ if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE)
+ continue;
+
+ //0. Else branch: Node has been seen before
+ //
+ //1. Check if the node has a corresponding letvar in the
+ //1. NodeLetVarMap.
+ //
+ //2. if no, then create a new var and add it to the
+ //2. NodeLetVarMap
+ if (bm->NodeLetVarMap.find(ccc) == bm->NodeLetVarMap.end())
+ {
+ //Create a new symbol. Get some name. if it conflicts with a
+ //declared name, too bad.
+ int sz = bm->NodeLetVarMap.size();
+ ostringstream oss;
+ oss << "let_k_" << sz;
+
+ ASTNode CurrentSymbol = bm->CreateSymbol(oss.str().c_str());
+ CurrentSymbol.SetValueWidth(this->GetValueWidth());
+ CurrentSymbol.SetIndexWidth(this->GetIndexWidth());
+ /* If for some reason the variable being created here is
+ * already declared by the user then the printed output will
+ * not be a legal input to the system. too bad. I refuse to
+ * check for this. [Vijay is the author of this comment.]
+ */
+
+ bm->NodeLetVarMap[ccc] = CurrentSymbol;
+ std::pair<ASTNode, ASTNode> node_letvar_pair(CurrentSymbol, ccc);
+ bm->NodeLetVarVec.push_back(node_letvar_pair);
+ }
+ }
+ }
+ } //end of LetizeNode()
+};//end of namespace
--- /dev/null
+// -*- c++ -*-
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+
+#include "AST.h"
+namespace BEEV
+{
+ /****************************************************************
+ * ASTSymbol Member Function definitions *
+ ****************************************************************/
+
+ // Get the name of the symbol
+ const char * ASTSymbol::GetName() const
+ {
+ return _name;
+ }//End of GetName()
+
+ // Print function for symbol -- return name. (c_friendly is for
+ // printing hex. numbers that C compilers will accept)
+ void ASTSymbol::nodeprint(ostream& os, bool c_friendly)
+ {
+ os << _name;
+ } //end of nodeprint()
+
+ // Call this when deleting a node that has been stored in the the
+ // unique table
+ void ASTSymbol::CleanUp()
+ {
+ GlobalBeevMgr->_symbol_unique_table.erase(this);
+ free((char*) this->_name);
+ delete this;
+ }//End of cleanup()
+};//end of namespace
* *
* Class to represent internals of Symbol node. *
******************************************************************/
- class ASTSymbol: public ASTInternal
+ class ASTSymbol : public ASTInternal
{
friend class BeevMgr;
friend class ASTNode;
return h(sym_ptr->_name);
}
;
- };
+ }; // End of class ASTSymbolHasher
/****************************************************************
* Class ASTSymbolEqual: *
{
return (*sym_ptr1 == *sym_ptr2);
}
- };
+ }; //End of class ASTSymbolEqual
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 *
****************************************************************/
+ // Get the name of the symbol
+ const char * GetName() const;
+
// 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;
- }
+ virtual void nodeprint(ostream& os, bool c_friendly = false);
// Call this when deleting a node that has been stored in the the
// unique table
}
// Destructor (does nothing, but is declared virtual here.
- virtual ~ASTSymbol();
+ virtual ~ASTSymbol()
+ {
+ }
// Copy constructor
ASTSymbol(const ASTSymbol &sym) :
#ifndef TOPLEVEL_H
#define TOPLEVEL_H
+#include <stdio.h>
+#include <stdint.h>
+#include <stdlib.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 <assert.h>
+
+#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 "../main/Globals.h"
#include "ASTUtil.h"
#include "ASTKind.h"
-#include <stdint.h>
-#include <stdlib.h>
#include "../extlib-constbv/constantbv.h"
#include "RunTimes.h"
projects / francis / stp.git / commitdiff