00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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
00039 d_clauseIdNext(0),
00040
00041 d_bottomScope(-1),
00042 d_statistics(statistics),
00043 d_cnfCallback(NULL)
00044 {
00045 d_rules = createProofRules(tm);
00046
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
00074 if (e.isAtomic()) return d_commonRules->reflexivityRule(e);
00075
00076
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
00087 DebugAssert(!e.getType().isBool(), "Expected non-Bool ITE");
00088
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
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
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
00297
00298
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
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
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
00430 Expr e2 = d_vc->importExpr(e);
00431 vector<unsigned> newLits;
00432 DebugAssert(d_vc->scopeLevel() == 1, "expected scope level 1");
00433
00434
00435 cons(0, e.arity()-1, e2, newLits);
00436
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
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
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
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
00494 cnf.getCurrentClause().setId(d_clauseIdNext++);
00495 FatalAssert(d_clauseIdNext != 0, "Overflow of clause id's");
00496
00497 return l;
00498 }