diff options
Diffstat (limited to 'stp/AST/ToCNF.cpp')
| -rw-r--r-- | stp/AST/ToCNF.cpp | 506 |
1 files changed, 0 insertions, 506 deletions
diff --git a/stp/AST/ToCNF.cpp b/stp/AST/ToCNF.cpp deleted file mode 100644 index 2a18b3f5..00000000 --- a/stp/AST/ToCNF.cpp +++ /dev/null @@ -1,506 +0,0 @@ -/******************************************************************** - * AUTHORS: David L. Dill, Vijay Ganesh - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -// THEORY: This code translates an arbitrary Boolean DAG, generated by -// the BitBlast.cpp, to an equi-satisfiable CNF formula. There are -// four kinds of variables in the CNF formula: (1) propositional -// variables from the original formula; (2) BVGETBIT formulas from the -// original formula (a precondition is that the BVGETBIT can only be -// applied to bitvector-valued variables, array reads, or -// uninterpreted functions); (3) TRUE; or (4) representative variables -// (see below). Each literal in the CNF formula is one of these or -// its negation. - -// It is convenient (though not perfectly efficient) to be able to add -// TRUE and FALSE constants to clauses, which is not allowed in CNF. -// So, there is a "dummy variable" representing TRUE, which is used in -// its place (so FALSE is represented by the negation of the dummy -// var). The CNF formula has a unit clause containing this dummy -// variable, so that any satisfying assignment must make the dummy var -// TRUE. - -// Every sub-formula of the input formula has a "representative -// literal." A truth assignment satisfies the CNF formula iff the -// restriction of that assignment to the original variables satisfies -// the original formula, AND the rep lits have the same truth values -// as the subformulas they represent in the original formula. In the -// trivial cases, the representative literal is the input variable, or -// dummy true var, or its negation. Representative literals may be -// negated variables -- essentially, only AND formulas are translated, -// and everything else is handled by rewriting or negating formulas. -// The representative for (NOT alpha) is the negation of the -// representative for alpha. - -// The translation is performed by ToCNF_int, which traverses the original -// formula. ToCNF adds clauses that constrain the representative variables -// to be equal to the truth values of the formulas they represent. -// ToCNF always returns a literal whose value must be equivalent to the formula -// it translated. In trivial cases, this literal is a literal from the original -// formula, or the dummy true/false literals. If the formula is of the form -// (not alpha), ToCNF_int negates the literal representing alpha (which may -// itself be a negative literal) and returns it. Otherwise, ToCNF_int assigns -// a new rep var, adds the clauses, and returns the new var. ToCNF_int is -// memoized so that it doesn't assign more than one variable to a subformula, -// and to prevent exponential numbers of redundant visits to shared subformulas. - -// In reality, only AND/OR/NOT formulas are translated directly. Everything -// else (XOR, IFF, IMPLIES) is rewritten on-the-fly into these forms. I -// could have done that in bit-blasting, but I thought that, in the future, -// we might be able to translate these operations differently in different -// contexts to optimize the CNF formula. - -// FIXME: Inspection of the clauses is kind of horrifying. In -// addition to true/false, there are duplicate literals and duplicate -// clauses all over the place. -#include "AST.h" -static bool CNF_trace = false; -namespace BEEV { -/** Statistics class. Total number of variables is best tracked in - ToSAT. Number of clauses is just cll.size() */ - -class CNFstats { -public: - int _num_new_rep_vars; - int _num_clauses; - - // constructor - CNFstats() : _num_new_rep_vars(0), _num_clauses(0) {} - - void printStats() { - if(stats) { - cout << "ToCNF statistics:" << endl; - cout << "Number of new representative variables: " - << _num_new_rep_vars << endl; - cout << "Number of new clauses: " - << _num_clauses << endl; - } - } - -}; - - -/** This class contains private data and function members for the - CNF conversion */ -class CNFMgr { - - friend class BeevMgr; - -public: - - // Needed in the body of BeevMgr::ToCNF. It's not visible outside - // this file, though. - ASTNode dummy_true_var; - - // CNF Pre-pass - ASTNodeMap ToCNFPrePassMemo; - - // CNF Memo Table. - ASTNodeMap CNFMemo; - - -private: - - // Pointer back to BeevMgr with the node tables, etc. - BeevMgr *bm; - - // For ToCNF conversion. This holds a dummy variable representing - // "True". It is added as a unit clause, so that it will be assigned - // to true and propagated immediately by any CNF solver. - - ASTNode dummy_false_var; // not of dummy_true_var - - CNFstats stats; - - // constructor - CNFMgr(BeevMgr *bmgr) - { - bm = bmgr; - - // Dummy variable so TRUE can be a literal. - dummy_true_var = bm->CreateSymbol("*TrueDummy*"); - dummy_false_var = bm->CreateSimpNot(dummy_true_var); - } - - // Returns true iff result has been memoized. - // if it returns true, result is returned in by-ref parameter "result" - // Consider just putitng this in-line. - bool CNFIsMemoized(ASTNode &form, ASTNode &result) - { - ASTNodeMap::iterator it = CNFMemo.find(form); - if (it != CNFMemo.end()) { - result = it->second; //already there. Just return it. - return true; - } - else { - return false; - } - } - - - // Convert a big XOR to a bunch of AND/ORs. Assumes subformulas have - // already been converted. - ASTNode convertXORs(ASTVec children) - { - ASTNode accum = children[0]; - ASTVec::iterator itend = children.end(); - for (ASTVec::iterator it = children.begin()+1; it < itend; it++) { - // a XOR b -> (a | b) & (!a | !b) - - // For each XOR node with k children, creates approximately - // 5*(k-1) nodes. AND + 2 OR + 2 NOT. - - ASTNode or1 = bm->CreateNode(OR, accum, *it); - ASTNode or2 = bm->CreateNode(OR, bm->CreateSimpNot(accum), bm->CreateSimpNot(*it)); - accum = bm->CreateNode(AND, or1, or2); - - } - - return accum; - } - - - // Do preliminary transformations on bitblasted formula to make - // CNF conversion easier. - // Converts XORs to AND/OR form. - ASTNode ToCNFPrePass(const ASTNode &form) - { - - // Check memo table - ASTNodeMap::iterator mem_it = ToCNFPrePassMemo.find(form); - if (mem_it != ToCNFPrePassMemo.end()) { - return mem_it->second; - } - - ASTNode result; - - ASTVec new_children; - ASTVec::const_iterator endit = form.end(); - for (ASTVec::const_iterator it = form.begin(); it != endit; it++) { - ASTNode ch = ToCNFPrePass(*it); - new_children.push_back(ch); - } - - Kind k = form.GetKind(); - - switch (k) { - case FALSE: - case TRUE: - case SYMBOL: - case BVGETBIT: { - result = form; - break; - } - case XOR: { - // convertXORs can only be called once per XOR node. - result = convertXORs(new_children); - - // cout << "convertXORs num args: " << new_children.size() << endl; - // temporary node for node count. - // ASTNode tmp = bm->CreateNode(XOR, new_children ); - // cout << "convertXORs size of [" << form.GetNodeNum() << "] " << bm->NodeSize(form, true) << endl; - // cout << "convertXORs before size: " << bm->NodeSize(tmp, true) << endl; - // cout << "convertXORs after size: " << bm->NodeSize(result, true) << endl; - break; - } - default: { - // Be cautious about using CreateSimpForm -- It makes big xors! - result = bm->CreateNode(k, new_children); - } - } - -// cout << "================" << endl -// << "ToCNFPrePass:" << form << endl -// << "----------------" << endl -// << "ToCNFPrePass Result:" << result << endl; - - return (ToCNFPrePassMemo[form] = result); - - } - - // Memoize and return formula value - ASTNode CNFMemoize(ASTNode& form, ASTNode result) - { - CNFMemo[form] = result; - return result; - } - - - // Create a representative variable for an original formula. - // The convention is that the variable will have the same truth - // value as the expression numbered "num." - ASTNode RepLit(const char *name, int exprnum) - { - // FIXME: can this be done more efficiently with string type? - ostringstream oss; - oss << name << "{" << exprnum << "}"; - ASTNode t = bm->CreateSymbol(oss.str().c_str()); - - // Track how many we're generating. - stats._num_new_rep_vars++; - - //ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0)) - t.SetIndexWidth(0); - t.SetValueWidth(0); - return t; - } - - // Handle the cases where it's necessary to do n children. - // This code translates ANDs, and converts NAND, NOR, OR by negating - // the inputs or outputs of the AND. - ASTNode ToCNF_AndLike(Kind k, BeevMgr::ClauseList& cll, ASTNode form) - { - // Build vectors of positive and negative rep lits for children - ASTVec kidlits(0); - ASTVec negkidlits(0); - ASTVec::const_iterator kids_end = form.end(); - for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) { - ASTNode kidreplit = ToCNF_int(cll, *it); - kidlits.push_back(kidreplit); - negkidlits.push_back(bm->CreateSimpNot(kidreplit)); - } - - ASTNode replit; - // translate the AND, negating inputs as appropriate. - if (k == OR || k == NOR) { - replit = ToCNF_AND(cll, form.GetNodeNum(), negkidlits, kidlits); - } - else { - replit = ToCNF_AND(cll, form.GetNodeNum(), kidlits, negkidlits); - } - - // Reduce NAND/OR to AND by negating result. - if (k == NAND || k == OR) { - return CNFMemoize(form, bm->CreateSimpNot(replit)); - } - else { - return CNFMemoize(form, replit); - } - } - - ASTNode ToCNF_AND(BeevMgr::ClauseList& cll, int nodenum, ASTVec& kidlits, ASTVec& negkidlits) - { - // Translate an AND, given rep lits for children - // Build clauses for (replit <-> a AND b AND c) - - ASTNode replit = RepLit("cnf", nodenum); - ASTNode notreplit = bm->CreateSimpNot(replit); - - if (CNF_trace) { - cout << "Translating AND" << endl << "-----------------------" << endl - << "Rep lit =" << replit << endl - << "-----------------------"; - } - - // (a AND b AND c -> replit) == (~a OR ~b OR ~c OR replit) - BeevMgr::ClausePtr clp = new ASTVec(negkidlits); - clp->push_back(replit); - - if (CNF_trace) { - LispPrintVec(cout, *clp, 0); - cout << endl << "-----------------------" << endl; - } - - cll.push_back(clp); - - // (replit -> (a AND b AND c)) == - // (~replit OR a) AND (~replit OR b) AND (~replit OR c) - ASTVec::const_iterator kidlits_end = kidlits.end(); - for (ASTVec::iterator it = kidlits.begin(); it != kidlits_end; it++) { - clp = new ASTVec(); - clp->push_back(notreplit); - clp->push_back(*it); - - if (CNF_trace) { - LispPrintVec(cout, *clp, 0); - cout << endl << "-----------------------" << endl; - } - - cll.push_back(clp); - } - - return replit; - } - -public: - - /** Builds clauses globally and returns a literal. - The literal can be a leaf from the expression, or a rep var - made up to represent the subexpression. */ - ASTNode ToCNF_int(BeevMgr::BeevMgr::ClauseList& cll, ASTNode form) { - // FIXME: assert indexwidth= 0, valuewidth = 1 - - // FIXME: rewriting is top-down, which is not efficient. - // It rewrites the top node of the tree, then does the children. - // Either rewrite in a separate pass, or translate children - // before rewriting somehow (might require handling rep lits - // as though they were real lits, which is probably ok). - - // Return memoized value if seen before. - ASTNode result; - Kind k = form.GetKind(); - - if (CNFIsMemoized(form, result)) { - return result; - } - - switch (k) { - // handle the trivial cases here. If none apply, call the - // heavy-duty function. If a constant or literal, just return - // without creating a clause. - case FALSE: { - result = dummy_false_var; - break; - } - case TRUE: { - result = dummy_true_var; - break; - } - case SYMBOL: - case BVGETBIT: { - result = form; - break; - } - - case NOT: { - ASTNode replit = ToCNF_int(cll, form[0]); - result = bm->CreateSimpNot(replit); - break; - } - - // For these, I can't think of anything better than expanding into ANDs/ORs - case ITE: { - // (ite a b c) == (~a OR b) AND (a OR c) - ASTNode l = bm->CreateNode(OR, bm->CreateSimpNot(form[0]), form[1]); - ASTNode r = bm->CreateNode(OR, form[0], form[2]); - ASTNode andor = bm->CreateNode(AND, l, r); - if (CNF_trace) { - cout << "Rewriting " << form << endl - << "to" << andor << endl - << "-------------------" << endl; - } - result = ToCNF_int(cll, andor); - break; - } - case IMPLIES: { - // Just rewrite into (~a OR b) - ASTNode l = bm->CreateSimpNot(form[0]); - ASTNode andor = bm->CreateNode(OR, l, form[1]); - if (CNF_trace) { - cout << "Rewriting " << form << endl - << "to" << andor << endl - << "-------------------" << endl; - } - result = ToCNF_int(cll, andor); - break; - } - case XOR: { - FatalError("ToCNF_int: XORs should have been converted to AND/OR by this point."); - break; - } - - case IFF: { - FatalError("BitBlaster failed to eliminate all IFFs."); - break; - } - - case AND: - case OR: - case NOR: - case NAND: { - result = ToCNF_AndLike(k, cll, form); - break; - } - default: - cerr << "ToCNF: can't handle this kind: " << k << endl; - FatalError(""); - } - - if (CNF_trace) { - cout << "ToCNF_int: Literal " << result << " represents formula " << - form << endl << "---------------" << endl; - } - - return CNFMemoize(form, result); - } //end of ToCNF_int() - - -}; // end of CNFMgr class - - // These are the bodies of functions in the BeevMgr that are part of - // the public interface. - - // Debug printing function. - void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll) - { - int num_clauses = cll.size(); - os << "Clauses: " << endl << "=========================================" << endl; - for(int i=0; i < num_clauses; i++) { - os << "Clause " << i << endl - << "-------------------------------------------" << endl; - LispPrintVec(os, *cll[i], 0); - os << endl - << "-------------------------------------------" << endl; - } - } - - void BeevMgr::DeleteClauseList(BeevMgr::ClauseList *cllp) - { - BeevMgr::ClauseList::const_iterator iend = cllp->end(); - for (BeevMgr::ClauseList::const_iterator i = cllp->begin(); i < iend; i++) { - delete *i; - } - delete cllp; - } - - // Top level conversion function - BeevMgr::ClauseList *BeevMgr::ToCNF(const ASTNode& form) - { - - // FIXME: This is leaked as well. - CNFMgr *cm = new CNFMgr(this); - - // Prepass - ASTNode form1 = cm->ToCNFPrePass(form); - - // cout << "Number of nodes after ToCNFPrePass" << NodeSize(form1, true) << endl; - - // cout << "ToCNF: After ToCNFPrePass" << form1 << endl; - - // FIXME: Assert CNFMemo is empty. - - // The clause list we will be building up. - // FIXME: This is never freed. - ClauseList *cllp = new ClauseList(); - - BeevMgr::ClausePtr dummy_true_unit_clause = new ASTVec(); - dummy_true_unit_clause->push_back(cm->dummy_true_var); - cllp->push_back(dummy_true_unit_clause); - - // This is where the translation happens. - ASTNode toplit = cm->ToCNF_int(*cllp, form1); - - // Add the top literal as a unit clause, since it must - // be true when original formula is satsfied. - BeevMgr::ClausePtr clp = new ASTVec(0); - clp->push_back(toplit); - cllp->push_back(clp); - - cm->stats._num_clauses = cllp->size(); - cm->stats.printStats(); - - RepLitMap = cm->CNFMemo; // Save memo table for debugging (DD 1/13/07). - - cm->CNFMemo.clear(); // Important to do this so nodes get freed. - - delete cm; - - return cllp; - } - -} // end namespace |