--- /dev/null
+1. We try to follow the GNU coding guidelines and indentation
+standards. Please visit the following website to learn more:
+
+http://www.gnu.org/prep/standards/standards.html
+
+2. The code is automatically formatted with the indent tool before
+check-in.
#OPTIMIZE = -g -pg # Debugging and gprof-style profiling
OPTIMIZE = -g # Debugging
OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
+#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE
CFLAGS_BASE = $(OPTIMIZE)
void ASTInterior::CleanUp()
{
// cout << "Deleting node " << this->GetNodeNum() << endl;
- _bm._interior_unique_table.erase(this);
+ GlobalBeevMgr->_interior_unique_table.erase(this);
delete this;
}
//ASTNode constructors are inlined in AST.h
bool ASTNode::IsAlreadyPrinted() const
{
- BeevMgr &bm = GetBeevMgr();
- return (bm.AlreadyPrintedSet.find(*this) != bm.AlreadyPrintedSet.end());
+ BeevMgr * bm = GetBeevMgr();
+ return (bm->AlreadyPrintedSet.find(*this) != bm->AlreadyPrintedSet.end());
}
void ASTNode::nodeprint(ostream& os, bool c_friendly) const
void ASTNode::MarkAlreadyPrinted() const
{
- BeevMgr &bm = GetBeevMgr();
- bm.AlreadyPrintedSet.insert(*this);
+ BeevMgr * bm = GetBeevMgr();
+ bm->AlreadyPrintedSet.insert(*this);
}
// Get the name from a symbol (char *). It's an error if kind != SYMBOL
return;
//FIXME: this is ugly.
- BeevMgr& bm = GetBeevMgr();
+ 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 (bm->PLPrintNodeSet.find(ccc) == bm->PLPrintNodeSet.end())
{
//If branch: if *it is not in NodeSet then,
//
//
//2. Letize its childNodes
- bm.PLPrintNodeSet.insert(ccc);
+ bm->PLPrintNodeSet.insert(ccc);
//debugging
//cerr << ccc;
ccc.LetizeNode();
//
//2. if no, then create a new var and add it to the
//2. NodeLetVarMap
- if (bm.NodeLetVarMap.find(ccc) == bm.NodeLetVarMap.end())
+ 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();
+ int sz = bm->NodeLetVarMap.size();
ostringstream oss;
oss << "let_k_" << sz;
- ASTNode CurrentSymbol = bm.CreateSymbol(oss.str().c_str());
+ 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
* check for this. [Vijay is the author of this comment.]
*/
- bm.NodeLetVarMap[ccc] = CurrentSymbol;
+ bm->NodeLetVarMap[ccc] = CurrentSymbol;
std::pair<ASTNode, ASTNode> node_letvar_pair(CurrentSymbol, ccc);
- bm.NodeLetVarVec.push_back(node_letvar_pair);
+ bm->NodeLetVarVec.push_back(node_letvar_pair);
}
}
}
ASTNode BeevMgr::CreateNode(Kind kind, const ASTVec & back_children)
{
// create a new node. Children will be modified.
- ASTInterior *n_ptr = new ASTInterior(kind, *this);
+ ASTInterior *n_ptr = new ASTInterior(kind);
// insert all of children at end of new_children.
ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTVec & back_children)
{
- ASTInterior *n_ptr = new ASTInterior(kind, *this);
+ ASTInterior *n_ptr = new ASTInterior(kind);
ASTVec &front_children = n_ptr->_children;
front_children.push_back(child0);
ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTVec & back_children)
{
- ASTInterior *n_ptr = new ASTInterior(kind, *this);
+ ASTInterior *n_ptr = new ASTInterior(kind);
ASTVec &front_children = n_ptr->_children;
front_children.push_back(child0);
front_children.push_back(child1);
ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2, const ASTVec & back_children)
{
- ASTInterior *n_ptr = new ASTInterior(kind, *this);
+ ASTInterior *n_ptr = new ASTInterior(kind);
ASTVec &front_children = n_ptr->_children;
front_children.push_back(child0);
front_children.push_back(child1);
////////////////////////////////////////////////////////////////
ASTNode BeevMgr::CreateSymbol(const char * const name)
{
- ASTSymbol temp_sym(name, *this);
+ ASTSymbol temp_sym(name);
ASTNode n(LookupOrCreateSymbol(temp_sym));
return n;
}
//FIXME Code currently assumes that it will destroy the bitvector passed to it
ASTNode BeevMgr::CreateBVConst(CBV bv, unsigned width)
{
- ASTBVConst temp_bvconst(bv, width, *this);
+ ASTBVConst temp_bvconst(bv, width);
ASTNode n(LookupOrCreateBVConst(temp_bvconst));
CONSTANTBV::BitVector_Destroy(bv);
void ASTBVConst::CleanUp()
{
// cout << "Deleting node " << this->GetNodeNum() << endl;
- _bm._bvconst_unique_table.erase(this);
+ GlobalBeevMgr->_bvconst_unique_table.erase(this);
delete this;
}
// _name because it's const). Can cast the iterator to
// non-const -- carefully.
//std::string strname(s_ptr->GetName());
- ASTSymbol * s_ptr1 = new ASTSymbol(strdup(s_ptr->GetName()), *this);
+ ASTSymbol * s_ptr1 = new ASTSymbol(strdup(s_ptr->GetName()));
s_ptr1->SetNodeNum(NewNodeNum());
s_ptr1->_value_width = s_ptr->_value_width;
pair<ASTSymbolSet::const_iterator, bool> p = _symbol_unique_table.insert(s_ptr1);
void ASTSymbol::CleanUp()
{
// cout << "Deleting node " << this->GetNodeNum() << endl;
- _bm._symbol_unique_table.erase(this);
+ GlobalBeevMgr->_symbol_unique_table.erase(this);
//FIXME This is a HUGE free to invoke.
//TEST IT!
free((char*) this->_name);
// Assignment (for ref counting)
ASTNode& operator=(const ASTNode& n);
- BeevMgr &GetBeevMgr() const;
+ BeevMgr* GetBeevMgr() const;
// Access node number
int GetNodeNum() const;
friend class CNFMgr;
protected:
-
// reference count.
- int _ref_count;
+ //#ifdef LESSBYTES_PERNODE
+ //unsigned short _ref_count;
+ //#else
+ unsigned int _ref_count;
+ //#endif
// Kind. It's a type tag and the operator.
- //Kind _kind;
enumeration<Kind,unsigned char> _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;
+ 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.
- unsigned short _index_width;
+#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.
- unsigned short _value_width;
+#ifdef LESSBYTES_PERNODE
+ unsigned char _value_width;
+#else
+ unsigned int _value_width;
+#endif
// Increment refcount.
void IncRef()
;
// Constructor (bm only)
- ASTInternal(BeevMgr &bm, int nodenum = 0) :
- _ref_count(0), _kind(UNDEFINED), _bm(bm),
+ 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, BeevMgr &bm, int nodenum = 0) :
- _ref_count(0), _kind(kind), _bm(bm),
+ 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, BeevMgr &bm, int nodenum = 0) :
+ ASTInternal(Kind kind, const ASTVec &children, int nodenum = 0) :
_ref_count(0), _kind(kind), _children(children),
- _bm(bm), _node_num(nodenum), _index_width(0), _value_width(0)
+ _node_num(nodenum), _index_width(0), _value_width(0)
{
}
// 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),
+ _children(int_node._children),
_node_num(int_node._node_num), _index_width(int_node._index_width),
_value_width(int_node._value_width)
{
// to put "friend class hash_set<ASTInterior, ...>" in here.
// Basic constructors
- ASTInterior(Kind kind, BeevMgr &bm) :
- ASTInternal(kind, bm)
+ ASTInterior(Kind kind) :
+ ASTInternal(kind)
{
}
- ASTInterior(Kind kind, ASTVec &children, BeevMgr &bm) :
- ASTInternal(kind, children, bm)
+ ASTInterior(Kind kind, ASTVec &children) :
+ ASTInternal(kind, children)
{
}
public:
// Default constructor
- ASTSymbol(BeevMgr &bm) :
- ASTInternal(bm), _name(NULL)
+ ASTSymbol() :
+ ASTInternal(), _name(NULL)
{
}
// Constructor. This does NOT copy its argument.
- ASTSymbol(const char * const name, BeevMgr &bm) :
- ASTInternal(SYMBOL, bm), _name(name)
+ ASTSymbol(const char * const name) :
+ ASTInternal(SYMBOL), _name(name)
{
}
// 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)
+ ASTInternal(sym._kind, sym._children), _name(sym._name)
{
}
}; //End of ASTSymbol
};
//FIXME Keep an eye on this function
- ASTBVConst(CBV bv, unsigned int width, BeevMgr &bm) :
- ASTInternal(BVCONST, bm)
+ ASTBVConst(CBV bv, unsigned int width) :
+ ASTInternal(BVCONST)
{
_bvconst = CONSTANTBV::BitVector_Clone(bv);
_value_width = width;
// Copy constructor.
ASTBVConst(const ASTBVConst &sym) :
- ASTInternal(sym._kind, sym._children, sym._bm)
+ ASTInternal(sym._kind, sym._children)
{
_bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst);
_value_width = sym._value_width;
}
}
- inline BeevMgr& ASTNode::GetBeevMgr() const
+ inline BeevMgr* ASTNode::GetBeevMgr() const
{
- return _int_node_ptr->_bm;
+ return GlobalBeevMgr;
}
//Return the unsigned constant value of the input 'n'
//Translates signed BVDIV,BVMOD and BVREM into unsigned variety
ASTNode TranslateSignedDivModRem(const ASTNode& in)
{
- BeevMgr& bm = in.GetBeevMgr();
+ BeevMgr* bm = GlobalBeevMgr;
assert(in.GetChildren().size() ==2);
ASTNode dividend = in[0];
ASTNode divisor = in[1];
unsigned len = in.GetValueWidth();
- ASTNode hi1 = bm.CreateBVConst(32, len - 1);
- ASTNode one = bm.CreateOneConst(1);
- ASTNode zero = bm.CreateZeroConst(1);
+ ASTNode hi1 = bm->CreateBVConst(32, len - 1);
+ ASTNode one = bm->CreateOneConst(1);
+ ASTNode zero = bm->CreateZeroConst(1);
// create the condition for the dividend
- ASTNode cond_dividend = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1));
+ ASTNode cond_dividend = bm->CreateNode(EQ, one, bm->CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1));
// create the condition for the divisor
- ASTNode cond_divisor = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1));
+ ASTNode cond_divisor = bm->CreateNode(EQ, one, bm->CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1));
if (SBVREM == in.GetKind())
{
//BVMOD is an expensive operation. So have the fewest bvmods possible. Just one.
//Take absolute value.
- ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend);
- ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor);
+ ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend);
+ ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor);
//create the modulus term
- ASTNode modnode = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
+ ASTNode modnode = bm->CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
//If the dividend is <0 take the unary minus.
- ASTNode n = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, modnode), modnode);
+ ASTNode n = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, modnode), modnode);
//put everything together, simplify, and return
- return bm.SimplifyTerm_TopLevel(n);
+ return bm->SimplifyTerm_TopLevel(n);
}
// This is the modulus of dividing rounding to -infinity.
// (bvneg (bvurem (bvneg s) (bvneg t)))))))
//Take absolute value.
- ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend);
- ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor);
+ ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend);
+ ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor);
- ASTNode urem_node = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
+ ASTNode urem_node = bm->CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
// If the dividend is <0, then we negate the whole thing.
- ASTNode rev_node = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, urem_node), urem_node);
+ ASTNode rev_node = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, urem_node), urem_node);
// if It's XOR <0 then add t (not its absolute value).
- ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor);
- ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVPLUS, len, rev_node, divisor), rev_node);
+ ASTNode xor_node = bm->CreateNode(XOR, cond_dividend, cond_divisor);
+ ASTNode n = bm->CreateTerm(ITE, len, xor_node, bm->CreateTerm(BVPLUS, len, rev_node, divisor), rev_node);
- return bm.SimplifyTerm_TopLevel(n);
+ return bm->SimplifyTerm_TopLevel(n);
}
else if (SBVDIV == in.GetKind())
{
//else simply output BVDIV(dividend,divisor)
//Take absolute value.
- ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend);
- ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor);
+ ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend);
+ ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor);
- ASTNode divnode = bm.CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
+ ASTNode divnode = bm->CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
// A little confusing. Only negate the result if they are XOR <0.
- ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor);
- ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVUMINUS, len, divnode), divnode);
+ ASTNode xor_node = bm->CreateNode(XOR, cond_dividend, cond_divisor);
+ ASTNode n = bm->CreateTerm(ITE, len, xor_node, bm->CreateTerm(BVUMINUS, len, divnode), divnode);
- return bm.SimplifyTerm_TopLevel(n);
+ return bm->SimplifyTerm_TopLevel(n);
}
FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in);
- return bm.CreateNode(UNDEFINED);
+ return bm->CreateNode(UNDEFINED);
}//end of TranslateSignedDivModRem()
********************************************************/
ASTNode TransformFormula(const ASTNode& form)
{
- BeevMgr& bm = form.GetBeevMgr();
+ BeevMgr* bm = form.GetBeevMgr();
assert(TransformMap != NULL);
{
ASTVec c;
c.push_back(TransformFormula(simpleForm[0]));
- result = bm.CreateNode(NOT, c);
+ result = bm->CreateNode(NOT, c);
break;
}
case BVLT:
ASTVec c;
c.push_back(TransformTerm(simpleForm[0]));
c.push_back(TransformTerm(simpleForm[1]));
- result = bm.CreateNode(k, c);
+ result = bm->CreateNode(k, c);
break;
}
case EQ:
{
ASTNode term1 = TransformTerm(simpleForm[0]);
ASTNode term2 = TransformTerm(simpleForm[1]);
- result = bm.CreateSimplifiedEQ(term1, term2);
+ result = bm->CreateSimplifiedEQ(term1, term2);
break;
}
case AND:
vec.push_back(o);
}
- result = bm.CreateNode(k, vec);
+ result = bm->CreateNode(k, vec);
break;
}
case FOR:
{
//Insert in a global list of FOR constructs. Return TRUE now
- bm.GlobalList_Of_FiniteLoops.push_back(simpleForm);
- return bm.CreateNode(TRUE);
+ bm->GlobalList_Of_FiniteLoops.push_back(simpleForm);
+ return bm->CreateNode(TRUE);
break;
}
case PARAMBOOL:
//VAR(expression), then simply return it
if(BVCONST == simpleForm[1].GetKind())
{
- result = bm.NewBooleanVar(simpleForm[0],simpleForm[1]);
+ result = bm->NewBooleanVar(simpleForm[0],simpleForm[1]);
}
else
{
result = simpleForm;
else
{
- FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k);
+ FatalError("TransformFormula: Illegal kind: ", bm->CreateNode(UNDEFINED), k);
cerr << "The input is: " << simpleForm << endl;
cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl;
}
{
assert(TransformMap != NULL);
- BeevMgr& bm = inputterm.GetBeevMgr();
+ BeevMgr* bm = inputterm.GetBeevMgr();
ASTNode result;
ASTNode term = inputterm;
FatalError("TransformTerm: this kind is not supported", term);
break;
case READ:
- result = bm.TransformArray(term);
+ result = bm->TransformArray(term);
break;
case ITE:
{
thn = TransformTerm(thn);
els = TransformTerm(els);
//result = CreateTerm(ITE,term.GetValueWidth(),cond,thn,els);
- result = bm.CreateSimplifiedTermITE(cond, thn, els);
+ result = bm->CreateSimplifiedTermITE(cond, thn, els);
result.SetIndexWidth(term.GetIndexWidth());
break;
}
o.push_back(TransformTerm(*it));
}
- result = bm.CreateTerm(k, width, o);
+ result = bm->CreateTerm(k, width, o);
result.SetIndexWidth(indexwidth);
Kind k = result.GetKind();
// result is embedded unchanged inside the result.
unsigned inputValueWidth = result.GetValueWidth();
- ASTNode zero = bm.CreateZeroConst(inputValueWidth);
- ASTNode one = bm.CreateOneConst(inputValueWidth);
- result = bm.CreateTerm(ITE, inputValueWidth, bm.CreateNode(EQ, zero, bottom), one, result);
+ ASTNode zero = bm->CreateZeroConst(inputValueWidth);
+ ASTNode one = bm->CreateOneConst(inputValueWidth);
+ result = bm->CreateTerm(ITE, inputValueWidth, bm->CreateNode(EQ, zero, bottom), one, result);
}
}
}
void lpvec(const ASTVec &vec)
{
- vec[0].GetBeevMgr().AlreadyPrintedSet.clear();
+ (vec[0].GetBeevMgr())->AlreadyPrintedSet.clear();
LispPrintVec(cout, vec, 0);
cout << endl;
}
}
//if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = n.GetBeevMgr();
+ BeevMgr *bm = n.GetBeevMgr();
//this is to print letvars for shared subterms inside the printing
//of "(LET v0 = term1, v1=term1@term2,...
- if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
+ if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize)
{
- C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ C_Print1(os, (bm->NodeLetVarMap1[n]), indentation, letize);
return;
}
//this is to print letvars for shared subterms inside the actual
//term to be printed
- if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
+ if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize)
{
- C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ C_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize);
return;
}
ostream& C_Print(ostream &os, const ASTNode n, int indentation)
{
// Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
+ BeevMgr* bm = n.GetBeevMgr();
+ bm->PLPrintNodeSet.clear();
+ bm->NodeLetVarMap.clear();
+ bm->NodeLetVarVec.clear();
+ bm->NodeLetVarMap1.clear();
//pass 1: letize the node
n.LetizeNode();
//3. Then print the Node itself, replacing every occurence of
//3. expr1 with var1, expr2 with var2, ...
//os << "(";
- if (0 < bm.NodeLetVarMap.size())
+ if (0 < bm->NodeLetVarMap.size())
{
- //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
- //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
- std::vector<pair<ASTNode, ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
- std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
+ //ASTNodeMap::iterator it=bm->NodeLetVarMap.begin();
+ //ASTNodeMap::iterator itend=bm->NodeLetVarMap.end();
+ std::vector<pair<ASTNode, ASTNode> >::iterator it = bm->NodeLetVarVec.begin();
+ std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm->NodeLetVarVec.end();
// start a new block to create new static scope
os << "{" << endl;
}
//update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
+ bm->NodeLetVarMap1[it->second] = it->first;
}
os << endl << "stp_assert ";
ostream &Lisp_Print(ostream &os, const ASTNode& n, int indentation)
{
// Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.AlreadyPrintedSet.clear();
+ BeevMgr* bm = n.GetBeevMgr();
+ bm->AlreadyPrintedSet.clear();
Lisp_Print_indent(os, n, indentation);
printf("\n");
return os;
}
//if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = n.GetBeevMgr();
+ BeevMgr *bm = n.GetBeevMgr();
//this is to print letvars for shared subterms inside the printing
//of "(LET v0 = term1, v1=term1@term2,...
- if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
+ if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize)
{
- PL_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ PL_Print1(os, (bm->NodeLetVarMap1[n]), indentation, letize);
return;
}
//this is to print letvars for shared subterms inside the actual
//term to be printed
- if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
+ if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize)
{
- PL_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ PL_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize);
return;
}
case FOR:
if(expand_finitefor_flag)
{
- ASTNode expandedfor = bm.Expand_FiniteLoop_TopLevel(n);
+ ASTNode expandedfor = bm->Expand_FiniteLoop_TopLevel(n);
PL_Print1(os, expandedfor, indentation, letize);
}
else
ostream& PL_Print(ostream &os, const ASTNode& n, int indentation)
{
// Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
+ BeevMgr* bm = n.GetBeevMgr();
+ bm->PLPrintNodeSet.clear();
+ bm->NodeLetVarMap.clear();
+ bm->NodeLetVarVec.clear();
+ bm->NodeLetVarMap1.clear();
//pass 1: letize the node
n.LetizeNode();
//3. Then print the Node itself, replacing every occurence of
//3. expr1 with var1, expr2 with var2, ...
//os << "(";
- if (0 < bm.NodeLetVarMap.size())
+ if (0 < bm->NodeLetVarMap.size())
{
- //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
- //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
- std::vector<pair<ASTNode, ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
- std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
+ //ASTNodeMap::iterator it=bm->NodeLetVarMap.begin();
+ //ASTNodeMap::iterator itend=bm->NodeLetVarMap.end();
+ std::vector<pair<ASTNode, ASTNode> >::iterator it = bm->NodeLetVarVec.begin();
+ std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm->NodeLetVarVec.end();
os << "(LET ";
//print the let var first
PL_Print1(os, it->second, indentation, false);
//update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
+ bm->NodeLetVarMap1[it->second] = it->first;
for (it++; it != itend; it++)
{
PL_Print1(os, it->second, indentation, false);
//update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
+ bm->NodeLetVarMap1[it->second] = it->first;
}
os << " IN " << endl;
string functionToSMTLIBName(const BEEV::Kind k);
void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
- void printVarDeclsToStream( const BeevMgr& mgr, ostream &os);
+ void printVarDeclsToStream( const BeevMgr* mgr, ostream &os);
// Initial version intended to print the whole thing back.
void SMTLIB_PrintBack(ostream &os, const ASTNode& n) {
os << ")" << endl;
}
- void printVarDeclsToStream( const BeevMgr& mgr, ostream &os) {
- for(ASTVec::const_iterator i = mgr.ListOfDeclaredVars.begin(),iend=mgr.ListOfDeclaredVars.end();i!=iend;i++) {
+ void printVarDeclsToStream( const BeevMgr* mgr, ostream &os) {
+ for(ASTVec::const_iterator i = mgr->ListOfDeclaredVars.begin(),iend=mgr->ListOfDeclaredVars.end();i!=iend;i++) {
const BEEV::ASTNode& a = *i;
// Should be a symbol.
// Prepend with zero to convert to unsigned.
os << "bv";
- CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst());
+ CBV unsign = CONSTANTBV::BitVector_Concat((n.GetBeevMgr())->CreateZeroConst(1).GetBVConst(), op.GetBVConst());
unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign);
CONSTANTBV::BitVector_Destroy(unsign);
os << str << "[" << op.GetValueWidth() << "]";
}
//if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = n.GetBeevMgr();
+ BeevMgr * bm = n.GetBeevMgr();
//this is to print letvars for shared subterms inside the printing
//of "(LET v0 = term1, v1=term1@term2,...
- if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
+ if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize)
{
- SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ SMTLIB_Print1(os, (bm->NodeLetVarMap1[n]), indentation, letize);
return;
}
//this is to print letvars for shared subterms inside the actual
//term to be printed
- if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
+ if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize)
{
- SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ SMTLIB_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize);
return;
}
ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation)
{
// Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
+ BeevMgr* bm = n.GetBeevMgr();
+ bm->PLPrintNodeSet.clear();
+ bm->NodeLetVarMap.clear();
+ bm->NodeLetVarVec.clear();
+ bm->NodeLetVarMap1.clear();
//pass 1: letize the node
n.LetizeNode();
//3. Then print the Node itself, replacing every occurence of
//3. expr1 with var1, expr2 with var2, ...
//os << "(";
- if (0 < bm.NodeLetVarMap.size())
+ if (0 < bm->NodeLetVarMap.size())
{
- //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
- //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
- std::vector<pair<ASTNode, ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
- std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
+ //ASTNodeMap::iterator it=bm->NodeLetVarMap.begin();
+ //ASTNodeMap::iterator itend=bm->NodeLetVarMap.end();
+ std::vector<pair<ASTNode, ASTNode> >::iterator it = bm->NodeLetVarVec.begin();
+ std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm->NodeLetVarVec.end();
os << "(LET ";
//print the let var first
SMTLIB_Print1(os, it->second, indentation, false);
//update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
+ bm->NodeLetVarMap1[it->second] = it->first;
for (it++; it != itend; it++)
{
SMTLIB_Print1(os, it->second, indentation, false);
//update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
+ bm->NodeLetVarMap1[it->second] = it->first;
}
os << " IN " << endl;
return 0;
}
bmstar bm = new BEEV::BeevMgr();
+ BEEV::GlobalBeevMgr = bm;
decls = new BEEV::ASTVec();
//created_exprs.clear();
return (VC)bm;
// prints Expr 'e' to stdout as C code
void vc_printExprCCode(VC vc, Expr e) {
BEEV::ASTNode q = (*(nodestar)e);
+ bmstar b = (bmstar)vc;
// print variable declarations
- BEEV::ASTVec declsFromParser = (nodelist)BEEV::GlobalBeevMgr->ListOfDeclaredVars;
+ BEEV::ASTVec declsFromParser = (nodelist)b->ListOfDeclaredVars;
for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) {
if(BEEV::BITVECTOR_TYPE == it->GetType()) {
}
#endif
-// Expr vc_parseExpr(VC vc, char* infile) {
-// bmstar b = (bmstar)vc;
-// extern FILE* cvcin;
-// const char * prog = "stp";
-
-// cvcin = fopen(infile,"r");
-// if(cvcin == NULL) {
-// fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
-// BEEV::FatalError("");
-// }
-
-// BEEV::GlobalBeevMgr = b;
-
-// CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
-// if(0 != c) {
-// cout << CONSTANTBV::BitVector_Error(c) << endl;
-// return 0;
-// }
-
-// cvcparse();
-// nodelist aaa = b->GetAsserts();
-
-// //Don't add the query. It gets added automatically if the input file
-// //has QUERY in it
-// //
-// //node bbb = b->CreateNode(BEEV::NOT,b->GetQuery());
-// node o = b->CreateNode(BEEV::AND,aaa);
-// //node o = b->CreateNode(BEEV::AND,oo,bbb);
-
-// nodestar output = new node(o);
-// return output;
-// } //end of vc_parseExpr()
-
-
Expr vc_parseExpr(VC vc, const char* infile) {
bmstar b = (bmstar)vc;
extern FILE* cvcin;
while (true)
{
ASTNode& nold = n;
- n = a.GetBeevMgr().FlattenOneLevel(n);
+ n = a.GetBeevMgr()->FlattenOneLevel(n);
if ((n == nold))
break;
}
// ASSERT: IndexWidth = 0? Semantic analysis should check.
//Leaking ASTVec& bbvec = *(new ASTVec);
- //FIXME Why is isn't this ASTVEC bbvec(num_bits) ?
ASTVec bbvec;
- /*
- if(term.GetNodeNum() == 17132){
- weregood = true;
- }
- */
-
- /*
- if(weregood){
- printf("number of bits for node 17132: %d\n", num_bits);
- }
- */
for (unsigned int i = 0; i < num_bits; i++)
{
ASTNode bit_node = CreateNode(BVGETBIT, term, CreateBVConst(32, i));
bbvec.push_back(bit_node);
}
result = CreateNode(BOOLVEC, bbvec);
- /*
- if(weregood){
- printf("done\n");
- }
- */
break;
}
case BVCONST:
BeevMgr::ClauseList* convertToCNF(const ASTNode& varphi)
{
- varphi.GetBeevMgr().runTimes.start(RunTimes::CNFConversion);
+ varphi.GetBeevMgr()->runTimes.start(RunTimes::CNFConversion);
scanFormula(varphi, true);
ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
BeevMgr::ClauseList* defs = SINGLETON(dummy_true_var);
defs->insert(defs->begin() + 1, top->begin(), top->end());
cleanup(varphi);
- varphi.GetBeevMgr().runTimes.stop(RunTimes::CNFConversion);
+ varphi.GetBeevMgr()->runTimes.stop(RunTimes::CNFConversion);
return defs;
}
projects / francis / stp.git / commitdiff