diff options
Diffstat (limited to 'stp/AST')
| -rw-r--r-- | stp/AST/AST.cpp | 1587 | ||||
| -rw-r--r-- | stp/AST/AST.h | 1805 | ||||
| -rw-r--r-- | stp/AST/ASTKind.kinds | 71 | ||||
| -rw-r--r-- | stp/AST/ASTUtil.cpp | 45 | ||||
| -rw-r--r-- | stp/AST/ASTUtil.h | 107 | ||||
| -rw-r--r-- | stp/AST/BitBlast.cpp | 812 | ||||
| -rw-r--r-- | stp/AST/Makefile | 54 | ||||
| -rw-r--r-- | stp/AST/STLport_config.h | 20 | ||||
| -rw-r--r-- | stp/AST/SimpBool.cpp | 408 | ||||
| -rw-r--r-- | stp/AST/ToCNF.cpp | 506 | ||||
| -rw-r--r-- | stp/AST/ToSAT.cpp | 1385 | ||||
| -rw-r--r-- | stp/AST/Transform.cpp | 492 | ||||
| -rw-r--r-- | stp/AST/asttest.cpp | 29 | ||||
| -rw-r--r-- | stp/AST/bbtest.cpp | 96 | ||||
| -rw-r--r-- | stp/AST/cnftest.cpp | 47 | ||||
| -rwxr-xr-x | stp/AST/genkinds.pl | 123 |
16 files changed, 7587 insertions, 0 deletions
diff --git a/stp/AST/AST.cpp b/stp/AST/AST.cpp new file mode 100644 index 00000000..ab290395 --- /dev/null +++ b/stp/AST/AST.cpp @@ -0,0 +1,1587 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "AST.h" +namespace BEEV { + //some global variables that are set through commandline options. it + //is best that these variables remain global. Default values set + //here + // + //collect statistics on certain functions + bool stats = false; + //print DAG nodes + bool print_nodes = false; + //tentative global var to allow for variable activity optimization + //in the SAT solver. deprecated. + bool variable_activity_optimize = false; + //run STP in optimized mode + bool optimize = true; + //do sat refinement, i.e. underconstraint the problem, and feed to + //SAT. if this works, great. else, add a set of suitable constraints + //to re-constraint the problem correctly, and call SAT again, until + //all constraints have been added. + bool arrayread_refinement = true; + //flag to control write refinement + bool arraywrite_refinement = true; + //check the counterexample against the original input to STP + bool check_counterexample = false; + //construct the counterexample in terms of original variable based + //on the counterexample returned by SAT solver + bool construct_counterexample = true; + bool print_counterexample = false; + //if this option is true then print the way dawson wants using a + //different printer. do not use this printer. + bool print_arrayval_declaredorder = false; + //flag to decide whether to print "valid/invalid" or not + bool print_output = false; + //do linear search in the array values of an input array. experimental + bool linear_search = false; + //print the variable order chosen by the sat solver while it is + //solving. + bool print_sat_varorder = false; + //turn on word level bitvector solver + bool wordlevel_solve = true; + //turn off XOR flattening + bool xor_flatten = false; + + //the smtlib parser has been turned on + bool smtlib_parser_enable = false; + //print the input back + bool print_STPinput_back = false; + + //global BEEVMGR for the parser + BeevMgr * globalBeevMgr_for_parser; + + void (*vc_error_hdlr)(const char* err_msg) = NULL; + /** This is reusable empty vector, for representing empty children arrays */ + ASTVec _empty_ASTVec; + //////////////////////////////////////////////////////////////// + // ASTInternal members + //////////////////////////////////////////////////////////////// + /** Trivial but virtual destructor */ + ASTInternal::~ASTInternal() { } + + //////////////////////////////////////////////////////////////// + // ASTInterior members + //////////////////////////////////////////////////////////////// + /** Copy constructor */ + // ASTInterior::ASTInterior(const ASTInterior &int_node) + // { + // _kind = int_node._kind; + // _children = int_node._children; + // } + + /** Trivial but virtual destructor */ + ASTInterior::~ASTInterior() { } + + // FIXME: Darn it! I think this ends up copying the children twice! + /** Either return an old node or create it if it doesn't exist. + Note that nodes are physically allocated in the hash table. */ + + // There is an inelegance here that I don't know how to solve. I'd + // like to heap allocate and do some other initialization on keys only + // if they aren't in the hash table. It would be great if the + // "insert" method took a "creator" class so that I could do that + // between when it notices that the key is not there and when it + // inserts it. Alternatively, it would be great if I could insert the + // temporary key and replace it if it actually got inserted. But STL + // hash_set doesn't have the creator feature and paternalistically + // declares that keys are immutable, even though (it seems to me) that + // they could be mutated if the hash value and eq values did not + // change. + + ASTInterior *BeevMgr::LookupOrCreateInterior(ASTInterior *n_ptr) { + ASTInteriorSet::iterator it; + + if ((it = _interior_unique_table.find(n_ptr)) == _interior_unique_table.end()) { + // Make a new ASTInterior node + // We want (NOT alpha) always to have alpha.nodenum + 1. + if (n_ptr->GetKind() == NOT) { + n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum()+1); + } + else { + n_ptr->SetNodeNum(NewNodeNum()); + } + pair<ASTInteriorSet::const_iterator, bool> p = _interior_unique_table.insert(n_ptr); + return *(p.first); + } + else + // Delete the temporary node, and return the found node. + delete n_ptr; + return *it; + } + + size_t ASTInterior::ASTInteriorHasher::operator() (const ASTInterior *int_node_ptr) const { + //size_t hashval = 0; + size_t hashval = ((size_t) int_node_ptr->GetKind()); + const ASTVec &ch = int_node_ptr->GetChildren(); + ASTVec::const_iterator iend = ch.end(); + for (ASTVec::const_iterator i = ch.begin(); i != iend; i++) { + //Using "One at a time hash" by Bob Jenkins + hashval += i->Hash(); + hashval += (hashval << 10); + hashval ^= (hashval >> 6); + } + + hashval += (hashval << 3); + hashval ^= (hashval >> 11); + hashval += (hashval << 15); + return hashval; + //return hashval += ((size_t) int_node_ptr->GetKind()); + } + + + void ASTInterior::CleanUp() { + // cout << "Deleting node " << this->GetNodeNum() << endl; + _bm._interior_unique_table.erase(this); + delete this; + } + + //////////////////////////////////////////////////////////////// + // ASTNode members + //////////////////////////////////////////////////////////////// + //ASTNode constructors are inlined in AST.h + bool ASTNode::IsAlreadyPrinted() const { + BeevMgr &bm = GetBeevMgr(); + return (bm.AlreadyPrintedSet.find(*this) != bm.AlreadyPrintedSet.end()); + } + + void ASTNode::MarkAlreadyPrinted() const { + // FIXME: Fetching BeevMgr is annoying. Can we put this in lispprinter class? + BeevMgr &bm = GetBeevMgr(); + bm.AlreadyPrintedSet.insert(*this); + } + + // Get the name from a symbol (char *). It's an error if kind != SYMBOL + const char * const ASTNode::GetName() const { + if (GetKind() != SYMBOL) + FatalError("GetName: Called GetName on a non-symbol: ", *this); + return ((ASTSymbol *) _int_node_ptr)->GetName(); + } + + // Print in lisp format + ostream &ASTNode::LispPrint(ostream &os, int indentation) const { + // Clear the PrintMap + BeevMgr& bm = GetBeevMgr(); + bm.AlreadyPrintedSet.clear(); + return LispPrint_indent(os, indentation); + } + + // Print newline and indentation, then print the thing. + ostream &ASTNode::LispPrint_indent(ostream &os, + int indentation) const + { + os << endl << spaces(indentation); + LispPrint1(os, indentation); + return os; + } + + /** Internal function to print in lisp format. Assume newline + and indentation printed already before first line. Recursive + calls will have newline & indent, though */ + ostream &ASTNode::LispPrint1(ostream &os, int indentation) const { + if (!IsDefined()) { + os << "<undefined>"; + return os; + } + Kind kind = GetKind(); + // FIXME: figure out how to avoid symbols with same names as kinds. +// if (kind == READ) { +// const ASTVec &children = GetChildren(); +// children[0].LispPrint1(os, indentation); +// os << "[" << children[1] << "]"; +// } else + if(kind == BVGETBIT) { + const ASTVec &children = GetChildren(); + // child 0 is a symbol. Print without the NodeNum. + os << GetNodeNum() << ":"; + + + + children[0]._int_node_ptr->nodeprint(os); + //os << "{" << children[1].GetBVConst() << "}"; + os << "{"; + children[1]._int_node_ptr->nodeprint(os); + os << "}"; + } else if (kind == NOT) { + const ASTVec &children = GetChildren(); + os << GetNodeNum() << ":"; + os << "(NOT "; + children[0].LispPrint1(os, indentation); + os << ")"; + } + else if (Degree() == 0) { + // Symbol or a kind with no children print as index:NAME if shared, + // even if they have been printed before. + os << GetNodeNum() << ":"; + _int_node_ptr->nodeprint(os); + // os << "(" << _int_node_ptr->_ref_count << ")"; + // os << "{" << GetValueWidth() << "}"; + } + else if (IsAlreadyPrinted()) { + // print non-symbols as "[index]" if seen before. + os << "[" << GetNodeNum() << "]"; + // << "(" << _int_node_ptr->_ref_count << ")"; + } + else { + MarkAlreadyPrinted(); + const ASTVec &children = GetChildren(); + os << GetNodeNum() << ":" + //<< "(" << _int_node_ptr->_ref_count << ")" + << "(" << kind << " "; + // os << "{" << GetValueWidth() << "}"; + ASTVec::const_iterator iend = children.end(); + for (ASTVec::const_iterator i = children.begin(); i != iend; i++) { + i->LispPrint_indent(os, indentation+2); + } + os << ")"; + } + return os; + } + + //print in PRESENTATION LANGUAGE + // + //two pass algorithm: + // + //1. In the first pass, letize this Node, N: i.e. if a node + //1. appears more than once in N, then record this fact. + // + //2. In the second pass print a "global let" and then print N + //2. as follows: Every occurence of a node occuring more than + //2. once is replaced with the corresponding let variable. + ostream& ASTNode::PL_Print(ostream &os, + int indentation) const { + // Clear the PrintMap + BeevMgr& bm = GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); + + //pass 1: letize the node + LetizeNode(); + + //pass 2: + // + //2. print all the let variables and their counterpart expressions + //2. as follows (LET var1 = expr1, var2 = expr2, ... + // + //3. Then print the Node itself, replacing every occurence of + //3. expr1 with var1, expr2 with var2, ... + //os << "("; + if(0 < bm.NodeLetVarMap.size()) { + //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); + //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); + std::vector<pair<ASTNode,ASTNode> >::iterator it = bm.NodeLetVarVec.begin(); + std::vector<pair<ASTNode,ASTNode> >::iterator itend = bm.NodeLetVarVec.end(); + + os << "(LET "; + //print the let var first + it->first.PL_Print1(os,indentation,false); + os << " = "; + //print the expr + it->second.PL_Print1(os,indentation,false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + + for(it++;it!=itend;it++) { + os << "," << endl; + //print the let var first + it->first.PL_Print1(os,indentation,false); + os << " = "; + //print the expr + it->second.PL_Print1(os,indentation,false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } + + os << " IN " << endl; + PL_Print1(os,indentation, true); + os << ") "; + } + else + PL_Print1(os,indentation, false); + //os << " )"; + os << " "; + return os; + } //end of PL_Print() + + //traverse "*this", and construct "let variables" for terms that + //occur more than once in "*this". + void ASTNode::LetizeNode(void) const { + Kind kind = this->GetKind(); + + if(kind == SYMBOL || + kind == BVCONST || + kind == FALSE || + kind == TRUE) + return; + + //FIXME: this is ugly. + BeevMgr& bm = GetBeevMgr(); + const ASTVec &c = this->GetChildren(); + for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++){ + ASTNode ccc = *it; + if(bm.PLPrintNodeSet.find(ccc) == bm.PLPrintNodeSet.end()){ + //If branch: if *it is not in NodeSet then, + // + //1. add it to NodeSet + // + //2. Letize its childNodes + + //FIXME: Fetching BeevMgr is annoying. Can we put this in + //some kind of a printer class + bm.PLPrintNodeSet.insert(ccc); + //debugging + //cerr << ccc; + ccc.LetizeNode(); + } + else{ + Kind k = ccc.GetKind(); + if(k == SYMBOL || + k == BVCONST || + k == FALSE || + k == TRUE) + continue; + + //0. Else branch: Node has been seen before + // + //1. Check if the node has a corresponding letvar in the + //1. NodeLetVarMap. + // + //2. if no, then create a new var and add it to the + //2. NodeLetVarMap + if(bm.NodeLetVarMap.find(ccc) == bm.NodeLetVarMap.end()) { + //Create a new symbol. Get some name. if it conflicts with a + //declared name, too bad. + int sz = bm.NodeLetVarMap.size(); + ostringstream oss; + oss << "let_k_" << sz; + + ASTNode CurrentSymbol = bm.CreateSymbol(oss.str().c_str()); + CurrentSymbol.SetValueWidth(this->GetValueWidth()); + CurrentSymbol.SetIndexWidth(this->GetIndexWidth()); + /* If for some reason the variable being created here is + * already declared by the user then the printed output will + * not be a legal input to the system. too bad. I refuse to + * check for this. [Vijay is the author of this comment.] + */ + + bm.NodeLetVarMap[ccc] = CurrentSymbol; + std::pair<ASTNode,ASTNode> node_letvar_pair(CurrentSymbol,ccc); + bm.NodeLetVarVec.push_back(node_letvar_pair); + } + } + } + } //end of LetizeNode() + + void ASTNode::PL_Print1(ostream& os, + int indentation, + bool letize) const { + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!IsDefined()) { + os << "<undefined>"; + return; + } + + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = GetBeevMgr(); + + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) { + (bm.NodeLetVarMap1[*this]).PL_Print1(os,indentation,letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) { + (bm.NodeLetVarMap[*this]).PL_Print1(os,indentation,letize); + return; + } + + //otherwise print it normally + Kind kind = GetKind(); + const ASTVec &c = GetChildren(); + switch(kind) { + case BVGETBIT: + c[0].PL_Print1(os,indentation,letize); + os << "{"; + c[1].PL_Print1(os,indentation,letize); + os << "}"; + break; + case BITVECTOR: + os << "BITVECTOR("; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); + os << str << ")"; + CONSTANTBV::BitVector_Dispose(str); + break; + case BOOLEAN: + os << "BOOLEAN"; + break; + case FALSE: + case TRUE: + os << kind; + break; + case BVCONST: + case SYMBOL: + _int_node_ptr->nodeprint(os); + break; + case READ: + c[0].PL_Print1(os, indentation,letize); + os << "["; + c[1].PL_Print1(os,indentation,letize); + os << "]"; + break; + case WRITE: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " WITH ["; + c[1].PL_Print1(os,indentation,letize); + os << "] := "; + c[2].PL_Print1(os,indentation,letize); + os << ")"; + os << endl; + break; + case BVUMINUS: + os << kind << "( "; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + break; + case NOT: + os << "NOT("; + c[0].PL_Print1(os,indentation,letize); + os << ") " << endl; + break; + case BVNEG: + os << " ~("; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + break; + case BVCONCAT: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " @ "; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVOR: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " | "; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + break; + case BVAND: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " & "; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + break; + case BVEXTRACT: + c[0].PL_Print1(os,indentation,letize); + os << "["; + os << GetUnsignedConst(c[1]); + os << ":"; + os << GetUnsignedConst(c[2]); + os << "]"; + break; + case BVLEFTSHIFT: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " << "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVRIGHTSHIFT: + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << " >> "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVMULT: + case BVSUB: + case BVPLUS: + case SBVDIV: + case SBVMOD: + case BVDIV: + case BVMOD: + os << kind << "("; + os << this->GetValueWidth(); + for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) { + os << ", " << endl; + it->PL_Print1(os,indentation,letize); + } + os << ")" << endl; + break; + case ITE: + os << "IF("; + c[0].PL_Print1(os,indentation,letize); + os << ")" << endl; + os << "THEN "; + c[1].PL_Print1(os,indentation,letize); + os << endl << "ELSE "; + c[2].PL_Print1(os,indentation,letize); + os << endl << "ENDIF"; + break; + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + os << kind << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSLT: + os << "SBVLT" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSLE: + os << "SBVLE" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSGT: + os << "SBVGT" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVSGE: + os << "SBVGE" << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + c[1].PL_Print1(os,indentation,letize); + os << ")" << endl; + break; + case EQ: + c[0].PL_Print1(os,indentation,letize); + os << " = "; + c[1].PL_Print1(os,indentation,letize); + os << endl; + break; + case NEQ: + c[0].PL_Print1(os,indentation,letize); + os << " /= "; + c[1].PL_Print1(os,indentation,letize); + os << endl; + break; + case AND: + case OR: + case NAND: + case NOR: + case XOR: { + os << "("; + c[0].PL_Print1(os,indentation,letize); + ASTVec::const_iterator it=c.begin(); + ASTVec::const_iterator itend=c.end(); + + it++; + for(;it!=itend;it++) { + os << " " << kind << " "; + it->PL_Print1(os,indentation,letize); + os << endl; + } + os << ")"; + break; + } + case IFF: + os << "("; + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + os << " <=> "; + os << "("; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + os << ")"; + os << endl; + break; + case IMPLIES: + os << "("; + os << "("; + c[0].PL_Print1(os,indentation,letize); + os << ")"; + os << " => "; + os << "("; + c[1].PL_Print1(os,indentation,letize); + os << ")"; + os << ")"; + os << endl; + break; + case BVSX: + os << kind << "("; + c[0].PL_Print1(os,indentation,letize); + os << ","; + os << this->GetValueWidth(); + os << ")" << endl; + break; + default: + //remember to use LispPrinter here. Otherwise this function will + //go into an infinite loop. Recall that "<<" is overloaded to + //the lisp printer. FatalError uses lispprinter + FatalError("PL_Print1: printing not implemented for this kind: ",*this); + break; + } + } //end of PL_Print1() + + //////////////////////////////////////////////////////////////// + // BeevMgr members + //////////////////////////////////////////////////////////////// + ASTNode BeevMgr::CreateNode(Kind kind, const ASTVec & back_children) { + // create a new node. Children will be modified. + ASTInterior *n_ptr = new ASTInterior(kind, *this); + + // insert all of children at end of new_children. + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + ASTNode BeevMgr::CreateNode(Kind kind, + const ASTNode& child0, + const ASTVec & back_children) { + + ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTVec &front_children = n_ptr->_children; + front_children.push_back(child0); + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + ASTNode BeevMgr::CreateNode(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec & back_children) { + + ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTVec &front_children = n_ptr->_children; + front_children.push_back(child0); + front_children.push_back(child1); + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + + ASTNode BeevMgr::CreateNode(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec & back_children) { + ASTInterior *n_ptr = new ASTInterior(kind, *this); + ASTVec &front_children = n_ptr->_children; + front_children.push_back(child0); + front_children.push_back(child1); + front_children.push_back(child2); + ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); + return n; + } + + + ASTInterior *BeevMgr::CreateInteriorNode(Kind kind, + // children array of this node will be modified. + ASTInterior *n_ptr, + const ASTVec & back_children) { + + // insert back_children at end of front_children + ASTVec &front_children = n_ptr->_children; + + front_children.insert(front_children.end(), back_children.begin(), back_children.end()); + + // check for undefined nodes. + ASTVec::const_iterator it_end = front_children.end(); + for (ASTVec::const_iterator it = front_children.begin(); it != it_end; it++) { + if (it->IsNull()) + FatalError("CreateInteriorNode: Undefined childnode in CreateInteriorNode: ", ASTUndefined); + } + + return LookupOrCreateInterior(n_ptr); + } + + /** Trivial but virtual destructor */ + ASTSymbol::~ASTSymbol() {} + + ostream &operator<<(ostream &os, const ASTNodeMap &nmap) + { + ASTNodeMap::const_iterator iend = nmap.end(); + for (ASTNodeMap::const_iterator i = nmap.begin(); i!=iend; i++) { + os << "Key: " << i->first << endl; + os << "Value: " << i->second << endl; + } + return os; + } + + //////////////////////////////////////////////////////////////// + // BeevMgr member functions to create ASTSymbol and ASTBVConst + //////////////////////////////////////////////////////////////// + ASTNode BeevMgr::CreateSymbol(const char * const name) + { + ASTSymbol temp_sym(name, *this); + ASTNode n(LookupOrCreateSymbol(temp_sym)); + return n; + } + +#ifndef NATIVE_C_ARITH + //Create a ASTBVConst node + ASTNode BeevMgr::CreateBVConst(unsigned int width, + unsigned long long int bvconst){ + if(width > (sizeof(unsigned long long int)<<3) || width <= 0) + FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width); + + + CBV bv = CONSTANTBV::BitVector_Create(width, true); + unsigned long c_val = (0x00000000ffffffffLL) & bvconst; + unsigned int copied = 0; + + // sizeof(unsigned long) returns the number of bytes in unsigned + // long. In order to convert it to bits, we need to shift left by + // 3. Hence, sizeof(unsigned long) << 3 + + //The algo below works as follows: It starts by copying the + //lower-order bits of the input "bvconst" in chunks of size = + //number of bits in unsigned long. The variable "copied" keeps + //track of the number of chunks copied so far + + while(copied + (sizeof(unsigned long)<<3) < width){ + CONSTANTBV::BitVector_Chunk_Store(bv, sizeof(unsigned long)<<3,copied,c_val); + bvconst = bvconst >> (sizeof(unsigned long) << 3); + c_val = (0x00000000ffffffffLL) & bvconst; + copied += sizeof(unsigned long) << 3; + } + CONSTANTBV::BitVector_Chunk_Store(bv,width - copied,copied,c_val); + return CreateBVConst(bv,width); + } + + //Create a ASTBVConst node from std::string + ASTNode BeevMgr::CreateBVConst(const char* const strval, int base) { + size_t width = strlen((const char *)strval); + if(!(2 == base || 10 == base || 16 == base)){ + FatalError("CreateBVConst: unsupported base: ",ASTUndefined,base); + } + //FIXME Tim: Earlier versions of the code assume that the length of + //binary strings is 32 bits. + if(10 == base) width = 32; + if(16 == base) width = width * 4; + + //checking if the input is in the correct format + CBV bv = CONSTANTBV::BitVector_Create(width,true); + CONSTANTBV::ErrCode e; + if(2 == base){ + e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*)strval); + }else if(10 == base){ + e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*)strval); + }else if(16 == base){ + e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*)strval); + }else{ + e = CONSTANTBV::ErrCode_Pars; + } + + if(0 != e) { + cerr << "CreateBVConst: " << BitVector_Error(e); + FatalError("",ASTUndefined); + } + + //FIXME + return CreateBVConst(bv, width); + } + + + //FIXME Code currently assumes that it will destroy the bitvector passed to it + ASTNode BeevMgr::CreateBVConst(CBV bv, unsigned width){ + ASTBVConst temp_bvconst(bv, width, *this); + ASTNode n(LookupOrCreateBVConst(temp_bvconst)); + + CONSTANTBV::BitVector_Destroy(bv); + + return n; + } + + ASTNode BeevMgr::CreateZeroConst(unsigned width) { + CBV z = CONSTANTBV::BitVector_Create(width, true); + return CreateBVConst(z, width); + } + + ASTNode BeevMgr::CreateOneConst(unsigned width) { + CBV o = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_increment(o); + + return CreateBVConst(o,width); + } + + ASTNode BeevMgr::CreateTwoConst(unsigned width) { + CBV two = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_increment(two); + CONSTANTBV::BitVector_increment(two); + + return CreateBVConst(two,width); + } + + ASTNode BeevMgr::CreateMaxConst(unsigned width) { + CBV max = CONSTANTBV::BitVector_Create(width, false); + CONSTANTBV::BitVector_Fill(max); + + return CreateBVConst(max,width); + } + + //To ensure unique BVConst nodes, lookup the node in unique-table + //before creating a new one. + ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) { + ASTBVConst *s_ptr = &s; // it's a temporary key. + + // Do an explicit lookup to see if we need to create a copy of the string. + ASTBVConstSet::const_iterator it; + if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) { + // Make a new ASTBVConst with duplicated string (can't assign + // _name because it's const). Can cast the iterator to + // non-const -- carefully. + + ASTBVConst * s_copy = new ASTBVConst(s); + s_copy->SetNodeNum(NewNodeNum()); + + pair<ASTBVConstSet::const_iterator, bool> p = _bvconst_unique_table.insert(s_copy); + return *p.first; + } + else{ + // return symbol found in table. + return *it; + } + } + + // Inline because we need to wait until unique_table is defined + void ASTBVConst::CleanUp() { + // cout << "Deleting node " << this->GetNodeNum() << endl; + _bm._bvconst_unique_table.erase(this); + delete this; + } + + // Get the value of bvconst from a bvconst. It's an error if kind != BVCONST + CBV const ASTNode::GetBVConst() const { + if(GetKind() != BVCONST) + FatalError("GetBVConst: non bitvector-constant: ",*this); + return ((ASTBVConst *) _int_node_ptr)->GetBVConst(); + } +#else + //Create a ASTBVConst node + ASTNode BeevMgr::CreateBVConst(const unsigned int width, + const unsigned long long int bvconst) { + if(width > 64 || width <= 0) + FatalError("Fatal Error: CreateBVConst: trying to create a bvconst of width:", ASTUndefined, width); + + //64 bit mask + unsigned long long int mask = 0xffffffffffffffffLL; + mask = mask >> (64 - width); + + unsigned long long int bv = bvconst; + bv = bv & mask; + + ASTBVConst temp_bvconst(bv, *this); + temp_bvconst._value_width = width; + ASTNode n(LookupOrCreateBVConst(temp_bvconst)); + n.SetValueWidth(width); + n.SetIndexWidth(0); + return n; + } + //Create a ASTBVConst node from std::string + ASTNode BeevMgr::CreateBVConst(const char* strval, int base) { + if(!(base == 2 || base == 16 || base == 10)) + FatalError("CreateBVConst: This base is not supported: ", ASTUndefined, base); + + if(10 != base) { + unsigned int width = (base == 2) ? strlen(strval) : strlen(strval)*4; + unsigned long long int val = strtoull(strval, NULL, base); + ASTNode bvcon = CreateBVConst(width, val); + return bvcon; + } + else { + //this is an ugly hack to accomodate SMTLIB format + //restrictions. SMTLIB format represents bitvector constants in + //base 10 (what a terrible idea, but i have no choice but to + //support it), and make an implicit assumption that the length + //is 32 (another terrible idea). + unsigned width = 32; + unsigned long long int val = strtoull(strval, NULL, base); + ASTNode bvcon = CreateBVConst(width, val); + return bvcon; + } + } + + //To ensure unique BVConst nodes, lookup the node in unique-table + //before creating a new one. + ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) { + ASTBVConst *s_ptr = &s; // it's a temporary key. + + // Do an explicit lookup to see if we need to create a copy of the + // string. + ASTBVConstSet::const_iterator it; + if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) { + // Make a new ASTBVConst. Can cast the iterator to non-const -- + // carefully. + unsigned int width = s_ptr->_value_width; + ASTBVConst * s_ptr1 = new ASTBVConst(s_ptr->GetBVConst(), *this); + s_ptr1->SetNodeNum(NewNodeNum()); + s_ptr1->_value_width = width; + pair<ASTBVConstSet::const_iterator, bool> p = _bvconst_unique_table.insert(s_ptr1); + return *p.first; + } + else + // return BVConst found in table. + return *it; + } + + // Inline because we need to wait until unique_table is defined + void ASTBVConst::CleanUp() { + // cout << "Deleting node " << this->GetNodeNum() << endl; + _bm._bvconst_unique_table.erase(this); + delete this; + } + + // Get the value of bvconst from a bvconst. It's an error if kind + // != BVCONST + unsigned long long int ASTNode::GetBVConst() const { + if(GetKind() != BVCONST) + FatalError("GetBVConst: non bitvector-constant: ", *this); + return ((ASTBVConstTmp *) _int_node_ptr)->GetBVConst(); + } + + ASTNode BeevMgr::CreateZeroConst(unsigned width) { + return CreateBVConst(width,0); + } + + ASTNode BeevMgr::CreateOneConst(unsigned width) { + return CreateBVConst(width,1); + } + + ASTNode BeevMgr::CreateTwoConst(unsigned width) { + return CreateBVConst(width,2); + } + + ASTNode BeevMgr::CreateMaxConst(unsigned width) { + std::string s; + s.insert(s.end(),width,'1'); + return CreateBVConst(s.c_str(),2); + } + +#endif + + // FIXME: _name is now a constant field, and this assigns to it + // because it tries not to copy the string unless it needs to. How + // do I avoid copying children in ASTInterior? Perhaps I don't! + + // Note: There seems to be a limitation of hash_set, in that insert + // returns a const iterator to the value. That prevents us from + // modifying the name (in a hash-preserving way) after the symbol is + // inserted. FIXME: Is there a way to do this with insert? Need a + // function to make a new object in the middle of insert. Read STL + // documentation. + + ASTSymbol *BeevMgr::LookupOrCreateSymbol(ASTSymbol& s) { + ASTSymbol *s_ptr = &s; // it's a temporary key. + + // Do an explicit lookup to see if we need to create a copy of the string. + ASTSymbolSet::const_iterator it; + if ((it = _symbol_unique_table.find(s_ptr)) == _symbol_unique_table.end()) { + // Make a new ASTSymbol with duplicated string (can't assign + // _name because it's const). Can cast the iterator to + // non-const -- carefully. + //std::string strname(s_ptr->GetName()); + ASTSymbol * s_ptr1 = new ASTSymbol(strdup(s_ptr->GetName()), *this); + s_ptr1->SetNodeNum(NewNodeNum()); + s_ptr1->_value_width = s_ptr->_value_width; + pair<ASTSymbolSet::const_iterator, bool> p = _symbol_unique_table.insert(s_ptr1); + return *p.first; + } + else + // return symbol found in table. + return *it; + } + + bool BeevMgr::LookupSymbol(ASTSymbol& s) { + ASTSymbol* s_ptr = &s; // it's a temporary key. + + if(_symbol_unique_table.find(s_ptr) == _symbol_unique_table.end()) + return false; + else + return true; + } + + // Inline because we need to wait until unique_table is defined + void ASTSymbol::CleanUp() { + // cout << "Deleting node " << this->GetNodeNum() << endl; + _bm._symbol_unique_table.erase(this); + //FIXME This is a HUGE free to invoke. + //TEST IT! + free((char*) this->_name); + delete this; + } + + //////////////////////////////////////////////////////////////// + // + // IO manipulators for Lisp format printing of AST. + // + //////////////////////////////////////////////////////////////// + + // FIXME: Additional controls + // * Print node numbers (addresses/nums) + // * Printlength limit + // * Printdepth limit + + /** Print a vector of ASTNodes in lisp format */ + ostream &LispPrintVec(ostream &os, const ASTVec &v, int indentation) + { + // Print the children + ASTVec::const_iterator iend = v.end(); + for (ASTVec::const_iterator i = v.begin(); i != iend; i++) { + i->LispPrint_indent(os, indentation); + } + return os; + } + + // FIXME: Made non-ref in the hope that it would work better. + void lp(ASTNode node) + { + cout << lisp(node) << endl; + } + + void lpvec(const ASTVec &vec) + { + vec[0].GetBeevMgr().AlreadyPrintedSet.clear(); + LispPrintVec(cout, vec, 0); + cout << endl; + } + + // Copy constructor. Maintain _ref_count + ASTNode::ASTNode(const ASTNode &n) : _int_node_ptr(n._int_node_ptr) { +#ifndef SMTLIB + if (n._int_node_ptr) { + n._int_node_ptr->IncRef(); + } +#endif + } + + + /* FUNCTION: Typechecker for terms and formulas + * + * TypeChecker: Assumes that the immediate Children of the input + * ASTNode have been typechecked. This function is suitable in + * scenarios like where you are building the ASTNode Tree, and you + * typecheck as you go along. It is not suitable as a general + * typechecker + */ + void BeevMgr::BVTypeCheck(const ASTNode& n) { + Kind k = n.GetKind(); + //The children of bitvector terms are in turn bitvectors. + ASTVec v = n.GetChildren(); + if(is_Term_kind(k)) { + switch(k) { + case BVCONST: + if(BITVECTOR_TYPE != n.GetType()) + FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n); + break; + case SYMBOL: + return; + case ITE: + if(BOOLEAN_TYPE != n[0].GetType() && + BITVECTOR_TYPE != n[1].GetType() && + BITVECTOR_TYPE != n[2].GetType()) + FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n); + if(n[1].GetValueWidth() != n[2].GetValueWidth()) + FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n); + if(n[1].GetIndexWidth() != n[2].GetIndexWidth()) + FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n); + break; + case READ: + if(n[0].GetIndexWidth() != n[1].GetValueWidth()) { + cerr << "Length of indexwidth of array: " << n[0] << " is : " << n[0].GetIndexWidth() << endl; + cerr << "Length of the actual index is: " << n[1] << " is : " << n[1].GetValueWidth() << endl; + FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n); + } + break; + case WRITE: + if(n[0].GetIndexWidth() != n[1].GetValueWidth()) + FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n); + if(n[0].GetValueWidth() != n[2].GetValueWidth()) + FatalError("BVTypeCheck: valuewidth of array != length of actual value in the term t = \n",n); + break; + case BVOR: + case BVAND: + case BVXOR: + case BVNOR: + case BVNAND: + case BVXNOR: + case BVPLUS: + case BVMULT: + case BVDIV: + case BVMOD: + case BVSUB: { + if(!(v.size() >= 2)) + FatalError("BVTypeCheck:bitwise Booleans and BV arith operators must have atleast two arguments\n",n); + unsigned int width = n.GetValueWidth(); + for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++){ + if(width != it->GetValueWidth()) { + cerr << "BVTypeCheck:Operands of bitwise-Booleans and BV arith operators must be of equal length\n"; + cerr << n << endl; + cerr << "width of term:" << width << endl; + cerr << "width of offending operand:" << it->GetValueWidth() << endl; + FatalError("BVTypeCheck:Offending operand:\n",*it); + } + if(BITVECTOR_TYPE != it->GetType()) + FatalError("BVTypeCheck: ChildNodes of bitvector-terms must be bitvectors\n",n); + } + break; + } + case BVSX: + //in BVSX(n[0],len), the length of the BVSX term must be + //greater than the length of n[0] + if(n[0].GetValueWidth() >= n.GetValueWidth()) { + FatalError("BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n",n); + } + break; + default: + for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++) + if(BITVECTOR_TYPE != it->GetType()) { + cerr << "The type is: " << it->GetType() << endl; + FatalError("BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors\n",n); + } + break; + } + + switch(k) { + case BVCONCAT: + if(n.Degree() != 2) + FatalError("BVTypeCheck: should have exactly 2 args\n",n); + if(n.GetValueWidth() != n[0].GetValueWidth() + n[1].GetValueWidth()) + FatalError("BVTypeCheck:BVCONCAT: lengths do not add up\n",n); + break; + case BVUMINUS: + case BVNEG: + if(n.Degree() != 1) + FatalError("BVTypeCheck: should have exactly 1 args\n",n); + break; + case BVEXTRACT: + if(n.Degree() != 3) + FatalError("BVTypeCheck: should have exactly 3 args\n",n); + if(!(BVCONST == n[1].GetKind() && BVCONST == n[2].GetKind())) + FatalError("BVTypeCheck: indices should be BVCONST\n",n); + if(n.GetValueWidth() != GetUnsignedConst(n[1])- GetUnsignedConst(n[2])+1) + FatalError("BVTypeCheck: length mismatch\n",n); + break; + case BVLEFTSHIFT: + case BVRIGHTSHIFT: + if(n.Degree() != 2) + FatalError("BVTypeCheck: should have exactly 2 args\n",n); + break; + //case BVVARSHIFT: + //case BVSRSHIFT: + break; + default: + break; + } + } + else { + if(!(is_Form_kind(k) && BOOLEAN_TYPE == n.GetType())) + FatalError("BVTypeCheck: not a formula:",n); + switch(k){ + case TRUE: + case FALSE: + case SYMBOL: + return; + case EQ: + case NEQ: + if(!(n[0].GetValueWidth() == n[1].GetValueWidth() && + n[0].GetIndexWidth() == n[1].GetIndexWidth())) { + cerr << "valuewidth of lhs of EQ: " << n[0].GetValueWidth() << endl; + cerr << "valuewidth of rhs of EQ: " << n[1].GetValueWidth() << endl; + cerr << "indexwidth of lhs of EQ: " << n[0].GetIndexWidth() << endl; + cerr << "indexwidth of rhs of EQ: " << n[1].GetIndexWidth() << endl; + FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); + } + break; + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVSLT: + case BVSLE: + case BVSGT: + case BVSGE: + if(BITVECTOR_TYPE != n[0].GetType() && BITVECTOR_TYPE != n[1].GetType()) + FatalError("BVTypeCheck: terms in atomic formulas must be bitvectors",n); + if(n[0].GetValueWidth() != n[1].GetValueWidth()) + FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); + if(n[0].GetIndexWidth() != n[1].GetIndexWidth()) + FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); + break; + case NOT: + if(1 != n.Degree()) + FatalError("BVTypeCheck: NOT formula can have exactly one childNode",n); + break; + case AND: + case OR: + case XOR: + case NAND: + case NOR: + if(2 > n.Degree()) + FatalError("BVTypeCheck: AND/OR/XOR/NAND/NOR: must have atleast 2 ChildNodes",n); + break; + case IFF: + case IMPLIES: + if(2 != n.Degree()) + FatalError("BVTypeCheck:IFF/IMPLIES must have exactly 2 ChildNodes",n); + break; + case ITE: + if(3 != n.Degree()) + FatalError("BVTypeCheck:ITE must have exactly 3 ChildNodes",n); + break; + default: + FatalError("BVTypeCheck: Unrecognized kind: ",ASTUndefined); + break; + } + } + } //End of TypeCheck function + + //add an assertion to the current logical context + void BeevMgr::AddAssert(const ASTNode& assert) { + if(!(is_Form_kind(assert.GetKind()) && BOOLEAN_TYPE == assert.GetType())) { + FatalError("AddAssert:Trying to assert a non-formula:",assert); + } + + ASTVec * v; + //if the stack of ASTVec is not empty, then take the top ASTVec + //and add the input assert to it + if(!_asserts.empty()) { + v = _asserts.back(); + //v->push_back(TransformFormula(assert)); + v->push_back(assert); + } + else { + //else create a logical context, and add it to the top of the + //stack + v = new ASTVec(); + //v->push_back(TransformFormula(assert)); + v->push_back(assert); + _asserts.push_back(v); + } + } + + void BeevMgr::Push(void) { + ASTVec * v; + v = new ASTVec(); + _asserts.push_back(v); + } + + void BeevMgr::Pop(void) { + if(!_asserts.empty()) { + ASTVec * c = _asserts.back(); + //by calling the clear function we ensure that the ref count is + //decremented for the ASTNodes stored in c + c->clear(); + delete c; + _asserts.pop_back(); + } + } + + void BeevMgr::AddQuery(const ASTNode& q) { + //_current_query = TransformFormula(q); + //cerr << "\nThe current query is: " << q << endl; + _current_query = q; + } + + const ASTNode BeevMgr::PopQuery() { + ASTNode q = _current_query; + _current_query = ASTTrue; + return q; + } + + const ASTNode BeevMgr::GetQuery() { + return _current_query; + } + + const ASTVec BeevMgr::GetAsserts(void) { + vector<ASTVec *>::iterator it = _asserts.begin(); + vector<ASTVec *>::iterator itend = _asserts.end(); + + ASTVec v; + for(;it!=itend;it++) { + if(!(*it)->empty()) + v.insert(v.end(),(*it)->begin(),(*it)->end()); + } + return v; + } + + //Create a new variable of ValueWidth 'n' + ASTNode BeevMgr::NewArrayVar(unsigned int index, unsigned int value) { + std:: string c("v"); + char d[32]; + sprintf(d,"%d",_symbol_count++); + std::string ccc(d); + c += "_writearray_" + ccc; + + ASTNode CurrentSymbol = CreateSymbol(c.c_str()); + CurrentSymbol.SetValueWidth(value); + CurrentSymbol.SetIndexWidth(index); + return CurrentSymbol; + } //end of NewArrayVar() + + + //Create a new variable of ValueWidth 'n' + ASTNode BeevMgr::NewVar(unsigned int value) { + std:: string c("v"); + char d[32]; + sprintf(d,"%d",_symbol_count++); + std::string ccc(d); + c += "_new_stp_var_" + ccc; + + ASTNode CurrentSymbol = CreateSymbol(c.c_str()); + CurrentSymbol.SetValueWidth(value); + CurrentSymbol.SetIndexWidth(0); + _introduced_symbols.insert(CurrentSymbol); + return CurrentSymbol; + } //end of NewVar() + + //prints statistics for the ASTNode + void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a){ + if(!stats) + return; + + StatInfoSet.clear(); + //print node size: + cout << endl << "Printing: " << c; + if(print_nodes) { + //a.PL_Print(cout,0); + //cout << endl; + cout << a << endl; + } + cout << "Node size is: "; + cout << NodeSize(a) << endl << endl; + } + + unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo) { + if(clearStatInfo) + StatInfoSet.clear(); + + ASTNodeSet::iterator it; + if((it = StatInfoSet.find(a)) != StatInfoSet.end()) + //has already been counted + return 0; + + //record that you have seen this node already + StatInfoSet.insert(a); + + //leaf node has a size of 1 + if(a.Degree() == 0) + return 1; + + unsigned newn = 1; + ASTVec c = a.GetChildren(); + for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) + newn += NodeSize(*it); + return newn; + } + + void BeevMgr::ClearAllTables(void) { + //clear all tables before calling toplevelsat + _ASTNode_to_SATVar.clear(); + _SATVar_to_AST.clear(); + + for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), + itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { + delete it->second; + } + _ASTNode_to_Bitvector.clear(); + + /* OLD Destructor + * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + + /*What should I do here? For ASTNodes? + * for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + BBTermMemo.clear(); + BBFormMemo.clear(); + NodeLetVarMap.clear(); + NodeLetVarMap1.clear(); + PLPrintNodeSet.clear(); + AlreadyPrintedSet.clear(); + SimplifyMap.clear(); + SimplifyNegMap.clear(); + SolverMap.clear(); + AlwaysTrueFormMap.clear(); + _arrayread_ite.clear(); + _arrayread_symbol.clear(); + _introduced_symbols.clear(); + TransformMap.clear(); + _letid_expr_map.clear(); + CounterExampleMap.clear(); + ComputeFormulaMap.clear(); + StatInfoSet.clear(); + + // for(std::vector<ASTVec *>::iterator it=_asserts.begin(), + // itend=_asserts.end();it!=itend;it++) { + // (*it)->clear(); + // } + _asserts.clear(); + for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), + iset_end = _arrayname_readindices.end(); + iset!=iset_end;iset++) { + iset->second.clear(); + } + + _arrayname_readindices.clear(); + _interior_unique_table.clear(); + _symbol_unique_table.clear(); + _bvconst_unique_table.clear(); + } + + void BeevMgr::ClearAllCaches(void) { + //clear all tables before calling toplevelsat + _ASTNode_to_SATVar.clear(); + _SATVar_to_AST.clear(); + + + for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), + itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { + delete it->second; + } + _ASTNode_to_Bitvector.clear(); + + /*OLD destructor + * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + + /*What should I do here? + *for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), + ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { + ivec->second.clear(); + }*/ + BBTermMemo.clear(); + BBFormMemo.clear(); + NodeLetVarMap.clear(); + NodeLetVarMap1.clear(); + PLPrintNodeSet.clear(); + AlreadyPrintedSet.clear(); + SimplifyMap.clear(); + SimplifyNegMap.clear(); + SolverMap.clear(); + AlwaysTrueFormMap.clear(); + _arrayread_ite.clear(); + _arrayread_symbol.clear(); + _introduced_symbols.clear(); + TransformMap.clear(); + _letid_expr_map.clear(); + CounterExampleMap.clear(); + ComputeFormulaMap.clear(); + StatInfoSet.clear(); + + for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), + iset_end = _arrayname_readindices.end(); + iset!=iset_end;iset++) { + iset->second.clear(); + } + + _arrayname_readindices.clear(); + //_interior_unique_table.clear(); + //_symbol_unique_table.clear(); + //_bvconst_unique_table.clear(); + } + + void BeevMgr::CopySolverMap_To_CounterExample(void) { + if(!SolverMap.empty()) { + CounterExampleMap.insert(SolverMap.begin(),SolverMap.end()); + } + } + + void FatalError(const char * str, const ASTNode& a, int w) { + if(a.GetKind() != UNDEFINED) { + cerr << "Fatal Error: " << str << endl << a << endl; + cerr << w << endl; + } + else { + cerr << "Fatal Error: " << str << endl; + cerr << w << endl; + } + if (vc_error_hdlr) + vc_error_hdlr(str); + exit(-1); + //assert(0); + } + + void FatalError(const char * str) { + cerr << "Fatal Error: " << str << endl; + if (vc_error_hdlr) + vc_error_hdlr(str); + exit(-1); + //assert(0); + } + + //Variable Order Printer: A global function which converts a MINISAT + //var into a ASTNODE var. It then prints this var along with + //variable order dcisions taken by MINISAT. + void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, + int decision_level, int polarity) { + BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var]; + cout << spaces(decision_level); + if(polarity) { + cout << "!"; + } + vv.PL_Print(cout,0); + cout << endl; + } + + void SortByExprNum(ASTVec& v) { + sort(v.begin(), v.end(), exprless); + } + + bool isAtomic(Kind kind) { + if(TRUE == kind || + FALSE == kind || + EQ == kind || + NEQ == kind || + BVLT == kind || + BVLE == kind || + BVGT == kind || + BVGE == kind || + BVSLT == kind || + BVSLE == kind || + BVSGT == kind || + BVSGE == kind || + SYMBOL == kind || + BVGETBIT == kind) + return true; + return false; + } + + BeevMgr::~BeevMgr() { + ClearAllTables(); + } +}; // end namespace + diff --git a/stp/AST/AST.h b/stp/AST/AST.h new file mode 100644 index 00000000..53ed7016 --- /dev/null +++ b/stp/AST/AST.h @@ -0,0 +1,1805 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef AST_H +#define AST_H +#include <vector> +#ifdef EXT_HASH_MAP +#include <ext/hash_set> +#include <ext/hash_map> +#else +#include <hash_set> +#include <hash_map> +#endif +#include <iostream> +#include <sstream> +#include <string> +#include <map> +#include <set> +#include "ASTUtil.h" +#include "ASTKind.h" +#include "../sat/Solver.h" +#include "../sat/SolverTypes.h" +#include <cstdlib> +#ifndef NATIVE_C_ARITH +#include "../constantbv/constantbv.h" +#endif +/***************************************************************************** + * LIST OF CLASSES DECLARED IN THIS FILE: + * + * class BeevMgr; + * class ASTNode; + * class ASTInternal; + * class ASTInterior; + * class ASTSymbol; + * class ASTBVConst; + *****************************************************************************/ +namespace BEEV { + using namespace std; + using namespace MINISAT; +#ifdef EXT_HASH_MAP + using namespace __gnu_cxx; +#endif + + //return types for the GetType() function in ASTNode class + enum types { + BOOLEAN_TYPE = 0, + BITVECTOR_TYPE, + ARRAY_TYPE, + UNKNOWN_TYPE + }; + + class BeevMgr; + class ASTNode; + class ASTInternal; + class ASTInterior; + class ASTSymbol; + class ASTBVConst; + class BVSolver; + + //Vector of ASTNodes, used for child nodes among other things. + typedef vector<ASTNode> ASTVec; + extern ASTVec _empty_ASTVec; + extern BeevMgr * globalBeevMgr_for_parser; + + typedef unsigned int * CBV; + + /***************************************************************************/ + /* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */ + /***************************************************************************/ + class ASTNode { + friend class BeevMgr; + friend class vector<ASTNode>; + //Print the arguments in lisp format. + friend ostream &LispPrintVec(ostream &os, + const ASTVec &v, int indentation = 0); + + private: + // FIXME: make this into a reference? + ASTInternal * _int_node_ptr; // The real data. + + // Usual constructor. + ASTNode(ASTInternal *in); + + //Check if it points to a null node + bool IsNull () const { return _int_node_ptr == NULL; } + + //Equal iff ASTIntNode pointers are the same. + friend bool operator==(const ASTNode node1, const ASTNode node2){ + return ((size_t) node1._int_node_ptr) == ((size_t) node2._int_node_ptr); + } + + /* FIXME: Nondeterministic code *** */ + /** questionable pointer comparison function */ + friend bool operator<(const ASTNode node1, const ASTNode node2){ + return ((size_t) node1._int_node_ptr) < ((size_t) node2._int_node_ptr); + } + + public: + // This is for sorting by expression number (used in Boolean + //optimization) + friend bool exprless(const ASTNode n1, const ASTNode n2) { + Kind k1 = n1.GetKind(); + Kind k2 = n2.GetKind(); + + if(BVCONST == k1 && BVCONST != k2){ + return true; + } + if(BVCONST != k1 && BVCONST == k2){ + return false; + } + + if(SYMBOL == k1 && SYMBOL != k2) { + return true; + } + + if(SYMBOL != k1 && SYMBOL == k2) { + return false; + } + + return (n1.GetNodeNum() < n2.GetNodeNum()); + }//end of exprless + + // Internal lisp-form printer that does not clear _node_print_table + ostream &LispPrint1(ostream &os, int indentation) const; + + ostream &LispPrint_indent(ostream &os, int indentation) const; + + // For lisp DAG printing. Has it been printed already, so we can + // just print the node number? + bool IsAlreadyPrinted() const; + void MarkAlreadyPrinted() const; + + public: + // Default constructor. This gets used when declaring an ASTVec + // of a given size, in the hash table, etc. For faster + // refcounting, create a symbol node for NULL. Give it a big + // initial refcount. Never free it. also check, for ref-count + // overflow? + ASTNode() : _int_node_ptr(NULL) { }; + + // Copy constructor + ASTNode(const ASTNode &n); + + // Destructor + ~ASTNode(); + + // Assignment (for ref counting) + ASTNode& operator=(const ASTNode& n); + + BeevMgr &GetBeevMgr() const; + + // Access node number + int GetNodeNum() const; + + // Access kind. Inlined later because of declaration ordering problems. + Kind GetKind() const; + + // access Children + const ASTVec &GetChildren() const; + + // Return the number of child nodes + size_t Degree() const{ + return GetChildren().size(); + }; + + // Get indexth childNode. + const ASTNode operator[](size_t index) const { + return GetChildren()[index]; + }; + + // Get begin() iterator for child nodes + ASTVec::const_iterator begin() const{ + return GetChildren().begin(); + }; + + // Get end() iterator for child nodes + ASTVec::const_iterator end() const{ + return GetChildren().end(); + }; + + //Get back() element for child nodes + const ASTNode back() const{ + return GetChildren().back(); + }; + + // Get the name from a symbol (char *). It's an error if kind != SYMBOL + const char * const GetName() const; + + //Get the BVCONST value +#ifndef NATIVE_C_ARITH + const 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. + const 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 const Kind GetKind() const { return _kind; } + + virtual ASTVec const &GetChildren() const { return _children; } + + int GetNodeNum() const { return _node_num; } + + void SetNodeNum(int nn) { _node_num = nn; }; + + // Constructor (bm only) + ASTInternal(BeevMgr &bm, int nodenum = 0) : + _ref_count(0), + _kind(UNDEFINED), + _bm(bm), + _node_num(nodenum), + _index_width(0), + _value_width(0) { } + + // Constructor (kind only, empty children, int nodenum) + ASTInternal(Kind kind, BeevMgr &bm, int nodenum = 0) : + _ref_count(0), + _kind(kind), + _bm(bm), + _node_num(nodenum), + _index_width(0), + _value_width(0) { } + + // Constructor (kind and children). This copies the contents of + // the child nodes. + // FIXME: is there a way to avoid repeating these? + ASTInternal(Kind kind, const ASTVec &children, BeevMgr &bm, int nodenum = 0) : + _ref_count(0), + _kind(kind), + _children(children), + _bm(bm), + _node_num(nodenum), + _index_width(0), + _value_width(0) { } + + // Copy constructor. This copies the contents of the child nodes + // array, along with everything else. Assigning the smart pointer, + // ASTNode, does NOT invoke this; This should only be used for + // temporary hash keys before uniquefication. + // FIXME: I don't think children need to be copied. + ASTInternal(const ASTInternal &int_node, int nodenum = 0) : + _ref_count(0), + _kind(int_node._kind), + _children(int_node._children), + _bm(int_node._bm), + _node_num(int_node._node_num), + _index_width(int_node._index_width), + _value_width(int_node._value_width) { } + + // Copying assign operator. Also copies contents of children. + ASTInternal& operator=(const ASTInternal &int_node); + + // Cleanup function for removing from hash table + virtual void CleanUp() = 0; + + // Destructor (does nothing, but is declared virtual here. + virtual ~ASTInternal(); + + // Abstract virtual print function for internal node. + virtual void nodeprint(ostream& os) { os << "*"; }; + }; //End of Class ASTInternal + + // FIXME: Should children be only in interior node type? + /*************************************************************************** + Class ASTInterior: Internal representation of an interior + ASTNode. Generally, these nodes should have at least one + child + ***************************************************************************/ + class ASTInterior : public ASTInternal { + + friend class BeevMgr; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + + // Hasher for ASTInterior pointer nodes + class ASTInteriorHasher { + public: + size_t operator()(const ASTInterior *int_node_ptr) const; + }; + + // Equality for ASTInterior nodes + class ASTInteriorEqual { + public: + bool operator()(const ASTInterior *int_node_ptr1, + const ASTInterior *int_node_ptr2) const{ + return (*int_node_ptr1 == *int_node_ptr2); + } + }; + + // Used in Equality class for hash tables + friend bool operator==(const ASTInterior &int_node1, + const ASTInterior &int_node2){ + return (int_node1._kind == int_node2._kind) && + (int_node1._children == int_node2._children); + } + + // Call this when deleting a node that has been stored in the + // the unique table + virtual void CleanUp(); + + // Returns kinds. "lispprinter" handles printing of parenthesis + // and childnodes. + virtual void nodeprint(ostream& os) { + os << _kind_names[_kind]; + } + public: + + // FIXME: This should not be public, but has to be because the + // ASTInterior hash table insists on it. I can't seem to make the + // private destructor visible to hash_set. It does not even work + // to put "friend class hash_set<ASTInterior, ...>" in here. + + // Basic constructors + ASTInterior(Kind kind, BeevMgr &bm) : + ASTInternal(kind, bm) { } + + ASTInterior(Kind kind, ASTVec &children, BeevMgr &bm) : + ASTInternal(kind, children, bm) { } + + //Copy constructor. This copies the contents of the child nodes + //array, along with everything else. Assigning the smart pointer, + //ASTNode, does NOT invoke this. + ASTInterior(const ASTInterior &int_node) : ASTInternal(int_node) { } + + // Destructor (does nothing, but is declared virtual here. + virtual ~ASTInterior(); + + }; //End of ASTNodeInterior + + + /***************************************************************************/ + /* Class ASTSymbol: Class to represent internals of Symbol node. */ + /***************************************************************************/ + class ASTSymbol : public ASTInternal{ + friend class BeevMgr; + friend class ASTNode; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + // The name of the symbol + const char * const _name; + + class ASTSymbolHasher{ + public: + size_t operator() (const ASTSymbol *sym_ptr) const{ + hash<char*> h; + return h(sym_ptr->_name); + }; + }; + + // Equality for ASTInternal nodes + class ASTSymbolEqual{ + public: + bool operator()(const ASTSymbol *sym_ptr1, const ASTSymbol *sym_ptr2) const{ + return (*sym_ptr1 == *sym_ptr2); + } + }; + + friend bool operator==(const ASTSymbol &sym1, const ASTSymbol &sym2){ + return (strcmp(sym1._name, sym2._name) == 0); + } + + const char * const GetName() const{return _name;} + + // Print function for symbol -- return name */ + virtual void nodeprint(ostream& os) { os << _name;} + + // Call this when deleting a node that has been stored in the + // the unique table + virtual void CleanUp(); + + public: + + // Default constructor + ASTSymbol(BeevMgr &bm) : ASTInternal(bm), _name(NULL) { } + + // Constructor. This does NOT copy its argument. + ASTSymbol(const char * const name, BeevMgr &bm) : ASTInternal(SYMBOL, bm), + _name(name) { } + + // Destructor (does nothing, but is declared virtual here. + virtual ~ASTSymbol(); + + // Copy constructor + // FIXME: seems to be calling default constructor for astinternal + ASTSymbol(const ASTSymbol &sym) : + ASTInternal(sym._kind, sym._children, sym._bm), + _name(sym._name) { } + }; //End of ASTSymbol + + + /***************************************************************************/ + /* Class ASTBVConst: Class to represent internals of a bitvectorconst */ + /***************************************************************************/ + +#ifndef NATIVE_C_ARITH + + class ASTBVConst : public ASTInternal { + friend class BeevMgr; + friend class ASTNode; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + //This is the private copy of a bvconst currently + //This should not be changed at any point + CBV _bvconst; + + class ASTBVConstHasher{ + public: + size_t operator() (const ASTBVConst * bvc) const { + return CONSTANTBV::BitVector_Hash(bvc->_bvconst); + }; + }; + + class ASTBVConstEqual{ + public: + bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const { + if( bvc1->_value_width != bvc2->_value_width){ + return false; + } + return (0==CONSTANTBV::BitVector_Compare(bvc1->_bvconst,bvc2->_bvconst)); + } + }; + + //FIXME Keep an eye on this function + ASTBVConst(CBV bv, unsigned int width, BeevMgr &bm) : + ASTInternal(BVCONST, bm) + { + _bvconst = CONSTANTBV::BitVector_Clone(bv); + _value_width = width; + } + + friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){ + if(bvc1._value_width != bvc2._value_width) + return false; + return (0==CONSTANTBV::BitVector_Compare(bvc1._bvconst,bvc2._bvconst)); + } + // Call this when deleting a node that has been stored in the + // the unique table + virtual void CleanUp(); + + // Print function for bvconst -- return _bvconst value in bin format + virtual void nodeprint(ostream& os) { + unsigned char *res; + const char *prefix; + + if (_value_width%4 == 0) { + res = CONSTANTBV::BitVector_to_Hex(_bvconst); + prefix = "0hex"; + } else { + res = CONSTANTBV::BitVector_to_Bin(_bvconst); + prefix = "0bin"; + } + if (NULL == res) { + os << "nodeprint: BVCONST : could not convert to string" << _bvconst; + FatalError(""); + } + os << prefix << res; + CONSTANTBV::BitVector_Dispose(res); + } + + // Copy constructor. + ASTBVConst(const ASTBVConst &sym) : + ASTInternal(sym._kind, sym._children, sym._bm) + { + _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst); + _value_width = sym._value_width; + } + + public: + virtual ~ASTBVConst(){ + CONSTANTBV::BitVector_Destroy(_bvconst); + } + + CBV GetBVConst() const {return _bvconst;} + }; //End of ASTBVConst + + //FIXME This function is DEPRICATED + //Do not use in the future + inline unsigned int GetUnsignedConst(const ASTNode n) { + if(32 < n.GetValueWidth()) + FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:"); + + return (unsigned int) *((unsigned int *)n.GetBVConst()); + } +#else + class ASTBVConst : public ASTInternal { + friend class BeevMgr; + friend class ASTNode; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + // the bitvector contents. bitvector contents will be in two + // modes. one mode where all bitvectors are NATIVE and in this + // mode we use native unsigned long long int to represent the + // 32/64 bitvectors. The other for arbitrary length bitvector + // operations. + const unsigned long long int _bvconst; + + class ASTBVConstHasher{ + public: + size_t operator() (const ASTBVConst * bvc) const{ + //Thomas Wang's 64 bit Mix Function + unsigned long long int key(bvc->_bvconst); + key += ~(key << 32); + key ^= (key >> 22); + key += ~(key << 13); + key ^= (key >> 8); + key += (key << 3); + key ^= (key >> 15); + key += ~(key << 27); + key ^= (key >> 31); + + size_t return_key = key; + return return_key; + }; + }; + + class ASTBVConstEqual{ + public: + bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const { + return ((bvc1->_bvconst == bvc2->_bvconst) + && (bvc1->_value_width == bvc2->_value_width)); + } + }; + + // Call this when deleting a node that has been stored in the + // the unique table + virtual void CleanUp(); + public: + // Default constructor + ASTBVConst(const unsigned long long int bv, BeevMgr &bm) : + ASTInternal(BVCONST, bm), _bvconst(bv) { + } + + // Copy constructor. FIXME: figure out how this is supposed to + // work. + ASTBVConst(const ASTBVConst &sym) : + ASTInternal(sym._kind, sym._children, sym._bm), + _bvconst(sym._bvconst) { + _value_width = sym._value_width; + } + + // Destructor (does nothing, but is declared virtual here) + virtual ~ASTBVConst() { } + + friend bool operator==(const ASTBVConst &sym1, const ASTBVConst &sym2){ + return ((sym1._bvconst == sym2._bvconst) && + (sym1._value_width == sym2._value_width)); + } + + // Print function for bvconst -- return _bvconst value in binary format + virtual void nodeprint(ostream& os) { + string s = "0bin"; + unsigned long long int bitmask = 0x8000000000000000LL; + bitmask = bitmask >> (64-_value_width); + + for (; bitmask > 0; bitmask >>= 1) + s += (_bvconst & bitmask) ? '1' : '0'; + os << s; + } + + unsigned long long int GetBVConst() const {return _bvconst;} + }; //End of ASTBVConst + + //return value of bvconst + inline unsigned int GetUnsignedConst(const ASTNode n) { + if(32 < n.GetValueWidth()) + FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:"); + return (unsigned int)n.GetBVConst(); + } +#endif +/* +#else + // the bitvector contents. bitvector contents will be in two + // modes. one mode where all bitvectors are NATIVE and in this mode + // we use native unsigned long long int to represent the 32/64 + // bitvectors. The other for arbitrary length bitvector operations. + + //BVCONST defined for arbitrary length bitvectors + class ASTBVConst : public ASTInternal{ + friend class BeevMgr; + friend class ASTNode; + friend class ASTNodeHasher; + friend class ASTNodeEqual; + + private: + const char * const _bvconst; + + class ASTBVConstHasher{ + public: + size_t operator() (const ASTBVConst * bvc) const{ + hash<char*> h; + return h(bvc->_bvconst); + }; + }; + + class ASTBVConstEqual{ + public: + bool operator()(const ASTBVConst * bvc1, const ASTBVConst * bvc2) const { + if(bvc1->_value_width != bvc2->_value_width) + return false; + return (0 == strncmp(bvc1->_bvconst,bvc2->_bvconst,bvc1->_value_width)); + } + }; + + ASTBVConst(const char * bv, BeevMgr &bm) : + ASTInternal(BVCONST, bm), _bvconst(bv) { + //_value_width = strlen(bv); + } + + friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){ + if(bvc1._value_width != bvc2._value_width) + return false; + return (0 == strncmp(bvc1._bvconst,bvc2._bvconst,bvc1._value_width)); + } + + // Call this when deleting a node that has been stored in the + // the unique table + virtual void CleanUp(); + + // Print function for bvconst -- return _bvconst value in binary format + virtual void nodeprint(ostream& os) { + if(_value_width%4 == 0) { + unsigned int * iii = CONSTANTBV::BitVector_Create(_value_width,true); + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_from_Bin(iii,(unsigned char*)_bvconst); + //error printing + if(0 != e) { + os << "nodeprint: BVCONST : wrong hex value: " << BitVector_Error(e); + FatalError(""); + } + unsigned char * ccc = CONSTANTBV::BitVector_to_Hex(iii); + os << "0hex" << ccc; + CONSTANTBV::BitVector_Destroy(iii); + } + else { + std::string s(_bvconst,_value_width); + s = "0bin" + s; + os << s; + } + } + + // Copy constructor. + ASTBVConst(const ASTBVConst &sym) : ASTInternal(sym._kind, sym._children, sym._bm),_bvconst(sym._bvconst) { + //checking if the input is in the correct format + for(unsigned int jj=0;jj<sym._value_width;jj++) + if(!(sym._bvconst[jj] == '0' || sym._bvconst[jj] == '1')) { + cerr << "Fatal Error: wrong input to ASTBVConst copy constructor:" << sym._bvconst << endl; + FatalError(""); + } + _value_width = sym._value_width; + } + public: + // Destructor (does nothing, but is declared virtual here) + virtual ~ASTBVConst(){} + + const char * const GetBVConst() const {return _bvconst;} + }; //End of ASTBVConst + + unsigned int * ConvertToCONSTANTBV(const char * s); + + //return value of bvconst + inline unsigned int GetUnsignedConst(const ASTNode n) { + if(32 < n.GetValueWidth()) + FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:"); + std::string s(n.GetBVConst(), n.GetValueWidth()); + unsigned int output = strtoul(s.c_str(),NULL,2); + return output; + } //end of ASTBVConst class +#endif +*/ + /*************************************************************************** + * Typedef ASTNodeMap: This is a hash table from ASTNodes to ASTNodes. + * It is very convenient for attributes that are not speed-critical + **************************************************************************/ + // These are generally useful for storing ASTNodes or attributes thereof + // Hash table from ASTNodes to ASTNodes + typedef hash_map<ASTNode, ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeMap; + + // Function to dump contents of ASTNodeMap + ostream &operator<<(ostream &os, const ASTNodeMap &nmap); + + /*************************************************************************** + Typedef ASTNodeSet: This is a hash set of ASTNodes. Very useful + for representing things like "visited nodes" + ***************************************************************************/ + typedef hash_set<ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeSet; + + typedef hash_multiset<ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeMultiSet; + + //external parser table for declared symbols. + //FIXME: move to a more appropriate place + extern ASTNodeSet _parser_symbol_table; + + /*************************************************************************** + Class LispPrinter: iomanipulator for printing ASTNode or ASTVec + ***************************************************************************/ + class LispPrinter { + + public: + ASTNode _node; + + // number of spaces to print before first real character of + // object. + int _indentation; + + // FIXME: pass ASTNode by reference + // Constructor to build the LispPrinter object + LispPrinter(ASTNode node, int indentation): _node(node), _indentation(indentation) { } + + friend ostream &operator<<(ostream &os, const LispPrinter &lp){ + return lp._node.LispPrint(os, lp._indentation); + }; + + }; //End of ListPrinter + + //This is the IO manipulator. It builds an object of class + //"LispPrinter" that has a special overloaded "<<" operator. + inline LispPrinter lisp(const ASTNode &node, int indentation = 0){ + LispPrinter lp(node, indentation); + return lp; + } + + /***************************************************************************/ + /* Class LispVecPrinter:iomanipulator for printing vector of ASTNodes */ + /***************************************************************************/ + class LispVecPrinter { + + public: + const ASTVec * _vec; + // number of spaces to print before first real + // character of object. + int _indentation; + + // Constructor to build the LispPrinter object + LispVecPrinter(const ASTVec &vec, int indentation){ + _vec = &vec; _indentation = indentation; + } + + friend ostream &operator<<(ostream &os, const LispVecPrinter &lvp){ + LispPrintVec(os, *lvp._vec, lvp._indentation); + return os; + }; + }; //End of Class ListVecPrinter + + //iomanipulator. builds an object of class "LisPrinter" that has a + //special overloaded "<<" operator. + inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0){ + LispVecPrinter lvp(vec, indentation); + return lvp; + } + + + /***************************************************************** + * INLINE METHODS from various classed, declared here because of + * dependencies on classes that are declared later. + *****************************************************************/ + // ASTNode accessor function. + inline Kind ASTNode::GetKind() const { + //cout << "GetKind: " << _int_node_ptr; + return _int_node_ptr->GetKind(); + } + + // FIXME: should be const ASTVec const? + // Declared here because of same ordering problem as GetKind. + inline const ASTVec &ASTNode::GetChildren() const { + return _int_node_ptr->GetChildren(); + } + + // Access node number + inline int ASTNode::GetNodeNum() const { + return _int_node_ptr->_node_num; + } + + inline unsigned int ASTNode::GetIndexWidth () const { + return _int_node_ptr->_index_width; + } + + inline void ASTNode::SetIndexWidth (unsigned int iw) const { + _int_node_ptr->_index_width = iw; + } + + inline unsigned int ASTNode::GetValueWidth () const { + return _int_node_ptr->_value_width; + } + + inline void ASTNode::SetValueWidth (unsigned int vw) const { + _int_node_ptr->_value_width = vw; + } + + //return the type of the ASTNode: 0 iff BOOLEAN; 1 iff BITVECTOR; 2 + //iff ARRAY; 3 iff UNKNOWN; + inline types ASTNode::GetType() const { + if((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN + return BOOLEAN_TYPE; + if((GetIndexWidth() == 0) && (GetValueWidth() > 0)) //BITVECTOR + return BITVECTOR_TYPE; + if((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY + return ARRAY_TYPE; + return UNKNOWN_TYPE; + } + + // Constructor; creates a new pointer, increments refcount of + // pointed-to object. +#ifndef SMTLIB + inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { + if (in) in->IncRef(); + } +#else + inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { }; +#endif + + // Assignment. Increment refcount of new value, decrement refcount + // of old value and destroy if this was the last pointer. FIXME: + // accelerate this by creating an intnode with a ref counter instead + // of pointing to NULL. Need a special check in CleanUp to make + // sure the null node never gets freed. + +#ifndef SMTLIB + inline ASTNode& ASTNode::operator=(const ASTNode& n) { + if (n._int_node_ptr) { + n._int_node_ptr->IncRef(); + } + if (_int_node_ptr) { + _int_node_ptr->DecRef(); + } + _int_node_ptr = n._int_node_ptr; + return *this; + } +#else + inline ASTNode& ASTNode::operator=(const ASTNode& n) { + _int_node_ptr = n._int_node_ptr; + return *this; + } +#endif + +#ifndef SMTLIB + inline void ASTInternal::DecRef() + { + if (--_ref_count == 0) { + // Delete node from unique table and kill it. + CleanUp(); + } + } + + // Destructor + inline ASTNode::~ASTNode() + { + if (_int_node_ptr) { + _int_node_ptr->DecRef(); + } + }; +#else + // No refcounting + inline void ASTInternal::DecRef() + { + } + + // Destructor + inline ASTNode::~ASTNode() + { + }; +#endif + + inline BeevMgr& ASTNode::GetBeevMgr() const { return _int_node_ptr->_bm; } + + /*************************************************************************** + * Class BeevMgr. This holds all "global" variables for the system, such as + * unique tables for the various kinds of nodes. + ***************************************************************************/ + class BeevMgr { + friend class ASTNode; // ASTNode modifies AlreadyPrintedSet + // in BeevMgr + friend class ASTInterior; + friend class ASTBVConst; + friend class ASTSymbol; + + // FIXME: The values appear to be the same regardless of the value of SMTLIB + // initial hash table sizes, to save time on resizing. +#ifdef SMTLIB + static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100; + static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100; + + static const int INITIAL_SIMPLIFY_MAP_SIZE = 100; + static const int INITIAL_SOLVER_MAP_SIZE = 100; + static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; + static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; +#else + // these are the STL defaults + static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; + static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100; + static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100; + + static const int INITIAL_SIMPLIFY_MAP_SIZE = 100; + static const int INITIAL_SOLVER_MAP_SIZE = 100; + static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; + static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; +#endif + + private: + // Typedef for unique Interior node table. + typedef hash_set<ASTInterior *, + ASTInterior::ASTInteriorHasher, + ASTInterior::ASTInteriorEqual> ASTInteriorSet; + + // Typedef for unique Symbol node (leaf) table. + typedef hash_set<ASTSymbol *, + ASTSymbol::ASTSymbolHasher, + ASTSymbol::ASTSymbolEqual> ASTSymbolSet; + + // Unique tables to share nodes whenever possible. + ASTInteriorSet _interior_unique_table; + //The _symbol_unique_table is also the symbol table to be used + //during parsing/semantic analysis + ASTSymbolSet _symbol_unique_table; + + //Typedef for unique BVConst node (leaf) table. + typedef hash_set<ASTBVConst *, + ASTBVConst::ASTBVConstHasher, + ASTBVConst::ASTBVConstEqual> ASTBVConstSet; + + //table to uniquefy bvconst + ASTBVConstSet _bvconst_unique_table; + + // type of memo table. + typedef hash_map<ASTNode, ASTVec, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToVecMap; + + typedef hash_map<ASTNode,ASTNodeSet, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToSetMap; + + // Memo table for bit blasted terms. If a node has already been + // bitblasted, it is mapped to a vector of Boolean formulas for + // the bits. + + //OLD: ASTNodeToVecMap BBTermMemo; + ASTNodeMap BBTermMemo; + + // Memo table for bit blasted formulas. If a node has already + // been bitblasted, it is mapped to a node representing the + // bitblasted equivalent + ASTNodeMap BBFormMemo; + + //public: + // Get vector of Boolean formulas for sum of two + // vectors of Boolean formulas + void BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin); + // Increment + ASTVec BBInc(ASTVec& x); + // Add one bit to a vector of bits. + ASTVec BBAddOneBit(ASTVec& x, ASTNode cin); + // Bitwise complement + ASTVec BBNeg(const ASTVec& x); + // Unary minus + ASTVec BBUminus(const ASTVec& x); + // Multiply. + ASTVec BBMult(const ASTVec& x, const ASTVec& y); + // AND each bit of vector y with single bit b and return the result. + // (used in BBMult) + ASTVec BBAndBit(const ASTVec& y, ASTNode b); + // Returns ASTVec for result - y. This destroys "result". + void BBSub(ASTVec& result, const ASTVec& y); + // build ITE's (ITE cond then[i] else[i]) for each i. + ASTVec BBITE(const ASTNode& cond, + const ASTVec& thn, const ASTVec& els); + // Build a vector of zeros. + ASTVec BBfill(unsigned int width, ASTNode fillval); + // build an EQ formula + ASTNode BBEQ(const ASTVec& left, const ASTVec& right); + + // This implements a variant of binary long division. + // q and r are "out" parameters. rwidth puts a bound on the + // recursion depth. Unsigned only, for now. + void BBDivMod(const ASTVec &y, + const ASTVec &x, + ASTVec &q, + ASTVec &r, + unsigned int rwidth); + + // Return formula for majority function of three formulas. + ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c); + + // Internal bit blasting routines. + ASTNode BBBVLE(const ASTVec& x, const ASTVec& y, bool is_signed); + + // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. + ASTNode BBcompare(const ASTNode& form); + + // Left and right shift one. Writes into x. + void BBLShift(ASTVec& x); + void BBRShift(ASTVec& x); + + public: + // Simplifying create functions + ASTNode CreateSimpForm(Kind kind, ASTVec &children); + ASTNode CreateSimpForm(Kind kind, const ASTNode& child0); + ASTNode CreateSimpForm(Kind kind, + const ASTNode& child0, + const ASTNode& child1); + ASTNode CreateSimpForm(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2); + + ASTNode CreateSimpNot(const ASTNode& form); + + // These are for internal use only. + // FIXME: Find a way to make this local to SimpBool, so they're + // not in AST.h + ASTNode CreateSimpXor(const ASTNode& form1, + const ASTNode& form2); + ASTNode CreateSimpXor(ASTVec &children); + ASTNode CreateSimpAndOr(bool isAnd, + const ASTNode& form1, + const ASTNode& form2); + ASTNode CreateSimpAndOr(bool IsAnd, ASTVec &children); + ASTNode CreateSimpFormITE(const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2); + + + // Declarations of BitBlaster functions (BitBlast.cpp) + public: + // Adds or removes a NOT as necessary to negate a literal. + ASTNode Negate(const ASTNode& form); + + // Bit blast a bitvector term. The term must have a kind for a + // bitvector term. Result is a ref to a vector of formula nodes + // representing the boolean formula. + const ASTNode BBTerm(const ASTNode& term); + + const ASTNode BBForm(const ASTNode& formula); + + // Declarations of CNF conversion (ToCNF.cpp) + public: + // ToCNF converts a bit-blasted Boolean formula to Conjunctive + // Normal Form, suitable for many SAT solvers. Our CNF representation + // is an STL vector of STL vectors, for independence from any particular + // SAT solver's representation. There needs to be a separate driver to + // convert our clauselist to the representation used by the SAT solver. + // Currently, there is only one such solver and its driver is "ToSAT" + + // Datatype for clauses + typedef ASTVec * ClausePtr; + + // Datatype for Clauselists + typedef vector<ClausePtr> ClauseList; + + // Convert a Boolean formula to an equisatisfiable CNF formula. + ClauseList *ToCNF(const ASTNode& form); + + // Print function for debugging + void PrintClauseList(ostream& os, ClauseList& cll); + + // Free the clause list and all its clauses. + void DeleteClauseList(BeevMgr::ClauseList *cllp); + + // Map from formulas to representative literals, for debugging. + ASTNodeMap RepLitMap; + + private: + // Global for assigning new node numbers. + int _max_node_num; + + const ASTNode ASTFalse, ASTTrue, ASTUndefined; + + // I just did this so I could put it in as a fake return value in + // methods that return a ASTNode &, to make -Wall shut up. + ASTNode dummy_node; + + //BeevMgr Constructor, Destructor and other misc. functions + public: + + int NewNodeNum() { _max_node_num += 2; return _max_node_num; } + + // Table for DAG printing. + ASTNodeSet AlreadyPrintedSet; + + //Tables for Presentation language printing + + //Nodes seen so far + ASTNodeSet PLPrintNodeSet; + + //Map from ASTNodes to LetVars + ASTNodeMap NodeLetVarMap; + + //This is a vector which stores the Node to LetVars pairs. It + //allows for sorted printing, as opposed to NodeLetVarMap + std::vector<pair<ASTNode,ASTNode> > NodeLetVarVec; + + //a partial Map from ASTNodes to LetVars. Needed in order to + //correctly print shared subterms inside the LET itself + ASTNodeMap NodeLetVarMap1; + + //functions to lookup nodes from the memo tables. these should be + //private. + private: + //Destructively appends back_child nodes to front_child nodes. + //If back_child nodes is NULL, no appending is done. back_child + //nodes are not modified. Then it returns the hashed copy of the + //node, which is created if necessary. + ASTInterior *CreateInteriorNode(Kind kind, + ASTInterior *new_node, + // this is destructively modified. + const ASTVec & back_children = _empty_ASTVec); + + // Create unique ASTInterior node. + ASTInterior *LookupOrCreateInterior(ASTInterior *n); + + // Create unique ASTSymbol node. + ASTSymbol *LookupOrCreateSymbol(ASTSymbol& s); + + // Called whenever we want to make sure that the Symbol is + // declared during semantic analysis + bool LookupSymbol(ASTSymbol& s); + + // Called by ASTNode constructors to uniqueify ASTBVConst + ASTBVConst *LookupOrCreateBVConst(ASTBVConst& s); + + //Public functions for CreateNodes and Createterms + public: + // Create and return an ASTNode for a symbol + ASTNode CreateSymbol(const char * const name); + + // Create and return an ASTNode for a symbol + // Width is number of bits. + ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst); + ASTNode CreateZeroConst(unsigned int width); + ASTNode CreateOneConst(unsigned int width); + ASTNode CreateTwoConst(unsigned int width); + ASTNode CreateMaxConst(unsigned int width); + + // Create and return an ASTNode for a symbol + // Optional base was a problem because 0 could be an int or char *, + // so CreateBVConst was ambiguous. + ASTNode CreateBVConst(const char *strval, int base); + + //FIXME This is a dangerous function + ASTNode CreateBVConst(CBV bv, unsigned width); + + // Create and return an interior ASTNode + ASTNode CreateNode(Kind kind, const ASTVec &children = _empty_ASTVec); + + ASTNode CreateNode(Kind kind, + const ASTNode& child0, + const ASTVec &children = _empty_ASTVec); + + ASTNode CreateNode(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec &children = _empty_ASTVec); + + ASTNode CreateNode(Kind kind, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec &children = _empty_ASTVec); + + // Create and return an ASTNode for a term + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, children); + n.SetValueWidth(width); + + //by default we assume that the term is a Bitvector. If + //necessary the indexwidth can be changed later + n.SetIndexWidth(0); + return n; + } + + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTNode& child0, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, child0, children); + n.SetValueWidth(width); + return n; + } + + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, child0, child1, children); + n.SetValueWidth(width); + return n; + } + + inline ASTNode CreateTerm(Kind kind, + unsigned int width, + const ASTNode& child0, + const ASTNode& child1, + const ASTNode& child2, + const ASTVec &children = _empty_ASTVec) { + if(!is_Term_kind(kind)) + FatalError("CreateTerm: Illegal kind to CreateTerm:",ASTUndefined, kind); + ASTNode n = CreateNode(kind, child0, child1, child2, children); + n.SetValueWidth(width); + return n; + } + + ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg); + ASTNode SimplifyFormula_TopLevel(const ASTNode& a, bool pushNeg); + ASTNode SimplifyFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyTerm_TopLevel(const ASTNode& b); + ASTNode SimplifyTerm(const ASTNode& a); + void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); + private: + //memo table for simplifcation + ASTNodeMap SimplifyMap; + ASTNodeMap SimplifyNegMap; + ASTNodeMap SolverMap; + ASTNodeSet AlwaysTrueFormMap; + ASTNodeMap MultInverseMap; + + public: + ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg); + ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2); + ASTNode ITEOpt_InEqs(const ASTNode& in1); + ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3); + ASTNode CreateSimplifiedINEQ(Kind k, const ASTNode& a0, const ASTNode& a1, bool pushNeg); + ASTNode SimplifyNotFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyAndOrFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyXorFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyNandFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyNorFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyImpliesFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyIffFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyIteFormula(const ASTNode& a, bool pushNeg); + ASTNode FlattenOneLevel(const ASTNode& a); + ASTNode FlattenAndOr(const ASTNode& a); + ASTNode CombineLikeTerms(const ASTNode& a); + ASTNode LhsMinusRhs(const ASTNode& eq); + ASTNode DistributeMultOverPlus(const ASTNode& a, + bool startdistribution=false); + ASTNode ConvertBVSXToITE(const ASTNode& a); + //checks if the input constant is odd or not + bool BVConstIsOdd(const ASTNode& c); + //computes the multiplicatve inverse of the input + ASTNode MultiplicativeInverse(const ASTNode& c); + + void ClearAllTables(void); + void ClearAllCaches(void); + int BeforeSAT_ResultCheck(const ASTNode& q); + int CallSAT_ResultCheck(MINISAT::Solver& newS, + const ASTNode& q, const ASTNode& orig_input); + int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, + const ASTNode& q, const ASTNode& orig_input); + int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); + //creates array write axiom only for the input term or formula, if + //necessary. If there are no axioms to produce then it simply + //generates TRUE + ASTNode Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, const ASTNode& array_newname); + ASTVec ArrayWrite_RemainingAxioms; + //variable indicates that counterexample will now be checked by + //the counterexample checker, and hence simplifyterm must switch + //off certain optimizations. In particular, array write + //optimizations + bool start_abstracting; + bool Begin_RemoveWrites; + bool SimplifyWrites_InPlace_Flag; + + void CopySolverMap_To_CounterExample(void); + //int LinearSearch(const ASTNode& orig_input); + //Datastructures and functions needed for counterexample + //generation, and interface with MINISAT + private: + /* MAP: This is a map from ASTNodes to MINISAT::Vars. + * + * The map is populated while ASTclauses are read from the AST + * ClauseList returned by CNF converter. For every new boolean + * variable in ASTClause a new MINISAT::Var is created (these vars + * typedefs for ints) + */ + typedef hash_map<ASTNode, MINISAT::Var, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTtoSATMap; + ASTtoSATMap _ASTNode_to_SATVar; + + public: + //converts the clause to SAT and calls SAT solver + bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll); + + ///print SAT solver statistics + void PrintStats(MINISAT::SolverStats& stats); + + //accepts query and returns the answer. if query is valid, return + //true, else return false. Automatically constructs counterexample + //for invalid queries, and prints them upon request. + int TopLevelSAT(const ASTNode& query, const ASTNode& asserts); + + // Debugging function to find problems in BitBlast and ToCNF. + // See body in ToSAT.cpp for more explanation. + ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form); + + // Internal recursive body of above. + ASTNode CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form); + + // Helper function for CheckBBandCNF + ASTNode SymbolTruthValue(MINISAT::Solver &newS, ASTNode form); + + //looksup a MINISAT var from the minisat-var memo-table. if none + //exists, then creates one. + const MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n); + + // Memo table for CheckBBandCNF debugging function + ASTNodeMap CheckBBandCNFMemo; + + + //Data structures for Array Read Transformations + private: + /* MAP: This is a map from Array Names to list of array-read + * indices in the input. This map is used by the TransformArray() + * function + * + * This map is useful in converting array reads into nested ITE + * constructs. Suppose there are two array reads in the input + * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a + * symbolic constant, say v1, and Read(A,j) is replaced with the + * following ITE: + * + * ITE(i=j,v1,v2) + */ + //CAUTION: I tried using a set instead of vector for + //readindicies. for some odd reason the performance went down + //considerably. this is totally inexplicable. + ASTNodeToVecMap _arrayname_readindices; + + /* MAP: This is a map from Array Names to nested ITE constructs, + * which are built as described below. This map is used by the + * TransformArray() function + * + * This map is useful in converting array reads into nested ITE + * constructs. Suppose there are two array reads in the input + * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a + * symbolic constant, say v1, and Read(A,j) is replaced with the + * following ITE: + * + * ITE(i=j,v1,v2) + */ + ASTNodeMap _arrayread_ite; + + /*MAP: This is a map from array-reads to symbolic constants. This + *map is used by the TransformArray() + */ + ASTNodeMap _arrayread_symbol; + + ASTNodeSet _introduced_symbols; + + /*Memoization map for TransformFormula/TransformTerm/TransformArray function + */ + ASTNodeMap TransformMap; + + //count to keep track of new symbolic constants introduced + //corresponding to Array Reads + unsigned int _symbol_count; + + //Formula/Term Transformers. Let Expr Manager, Type Checker + public: + //Functions that Transform ASTNodes + ASTNode TransformFormula(const ASTNode& query); + ASTNode TransformTerm(const ASTNode& term); + ASTNode TransformArray(const ASTNode& term); + ASTNode TranslateSignedDivMod(const ASTNode& term); + + //LET Management + private: + // MAP: This map is from bound IDs that occur in LETs to + // expression. The map is useful in checking replacing the IDs + // with the corresponding expressions. + ASTNodeMap _letid_expr_map; + public: + + ASTNode ResolveID(const ASTNode& var); + + //Functions that are used to manage LET expressions + void LetExprMgr(const ASTNode& var, const ASTNode& letExpr); + + //Delete Letid Map + void CleanupLetIDMap(void); + + //Allocate LetID map + void InitializeLetIDMap(void); + + //Substitute Let-vars with LetExprs + ASTNode SubstituteLetExpr(ASTNode inExpr); + + /* MAP: This is a map from MINISAT::Vars to ASTNodes + * + * This is a reverse map, useful in constructing + * counterexamples. MINISAT returns a model in terms of MINISAT + * Vars, and this map helps us convert it to a model over ASTNode + * variables. + */ + vector<ASTNode> _SATVar_to_AST; + + private: + /* MAP: This is a map from ASTNodes to vectors of bits + * + * This map is used in constructing and printing + * counterexamples. MINISAT returns values for each bit (a + * BVGETBIT Node), and this maps allows us to assemble the bits + * into bitvectors. + */ + typedef hash_map<ASTNode, hash_map<unsigned int, bool> *, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTtoBitvectorMap; + ASTtoBitvectorMap _ASTNode_to_Bitvector; + + //Data structure that holds the counter-model + ASTNodeMap CounterExampleMap; + + //Checks if the counter_example is ok. In order for the + //counter_example to be ok, Every assert must evaluate to true + //w.r.t couner_example and the query must evaluate to + //false. Otherwise the counter_example is bogus. + void CheckCounterExample(bool t); + + //Converts a vector of bools to a BVConst + ASTNode BoolVectoBVConst(hash_map<unsigned,bool> * w, unsigned int l); + + //accepts a term and turns it into a constant-term w.r.t counter_example + ASTNode TermToConstTermUsingModel(const ASTNode& term, bool ArrayReadFlag = true); + ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool ArrayReadFlag = true); + //Computes the truth value of a formula w.r.t counter_example + ASTNode ComputeFormulaUsingModel(const ASTNode& form); + + //Replaces WRITE(Arr,i,val) with ITE(j=i, val, READ(Arr,j)) + ASTNode RemoveWrites_TopLevel(const ASTNode& term); + ASTNode RemoveWrites(const ASTNode& term); + ASTNode SimplifyWrites_InPlace(const ASTNode& term); + ASTNode ReadOverWrite_To_ITE(const ASTNode& term); + + ASTNode NewArrayVar(unsigned int index, unsigned int value); + ASTNode NewVar(unsigned int valuewidth); + //For ArrayWrite Abstraction: map from read-over-write term to + //newname. + ASTNodeMap ReadOverWrite_NewName_Map; + //For ArrayWrite Refinement: Map new arraynames to Read-Over-Write + //terms + ASTNodeMap NewName_ReadOverWrite_Map; + + public: + //print the STP solver output + void PrintOutput(bool true_iff_valid); + + //Converts MINISAT counterexample into an AST memotable (i.e. the + //function populates the datastructure CounterExampleMap) + void ConstructCounterExample(MINISAT::Solver& S); + + //Prints the counterexample to stdout + void PrintCounterExample(bool t,std::ostream& os=cout); + + //Prints the counterexample to stdout + void PrintCounterExample_InOrder(bool t); + + //queries the counterexample, and returns the value corresponding + //to e + ASTNode GetCounterExample(bool t, const ASTNode& e); + + int CounterExampleSize(void) const {return CounterExampleMap.size();} + + //FIXME: This is bloody dangerous function. Hack attack to take + //care of requests from users who want to store complete + //counter-examples in their own data structures. + ASTNodeMap GetCompleteCounterExample() {return CounterExampleMap;} + + // prints MINISAT assigment one bit at a time, for debugging. + void PrintSATModel(MINISAT::Solver& S); + + //accepts constant input and normalizes it. + ASTNode BVConstEvaluator(const ASTNode& t); + + //FUNCTION TypeChecker: Assumes that the immediate Children of the + //input ASTNode have been typechecked. This function is suitable + //in scenarios like where you are building the ASTNode Tree, and + //you typecheck as you go along. It is not suitable as a general + //typechecker + void BVTypeCheck(const ASTNode& n); + + private: + //stack of Logical Context. each entry in the stack is a logical + //context. A logical context is a vector of assertions. The + //logical context is represented by a ptr to a vector of + //assertions in that logical context. Logical contexts are created + //by PUSH/POP + std::vector<ASTVec *> _asserts; + //The query for the current logical context. + ASTNode _current_query; + + //this flag, when true, indicates that counterexample is being + //checked by the counterexample checker + bool counterexample_checking_during_refinement; + + //this flag indicates as to whether the input has been determined to + //be valid or not by this tool + bool ValidFlag; + + //this flag, when true, indicates that a BVDIV divide by zero + //exception occured. However, the program must not exit with a + //fatalerror. Instead, it should evaluate the whole formula (which + //contains the BVDIV term) to be FALSE. + bool bvdiv_exception_occured; + + public: + //set of functions that manipulate Logical Contexts. + // + //add an assertion to the current logical context + void AddAssert(const ASTNode& assert); + void Push(void); + void Pop(void); + void AddQuery(const ASTNode& q); + const ASTNode PopQuery(); + const ASTNode GetQuery(); + const ASTVec GetAsserts(void); + + //reports node size. Second arg is "clearstatinfo", whatever that is. + unsigned int NodeSize(const ASTNode& a, bool t = false); + + private: + //This memo map is used by the ComputeFormulaUsingModel() + ASTNodeMap ComputeFormulaMap; + //Map for statiscal purposes + ASTNodeSet StatInfoSet; + + + ASTNodeMap TermsAlreadySeenMap; + ASTNode CreateSubstitutionMap(const ASTNode& a); + public: + //prints statistics for the ASTNode. can add a prefix string c + void ASTNodeStats(const char * c, const ASTNode& a); + + //substitution + bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); + bool CheckSubstitutionMap(const ASTNode& a); + bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); + //if (a > b) in the termorder, then return 1 + //elseif (a < b) in the termorder, then return -1 + //else return 0 + int TermOrder(const ASTNode& a, const ASTNode& b); + //fill the arrayname_readindices vector if e0 is a READ(Arr,index) + //and index is a BVCONST + void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1); + bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); + + //functions for checking and updating simplifcation map + bool CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg); + void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg); + bool CheckAlwaysTrueFormMap(const ASTNode& key); + void UpdateAlwaysTrueFormMap(const ASTNode& val); + bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); + void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); + + //Map for solved variables + bool CheckSolverMap(const ASTNode& a, ASTNode& output); + bool CheckSolverMap(const ASTNode& a); + bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); + public: + //FIXME: HACK_ATTACK. this vector was hacked into the code to + //support a special request by Dawson' group. They want the + //counterexample to be printed in the order of variables declared. + //TO BE COMMENTED LATER (say by 1st week of march,2006) + ASTVec _special_print_set; + + //prints the initial activity levels of variables + void PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS); + + //this function biases the activity levels of MINISAT variables. + void ChangeActivityLevels_Of_SATVars(MINISAT::Solver& n); + + // Constructor + BeevMgr() : _interior_unique_table(INITIAL_INTERIOR_UNIQUE_TABLE_SIZE), + _symbol_unique_table(INITIAL_SYMBOL_UNIQUE_TABLE_SIZE), + _bvconst_unique_table(INITIAL_BVCONST_UNIQUE_TABLE_SIZE), + BBTermMemo(INITIAL_BBTERM_MEMO_TABLE_SIZE), + BBFormMemo(INITIAL_BBFORM_MEMO_TABLE_SIZE), + _max_node_num(0), + ASTFalse(CreateNode(FALSE)), + ASTTrue(CreateNode(TRUE)), + ASTUndefined(CreateNode(UNDEFINED)), + SimplifyMap(INITIAL_SIMPLIFY_MAP_SIZE), + SimplifyNegMap(INITIAL_SIMPLIFY_MAP_SIZE), + SolverMap(INITIAL_SOLVER_MAP_SIZE), + _arrayread_symbol(INITIAL_ARRAYREAD_SYMBOL_SIZE), + _introduced_symbols(INITIAL_INTRODUCED_SYMBOLS_SIZE), + _symbol_count(0) { + _current_query = ASTUndefined; + ValidFlag = false; + bvdiv_exception_occured = false; + counterexample_checking_during_refinement = false; + start_abstracting = false; + Begin_RemoveWrites = false; + SimplifyWrites_InPlace_Flag = false; + }; + + //destructor + ~BeevMgr(); + }; //End of Class BeevMgr + + + class CompleteCounterExample { + ASTNodeMap counterexample; + BeevMgr * bv; + public: + CompleteCounterExample(ASTNodeMap a, BeevMgr* beev) : counterexample(a), bv(beev){} + ASTNode GetCounterExample(ASTNode e) { + if(BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind()) { + FatalError("You must input a term or propositional variables\n",e); + } + if(counterexample.find(e) != counterexample.end()) { + return counterexample[e]; + } + else { + if(SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType()) { + return bv->CreateNode(BEEV::FALSE); + } + + if(SYMBOL == e.GetKind()) { + ASTNode z = bv->CreateZeroConst(e.GetValueWidth()); + return z; + } + + return e; + } + } + }; + +}; // end namespace BEEV +#endif diff --git a/stp/AST/ASTKind.kinds b/stp/AST/ASTKind.kinds new file mode 100644 index 00000000..03112eb8 --- /dev/null +++ b/stp/AST/ASTKind.kinds @@ -0,0 +1,71 @@ +#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 new file mode 100644 index 00000000..bc36812c --- /dev/null +++ b/stp/AST/ASTUtil.cpp @@ -0,0 +1,45 @@ +/******************************************************************** + * 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 <ostream> + +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<const char*,int,hash<const char*>,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 new file mode 100644 index 00000000..0ed6bfa2 --- /dev/null +++ b/stp/AST/ASTUtil.h @@ -0,0 +1,107 @@ +/******************************************************************** + * 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 <cstring> +#include <iostream> +#include <vector> +#ifdef EXT_HASH_MAP +#include <ext/hash_set> +#include <ext/hash_map> +#else +#include <hash_set> +#include <hash_map> +#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<const char*,int, + hash<const char *>,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 new file mode 100644 index 00000000..de78ec74 --- /dev/null +++ b/stp/AST/BitBlast.cpp @@ -0,0 +1,812 @@ +/******************************************************************** + * 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"<<endl; + // cout << "================" << endl << "BBTerm:" << term << endl; + // cout << "----------------" << endl << "BBTerm result:"; + // lpvec(result); + // cout << endl; + + return (BBTermMemo[term] = result); + +} + +// bit blast a formula (boolean term). Result is one bit wide, +// so it returns a single ASTNode. +// FIXME: Add IsNegated flag. +const ASTNode BeevMgr::BBForm(const ASTNode& form) +{ + + ASTNodeMap::iterator it = BBFormMemo.find(form); + if (it != BBFormMemo.end()) { + // already there. Just return it. + return it->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 new file mode 100644 index 00000000..0218510b --- /dev/null +++ b/stp/AST/Makefile @@ -0,0 +1,54 @@ +include ../Makefile.common + +SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp +OBJS = $(SRCS:.cpp=.o) + +#Make the ast library for use by other modules +libast.a: $(OBJS) + -rm -rf $@ + $(AR) rc libast.a $(OBJS) + $(RANLIB) libast.a + +ASTKind.o: ASTKind.h ASTKind.cpp + $(CXX) $(CXXFLAGS) -c -o ASTKind.o ASTKind.cpp + +# ASTKind.h and ASTKind.cpp are automatically generated +ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl + ./genkinds.pl + +# cnftest: cnftest.o ToCNF.o AST.o ASTUtil.o ASTKind.o BitBlast.o AST.h +# $(CC) $(LDFLAGS) ToCNF.o BitBlast.o ASTKind.o ASTUtil.o AST.o cnftest.o -o cnftest + +# bbtest: $(OBJS) +# $(CC) $(LDFLAGS) BitBlast.o ASTKind.o ASTUtil.o AST.o bbtest.o -o bbtest + +# asttest: $(OBJS) +# $(CC) $(LDFLAGS) ASTKind.o ASTUtil.o AST.o asttest.o -lstdc++ -o asttest + +clean: + rm -rf *.o *~ bbtest asttest cnftest *.a ASTKind.h ASTKind.cpp .#* + +depend: + makedepend -Y -- $(CFLAGS) -- $(SRCS) +# DO NOT DELETE + +AST.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h +AST.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h +AST.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h +ASTUtil.o: ASTUtil.h +BitBlast.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h +BitBlast.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h +BitBlast.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h +SimpBool.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h +SimpBool.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h +SimpBool.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h +ToCNF.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h +ToCNF.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h +ToCNF.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h +ToSAT.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h +ToSAT.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h +ToSAT.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h +ToSAT.o: ../simplifier/bvsolver.h ../AST/AST.h +Transform.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h +Transform.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h +Transform.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h diff --git a/stp/AST/STLport_config.h b/stp/AST/STLport_config.h new file mode 100644 index 00000000..9b7bc14f --- /dev/null +++ b/stp/AST/STLport_config.h @@ -0,0 +1,20 @@ +/******************************************************************** + * 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 new file mode 100644 index 00000000..67f9825d --- /dev/null +++ b/stp/AST/SimpBool.cpp @@ -0,0 +1,408 @@ +/******************************************************************** + * 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 new file mode 100644 index 00000000..2a18b3f5 --- /dev/null +++ b/stp/AST/ToCNF.cpp @@ -0,0 +1,506 @@ +/******************************************************************** + * 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 new file mode 100644 index 00000000..7a164c9c --- /dev/null +++ b/stp/AST/ToSAT.cpp @@ -0,0 +1,1385 @@ +/******************************************************************** + * 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 <math.h> + + +namespace BEEV { + /* FUNCTION: lookup or create a new MINISAT literal + * lookup or create new MINISAT Vars from the global MAP + * _ASTNode_to_SATVar. + */ + const 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<MINISAT::Lit> 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<MINISAT::vec<MINISAT::Lit> >)(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(); + reportf("restarts : %"I64_fmt"\n", s.starts); + reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); + reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); + reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); + reportf("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) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); + reportf("CPU time : %g s\n", cpu_time); + } + + // 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<unsigned,bool> * v; + if(_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end()) + _ASTNode_to_Bitvector[symbol] = new hash_map<unsigned,bool>(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<unsigned,bool> * 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<int> 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<unsigned,bool> * 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 new file mode 100644 index 00000000..598b831e --- /dev/null +++ b/stp/AST/Transform.cpp @@ -0,0 +1,492 @@ +/******************************************************************** + * 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 <stdlib.h> +#include <stdio.h> +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/asttest.cpp b/stp/AST/asttest.cpp new file mode 100644 index 00000000..57f3d20c --- /dev/null +++ b/stp/AST/asttest.cpp @@ -0,0 +1,29 @@ +#include "AST.h" + +using namespace BEEV; + +int main() +{ + + BeevMgr * bm = new BeevMgr(); + ASTNode s1 = bm->CreateSymbol("foo"); + s1 = bm->CreateSymbol("foo1"); + s1 = bm->CreateSymbol("foo2"); + ASTNode s2 = bm->CreateSymbol("bar"); + cout << "s1" << s1 << endl; + cout << "s2" << s2 << endl; + + ASTNode b1 = bm->CreateBVConst(5,12); + ASTNode b2 = bm->CreateBVConst(6,36); + cout << "b1: " << b1 << endl; + cout << "b2: " << b2 << endl; + + ASTNode a1 = bm->CreateNode(EQ, s1, s2); + ASTNode a2 = bm->CreateNode(AND, s1, s2); + a1 = bm->CreateNode(OR, s1, s2); + ASTNode a3 = bm->CreateNode(IMPLIES, a1, a2); + ASTNode a4 = bm->CreateNode(IMPLIES, s1, a2); + cout << "a3" << a3 << endl; + cout << "a4" << a4 << endl; + return 0; +} diff --git a/stp/AST/bbtest.cpp b/stp/AST/bbtest.cpp new file mode 100644 index 00000000..83aa6a4e --- /dev/null +++ b/stp/AST/bbtest.cpp @@ -0,0 +1,96 @@ +#include "AST.h" + +using namespace BEEV; + +int main() +{ + const int size = 32; + + BeevMgr *bm = new BeevMgr(); + ASTNode s1 = bm->CreateSymbol("x"); + s1.SetValueWidth(size); + cout << "s1" << s1 << endl; + ASTNode s2 = bm->CreateSymbol("y"); + s2.SetValueWidth(size); + cout << "s2" << s2 << endl; + ASTNode s3 = bm->CreateSymbol("z"); + s3.SetValueWidth(size); + cout << "s3" << s3 << endl; + + ASTNode c1 = bm->CreateBVConst(size,0); + cout << "c1" << c1 << endl; + ASTVec bbc1 = bm->BBTerm(c1); + cout << "bitblasted c1 " << endl; + LispPrintVec(cout, bbc1, 0); + cout << endl; + bm->AlreadyPrintedSet.clear(); + + ASTNode c2 = bm->CreateBVConst(size,1); + c2.SetValueWidth(size); + cout << "c2" << c2 << endl; + ASTVec bbc2 = bm->BBTerm(c2); + cout << "bitblasted c2 " << endl; + LispPrintVec(cout, bbc2, 0); + cout << endl; + bm->AlreadyPrintedSet.clear(); + + ASTNode c3 = bm->CreateBVConst(size, 0xFFFFFFFF); + c3.SetValueWidth(size); + cout << "c3" << c3 << endl; + ASTVec bbc3 = bm->BBTerm(c3); + cout << "bitblasted c3 " << endl; + LispPrintVec(cout, bbc3, 0); + cout << endl; + bm->AlreadyPrintedSet.clear(); + + ASTNode c4 = bm->CreateBVConst(size, 0xAAAAAAAA); + c4.SetValueWidth(size); + cout << "c4" << c4 << endl; + ASTVec bbc4 = bm->BBTerm(c4); + cout << "bitblasted c4 " << endl; + LispPrintVec(cout, bbc4, 0); + cout << endl; + bm->AlreadyPrintedSet.clear(); + +// ASTNode b1 = bm->CreateBVConst(12); +// ASTNode b2 = bm->CreateBVConst(36); +// cout << "b1: " << b1 << endl; +// cout << "b2: " << b2 << endl; + + ASTNode a1 = bm->CreateNode(BVPLUS, s1, s2); + a1.SetValueWidth(size); + + ASTVec& bba1 = bm->BBTerm(a1); + cout << "bitblasted a1 " << endl; + LispPrintVec(cout, bba1, 0); + cout << endl; + bm->AlreadyPrintedSet.clear(); + + ASTNode a2 = bm->CreateNode(BVPLUS, s1, s2, s3); + a1.SetValueWidth(2); + + ASTVec& bba2 = bm->BBTerm(a2); + cout << "bitblasted a2 " << endl; + LispPrintVec(cout, bba2, 0); + cout << endl; + bm->AlreadyPrintedSet.clear(); + + ASTNode a3 = bm->CreateNode(BVXOR, s1, s2); + a3.SetValueWidth(2); + + ASTVec& bba3 = bm->BBTerm(a3); + cout << "bitblasted a3 " << endl; + LispPrintVec(cout, bba3, 0); + cout << endl; + bm->AlreadyPrintedSet.clear(); + + ASTNode a4 = bm->CreateNode(EQ, s1, s2); + ASTNode bba4 = bm->BBForm(a4); + cout << "bitblasted a4 " << endl << bba4 << endl; + + ASTNode a5 = bm->CreateNode(BVLE, s1, s2); + ASTNode bba5 = bm->BBForm(a5); + cout << "bitblasted a5 " << endl << bba5 << endl; + + return 0; +} diff --git a/stp/AST/cnftest.cpp b/stp/AST/cnftest.cpp new file mode 100644 index 00000000..7ce270c8 --- /dev/null +++ b/stp/AST/cnftest.cpp @@ -0,0 +1,47 @@ +// -*- c++ -*- + +// Test program for CNF conversion. + +#include "AST.h" + +using namespace BEEV; + +int main() +{ + const int size = 1; + + BeevMgr *bm = new BeevMgr(); + ASTNode s1 = bm->CreateSymbol("x"); + s1.SetValueWidth(size); + + cout << "s1" << s1 << endl; + ASTNode s2 = bm->CreateSymbol("y"); + s2.SetValueWidth(size); + + cout << "s2" << s2 << endl; + ASTNode s3 = bm->CreateSymbol("z"); + s3.SetValueWidth(size); + + cout << "s3" << s3 << endl; + + ASTNode bbs1 = bm->BBForm(s1); + cout << "bitblasted s1" << endl << bbs1 << endl; + bm->PrintClauseList(cout, bm->ToCNF(bbs1)); + + ASTNode a2 = bm->CreateNode(AND, s1, s2); + ASTNode bba2 = bm->BBForm(a2); + cout << "bitblasted a2" << endl << bba2 << endl; + bm->PrintClauseList(cout, bm->ToCNF(bba2)); + + ASTNode a3 = bm->CreateNode(OR, s1, s2); + ASTNode bba3 = bm->BBForm(a3); + cout << "bitblasted a3" << endl << bba3 << endl; + bm->PrintClauseList(cout, bm->ToCNF(bba3)); + + ASTNode a4 = bm->CreateNode(EQ, s1, s2); + ASTNode bba4 = bm->BBForm(a4); + cout << "bitblasted a4 " << endl << bba4 << endl; + + bm->PrintClauseList(cout, bm->ToCNF(bba4)); + +} diff --git a/stp/AST/genkinds.pl b/stp/AST/genkinds.pl new file mode 100755 index 00000000..7944832b --- /dev/null +++ b/stp/AST/genkinds.pl @@ -0,0 +1,123 @@ +#!/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 = <KFILE>; + 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; |