diff options
Diffstat (limited to 'stp/AST/AST.cpp')
| -rw-r--r-- | stp/AST/AST.cpp | 1587 |
1 files changed, 1587 insertions, 0 deletions
diff --git a/stp/AST/AST.cpp b/stp/AST/AST.cpp new file mode 100644 index 00000000..ab290395 --- /dev/null +++ b/stp/AST/AST.cpp @@ -0,0 +1,1587 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "AST.h" +namespace BEEV { + //some global variables that are set through commandline options. it + //is best that these variables remain global. Default values set + //here + // + //collect statistics on certain functions + bool stats = false; + //print DAG nodes + bool print_nodes = false; + //tentative global var to allow for variable activity optimization + //in the SAT solver. deprecated. + bool variable_activity_optimize = false; + //run STP in optimized mode + bool optimize = true; + //do sat refinement, i.e. underconstraint the problem, and feed to + //SAT. if this works, great. else, add a set of suitable constraints + //to re-constraint the problem correctly, and call SAT again, until + //all constraints have been added. + bool arrayread_refinement = true; + //flag to control write refinement + bool arraywrite_refinement = true; + //check the counterexample against the original input to STP + bool check_counterexample = false; + //construct the counterexample in terms of original variable based + //on the counterexample returned by SAT solver + bool construct_counterexample = true; + bool print_counterexample = false; + //if this option is true then print the way dawson wants using a + //different printer. do not use this printer. + bool print_arrayval_declaredorder = false; + //flag to decide whether to print "valid/invalid" or not + bool print_output = false; + //do linear search in the array values of an input array. experimental + bool linear_search = false; + //print the variable order chosen by the sat solver while it is + //solving. + bool print_sat_varorder = false; + //turn on word level bitvector solver + bool wordlevel_solve = true; + //turn off XOR flattening + bool xor_flatten = false; + + //the smtlib parser has been turned on + bool smtlib_parser_enable = false; + //print the input back + bool print_STPinput_back = false; + + //global BEEVMGR for the parser + BeevMgr * globalBeevMgr_for_parser; + + void (*vc_error_hdlr)(const char* err_msg) = NULL; + /** This is reusable empty vector, for representing empty children arrays */ + ASTVec _empty_ASTVec; + //////////////////////////////////////////////////////////////// + // 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. */ + + // There is an inelegance here that I don't know how to solve. I'd + // like to heap allocate and do some other initialization on keys only + // if they aren't in the hash table. It would be great if the + // "insert" method took a "creator" class so that I could do that + // between when it notices that the key is not there and when it + // inserts it. Alternatively, it would be great if I could insert the + // temporary key and replace it if it actually got inserted. But STL + // hash_set doesn't have the creator feature and paternalistically + // declares that keys are immutable, even though (it seems to me) that + // they could be mutated if the hash value and eq values did not + // change. + + ASTInterior *BeevMgr::LookupOrCreateInterior(ASTInterior *n_ptr) { + ASTInteriorSet::iterator it; + + if ((it = _interior_unique_table.find(n_ptr)) == _interior_unique_table.end()) { + // Make a new ASTInterior node + // We want (NOT alpha) always to have alpha.nodenum + 1. + if (n_ptr->GetKind() == NOT) { + n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum()+1); + } + else { + n_ptr->SetNodeNum(NewNodeNum()); + } + pair<ASTInteriorSet::const_iterator, bool> p = _interior_unique_table.insert(n_ptr); + return *(p.first); + } + else + // Delete the temporary node, and return the found node. + delete n_ptr; + 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; + _bm._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::MarkAlreadyPrinted() const { + // FIXME: Fetching BeevMgr is annoying. Can we put this in lispprinter class? + 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(); + } + + // Print in lisp format + ostream &ASTNode::LispPrint(ostream &os, int indentation) const { + // Clear the PrintMap + BeevMgr& bm = GetBeevMgr(); + bm.AlreadyPrintedSet.clear(); + return LispPrint_indent(os, indentation); + } + + // Print newline and indentation, then print the thing. + ostream &ASTNode::LispPrint_indent(ostream &os, + int indentation) const + { + os << endl << spaces(indentation); + LispPrint1(os, indentation); + return os; + } + + /** Internal function to print in lisp format. Assume newline + and indentation printed already before first line. Recursive + calls will have newline & indent, though */ + ostream &ASTNode::LispPrint1(ostream &os, int indentation) const { + if (!IsDefined()) { + os << "<undefined>"; + return os; + } + Kind kind = GetKind(); + // FIXME: figure out how to avoid symbols with same names as kinds. +// if (kind == READ) { +// const ASTVec &children = GetChildren(); +// children[0].LispPrint1(os, indentation); +// os << "[" << children[1] << "]"; +// } else + if(kind == BVGETBIT) { + const ASTVec &children = GetChildren(); + // child 0 is a symbol. Print without the NodeNum. + os << GetNodeNum() << ":"; + + + + children[0]._int_node_ptr->nodeprint(os); + //os << "{" << children[1].GetBVConst() << "}"; + os << "{"; + children[1]._int_node_ptr->nodeprint(os); + os << "}"; + } else if (kind == NOT) { + const ASTVec &children = GetChildren(); + os << GetNodeNum() << ":"; + os << "(NOT "; + children[0].LispPrint1(os, indentation); + os << ")"; + } + else if (Degree() == 0) { + // Symbol or a kind with no children print as index:NAME if shared, + // even if they have been printed before. + os << GetNodeNum() << ":"; + _int_node_ptr->nodeprint(os); + // os << "(" << _int_node_ptr->_ref_count << ")"; + // os << "{" << GetValueWidth() << "}"; + } + else if (IsAlreadyPrinted()) { + // print non-symbols as "[index]" if seen before. + os << "[" << GetNodeNum() << "]"; + // << "(" << _int_node_ptr->_ref_count << ")"; + } + else { + MarkAlreadyPrinted(); + const ASTVec &children = GetChildren(); + os << GetNodeNum() << ":" + //<< "(" << _int_node_ptr->_ref_count << ")" + << "(" << kind << " "; + // os << "{" << GetValueWidth() << "}"; + ASTVec::const_iterator iend = children.end(); + for (ASTVec::const_iterator i = children.begin(); i != iend; i++) { + i->LispPrint_indent(os, indentation+2); + } + os << ")"; + } + return os; + } + + //print in PRESENTATION LANGUAGE + // + //two pass algorithm: + // + //1. In the first pass, letize this Node, N: i.e. if a node + //1. appears more than once in N, then record this fact. + // + //2. In the second pass print a "global let" and then print N + //2. as follows: Every occurence of a node occuring more than + //2. once is replaced with the corresponding let variable. + ostream& ASTNode::PL_Print(ostream &os, + int indentation) const { + // Clear the PrintMap + BeevMgr& bm = GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); + + //pass 1: letize the node + LetizeNode(); + + //pass 2: + // + //2. print all the let variables and their counterpart expressions + //2. as follows (LET var1 = expr1, var2 = expr2, ... + // + //3. Then print the Node itself, replacing every occurence of + //3. expr1 with var1, expr2 with var2, ... + //os << "("; + 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(); + + os << "(LET "; + //print the let var first + it->first.PL_Print1(os,indentation,false); + os << " = "; + //print the expr + it->second.PL_Print1(os,indentation,false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + + for(it++;it!=itend;it++) { + os << "," << endl; + //print the let var first + it->first.PL_Print1(os,indentation,false); + os << " = "; + //print the expr + it->second.PL_Print1(os,indentation,false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } + + os << " IN " << endl; + PL_Print1(os,indentation, true); + os << ") "; + } + else + PL_Print1(os,indentation, false); + //os << " )"; + os << " "; + return os; + } //end of PL_Print() + + //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 + + //FIXME: Fetching BeevMgr is annoying. Can we put this in + //some kind of a printer class + 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() + + void ASTNode::PL_Print1(ostream& os, + int indentation, + bool letize) const { + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!IsDefined()) { + os << "<undefined>"; + return; + } + + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = GetBeevMgr(); + + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) { + (bm.NodeLetVarMap1[*this]).PL_Print1(os,indentation,letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) { + (bm.NodeLetVarMap[*this]).PL_Print1(os,indentation,letize); + return; + } + + //otherwise print it normally + Kind kind = GetKind(); + const ASTVec &c = GetChildren(); + switch(kind) { + case BVGETBIT: + c[0].PL_Print1(os,indentation,letize); + os << "{"; + c[1].PL_Print1(os,indentation,letize); + os << "}"; + break; + case BITVECTOR: + os << "BITVECTOR("; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); + os << str << ")"; + CONSTANTBV::BitVector_Dispose(str); + break; + case BOOLEAN: + os << "BOOLEAN"; + break; + case FALSE: + case TRUE: + os << kind; + break; + case BVCONST: + case SYMBOL: + _int_node_ptr->nodeprint(os); + break; + case READ: + c[0].PL_Print1(os, indentation,letize); + os << "["; + c[1].PL_Print1(os,indentation,letize); + os << "]"; + break; + case WRITE: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " WITH ["; + c[1].PL_Print1(os,indentation,letize); + os << "] := "; + c[2].PL_Print1(os,indentation,letize); + os << ")"; + os << endl; + break; + case BVUMINUS: + os << kind << "( "; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + break; + case NOT: + os << "NOT("; + c[0].PL_Print1(os,indentation,letize); + os << ") " << endl; + break; + case BVNEG: + os << " ~("; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + break; + case BVCONCAT: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " @ "; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVOR: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " | "; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + break; + case BVAND: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " & "; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + break; + case BVEXTRACT: + c[0].PL_Print1(os,indentation,letize); + os << "["; + os << GetUnsignedConst(c[1]); + os << ":"; + os << GetUnsignedConst(c[2]); + os << "]"; + break; + case BVLEFTSHIFT: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " << "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVRIGHTSHIFT: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " >> "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVMULT: + case BVSUB: + case BVPLUS: + case SBVDIV: + case SBVMOD: + case BVDIV: + case BVMOD: + os << kind << "("; + os << this->GetValueWidth(); + for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) { + os << ", " << endl; + it->PL_Print1(os,indentation,letize); + } + os << ")" << endl; + break; + case ITE: + os << "IF("; + c[0].PL_Print1(os,indentation,letize); + os << ")" << endl; + os << "THEN "; + c[1].PL_Print1(os,indentation,letize); + os << endl << "ELSE "; + c[2].PL_Print1(os,indentation,letize); + os << endl << "ENDIF"; + break; + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + os << kind << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSLT: + os << "SBVLT" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSLE: + os << "SBVLE" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSGT: + os << "SBVGT" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSGE: + os << "SBVGE" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case EQ: + c[0].PL_Print1(os,indentation,letize); + os << " = "; + c[1].PL_Print1(os,indentation,letize); + os << endl; + break; + case NEQ: + c[0].PL_Print1(os,indentation,letize); + os << " /= "; + c[1].PL_Print1(os,indentation,letize); + os << endl; + break; + case AND: + case OR: + case NAND: + case NOR: + case XOR: { + os << "("; + c[0].PL_Print1(os,indentation,letize); + ASTVec::const_iterator it=c.begin(); + ASTVec::const_iterator itend=c.end(); + + it++; + for(;it!=itend;it++) { + os << " " << kind << " "; + it->PL_Print1(os,indentation,letize); + os << endl; + } + os << ")"; + break; + } + case IFF: + os << "("; + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + os << " <=> "; + os << "("; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + os << ")"; + os << endl; + break; + case IMPLIES: + os << "("; + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + os << " => "; + os << "("; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + os << ")"; + os << endl; + break; + case BVSX: + os << kind << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + os << this->GetValueWidth(); + os << ")" << endl; + break; + default: + //remember to use LispPrinter here. Otherwise this function will + //go into an infinite loop. Recall that "<<" is overloaded to + //the lisp printer. FatalError uses lispprinter + FatalError("PL_Print1: printing not implemented for this kind: ",*this); + break; + } + } //end of PL_Print1() + + //////////////////////////////////////////////////////////////// + // BeevMgr members + //////////////////////////////////////////////////////////////// + ASTNode BeevMgr::CreateNode(Kind kind, const ASTVec & back_children) { + // create a new node. Children will be modified. + ASTInterior *n_ptr = new ASTInterior(kind, *this); + + // insert all of children at end of new_children. + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + ASTNode BeevMgr::CreateNode(Kind kind, + const ASTNode& child0, + const ASTVec & back_children) { + + ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTVec &front_children = n_ptr->_children; + front_children.push_back(child0); + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + ASTNode BeevMgr::CreateNode(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec & back_children) { + + ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTVec &front_children = n_ptr->_children; + front_children.push_back(child0); + front_children.push_back(child1); + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + + 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); + ASTVec &front_children = n_ptr->_children; + front_children.push_back(child0); + front_children.push_back(child1); + front_children.push_back(child2); + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + + ASTInterior *BeevMgr::CreateInteriorNode(Kind kind, + // children array of this node will be modified. + ASTInterior *n_ptr, + const ASTVec & back_children) { + + // insert back_children at end of front_children + ASTVec &front_children = n_ptr->_children; + + front_children.insert(front_children.end(), back_children.begin(), back_children.end()); + + // check for undefined nodes. + ASTVec::const_iterator it_end = front_children.end(); + for (ASTVec::const_iterator it = front_children.begin(); it != it_end; it++) { + if (it->IsNull()) + FatalError("CreateInteriorNode: Undefined childnode in CreateInteriorNode: ", ASTUndefined); + } + + return LookupOrCreateInterior(n_ptr); + } + + /** Trivial but virtual destructor */ + ASTSymbol::~ASTSymbol() {} + + ostream &operator<<(ostream &os, const ASTNodeMap &nmap) + { + ASTNodeMap::const_iterator iend = nmap.end(); + for (ASTNodeMap::const_iterator i = nmap.begin(); i!=iend; i++) { + os << "Key: " << i->first << endl; + os << "Value: " << i->second << endl; + } + return os; + } + + //////////////////////////////////////////////////////////////// + // BeevMgr member functions to create ASTSymbol and ASTBVConst + //////////////////////////////////////////////////////////////// + ASTNode BeevMgr::CreateSymbol(const char * const name) + { + ASTSymbol temp_sym(name, *this); + ASTNode n(LookupOrCreateSymbol(temp_sym)); + return n; + } + +#ifndef NATIVE_C_ARITH + //Create a ASTBVConst node + ASTNode BeevMgr::CreateBVConst(unsigned int width, + unsigned long long int bvconst){ + if(width > (sizeof(unsigned long long int)<<3) || width <= 0) + FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width); + + + CBV bv = CONSTANTBV::BitVector_Create(width, true); + unsigned long c_val = (0x00000000ffffffffLL) & bvconst; + unsigned int copied = 0; + + // sizeof(unsigned long) returns the number of bytes in unsigned + // long. In order to convert it to bits, we need to shift left by + // 3. Hence, sizeof(unsigned long) << 3 + + //The algo below works as follows: It starts by copying the + //lower-order bits of the input "bvconst" in chunks of size = + //number of bits in unsigned long. The variable "copied" keeps + //track of the number of chunks copied so far + + while(copied + (sizeof(unsigned long)<<3) < width){ + CONSTANTBV::BitVector_Chunk_Store(bv, sizeof(unsigned long)<<3,copied,c_val); + bvconst = bvconst >> (sizeof(unsigned long) << 3); + c_val = (0x00000000ffffffffLL) & bvconst; + copied += sizeof(unsigned long) << 3; + } + CONSTANTBV::BitVector_Chunk_Store(bv,width - copied,copied,c_val); + return CreateBVConst(bv,width); + } + + //Create a ASTBVConst node from std::string + ASTNode BeevMgr::CreateBVConst(const char* const strval, int base) { + size_t width = strlen((const char *)strval); + if(!(2 == base || 10 == base || 16 == base)){ + FatalError("CreateBVConst: unsupported base: ",ASTUndefined,base); + } + //FIXME Tim: Earlier versions of the code assume that the length of + //binary strings is 32 bits. + if(10 == base) width = 32; + if(16 == base) width = width * 4; + + //checking if the input is in the correct format + CBV bv = CONSTANTBV::BitVector_Create(width,true); + CONSTANTBV::ErrCode e; + if(2 == base){ + e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*)strval); + }else if(10 == base){ + e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*)strval); + }else if(16 == base){ + e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*)strval); + }else{ + e = CONSTANTBV::ErrCode_Pars; + } + + if(0 != e) { + cerr << "CreateBVConst: " << BitVector_Error(e); + FatalError("",ASTUndefined); + } + + //FIXME + return CreateBVConst(bv, width); + } + + + //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); + ASTNode n(LookupOrCreateBVConst(temp_bvconst)); + + CONSTANTBV::BitVector_Destroy(bv); + + return n; + } + + ASTNode BeevMgr::CreateZeroConst(unsigned width) { + CBV z = CONSTANTBV::BitVector_Create(width, true); + return CreateBVConst(z, width); + } + + ASTNode BeevMgr::CreateOneConst(unsigned width) { + CBV o = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_increment(o); + + return CreateBVConst(o,width); + } + + ASTNode BeevMgr::CreateTwoConst(unsigned width) { + CBV two = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_increment(two); + CONSTANTBV::BitVector_increment(two); + + return CreateBVConst(two,width); + } + + ASTNode BeevMgr::CreateMaxConst(unsigned width) { + CBV max = CONSTANTBV::BitVector_Create(width, false); + CONSTANTBV::BitVector_Fill(max); + + return CreateBVConst(max,width); + } + + //To ensure unique BVConst nodes, lookup the node in unique-table + //before creating a new one. + ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) { + ASTBVConst *s_ptr = &s; // it's a temporary key. + + // Do an explicit lookup to see if we need to create a copy of the string. + ASTBVConstSet::const_iterator it; + if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) { + // Make a new ASTBVConst with duplicated string (can't assign + // _name because it's const). Can cast the iterator to + // non-const -- carefully. + + ASTBVConst * s_copy = new ASTBVConst(s); + s_copy->SetNodeNum(NewNodeNum()); + + pair<ASTBVConstSet::const_iterator, bool> p = _bvconst_unique_table.insert(s_copy); + return *p.first; + } + else{ + // return symbol found in table. + return *it; + } + } + + // Inline because we need to wait until unique_table is defined + void ASTBVConst::CleanUp() { + // cout << "Deleting node " << this->GetNodeNum() << endl; + _bm._bvconst_unique_table.erase(this); + delete this; + } + + // Get the value of bvconst from a bvconst. It's an error if kind != BVCONST + CBV const ASTNode::GetBVConst() const { + if(GetKind() != BVCONST) + FatalError("GetBVConst: non bitvector-constant: ",*this); + return ((ASTBVConst *) _int_node_ptr)->GetBVConst(); + } +#else + //Create a ASTBVConst node + ASTNode BeevMgr::CreateBVConst(const unsigned int width, + const unsigned long long int bvconst) { + if(width > 64 || width <= 0) + FatalError("Fatal Error: CreateBVConst: trying to create a bvconst of width:", ASTUndefined, width); + + //64 bit mask + unsigned long long int mask = 0xffffffffffffffffLL; + mask = mask >> (64 - width); + + unsigned long long int bv = bvconst; + bv = bv & mask; + + ASTBVConst temp_bvconst(bv, *this); + temp_bvconst._value_width = width; + ASTNode n(LookupOrCreateBVConst(temp_bvconst)); + n.SetValueWidth(width); + n.SetIndexWidth(0); + return n; + } + //Create a ASTBVConst node from std::string + ASTNode BeevMgr::CreateBVConst(const char* strval, int base) { + if(!(base == 2 || base == 16 || base == 10)) + FatalError("CreateBVConst: This base is not supported: ", ASTUndefined, base); + + if(10 != base) { + unsigned int width = (base == 2) ? strlen(strval) : strlen(strval)*4; + unsigned long long int val = strtoull(strval, NULL, base); + ASTNode bvcon = CreateBVConst(width, val); + return bvcon; + } + else { + //this is an ugly hack to accomodate SMTLIB format + //restrictions. SMTLIB format represents bitvector constants in + //base 10 (what a terrible idea, but i have no choice but to + //support it), and make an implicit assumption that the length + //is 32 (another terrible idea). + unsigned width = 32; + unsigned long long int val = strtoull(strval, NULL, base); + ASTNode bvcon = CreateBVConst(width, val); + return bvcon; + } + } + + //To ensure unique BVConst nodes, lookup the node in unique-table + //before creating a new one. + ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) { + ASTBVConst *s_ptr = &s; // it's a temporary key. + + // Do an explicit lookup to see if we need to create a copy of the + // string. + ASTBVConstSet::const_iterator it; + if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) { + // Make a new ASTBVConst. Can cast the iterator to non-const -- + // carefully. + unsigned int width = s_ptr->_value_width; + ASTBVConst * s_ptr1 = new ASTBVConst(s_ptr->GetBVConst(), *this); + s_ptr1->SetNodeNum(NewNodeNum()); + s_ptr1->_value_width = width; + pair<ASTBVConstSet::const_iterator, bool> p = _bvconst_unique_table.insert(s_ptr1); + return *p.first; + } + else + // return BVConst found in table. + return *it; + } + + // Inline because we need to wait until unique_table is defined + void ASTBVConst::CleanUp() { + // cout << "Deleting node " << this->GetNodeNum() << endl; + _bm._bvconst_unique_table.erase(this); + delete this; + } + + // Get the value of bvconst from a bvconst. It's an error if kind + // != BVCONST + unsigned long long int ASTNode::GetBVConst() const { + if(GetKind() != BVCONST) + FatalError("GetBVConst: non bitvector-constant: ", *this); + return ((ASTBVConstTmp *) _int_node_ptr)->GetBVConst(); + } + + ASTNode BeevMgr::CreateZeroConst(unsigned width) { + return CreateBVConst(width,0); + } + + ASTNode BeevMgr::CreateOneConst(unsigned width) { + return CreateBVConst(width,1); + } + + ASTNode BeevMgr::CreateTwoConst(unsigned width) { + return CreateBVConst(width,2); + } + + ASTNode BeevMgr::CreateMaxConst(unsigned width) { + std::string s; + s.insert(s.end(),width,'1'); + return CreateBVConst(s.c_str(),2); + } + +#endif + + // 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! + + // Note: There seems to be a limitation of hash_set, in that insert + // returns a const iterator to the value. That prevents us from + // modifying the name (in a hash-preserving way) after the symbol is + // inserted. FIXME: Is there a way to do this with insert? Need a + // function to make a new object in the middle of insert. Read STL + // documentation. + + ASTSymbol *BeevMgr::LookupOrCreateSymbol(ASTSymbol& s) { + ASTSymbol *s_ptr = &s; // it's a temporary key. + + // Do an explicit lookup to see if we need to create a copy of the string. + ASTSymbolSet::const_iterator it; + if ((it = _symbol_unique_table.find(s_ptr)) == _symbol_unique_table.end()) { + // Make a new ASTSymbol with duplicated string (can't assign + // _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); + s_ptr1->SetNodeNum(NewNodeNum()); + s_ptr1->_value_width = s_ptr->_value_width; + pair<ASTSymbolSet::const_iterator, bool> p = _symbol_unique_table.insert(s_ptr1); + return *p.first; + } + else + // return symbol found in table. + return *it; + } + + bool BeevMgr::LookupSymbol(ASTSymbol& s) { + ASTSymbol* s_ptr = &s; // it's a temporary key. + + if(_symbol_unique_table.find(s_ptr) == _symbol_unique_table.end()) + return false; + else + return true; + } + + // Inline because we need to wait until unique_table is defined + void ASTSymbol::CleanUp() { + // cout << "Deleting node " << this->GetNodeNum() << endl; + _bm._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. + // + //////////////////////////////////////////////////////////////// + + // FIXME: Additional controls + // * Print node numbers (addresses/nums) + // * Printlength limit + // * Printdepth limit + + /** Print a vector of ASTNodes in lisp format */ + ostream &LispPrintVec(ostream &os, const ASTVec &v, int indentation) + { + // Print the children + ASTVec::const_iterator iend = v.end(); + for (ASTVec::const_iterator i = v.begin(); i != iend; i++) { + i->LispPrint_indent(os, indentation); + } + return os; + } + + // FIXME: Made non-ref in the hope that it would work better. + void lp(ASTNode node) + { + cout << lisp(node) << endl; + } + + void lpvec(const ASTVec &vec) + { + vec[0].GetBeevMgr().AlreadyPrintedSet.clear(); + LispPrintVec(cout, vec, 0); + cout << endl; + } + + // Copy constructor. Maintain _ref_count + ASTNode::ASTNode(const ASTNode &n) : _int_node_ptr(n._int_node_ptr) { +#ifndef SMTLIB + if (n._int_node_ptr) { + n._int_node_ptr->IncRef(); + } +#endif + } + + + /* FUNCTION: Typechecker for terms and formulas + * + * 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 BeevMgr::BVTypeCheck(const ASTNode& n) { + Kind k = n.GetKind(); + //The children of bitvector terms are in turn bitvectors. + ASTVec v = n.GetChildren(); + if(is_Term_kind(k)) { + switch(k) { + case BVCONST: + if(BITVECTOR_TYPE != n.GetType()) + FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n); + break; + case SYMBOL: + return; + case ITE: + if(BOOLEAN_TYPE != n[0].GetType() && + BITVECTOR_TYPE != n[1].GetType() && + BITVECTOR_TYPE != n[2].GetType()) + FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n); + if(n[1].GetValueWidth() != n[2].GetValueWidth()) + FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n); + if(n[1].GetIndexWidth() != n[2].GetIndexWidth()) + FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n); + break; + case READ: + if(n[0].GetIndexWidth() != n[1].GetValueWidth()) { + cerr << "Length of indexwidth of array: " << n[0] << " is : " << n[0].GetIndexWidth() << endl; + cerr << "Length of the actual index is: " << n[1] << " is : " << n[1].GetValueWidth() << endl; + FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n); + } + break; + case WRITE: + if(n[0].GetIndexWidth() != n[1].GetValueWidth()) + FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n); + if(n[0].GetValueWidth() != n[2].GetValueWidth()) + FatalError("BVTypeCheck: valuewidth of array != length of actual value in the term t = \n",n); + break; + case BVOR: + case BVAND: + case BVXOR: + case BVNOR: + case BVNAND: + case BVXNOR: + case BVPLUS: + case BVMULT: + case BVDIV: + case BVMOD: + case BVSUB: { + if(!(v.size() >= 2)) + FatalError("BVTypeCheck:bitwise Booleans and BV arith operators must have atleast two arguments\n",n); + unsigned int width = n.GetValueWidth(); + for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++){ + if(width != it->GetValueWidth()) { + cerr << "BVTypeCheck:Operands of bitwise-Booleans and BV arith operators must be of equal length\n"; + cerr << n << endl; + cerr << "width of term:" << width << endl; + cerr << "width of offending operand:" << it->GetValueWidth() << endl; + FatalError("BVTypeCheck:Offending operand:\n",*it); + } + if(BITVECTOR_TYPE != it->GetType()) + FatalError("BVTypeCheck: ChildNodes of bitvector-terms must be bitvectors\n",n); + } + break; + } + case BVSX: + //in BVSX(n[0],len), the length of the BVSX term must be + //greater than the length of n[0] + if(n[0].GetValueWidth() >= n.GetValueWidth()) { + FatalError("BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n",n); + } + break; + default: + for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++) + if(BITVECTOR_TYPE != it->GetType()) { + cerr << "The type is: " << it->GetType() << endl; + FatalError("BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors\n",n); + } + break; + } + + switch(k) { + case BVCONCAT: + if(n.Degree() != 2) + FatalError("BVTypeCheck: should have exactly 2 args\n",n); + if(n.GetValueWidth() != n[0].GetValueWidth() + n[1].GetValueWidth()) + FatalError("BVTypeCheck:BVCONCAT: lengths do not add up\n",n); + break; + case BVUMINUS: + case BVNEG: + if(n.Degree() != 1) + FatalError("BVTypeCheck: should have exactly 1 args\n",n); + break; + case BVEXTRACT: + if(n.Degree() != 3) + FatalError("BVTypeCheck: should have exactly 3 args\n",n); + if(!(BVCONST == n[1].GetKind() && BVCONST == n[2].GetKind())) + FatalError("BVTypeCheck: indices should be BVCONST\n",n); + if(n.GetValueWidth() != GetUnsignedConst(n[1])- GetUnsignedConst(n[2])+1) + FatalError("BVTypeCheck: length mismatch\n",n); + break; + case BVLEFTSHIFT: + case BVRIGHTSHIFT: + if(n.Degree() != 2) + FatalError("BVTypeCheck: should have exactly 2 args\n",n); + break; + //case BVVARSHIFT: + //case BVSRSHIFT: + break; + default: + break; + } + } + else { + if(!(is_Form_kind(k) && BOOLEAN_TYPE == n.GetType())) + FatalError("BVTypeCheck: not a formula:",n); + switch(k){ + case TRUE: + case FALSE: + case SYMBOL: + return; + case EQ: + case NEQ: + if(!(n[0].GetValueWidth() == n[1].GetValueWidth() && + n[0].GetIndexWidth() == n[1].GetIndexWidth())) { + cerr << "valuewidth of lhs of EQ: " << n[0].GetValueWidth() << endl; + cerr << "valuewidth of rhs of EQ: " << n[1].GetValueWidth() << endl; + cerr << "indexwidth of lhs of EQ: " << n[0].GetIndexWidth() << endl; + cerr << "indexwidth of rhs of EQ: " << n[1].GetIndexWidth() << endl; + FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); + } + break; + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVSLT: + case BVSLE: + case BVSGT: + case BVSGE: + if(BITVECTOR_TYPE != n[0].GetType() && BITVECTOR_TYPE != n[1].GetType()) + FatalError("BVTypeCheck: terms in atomic formulas must be bitvectors",n); + if(n[0].GetValueWidth() != n[1].GetValueWidth()) + FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); + if(n[0].GetIndexWidth() != n[1].GetIndexWidth()) + FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); + break; + case NOT: + if(1 != n.Degree()) + FatalError("BVTypeCheck: NOT formula can have exactly one childNode",n); + break; + case AND: + case OR: + case XOR: + case NAND: + case NOR: + if(2 > n.Degree()) + FatalError("BVTypeCheck: AND/OR/XOR/NAND/NOR: must have atleast 2 ChildNodes",n); + break; + case IFF: + case IMPLIES: + if(2 != n.Degree()) + FatalError("BVTypeCheck:IFF/IMPLIES must have exactly 2 ChildNodes",n); + break; + case ITE: + if(3 != n.Degree()) + FatalError("BVTypeCheck:ITE must have exactly 3 ChildNodes",n); + break; + default: + FatalError("BVTypeCheck: Unrecognized kind: ",ASTUndefined); + break; + } + } + } //End of TypeCheck function + + //add an assertion to the current logical context + void BeevMgr::AddAssert(const ASTNode& assert) { + if(!(is_Form_kind(assert.GetKind()) && BOOLEAN_TYPE == assert.GetType())) { + FatalError("AddAssert:Trying to assert a non-formula:",assert); + } + + ASTVec * v; + //if the stack of ASTVec is not empty, then take the top ASTVec + //and add the input assert to it + if(!_asserts.empty()) { + v = _asserts.back(); + //v->push_back(TransformFormula(assert)); + v->push_back(assert); + } + else { + //else create a logical context, and add it to the top of the + //stack + v = new ASTVec(); + //v->push_back(TransformFormula(assert)); + v->push_back(assert); + _asserts.push_back(v); + } + } + + void BeevMgr::Push(void) { + ASTVec * v; + v = new ASTVec(); + _asserts.push_back(v); + } + + void BeevMgr::Pop(void) { + if(!_asserts.empty()) { + ASTVec * c = _asserts.back(); + //by calling the clear function we ensure that the ref count is + //decremented for the ASTNodes stored in c + c->clear(); + delete c; + _asserts.pop_back(); + } + } + + void BeevMgr::AddQuery(const ASTNode& q) { + //_current_query = TransformFormula(q); + //cerr << "\nThe current query is: " << q << endl; + _current_query = q; + } + + const ASTNode BeevMgr::PopQuery() { + ASTNode q = _current_query; + _current_query = ASTTrue; + return q; + } + + const ASTNode BeevMgr::GetQuery() { + return _current_query; + } + + const ASTVec BeevMgr::GetAsserts(void) { + vector<ASTVec *>::iterator it = _asserts.begin(); + vector<ASTVec *>::iterator itend = _asserts.end(); + + ASTVec v; + for(;it!=itend;it++) { + if(!(*it)->empty()) + v.insert(v.end(),(*it)->begin(),(*it)->end()); + } + return v; + } + + //Create a new variable of ValueWidth 'n' + ASTNode BeevMgr::NewArrayVar(unsigned int index, unsigned int value) { + std:: string c("v"); + char d[32]; + sprintf(d,"%d",_symbol_count++); + std::string ccc(d); + c += "_writearray_" + ccc; + + ASTNode CurrentSymbol = CreateSymbol(c.c_str()); + CurrentSymbol.SetValueWidth(value); + CurrentSymbol.SetIndexWidth(index); + return CurrentSymbol; + } //end of NewArrayVar() + + + //Create a new variable of ValueWidth 'n' + ASTNode BeevMgr::NewVar(unsigned int value) { + std:: string c("v"); + char d[32]; + sprintf(d,"%d",_symbol_count++); + std::string ccc(d); + c += "_new_stp_var_" + ccc; + + ASTNode CurrentSymbol = CreateSymbol(c.c_str()); + CurrentSymbol.SetValueWidth(value); + CurrentSymbol.SetIndexWidth(0); + _introduced_symbols.insert(CurrentSymbol); + return CurrentSymbol; + } //end of NewVar() + + //prints statistics for the ASTNode + void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a){ + if(!stats) + return; + + StatInfoSet.clear(); + //print node size: + cout << endl << "Printing: " << c; + if(print_nodes) { + //a.PL_Print(cout,0); + //cout << endl; + cout << a << endl; + } + cout << "Node size is: "; + cout << NodeSize(a) << endl << endl; + } + + unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo) { + if(clearStatInfo) + StatInfoSet.clear(); + + ASTNodeSet::iterator it; + if((it = StatInfoSet.find(a)) != StatInfoSet.end()) + //has already been counted + return 0; + + //record that you have seen this node already + StatInfoSet.insert(a); + + //leaf node has a size of 1 + if(a.Degree() == 0) + return 1; + + unsigned newn = 1; + ASTVec c = a.GetChildren(); + for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) + newn += NodeSize(*it); + return newn; + } + + void BeevMgr::ClearAllTables(void) { + //clear all tables before calling toplevelsat + _ASTNode_to_SATVar.clear(); + _SATVar_to_AST.clear(); + + for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), + itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { + delete it->second; + } + _ASTNode_to_Bitvector.clear(); + + /* OLD Destructor + * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + + /*What should I do here? For ASTNodes? + * for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + BBTermMemo.clear(); + BBFormMemo.clear(); + NodeLetVarMap.clear(); + NodeLetVarMap1.clear(); + PLPrintNodeSet.clear(); + AlreadyPrintedSet.clear(); + SimplifyMap.clear(); + SimplifyNegMap.clear(); + SolverMap.clear(); + AlwaysTrueFormMap.clear(); + _arrayread_ite.clear(); + _arrayread_symbol.clear(); + _introduced_symbols.clear(); + TransformMap.clear(); + _letid_expr_map.clear(); + CounterExampleMap.clear(); + ComputeFormulaMap.clear(); + StatInfoSet.clear(); + + // for(std::vector<ASTVec *>::iterator it=_asserts.begin(), + // itend=_asserts.end();it!=itend;it++) { + // (*it)->clear(); + // } + _asserts.clear(); + for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), + iset_end = _arrayname_readindices.end(); + iset!=iset_end;iset++) { + iset->second.clear(); + } + + _arrayname_readindices.clear(); + _interior_unique_table.clear(); + _symbol_unique_table.clear(); + _bvconst_unique_table.clear(); + } + + void BeevMgr::ClearAllCaches(void) { + //clear all tables before calling toplevelsat + _ASTNode_to_SATVar.clear(); + _SATVar_to_AST.clear(); + + + for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), + itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { + delete it->second; + } + _ASTNode_to_Bitvector.clear(); + + /*OLD destructor + * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + + /*What should I do here? + *for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + BBTermMemo.clear(); + BBFormMemo.clear(); + NodeLetVarMap.clear(); + NodeLetVarMap1.clear(); + PLPrintNodeSet.clear(); + AlreadyPrintedSet.clear(); + SimplifyMap.clear(); + SimplifyNegMap.clear(); + SolverMap.clear(); + AlwaysTrueFormMap.clear(); + _arrayread_ite.clear(); + _arrayread_symbol.clear(); + _introduced_symbols.clear(); + TransformMap.clear(); + _letid_expr_map.clear(); + CounterExampleMap.clear(); + ComputeFormulaMap.clear(); + StatInfoSet.clear(); + + for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), + iset_end = _arrayname_readindices.end(); + iset!=iset_end;iset++) { + iset->second.clear(); + } + + _arrayname_readindices.clear(); + //_interior_unique_table.clear(); + //_symbol_unique_table.clear(); + //_bvconst_unique_table.clear(); + } + + void BeevMgr::CopySolverMap_To_CounterExample(void) { + if(!SolverMap.empty()) { + CounterExampleMap.insert(SolverMap.begin(),SolverMap.end()); + } + } + + void FatalError(const char * str, const ASTNode& a, int w) { + if(a.GetKind() != UNDEFINED) { + cerr << "Fatal Error: " << str << endl << a << endl; + cerr << w << endl; + } + else { + cerr << "Fatal Error: " << str << endl; + cerr << w << endl; + } + if (vc_error_hdlr) + vc_error_hdlr(str); + exit(-1); + //assert(0); + } + + void FatalError(const char * str) { + cerr << "Fatal Error: " << str << endl; + if (vc_error_hdlr) + vc_error_hdlr(str); + exit(-1); + //assert(0); + } + + //Variable Order Printer: A global function which converts a MINISAT + //var into a ASTNODE var. It then prints this var along with + //variable order dcisions taken by MINISAT. + void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, + int decision_level, int polarity) { + BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var]; + cout << spaces(decision_level); + if(polarity) { + cout << "!"; + } + vv.PL_Print(cout,0); + cout << endl; + } + + void SortByExprNum(ASTVec& v) { + sort(v.begin(), v.end(), exprless); + } + + bool isAtomic(Kind kind) { + if(TRUE == kind || + FALSE == kind || + EQ == kind || + NEQ == kind || + BVLT == kind || + BVLE == kind || + BVGT == kind || + BVGE == kind || + BVSLT == kind || + BVSLE == kind || + BVSGT == kind || + BVSGE == kind || + SYMBOL == kind || + BVGETBIT == kind) + return true; + return false; + } + + BeevMgr::~BeevMgr() { + ClearAllTables(); + } +}; // end namespace + |