From 28aacfaeddbfe047ab0fba29b6843facc5e5e06a Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 31 Jul 2012 17:27:46 +0000 Subject: Forgot to remove the actual stp directory. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161056 91177308-0d34-0410-b5e6-96231b3b80d8 --- stp/AST/AST.cpp | 1579 ---------------------------------------- stp/AST/AST.h | 1806 ---------------------------------------------- stp/AST/ASTKind.cpp | 118 --- stp/AST/ASTKind.h | 79 -- stp/AST/ASTKind.kinds | 71 -- stp/AST/ASTUtil.cpp | 45 -- stp/AST/ASTUtil.h | 107 --- stp/AST/BitBlast.cpp | 812 --------------------- stp/AST/Makefile | 19 - stp/AST/STLport_config.h | 20 - stp/AST/SimpBool.cpp | 408 ----------- stp/AST/ToCNF.cpp | 506 ------------- stp/AST/ToSAT.cpp | 1386 ----------------------------------- stp/AST/Transform.cpp | 492 ------------- stp/AST/genkinds.pl | 123 ---- 15 files changed, 7571 deletions(-) delete mode 100644 stp/AST/AST.cpp delete mode 100644 stp/AST/AST.h delete mode 100644 stp/AST/ASTKind.cpp delete mode 100644 stp/AST/ASTKind.h delete mode 100644 stp/AST/ASTKind.kinds delete mode 100644 stp/AST/ASTUtil.cpp delete mode 100644 stp/AST/ASTUtil.h delete mode 100644 stp/AST/BitBlast.cpp delete mode 100644 stp/AST/Makefile delete mode 100644 stp/AST/STLport_config.h delete mode 100644 stp/AST/SimpBool.cpp delete mode 100644 stp/AST/ToCNF.cpp delete mode 100644 stp/AST/ToSAT.cpp delete mode 100644 stp/AST/Transform.cpp delete mode 100755 stp/AST/genkinds.pl (limited to 'stp/AST') diff --git a/stp/AST/AST.cpp b/stp/AST/AST.cpp deleted file mode 100644 index 63319de9..00000000 --- a/stp/AST/AST.cpp +++ /dev/null @@ -1,1579 +0,0 @@ -/******************************************************************** - * 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 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 *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 << ""; - 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 >::iterator it = bm.NodeLetVarVec.begin(); - std::vector >::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 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 << ""; - 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 == 0 || width > (sizeof(unsigned long long int)<<3)) - FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width); - - CBV bv = CONSTANTBV::BitVector_Create(width, true); - - // Copy bvconst in using at most MaxChunkSize chunks, starting with the - // least significant bits. - const uint32_t MaxChunkSize = 32; - for (unsigned offset = 0; offset != width;) { - uint32_t numbits = std::min(MaxChunkSize, width - offset); - uint32_t mask = ~0 >> (32 - numbits); - CONSTANTBV::BitVector_Chunk_Store(bv, numbits, offset, - (bvconst >> offset) & mask); - offset += numbits; - } - - 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 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 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 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 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::iterator it = _asserts.begin(); - vector::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::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 - diff --git a/stp/AST/AST.h b/stp/AST/AST.h deleted file mode 100644 index 3052107f..00000000 --- a/stp/AST/AST.h +++ /dev/null @@ -1,1806 +0,0 @@ -// -*- c++ -*- -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ - -#ifndef AST_H -#define AST_H -#include -#ifdef EXT_HASH_MAP -#include -#include -#else -#include -#include -#endif -#include -#include -#include -#include -#include -#include "ASTUtil.h" -#include "ASTKind.h" -#include "../sat/Solver.h" -#include "../sat/SolverTypes.h" -#include -#include -#ifndef NATIVE_C_ARITH -#include "../constantbv/constantbv.h" -#endif -/***************************************************************************** - * LIST OF CLASSES DECLARED IN THIS FILE: - * - * class BeevMgr; - * class ASTNode; - * class ASTInternal; - * class ASTInterior; - * class ASTSymbol; - * class ASTBVConst; - *****************************************************************************/ -namespace BEEV { - using namespace std; - using namespace MINISAT; -#ifdef EXT_HASH_MAP - using namespace __gnu_cxx; -#endif - - //return types for the GetType() function in ASTNode class - enum types { - BOOLEAN_TYPE = 0, - BITVECTOR_TYPE, - ARRAY_TYPE, - UNKNOWN_TYPE - }; - - class BeevMgr; - class ASTNode; - class ASTInternal; - class ASTInterior; - class ASTSymbol; - class ASTBVConst; - class BVSolver; - - //Vector of ASTNodes, used for child nodes among other things. - typedef vector ASTVec; - extern ASTVec _empty_ASTVec; - extern BeevMgr * globalBeevMgr_for_parser; - - typedef unsigned int * CBV; - - /***************************************************************************/ - /* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */ - /***************************************************************************/ - class ASTNode { - friend class BeevMgr; - friend class vector; - //Print the arguments in lisp format. - friend ostream &LispPrintVec(ostream &os, - const ASTVec &v, int indentation = 0); - - private: - // FIXME: make this into a reference? - ASTInternal * _int_node_ptr; // The real data. - - // Usual constructor. - ASTNode(ASTInternal *in); - - //Check if it points to a null node - bool IsNull () const { return _int_node_ptr == NULL; } - - //Equal iff ASTIntNode pointers are the same. - friend bool operator==(const ASTNode node1, const ASTNode node2){ - return ((size_t) node1._int_node_ptr) == ((size_t) node2._int_node_ptr); - } - - /* FIXME: Nondeterministic code *** */ - /** questionable pointer comparison function */ - friend bool operator<(const ASTNode node1, const ASTNode node2){ - return ((size_t) node1._int_node_ptr) < ((size_t) node2._int_node_ptr); - } - - public: - // This is for sorting by expression number (used in Boolean - //optimization) - friend bool exprless(const ASTNode n1, const ASTNode n2) { - Kind k1 = n1.GetKind(); - Kind k2 = n2.GetKind(); - - if(BVCONST == k1 && BVCONST != k2){ - return true; - } - if(BVCONST != k1 && BVCONST == k2){ - return false; - } - - if(SYMBOL == k1 && SYMBOL != k2) { - return true; - } - - if(SYMBOL != k1 && SYMBOL == k2) { - return false; - } - - return (n1.GetNodeNum() < n2.GetNodeNum()); - }//end of exprless - - // Internal lisp-form printer that does not clear _node_print_table - ostream &LispPrint1(ostream &os, int indentation) const; - - ostream &LispPrint_indent(ostream &os, int indentation) const; - - // For lisp DAG printing. Has it been printed already, so we can - // just print the node number? - bool IsAlreadyPrinted() const; - void MarkAlreadyPrinted() const; - - public: - // Default constructor. This gets used when declaring an ASTVec - // of a given size, in the hash table, etc. For faster - // refcounting, create a symbol node for NULL. Give it a big - // initial refcount. Never free it. also check, for ref-count - // overflow? - ASTNode() : _int_node_ptr(NULL) { }; - - // Copy constructor - ASTNode(const ASTNode &n); - - // Destructor - ~ASTNode(); - - // Assignment (for ref counting) - ASTNode& operator=(const ASTNode& n); - - BeevMgr &GetBeevMgr() const; - - // Access node number - int GetNodeNum() const; - - // Access kind. Inlined later because of declaration ordering problems. - Kind GetKind() const; - - // access Children - const ASTVec &GetChildren() const; - - // Return the number of child nodes - size_t Degree() const{ - return GetChildren().size(); - }; - - // Get indexth childNode. - const ASTNode operator[](size_t index) const { - return GetChildren()[index]; - }; - - // Get begin() iterator for child nodes - ASTVec::const_iterator begin() const{ - return GetChildren().begin(); - }; - - // Get end() iterator for child nodes - ASTVec::const_iterator end() const{ - return GetChildren().end(); - }; - - //Get back() element for child nodes - const ASTNode back() const{ - return GetChildren().back(); - }; - - // Get the name from a symbol (char *). It's an error if kind != SYMBOL - const char *GetName() const; - - //Get the BVCONST value -#ifndef NATIVE_C_ARITH - CBV GetBVConst() const; -#else - unsigned long long int GetBVConst() const; -#endif - - /*ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0)) - * - *ASTNode is of type ARRAY <==> ((indexwidth>0)&&(valuewidth>0)) - * - *ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0)) - * - *both indexwidth and valuewidth should never be less than 0 - */ - unsigned int GetIndexWidth () const; - - // FIXME: This function is dangerous. Try to eliminate it's use. - void SetIndexWidth (unsigned int iw) const; - - unsigned int GetValueWidth () const; - - // FIXME: This function is dangerous. Try to eliminate it's use. - void SetValueWidth (unsigned int vw) const; - - //return the type of the ASTNode - //0 iff BOOLEAN - //1 iff BITVECTOR - //2 iff ARRAY - - /*ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0)) - * - *ASTNode is of type ARRAY <==> ((indexwidth>0)&&(valuewidth>0)) - * - *ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0)) - * - *both indexwidth and valuewidth should never be less than 0 - */ - types GetType(void) const; - - // Hash is pointer value of _int_node_ptr. - size_t Hash() const{ - return (size_t) _int_node_ptr; - //return GetNodeNum(); - } - - // lisp-form printer - ostream& LispPrint(ostream &os, int indentation = 0) const; - - //Presentation Language Printer - ostream& PL_Print(ostream &os, int indentation = 0) const; - - void PL_Print1(ostream &os, int indentation = 0, bool b = false) const; - - //Construct let variables for shared subterms - void LetizeNode(void) const; - - // Attempt to define something that will work in the gdb - friend void lp(ASTNode &node); - friend void lpvec(const ASTVec &vec); - - friend ostream &operator<<(ostream &os, const ASTNode &node) { - node.LispPrint(os, 0); - return os; - }; - - // Check whether the ASTNode points to anything. Undefined nodes - // are created by the default constructor. In binding table (for - // lambda args, etc.), undefined nodes are used to represent - // deleted entries. - bool IsDefined() const { return _int_node_ptr != NULL; } - - /* Hasher class for STL hash_maps and hash_sets that use ASTNodes - * as keys. Needs to be public so people can define hash tables - * (and use ASTNodeMap class)*/ - class ASTNodeHasher { - public: - size_t operator() (const ASTNode& n) const{ - return (size_t) n._int_node_ptr; - //return (size_t)n.GetNodeNum(); - }; - }; //End of ASTNodeHasher - - /* Equality for ASTNode hash_set and hash_map. Returns true iff - * internal pointers are the same. Needs to be public so people - * can define hash tables (and use ASTNodeSet class)*/ - class ASTNodeEqual { - public: - bool operator()(const ASTNode& n1, const ASTNode& n2) const{ - return (n1._int_node_ptr == n2._int_node_ptr); - } - }; //End of ASTNodeEqual - }; //End of Class ASTNode - - void FatalError(const char * str, const ASTNode& a, int w = 0); - void FatalError(const char * str); - void SortByExprNum(ASTVec& c); - bool exprless(const ASTNode n1, const ASTNode n2); - bool isAtomic(Kind k); - - /***************************************************************************/ - /* Class ASTInternal:Abstract base class for internal node representation.*/ - /* Requires Kind and ChildNodes so same traversal works */ - /* on all nodes. */ - /***************************************************************************/ - class ASTInternal { - - friend class ASTNode; - - protected: - - // reference count. - int _ref_count; - - // Kind. It's a type tag and the operator. - Kind _kind; - - // The vector of children (*** should this be in ASTInterior? ***) - ASTVec _children; - - // Manager object. Having this backpointer means it's easy to - // find the manager when we need it. - BeevMgr &_bm; - - //Nodenum is a unique positive integer for the node. The nodenum - //of a node should always be greater than its descendents (which - //is easily achieved by incrementing the number each time a new - //node is created). - int _node_num; - - // Length of bitvector type for array index. The term is an - // array iff this is positive. Otherwise, the term is a bitvector - // or a bit. - unsigned int _index_width; - - // Length of bitvector type for scalar value or array element. - // If this is one, the term represents a single bit (same as a bitvector - // of length 1). It must be 1 or greater. - unsigned int _value_width; - - // Increment refcount. -#ifndef SMTLIB - void IncRef() { ++_ref_count; } -#else - void IncRef() { } -#endif - - // DecRef is a potentially expensive, because it has to delete - // the node from the unique table, in addition to freeing it. - // FIXME: Consider putting in a backpointer (iterator) to the hash - // table entry so it can be deleted without looking it up again. - void DecRef(); - - virtual Kind GetKind() const { return _kind; } - - virtual ASTVec const &GetChildren() const { return _children; } - - int GetNodeNum() const { return _node_num; } - - void SetNodeNum(int nn) { _node_num = nn; }; - - // Constructor (bm only) - ASTInternal(BeevMgr &bm, int nodenum = 0) : - _ref_count(0), - _kind(UNDEFINED), - _bm(bm), - _node_num(nodenum), - _index_width(0), - _value_width(0) { } - - // Constructor (kind only, empty children, int nodenum) - ASTInternal(Kind kind, BeevMgr &bm, int nodenum = 0) : - _ref_count(0), - _kind(kind), - _bm(bm), - _node_num(nodenum), - _index_width(0), - _value_width(0) { } - - // Constructor (kind and children). This copies the contents of - // the child nodes. - // FIXME: is there a way to avoid repeating these? - ASTInternal(Kind kind, const ASTVec &children, BeevMgr &bm, int nodenum = 0) : - _ref_count(0), - _kind(kind), - _children(children), - _bm(bm), - _node_num(nodenum), - _index_width(0), - _value_width(0) { } - - // Copy constructor. This copies the contents of the child nodes - // array, along with everything else. Assigning the smart pointer, - // ASTNode, does NOT invoke this; This should only be used for - // temporary hash keys before uniquefication. - // FIXME: I don't think children need to be copied. - ASTInternal(const ASTInternal &int_node, int nodenum = 0) : - _ref_count(0), - _kind(int_node._kind), - _children(int_node._children), - _bm(int_node._bm), - _node_num(int_node._node_num), - _index_width(int_node._index_width), - _value_width(int_node._value_width) { } - - // Copying assign operator. Also copies contents of children. - ASTInternal& operator=(const ASTInternal &int_node); - - // Cleanup function for removing from hash table - virtual void CleanUp() = 0; - - // Destructor (does nothing, but is declared virtual here. - virtual ~ASTInternal(); - - // Abstract virtual print function for internal node. - virtual void nodeprint(ostream& os) { os << "*"; }; - }; //End of Class ASTInternal - - // FIXME: Should children be only in interior node type? - /*************************************************************************** - Class ASTInterior: Internal representation of an interior - ASTNode. Generally, these nodes should have at least one - child - ***************************************************************************/ - class ASTInterior : public ASTInternal { - - friend class BeevMgr; - friend class ASTNodeHasher; - friend class ASTNodeEqual; - - private: - - // Hasher for ASTInterior pointer nodes - class ASTInteriorHasher { - public: - size_t operator()(const ASTInterior *int_node_ptr) const; - }; - - // Equality for ASTInterior nodes - class ASTInteriorEqual { - public: - bool operator()(const ASTInterior *int_node_ptr1, - const ASTInterior *int_node_ptr2) const{ - return (*int_node_ptr1 == *int_node_ptr2); - } - }; - - // Used in Equality class for hash tables - friend bool operator==(const ASTInterior &int_node1, - const ASTInterior &int_node2){ - return (int_node1._kind == int_node2._kind) && - (int_node1._children == int_node2._children); - } - - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); - - // Returns kinds. "lispprinter" handles printing of parenthesis - // and childnodes. - virtual void nodeprint(ostream& os) { - os << _kind_names[_kind]; - } - public: - - // FIXME: This should not be public, but has to be because the - // ASTInterior hash table insists on it. I can't seem to make the - // private destructor visible to hash_set. It does not even work - // to put "friend class hash_set" in here. - - // Basic constructors - ASTInterior(Kind kind, BeevMgr &bm) : - ASTInternal(kind, bm) { } - - ASTInterior(Kind kind, ASTVec &children, BeevMgr &bm) : - ASTInternal(kind, children, bm) { } - - //Copy constructor. This copies the contents of the child nodes - //array, along with everything else. Assigning the smart pointer, - //ASTNode, does NOT invoke this. - ASTInterior(const ASTInterior &int_node) : ASTInternal(int_node) { } - - // Destructor (does nothing, but is declared virtual here. - virtual ~ASTInterior(); - - }; //End of ASTNodeInterior - - - /***************************************************************************/ - /* Class ASTSymbol: Class to represent internals of Symbol node. */ - /***************************************************************************/ - class ASTSymbol : public ASTInternal{ - friend class BeevMgr; - friend class ASTNode; - friend class ASTNodeHasher; - friend class ASTNodeEqual; - - private: - // The name of the symbol - const char * const _name; - - class ASTSymbolHasher{ - public: - size_t operator() (const ASTSymbol *sym_ptr) const{ - hash h; - return h(sym_ptr->_name); - }; - }; - - // Equality for ASTInternal nodes - class ASTSymbolEqual{ - public: - bool operator()(const ASTSymbol *sym_ptr1, const ASTSymbol *sym_ptr2) const{ - return (*sym_ptr1 == *sym_ptr2); - } - }; - - friend bool operator==(const ASTSymbol &sym1, const ASTSymbol &sym2){ - return (strcmp(sym1._name, sym2._name) == 0); - } - - const char *GetName() const{return _name;} - - // Print function for symbol -- return name */ - virtual void nodeprint(ostream& os) { os << _name;} - - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); - - public: - - // Default constructor - ASTSymbol(BeevMgr &bm) : ASTInternal(bm), _name(NULL) { } - - // Constructor. This does NOT copy its argument. - ASTSymbol(const char * const name, BeevMgr &bm) : ASTInternal(SYMBOL, bm), - _name(name) { } - - // Destructor (does nothing, but is declared virtual here. - virtual ~ASTSymbol(); - - // Copy constructor - // FIXME: seems to be calling default constructor for astinternal - ASTSymbol(const ASTSymbol &sym) : - ASTInternal(sym._kind, sym._children, sym._bm), - _name(sym._name) { } - }; //End of ASTSymbol - - - /***************************************************************************/ - /* Class ASTBVConst: Class to represent internals of a bitvectorconst */ - /***************************************************************************/ - -#ifndef NATIVE_C_ARITH - - class ASTBVConst : public ASTInternal { - friend class BeevMgr; - friend class ASTNode; - friend class ASTNodeHasher; - friend class ASTNodeEqual; - - private: - //This is the private copy of a bvconst currently - //This should not be changed at any point - CBV _bvconst; - - class ASTBVConstHasher{ - public: - size_t operator() (const ASTBVConst * bvc) const { - return CONSTANTBV::BitVector_Hash(bvc->_bvconst); - }; - }; - - class ASTBVConstEqual{ - public: - bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const { - if( bvc1->_value_width != bvc2->_value_width){ - return false; - } - return (0==CONSTANTBV::BitVector_Compare(bvc1->_bvconst,bvc2->_bvconst)); - } - }; - - //FIXME Keep an eye on this function - ASTBVConst(CBV bv, unsigned int width, BeevMgr &bm) : - ASTInternal(BVCONST, bm) - { - _bvconst = CONSTANTBV::BitVector_Clone(bv); - _value_width = width; - } - - friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){ - if(bvc1._value_width != bvc2._value_width) - return false; - return (0==CONSTANTBV::BitVector_Compare(bvc1._bvconst,bvc2._bvconst)); - } - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); - - // Print function for bvconst -- return _bvconst value in bin format - virtual void nodeprint(ostream& os) { - unsigned char *res; - const char *prefix; - - if (_value_width%4 == 0) { - res = CONSTANTBV::BitVector_to_Hex(_bvconst); - prefix = "0hex"; - } else { - res = CONSTANTBV::BitVector_to_Bin(_bvconst); - prefix = "0bin"; - } - if (NULL == res) { - os << "nodeprint: BVCONST : could not convert to string" << _bvconst; - FatalError(""); - } - os << prefix << res; - CONSTANTBV::BitVector_Dispose(res); - } - - // Copy constructor. - ASTBVConst(const ASTBVConst &sym) : - ASTInternal(sym._kind, sym._children, sym._bm) - { - _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst); - _value_width = sym._value_width; - } - - public: - virtual ~ASTBVConst(){ - CONSTANTBV::BitVector_Destroy(_bvconst); - } - - CBV GetBVConst() const {return _bvconst;} - }; //End of ASTBVConst - - //FIXME This function is DEPRICATED - //Do not use in the future - inline unsigned int GetUnsignedConst(const ASTNode n) { - if(32 < n.GetValueWidth()) - FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:"); - - return (unsigned int) *((unsigned int *)n.GetBVConst()); - } -#else - class ASTBVConst : public ASTInternal { - friend class BeevMgr; - friend class ASTNode; - friend class ASTNodeHasher; - friend class ASTNodeEqual; - - private: - // the bitvector contents. bitvector contents will be in two - // modes. one mode where all bitvectors are NATIVE and in this - // mode we use native unsigned long long int to represent the - // 32/64 bitvectors. The other for arbitrary length bitvector - // operations. - const unsigned long long int _bvconst; - - class ASTBVConstHasher{ - public: - size_t operator() (const ASTBVConst * bvc) const{ - //Thomas Wang's 64 bit Mix Function - unsigned long long int key(bvc->_bvconst); - key += ~(key << 32); - key ^= (key >> 22); - key += ~(key << 13); - key ^= (key >> 8); - key += (key << 3); - key ^= (key >> 15); - key += ~(key << 27); - key ^= (key >> 31); - - size_t return_key = key; - return return_key; - }; - }; - - class ASTBVConstEqual{ - public: - bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const { - return ((bvc1->_bvconst == bvc2->_bvconst) - && (bvc1->_value_width == bvc2->_value_width)); - } - }; - - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); - public: - // Default constructor - ASTBVConst(const unsigned long long int bv, BeevMgr &bm) : - ASTInternal(BVCONST, bm), _bvconst(bv) { - } - - // Copy constructor. FIXME: figure out how this is supposed to - // work. - ASTBVConst(const ASTBVConst &sym) : - ASTInternal(sym._kind, sym._children, sym._bm), - _bvconst(sym._bvconst) { - _value_width = sym._value_width; - } - - // Destructor (does nothing, but is declared virtual here) - virtual ~ASTBVConst() { } - - friend bool operator==(const ASTBVConst &sym1, const ASTBVConst &sym2){ - return ((sym1._bvconst == sym2._bvconst) && - (sym1._value_width == sym2._value_width)); - } - - // Print function for bvconst -- return _bvconst value in binary format - virtual void nodeprint(ostream& os) { - string s = "0bin"; - unsigned long long int bitmask = 0x8000000000000000LL; - bitmask = bitmask >> (64-_value_width); - - for (; bitmask > 0; bitmask >>= 1) - s += (_bvconst & bitmask) ? '1' : '0'; - os << s; - } - - unsigned long long int GetBVConst() const {return _bvconst;} - }; //End of ASTBVConst - - //return value of bvconst - inline unsigned int GetUnsignedConst(const ASTNode n) { - if(32 < n.GetValueWidth()) - FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:"); - return (unsigned int)n.GetBVConst(); - } -#endif -/* -#else - // the bitvector contents. bitvector contents will be in two - // modes. one mode where all bitvectors are NATIVE and in this mode - // we use native unsigned long long int to represent the 32/64 - // bitvectors. The other for arbitrary length bitvector operations. - - //BVCONST defined for arbitrary length bitvectors - class ASTBVConst : public ASTInternal{ - friend class BeevMgr; - friend class ASTNode; - friend class ASTNodeHasher; - friend class ASTNodeEqual; - - private: - const char * const _bvconst; - - class ASTBVConstHasher{ - public: - size_t operator() (const ASTBVConst * bvc) const{ - hash h; - return h(bvc->_bvconst); - }; - }; - - class ASTBVConstEqual{ - public: - bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const { - if(bvc1->_value_width != bvc2->_value_width) - return false; - return (0 == strncmp(bvc1->_bvconst,bvc2->_bvconst,bvc1->_value_width)); - } - }; - - ASTBVConst(const char * bv, BeevMgr &bm) : - ASTInternal(BVCONST, bm), _bvconst(bv) { - //_value_width = strlen(bv); - } - - friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){ - if(bvc1._value_width != bvc2._value_width) - return false; - return (0 == strncmp(bvc1._bvconst,bvc2._bvconst,bvc1._value_width)); - } - - // Call this when deleting a node that has been stored in the - // the unique table - virtual void CleanUp(); - - // Print function for bvconst -- return _bvconst value in binary format - virtual void nodeprint(ostream& os) { - if(_value_width%4 == 0) { - unsigned int * iii = CONSTANTBV::BitVector_Create(_value_width,true); - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_from_Bin(iii,(unsigned char*)_bvconst); - //error printing - if(0 != e) { - os << "nodeprint: BVCONST : wrong hex value: " << BitVector_Error(e); - FatalError(""); - } - unsigned char * ccc = CONSTANTBV::BitVector_to_Hex(iii); - os << "0hex" << ccc; - CONSTANTBV::BitVector_Destroy(iii); - } - else { - std::string s(_bvconst,_value_width); - s = "0bin" + s; - os << s; - } - } - - // Copy constructor. - ASTBVConst(const ASTBVConst &sym) : ASTInternal(sym._kind, sym._children, sym._bm),_bvconst(sym._bvconst) { - //checking if the input is in the correct format - for(unsigned int jj=0;jj ASTNodeMap; - - // Function to dump contents of ASTNodeMap - ostream &operator<<(ostream &os, const ASTNodeMap &nmap); - - /*************************************************************************** - Typedef ASTNodeSet: This is a hash set of ASTNodes. Very useful - for representing things like "visited nodes" - ***************************************************************************/ - typedef hash_set ASTNodeSet; - - typedef hash_multiset ASTNodeMultiSet; - - //external parser table for declared symbols. - //FIXME: move to a more appropriate place - extern ASTNodeSet _parser_symbol_table; - - /*************************************************************************** - Class LispPrinter: iomanipulator for printing ASTNode or ASTVec - ***************************************************************************/ - class LispPrinter { - - public: - ASTNode _node; - - // number of spaces to print before first real character of - // object. - int _indentation; - - // FIXME: pass ASTNode by reference - // Constructor to build the LispPrinter object - LispPrinter(ASTNode node, int indentation): _node(node), _indentation(indentation) { } - - friend ostream &operator<<(ostream &os, const LispPrinter &lp){ - return lp._node.LispPrint(os, lp._indentation); - }; - - }; //End of ListPrinter - - //This is the IO manipulator. It builds an object of class - //"LispPrinter" that has a special overloaded "<<" operator. - inline LispPrinter lisp(const ASTNode &node, int indentation = 0){ - LispPrinter lp(node, indentation); - return lp; - } - - /***************************************************************************/ - /* Class LispVecPrinter:iomanipulator for printing vector of ASTNodes */ - /***************************************************************************/ - class LispVecPrinter { - - public: - const ASTVec * _vec; - // number of spaces to print before first real - // character of object. - int _indentation; - - // Constructor to build the LispPrinter object - LispVecPrinter(const ASTVec &vec, int indentation){ - _vec = &vec; _indentation = indentation; - } - - friend ostream &operator<<(ostream &os, const LispVecPrinter &lvp){ - LispPrintVec(os, *lvp._vec, lvp._indentation); - return os; - }; - }; //End of Class ListVecPrinter - - //iomanipulator. builds an object of class "LisPrinter" that has a - //special overloaded "<<" operator. - inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0){ - LispVecPrinter lvp(vec, indentation); - return lvp; - } - - - /***************************************************************** - * INLINE METHODS from various classed, declared here because of - * dependencies on classes that are declared later. - *****************************************************************/ - // ASTNode accessor function. - inline Kind ASTNode::GetKind() const { - //cout << "GetKind: " << _int_node_ptr; - return _int_node_ptr->GetKind(); - } - - // FIXME: should be const ASTVec const? - // Declared here because of same ordering problem as GetKind. - inline const ASTVec &ASTNode::GetChildren() const { - return _int_node_ptr->GetChildren(); - } - - // Access node number - inline int ASTNode::GetNodeNum() const { - return _int_node_ptr->_node_num; - } - - inline unsigned int ASTNode::GetIndexWidth () const { - return _int_node_ptr->_index_width; - } - - inline void ASTNode::SetIndexWidth (unsigned int iw) const { - _int_node_ptr->_index_width = iw; - } - - inline unsigned int ASTNode::GetValueWidth () const { - return _int_node_ptr->_value_width; - } - - inline void ASTNode::SetValueWidth (unsigned int vw) const { - _int_node_ptr->_value_width = vw; - } - - //return the type of the ASTNode: 0 iff BOOLEAN; 1 iff BITVECTOR; 2 - //iff ARRAY; 3 iff UNKNOWN; - inline types ASTNode::GetType() const { - if((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN - return BOOLEAN_TYPE; - if((GetIndexWidth() == 0) && (GetValueWidth() > 0)) //BITVECTOR - return BITVECTOR_TYPE; - if((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY - return ARRAY_TYPE; - return UNKNOWN_TYPE; - } - - // Constructor; creates a new pointer, increments refcount of - // pointed-to object. -#ifndef SMTLIB - inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { - if (in) in->IncRef(); - } -#else - inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { }; -#endif - - // Assignment. Increment refcount of new value, decrement refcount - // of old value and destroy if this was the last pointer. FIXME: - // accelerate this by creating an intnode with a ref counter instead - // of pointing to NULL. Need a special check in CleanUp to make - // sure the null node never gets freed. - -#ifndef SMTLIB - inline ASTNode& ASTNode::operator=(const ASTNode& n) { - if (n._int_node_ptr) { - n._int_node_ptr->IncRef(); - } - if (_int_node_ptr) { - _int_node_ptr->DecRef(); - } - _int_node_ptr = n._int_node_ptr; - return *this; - } -#else - inline ASTNode& ASTNode::operator=(const ASTNode& n) { - _int_node_ptr = n._int_node_ptr; - return *this; - } -#endif - -#ifndef SMTLIB - inline void ASTInternal::DecRef() - { - if (--_ref_count == 0) { - // Delete node from unique table and kill it. - CleanUp(); - } - } - - // Destructor - inline ASTNode::~ASTNode() - { - if (_int_node_ptr) { - _int_node_ptr->DecRef(); - } - } -#else - // No refcounting - inline void ASTInternal::DecRef() - { - } - - // Destructor - inline ASTNode::~ASTNode() - { - }; -#endif - - inline BeevMgr& ASTNode::GetBeevMgr() const { return _int_node_ptr->_bm; } - - /*************************************************************************** - * Class BeevMgr. This holds all "global" variables for the system, such as - * unique tables for the various kinds of nodes. - ***************************************************************************/ - class BeevMgr { - friend class ASTNode; // ASTNode modifies AlreadyPrintedSet - // in BeevMgr - friend class ASTInterior; - friend class ASTBVConst; - friend class ASTSymbol; - - // FIXME: The values appear to be the same regardless of the value of SMTLIB - // initial hash table sizes, to save time on resizing. -#ifdef SMTLIB - static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100; - static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100; - - static const int INITIAL_SIMPLIFY_MAP_SIZE = 100; - static const int INITIAL_SOLVER_MAP_SIZE = 100; - static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; - static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; -#else - // these are the STL defaults - static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100; - static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100; - - static const int INITIAL_SIMPLIFY_MAP_SIZE = 100; - static const int INITIAL_SOLVER_MAP_SIZE = 100; - static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; - static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; -#endif - - private: - // Typedef for unique Interior node table. - typedef hash_set ASTInteriorSet; - - // Typedef for unique Symbol node (leaf) table. - typedef hash_set ASTSymbolSet; - - // Unique tables to share nodes whenever possible. - ASTInteriorSet _interior_unique_table; - //The _symbol_unique_table is also the symbol table to be used - //during parsing/semantic analysis - ASTSymbolSet _symbol_unique_table; - - //Typedef for unique BVConst node (leaf) table. - typedef hash_set ASTBVConstSet; - - //table to uniquefy bvconst - ASTBVConstSet _bvconst_unique_table; - - // type of memo table. - typedef hash_map ASTNodeToVecMap; - - typedef hash_map ASTNodeToSetMap; - - // Memo table for bit blasted terms. If a node has already been - // bitblasted, it is mapped to a vector of Boolean formulas for - // the bits. - - //OLD: ASTNodeToVecMap BBTermMemo; - ASTNodeMap BBTermMemo; - - // Memo table for bit blasted formulas. If a node has already - // been bitblasted, it is mapped to a node representing the - // bitblasted equivalent - ASTNodeMap BBFormMemo; - - //public: - // Get vector of Boolean formulas for sum of two - // vectors of Boolean formulas - void BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin); - // Increment - ASTVec BBInc(ASTVec& x); - // Add one bit to a vector of bits. - ASTVec BBAddOneBit(ASTVec& x, ASTNode cin); - // Bitwise complement - ASTVec BBNeg(const ASTVec& x); - // Unary minus - ASTVec BBUminus(const ASTVec& x); - // Multiply. - ASTVec BBMult(const ASTVec& x, const ASTVec& y); - // AND each bit of vector y with single bit b and return the result. - // (used in BBMult) - ASTVec BBAndBit(const ASTVec& y, ASTNode b); - // Returns ASTVec for result - y. This destroys "result". - void BBSub(ASTVec& result, const ASTVec& y); - // build ITE's (ITE cond then[i] else[i]) for each i. - ASTVec BBITE(const ASTNode& cond, - const ASTVec& thn, const ASTVec& els); - // Build a vector of zeros. - ASTVec BBfill(unsigned int width, ASTNode fillval); - // build an EQ formula - ASTNode BBEQ(const ASTVec& left, const ASTVec& right); - - // This implements a variant of binary long division. - // q and r are "out" parameters. rwidth puts a bound on the - // recursion depth. Unsigned only, for now. - void BBDivMod(const ASTVec &y, - const ASTVec &x, - ASTVec &q, - ASTVec &r, - unsigned int rwidth); - - // Return formula for majority function of three formulas. - ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c); - - // Internal bit blasting routines. - ASTNode BBBVLE(const ASTVec& x, const ASTVec& y, bool is_signed); - - // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. - ASTNode BBcompare(const ASTNode& form); - - // Left and right shift one. Writes into x. - void BBLShift(ASTVec& x); - void BBRShift(ASTVec& x); - - public: - // Simplifying create functions - ASTNode CreateSimpForm(Kind kind, ASTVec &children); - ASTNode CreateSimpForm(Kind kind, const ASTNode& child0); - ASTNode CreateSimpForm(Kind kind, - const ASTNode& child0, - const ASTNode& child1); - ASTNode CreateSimpForm(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2); - - ASTNode CreateSimpNot(const ASTNode& form); - - // These are for internal use only. - // FIXME: Find a way to make this local to SimpBool, so they're - // not in AST.h - ASTNode CreateSimpXor(const ASTNode& form1, - const ASTNode& form2); - ASTNode CreateSimpXor(ASTVec &children); - ASTNode CreateSimpAndOr(bool isAnd, - const ASTNode& form1, - const ASTNode& form2); - ASTNode CreateSimpAndOr(bool IsAnd, ASTVec &children); - ASTNode CreateSimpFormITE(const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2); - - - // Declarations of BitBlaster functions (BitBlast.cpp) - public: - // Adds or removes a NOT as necessary to negate a literal. - ASTNode Negate(const ASTNode& form); - - // Bit blast a bitvector term. The term must have a kind for a - // bitvector term. Result is a ref to a vector of formula nodes - // representing the boolean formula. - const ASTNode BBTerm(const ASTNode& term); - - const ASTNode BBForm(const ASTNode& formula); - - // Declarations of CNF conversion (ToCNF.cpp) - public: - // ToCNF converts a bit-blasted Boolean formula to Conjunctive - // Normal Form, suitable for many SAT solvers. Our CNF representation - // is an STL vector of STL vectors, for independence from any particular - // SAT solver's representation. There needs to be a separate driver to - // convert our clauselist to the representation used by the SAT solver. - // Currently, there is only one such solver and its driver is "ToSAT" - - // Datatype for clauses - typedef ASTVec * ClausePtr; - - // Datatype for Clauselists - typedef vector ClauseList; - - // Convert a Boolean formula to an equisatisfiable CNF formula. - ClauseList *ToCNF(const ASTNode& form); - - // Print function for debugging - void PrintClauseList(ostream& os, ClauseList& cll); - - // Free the clause list and all its clauses. - void DeleteClauseList(BeevMgr::ClauseList *cllp); - - // Map from formulas to representative literals, for debugging. - ASTNodeMap RepLitMap; - - private: - // Global for assigning new node numbers. - int _max_node_num; - - const ASTNode ASTFalse, ASTTrue, ASTUndefined; - - // I just did this so I could put it in as a fake return value in - // methods that return a ASTNode &, to make -Wall shut up. - ASTNode dummy_node; - - //BeevMgr Constructor, Destructor and other misc. functions - public: - - int NewNodeNum() { _max_node_num += 2; return _max_node_num; } - - // Table for DAG printing. - ASTNodeSet AlreadyPrintedSet; - - //Tables for Presentation language printing - - //Nodes seen so far - ASTNodeSet PLPrintNodeSet; - - //Map from ASTNodes to LetVars - ASTNodeMap NodeLetVarMap; - - //This is a vector which stores the Node to LetVars pairs. It - //allows for sorted printing, as opposed to NodeLetVarMap - std::vector > NodeLetVarVec; - - //a partial Map from ASTNodes to LetVars. Needed in order to - //correctly print shared subterms inside the LET itself - ASTNodeMap NodeLetVarMap1; - - //functions to lookup nodes from the memo tables. these should be - //private. - private: - //Destructively appends back_child nodes to front_child nodes. - //If back_child nodes is NULL, no appending is done. back_child - //nodes are not modified. Then it returns the hashed copy of the - //node, which is created if necessary. - ASTInterior *CreateInteriorNode(Kind kind, - ASTInterior *new_node, - // this is destructively modified. - const ASTVec & back_children = _empty_ASTVec); - - // Create unique ASTInterior node. - ASTInterior *LookupOrCreateInterior(ASTInterior *n); - - // Create unique ASTSymbol node. - ASTSymbol *LookupOrCreateSymbol(ASTSymbol& s); - - // Called whenever we want to make sure that the Symbol is - // declared during semantic analysis - bool LookupSymbol(ASTSymbol& s); - - // Called by ASTNode constructors to uniqueify ASTBVConst - ASTBVConst *LookupOrCreateBVConst(ASTBVConst& s); - - //Public functions for CreateNodes and Createterms - public: - // Create and return an ASTNode for a symbol - ASTNode CreateSymbol(const char * const name); - - // Create and return an ASTNode for a symbol - // Width is number of bits. - ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst); - ASTNode CreateZeroConst(unsigned int width); - ASTNode CreateOneConst(unsigned int width); - ASTNode CreateTwoConst(unsigned int width); - ASTNode CreateMaxConst(unsigned int width); - - // Create and return an ASTNode for a symbol - // Optional base was a problem because 0 could be an int or char *, - // so CreateBVConst was ambiguous. - ASTNode CreateBVConst(const char *strval, int base); - - //FIXME This is a dangerous function - ASTNode CreateBVConst(CBV bv, unsigned width); - - // Create and return an interior ASTNode - ASTNode CreateNode(Kind kind, const ASTVec &children = _empty_ASTVec); - - ASTNode CreateNode(Kind kind, - const ASTNode& child0, - const ASTVec &children = _empty_ASTVec); - - ASTNode CreateNode(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTVec &children = _empty_ASTVec); - - ASTNode CreateNode(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2, - const ASTVec &children = _empty_ASTVec); - - // Create and return an ASTNode for a term - inline ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTVec &children = _empty_ASTVec) { - if(!is_Term_kind(kind)) - FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); - ASTNode n = CreateNode(kind, children); - n.SetValueWidth(width); - - //by default we assume that the term is a Bitvector. If - //necessary the indexwidth can be changed later - n.SetIndexWidth(0); - return n; - } - - inline ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTVec &children = _empty_ASTVec) { - if(!is_Term_kind(kind)) - FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); - ASTNode n = CreateNode(kind, child0, children); - n.SetValueWidth(width); - return n; - } - - inline ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTNode& child1, - const ASTVec &children = _empty_ASTVec) { - if(!is_Term_kind(kind)) - FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); - ASTNode n = CreateNode(kind, child0, child1, children); - n.SetValueWidth(width); - return n; - } - - inline ASTNode CreateTerm(Kind kind, - unsigned int width, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2, - const ASTVec &children = _empty_ASTVec) { - if(!is_Term_kind(kind)) - FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); - ASTNode n = CreateNode(kind, child0, child1, child2, children); - n.SetValueWidth(width); - return n; - } - - ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg); - ASTNode SimplifyFormula_TopLevel(const ASTNode& a, bool pushNeg); - ASTNode SimplifyFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyTerm_TopLevel(const ASTNode& b); - ASTNode SimplifyTerm(const ASTNode& a); - void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); - private: - //memo table for simplifcation - ASTNodeMap SimplifyMap; - ASTNodeMap SimplifyNegMap; - ASTNodeMap SolverMap; - ASTNodeSet AlwaysTrueFormMap; - ASTNodeMap MultInverseMap; - - public: - ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg); - ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2); - ASTNode ITEOpt_InEqs(const ASTNode& in1); - ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3); - ASTNode CreateSimplifiedINEQ(Kind k, const ASTNode& a0, const ASTNode& a1, bool pushNeg); - ASTNode SimplifyNotFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyAndOrFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyXorFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyNandFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyNorFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyImpliesFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyIffFormula(const ASTNode& a, bool pushNeg); - ASTNode SimplifyIteFormula(const ASTNode& a, bool pushNeg); - ASTNode FlattenOneLevel(const ASTNode& a); - ASTNode FlattenAndOr(const ASTNode& a); - ASTNode CombineLikeTerms(const ASTNode& a); - ASTNode LhsMinusRhs(const ASTNode& eq); - ASTNode DistributeMultOverPlus(const ASTNode& a, - bool startdistribution=false); - ASTNode ConvertBVSXToITE(const ASTNode& a); - //checks if the input constant is odd or not - bool BVConstIsOdd(const ASTNode& c); - //computes the multiplicatve inverse of the input - ASTNode MultiplicativeInverse(const ASTNode& c); - - void ClearAllTables(void); - void ClearAllCaches(void); - int BeforeSAT_ResultCheck(const ASTNode& q); - int CallSAT_ResultCheck(MINISAT::Solver& newS, - const ASTNode& q, const ASTNode& orig_input); - int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, - const ASTNode& q, const ASTNode& orig_input); - int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); - //creates array write axiom only for the input term or formula, if - //necessary. If there are no axioms to produce then it simply - //generates TRUE - ASTNode Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, const ASTNode& array_newname); - ASTVec ArrayWrite_RemainingAxioms; - //variable indicates that counterexample will now be checked by - //the counterexample checker, and hence simplifyterm must switch - //off certain optimizations. In particular, array write - //optimizations - bool start_abstracting; - bool Begin_RemoveWrites; - bool SimplifyWrites_InPlace_Flag; - - void CopySolverMap_To_CounterExample(void); - //int LinearSearch(const ASTNode& orig_input); - //Datastructures and functions needed for counterexample - //generation, and interface with MINISAT - private: - /* MAP: This is a map from ASTNodes to MINISAT::Vars. - * - * The map is populated while ASTclauses are read from the AST - * ClauseList returned by CNF converter. For every new boolean - * variable in ASTClause a new MINISAT::Var is created (these vars - * typedefs for ints) - */ - typedef hash_map ASTtoSATMap; - ASTtoSATMap _ASTNode_to_SATVar; - - public: - //converts the clause to SAT and calls SAT solver - bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll); - - ///print SAT solver statistics - void PrintStats(MINISAT::SolverStats& stats); - - //accepts query and returns the answer. if query is valid, return - //true, else return false. Automatically constructs counterexample - //for invalid queries, and prints them upon request. - int TopLevelSAT(const ASTNode& query, const ASTNode& asserts); - - // Debugging function to find problems in BitBlast and ToCNF. - // See body in ToSAT.cpp for more explanation. - ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form); - - // Internal recursive body of above. - ASTNode CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form); - - // Helper function for CheckBBandCNF - ASTNode SymbolTruthValue(MINISAT::Solver &newS, ASTNode form); - - //looksup a MINISAT var from the minisat-var memo-table. if none - //exists, then creates one. - MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n); - - // Memo table for CheckBBandCNF debugging function - ASTNodeMap CheckBBandCNFMemo; - - - //Data structures for Array Read Transformations - private: - /* MAP: This is a map from Array Names to list of array-read - * indices in the input. This map is used by the TransformArray() - * function - * - * This map is useful in converting array reads into nested ITE - * constructs. Suppose there are two array reads in the input - * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a - * symbolic constant, say v1, and Read(A,j) is replaced with the - * following ITE: - * - * ITE(i=j,v1,v2) - */ - //CAUTION: I tried using a set instead of vector for - //readindicies. for some odd reason the performance went down - //considerably. this is totally inexplicable. - ASTNodeToVecMap _arrayname_readindices; - - /* MAP: This is a map from Array Names to nested ITE constructs, - * which are built as described below. This map is used by the - * TransformArray() function - * - * This map is useful in converting array reads into nested ITE - * constructs. Suppose there are two array reads in the input - * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a - * symbolic constant, say v1, and Read(A,j) is replaced with the - * following ITE: - * - * ITE(i=j,v1,v2) - */ - ASTNodeMap _arrayread_ite; - - /*MAP: This is a map from array-reads to symbolic constants. This - *map is used by the TransformArray() - */ - ASTNodeMap _arrayread_symbol; - - ASTNodeSet _introduced_symbols; - - /*Memoization map for TransformFormula/TransformTerm/TransformArray function - */ - ASTNodeMap TransformMap; - - //count to keep track of new symbolic constants introduced - //corresponding to Array Reads - unsigned int _symbol_count; - - //Formula/Term Transformers. Let Expr Manager, Type Checker - public: - //Functions that Transform ASTNodes - ASTNode TransformFormula(const ASTNode& query); - ASTNode TransformTerm(const ASTNode& term); - ASTNode TransformArray(const ASTNode& term); - ASTNode TranslateSignedDivMod(const ASTNode& term); - - //LET Management - private: - // MAP: This map is from bound IDs that occur in LETs to - // expression. The map is useful in checking replacing the IDs - // with the corresponding expressions. - ASTNodeMap _letid_expr_map; - public: - - ASTNode ResolveID(const ASTNode& var); - - //Functions that are used to manage LET expressions - void LetExprMgr(const ASTNode& var, const ASTNode& letExpr); - - //Delete Letid Map - void CleanupLetIDMap(void); - - //Allocate LetID map - void InitializeLetIDMap(void); - - //Substitute Let-vars with LetExprs - ASTNode SubstituteLetExpr(ASTNode inExpr); - - /* MAP: This is a map from MINISAT::Vars to ASTNodes - * - * This is a reverse map, useful in constructing - * counterexamples. MINISAT returns a model in terms of MINISAT - * Vars, and this map helps us convert it to a model over ASTNode - * variables. - */ - vector _SATVar_to_AST; - - private: - /* MAP: This is a map from ASTNodes to vectors of bits - * - * This map is used in constructing and printing - * counterexamples. MINISAT returns values for each bit (a - * BVGETBIT Node), and this maps allows us to assemble the bits - * into bitvectors. - */ - typedef hash_map *, - ASTNode::ASTNodeHasher, - ASTNode::ASTNodeEqual> ASTtoBitvectorMap; - ASTtoBitvectorMap _ASTNode_to_Bitvector; - - //Data structure that holds the counter-model - ASTNodeMap CounterExampleMap; - - //Checks if the counter_example is ok. In order for the - //counter_example to be ok, Every assert must evaluate to true - //w.r.t couner_example and the query must evaluate to - //false. Otherwise the counter_example is bogus. - void CheckCounterExample(bool t); - - //Converts a vector of bools to a BVConst - ASTNode BoolVectoBVConst(hash_map * w, unsigned int l); - - //accepts a term and turns it into a constant-term w.r.t counter_example - ASTNode TermToConstTermUsingModel(const ASTNode& term, bool ArrayReadFlag = true); - ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool ArrayReadFlag = true); - //Computes the truth value of a formula w.r.t counter_example - ASTNode ComputeFormulaUsingModel(const ASTNode& form); - - //Replaces WRITE(Arr,i,val) with ITE(j=i, val, READ(Arr,j)) - ASTNode RemoveWrites_TopLevel(const ASTNode& term); - ASTNode RemoveWrites(const ASTNode& term); - ASTNode SimplifyWrites_InPlace(const ASTNode& term); - ASTNode ReadOverWrite_To_ITE(const ASTNode& term); - - ASTNode NewArrayVar(unsigned int index, unsigned int value); - ASTNode NewVar(unsigned int valuewidth); - //For ArrayWrite Abstraction: map from read-over-write term to - //newname. - ASTNodeMap ReadOverWrite_NewName_Map; - //For ArrayWrite Refinement: Map new arraynames to Read-Over-Write - //terms - ASTNodeMap NewName_ReadOverWrite_Map; - - public: - //print the STP solver output - void PrintOutput(bool true_iff_valid); - - //Converts MINISAT counterexample into an AST memotable (i.e. the - //function populates the datastructure CounterExampleMap) - void ConstructCounterExample(MINISAT::Solver& S); - - //Prints the counterexample to stdout - void PrintCounterExample(bool t,std::ostream& os=cout); - - //Prints the counterexample to stdout - void PrintCounterExample_InOrder(bool t); - - //queries the counterexample, and returns the value corresponding - //to e - ASTNode GetCounterExample(bool t, const ASTNode& e); - - int CounterExampleSize(void) const {return CounterExampleMap.size();} - - //FIXME: This is bloody dangerous function. Hack attack to take - //care of requests from users who want to store complete - //counter-examples in their own data structures. - ASTNodeMap GetCompleteCounterExample() {return CounterExampleMap;} - - // prints MINISAT assigment one bit at a time, for debugging. - void PrintSATModel(MINISAT::Solver& S); - - //accepts constant input and normalizes it. - ASTNode BVConstEvaluator(const ASTNode& t); - - //FUNCTION TypeChecker: Assumes that the immediate Children of the - //input ASTNode have been typechecked. This function is suitable - //in scenarios like where you are building the ASTNode Tree, and - //you typecheck as you go along. It is not suitable as a general - //typechecker - void BVTypeCheck(const ASTNode& n); - - private: - //stack of Logical Context. each entry in the stack is a logical - //context. A logical context is a vector of assertions. The - //logical context is represented by a ptr to a vector of - //assertions in that logical context. Logical contexts are created - //by PUSH/POP - std::vector _asserts; - //The query for the current logical context. - ASTNode _current_query; - - //this flag, when true, indicates that counterexample is being - //checked by the counterexample checker - bool counterexample_checking_during_refinement; - - //this flag indicates as to whether the input has been determined to - //be valid or not by this tool - bool ValidFlag; - - //this flag, when true, indicates that a BVDIV divide by zero - //exception occured. However, the program must not exit with a - //fatalerror. Instead, it should evaluate the whole formula (which - //contains the BVDIV term) to be FALSE. - bool bvdiv_exception_occured; - - public: - //set of functions that manipulate Logical Contexts. - // - //add an assertion to the current logical context - void AddAssert(const ASTNode& assert); - void Push(void); - void Pop(void); - void AddQuery(const ASTNode& q); - const ASTNode PopQuery(); - const ASTNode GetQuery(); - const ASTVec GetAsserts(void); - - //reports node size. Second arg is "clearstatinfo", whatever that is. - unsigned int NodeSize(const ASTNode& a, bool t = false); - - private: - //This memo map is used by the ComputeFormulaUsingModel() - ASTNodeMap ComputeFormulaMap; - //Map for statiscal purposes - ASTNodeSet StatInfoSet; - - - ASTNodeMap TermsAlreadySeenMap; - ASTNode CreateSubstitutionMap(const ASTNode& a); - public: - //prints statistics for the ASTNode. can add a prefix string c - void ASTNodeStats(const char * c, const ASTNode& a); - - //substitution - bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); - bool CheckSubstitutionMap(const ASTNode& a); - bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); - //if (a > b) in the termorder, then return 1 - //elseif (a < b) in the termorder, then return -1 - //else return 0 - int TermOrder(const ASTNode& a, const ASTNode& b); - //fill the arrayname_readindices vector if e0 is a READ(Arr,index) - //and index is a BVCONST - void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1); - bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); - - //functions for checking and updating simplifcation map - bool CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg); - void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg); - bool CheckAlwaysTrueFormMap(const ASTNode& key); - void UpdateAlwaysTrueFormMap(const ASTNode& val); - bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); - void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); - - //Map for solved variables - bool CheckSolverMap(const ASTNode& a, ASTNode& output); - bool CheckSolverMap(const ASTNode& a); - bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); - public: - //FIXME: HACK_ATTACK. this vector was hacked into the code to - //support a special request by Dawson' group. They want the - //counterexample to be printed in the order of variables declared. - //TO BE COMMENTED LATER (say by 1st week of march,2006) - ASTVec _special_print_set; - - //prints the initial activity levels of variables - void PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS); - - //this function biases the activity levels of MINISAT variables. - void ChangeActivityLevels_Of_SATVars(MINISAT::Solver& n); - - // Constructor - BeevMgr() : _interior_unique_table(INITIAL_INTERIOR_UNIQUE_TABLE_SIZE), - _symbol_unique_table(INITIAL_SYMBOL_UNIQUE_TABLE_SIZE), - _bvconst_unique_table(INITIAL_BVCONST_UNIQUE_TABLE_SIZE), - BBTermMemo(INITIAL_BBTERM_MEMO_TABLE_SIZE), - BBFormMemo(INITIAL_BBFORM_MEMO_TABLE_SIZE), - _max_node_num(0), - ASTFalse(CreateNode(FALSE)), - ASTTrue(CreateNode(TRUE)), - ASTUndefined(CreateNode(UNDEFINED)), - SimplifyMap(INITIAL_SIMPLIFY_MAP_SIZE), - SimplifyNegMap(INITIAL_SIMPLIFY_MAP_SIZE), - SolverMap(INITIAL_SOLVER_MAP_SIZE), - _arrayread_symbol(INITIAL_ARRAYREAD_SYMBOL_SIZE), - _introduced_symbols(INITIAL_INTRODUCED_SYMBOLS_SIZE), - _symbol_count(0) { - _current_query = ASTUndefined; - ValidFlag = false; - bvdiv_exception_occured = false; - counterexample_checking_during_refinement = false; - start_abstracting = false; - Begin_RemoveWrites = false; - SimplifyWrites_InPlace_Flag = false; - }; - - //destructor - ~BeevMgr(); - }; //End of Class BeevMgr - - - class CompleteCounterExample { - ASTNodeMap counterexample; - BeevMgr * bv; - public: - CompleteCounterExample(ASTNodeMap a, BeevMgr* beev) : counterexample(a), bv(beev){} - ASTNode GetCounterExample(ASTNode e) { - if(BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind()) { - FatalError("You must input a term or propositional variables\n",e); - } - if(counterexample.find(e) != counterexample.end()) { - return counterexample[e]; - } - else { - if(SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType()) { - return bv->CreateNode(BEEV::FALSE); - } - - if(SYMBOL == e.GetKind()) { - ASTNode z = bv->CreateZeroConst(e.GetValueWidth()); - return z; - } - - return e; - } - } - }; - -} // end namespace BEEV -#endif diff --git a/stp/AST/ASTKind.cpp b/stp/AST/ASTKind.cpp deleted file mode 100644 index 9a2392c9..00000000 --- a/stp/AST/ASTKind.cpp +++ /dev/null @@ -1,118 +0,0 @@ -// Generated automatically by genkinds.h from ASTKind.kinds Sun Apr 4 19:39:09 2010. -// Do not edit -namespace BEEV { -const char * _kind_names[] = { - "UNDEFINED", - "SYMBOL", - "BVCONST", - "BVNEG", - "BVCONCAT", - "BVOR", - "BVAND", - "BVXOR", - "BVNAND", - "BVNOR", - "BVXNOR", - "BVEXTRACT", - "BVLEFTSHIFT", - "BVRIGHTSHIFT", - "BVSRSHIFT", - "BVVARSHIFT", - "BVPLUS", - "BVSUB", - "BVUMINUS", - "BVMULTINVERSE", - "BVMULT", - "BVDIV", - "BVMOD", - "SBVDIV", - "SBVMOD", - "BVSX", - "BOOLVEC", - "ITE", - "BVGETBIT", - "BVLT", - "BVLE", - "BVGT", - "BVGE", - "BVSLT", - "BVSLE", - "BVSGT", - "BVSGE", - "EQ", - "NEQ", - "FALSE", - "TRUE", - "NOT", - "AND", - "OR", - "NAND", - "NOR", - "XOR", - "IFF", - "IMPLIES", - "READ", - "WRITE", - "ARRAY", - "BITVECTOR", - "BOOLEAN", -}; - -unsigned char _kind_categories[] = { - 0, - 3, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 1, - 3, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 2, - 1, - 1, - 0, - 0, - 0, -}; - -} // end namespace diff --git a/stp/AST/ASTKind.h b/stp/AST/ASTKind.h deleted file mode 100644 index 2480b6e6..00000000 --- a/stp/AST/ASTKind.h +++ /dev/null @@ -1,79 +0,0 @@ -// -*- c++ -*- -#ifndef TESTKINDS_H -#define TESTKINDS_H -// Generated automatically by genkinds.pl from ASTKind.kinds Sun Apr 4 19:39:09 2010. -// Do not edit -namespace BEEV { - typedef enum { - UNDEFINED, - SYMBOL, - BVCONST, - BVNEG, - BVCONCAT, - BVOR, - BVAND, - BVXOR, - BVNAND, - BVNOR, - BVXNOR, - BVEXTRACT, - BVLEFTSHIFT, - BVRIGHTSHIFT, - BVSRSHIFT, - BVVARSHIFT, - BVPLUS, - BVSUB, - BVUMINUS, - BVMULTINVERSE, - BVMULT, - BVDIV, - BVMOD, - SBVDIV, - SBVMOD, - BVSX, - BOOLVEC, - ITE, - BVGETBIT, - BVLT, - BVLE, - BVGT, - BVGE, - BVSLT, - BVSLE, - BVSGT, - BVSGE, - EQ, - NEQ, - FALSE, - TRUE, - NOT, - AND, - OR, - NAND, - NOR, - XOR, - IFF, - IMPLIES, - READ, - WRITE, - ARRAY, - BITVECTOR, - BOOLEAN -} Kind; - -extern unsigned char _kind_categories[]; - -inline bool is_Term_kind(Kind k) { return (_kind_categories[k] & 1); } - -inline bool is_Form_kind(Kind k) { return (_kind_categories[k] & 2); } - -extern const char *_kind_names[]; - -/** Prints symbolic name of kind */ -inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; } - - -} // end namespace - - -#endif diff --git a/stp/AST/ASTKind.kinds b/stp/AST/ASTKind.kinds deleted file mode 100644 index 03112eb8..00000000 --- a/stp/AST/ASTKind.kinds +++ /dev/null @@ -1,71 +0,0 @@ -#Please refer LICENSE FILE in the home directory for licensing information -# name minkids maxkids cat1 cat2 ... -Categories: Term Form - -# Leaf nodes. -UNDEFINED 0 0 -SYMBOL 0 0 Term Form - -# These always produce terms -BVCONST 0 0 Term -BVNEG 1 1 Term -BVCONCAT 2 - Term -BVOR 1 - Term -BVAND 1 - Term -BVXOR 1 - Term -BVNAND 1 - Term -BVNOR 1 - Term -BVXNOR 1 - Term -BVEXTRACT 3 3 Term -BVLEFTSHIFT 3 3 Term -BVRIGHTSHIFT 3 3 Term -BVSRSHIFT 3 3 Term -BVVARSHIFT 3 3 Term -BVPLUS 1 - Term -BVSUB 2 2 Term -BVUMINUS 1 1 Term -BVMULTINVERSE 1 1 Term -BVMULT 1 - Term -BVDIV 2 2 Term -BVMOD 2 2 Term -SBVDIV 2 2 Term -SBVMOD 2 2 Term -BVSX 1 1 Term -BOOLVEC 0 - Term - -# Formula OR term, depending on context -ITE 3 3 Term Form - -# These produce formulas. -BVGETBIT 2 2 Form -BVLT 2 2 Form -BVLE 2 2 Form -BVGT 2 2 Form -BVGE 2 2 Form -BVSLT 2 2 Form -BVSLE 2 2 Form -BVSGT 2 2 Form -BVSGE 2 2 Form -EQ 2 2 Form -NEQ 2 2 Form -FALSE 0 0 Form -TRUE 0 0 Form -NOT 1 1 Form -AND 1 - Form -OR 1 - Form -NAND 1 - Form -NOR 1 - Form -XOR 1 - Form -IFF 1 - Form -IMPLIES 2 2 Form - -# array operations -READ 2 2 Term -WRITE 3 3 Term - -#Types: These kinds are used only in the API. Once processed inside -#the API, they are never used again in the system -ARRAY 0 0 -BITVECTOR 0 0 -BOOLEAN 0 0 - diff --git a/stp/AST/ASTUtil.cpp b/stp/AST/ASTUtil.cpp deleted file mode 100644 index ecb54a4a..00000000 --- a/stp/AST/ASTUtil.cpp +++ /dev/null @@ -1,45 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -#include "ASTUtil.h" -#include - -namespace BEEV { - ostream &operator<<(ostream &os, const Spacer &sp) { - // Instead of wrapping lines with hundreds of spaces, prints - // a "+" at the beginning of the line for each wrap-around. - // so lines print like: +14+ (XOR ... - int blanks = sp._spaces % 60; - int wraps = sp._spaces / 60; - if (wraps > 0) { - os << "+" << wraps; - } - for (int i = 0; i < blanks; i++) - os << " "; - return os; - } - - //this function accepts the name of a function (as a char *), and - //records some stats about it. if the input is "print_func_stats", - //the function will then print the stats that it has collected. - void CountersAndStats(const char * functionname) { - if(!stats) - return; - static function_counters s; - - if(!strcmp(functionname,"print_func_stats")) { - cout << endl; - for(hash_map,eqstr>::iterator it=s.begin(),itend=s.end(); - it!=itend;it++) - cout << "Number of times the function: " << it->first << ": is called: " << it->second << endl; - return; - } - s[functionname] += 1; - } -} // end of namespace diff --git a/stp/AST/ASTUtil.h b/stp/AST/ASTUtil.h deleted file mode 100644 index c90ee0ce..00000000 --- a/stp/AST/ASTUtil.h +++ /dev/null @@ -1,107 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -#ifndef ASTUTIL_H -#define ASTUTIL_H - -#include -#include -#include -#ifdef EXT_HASH_MAP -#include -#include -#else -#include -#include -#endif - -using namespace std; -namespace BEEV { -#ifdef EXT_HASH_MAP - using namespace __gnu_cxx; -#endif - //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 - extern bool stats; - //print DAG nodes - extern bool print_nodes; - //tentative global var to allow for variable activity optimization - //in the SAT solver. deprecated. - extern bool variable_activity_optimize; - //run STP in optimized mode - extern bool optimize; - //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. - extern bool arrayread_refinement; - //switch to control write refinements - extern bool arraywrite_refinement; - //check the counterexample against the original input to STP - extern bool check_counterexample; - //construct the counterexample in terms of original variable based - //on the counterexample returned by SAT solver - extern bool construct_counterexample; - extern bool print_counterexample; - //if this option is true then print the way dawson wants using a - //different printer. do not use this printer. - extern bool print_arrayval_declaredorder; - //flag to decide whether to print "valid/invalid" or not - extern bool print_output; - //do linear search in the array values of an input array. experimental - extern bool linear_search; - //print the variable order chosen by the sat solver while it is - //solving. - extern bool print_sat_varorder; - //turn on word level bitvector solver - extern bool wordlevel_solve; - //XOR flattening optimizations. - extern bool xor_flatten; - //this flag indicates that the BVSolver() succeeded - extern bool toplevel_solved; - //the smtlib parser has been turned on - extern bool smtlib_parser_enable; - //print the input back - extern bool print_STPinput_back; - - extern void (*vc_error_hdlr)(const char* err_msg); - /*Spacer class is basically just an int, but the new class allows - overloading of << with a special definition that prints the int as - that many spaces. */ - class Spacer { - public: - int _spaces; - Spacer(int spaces) { _spaces = spaces; } - friend ostream& operator<<(ostream& os, const Spacer &ind); - }; - - inline Spacer spaces(int width) { - Spacer sp(width); - return sp; - } - - struct eqstr { - bool operator()(const char* s1, const char* s2) const { - return strcmp(s1, s2) == 0; - } - }; - - typedef hash_map,eqstr> function_counters; - void CountersAndStats(const char * functionname); - - //global function which accepts an integer and looks up the - //corresponding ASTNode and prints a char* of that ASTNode - void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, - int decision, int polarity=0); -} // end namespace. -#endif diff --git a/stp/AST/BitBlast.cpp b/stp/AST/BitBlast.cpp deleted file mode 100644 index de78ec74..00000000 --- a/stp/AST/BitBlast.cpp +++ /dev/null @@ -1,812 +0,0 @@ -/******************************************************************** - * AUTHORS: David L. Dill, Vijay Ganesh - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -// BitBlast -- convert bitvector terms and formulas to boolean -// formulas. A term is something that can represent a multi-bit -// bitvector, such as BVPLUS or BVXOR (or a BV variable or constant). -// A formula (form) represents a boolean value, such as EQ or BVLE. -// Bit blasting a term representing an n-bit bitvector with BBTerm -// yields a vector of n boolean formulas (returning ASTVec). -// Bit blasting a formula returns a single boolean formula (type ASTNode). - -// A bitblasted term is a vector of ASTNodes for formulas. -// The 0th element of the vector corresponds to bit 0 -- the low-order bit. - -#include "AST.h" -namespace BEEV { - // extern void lpvec(ASTVec &vec); - -// FIXME: Assert no zero-length bit vectors!!! -// FIXME: Need top-level functions that create and destroy the memo tables. -// FIXME: Check resource limits and generate an exception when exceeded. -// FIXME: THis does a lot of unnecessary copying of vectors. -// Had to be careful not to modify memoized vectors! -// FIXME: Might be some redundant variables. - -// accepts a term, and returns a vector of bitblasted bits(ASTVec) - -ASTNode ASTJunk; -const ASTNode BeevMgr::BBTerm(const ASTNode& term) { - //CHANGED TermMemo is now an ASTNodeMap. Based on BBFormMemo - ASTNodeMap::iterator it = BBTermMemo.find(term); - if (it != BBTermMemo.end()) { - // already there. Just return it. - return it->second; - } - -// ASTNode& result = ASTJunk; - ASTNode result; - - Kind k = term.GetKind(); - if (!is_Term_kind(k)) - FatalError("BBTerm: Illegal kind to BBTerm",term); - - ASTVec::const_iterator kids_end = term.end(); - unsigned int num_bits = term.GetValueWidth(); - switch (k) { - case BVNEG: { - // bitwise complement - // bitblast the child. - //FIXME Uses a tempory const ASTNode - const ASTNode& bbkids = BBTerm(term[0]); - result = CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren())); - break; - } - case BVSRSHIFT: - case BVVARSHIFT: - FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term); - break; - case ITE: { - // Term version of ITE. - - // Blast the args - // FIXME Uses temporary const ASTNodes and an ASTVec& - const ASTNode& cond = BBForm(term[0]); - const ASTNode& thn = BBTerm(term[1]); - const ASTNode& els = BBTerm(term[2]); - result = - CreateNode(BOOLVEC, BBITE(cond, thn.GetChildren(), els.GetChildren())); - break; - } - case BVSX: { - // Replicate high-order bit as many times as necessary. - // Arg 0 is expression to be sign extended. - const ASTNode& arg = term[0]; - unsigned long result_width = term.GetValueWidth(); - unsigned long arg_width = arg.GetValueWidth(); - //FIXME Uses a temporary const ASTNode reference - const ASTNode& bbarg = BBTerm(arg); - - if (result_width == arg_width) { - //nothing to sign extend - break; - } - else { - //we need to sign extend - const ASTNode& msbX = bbarg.back(); - //const ASTNode& msb1 = msbX; - - ASTVec ccc = msbX.GetChildren(); - const ASTNode& msb = CreateSimpForm(msbX.GetKind(),ccc); - - // Old version - // ASTNode msb = bbarg.back(); - // const ASTNode msb1 = msb; - - // ASTVec ccc = msb.GetChildren(); - // msb = CreateSimpForm(msb.GetKind(),ccc); - - // DD 1/14/07 Simplify silently drops all but first two args of XOR. - // I expanded XOR to N args with flattening optimization. - // This bug took 2 days to track down! - - // msb = SimplifyFormula(msb,false); - - // cout << "!!!!!!!!!!!!!!!!" << endl - // << "Simplify msb:" << msb2 << endl - // << "Simplify result:" << msb << endl; - - //FIXME Dynamically allocate the result vector? - //Is this doing multiple copies? - //ASTVec& tmp_res = *(new ASTVec(result_width)); - ASTVec tmp_res(result_width); - - //FIXME Should these be gotten from result? - ASTVec::const_iterator bb_it = bbarg.begin(); - ASTVec::iterator res_it = tmp_res.begin(); - ASTVec::iterator res_ext = res_it+arg_width; // first bit of extended part - ASTVec::iterator res_end = tmp_res.end(); - // copy LSBs directly from bbvec - for( ; res_it < res_ext; (res_it++, bb_it++)) { - *res_it = *bb_it; - } - // repeat MSB to fill up rest of result. - for( ; res_it < res_end; (res_it++, bb_it++)) { - *res_it = msb; - } - - //Temporary debugging code - // cout << "Sign extending:" << endl - // << " Vec "; - // lpvec( bbarg.GetChildren() ); - // cout << " Extended to "; - // lp(result); - // cout << endl; - - result = CreateNode(BOOLVEC, tmp_res); - - break; - } - } - case BVEXTRACT: { - // bitblast the child, then extract the relevant bits. - // Note: This could be optimized by not bitblasting the bits - // that aren't fetched. But that would be tricky, especially - // with memo-ization. - - //FIXME Using const ASTNode w/out reference - const ASTNode& bbkids = BBTerm(term[0]); - unsigned int high = GetUnsignedConst(term[1]); - unsigned int low = GetUnsignedConst(term[2]); - - ASTVec::const_iterator bbkfit = bbkids.begin(); - // I should have used pointers to ASTVec, to avoid this crock - - //FIXME Creates a new local ASTVec and does the CreateNode from that - result = CreateNode(BOOLVEC, ASTVec(bbkfit+low, bbkfit+high+1)); - break; - } - case BVCONCAT: { - //FIXME Using temporary const ASTNodes - const ASTNode& vec1 = BBTerm(term[0]); - const ASTNode& vec2 = BBTerm(term[1]); - - //FIXME This has to be an unnessecary copy and a memory leak - //Leaking ASTVec tmp_res = *(new ASTVec(vec2.GetChildren())); - ASTVec tmp_res(vec2.GetChildren()); - tmp_res.insert(tmp_res.end(), vec1.begin(), vec1.end()); - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BVPLUS: { - // ASSERT: at least one child. - // ASSERT: all children and result are the same size. - // Previous phase must make sure this is true. - // Add children pairwise and accumulate in BBsum - - // FIXME: Unnecessary array copies. - ASTVec::const_iterator it = term.begin(); - ASTVec tmp_res = BBTerm(*it).GetChildren(); - for (++it; it < kids_end; it++) { - const ASTVec& tmp = BBTerm(*it).GetChildren(); - BBPlus2(tmp_res, tmp, ASTFalse); - } - - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BVUMINUS: { - //FIXME Using const ASTNode reference - const ASTNode& bbkid = BBTerm(term[0]); - result = CreateNode(BOOLVEC, BBUminus(bbkid.GetChildren())); - break; - } - case BVSUB: { - // complement of subtrahend - // copy, since BBSub writes into it. - - //FIXME: Unnecessary array copies? - ASTVec tmp_res = BBTerm(term[0]).GetChildren(); - - const ASTVec& bbkid1 = BBTerm(term[1]).GetChildren(); - BBSub(tmp_res, bbkid1); - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BVMULT: { - // ASSERT 2 arguments, same length, result is same length. - - const ASTNode& t0 = term[0]; - const ASTNode& t1 = term[1]; - - const ASTNode& mpcd1 = BBTerm(t0); - const ASTNode& mpcd2 = BBTerm(t1); - //Reverese the order of the nodes w/out the need for temporaries - //This is needed because t0 an t1 must be const - if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) { - result = CreateNode(BOOLVEC, - BBMult(mpcd2.GetChildren(), mpcd1.GetChildren()) ); - }else{ - result = CreateNode(BOOLVEC, - BBMult(mpcd1.GetChildren(), mpcd2.GetChildren()) ); - } - break; - } - case BVDIV: - case BVMOD: { - const ASTNode& dvdd = BBTerm(term[0]); - const ASTNode& dvsr = BBTerm(term[1]); - unsigned int width = dvdd.Degree(); - ASTVec q(width); - ASTVec r(width); - BBDivMod(dvdd.GetChildren(), dvsr.GetChildren(), q, r, width); - if (k == BVDIV) - result = CreateNode(BOOLVEC, q); - else - result = CreateNode(BOOLVEC, r); - break; - } - // n-ary bitwise operators. - case BVXOR: - case BVXNOR: - case BVAND: - case BVOR: - case BVNOR: - case BVNAND: { - // Add children pairwise and accumulate in BBsum - ASTVec::const_iterator it = term.begin(); - Kind bk = UNDEFINED; // Kind of individual bit op. - switch (k) { - case BVXOR: bk = XOR; break; - case BVXNOR: bk = IFF; break; - case BVAND: bk = AND; break; - case BVOR: bk = OR; break; - case BVNOR: bk = NOR; break; - case BVNAND: bk = NAND; break; - default: - FatalError("BBTerm: Illegal kind to BBTerm",term); - break; - } - - // Sum is destructively modified in the loop, so make a copy of value - // returned by BBTerm. - ASTNode temp = BBTerm(*it); - ASTVec sum(temp.GetChildren()); // First operand. - - // Iterate over remaining bitvector term operands - for (++it; it < kids_end; it++) { - //FIXME FIXME FIXME: Why does using a temp. var change the behavior? - temp = BBTerm(*it); - const ASTVec& y = temp.GetChildren(); - - // Iterate over bits - // FIXME: Why is this not using an iterator??? - int n = y.size(); - for (int i = 0; i < n; i++) { - sum[i] = CreateSimpForm(bk, sum[i], y[i]); - } - } - result = CreateNode(BOOLVEC, sum); - break; - } - case SYMBOL: { - // ASSERT: IndexWidth = 0? Semantic analysis should check. - //Leaking ASTVec& bbvec = *(new ASTVec); - - //FIXME Why is isn't this ASTVEC bbvec(num_bits) ? - ASTVec bbvec; - 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); - break; - } - case BVCONST: { - ASTVec tmp_res(num_bits); -#ifndef NATIVE_C_ARITH - CBV bv = term.GetBVConst(); - for(unsigned int i = 0; i < num_bits; i++){ - tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv,i) ? ASTTrue : ASTFalse; - } -#else - const unsigned long long int c = term.GetBVConst(); - unsigned long long int bitmask = 0x00000000000000001LL; - for (unsigned int i = 0; i < num_bits; i++, bitmask <<= 1) - tmp_res[i] = ((c & (bitmask)) ? ASTTrue : ASTFalse); -#endif - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BOOLVEC: { - cerr << "Hit a boolvec! what to do?" << endl; - break; - } - default: - FatalError("BBTerm: Illegal kind to BBTerm",term); - } - - //if(result == ASTJunk) - // cout<<"result does not change"<second; - } - - ASTNode result = ASTUndefined; - - Kind k = form.GetKind(); - if (!is_Form_kind(k)) { - FatalError("BBForm: Illegal kind: ",form); - } - - // Not returning until end, and memoizing everything, makes it easier - // to trace coherently. - - // Various special cases - switch (k) { - case TRUE: - case FALSE: { - result = form; - break; - } - - case SYMBOL: - if (form.GetType() != BOOLEAN_TYPE) { - FatalError("BBForm: Symbol represents more than one bit", form); - } - - result = form; - break; - - case BVGETBIT: { - // exactly two children - const ASTNode bbchild = BBTerm(form[0]); - unsigned int index = GetUnsignedConst(form[1]); - result = bbchild[index]; - break; - } - - case NOT: - result = CreateSimpNot(BBForm(form[0])); - break; - - case ITE: - // FIXME: SHould this be CreateSimpITE? - result = CreateNode(ITE, BBForm(form[0]), BBForm(form[1]), BBForm(form[2])); - break; - - case AND: - case OR: - case NAND: - case NOR: - case IFF: - case XOR: - case IMPLIES: { - ASTVec bbkids; // bit-blasted children (formulas) - - // FIXME: Put in fast exits for AND/OR/NAND/NOR/IMPLIES - ASTVec::const_iterator kids_end = form.end(); - for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) { - bbkids.push_back(BBForm(*it)); - } - result = CreateSimpForm(k, bbkids); - break; - } - - case NEQ: { - ASTNode bbkid = BBForm(CreateNode(EQ, form.GetChildren())); - result = CreateSimpNot(bbkid); - break; - } - - case EQ: { - // Common code for binary operations - // FIXME: This ought to be in a semantic analysis phase. - const ASTNode left = BBTerm(form[0]); - const ASTNode right = BBTerm(form[1]); - if (left.Degree() != right.Degree()) { - cerr << "BBForm: Size mismatch" << endl << form[0] << endl << form[1] << endl; - FatalError("",ASTUndefined); - } - result = BBEQ(left.GetChildren(), right.GetChildren()); - break; - } - - case BVLE: - case BVGE: - case BVGT: - case BVLT: - case BVSLE: - case BVSGE: - case BVSGT: - case BVSLT: { - result = BBcompare(form); - break; - } - default: - FatalError("BBForm: Illegal kind: ", form); - break; - } - - // cout << "================" << endl - // << "BBForm: " << form << endl - // << "----------------" << endl - // << "BBForm Result: " << result << endl; - - return (BBFormMemo[form] = result); -} - -// Bit blast a sum of two equal length BVs. -// Update sum vector destructively with new sum. -void BeevMgr::BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin) -{ -// cout << "Bitblasting plus. Operand 1: " << endl; -// lpvec(sum); -// cout << endl << " operand 2: " << endl; -// lpvec(y); -// cout << endl << "carry: " << endl << cin << endl; - - - int n = sum.size(); - // ASSERT: y.size() == x.size() - // FIXME: Don't bother computing i+1 carry, which is discarded. - for (int i = 0; i < n; i++) { - ASTNode nextcin = Majority(sum[i], y[i], cin); - sum[i] = CreateSimpForm(XOR, CreateSimpForm(XOR, sum[i], y[i]), cin); - cin = nextcin; - } - -// cout << "----------------" << endl << "Result: " << endl; -// lpvec(sum); -// cout << endl; - -} - -// Stores result - x in result, destructively -void BeevMgr::BBSub(ASTVec& result, const ASTVec& y) -{ - ASTVec compsubtrahend = BBNeg(y); - BBPlus2(result, compsubtrahend, ASTTrue); -} - -// Add one bit -ASTVec BeevMgr::BBAddOneBit(ASTVec& x, ASTNode cin) -{ - ASTVec result = ASTVec(0); - ASTVec::const_iterator itend = x.end(); - for (ASTVec::const_iterator it = x.begin(); it < itend; it++) { - ASTNode nextcin = CreateSimpForm(AND, *it, cin); - result.push_back(CreateSimpForm(XOR, *it, cin)); - cin = nextcin; - } - // FIXME: unnecessary array copy on return? - return result; -} - -// Increment bit-blasted vector and return result. -ASTVec BeevMgr::BBInc(ASTVec& x) -{ - return BBAddOneBit(x, ASTTrue); -} - -// Return formula for majority function of three bits. -// Pass arguments by reference to reduce refcounting. -ASTNode BeevMgr::Majority(const ASTNode& a, const ASTNode& b,const ASTNode& c) -{ - // Checking explicitly for constant a, b and c could - // be more efficient, because they are repeated in the logic. - if (ASTTrue == a) { - return CreateSimpForm(OR, b, c); - } - else if (ASTFalse == a) { - return CreateSimpForm(AND, b, c); - } - else if (ASTTrue == b) { - return CreateSimpForm(OR, a, c); - } - else if (ASTFalse == b) { - return CreateSimpForm(AND, a, c); - } - else if (ASTTrue == c) { - return CreateSimpForm(OR, a, b); - } - else if (ASTFalse == c) { - return CreateSimpForm(AND, a, b); - } - // there are lots more simplifications, but I'm not sure they're - // worth doing explicitly (e.g., a = b, a = ~b, etc.) - else { - return - CreateSimpForm(OR, - CreateSimpForm(AND, a, b), - CreateSimpForm(AND, b, c), - CreateSimpForm(AND, a, c)); - } -} - - -// Bitwise complement -ASTVec BeevMgr::BBNeg(const ASTVec& x) -{ - ASTVec result = ASTVec(0); // FIXME: faster to preallocate n entries? - // Negate each bit. - ASTVec::const_iterator xend = x.end(); - for (ASTVec::const_iterator it = x.begin(); it < xend; it++) { - result.push_back(CreateSimpNot(*it)); - } - // FIXME: unecessary array copy when it returns? - return result; -} - -// Compute unary minus -ASTVec BeevMgr::BBUminus(const ASTVec& x) -{ - ASTVec xneg = BBNeg(x); - return BBInc(xneg); -} - -// Multiply two bitblasted numbers -ASTVec BeevMgr::BBMult(const ASTVec& x, const ASTVec& y) -{ - ASTVec ycopy(y); - ASTVec::const_iterator xend = x.end(); - ASTVec::const_iterator xit = x.begin(); - // start prod with first partial product. - // FIXME: This is unnecessary. Clean it up. - ASTVec prod = ASTVec(BBAndBit(y, *xit)); - // start loop at next bit. - for(xit++; xit < xend; xit++) { - // shift first - BBLShift(ycopy); - - if (ASTFalse == *xit) { - // If this bit is zero, the partial product will - // be zero. No reason to add that in. - continue; - } - - ASTVec pprod = BBAndBit(ycopy, *xit); - // accumulate in the product. - BBPlus2(prod, pprod, ASTFalse); - } - return prod; -} - -// This implements a variant of binary long division. -// q and r are "out" parameters. rwidth puts a bound on the -// recursion depth. -void BeevMgr::BBDivMod(const ASTVec &y, const ASTVec &x, ASTVec &q, ASTVec &r, unsigned int rwidth) -{ - unsigned int width = y.size(); - if (rwidth == 0) { - // When we have shifted the entire width, y is guaranteed to be 0. - q = BBfill(width, ASTFalse); - r = BBfill(width, ASTFalse); - } - else { - ASTVec q1, r1; - ASTVec yrshift1(y); - BBRShift(yrshift1); - - // recursively divide y/2 by x. - BBDivMod(yrshift1, x, q1, r1, rwidth-1); - - ASTVec q1lshift1(q1); - BBLShift(q1lshift1); - - ASTVec r1lshift1(r1); - BBLShift(r1lshift1); - - ASTVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]); - ASTVec rminusx(r1lshift1plusyodd); - BBSub(rminusx, x); - - // Adjusted q, r values when when r is too large. - ASTNode rtoolarge = BBBVLE(x, r1lshift1plusyodd, false); - ASTVec ygtrxqval = BBITE(rtoolarge, BBInc(q1lshift1), q1lshift1); - ASTVec ygtrxrval = BBITE(rtoolarge, rminusx, r1lshift1plusyodd); - - // q & r values when y >= x - ASTNode yeqx = BBEQ(y, x); - // *** Problem: the bbfill for qval is wrong. Should be 1, not -1. - ASTVec one = BBfill(width, ASTFalse); - one[0] = ASTTrue; - ASTVec notylessxqval = BBITE(yeqx, one, ygtrxqval); - ASTVec notylessxrval = BBITE(yeqx, BBfill(width, ASTFalse), ygtrxrval); - // y < x <=> not x >= y. - ASTNode ylessx = CreateSimpNot(BBBVLE(x, y, false)); - // final values of q and r - q = BBITE(ylessx, BBfill(width, ASTFalse), notylessxqval); - r = BBITE(ylessx, y, notylessxrval); - } -} - -// build ITE's (ITE cond then[i] else[i]) for each i. -ASTVec BeevMgr::BBITE(const ASTNode& cond, const ASTVec& thn, const ASTVec& els) -{ - // Fast exits. - if (ASTTrue == cond) { - return thn; - } - else if (ASTFalse == cond) { - return els; - } - - ASTVec result(0); - ASTVec::const_iterator th_it_end = thn.end(); - ASTVec::const_iterator el_it = els.begin(); - for (ASTVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) { - result.push_back(CreateSimpForm(ITE, cond, *th_it, *el_it)); - } - return result; -} -// AND each bit of vector y with single bit b and return the result. -ASTVec BeevMgr::BBAndBit(const ASTVec& y, ASTNode b) -{ - ASTVec result(0); - - if (ASTTrue == b) { - return y; - } - // FIXME: put in fast exits when b is constant 0. - - ASTVec::const_iterator yend = y.end(); - for(ASTVec::const_iterator yit = y.begin(); yit < yend; yit++) { - result.push_back(CreateSimpForm(AND, *yit, b)); - } - return result; -} - - -// Workhorse for comparison routines. This does a signed BVLE if is_signed -// is true, else it's unsigned. All other comparison operators can be reduced -// to this by swapping args or complementing the result bit. -// FIXME: If this were done MSB first, it would enable a fast exit sometimes -// when the MSB is constant, deciding the result without looking at the rest -// of the bits. -ASTNode BeevMgr::BBBVLE(const ASTVec& left, const ASTVec& right, bool is_signed) -{ - // "thisbit" represents BVLE of the suffixes of the BVs - // from that position . if R < L, return TRUE, else if L < R - // return FALSE, else return BVLE of lower-order bits. MSB is - // treated separately, because signed comparison is done by - // complementing the MSB of each BV, then doing an unsigned - // comparison. - ASTVec::const_iterator lit = left.begin(); - ASTVec::const_iterator litend = left.end(); - ASTVec::const_iterator rit = right.begin(); - ASTNode prevbit = ASTTrue; - for ( ; lit < litend-1; lit++, rit++) { - ASTNode neglit = CreateSimpNot(*lit); - ASTNode thisbit = - CreateSimpForm(OR, - CreateSimpForm(AND,neglit,*rit), // TRUE if l < r - CreateSimpForm(AND, - CreateSimpForm(OR, neglit, *rit), // false if not equal - prevbit)); // else prevbit - prevbit = thisbit; - } - - // Handle MSB -- negate MSBs if signed comparison - // FIXME: make into refs after it's debugged. - ASTNode lmsb = *lit; - ASTNode rmsb = *rit; - if (is_signed) { - lmsb = CreateSimpNot(*lit); - rmsb = CreateSimpNot(*rit); - } - - ASTNode neglmsb = CreateSimpNot(lmsb); - ASTNode msb = - CreateSimpForm(OR, - CreateSimpForm(AND,neglmsb, rmsb), // TRUE if l < r - CreateSimpForm(AND, - CreateSimpForm(OR, neglmsb, rmsb), // false if not equal - prevbit)); // else prevbit - return msb; -} - -// Left shift by 1 within fixed field inserting zeros at LSB. -// Writes result into first argument. -// Fixme: generalize to n bits -void BeevMgr::BBLShift(ASTVec& x) -{ - // left shift x (destructively) within width. - // loop backwards so that copy to self works correctly. (DON'T use STL insert!) - ASTVec::iterator xbeg = x.begin(); - for(ASTVec::iterator xit = x.end()-1; xit > xbeg; xit--) { - *xit = *(xit-1); - } - *xbeg = ASTFalse; // new LSB is zero. - // cout << "Shifted result" << endl; - // lpvec(x); -} - -// Right shift by 1 within fixed field, inserting new zeros at MSB. -// Writes result into first argument. -// Fixme: generalize to n bits. -void BeevMgr::BBRShift(ASTVec& x) -{ - ASTVec::iterator xend = x.end() - 1; - ASTVec::iterator xit = x.begin(); - for( ; xit < xend; xit++) { - *xit = *(xit+1); - } - *xit = ASTFalse; // new MSB is zero. -} - - -// Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. -ASTNode BeevMgr::BBcompare(const ASTNode& form) { - const ASTNode lnode = BBTerm(form[0]); - const ASTNode rnode = BBTerm(form[1]); - const ASTVec& left = lnode.GetChildren(); - const ASTVec& right = rnode.GetChildren(); - - //const ASTVec& left = BBTerm(form[0]).GetChildren(); - //const ASTVec& right = BBTerm(form[1]).GetChildren(); - - Kind k = form.GetKind(); - switch(k) { - case BVLE: { return BBBVLE(left, right, false); break; } - case BVGE: { return BBBVLE(right, left, false); break; } - case BVGT: { return CreateSimpNot(BBBVLE(left, right, false)); break; } - case BVLT: { return CreateSimpNot(BBBVLE(right, left, false)); break; } - case BVSLE: { return BBBVLE(left, right, true); break; } - case BVSGE: { return BBBVLE(right, left, true); break; } - case BVSGT: { return CreateSimpNot(BBBVLE(left, right, true)); break; } - case BVSLT: { return CreateSimpNot(BBBVLE(right, left, true)); break; } - default: - cerr << "BBCompare: Illegal kind" << form << endl; - FatalError("",ASTUndefined); - } - return ASTUndefined; -} - - -// return a vector with n copies of fillval -ASTVec BeevMgr::BBfill(unsigned int width, ASTNode fillval) -{ - ASTVec zvec(width, fillval); - return zvec; -} - -ASTNode BeevMgr::BBEQ(const ASTVec& left, const ASTVec& right) -{ - ASTVec andvec; - ASTVec::const_iterator lit = left.begin(); - ASTVec::const_iterator litend = left.end(); - ASTVec::const_iterator rit = right.begin(); - - if(left.size() > 1) { - for(; lit != litend; lit++, rit++) { - ASTNode biteq = CreateSimpForm(IFF, *lit, *rit); - // fast path exit - if (biteq == ASTFalse) { - return ASTFalse; - } - else { - andvec.push_back(biteq); - } - } - ASTNode n = CreateSimpForm(AND, andvec); - return n; - } - else - return CreateSimpForm(IFF,*lit,*rit); -} -} // BEEV namespace diff --git a/stp/AST/Makefile b/stp/AST/Makefile deleted file mode 100644 index c3b54672..00000000 --- a/stp/AST/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -#===-- stp/AST/Makefile ------------------------------------*- Makefile -*--===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# - -LEVEL=../.. - -LIBRARYNAME=stp_AST -DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 - -include $(LEVEL)/Makefile.common - -# HACK: Force -Wno-deprecated for ext container use. -CXX.Flags += -Wno-deprecated diff --git a/stp/AST/STLport_config.h b/stp/AST/STLport_config.h deleted file mode 100644 index 9b7bc14f..00000000 --- a/stp/AST/STLport_config.h +++ /dev/null @@ -1,20 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -// STLport debug checking, if we use STLport threads flag is to get -// rid of link errors, since iostreams compiles with threads. alloc -// and uninitialized are extra checks Later on, if used with Purify or -// Valgrind, may want to set flags to prevent reporting of false -// leaks. For some reason, _STLP_THREADS works on the command line -// but not here (?) -#define _STLP_THREADS -#define _STLP_DEBUG 1 -#define _STLP_DEBUG_LEVEL _STLP_STANDARD_DBG_LEVEL -#define _STLP_DEBUG_ALLOC 1 -#define _STLP_DEBUG_UNINITIALIZED 1 diff --git a/stp/AST/SimpBool.cpp b/stp/AST/SimpBool.cpp deleted file mode 100644 index 67f9825d..00000000 --- a/stp/AST/SimpBool.cpp +++ /dev/null @@ -1,408 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: April, 2006 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ - -// -*- c++ -*- - -// Simplifying create methods for Boolean operations. -// These are only very simple local simplifications. - -// This is somewhat redundant with Vijay's simplifier code. They -// need to be merged. -// FIXME: control with optimize flag. - -static bool _trace_simpbool = 0; -static bool _disable_simpbool = 0; - -#include "AST.h" - -// SMTLIB experimental hack. Try allocating a single stack here for -// children to reduce growing of vectors. -//BEEV::ASTVec child_stack; - -namespace BEEV { - - ASTNode BeevMgr::CreateSimpForm(Kind kind, ASTVec &children = _empty_ASTVec) { - if (_disable_simpbool) { - return CreateNode(kind, children); - } - else { - switch (kind) { - case NOT: return CreateSimpNot(children[0]); break; - case AND: return CreateSimpAndOr(1, children); break; - case OR: return CreateSimpAndOr(0, children); break; - case NAND: return CreateSimpNot(CreateSimpAndOr(1, children)); break; - case NOR: return CreateSimpNot(CreateSimpAndOr(0, children)); break; - case IFF: { - // Not sure children can ever be empty, but what the heck. - // if (children.size() == 0) { - // return ASTTrue; - // } - // Convert IFF to XOR ASAP. IFF is not associative, so this makes - // flattening much easier. - children[0] = CreateSimpNot(children[0]); - return CreateSimpXor(children); break; - } - case XOR: - return CreateSimpXor(children); break; - // FIXME: Earlier, check that this only has two arguments - case IMPLIES: return CreateSimpAndOr(0, CreateSimpNot(children[0]), children[1]); break; - case ITE: return CreateSimpFormITE(children[0], children[1], children[2]); - default: return CreateNode(kind, children); - } - } - } - - // specialized versions - - ASTNode BeevMgr::CreateSimpForm(Kind kind, - const ASTNode& child0) { - ASTVec children; - //child_stack.clear(); // could just reset top pointer. - children.push_back(child0); - //child_stack.push_back(child0); - return CreateSimpForm(kind, children); - //return CreateSimpForm(kind, child_stack); - } - - ASTNode BeevMgr::CreateSimpForm(Kind kind, - const ASTNode& child0, - const ASTNode& child1) { - ASTVec children; - //child_stack.clear(); // could just reset top pointer. - children.push_back(child0); - //child_stack.push_back(child0); - children.push_back(child1); - //child_stack.push_back(child1); - return CreateSimpForm(kind, children); - //return CreateSimpForm(kind, child_stack); - } - - - ASTNode BeevMgr::CreateSimpForm(Kind kind, - const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2) { - ASTVec children; - //child_stack.clear(); // could just reset top pointer. - children.push_back(child0); - //child_stack.push_back(child0); - children.push_back(child1); - //child_stack.push_back(child1); - children.push_back(child2); - //child_stack.push_back(child2); - return CreateSimpForm(kind, children); - //return CreateSimpForm(kind, child_stack); - } - - ASTNode BeevMgr::CreateSimpNot(const ASTNode& form) { - Kind k = form.GetKind(); - switch (k) { - case FALSE: { return ASTTrue; } - case TRUE: { return ASTFalse; } - case NOT: { return form[0]; } // NOT NOT cancellation - case XOR: { - // Push negation down in this case. - // FIXME: Separate pre-pass to push negation down? - // CreateSimp should be local, and this isn't. - // It isn't memoized. Arg. - ASTVec children = form.GetChildren(); - children[0] = CreateSimpNot(children[0]); - return CreateSimpXor(children); - } - default: { return CreateNode(NOT, form); } - } - } - - // I don't think this is even called, since it called - // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no - // ill effects. Calls seem to go to the version that takes a vector - // of children. - ASTNode BeevMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2) { - ASTVec children; - children.push_back(form1); - children.push_back(form2); - return CreateSimpXor(children); - } - - - ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2) { - ASTVec children; - children.push_back(form1); - children.push_back(form2); - return CreateSimpAndOr(IsAnd, children); - } - - ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, ASTVec &children) { - - if (_trace_simpbool) { - cout << "========" << endl << "CreateSimpAndOr " << (IsAnd ? "AND " : "OR ") ; - lpvec(children); - cout << endl; - } - - ASTVec new_children; - - // sort so that identical nodes occur in sequential runs, followed by - // their negations. - - SortByExprNum(children); - - ASTNode annihilator = (IsAnd ? ASTFalse : ASTTrue); - ASTNode identity = (IsAnd ? ASTTrue : ASTFalse); - - ASTNode retval; - - ASTVec::const_iterator it_end = children.end(); - ASTVec::const_iterator next_it; - for(ASTVec::const_iterator it = children.begin(); it != it_end; it = next_it) { - next_it = it + 1; - bool nextexists = (next_it < it_end); - - if (*it == annihilator) { - retval = annihilator; - if (_trace_simpbool) { - cout << "returns " << retval << endl; - } - return retval; - } - else if (*it == identity) { - // just drop it - } - else if (nextexists && (*next_it == *it)) { - // drop it - // cout << "Dropping [" << it->GetNodeNum() << "]" << endl; - } - else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) { - // form and negation -- return FALSE for AND, TRUE for OR. - retval = annihilator; - // cout << "X and/or NOT X" << endl; - if (_trace_simpbool) { - cout << "returns " << retval << endl; - } - return retval; - } - else { - // add to children - new_children.push_back(*it); - } - } - - // If we get here, we saw no annihilators, and children should - // be only the non-True nodes. - if (new_children.size() < 2) { - if (0 == new_children.size()) { - retval = identity; - } - else { - // there is just one child - retval = new_children[0]; - } - } - else { - // 2 or more children. Create a new node. - retval = CreateNode(IsAnd ? AND : OR, new_children); - } - if (_trace_simpbool) { - cout << "returns " << retval << endl; - } - return retval; - } - - - // Constant children are accumulated in "accumconst". - ASTNode BeevMgr::CreateSimpXor(ASTVec &children) { - - if (_trace_simpbool) { - cout << "========" << endl - << "CreateSimpXor "; - lpvec(children); - cout << endl; - } - - // Change this not to init to children if flattening code is present. - // ASTVec flat_children = children; // empty vector - - ASTVec flat_children; // empty vector - - ASTVec::const_iterator it_end = children.end(); - - if (xor_flatten) { - - bool fflag = 0; // ***Temp debugging - - // Experimental flattening code. - - for(ASTVec::iterator it = children.begin(); it != it_end; it++) { - Kind ck = it->GetKind(); - const ASTVec &gchildren = it->GetChildren(); - if (XOR == ck) { - fflag = 1; - // append grandchildren to children - flat_children.insert(flat_children.end(), gchildren.begin(), gchildren.end()); - } - else { - flat_children.push_back(*it); - } - } - - if (_trace_simpbool && fflag) { - cout << "========" << endl; - cout << "Flattening: " << endl; - lpvec(children); - - cout << "--------" << endl; - cout << "Flattening result: " << endl; - lpvec(flat_children); - } - } - else { - flat_children = children; - } - - - // sort so that identical nodes occur in sequential runs, followed by - // their negations. - SortByExprNum(flat_children); - - ASTNode retval; - - // This is the C Boolean value of all constant args seen. It is initially - // 0. TRUE children cause it to change value. - bool accumconst = 0; - - ASTVec new_children; - - it_end = flat_children.end(); - ASTVec::iterator next_it; - for(ASTVec::iterator it = flat_children.begin(); it != it_end; it++) { - next_it = it + 1; - bool nextexists = (next_it < it_end); - - if (ASTTrue == *it) { - accumconst = !accumconst; - } - else if (ASTFalse == *it) { - // Ignore it - } - else if (nextexists && (*next_it == *it)) { - // x XOR x = FALSE. Skip current, write "false" into next_it - // so that it gets tossed, too. - *next_it = ASTFalse; - } - else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) { - // x XOR NOT x = TRUE. Skip current, write "true" into next_it - // so that it gets tossed, too. - *next_it = ASTTrue; - } - else if (NOT == it->GetKind()) { - // If child is (NOT alpha), we can flip accumconst and use alpha. - // This is ok because (NOT alpha) == TRUE XOR alpha - accumconst = !accumconst; - // CreateSimpNot just takes child of not. - new_children.push_back(CreateSimpNot(*it)); - } - else { - new_children.push_back(*it); - } - } - - // Children should be non-constant. - if (new_children.size() < 2) { - if (0 == new_children.size()) { - // XOR(TRUE, FALSE) -- accumconst will be 1. - if (accumconst) { - retval = ASTTrue; - } - else { - retval = ASTFalse; - } - } - else { - // there is just one child - // XOR(x, TRUE) -- accumconst will be 1. - if (accumconst) { - retval = CreateSimpNot(new_children[0]); - } - else { - retval = new_children[0]; - } - } - } - else { - // negate first child if accumconst == 1 - if (accumconst) { - new_children[0] = CreateSimpNot(new_children[0]); - } - retval = CreateNode(XOR, new_children); - } - - if (_trace_simpbool) { - cout << "returns " << retval << endl; - } - return retval; - } - - // FIXME: How do I know whether ITE is a formula or not? - ASTNode BeevMgr::CreateSimpFormITE(const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2) { - - ASTNode retval; - - if (_trace_simpbool) { - cout << "========" << endl << "CreateSimpFormITE " - << child0 - << child1 - << child2 << endl; - } - - if (ASTTrue == child0) { - retval = child1; - } - else if (ASTFalse == child0) { - retval = child2; - } - else if (child1 == child2) { - retval = child1; - } - // ITE(x, TRUE, y ) == x OR y - else if (ASTTrue == child1) { - retval = CreateSimpAndOr(0, child0, child2); - } - // ITE(x, FALSE, y ) == (!x AND y) - else if (ASTFalse == child1) { - retval = CreateSimpAndOr(1, CreateSimpNot(child0), child2); - } - // ITE(x, y, TRUE ) == (!x OR y) - else if (ASTTrue == child2) { - retval = CreateSimpAndOr(0, CreateSimpNot(child0), child1); - } - // ITE(x, y, FALSE ) == (x AND y) - else if (ASTFalse == child2) { - retval = CreateSimpAndOr(1, child0, child1); - } - // ITE (x, !y, y) == x XOR y -// else if (NOT == child1.GetKind() && (child1[0] == child2)) { -// retval = CreateSimpXor(child0, child2); -// } -// // ITE (x, y, !y) == x IFF y. I think other cases are covered -// // by XOR/IFF optimizations -// else if (NOT == child2.GetKind() && (child2[0] == child1)) { -// retval = CreateSimpXor(CreateSimpNot(child0), child2); -// } - else { - retval = CreateNode(ITE, child0, child1, child2); - } - - if (_trace_simpbool) { - cout << "returns " << retval << endl; - } - - return retval; - } -} // BEEV namespace diff --git a/stp/AST/ToCNF.cpp b/stp/AST/ToCNF.cpp deleted file mode 100644 index 2a18b3f5..00000000 --- a/stp/AST/ToCNF.cpp +++ /dev/null @@ -1,506 +0,0 @@ -/******************************************************************** - * AUTHORS: David L. Dill, Vijay Ganesh - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -// THEORY: This code translates an arbitrary Boolean DAG, generated by -// the BitBlast.cpp, to an equi-satisfiable CNF formula. There are -// four kinds of variables in the CNF formula: (1) propositional -// variables from the original formula; (2) BVGETBIT formulas from the -// original formula (a precondition is that the BVGETBIT can only be -// applied to bitvector-valued variables, array reads, or -// uninterpreted functions); (3) TRUE; or (4) representative variables -// (see below). Each literal in the CNF formula is one of these or -// its negation. - -// It is convenient (though not perfectly efficient) to be able to add -// TRUE and FALSE constants to clauses, which is not allowed in CNF. -// So, there is a "dummy variable" representing TRUE, which is used in -// its place (so FALSE is represented by the negation of the dummy -// var). The CNF formula has a unit clause containing this dummy -// variable, so that any satisfying assignment must make the dummy var -// TRUE. - -// Every sub-formula of the input formula has a "representative -// literal." A truth assignment satisfies the CNF formula iff the -// restriction of that assignment to the original variables satisfies -// the original formula, AND the rep lits have the same truth values -// as the subformulas they represent in the original formula. In the -// trivial cases, the representative literal is the input variable, or -// dummy true var, or its negation. Representative literals may be -// negated variables -- essentially, only AND formulas are translated, -// and everything else is handled by rewriting or negating formulas. -// The representative for (NOT alpha) is the negation of the -// representative for alpha. - -// The translation is performed by ToCNF_int, which traverses the original -// formula. ToCNF adds clauses that constrain the representative variables -// to be equal to the truth values of the formulas they represent. -// ToCNF always returns a literal whose value must be equivalent to the formula -// it translated. In trivial cases, this literal is a literal from the original -// formula, or the dummy true/false literals. If the formula is of the form -// (not alpha), ToCNF_int negates the literal representing alpha (which may -// itself be a negative literal) and returns it. Otherwise, ToCNF_int assigns -// a new rep var, adds the clauses, and returns the new var. ToCNF_int is -// memoized so that it doesn't assign more than one variable to a subformula, -// and to prevent exponential numbers of redundant visits to shared subformulas. - -// In reality, only AND/OR/NOT formulas are translated directly. Everything -// else (XOR, IFF, IMPLIES) is rewritten on-the-fly into these forms. I -// could have done that in bit-blasting, but I thought that, in the future, -// we might be able to translate these operations differently in different -// contexts to optimize the CNF formula. - -// FIXME: Inspection of the clauses is kind of horrifying. In -// addition to true/false, there are duplicate literals and duplicate -// clauses all over the place. -#include "AST.h" -static bool CNF_trace = false; -namespace BEEV { -/** Statistics class. Total number of variables is best tracked in - ToSAT. Number of clauses is just cll.size() */ - -class CNFstats { -public: - int _num_new_rep_vars; - int _num_clauses; - - // constructor - CNFstats() : _num_new_rep_vars(0), _num_clauses(0) {} - - void printStats() { - if(stats) { - cout << "ToCNF statistics:" << endl; - cout << "Number of new representative variables: " - << _num_new_rep_vars << endl; - cout << "Number of new clauses: " - << _num_clauses << endl; - } - } - -}; - - -/** This class contains private data and function members for the - CNF conversion */ -class CNFMgr { - - friend class BeevMgr; - -public: - - // Needed in the body of BeevMgr::ToCNF. It's not visible outside - // this file, though. - ASTNode dummy_true_var; - - // CNF Pre-pass - ASTNodeMap ToCNFPrePassMemo; - - // CNF Memo Table. - ASTNodeMap CNFMemo; - - -private: - - // Pointer back to BeevMgr with the node tables, etc. - BeevMgr *bm; - - // For ToCNF conversion. This holds a dummy variable representing - // "True". It is added as a unit clause, so that it will be assigned - // to true and propagated immediately by any CNF solver. - - ASTNode dummy_false_var; // not of dummy_true_var - - CNFstats stats; - - // constructor - CNFMgr(BeevMgr *bmgr) - { - bm = bmgr; - - // Dummy variable so TRUE can be a literal. - dummy_true_var = bm->CreateSymbol("*TrueDummy*"); - dummy_false_var = bm->CreateSimpNot(dummy_true_var); - } - - // Returns true iff result has been memoized. - // if it returns true, result is returned in by-ref parameter "result" - // Consider just putitng this in-line. - bool CNFIsMemoized(ASTNode &form, ASTNode &result) - { - ASTNodeMap::iterator it = CNFMemo.find(form); - if (it != CNFMemo.end()) { - result = it->second; //already there. Just return it. - return true; - } - else { - return false; - } - } - - - // Convert a big XOR to a bunch of AND/ORs. Assumes subformulas have - // already been converted. - ASTNode convertXORs(ASTVec children) - { - ASTNode accum = children[0]; - ASTVec::iterator itend = children.end(); - for (ASTVec::iterator it = children.begin()+1; it < itend; it++) { - // a XOR b -> (a | b) & (!a | !b) - - // For each XOR node with k children, creates approximately - // 5*(k-1) nodes. AND + 2 OR + 2 NOT. - - ASTNode or1 = bm->CreateNode(OR, accum, *it); - ASTNode or2 = bm->CreateNode(OR, bm->CreateSimpNot(accum), bm->CreateSimpNot(*it)); - accum = bm->CreateNode(AND, or1, or2); - - } - - return accum; - } - - - // Do preliminary transformations on bitblasted formula to make - // CNF conversion easier. - // Converts XORs to AND/OR form. - ASTNode ToCNFPrePass(const ASTNode &form) - { - - // Check memo table - ASTNodeMap::iterator mem_it = ToCNFPrePassMemo.find(form); - if (mem_it != ToCNFPrePassMemo.end()) { - return mem_it->second; - } - - ASTNode result; - - ASTVec new_children; - ASTVec::const_iterator endit = form.end(); - for (ASTVec::const_iterator it = form.begin(); it != endit; it++) { - ASTNode ch = ToCNFPrePass(*it); - new_children.push_back(ch); - } - - Kind k = form.GetKind(); - - switch (k) { - case FALSE: - case TRUE: - case SYMBOL: - case BVGETBIT: { - result = form; - break; - } - case XOR: { - // convertXORs can only be called once per XOR node. - result = convertXORs(new_children); - - // cout << "convertXORs num args: " << new_children.size() << endl; - // temporary node for node count. - // ASTNode tmp = bm->CreateNode(XOR, new_children ); - // cout << "convertXORs size of [" << form.GetNodeNum() << "] " << bm->NodeSize(form, true) << endl; - // cout << "convertXORs before size: " << bm->NodeSize(tmp, true) << endl; - // cout << "convertXORs after size: " << bm->NodeSize(result, true) << endl; - break; - } - default: { - // Be cautious about using CreateSimpForm -- It makes big xors! - result = bm->CreateNode(k, new_children); - } - } - -// cout << "================" << endl -// << "ToCNFPrePass:" << form << endl -// << "----------------" << endl -// << "ToCNFPrePass Result:" << result << endl; - - return (ToCNFPrePassMemo[form] = result); - - } - - // Memoize and return formula value - ASTNode CNFMemoize(ASTNode& form, ASTNode result) - { - CNFMemo[form] = result; - return result; - } - - - // Create a representative variable for an original formula. - // The convention is that the variable will have the same truth - // value as the expression numbered "num." - ASTNode RepLit(const char *name, int exprnum) - { - // FIXME: can this be done more efficiently with string type? - ostringstream oss; - oss << name << "{" << exprnum << "}"; - ASTNode t = bm->CreateSymbol(oss.str().c_str()); - - // Track how many we're generating. - stats._num_new_rep_vars++; - - //ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0)) - t.SetIndexWidth(0); - t.SetValueWidth(0); - return t; - } - - // Handle the cases where it's necessary to do n children. - // This code translates ANDs, and converts NAND, NOR, OR by negating - // the inputs or outputs of the AND. - ASTNode ToCNF_AndLike(Kind k, BeevMgr::ClauseList& cll, ASTNode form) - { - // Build vectors of positive and negative rep lits for children - ASTVec kidlits(0); - ASTVec negkidlits(0); - ASTVec::const_iterator kids_end = form.end(); - for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) { - ASTNode kidreplit = ToCNF_int(cll, *it); - kidlits.push_back(kidreplit); - negkidlits.push_back(bm->CreateSimpNot(kidreplit)); - } - - ASTNode replit; - // translate the AND, negating inputs as appropriate. - if (k == OR || k == NOR) { - replit = ToCNF_AND(cll, form.GetNodeNum(), negkidlits, kidlits); - } - else { - replit = ToCNF_AND(cll, form.GetNodeNum(), kidlits, negkidlits); - } - - // Reduce NAND/OR to AND by negating result. - if (k == NAND || k == OR) { - return CNFMemoize(form, bm->CreateSimpNot(replit)); - } - else { - return CNFMemoize(form, replit); - } - } - - ASTNode ToCNF_AND(BeevMgr::ClauseList& cll, int nodenum, ASTVec& kidlits, ASTVec& negkidlits) - { - // Translate an AND, given rep lits for children - // Build clauses for (replit <-> a AND b AND c) - - ASTNode replit = RepLit("cnf", nodenum); - ASTNode notreplit = bm->CreateSimpNot(replit); - - if (CNF_trace) { - cout << "Translating AND" << endl << "-----------------------" << endl - << "Rep lit =" << replit << endl - << "-----------------------"; - } - - // (a AND b AND c -> replit) == (~a OR ~b OR ~c OR replit) - BeevMgr::ClausePtr clp = new ASTVec(negkidlits); - clp->push_back(replit); - - if (CNF_trace) { - LispPrintVec(cout, *clp, 0); - cout << endl << "-----------------------" << endl; - } - - cll.push_back(clp); - - // (replit -> (a AND b AND c)) == - // (~replit OR a) AND (~replit OR b) AND (~replit OR c) - ASTVec::const_iterator kidlits_end = kidlits.end(); - for (ASTVec::iterator it = kidlits.begin(); it != kidlits_end; it++) { - clp = new ASTVec(); - clp->push_back(notreplit); - clp->push_back(*it); - - if (CNF_trace) { - LispPrintVec(cout, *clp, 0); - cout << endl << "-----------------------" << endl; - } - - cll.push_back(clp); - } - - return replit; - } - -public: - - /** Builds clauses globally and returns a literal. - The literal can be a leaf from the expression, or a rep var - made up to represent the subexpression. */ - ASTNode ToCNF_int(BeevMgr::BeevMgr::ClauseList& cll, ASTNode form) { - // FIXME: assert indexwidth= 0, valuewidth = 1 - - // FIXME: rewriting is top-down, which is not efficient. - // It rewrites the top node of the tree, then does the children. - // Either rewrite in a separate pass, or translate children - // before rewriting somehow (might require handling rep lits - // as though they were real lits, which is probably ok). - - // Return memoized value if seen before. - ASTNode result; - Kind k = form.GetKind(); - - if (CNFIsMemoized(form, result)) { - return result; - } - - switch (k) { - // handle the trivial cases here. If none apply, call the - // heavy-duty function. If a constant or literal, just return - // without creating a clause. - case FALSE: { - result = dummy_false_var; - break; - } - case TRUE: { - result = dummy_true_var; - break; - } - case SYMBOL: - case BVGETBIT: { - result = form; - break; - } - - case NOT: { - ASTNode replit = ToCNF_int(cll, form[0]); - result = bm->CreateSimpNot(replit); - break; - } - - // For these, I can't think of anything better than expanding into ANDs/ORs - case ITE: { - // (ite a b c) == (~a OR b) AND (a OR c) - ASTNode l = bm->CreateNode(OR, bm->CreateSimpNot(form[0]), form[1]); - ASTNode r = bm->CreateNode(OR, form[0], form[2]); - ASTNode andor = bm->CreateNode(AND, l, r); - if (CNF_trace) { - cout << "Rewriting " << form << endl - << "to" << andor << endl - << "-------------------" << endl; - } - result = ToCNF_int(cll, andor); - break; - } - case IMPLIES: { - // Just rewrite into (~a OR b) - ASTNode l = bm->CreateSimpNot(form[0]); - ASTNode andor = bm->CreateNode(OR, l, form[1]); - if (CNF_trace) { - cout << "Rewriting " << form << endl - << "to" << andor << endl - << "-------------------" << endl; - } - result = ToCNF_int(cll, andor); - break; - } - case XOR: { - FatalError("ToCNF_int: XORs should have been converted to AND/OR by this point."); - break; - } - - case IFF: { - FatalError("BitBlaster failed to eliminate all IFFs."); - break; - } - - case AND: - case OR: - case NOR: - case NAND: { - result = ToCNF_AndLike(k, cll, form); - break; - } - default: - cerr << "ToCNF: can't handle this kind: " << k << endl; - FatalError(""); - } - - if (CNF_trace) { - cout << "ToCNF_int: Literal " << result << " represents formula " << - form << endl << "---------------" << endl; - } - - return CNFMemoize(form, result); - } //end of ToCNF_int() - - -}; // end of CNFMgr class - - // These are the bodies of functions in the BeevMgr that are part of - // the public interface. - - // Debug printing function. - void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll) - { - int num_clauses = cll.size(); - os << "Clauses: " << endl << "=========================================" << endl; - for(int i=0; i < num_clauses; i++) { - os << "Clause " << i << endl - << "-------------------------------------------" << endl; - LispPrintVec(os, *cll[i], 0); - os << endl - << "-------------------------------------------" << endl; - } - } - - void BeevMgr::DeleteClauseList(BeevMgr::ClauseList *cllp) - { - BeevMgr::ClauseList::const_iterator iend = cllp->end(); - for (BeevMgr::ClauseList::const_iterator i = cllp->begin(); i < iend; i++) { - delete *i; - } - delete cllp; - } - - // Top level conversion function - BeevMgr::ClauseList *BeevMgr::ToCNF(const ASTNode& form) - { - - // FIXME: This is leaked as well. - CNFMgr *cm = new CNFMgr(this); - - // Prepass - ASTNode form1 = cm->ToCNFPrePass(form); - - // cout << "Number of nodes after ToCNFPrePass" << NodeSize(form1, true) << endl; - - // cout << "ToCNF: After ToCNFPrePass" << form1 << endl; - - // FIXME: Assert CNFMemo is empty. - - // The clause list we will be building up. - // FIXME: This is never freed. - ClauseList *cllp = new ClauseList(); - - BeevMgr::ClausePtr dummy_true_unit_clause = new ASTVec(); - dummy_true_unit_clause->push_back(cm->dummy_true_var); - cllp->push_back(dummy_true_unit_clause); - - // This is where the translation happens. - ASTNode toplit = cm->ToCNF_int(*cllp, form1); - - // Add the top literal as a unit clause, since it must - // be true when original formula is satsfied. - BeevMgr::ClausePtr clp = new ASTVec(0); - clp->push_back(toplit); - cllp->push_back(clp); - - cm->stats._num_clauses = cllp->size(); - cm->stats.printStats(); - - RepLitMap = cm->CNFMemo; // Save memo table for debugging (DD 1/13/07). - - cm->CNFMemo.clear(); // Important to do this so nodes get freed. - - delete cm; - - return cllp; - } - -} // end namespace diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp deleted file mode 100644 index 3ad21f93..00000000 --- a/stp/AST/ToSAT.cpp +++ /dev/null @@ -1,1386 +0,0 @@ -/******************************************************************** - * 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" -#include "ASTUtil.h" -#include "../simplifier/bvsolver.h" -#include - - -namespace BEEV { - /* FUNCTION: lookup or create a new MINISAT literal - * lookup or create new MINISAT Vars from the global MAP - * _ASTNode_to_SATVar. - */ - MINISAT::Var BeevMgr::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n) { - ASTtoSATMap::iterator it; - MINISAT::Var v; - - //look for the symbol in the global map from ASTNodes to ints. if - //not found, create a S.newVar(), else use the existing one. - if((it = _ASTNode_to_SATVar.find(n)) == _ASTNode_to_SATVar.end()) { - v = newS.newVar(); - _ASTNode_to_SATVar[n] = v; - - //ASSUMPTION: I am assuming that the newS.newVar() call increments v - //by 1 each time it is called, and the initial value of a - //MINISAT::Var is 0. - _SATVar_to_AST.push_back(n); - } - else - v = it->second; - return v; - } - - /* FUNCTION: convert ASTClauses to MINISAT clauses and solve. - * Accepts ASTClauses and converts them to MINISAT clauses. Then adds - * the newly minted MINISAT clauses to the local SAT instance, and - * calls solve(). If solve returns unsat, then stop and return - * unsat. else continue. - */ - // FIXME: Still need to deal with TRUE/FALSE in clauses! - bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll) - { - CountersAndStats("SAT Solver"); - - //iterate through the list (conjunction) of ASTclauses cll - BeevMgr::ClauseList::const_iterator i = cll.begin(), iend = cll.end(); - - if(i == iend) - FatalError("toSATandSolve: Nothing to Solve",ASTUndefined); - - //turnOffSubsumption - newS.turnOffSubsumption(); - - // (*i) is an ASTVec-ptr which denotes an ASTclause - for(; i!=iend; i++) { - //Clause for the SATSolver - MINISAT::vec satSolverClause; - - //now iterate through the internals of the ASTclause itself - ASTVec::const_iterator j = (*i)->begin(), jend = (*i)->end(); - //j is a disjunct in the ASTclause (*i) - for(;j!=jend;j++) { - - bool negate = (NOT == j->GetKind()) ? true : false; - ASTNode n = negate ? (*j)[0] : *j; - - //Lookup or create the MINISAT::Var corresponding to the Booelan - //ASTNode Variable, and push into sat Solver clause - MINISAT::Var v = LookupOrCreateSATVar(newS,n); - MINISAT::Lit l(v, negate); - satSolverClause.push(l); - } - newS.addClause(satSolverClause); - // clause printing. - // (printClause >)(satSolverClause); - // cout << " 0 "; - // cout << endl; - - if(newS.okay()) { - continue; - } - else { - PrintStats(newS.stats); - return false; - } - - if(!newS.simplifyDB(false)) { - PrintStats(newS.stats); - return false; - } - } - - // if input is UNSAT return false, else return true - if(!newS.simplifyDB(false)) { - PrintStats(newS.stats); - return false; - } - - //PrintActivityLevels_Of_SATVars("Before SAT:",newS); - //ChangeActivityLevels_Of_SATVars(newS); - //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS); - newS.solve(); - //PrintActivityLevels_Of_SATVars("After SAT",newS); - - PrintStats(newS.stats); - if (newS.okay()) - return true; - else - return false; - } - - // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver - void BeevMgr::PrintStats(MINISAT::SolverStats& s) { - if(!stats) - return; - double cpu_time = MINISAT::cpuTime(); - MINISAT::int64 mem_used = MINISAT::memUsed(); - printf("restarts : %"I64_fmt"\n", s.starts); - printf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); - printf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); - printf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); - printf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", - s.tot_literals, - (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); - if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used / 1048576.0); - printf("CPU time : %g s\n", cpu_time); - fflush(stdout); - } - - // Prints Satisfying assignment directly, for debugging. - void BeevMgr::PrintSATModel(MINISAT::Solver& newS) { - if(!newS.okay()) - FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT",ASTUndefined); - // FIXME: Don't put tests like this in the print functions. The print functions - // should print unconditionally. Put a conditional around the call if you don't - // want them to print - if(!(stats && print_nodes)) - return; - - int num_vars = newS.nVars(); - cout << "Satisfying assignment: " << endl; - for (int i = 0; i < num_vars; i++) { - if (newS.model[i] == MINISAT::l_True) { - ASTNode s = _SATVar_to_AST[i]; - cout << s << endl; - } - else if (newS.model[i] == MINISAT::l_False) { - ASTNode s = _SATVar_to_AST[i]; - cout << CreateNode(NOT, s) << endl; - } - } - } - - - // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying assignment. - // Returns ASTTrue if true, ASTFalse if false or undefined. - ASTNode BeevMgr::SymbolTruthValue(MINISAT::Solver &newS, ASTNode form) - { - MINISAT::Var satvar = _ASTNode_to_SATVar[form]; - if (newS.model[satvar] == MINISAT::l_True) { - return ASTTrue; - } - else if (newS.model[satvar] == MINISAT::l_False){ - // False - return ASTFalse; - } - else { - return (rand() > 4096) ? ASTTrue : ASTFalse; - } - } - - - // This function is for debugging problems with BitBlast and especially - // ToCNF. It evaluates the bit-blasted formula in the satisfying - // assignment. While doing that, it checks that every subformula has - // the same truth value as its representative literal, if it has one. - // If this condition is violated, it halts immediately (on the leftmost - // lowest term). - // Use CreateSimpForm to evaluate, even though it's expensive, so that - // we can use the partial truth assignment. - ASTNode BeevMgr::CheckBBandCNF(MINISAT::Solver& newS, ASTNode form) - { - // Clear memo table (in case newS has changed). - CheckBBandCNFMemo.clear(); - // Call recursive version that does the work. - return CheckBBandCNF_int(newS, form); - } - - // Recursive body CheckBBandCNF - // FIXME: Modify this to just check if result is true, and print mismatch - // if not. Might have a trace flag for the other stuff. - ASTNode BeevMgr::CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form) - { - - // cout << "++++++++++++++++" << endl << "CheckBBandCNF_int form = " << - // form << endl; - - ASTNodeMap::iterator memoit = CheckBBandCNFMemo.find(form); - if (memoit != CheckBBandCNFMemo.end()) { - // found it. Return memoized value. - return memoit->second; - } - - ASTNode result; // return value, to memoize. - - Kind k = form.GetKind(); - switch (k) { - case TRUE: - case FALSE: { - return form; - break; - } - case SYMBOL: - case BVGETBIT: { - // Look up the truth value - // ASTNode -> Sat -> Truthvalue -> ASTTrue or ASTFalse; - // FIXME: Could make up a fresh var in undefined case. - - result = SymbolTruthValue(newS, form); - - cout << "================" << endl << "Checking BB formula:" << form << endl; - cout << "----------------" << endl << "Result:" << result << endl; - - break; - } - default: { - // Evaluate the children recursively. - ASTVec eval_children; - ASTVec ch = form.GetChildren(); - ASTVec::iterator itend = ch.end(); - for(ASTVec::iterator it = ch.begin(); it < itend; it++) { - eval_children.push_back(CheckBBandCNF_int(newS, *it)); - } - result = CreateSimpForm(k, eval_children); - - cout << "================" << endl << "Checking BB formula:" << form << endl; - cout << "----------------" << endl << "Result:" << result << endl; - - ASTNode replit_eval; - // Compare with replit, if there is one. - ASTNodeMap::iterator replit_it = RepLitMap.find(form); - if (replit_it != RepLitMap.end()) { - ASTNode replit = RepLitMap[form]; - // Replit is symbol or not symbol. - if (SYMBOL == replit.GetKind()) { - replit_eval = SymbolTruthValue(newS, replit); - } - else { - // It's (NOT sym). Get value of sym and complement. - replit_eval = CreateSimpNot(SymbolTruthValue(newS, replit[0])); - } - - cout << "----------------" << endl << "Rep lit: " << replit << endl; - cout << "----------------" << endl << "Rep lit value: " << replit_eval << endl; - - if (result != replit_eval) { - // Hit the panic button. - FatalError("Truth value of BitBlasted formula disagrees with representative literal in CNF."); - } - } - else { - cout << "----------------" << endl << "No rep lit" << endl; - } - - } - } - - return (CheckBBandCNFMemo[form] = result); - } - - /*FUNCTION: constructs counterexample from MINISAT counterexample - * step1 : iterate through MINISAT counterexample and assemble the - * bits for each AST term. Store it in a map from ASTNode to vector - * of bools (bits). - * - * step2: Iterate over the map from ASTNodes->Vector-of-Bools and - * populate the CounterExampleMap data structure (ASTNode -> BVConst) - */ - void BeevMgr::ConstructCounterExample(MINISAT::Solver& newS) { - //iterate over MINISAT counterexample and construct a map from AST - //terms to vector of bools. We need this iteration step because - //MINISAT might return the various bits of a term out of - //order. Therfore, we need to collect all the bits and assemble - //them properly - - if(!newS.okay()) - return; - if(!construct_counterexample) - return; - - CopySolverMap_To_CounterExample(); - for (int i = 0; i < newS.nVars(); i++) { - //Make sure that the MINISAT::Var is defined - if (newS.model[i] != MINISAT::l_Undef) { - - //mapping from MINISAT::Vars to ASTNodes. We do not need to - //print MINISAT vars or CNF vars. - ASTNode s = _SATVar_to_AST[i]; - - //assemble the counterexample here - if(s.GetKind() == BVGETBIT && s[0].GetKind() == SYMBOL) { - ASTNode symbol = s[0]; - unsigned int symbolWidth = symbol.GetValueWidth(); - - //'v' is the map from bit-index to bit-value - hash_map * v; - if(_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end()) - _ASTNode_to_Bitvector[symbol] = new hash_map(symbolWidth); - - //v holds the map from bit-index to bit-value - v = _ASTNode_to_Bitvector[symbol]; - - //kk is the index of BVGETBIT - unsigned int kk = GetUnsignedConst(s[1]); - - //Collect the bits of 'symbol' and store in v. Store in reverse order. - if(newS.model[i]==MINISAT::l_True) - (*v)[(symbolWidth-1) - kk] = true; - else - (*v)[(symbolWidth-1) - kk] = false; - } - else { - if(s.GetKind() == SYMBOL && s.GetType() == BOOLEAN_TYPE) { - const char * zz = s.GetName(); - //if the variables are not cnf variables then add them to the counterexample - if(0 != strncmp("cnf",zz,3) && 0 != strcmp("*TrueDummy*",zz)) { - if(newS.model[i]==MINISAT::l_True) - CounterExampleMap[s] = ASTTrue; - else - CounterExampleMap[s] = ASTFalse; - } - } - } - } - } - - //iterate over the ASTNode_to_Bitvector data-struct and construct - //the the aggregate value of the bitvector, and populate the - //CounterExampleMap datastructure - for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(),itend=_ASTNode_to_Bitvector.end(); - it!=itend;it++) { - ASTNode var = it->first; - //debugging - //cerr << var; - if(SYMBOL != var.GetKind()) - FatalError("ConstructCounterExample: error while constructing counterexample: not a variable: ",var); - - //construct the bitvector value - hash_map * w = it->second; - ASTNode value = BoolVectoBVConst(w, var.GetValueWidth()); - //debugging - //cerr << value; - - //populate the counterexample datastructure. add only scalars - //variables which were declared in the input and newly - //introduced variables for array reads - CounterExampleMap[var] = value; - } - - //In this loop, we compute the value of each array read, the - //corresponding ITE against the counterexample generated above. - for(ASTNodeMap::iterator it=_arrayread_ite.begin(),itend=_arrayread_ite.end(); - it!=itend;it++){ - //the array read - ASTNode arrayread = it->first; - ASTNode value_ite = _arrayread_ite[arrayread]; - - //convert it to a constant array-read and store it in the - //counter-example. First convert the index into a constant. then - //construct the appropriate array-read and store it in the - //counterexample - ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1]); - ASTNode key = CreateTerm(READ,arrayread.GetValueWidth(),arrayread[0],arrayread_index); - - //Get the ITE corresponding to the array-read and convert it - //to a constant against the model - ASTNode value = TermToConstTermUsingModel(value_ite); - //save the result in the counter_example - if(!CheckSubstitutionMap(key)) - CounterExampleMap[key] = value; - } - } //End of ConstructCounterExample - - // FUNCTION: accepts a non-constant term, and returns the - // corresponding constant term with respect to a model. - // - // term READ(A,i) is treated as follows: - // - //1. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead - //1. has value in counterexample), then return the value of the - //1. arrayread. - // - //2. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead - //2. doesn't have value in counterexample), then return the - //2. arrayread itself (normalized such that arrayread has a constant - //2. index) - // - //3. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead - //3. has a value in the counterexample then return the value of the - //3. arrayread. - // - //4. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead - //4. doesn't have a value in the counterexample then return 0 as the - //4. value of the arrayread. - ASTNode BeevMgr::TermToConstTermUsingModel(const ASTNode& t, bool ArrayReadFlag) { - Begin_RemoveWrites = false; - SimplifyWrites_InPlace_Flag = false; - //ASTNode term = SimplifyTerm(t); - ASTNode term = t; - Kind k = term.GetKind(); - - - //cerr << "Input to TermToConstTermUsingModel: " << term << endl; - if(!is_Term_kind(k)) { - FatalError("TermToConstTermUsingModel: The input is not a term: ",term); - } - if(k == WRITE) { - FatalError("TermToConstTermUsingModel: The input has wrong kind: WRITE : ",term); - } - if(k == SYMBOL && BOOLEAN_TYPE == term.GetType()) { - FatalError("TermToConstTermUsingModel: The input has wrong kind: Propositional variable : ",term); - } - - ASTNodeMap::iterator it1; - if((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end()) { - ASTNode val = it1->second; - if(BVCONST != val.GetKind()) { - //CounterExampleMap has two maps rolled into - //one. SubstitutionMap and SolverMap. - // - //recursion is fine here. There are two maps that are checked - //here. One is the substitutionmap. We garuntee that the value - //of a key in the substitutionmap is always a constant. - // - //in the SolverMap we garuntee that "term" does not occur in - //the value part of the map - if(term == val) { - FatalError("TermToConstTermUsingModel: The input term is stored as-is " - "in the CounterExample: Not ok: ",term); - } - return TermToConstTermUsingModel(val,ArrayReadFlag); - } - else { - return val; - } - } - - ASTNode output; - switch(k) { - case BVCONST: - output = term; - break; - case SYMBOL: { - if(term.GetType() == ARRAY_TYPE) { - return term; - } - - //when all else fails set symbol values to some constant by - //default. if the variable is queried the second time then add 1 - //to and return the new value. - ASTNode zero = CreateZeroConst(term.GetValueWidth()); - output = zero; - break; - } - case READ: { - ASTNode arrName = term[0]; - ASTNode index = term[1]; - if(0 == arrName.GetIndexWidth()) { - FatalError("TermToConstTermUsingModel: array has 0 index width: ",arrName); - } - - //READ over a WRITE - if(WRITE == arrName.GetKind()) { - ASTNode wrtterm = Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag); - if(wrtterm == term) { - FatalError("TermToConstTermUsingModel: Read_Over_Write term must be expanded into an ITE", term); - } - ASTNode rtterm = TermToConstTermUsingModel(wrtterm,ArrayReadFlag); - return rtterm; - } - //READ over an ITE - if(ITE == arrName.GetKind()) { - arrName = TermToConstTermUsingModel(arrName,ArrayReadFlag); - } - - ASTNode modelentry; - if(CounterExampleMap.find(index) != CounterExampleMap.end()) { - //index has a const value in the CounterExampleMap - ASTNode indexVal = CounterExampleMap[index]; - modelentry = CreateTerm(READ, arrName.GetValueWidth(), arrName, indexVal); - } - else { - //index does not have a const value in the CounterExampleMap. compute it. - ASTNode indexconstval = TermToConstTermUsingModel(index,ArrayReadFlag); - //update model with value of the index - //CounterExampleMap[index] = indexconstval; - modelentry = CreateTerm(READ,arrName.GetValueWidth(), arrName,indexconstval); - } - //modelentry is now an arrayread over a constant index - BVTypeCheck(modelentry); - - //if a value exists in the CounterExampleMap then return it - if(CounterExampleMap.find(modelentry) != CounterExampleMap.end()) { - output = TermToConstTermUsingModel(CounterExampleMap[modelentry],ArrayReadFlag); - } - else if(ArrayReadFlag) { - //return the array read over a constantindex - output = modelentry; - } - else { - //when all else fails set symbol values to some constant by - //default. if the variable is queried the second time then add 1 - //to and return the new value. - ASTNode zero = CreateZeroConst(modelentry.GetValueWidth()); - output = zero; - } - break; - } - case ITE: { - ASTNode condcompute = ComputeFormulaUsingModel(term[0]); - if(ASTTrue == condcompute) { - output = TermToConstTermUsingModel(term[1],ArrayReadFlag); - } - else if(ASTFalse == condcompute) { - output = TermToConstTermUsingModel(term[2],ArrayReadFlag); - } - else { - cerr << "TermToConstTermUsingModel: termITE: value of conditional is wrong: " << condcompute << endl; - FatalError(" TermToConstTermUsingModel: termITE: cannot compute ITE conditional against model: ",term); - } - break; - } - default: { - ASTVec c = term.GetChildren(); - ASTVec o; - for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) { - ASTNode ff = TermToConstTermUsingModel(*it,ArrayReadFlag); - o.push_back(ff); - } - output = CreateTerm(k,term.GetValueWidth(),o); - //output is a CONST expression. compute its value and store it - //in the CounterExampleMap - ASTNode oo = BVConstEvaluator(output); - //the return value - output = oo; - break; - } - } - - //when this flag is false, we should compute the arrayread to a - //constant. this constant is stored in the counter_example - //datastructure - if(!ArrayReadFlag) { - CounterExampleMap[term] = output; - } - - //cerr << "Output to TermToConstTermUsingModel: " << output << endl; - return output; - } //End of TermToConstTermUsingModel - - //Expands read-over-write by evaluating (readIndex=writeIndex) for - //every writeindex until, either it evaluates to TRUE or all - //(readIndex=writeIndex) evaluate to FALSE - ASTNode BeevMgr::Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool arrayread_flag) { - if(READ != term.GetKind() && - WRITE != term[0].GetKind()) { - FatalError("RemovesWrites: Input must be a READ over a WRITE",term); - } - - ASTNode output; - ASTNodeMap::iterator it1; - if((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end()) { - ASTNode val = it1->second; - if(BVCONST != val.GetKind()) { - //recursion is fine here. There are two maps that are checked - //here. One is the substitutionmap. We garuntee that the value - //of a key in the substitutionmap is always a constant. - if(term == val) { - FatalError("TermToConstTermUsingModel: The input term is stored as-is " - "in the CounterExample: Not ok: ",term); - } - return TermToConstTermUsingModel(val,arrayread_flag); - } - else { - return val; - } - } - - unsigned int width = term.GetValueWidth(); - ASTNode writeA = ASTTrue; - ASTNode newRead = term; - ASTNode readIndex = TermToConstTermUsingModel(newRead[1],false); - //iteratively expand read-over-write, and evaluate against the - //model at every iteration - do { - ASTNode write = newRead[0]; - writeA = write[0]; - ASTNode writeIndex = TermToConstTermUsingModel(write[1],false); - ASTNode writeVal = TermToConstTermUsingModel(write[2],false); - - ASTNode cond = ComputeFormulaUsingModel(CreateSimplifiedEQ(writeIndex,readIndex)); - if(ASTTrue == cond) { - //found the write-value. return it - output = writeVal; - CounterExampleMap[term] = output; - return output; - } - - newRead = CreateTerm(READ,width,writeA,readIndex); - } while(READ == newRead.GetKind() && WRITE == newRead[0].GetKind()); - - output = TermToConstTermUsingModel(newRead,arrayread_flag); - - //memoize - CounterExampleMap[term] = output; - return output; - } //Exand_ReadOverWrite_To_ITE_UsingModel() - - /* FUNCTION: accepts a non-constant formula, and checks if the - * formula is ASTTrue or ASTFalse w.r.t to a model - */ - ASTNode BeevMgr::ComputeFormulaUsingModel(const ASTNode& form) { - ASTNode in = form; - Kind k = form.GetKind(); - if(!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType())) { - FatalError(" ComputeConstFormUsingModel: The input is a non-formula: ", form); - } - - //cerr << "Input to ComputeFormulaUsingModel:" << form << endl; - ASTNodeMap::iterator it1; - if((it1 = ComputeFormulaMap.find(form)) != ComputeFormulaMap.end()) { - ASTNode res = it1->second; - if(ASTTrue == res || ASTFalse == res) { - return res; - } - else { - FatalError("ComputeFormulaUsingModel: The value of a formula must be TRUE or FALSE:", form); - } - } - - ASTNode t0,t1; - ASTNode output = ASTFalse; - switch(k) { - case TRUE: - case FALSE: - output = form; - break; - case SYMBOL: - if(BOOLEAN_TYPE != form.GetType()) - FatalError(" ComputeFormulaUsingModel: Non-Boolean variables are not formulas",form); - if(CounterExampleMap.find(form) != CounterExampleMap.end()) { - ASTNode counterexample_val = CounterExampleMap[form]; - if(!VarSeenInTerm(form,counterexample_val)) { - output = ComputeFormulaUsingModel(counterexample_val); - } - else { - output = counterexample_val; - } - } - else - output = ASTFalse; - break; - case EQ: - case NEQ: - case BVLT: - case BVLE: - case BVGT: - case BVGE: - case BVSLT: - case BVSLE: - case BVSGT: - case BVSGE: - //convert form[0] into a constant term - t0 = TermToConstTermUsingModel(form[0],false); - //convert form[0] into a constant term - t1 = TermToConstTermUsingModel(form[1],false); - output = BVConstEvaluator(CreateNode(k,t0,t1)); - - //evaluate formula to false if bvdiv execption occurs while - //counterexample is being checked during refinement. - if(bvdiv_exception_occured && - counterexample_checking_during_refinement) { - output = ASTFalse; - } - break; - case NAND: { - ASTNode o = ASTTrue; - for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) - if(ASTFalse == ComputeFormulaUsingModel(*it)) { - o = ASTFalse; - break; - } - if(o == ASTTrue) - output = ASTFalse; - else - output = ASTTrue; - break; - } - case NOR: { - ASTNode o = ASTFalse; - for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) - if(ASTTrue == ComputeFormulaUsingModel(*it)) { - o = ASTTrue; - break; - } - if(o == ASTTrue) - output = ASTFalse; - else - output = ASTTrue; - break; - } - case NOT: - if(ASTTrue == ComputeFormulaUsingModel(form[0])) - output = ASTFalse; - else - output = ASTTrue; - break; - case OR: - for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) - if(ASTTrue == ComputeFormulaUsingModel(*it)) - output = ASTTrue; - break; - case AND: - output = ASTTrue; - for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) { - if(ASTFalse == ComputeFormulaUsingModel(*it)) { - output = ASTFalse; - break; - } - } - break; - case XOR: - t0 = ComputeFormulaUsingModel(form[0]); - t1 = ComputeFormulaUsingModel(form[1]); - if((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1)) - output = ASTFalse; - else - output = ASTTrue; - break; - case IFF: - t0 = ComputeFormulaUsingModel(form[0]); - t1 = ComputeFormulaUsingModel(form[1]); - if((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1)) - output = ASTTrue; - else - output = ASTFalse; - break; - case IMPLIES: - t0 = ComputeFormulaUsingModel(form[0]); - t1 = ComputeFormulaUsingModel(form[1]); - if((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1)) - output = ASTTrue; - else - output = ASTFalse; - break; - case ITE: - t0 = ComputeFormulaUsingModel(form[0]); - if(ASTTrue == t0) - output = ComputeFormulaUsingModel(form[1]); - else if(ASTFalse == t0) - output = ComputeFormulaUsingModel(form[2]); - else - FatalError("ComputeFormulaUsingModel: ITE: something is wrong with the formula: ",form); - break; - default: - FatalError(" ComputeFormulaUsingModel: the kind has not been implemented", ASTUndefined); - break; - } - - //cout << "ComputeFormulaUsingModel output is:" << output << endl; - ComputeFormulaMap[form] = output; - return output; - } - - void BeevMgr::CheckCounterExample(bool t) { - // FIXME: Code is more useful if enable flags are check OUTSIDE the method. - // If I want to check a counterexample somewhere, I don't want to have to set - // the flag in order to make it actualy happen! - - if(!check_counterexample) { - return; - } - - //input is valid, no counterexample to check - if(ValidFlag) - return; - - //t is true if SAT solver generated a counterexample, else it is false - if(!t) - FatalError("CheckCounterExample: No CounterExample to check", ASTUndefined); - const ASTVec c = GetAsserts(); - for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) - if(ASTFalse == ComputeFormulaUsingModel(*it)) - FatalError("CheckCounterExample:counterexample bogus:"\ - "assert evaluates to FALSE under counterexample: NOT OK",*it); - - if(ASTTrue == ComputeFormulaUsingModel(_current_query)) - FatalError("CheckCounterExample:counterexample bogus:"\ - "query evaluates to TRUE under counterexample: NOT OK",_current_query); - } - - /* FUNCTION: prints a counterexample for INVALID inputs. iterate - * through the CounterExampleMap data structure and print it to - * stdout - */ - void BeevMgr::PrintCounterExample(bool t, std::ostream& os) { - //global command-line option - // FIXME: This should always print the counterexample. If you want - // to turn it off, check the switch at the point of call. - if(!print_counterexample) - return; - - //input is valid, no counterexample to print - if(ValidFlag) - return; - - //if this option is true then print the way dawson wants using a - //different printer. do not use this printer. - if(print_arrayval_declaredorder) - return; - - //t is true if SAT solver generated a counterexample, else it is - //false - if(!t) { - cerr << "PrintCounterExample: No CounterExample to print: " << endl; - return; - } - - //os << "\nCOUNTEREXAMPLE: \n" << endl; - ASTNodeMap::iterator it = CounterExampleMap.begin(); - ASTNodeMap::iterator itend = CounterExampleMap.end(); - for(;it!=itend;it++) { - ASTNode f = it->first; - ASTNode se = it->second; - - if(ARRAY_TYPE == se.GetType()) { - FatalError("TermToConstTermUsingModel: entry in counterexample is an arraytype. bogus:",se); - } - - //skip over introduced variables - if(f.GetKind() == SYMBOL && (_introduced_symbols.find(f) != _introduced_symbols.end())) - continue; - if(f.GetKind() == SYMBOL || - (f.GetKind() == READ && f[0].GetKind() == SYMBOL && f[1].GetKind() == BVCONST)) { - os << "ASSERT( "; - f.PL_Print(os,0); - os << " = "; - if(BITVECTOR_TYPE == se.GetType()) { - TermToConstTermUsingModel(se,false).PL_Print(os,0); - } - else { - se.PL_Print(os,0); - } - os << " );" << endl; - } - } - //os << "\nEND OF COUNTEREXAMPLE" << endl; - } //End of PrintCounterExample - - /* iterate through the CounterExampleMap data structure and print it - * to stdout. this function prints only the declared array variables - * IN the ORDER in which they were declared. It also assumes that - * the variables are of the form 'varname_number'. otherwise it will - * not print anything. This function was specifically written for - * Dawson Engler's group (bug finding research group at Stanford) - */ - void BeevMgr::PrintCounterExample_InOrder(bool t) { - //global command-line option to print counterexample. we do not - //want both counterexample printers to print at the sametime. - // FIXME: This should always print the counterexample. If you want - // to turn it off, check the switch at the point of call. - if(print_counterexample) - return; - - //input is valid, no counterexample to print - if(ValidFlag) - return; - - //print if the commandline option is '-q'. allows printing the - //counterexample in order. - if(!print_arrayval_declaredorder) - return; - - //t is true if SAT solver generated a counterexample, else it is - //false - if(!t) { - cerr << "PrintCounterExample: No CounterExample to print: " << endl; - return; - } - - //vector to store the integer values - std::vector out_int; - cout << "% "; - for(ASTVec::iterator it=_special_print_set.begin(),itend=_special_print_set.end(); - it!=itend;it++) { - if(ARRAY_TYPE == it->GetType()) { - //get the name of the variable - const char * c = it->GetName(); - std::string ss(c); - if(!(0 == strncmp(ss.c_str(),"ini_",4))) - continue; - reverse(ss.begin(),ss.end()); - - //cout << "debugging: " << ss; - size_t pos = ss.find('_',0); - if(!(0 < pos && pos < ss.size())) - continue; - - //get the associated length - std::string sss = ss.substr(0,pos); - reverse(sss.begin(),sss.end()); - int n = atoi(sss.c_str()); - - it->PL_Print(cout,2); - for(int j=0;j < n; j++) { - ASTNode index = CreateBVConst(it->GetIndexWidth(),j); - ASTNode readexpr = CreateTerm(READ,it->GetValueWidth(),*it,index); - ASTNode val = GetCounterExample(t, readexpr); - //cout << "ASSERT( "; - //cout << " = "; - out_int.push_back(GetUnsignedConst(val)); - //cout << "\n"; - } - } - } - cout << endl; - for(unsigned int jj=0; jj < out_int.size();jj++) - cout << out_int[jj] << endl; - cout << endl; - } //End of PrintCounterExample_InOrder - - /* FUNCTION: queries the CounterExampleMap object with 'expr' and - * returns the corresponding counterexample value. - */ - ASTNode BeevMgr::GetCounterExample(bool t, const ASTNode& expr) { - //input is valid, no counterexample to get - if(ValidFlag) - return ASTUndefined; - - if(BOOLEAN_TYPE == expr.GetType()) { - return ComputeFormulaUsingModel(expr); - } - - if(BVCONST == expr.GetKind()) { - return expr; - } - - ASTNodeMap::iterator it; - ASTNode output; - if((it = CounterExampleMap.find(expr)) != CounterExampleMap.end()) - output = TermToConstTermUsingModel(CounterExampleMap[expr],false); - else - output = CreateZeroConst(expr.GetValueWidth()); - return output; - } //End of GetCounterExample - - // FIXME: Don't use numeric codes. Use an enum type! - //Acceps a query, calls the SAT solver and generates Valid/InValid. - //if returned 0 then input is INVALID - //if returned 1 then input is VALID - //if returned 2 then ERROR - int BeevMgr::TopLevelSAT( const ASTNode& inputasserts, const ASTNode& query) { - /******start solving**********/ - ASTNode q = CreateNode(AND, inputasserts, CreateNode(NOT,query)); - ASTNode orig_input = q; - ASTNodeStats("input asserts and query: ", q); - - ASTNode newq = q; - //round of substitution, solving, and simplification. ensures that - //DAG is minimized as much as possibly, and ideally should - //garuntee that all liketerms in BVPLUSes have been combined. - BVSolver bvsolver(this); - SimplifyWrites_InPlace_Flag = false; - Begin_RemoveWrites = false; - start_abstracting = false; - TermsAlreadySeenMap.clear(); - do { - q = newq; - newq = CreateSubstitutionMap(newq); - //ASTNodeStats("after pure substitution: ", newq); - newq = SimplifyFormula_TopLevel(newq,false); - //ASTNodeStats("after simplification: ", newq); - //newq = bvsolver.TopLevelBVSolve(newq); - //ASTNodeStats("after solving: ", newq); - }while(q!=newq); - - ASTNodeStats("Before SimplifyWrites_Inplace begins: ", newq); - SimplifyWrites_InPlace_Flag = true; - Begin_RemoveWrites = false; - start_abstracting = false; - TermsAlreadySeenMap.clear(); - do { - q = newq; - //newq = CreateSubstitutionMap(newq); - //ASTNodeStats("after pure substitution: ", newq); - newq = SimplifyFormula_TopLevel(newq,false); - //ASTNodeStats("after simplification: ", newq); - newq = bvsolver.TopLevelBVSolve(newq); - //ASTNodeStats("after solving: ", newq); - }while(q!=newq); - ASTNodeStats("After SimplifyWrites_Inplace: ", newq); - - start_abstracting = (arraywrite_refinement) ? true : false; - SimplifyWrites_InPlace_Flag = false; - Begin_RemoveWrites = (start_abstracting) ? false : true; - if(start_abstracting) { - ASTNodeStats("before abstraction round begins: ", newq); - } - - TermsAlreadySeenMap.clear(); - do { - q = newq; - //newq = CreateSubstitutionMap(newq); - //Begin_RemoveWrites = true; - //ASTNodeStats("after pure substitution: ", newq); - newq = SimplifyFormula_TopLevel(newq,false); - //ASTNodeStats("after simplification: ", newq); - //newq = bvsolver.TopLevelBVSolve(newq); - //ASTNodeStats("after solving: ", newq); - }while(q!=newq); - - if(start_abstracting) { - ASTNodeStats("After abstraction: ", newq); - } - start_abstracting = false; - SimplifyWrites_InPlace_Flag = false; - Begin_RemoveWrites = false; - - newq = TransformFormula(newq); - ASTNodeStats("after transformation: ", newq); - TermsAlreadySeenMap.clear(); - - int res; - //solver instantiated here - MINISAT::Solver newS; - if(arrayread_refinement) { - counterexample_checking_during_refinement = true; - } - - //call SAT and check the result - res = CallSAT_ResultCheck(newS,newq,orig_input); - if(2 != res) { - CountersAndStats("print_func_stats"); - return res; - } - - res = SATBased_ArrayReadRefinement(newS,newq,orig_input); - if(2 != res) { - CountersAndStats("print_func_stats"); - return res; - } - - res = SATBased_ArrayWriteRefinement(newS,orig_input); - if(2 != res) { - CountersAndStats("print_func_stats"); - return res; - } - - res = SATBased_ArrayReadRefinement(newS,newq,orig_input); - if(2 != res) { - CountersAndStats("print_func_stats"); - return res; - } - - FatalError("TopLevelSAT: reached the end without proper conclusion:" - "either a divide by zero in the input or a bug in STP"); - //bogus return to make the compiler shut up - return 2; - } //End of TopLevelSAT - - //go over the list of indices for each array, and generate Leibnitz - //axioms. Then assert these axioms into the SAT solver. Check if the - //addition of the new constraints has made the bogus counterexample - //go away. if yes, return the correct answer. if no, continue adding - //Leibnitz axioms systematically. - // FIXME: What it really does is, for each array, loop over each index i. - // inside that loop, it finds all the true and false axioms with i as first - // index. When it's got them all, it adds the false axioms to the formula - // and re-solves, and returns if the result is correct. Otherwise, it - // goes on to the next index. - // If it gets through all the indices without a correct result (which I think - // is impossible, but this is pretty confusing), it then solves with all - // the true axioms, too. - // This is not the most obvious way to do it, and I don't know how it - // compares with other approaches (e.g., one false axiom at a time or - // all the false axioms each time). - int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, - const ASTNode& q, const ASTNode& orig_input) { - if(!arrayread_refinement) - FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); - - ASTVec FalseAxiomsVec, RemainingAxiomsVec; - RemainingAxiomsVec.push_back(ASTTrue); - FalseAxiomsVec.push_back(ASTTrue); - - //in these loops we try to construct Leibnitz axioms and add it to - //the solve(). We add only those axioms that are false in the - //current counterexample. we keep adding the axioms until there - //are no more axioms to add - // - //for each array, fetch its list of indices seen so far - for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); - iset!=iset_end;iset++) { - ASTVec listOfIndices = iset->second; - //loop over the list of indices for the array and create LA, and add to q - for(ASTVec::iterator it=listOfIndices.begin(),itend=listOfIndices.end();it!=itend;it++) { - if(BVCONST == it->GetKind()) { - continue; - } - - ASTNode the_index = *it; - //get the arrayname - ASTNode ArrName = iset->first; - // if(SYMBOL != ArrName.GetKind()) - // FatalError("SATBased_ArrayReadRefinement: arrname is not a SYMBOL",ArrName); - ASTNode arr_read1 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index); - //get the variable corresponding to the array_read1 - ASTNode arrsym1 = _arrayread_symbol[arr_read1]; - if(!(SYMBOL == arrsym1.GetKind() || BVCONST == arrsym1.GetKind())) - FatalError("TopLevelSAT: refinementloop:term arrsym1 corresponding to READ must be a var", arrsym1); - - //we have nonconst index here. create Leibnitz axiom for it - //w.r.t every index in listOfIndices - for(ASTVec::iterator it1=listOfIndices.begin(),itend1=listOfIndices.end(); - it1!=itend1;it1++) { - ASTNode compare_index = *it1; - //do not compare with yourself - if(the_index == compare_index) - continue; - - //prepare for SAT LOOP - //first construct the antecedent for the LA axiom - ASTNode eqOfIndices = - (exprless(the_index,compare_index)) ? - CreateSimplifiedEQ(the_index,compare_index) : CreateSimplifiedEQ(compare_index,the_index); - - ASTNode arr_read2 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index); - //get the variable corresponding to the array_read2 - ASTNode arrsym2 = _arrayread_symbol[arr_read2]; - if(!(SYMBOL == arrsym2.GetKind() || BVCONST == arrsym2.GetKind())) - FatalError("TopLevelSAT: refinement loop:" - "term arrsym2 corresponding to READ must be a var", arrsym2); - - ASTNode eqOfReads = CreateSimplifiedEQ(arrsym1,arrsym2); - //construct appropriate Leibnitz axiom - ASTNode LeibnitzAxiom = CreateNode(IMPLIES, eqOfIndices, eqOfReads); - if(ASTFalse == ComputeFormulaUsingModel(LeibnitzAxiom)) - //FalseAxioms = CreateNode(AND,FalseAxioms,LeibnitzAxiom); - FalseAxiomsVec.push_back(LeibnitzAxiom); - else - //RemainingAxioms = CreateNode(AND,RemainingAxioms,LeibnitzAxiom); - RemainingAxiomsVec.push_back(LeibnitzAxiom); - } - ASTNode FalseAxioms = (FalseAxiomsVec.size()>1) ? CreateNode(AND,FalseAxiomsVec) : FalseAxiomsVec[0]; - ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms); - int res2 = CallSAT_ResultCheck(newS,FalseAxioms,orig_input); - if(2!=res2) { - return res2; - } - } - } - ASTNode RemainingAxioms = (RemainingAxiomsVec.size()>1) ? CreateNode(AND,RemainingAxiomsVec):RemainingAxiomsVec[0]; - ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms); - return CallSAT_ResultCheck(newS,RemainingAxioms,orig_input); - } //end of SATBased_ArrayReadRefinement - - ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, const ASTNode& newvar) { - if(READ != term.GetKind() && WRITE != term[0].GetKind()) { - FatalError("Create_ArrayWriteAxioms: Input must be a READ over a WRITE",term); - } - - ASTNode lhs = newvar; - ASTNode rhs = term; - ASTNode arraywrite_axiom = CreateSimplifiedEQ(lhs,rhs); - return arraywrite_axiom; - }//end of Create_ArrayWriteAxioms() - - int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input) { - ASTNode writeAxiom; - ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin(); - ASTNodeMap::iterator itend = ReadOverWrite_NewName_Map.end(); - //int count = 0; - //int num_write_axioms = ReadOverWrite_NewName_Map.size(); - - ASTVec FalseAxioms, RemainingAxioms; - FalseAxioms.push_back(ASTTrue); - RemainingAxioms.push_back(ASTTrue); - for(;it!=itend;it++) { - //Guided refinement starts here - ComputeFormulaMap.clear(); - writeAxiom = Create_ArrayWriteAxioms(it->first,it->second); - if(ASTFalse == ComputeFormulaUsingModel(writeAxiom)) { - writeAxiom = TransformFormula(writeAxiom); - FalseAxioms.push_back(writeAxiom); - } - else { - writeAxiom = TransformFormula(writeAxiom); - RemainingAxioms.push_back(writeAxiom); - } - } - - writeAxiom = (FalseAxioms.size() != 1) ? CreateNode(AND,FalseAxioms) : FalseAxioms[0]; - ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom); - int res2 = CallSAT_ResultCheck(newS,writeAxiom,orig_input); - if(2!=res2) { - return res2; - } - - writeAxiom = (RemainingAxioms.size() != 1) ? CreateNode(AND,RemainingAxioms) : RemainingAxioms[0]; - ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom); - res2 = CallSAT_ResultCheck(newS,writeAxiom,orig_input); - if(2!=res2) { - return res2; - } - - return 2; - } //end of SATBased_ArrayWriteRefinement - - //Check result after calling SAT FIXME: Document arguments in - //comments, and give them meaningful names. How is anyone supposed - //to know what "q" is? - int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, - const ASTNode& q, const ASTNode& orig_input) { - //Bitblast, CNF, call SAT now - ASTNode BBFormula = BBForm(q); - //ASTNodeStats("after bitblasting", BBFormula); - ClauseList *cllp = ToCNF(BBFormula); - // if(stats && print_nodes) { - // cout << "\nClause list" << endl; - // PrintClauseList(cout, *cllp); - // cerr << "\n finished printing clauselist\n"; - // } - - bool sat = toSATandSolve(newS,*cllp); - // Temporary debugging call. - // CheckBBandCNF(newS, BBFormula); - - DeleteClauseList(cllp); - if(!sat) { - PrintOutput(true); - return 1; - } - else if(newS.okay()) { - CounterExampleMap.clear(); - ConstructCounterExample(newS); - if (stats && print_nodes) { - PrintSATModel(newS); - } - //check if the counterexample is good or not - ComputeFormulaMap.clear(); - if(counterexample_checking_during_refinement) - bvdiv_exception_occured = false; - ASTNode orig_result = ComputeFormulaUsingModel(orig_input); - if(!(ASTTrue == orig_result || ASTFalse == orig_result)) - FatalError("TopLevelSat: Original input must compute to true or false against model"); - -// if(!arrayread_refinement && !(ASTTrue == orig_result)) { -// print_counterexample = true; -// PrintCounterExample(true); -// FatalError("counterexample bogus : arrayread_refinement is switched off: " -// "EITHER all LA axioms have not been added OR bitblaster() or ToCNF()" -// "or satsolver() or counterexamplechecker() have a bug"); -// } - - // if the counterexample is indeed a good one, then return - // invalid - if(ASTTrue == orig_result) { - CheckCounterExample(newS.okay()); - PrintOutput(false); - PrintCounterExample(newS.okay()); - PrintCounterExample_InOrder(newS.okay()); - return 0; - } - // counterexample is bogus: flag it - else { - if(stats && print_nodes) { - cout << "Supposedly bogus one: \n"; - bool tmp = print_counterexample; - print_counterexample = true; - PrintCounterExample(true); - print_counterexample = tmp; - } - - return 2; - } - } - else { - PrintOutput(true); - return -100; - } - } //end of CALLSAT_ResultCheck - - - //FUNCTION: this function accepts a boolvector and returns a BVConst - ASTNode BeevMgr::BoolVectoBVConst(hash_map * w, unsigned int l) { - unsigned len = w->size(); - if(l < len) - FatalError("BoolVectorBVConst : length of bitvector does not match hash_map size:",ASTUndefined,l); - std::string cc; - for(unsigned int jj = 0; jj < l; jj++) { - if((*w)[jj] == true) - cc += '1'; - else if((*w)[jj] == false) - cc += '0'; - else - cc += '0'; - } - return CreateBVConst(cc.c_str(),2); - } - - void BeevMgr::PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS) { - if(!print_sat_varorder) - return; - - ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin(); - ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end(); - - cout << init_msg; - cout << ": Printing activity levels of variables\n"; - for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){ - cout << (it->second) << " : "; - (it->first).PL_Print(cout,0); - cout << " : "; - cout << newS.returnActivity(it->second) << endl; - } - } - - //this function biases the activity levels of MINISAT variables. - void BeevMgr::ChangeActivityLevels_Of_SATVars(MINISAT::Solver& newS) { - if(!variable_activity_optimize) - return; - - ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin(); - ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end(); - - unsigned int index=1; - double base = 2; - for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){ - ASTNode n = it->first; - - if(BVGETBIT == n.GetKind() || NOT == n.GetKind()) { - if(BVGETBIT == n.GetKind()) - index = GetUnsignedConst(n[1]); - else if (NOT == n.GetKind() && BVGETBIT == n[0].GetKind()) - index = GetUnsignedConst(n[0][1]); - else - index = 0; - double initial_activity = pow(base,(double)index); - newS.updateInitialActivity(it->second,initial_activity); - } - else { - double initial_activity = pow(base,pow(base,(double)index)); - newS.updateInitialActivity(it->second,initial_activity); - } - } - } - - //This function prints the output of the STP solver - void BeevMgr::PrintOutput(bool true_iff_valid) { - //self-explanatory - if(true_iff_valid) { - ValidFlag = true; - if(print_output) { - if(smtlib_parser_enable) - cout << "unsat\n"; - else - cout << "Valid.\n"; - } - } - else { - ValidFlag = false; - if(print_output) { - if(smtlib_parser_enable) - cout << "sat\n"; - else - cout << "Invalid.\n"; - } - } - } -} //end of namespace BEEV diff --git a/stp/AST/Transform.cpp b/stp/AST/Transform.cpp deleted file mode 100644 index 598b831e..00000000 --- a/stp/AST/Transform.cpp +++ /dev/null @@ -1,492 +0,0 @@ -/******************************************************************** - * 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" -#include -#include -namespace BEEV { - - //Translates signed BVDIV/BVMOD into unsigned variety - ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) { - if(!(SBVMOD == in.GetKind() || SBVDIV == in.GetKind())) { - FatalError("TranslateSignedDivMod: input must be signed DIV/MOD\n",in); - } - - ASTNode dividend = in[0]; - ASTNode divisor = in[1]; - unsigned len = in.GetValueWidth(); - if(SBVMOD == in.GetKind()) { - //if(TopBit(dividend)==1) - // - //then -BVMOD(-dividend,abs(divisor)) - // - //else BVMOD(dividend,abs(divisor)) - - //create the condition for the dividend - ASTNode hi1 = CreateBVConst(32,len-1); - ASTNode one = CreateOneConst(1); - ASTNode cond = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)); - - //create the condition and conditional for the divisor - ASTNode cond_divisor = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)); - ASTNode pos_divisor = CreateTerm(ITE,len,cond_divisor,CreateTerm(BVUMINUS,len,divisor),divisor); - - //create the modulus term for each case - ASTNode modnode = CreateTerm(BVMOD,len,dividend,pos_divisor); - ASTNode minus_modnode = CreateTerm(BVMOD,len,CreateTerm(BVUMINUS,len,dividend),pos_divisor); - minus_modnode = CreateTerm(BVUMINUS,len,minus_modnode); - - //put everything together, simplify, and return - ASTNode n = CreateTerm(ITE,len,cond,minus_modnode,modnode); - return SimplifyTerm_TopLevel(n); - } - - //now handle the BVDIV case - //if topBit(dividend) is 1 and topBit(divisor) is 0 - // - //then output is -BVDIV(-dividend,divisor) - // - //elseif topBit(dividend) is 0 and topBit(divisor) is 1 - // - //then output is -BVDIV(dividend,-divisor) - // - //elseif topBit(dividend) is 1 and topBit(divisor) is 1 - // - // then output is BVDIV(-dividend,-divisor) - // - //else simply output BVDIV(dividend,divisor) - ASTNode hi1 = CreateBVConst(32,len-1); - ASTNode zero = CreateZeroConst(1); - ASTNode one = CreateOneConst(1); - ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor); - - ASTNode cond1 = CreateNode(AND, - CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)), - CreateNode(EQ,one, CreateTerm(BVEXTRACT,1,divisor,hi1,hi1))); - ASTNode minus_divnode1 = CreateTerm(BVDIV,len, - dividend, - CreateTerm(BVUMINUS,len,divisor)); - minus_divnode1 = CreateTerm(BVUMINUS,len,minus_divnode1); - - ASTNode cond2 = CreateNode(AND, - CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)), - CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1))); - ASTNode minus_divnode2 = CreateTerm(BVDIV,len, - CreateTerm(BVUMINUS,len,dividend), - divisor); - minus_divnode2 = CreateTerm(BVUMINUS,len,minus_divnode2); - - ASTNode cond3 = CreateNode(AND, - CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)), - CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1))); - ASTNode minus_divnode3 = CreateTerm(BVDIV,len, - CreateTerm(BVUMINUS,len,dividend), - CreateTerm(BVUMINUS,len,divisor)); - ASTNode n = CreateTerm(ITE,len, - cond1, - minus_divnode1, - CreateTerm(ITE,len, - cond2, - minus_divnode2, - CreateTerm(ITE,len, - cond3, - minus_divnode3, - divnode))); - return SimplifyTerm_TopLevel(n); - }//end of TranslateSignedDivMod() - - ASTNode BeevMgr::TransformFormula(const ASTNode& form) { - ASTNode result; - - ASTNode simpleForm = form; - Kind k = simpleForm.GetKind(); - if(!(is_Form_kind(k) && BOOLEAN_TYPE == simpleForm.GetType())) { - //FIXME: "You have inputted a NON-formula"? - FatalError("TransformFormula: You have input a NON-formula",simpleForm); - } - - ASTNodeMap::iterator iter; - if((iter = TransformMap.find(simpleForm)) != TransformMap.end()) - return iter->second; - - switch(k) { - case TRUE: - case FALSE: { - result = simpleForm; - break; - } - case NOT: { - ASTVec c; - c.push_back(TransformFormula(simpleForm[0])); - result = CreateNode(NOT,c); - break; - } - case BVLT: - case BVLE: - case BVGT: - case BVGE: - case BVSLT: - case BVSLE: - case BVSGT: - case BVSGE: - case NEQ: { - ASTVec c; - c.push_back(TransformTerm(simpleForm[0])); - c.push_back(TransformTerm(simpleForm[1])); - result = CreateNode(k,c); - break; - } - case EQ: { - ASTNode term1 = TransformTerm(simpleForm[0]); - ASTNode term2 = TransformTerm(simpleForm[1]); - result = CreateSimplifiedEQ(term1,term2); - break; - } - case AND: - case OR: - case NAND: - case NOR: - case IFF: - case XOR: - case ITE: - case IMPLIES: { - ASTVec vec; - ASTNode o; - for (ASTVec::const_iterator it = simpleForm.begin(),itend=simpleForm.end(); it != itend; it++){ - o = TransformFormula(*it); - vec.push_back(o); - } - - result = CreateNode(k, vec); - break; - } - default: - if(k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType()) - result = simpleForm; - else { - cerr << "The input is: " << simpleForm << endl; - cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl; - FatalError("TransformFormula: Illegal kind: ",ASTUndefined, k); - } - break; - } - //BVTypeCheck(result); - TransformMap[simpleForm] = result; - return result; - } //End of TransformFormula - - ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) { - ASTNode result; - ASTNode term = inputterm; - - Kind k = term.GetKind(); - if(!is_Term_kind(k)) - FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k); - ASTNodeMap::iterator iter; - if((iter = TransformMap.find(term)) != TransformMap.end()) - return iter->second; - switch(k) { - case SYMBOL: { - // ASTNodeMap::iterator itsym; -// if((itsym = CounterExampleMap.find(term)) != CounterExampleMap.end()) -// result = itsym->second; -// else - result = term; - break; - } - case BVCONST: - result = term; - break; - case WRITE: - FatalError("TransformTerm: this kind is not supported",term); - break; - case READ: - result = TransformArray(term); - break; - case ITE: { - ASTNode cond = term[0]; - ASTNode thn = term[1]; - ASTNode els = term[2]; - cond = TransformFormula(cond); - thn = TransformTerm(thn); - els = TransformTerm(els); - //result = CreateTerm(ITE,term.GetValueWidth(),cond,thn,els); - result = CreateSimplifiedTermITE(cond,thn,els); - result.SetIndexWidth(term.GetIndexWidth()); - break; - } - default: { - ASTVec c = term.GetChildren(); - ASTVec::iterator it = c.begin(); - ASTVec::iterator itend = c.end(); - unsigned width = term.GetValueWidth(); - unsigned indexwidth = term.GetIndexWidth(); - ASTVec o; - for(;it!=itend;it++) { - o.push_back(TransformTerm(*it)); - } - - result = CreateTerm(k,width,o); - result.SetIndexWidth(indexwidth); - - if(SBVDIV == result.GetKind() || SBVMOD == result.GetKind()) { - result = TranslateSignedDivMod(result); - } - break; - } - } - - TransformMap[term] = result; - if(term.GetValueWidth() != result.GetValueWidth()) - FatalError("TransformTerm: result and input terms are of different length", result); - if(term.GetIndexWidth() != result.GetIndexWidth()) { - cerr << "TransformTerm: input term is : " << term << endl; - FatalError("TransformTerm: result and input terms have different index length", result); - } - return result; - } //End of TransformTerm - - /* This function transforms Array Reads, Read over Writes, Read over - * ITEs into flattened form. - * - * Transform1: Suppose there are two array reads in the input - * Read(A,i) and Read(A,j) over the same array. Then Read(A,i) is - * replaced with a symbolic constant, say v1, and Read(A,j) is - * replaced with the following ITE: - * - * ITE(i=j,v1,v2) - * - * Transform2: - * - * Transform3: - */ - ASTNode BeevMgr::TransformArray(const ASTNode& term) { - ASTNode result = term; - - unsigned int width = term.GetValueWidth(); - Kind k = term.GetKind(); - if (!is_Term_kind(k)) - FatalError("TransformArray: Illegal kind: You have input a nonterm:", ASTUndefined, k); - ASTNodeMap::iterator iter; - if((iter = TransformMap.find(term)) != TransformMap.end()) - return iter->second; - - switch(k) { - //'term' is of the form READ(arrName, readIndex) - case READ: { - ASTNode arrName = term[0]; - switch (arrName.GetKind()) { - case SYMBOL: { - /* input is of the form: READ(A, readIndex) - * - * output is of the from: A1, if this is the first READ over A - * - * ITE(previous_readIndex=readIndex,A1,A2) - * - * ..... - */ - - // Recursively transform read index, which may also contain reads. - ASTNode readIndex = TransformTerm(term[1]); - ASTNode processedTerm = CreateTerm(READ,width,arrName,readIndex); - - //check if the 'processedTerm' has a corresponding ITE construct - //already. if so, return it. else continue processing. - ASTNodeMap::iterator it; - if((it = _arrayread_ite.find(processedTerm)) != _arrayread_ite.end()) { - result = it->second; - break; - } - //Constructing Symbolic variable corresponding to 'processedTerm' - ASTNode CurrentSymbol; - ASTNodeMap::iterator it1; - // First, check if read index is constant and it has a constant value in the substitution map. - if(CheckSubstitutionMap(processedTerm,CurrentSymbol)) { - _arrayread_symbol[processedTerm] = CurrentSymbol; - } - // Check if it already has an abstract variable. - else if((it1 = _arrayread_symbol.find(processedTerm)) != _arrayread_symbol.end()) { - CurrentSymbol = it1->second; - } - else { - // Make up a new abstract variable. - // FIXME: Make this into a method (there already may BE a method) and - // get rid of the fixed-length buffer! - //build symbolic name corresponding to array read. The symbolic - //name has 2 components: stringname, and a count - const char * b = arrName.GetName(); - std::string c(b); - char d[32]; - sprintf(d,"%d",_symbol_count++); - std::string ccc(d); - c += "array_" + ccc; - - CurrentSymbol = CreateSymbol(c.c_str()); - CurrentSymbol.SetValueWidth(processedTerm.GetValueWidth()); - CurrentSymbol.SetIndexWidth(processedTerm.GetIndexWidth()); - _arrayread_symbol[processedTerm] = CurrentSymbol; - } - - //list of array-read indices corresponding to arrName, seen while - //traversing the AST tree. we need this list to construct the ITEs - // Dill: we hope to make this irrelevant. Harmless for now. - ASTVec readIndices = _arrayname_readindices[arrName]; - - //construct the ITE structure for this array-read - ASTNode ite = CurrentSymbol; - _introduced_symbols.insert(CurrentSymbol); - BVTypeCheck(ite); - - if(arrayread_refinement) { - // ite is really a variable here; it is an ite in the - // else-branch - result = ite; - } - else { - // Full Seshia transform if we're not doing read refinement. - //do not loop if the current readIndex is a BVCONST - // if(BVCONST == term[1].GetKind() && !SeenNonConstReadIndex && optimize) { - // result = ite; - // } - // else { - //else part: SET the SeenNonConstReadIndex var, and do the hard work - //SeenNonConstReadIndex = true; - ASTVec::reverse_iterator it2=readIndices.rbegin(); - ASTVec::reverse_iterator it2end=readIndices.rend(); - for(;it2!=it2end;it2++) { - ASTNode cond = CreateSimplifiedEQ(readIndex,*it2); - if(ASTFalse == cond) - continue; - - ASTNode arrRead = CreateTerm(READ,width,arrName,*it2); - //Good idea to TypeCheck internally constructed nodes - BVTypeCheck(arrRead); - - ASTNode arrayreadSymbol = _arrayread_symbol[arrRead]; - if(arrayreadSymbol.IsNull()) - FatalError("TransformArray:symbolic variable for processedTerm, p," - "does not exist:p = ",arrRead); - ite = CreateSimplifiedTermITE(cond,arrayreadSymbol,ite); - } - result = ite; - //} - } - - _arrayname_readindices[arrName].push_back(readIndex); - //save the ite corresponding to 'processedTerm' - _arrayread_ite[processedTerm] = result; - break; - } //end of READ over a SYMBOL - case WRITE:{ - /* The input to this case is: READ((WRITE A i val) j) - * - * The output of this case is: ITE( (= i j) val (READ A i)) - */ - - /* 1. arrName or term[0] is infact a WRITE(A,i,val) expression - * - * 2. term[1] is the read-index j - * - * 3. arrName[0] is the new arrName i.e. A. A can be either a - SYMBOL or a nested WRITE. no other possibility - * - * 4. arrName[1] is the WRITE index i.e. i - * - * 5. arrName[2] is the WRITE value i.e. val (val can inturn - * be an array read) - */ - ASTNode readIndex = TransformTerm(term[1]); - ASTNode writeIndex = TransformTerm(arrName[1]); - ASTNode writeVal = TransformTerm(arrName[2]); - - if(!(SYMBOL == arrName[0].GetKind() || - WRITE == arrName[0].GetKind())) - FatalError("TransformArray: An array write is being attempted on a non-array:",term); - if(ARRAY_TYPE != arrName[0].GetType()) - FatalError("TransformArray: An array write is being attempted on a non-array:",term); - - ASTNode cond = CreateSimplifiedEQ(writeIndex,readIndex); - //TypeCheck internally created node - BVTypeCheck(cond); - ASTNode readTerm = CreateTerm(READ,width,arrName[0],readIndex); - //TypeCheck internally created node - BVTypeCheck(readTerm); - ASTNode readPushedIn = TransformArray(readTerm); - //TypeCheck internally created node - BVTypeCheck(readPushedIn); - //result = CreateTerm(ITE, arrName[0].GetValueWidth(),cond,writeVal,readPushedIn); - result = CreateSimplifiedTermITE(cond,writeVal,readPushedIn); - - //Good idea to typecheck terms created inside the system - BVTypeCheck(result); - break; - } //end of READ over a WRITE - case ITE: { - /* READ((ITE cond thn els) j) - * - * is transformed into - * - * (ITE cond (READ thn j) (READ els j)) - */ - - //(ITE cond thn els) - ASTNode term0 = term[0]; - //READINDEX j - ASTNode j = TransformTerm(term[1]); - - ASTNode cond = term0[0]; - //first array - ASTNode t01 = term0[1]; - //second array - ASTNode t02 = term0[2]; - - cond = TransformFormula(cond); - ASTNode thn = TransformTerm(t01); - ASTNode els = TransformTerm(t02); - - if(!(t01.GetValueWidth() == t02.GetValueWidth() && - t01.GetValueWidth() == thn.GetValueWidth() && - t01.GetValueWidth() == els.GetValueWidth())) - FatalError("TransformArray: length of THENbranch != length of ELSEbranch in the term t = \n",term); - - if(!(t01.GetIndexWidth() == t02.GetIndexWidth() && - t01.GetIndexWidth() == thn.GetIndexWidth() && - t01.GetIndexWidth() == els.GetIndexWidth())) - FatalError("TransformArray: length of THENbranch != length of ELSEbranch in the term t = \n",term); - - //(READ thn j) - ASTNode thnRead = CreateTerm(READ,width,thn,j); - BVTypeCheck(thnRead); - thnRead = TransformArray(thnRead); - - //(READ els j) - ASTNode elsRead = CreateTerm(READ,width,els,j); - BVTypeCheck(elsRead); - elsRead = TransformArray(elsRead); - - //(ITE cond (READ thn j) (READ els j)) - result = CreateSimplifiedTermITE(cond,thnRead,elsRead); - BVTypeCheck(result); - break; - } - default: - FatalError("TransformArray: The READ is NOT over SYMBOL/WRITE/ITE",term); - break; - } - break; - } //end of READ switch - default: - FatalError("TransformArray: input term is of wrong kind: ",ASTUndefined); - break; - } - - TransformMap[term] = result; - return result; - } //end of TransformArray() -} //end of namespace BEEV diff --git a/stp/AST/genkinds.pl b/stp/AST/genkinds.pl deleted file mode 100755 index 672481ad..00000000 --- a/stp/AST/genkinds.pl +++ /dev/null @@ -1,123 +0,0 @@ -#!/usr/bin/perl -w - -#AUTHORS: Vijay Ganesh, David L. Dill BEGIN DATE: November, 2005 -#LICENSE: Please view LICENSE file in the home dir of this Program -#given a file containing kind names, one per line produces .h and .cpp -#files for the kinds. - -#globals -@kindnames = (); -$minkids = 0; -$maxkids = 0; -@cat_bits = (); -@category_names = (); -%cat_index = (); - -$now = localtime time; - -sub read_kind_defs { - open(KFILE, "< ASTKind.kinds") || die "Cannot open .kinds file: $!\n"; - @kindlines = ; - close(KFILE) -} - -# create lists of things indexed by kinds. -sub split_fields { - my $kind_cat_bits; - # matches anything with three whitespace-delimited alphanumeric fields, - # followed by rest of line. Automatically ignores lines beginning with '#' and blank lines. - for (@kindlines) { - if (/Categories:\s+(.*)/) { - @category_names = split(/\s+/, $1); - $i = 0; - for (@category_names) { - $cat_index{$_} = $i++; - # print "cat_index{$_} = $i\n"; - } - } - elsif (/^(\w+)\s+(\w+)\s+(\w+|-)\s+(.*)/) { - push(@kindnames, $1); - push(@minkids, $2); - push(@maxkids, $3); - @kind_cats = split(/\s+/, $4); - # build a bit vector of categories. - $kind_cat_bits = 0; - for (@kind_cats) { - $kind_cat_bits |= (1 << int($cat_index{$_})); - } - push(@cat_bits, $kind_cat_bits); - } - } -} - -sub gen_h_file { - open(HFILE, "> ASTKind.h") || die "Cannot open .h file: $!\n"; - - print HFILE - "// -*- c++ -*-\n", - "#ifndef TESTKINDS_H\n", - "#define TESTKINDS_H\n", - "// Generated automatically by genkinds.pl from ASTKind.kinds $now.\n", - "// Do not edit\n", - "namespace BEEV {\n typedef enum {\n"; - - for (@kindnames) { - print HFILE " $_,\n"; - } - - print HFILE - "} Kind;\n\n", - "extern unsigned char _kind_categories[];\n\n"; - - # For category named "cat", generate functions "bool is_cat_kind(k);" - - - for (@category_names) { - my $catname = $_; - my $kind_cat_bit = (1 << int($cat_index{$catname})); - print HFILE "inline bool is_", $catname, "_kind(Kind k) { return (_kind_categories[k] & $kind_cat_bit); }\n\n" - } - - print HFILE - "extern const char *_kind_names[];\n\n", - "/** Prints symbolic name of kind */\n", - "inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n", - "\n\n", - "} // end namespace\n", - "\n\n#endif\n"; - - close(HFILE); -} - -# generate the .cpp file - -sub gen_cpp_file { - open(CPPFILE, "> ASTKind.cpp") || die "Cannot open .h file: $!\n"; - - print CPPFILE - "// Generated automatically by genkinds.h from ASTKind.kinds $now.\n", - "// Do not edit\n", - "namespace BEEV {\n", - "const char * _kind_names[] = {\n"; - for (@kindnames) { - print CPPFILE " \"$_\",\n"; - } - print CPPFILE "};\n\n"; - - # category bits - print CPPFILE - "unsigned char _kind_categories[] = {\n"; - for (@cat_bits) { - print CPPFILE " $_,\n"; - } - print CPPFILE - "};\n", - "\n} // end namespace\n"; - - close(CPPFILE); -} - -&read_kind_defs; -&split_fields; -&gen_h_file; -&gen_cpp_file; -- cgit 1.4.1