cnf_manager.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file cnf_manager.cpp
00004  *\brief Implementation of CNF_Manager
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Jan  5 02:30:02 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #include "cnf_manager.h"
00023 #include "cnf_rules.h"
00024 #include "common_proof_rules.h"
00025 #include "theorem_manager.h"
00026 #include "vc.h"
00027 #include "command_line_flags.h"
00028 
00029 
00030 using namespace std;
00031 using namespace CVC3;
00032 using namespace SAT;
00033 
00034 
00035 CNF_Manager::CNF_Manager(TheoremManager* tm, Statistics& statistics, bool minimizeClauses)
00036   : d_vc(NULL), d_minimizeClauses(minimizeClauses),
00037     d_commonRules(tm->getRules()),
00038     //    d_theorems(tm->getCM()->getCurrentContext()),
00039     d_clauseIdNext(0),
00040     //    d_translated(tm->getCM()->getCurrentContext()),
00041     d_bottomScope(-1),
00042     d_statistics(statistics),
00043     d_cnfCallback(NULL)
00044 {
00045   d_rules = createProofRules(tm);
00046   // Push dummy varinfo onto d_varInfo since Var's are indexed from 1 not 0
00047   Varinfo v;
00048   d_varInfo.push_back(v);
00049   if (minimizeClauses) {
00050     CLFlags flags = ValidityChecker::createFlags();
00051     flags.setFlag("minimizeClauses",false);
00052     d_vc = ValidityChecker::create(flags);
00053   }
00054 }
00055 
00056 
00057 CNF_Manager::~CNF_Manager()
00058 {
00059   if (d_vc) delete d_vc;
00060   delete d_rules;
00061 }
00062 
00063 
00064 void CNF_Manager::registerAtom(const Expr& e, const Theorem& thm)
00065 {
00066   DebugAssert(!e.isRegisteredAtom() || e.isUserRegisteredAtom(), "Atom already registered");
00067   if (d_cnfCallback && !e.isRegisteredAtom()) d_cnfCallback->registerAtom(e, thm);
00068 }
00069 
00070 
00071 Theorem CNF_Manager::replaceITErec(const Expr& e, Var v, bool translateOnly)
00072 {
00073   // Quick exit for atomic expressions
00074   if (e.isAtomic()) return d_commonRules->reflexivityRule(e);
00075 
00076   // Check cache
00077   Theorem thm;
00078   bool foundInCache = false;
00079   ExprMap<Theorem>::iterator iMap = d_iteMap.find(e);
00080   if (iMap != d_iteMap.end()) {
00081     thm = (*iMap).second;
00082     foundInCache = true;
00083   }
00084 
00085   if (e.getKind() == ITE) {
00086     // Replace non-Bool ITE expressions
00087     DebugAssert(!e.getType().isBool(), "Expected non-Bool ITE");
00088     // generate e = x for new x
00089     if (!foundInCache) thm = d_commonRules->varIntroSkolem(e);
00090     Theorem thm2 = d_commonRules->symmetryRule(thm);
00091     thm2 = d_commonRules->iffMP(thm2, d_rules->ifLiftRule(thm2.getExpr(), 1));
00092     d_translateQueueVars.push_back(v);
00093     d_translateQueueThms.push_back(thm2);
00094     d_translateQueueFlags.push_back(translateOnly);
00095   }
00096   else {
00097     // Recursively traverse, replacing ITE's
00098     vector<Theorem> thms;
00099     vector<unsigned> changed;
00100     unsigned index = 0;
00101     Expr::iterator i, iend;
00102     if (foundInCache) {
00103       for(i = e.begin(), iend = e.end(); i!=iend; ++i, ++index) {
00104         replaceITErec(*i, v, translateOnly);
00105       }
00106     }
00107     else {
00108       for(i = e.begin(), iend = e.end(); i!=iend; ++i, ++index) {
00109         thm = replaceITErec(*i, v, translateOnly);
00110         if(thm.getLHS() != thm.getRHS()) {
00111           thms.push_back(thm);
00112           changed.push_back(index);
00113         }
00114       }
00115       if(changed.size() > 0) {
00116         thm = d_commonRules->substitutivityRule(e, changed, thms);
00117       }
00118       else thm = d_commonRules->reflexivityRule(e);
00119     }
00120   }
00121 
00122   // Update cache and return
00123   if (!foundInCache) d_iteMap[e] = thm;
00124   return thm;
00125 }
00126 
00127 
00128 Lit CNF_Manager::translateExprRec(const Expr& e, CNF_Formula& cnf, const Theorem& thmIn)
00129 {
00130   if (e.isFalse()) return Lit::getFalse();
00131   if (e.isTrue()) return Lit::getTrue();
00132   if (e.isNot()) return !translateExprRec(e[0], cnf, thmIn);
00133 
00134   ExprMap<Var>::iterator iMap = d_cnfVars.find(e);
00135 
00136   if (e.isTranslated()) {
00137     DebugAssert(iMap != d_cnfVars.end(), "Translated expr should be in map");
00138     return Lit((*iMap).second);
00139   }
00140   else e.setTranslated(d_bottomScope);
00141 
00142   Var v(int(d_varInfo.size()));
00143   bool translateOnly = false;
00144 
00145   if (iMap != d_cnfVars.end()) {
00146     v = (*iMap).second;
00147     translateOnly = true;
00148     d_varInfo[v].fanouts.clear();
00149   }
00150   else {
00151     d_varInfo.resize(v+1);
00152     d_varInfo.back().expr = e;
00153     d_cnfVars[e] = v;
00154   }
00155 
00156   Expr::iterator i, iend;
00157 
00158   bool isAnd = false;
00159   switch (e.getKind()) {
00160     case AND:
00161       isAnd = true;
00162     case OR: {
00163       vector<Lit> lits;
00164       unsigned idx;
00165       for (i = e.begin(), iend = e.end(); i != iend; ++i) {
00166         lits.push_back(translateExprRec(*i, cnf, thmIn));
00167       }
00168       for (idx = 0; idx < lits.size(); ++idx) {
00169         cnf.newClause();
00170         cnf.addLiteral(Lit(v),isAnd);
00171         cnf.addLiteral(lits[idx], !isAnd);
00172       }
00173       cnf.newClause();
00174       cnf.addLiteral(Lit(v),!isAnd);
00175       for (idx = 0; idx < lits.size(); ++idx) {
00176         cnf.addLiteral(lits[idx], isAnd);
00177       }
00178       break;
00179     }
00180     case IMPLIES: {
00181       Lit arg0 = translateExprRec(e[0], cnf, thmIn);
00182       Lit arg1 = translateExprRec(e[1], cnf, thmIn);
00183 
00184       cnf.newClause();
00185       cnf.addLiteral(Lit(v));
00186       cnf.addLiteral(arg0);
00187 
00188       cnf.newClause();
00189       cnf.addLiteral(Lit(v));
00190       cnf.addLiteral(arg1,true);
00191 
00192       cnf.newClause();
00193       cnf.addLiteral(Lit(v),true);
00194       cnf.addLiteral(arg0,true);
00195       cnf.addLiteral(arg1);
00196       break;
00197     }
00198     case IFF: {
00199       Lit arg0 = translateExprRec(e[0], cnf, thmIn);
00200       Lit arg1 = translateExprRec(e[1], cnf, thmIn);
00201 
00202       cnf.newClause();
00203       cnf.addLiteral(Lit(v));
00204       cnf.addLiteral(arg0);
00205       cnf.addLiteral(arg1);
00206 
00207       cnf.newClause();
00208       cnf.addLiteral(Lit(v));
00209       cnf.addLiteral(arg0,true);
00210       cnf.addLiteral(arg1,true);
00211 
00212       cnf.newClause();
00213       cnf.addLiteral(Lit(v),true);
00214       cnf.addLiteral(arg0,true);
00215       cnf.addLiteral(arg1);
00216 
00217       cnf.newClause();
00218       cnf.addLiteral(Lit(v),true);
00219       cnf.addLiteral(arg0);
00220       cnf.addLiteral(arg1,true);
00221       break;
00222     }
00223     case XOR: {
00224       Lit arg0 = translateExprRec(e[0], cnf, thmIn);
00225       Lit arg1 = translateExprRec(e[1], cnf, thmIn);
00226 
00227       cnf.newClause();
00228       cnf.addLiteral(Lit(v),true);
00229       cnf.addLiteral(arg0);
00230       cnf.addLiteral(arg1);
00231 
00232       cnf.newClause();
00233       cnf.addLiteral(Lit(v),true);
00234       cnf.addLiteral(arg0,true);
00235       cnf.addLiteral(arg1,true);
00236 
00237       cnf.newClause();
00238       cnf.addLiteral(Lit(v));
00239       cnf.addLiteral(arg0,true);
00240       cnf.addLiteral(arg1);
00241 
00242       cnf.newClause();
00243       cnf.addLiteral(Lit(v));
00244       cnf.addLiteral(arg0);
00245       cnf.addLiteral(arg1,true);
00246       break;
00247     }
00248     case ITE:
00249     {
00250       Lit arg0 = translateExprRec(e[0], cnf, thmIn);
00251       Lit arg1 = translateExprRec(e[1], cnf, thmIn);
00252       Lit arg2 = translateExprRec(e[2], cnf, thmIn);
00253 
00254       cnf.newClause();
00255       cnf.addLiteral(Lit(v),true);
00256       cnf.addLiteral(arg0);
00257       cnf.addLiteral(arg2);
00258 
00259       cnf.newClause();
00260       cnf.addLiteral(Lit(v));
00261       cnf.addLiteral(arg0);
00262       cnf.addLiteral(arg2,true);
00263 
00264       cnf.newClause();
00265       cnf.addLiteral(Lit(v));
00266       cnf.addLiteral(arg0,true);
00267       cnf.addLiteral(arg1,true);
00268 
00269       cnf.newClause();
00270       cnf.addLiteral(Lit(v),true);
00271       cnf.addLiteral(arg0,true);
00272       cnf.addLiteral(arg1);
00273 
00274       cnf.newClause();
00275       cnf.addLiteral(Lit(v));
00276       cnf.addLiteral(arg1,true);
00277       cnf.addLiteral(arg2,true);
00278 
00279       cnf.newClause();
00280       cnf.addLiteral(Lit(v),true);
00281       cnf.addLiteral(arg1);
00282       cnf.addLiteral(arg2);
00283       break;
00284     }
00285     default:
00286       DebugAssert(!e.isAbsAtomicFormula() || d_varInfo[v].expr == e,
00287                   "Corrupted Varinfo");
00288       if (e.isAbsAtomicFormula()) {
00289         registerAtom(e, thmIn);
00290         return Lit(v);
00291       }
00292       Theorem thm = replaceITErec(e, v, translateOnly);
00293       const Expr& e2 = thm.getRHS();
00294       DebugAssert(e2.isAbsAtomicFormula(), "Expected AbsAtomicFormula");
00295       if (e2.isTranslated()) {
00296         // Ugly corner case: we happen to create an expression that has been
00297         // created before.  We remove the current variable and fix up the
00298         // translation stack.
00299         if (translateOnly) {
00300           DebugAssert(v == d_cnfVars[e2], "Expected literal match");
00301         }
00302         else {
00303           d_varInfo.resize(v);
00304           while (!d_translateQueueVars.empty() &&
00305                  d_translateQueueVars.back() == v) {
00306             d_translateQueueVars.pop_back();
00307           }
00308           DebugAssert(d_cnfVars.find(e2) != d_cnfVars.end(),
00309                       "Expected existing literal");
00310           v = d_cnfVars[e2];
00311           d_cnfVars[e] = v;
00312           while (d_translateQueueVars.size() < d_translateQueueThms.size()) {
00313             d_translateQueueVars.push_back(v);
00314           }
00315         }
00316       }
00317       else {
00318         e2.setTranslated(d_bottomScope);
00319         registerAtom(e2, thmIn);
00320         if (!translateOnly) {
00321           DebugAssert(d_cnfVars.find(e2) == d_cnfVars.end(),
00322                       "Expected new literal");
00323           d_varInfo[v].expr = e2;
00324           d_cnfVars[e2] = v;
00325         }
00326       }
00327       return Lit(v);
00328   }
00329 
00330   // Record fanins / fanouts
00331   Lit l;
00332   for (i = e.begin(), iend = e.end(); i != iend; ++i) {
00333     l = getCNFLit(*i);
00334     DebugAssert(!l.isNull(), "Expected non-null literal");
00335     if (!translateOnly) d_varInfo[v].fanins.push_back(l);
00336     if (l.isVar()) d_varInfo[l.getVar()].fanouts.push_back(v);
00337   }
00338   return Lit(v);
00339 }
00340 
00341 Lit CNF_Manager::translateExpr(const Theorem& thmIn, CNF_Formula& cnf)
00342 {
00343   Lit l;
00344   Var v;
00345   Expr e = thmIn.getExpr();
00346   Theorem thm;
00347   bool translateOnly;
00348 
00349   Lit ret = translateExprRec(e, cnf, thmIn);
00350 
00351   while (d_translateQueueVars.size()) {
00352     v = d_translateQueueVars.front();
00353     d_translateQueueVars.pop_front();
00354     thm = d_translateQueueThms.front();
00355     d_translateQueueThms.pop_front();
00356     translateOnly = d_translateQueueFlags.front();
00357     d_translateQueueFlags.pop_front();
00358     l = translateExprRec(thm.getExpr(), cnf, thmIn);
00359     cnf.newClause();
00360     cnf.addLiteral(l);
00361     cnf.registerUnit();
00362     //    d_theorems.insert(d_clauseIdNext, thm);
00363     cnf.getCurrentClause().setId(d_clauseIdNext++);
00364     FatalAssert(d_clauseIdNext != 0, "Overflow of clause id's");
00365     if (!translateOnly) d_varInfo[v].fanins.push_back(l);
00366     d_varInfo[l.getVar()].fanouts.push_back(v);
00367   }
00368   return ret;
00369 }
00370 
00371 
00372 void CNF_Manager::cons(unsigned lb, unsigned ub, const Expr& e2, vector<unsigned>& newLits)
00373 {
00374   if (lb == ub) {
00375     newLits.push_back(lb);
00376     return;
00377   }
00378   unsigned new_lb = (ub-lb+1)/2 + lb;
00379   unsigned index;
00380   QueryResult res;
00381   d_vc->push();
00382   for (index = new_lb; index <= ub; ++index) {
00383     d_vc->assertFormula(e2[index].negate());
00384   }
00385   res = d_vc->query(d_vc->falseExpr());
00386   d_vc->pop();
00387   if (res == VALID) {
00388     cons(new_lb, ub, e2, newLits);
00389     return;
00390   }
00391 
00392   unsigned new_ub = new_lb-1;
00393   d_vc->push();
00394   for (index = lb; index <= new_ub; ++index) {
00395     d_vc->assertFormula(e2[index].negate());
00396   }
00397   res = d_vc->query(d_vc->falseExpr());
00398   if (res == VALID) {
00399     d_vc->pop();
00400     cons(lb, new_ub, e2, newLits);
00401     return;
00402   }
00403 
00404   cons(new_lb, ub, e2, newLits);
00405   d_vc->pop();
00406   d_vc->push();
00407   for (index = 0; index < newLits.size(); ++index) {
00408     d_vc->assertFormula(e2[newLits[index]].negate());
00409   }
00410   cons(lb, new_ub, e2, newLits);
00411   d_vc->pop();
00412 }
00413 
00414 
00415 void CNF_Manager::convertLemma(const Theorem& thm, Clause& c)
00416 {
00417   DebugAssert(c.size() == 0, "Expected empty clause");
00418   Theorem clause = d_rules->learnedClause(thm);
00419 
00420   Expr e = clause.getExpr();
00421   if (!e.isOr()) {
00422     DebugAssert(!getCNFLit(e).isNull(), "Unknown literal");
00423     c.addLiteral(getCNFLit(e));
00424   }
00425   else {
00426 
00427     if (e.arity() > 3 && d_minimizeClauses) {
00428 
00429       // Clause minimization
00430       Expr e2 = d_vc->importExpr(e);
00431       vector<unsigned> newLits;
00432       DebugAssert(d_vc->scopeLevel() == 1, "expected scope level 1");
00433       //      d_vc->push();
00434       //      d_vc->assertFormula(e2[e.arity()-1].negate());
00435       cons(0, e.arity()-1, e2, newLits);
00436       //      d_vc->pop();
00437       DebugAssert(d_vc->scopeLevel() == 1, "expected scope level 1");
00438       d_statistics.counter("clauses processed")++;
00439       if (newLits.size() < (unsigned)e.arity()) {
00440         d_statistics.counter("clauses minimized")++;
00441         vector<Expr> newKids;
00442         for (unsigned index = 0; index < newLits.size(); ++index) {
00443           newKids.push_back(e[newLits[index]]);
00444         }
00445         //        newKids.push_back(e[e.arity()-1]);
00446         e = Expr(OR, newKids);
00447         IF_DEBUG(
00448                  d_vc->push();
00449                  DebugAssert(d_vc->query(d_vc->importExpr(e)) == VALID, "expected valid");
00450                  d_vc->pop();
00451                  )
00452       }
00453     }
00454 
00455     Expr::iterator iend = e.end();
00456     for (Expr::iterator i = e.begin(); i != iend; ++i) {
00457       DebugAssert(!getCNFLit(*i).isNull(), "Unknown literal");
00458       c.addLiteral(getCNFLit(*i));
00459     }
00460   }
00461   if (c.size() == 1) c.setUnit();
00462 
00463   //  d_theorems.insert(d_clauseIdNext, clause);
00464   c.setId(d_clauseIdNext++);
00465   FatalAssert(d_clauseIdNext != 0, "Overflow of clause id's");
00466 }
00467 
00468 
00469 Lit CNF_Manager::addAssumption(const Theorem& thm, CNF_Formula& cnf)
00470 {
00471   Lit l = translateExpr(thm, cnf);
00472   cnf.newClause();
00473   cnf.addLiteral(l);
00474   cnf.registerUnit();
00475 
00476   //  d_theorems[d_clauseIdNext] = thm;
00477   cnf.getCurrentClause().setId(d_clauseIdNext++);
00478   FatalAssert(d_clauseIdNext != 0, "Overflow of clause id's");
00479 
00480   return l;
00481 }
00482 
00483 
00484 Lit CNF_Manager::addLemma(const Theorem& thm, CNF_Formula& cnf)
00485 {
00486   Theorem clause = d_rules->learnedClause(thm);
00487 
00488   Lit l = translateExpr(clause, cnf);
00489   cnf.newClause();
00490   cnf.addLiteral(l);
00491   cnf.registerUnit();
00492 
00493   //  d_theorems.insert(d_clauseIdNext, clause);
00494   cnf.getCurrentClause().setId(d_clauseIdNext++);
00495   FatalAssert(d_clauseIdNext != 0, "Overflow of clause id's");
00496 
00497   return l;
00498 }

Generated on Tue Jul 3 14:33:35 2007 for CVC3 by  doxygen 1.5.1