CVC3 2.2
|
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, 00036 const CLFlags& flags) 00037 : d_vc(NULL), 00038 d_commonRules(tm->getRules()), 00039 // d_theorems(tm->getCM()->getCurrentContext()), 00040 d_clauseIdNext(0), 00041 // d_translated(tm->getCM()->getCurrentContext()), 00042 d_bottomScope(-1), 00043 d_statistics(statistics), 00044 d_flags(flags), 00045 d_nullExpr(tm->getEM()->getNullExpr()), 00046 d_cnfCallback(NULL) 00047 { 00048 d_rules = createProofRules(tm, flags); 00049 // Push dummy varinfo onto d_varInfo since Var's are indexed from 1 not 0 00050 Varinfo v; 00051 d_varInfo.push_back(v); 00052 if (flags["minimizeClauses"].getBool()) { 00053 CLFlags flags = ValidityChecker::createFlags(); 00054 flags.setFlag("minimizeClauses",false); 00055 d_vc = ValidityChecker::create(flags); 00056 } 00057 } 00058 00059 00060 CNF_Manager::~CNF_Manager() 00061 { 00062 if (d_vc) delete d_vc; 00063 delete d_rules; 00064 } 00065 00066 00067 void CNF_Manager::registerAtom(const Expr& e, const Theorem& thm) 00068 { 00069 DebugAssert(!e.isRegisteredAtom() || e.isUserRegisteredAtom(), "Atom already registered"); 00070 if (d_cnfCallback && !e.isRegisteredAtom()) d_cnfCallback->registerAtom(e, thm); 00071 } 00072 00073 00074 Theorem CNF_Manager::replaceITErec(const Expr& e, Var v, bool translateOnly) 00075 { 00076 // Quick exit for atomic expressions 00077 if (e.isAtomic()) return d_commonRules->reflexivityRule(e); 00078 00079 // Check cache 00080 Theorem thm; 00081 bool foundInCache = false; 00082 ExprHashMap<Theorem>::iterator iMap = d_iteMap.find(e); 00083 if (iMap != d_iteMap.end()) { 00084 thm = (*iMap).second; 00085 foundInCache = true; 00086 } 00087 00088 if (e.getKind() == ITE) { 00089 // Replace non-Bool ITE expressions 00090 DebugAssert(!e.getType().isBool(), "Expected non-Bool ITE"); 00091 // generate e = x for new x 00092 if (!foundInCache) thm = d_commonRules->varIntroSkolem(e); 00093 Theorem thm2 = d_commonRules->symmetryRule(thm); 00094 thm2 = d_commonRules->iffMP(thm2, d_rules->ifLiftRule(thm2.getExpr(), 1)); 00095 d_translateQueueVars.push_back(v); 00096 d_translateQueueThms.push_back(thm2); 00097 d_translateQueueFlags.push_back(translateOnly); 00098 } 00099 else { 00100 // Recursively traverse, replacing ITE's 00101 vector<Theorem> thms; 00102 vector<unsigned> changed; 00103 unsigned index = 0; 00104 Expr::iterator i, iend; 00105 if (foundInCache) { 00106 for(i = e.begin(), iend = e.end(); i!=iend; ++i, ++index) { 00107 replaceITErec(*i, v, translateOnly); 00108 } 00109 } 00110 else { 00111 for(i = e.begin(), iend = e.end(); i!=iend; ++i, ++index) { 00112 thm = replaceITErec(*i, v, translateOnly); 00113 if (!thm.isRefl()) { 00114 thms.push_back(thm); 00115 changed.push_back(index); 00116 } 00117 } 00118 if(changed.size() > 0) { 00119 thm = d_commonRules->substitutivityRule(e, changed, thms); 00120 } 00121 else thm = d_commonRules->reflexivityRule(e); 00122 } 00123 } 00124 00125 // Update cache and return 00126 if (!foundInCache) d_iteMap[e] = thm; 00127 return thm; 00128 } 00129 00130 00131 Expr CNF_Manager::concreteExpr(const CVC3::Expr& e, const Lit& literal){ 00132 if ( e.isTrue() || e.isFalse() || 00133 (e.isNot() && (e[0].isTrue() || e[0].isFalse()))) 00134 return e; 00135 else 00136 return concreteLit(literal); 00137 } 00138 00139 00140 Lit CNF_Manager::translateExprRec(const Expr& e, CNF_Formula& cnf, const Theorem& thmIn) 00141 { 00142 if (e.isFalse()) return Lit::getFalse(); 00143 if (e.isTrue()) return Lit::getTrue(); 00144 if (e.isNot()) return !translateExprRec(e[0], cnf, thmIn); 00145 00146 ExprHashMap<Var>::iterator iMap = d_cnfVars.find(e); 00147 00148 if (e.isTranslated()) { 00149 DebugAssert(iMap != d_cnfVars.end(), "Translated expr should be in map"); 00150 return Lit((*iMap).second); 00151 } 00152 else e.setTranslated(d_bottomScope); 00153 00154 Var v(int(d_varInfo.size())); 00155 bool translateOnly = false; 00156 00157 if (iMap != d_cnfVars.end()) { 00158 v = (*iMap).second; 00159 translateOnly = true; 00160 d_varInfo[v].fanouts.clear(); 00161 } 00162 else { 00163 d_varInfo.resize(v+1); 00164 d_varInfo.back().expr = e; 00165 d_cnfVars[e] = v; 00166 } 00167 00168 Expr::iterator i, iend; 00169 bool isAnd = false; 00170 switch (e.getKind()) { 00171 case AND: 00172 isAnd = true; 00173 case OR: { 00174 00175 vector<Lit> lits; 00176 unsigned idx; 00177 for (i = e.begin(), iend = e.end(); i != iend; ++i) { 00178 lits.push_back(translateExprRec(*i, cnf, thmIn)); 00179 } 00180 00181 // DebugAssert(concreteExpr(e,Lit(v)) == e,"why here"); 00182 00183 for (idx = 0; idx < lits.size(); ++idx) { 00184 cnf.newClause(); 00185 cnf.addLiteral(Lit(v),isAnd); 00186 cnf.addLiteral(lits[idx], !isAnd); 00187 00188 // DebugAssert(concreteExpr(e[idx],lits[idx]) == e[idx], "why here"); 00189 00190 std::string reasonStr = (isAnd ? "and_mid" : "or_mid"); 00191 Expr after = e[idx] ; 00192 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, reasonStr, idx)); // by yeting 00193 } 00194 00195 cnf.newClause(); 00196 cnf.addLiteral(Lit(v),!isAnd); 00197 for (idx = 0; idx < lits.size(); ++idx) { 00198 cnf.addLiteral(lits[idx], isAnd); 00199 } 00200 00201 std::string reasonStr = (isAnd ? "and_final" : "or_final") ; 00202 Expr after = e ; 00203 00204 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, reasonStr, 0)); // by yeting 00205 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled"); 00206 break; 00207 } 00208 case IMPLIES: { 00209 Lit arg0 = translateExprRec(e[0], cnf, thmIn); 00210 Lit arg1 = translateExprRec(e[1], cnf, thmIn); 00211 00212 // DebugAssert(concreteExpr(e, Lit(v)) == e, "why here"); 00213 // DebugAssert(concreteExpr(e[0], arg0) == e[0], "why here"); 00214 // DebugAssert(concreteExpr(e[1], arg1) == e[1], "why here"); 00215 00216 cnf.newClause(); 00217 cnf.addLiteral(Lit(v)); 00218 cnf.addLiteral(arg0); 00219 00220 cnf.getCurrentClause().setClauseTheorem( d_rules->CNFtranslate(e, e, "imp", 0)); // by yeting 00221 00222 cnf.newClause(); 00223 cnf.addLiteral(Lit(v)); 00224 cnf.addLiteral(arg1,true); 00225 00226 cnf.getCurrentClause().setClauseTheorem( d_rules->CNFtranslate(e, e, "imp", 1)); // by yeting 00227 00228 cnf.newClause(); 00229 cnf.addLiteral(Lit(v),true); 00230 cnf.addLiteral(arg0,true); 00231 cnf.addLiteral(arg1); 00232 00233 cnf.getCurrentClause().setClauseTheorem( d_rules->CNFtranslate(e, e, "imp", 2)); // by yeting 00234 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled"); 00235 break; 00236 } 00237 case IFF: { 00238 Lit arg0 = translateExprRec(e[0], cnf, thmIn); 00239 Lit arg1 = translateExprRec(e[1], cnf, thmIn); 00240 00241 // DebugAssert(concreteExpr(e, Lit(v)) == e, "why here"); 00242 // DebugAssert(concreteExpr(e[0], arg0) == e[0], "why here"); 00243 // DebugAssert(concreteExpr(e[1], arg1) == e[1], "why here"); 00244 00245 cnf.newClause(); 00246 cnf.addLiteral(Lit(v)); 00247 cnf.addLiteral(arg0); 00248 cnf.addLiteral(arg1); 00249 00250 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "iff", 0)); // by yeting 00251 00252 cnf.newClause(); 00253 cnf.addLiteral(Lit(v)); 00254 cnf.addLiteral(arg0,true); 00255 cnf.addLiteral(arg1,true); 00256 00257 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "iff", 1)); // by yeting 00258 00259 cnf.newClause(); 00260 cnf.addLiteral(Lit(v),true); 00261 cnf.addLiteral(arg0,true); 00262 cnf.addLiteral(arg1); 00263 00264 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "iff", 2)); // by yeting 00265 00266 cnf.newClause(); 00267 cnf.addLiteral(Lit(v),true); 00268 cnf.addLiteral(arg0); 00269 cnf.addLiteral(arg1,true); 00270 00271 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "iff", 3)); // by yeting 00272 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled"); 00273 break; 00274 } 00275 case XOR: { 00276 00277 Lit arg0 = translateExprRec(e[0], cnf, thmIn); 00278 Lit arg1 = translateExprRec(e[1], cnf, thmIn); 00279 00280 // DebugAssert(concreteExpr(e, Lit(v)) == e, "why here"); 00281 // DebugAssert(concreteExpr(e[0], arg0) == e[0], "why here"); 00282 // DebugAssert(concreteExpr(e[1], arg1) == e[1], "why here"); 00283 00284 00285 cnf.newClause(); 00286 cnf.addLiteral(Lit(v),true); 00287 cnf.addLiteral(arg0); 00288 cnf.addLiteral(arg1); 00289 00290 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "xor", 0)); // by yeting 00291 00292 cnf.newClause(); 00293 cnf.addLiteral(Lit(v),true); 00294 cnf.addLiteral(arg0,true); 00295 cnf.addLiteral(arg1,true); 00296 00297 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "xor", 1)); // by yeting 00298 00299 cnf.newClause(); 00300 cnf.addLiteral(Lit(v)); 00301 cnf.addLiteral(arg0,true); 00302 cnf.addLiteral(arg1); 00303 00304 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "xor", 2)); // by yeting 00305 00306 cnf.newClause(); 00307 cnf.addLiteral(Lit(v)); 00308 cnf.addLiteral(arg0); 00309 cnf.addLiteral(arg1,true); 00310 00311 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, e, "xor", 3)); // by yeting 00312 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled"); 00313 break; 00314 } 00315 case ITE: 00316 { 00317 00318 Lit arg0 = translateExprRec(e[0], cnf, thmIn); 00319 Lit arg1 = translateExprRec(e[1], cnf, thmIn); 00320 Lit arg2 = translateExprRec(e[2], cnf, thmIn); 00321 00322 00323 Expr aftere0 = concreteExpr(e[0], arg0); 00324 Expr aftere1 = concreteExpr(e[1], arg1); 00325 Expr aftere2 = concreteExpr(e[2], arg2); 00326 00327 vector<Expr> after ; 00328 after.push_back(aftere0); 00329 after.push_back(aftere1); 00330 after.push_back(aftere2); 00331 00332 Theorem e0thm; 00333 Theorem e1thm; 00334 Theorem e2thm; 00335 00336 { e0thm = d_iteMap[e[0]]; 00337 if (e0thm.isNull()) e0thm = d_commonRules->reflexivityRule(e[0]); 00338 e1thm = d_iteMap[e[1]]; 00339 if (e1thm.isNull()) e1thm = d_commonRules->reflexivityRule(e[1]); 00340 e2thm = d_iteMap[e[2]]; 00341 if (e2thm.isNull()) e2thm = d_commonRules->reflexivityRule(e[2]); 00342 } 00343 00344 vector<Theorem> thms ; 00345 thms.push_back(e0thm); 00346 thms.push_back(e1thm); 00347 thms.push_back(e2thm); 00348 00349 00350 00351 cnf.newClause(); 00352 cnf.addLiteral(Lit(v),true); 00353 cnf.addLiteral(arg0); 00354 cnf.addLiteral(arg2); 00355 00356 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 1)); // by yeting 00357 00358 cnf.newClause(); 00359 cnf.addLiteral(Lit(v)); 00360 cnf.addLiteral(arg0); 00361 cnf.addLiteral(arg2,true); 00362 00363 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 2)); // by yeting 00364 00365 cnf.newClause(); 00366 cnf.addLiteral(Lit(v)); 00367 cnf.addLiteral(arg0,true); 00368 cnf.addLiteral(arg1,true); 00369 00370 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 3)); // by yeting 00371 00372 cnf.newClause(); 00373 cnf.addLiteral(Lit(v),true); 00374 cnf.addLiteral(arg0,true); 00375 cnf.addLiteral(arg1); 00376 00377 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 4)); // by yeting 00378 00379 cnf.newClause(); 00380 cnf.addLiteral(Lit(v)); 00381 cnf.addLiteral(arg1,true); 00382 cnf.addLiteral(arg2,true); 00383 00384 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 5)); // by yeting 00385 00386 cnf.newClause(); 00387 cnf.addLiteral(Lit(v),true); 00388 cnf.addLiteral(arg1); 00389 cnf.addLiteral(arg2); 00390 00391 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 6)); // by yeting 00392 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled"); 00393 break; 00394 } 00395 default: 00396 { 00397 DebugAssert(!e.isAbsAtomicFormula() || d_varInfo[v].expr == e, 00398 "Corrupted Varinfo"); 00399 if (e.isAbsAtomicFormula()) { 00400 registerAtom(e, thmIn); 00401 return Lit(v); 00402 } 00403 00404 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled"); 00405 00406 Theorem thm = replaceITErec(e, v, translateOnly); 00407 const Expr& e2 = thm.getRHS(); 00408 DebugAssert(e2.isAbsAtomicFormula(), "Expected AbsAtomicFormula"); 00409 if (e2.isTranslated()) { 00410 // Ugly corner case: we happen to create an expression that has been 00411 // created before. We remove the current variable and fix up the 00412 // translation stack. 00413 if (translateOnly) { 00414 DebugAssert(v == d_cnfVars[e2], "Expected literal match"); 00415 } 00416 else { 00417 d_varInfo.resize(v); 00418 while (!d_translateQueueVars.empty() && 00419 d_translateQueueVars.back() == v) { 00420 d_translateQueueVars.pop_back(); 00421 } 00422 DebugAssert(d_cnfVars.find(e2) != d_cnfVars.end(), 00423 "Expected existing literal"); 00424 v = d_cnfVars[e2]; 00425 d_cnfVars[e] = v; 00426 while (d_translateQueueVars.size() < d_translateQueueThms.size()) { 00427 d_translateQueueVars.push_back(v); 00428 } 00429 } 00430 } 00431 else { 00432 e2.setTranslated(d_bottomScope); 00433 // Corner case: don't register reflexive equality 00434 if (!e2.isEq() || e2[0] != e2[1]) registerAtom(e2, thmIn); 00435 if (!translateOnly) { 00436 if (d_cnfVars.find(e2) == d_cnfVars.end()) { 00437 d_varInfo[v].expr = e2; 00438 d_cnfVars[e2] = v; 00439 } 00440 else { 00441 // Same corner case in an untranslated expr 00442 d_varInfo.resize(v); 00443 while (!d_translateQueueVars.empty() && 00444 d_translateQueueVars.back() == v) { 00445 d_translateQueueVars.pop_back(); 00446 } 00447 v = d_cnfVars[e2]; 00448 d_cnfVars[e] = v; 00449 while (d_translateQueueVars.size() < d_translateQueueThms.size()) { 00450 d_translateQueueVars.push_back(v); 00451 } 00452 } 00453 } 00454 } 00455 return Lit(v); 00456 } 00457 } 00458 00459 // Record fanins / fanouts 00460 Lit l; 00461 for (i = e.begin(), iend = e.end(); i != iend; ++i) { 00462 l = getCNFLit(*i); 00463 DebugAssert(!l.isNull(), "Expected non-null literal"); 00464 if (!translateOnly) d_varInfo[v].fanins.push_back(l); 00465 if (l.isVar()) d_varInfo[l.getVar()].fanouts.push_back(v); 00466 } 00467 return Lit(v); 00468 } 00469 00470 Lit CNF_Manager::translateExpr(const Theorem& thmIn, CNF_Formula& cnf) 00471 { 00472 Lit l; 00473 Var v; 00474 Expr e = thmIn.getExpr(); 00475 Theorem thm; 00476 bool translateOnly; 00477 00478 Lit ret = translateExprRec(e, cnf, thmIn); 00479 00480 while (d_translateQueueVars.size()) { 00481 v = d_translateQueueVars.front(); 00482 d_translateQueueVars.pop_front(); 00483 thm = d_translateQueueThms.front(); 00484 d_translateQueueThms.pop_front(); 00485 translateOnly = d_translateQueueFlags.front(); 00486 d_translateQueueFlags.pop_front(); 00487 l = translateExprRec(thm.getExpr(), cnf, thmIn); 00488 cnf.newClause(); 00489 cnf.addLiteral(l); 00490 cnf.registerUnit(); 00491 00492 Theorem newThm = d_rules->CNFAddUnit(thm); 00493 // d_theorems.insert(d_clauseIdNext, thm); 00494 // cnf.getCurrentClause().setClauseTheorem(thmIn); // by yeting 00495 cnf.getCurrentClause().setClauseTheorem(newThm); // by yeting 00496 00497 /* 00498 cout<<"set clause theorem 1" << thm << endl; 00499 cout<<"set clause theorem 2 " << thmIn << endl; 00500 cout<<"set clause print" ; cnf.getCurrentClause().print() ; cout<<endl; 00501 cout<<"set clause id " << d_clauseIdNext << endl; 00502 */ 00503 if (!translateOnly) d_varInfo[v].fanins.push_back(l); 00504 d_varInfo[l.getVar()].fanouts.push_back(v); 00505 } 00506 return ret; 00507 } 00508 00509 00510 void CNF_Manager::cons(unsigned lb, unsigned ub, const Expr& e2, vector<unsigned>& newLits) 00511 { 00512 if (lb == ub) { 00513 newLits.push_back(lb); 00514 return; 00515 } 00516 unsigned new_lb = (ub-lb+1)/2 + lb; 00517 unsigned index; 00518 QueryResult res; 00519 d_vc->push(); 00520 for (index = new_lb; index <= ub; ++index) { 00521 d_vc->assertFormula(e2[index].negate()); 00522 } 00523 res = d_vc->query(d_vc->falseExpr()); 00524 d_vc->pop(); 00525 if (res == VALID) { 00526 cons(new_lb, ub, e2, newLits); 00527 return; 00528 } 00529 00530 unsigned new_ub = new_lb-1; 00531 d_vc->push(); 00532 for (index = lb; index <= new_ub; ++index) { 00533 d_vc->assertFormula(e2[index].negate()); 00534 } 00535 res = d_vc->query(d_vc->falseExpr()); 00536 if (res == VALID) { 00537 d_vc->pop(); 00538 cons(lb, new_ub, e2, newLits); 00539 return; 00540 } 00541 00542 cons(new_lb, ub, e2, newLits); 00543 d_vc->pop(); 00544 d_vc->push(); 00545 for (index = 0; index < newLits.size(); ++index) { 00546 d_vc->assertFormula(e2[newLits[index]].negate()); 00547 } 00548 cons(lb, new_ub, e2, newLits); 00549 d_vc->pop(); 00550 } 00551 00552 00553 void CNF_Manager::convertLemma(const Theorem& thm, CNF_Formula& cnf) 00554 { 00555 DebugAssert(cnf.empty(), "Expected empty cnf"); 00556 vector<Theorem> clauses; 00557 00558 d_rules->learnedClauses(thm, clauses, false); 00559 00560 vector<Theorem>::iterator i = clauses.begin(), iend = clauses.end(); 00561 for (; i < iend; ++i) { 00562 // for dumping lemmas: 00563 // cerr << "QUERY " << (*i).getExpr() << ";" << endl; 00564 cnf.newClause(); 00565 Expr e = (*i).getExpr(); 00566 if (!e.isOr()) { 00567 DebugAssert(!getCNFLit(e).isNull(), "Unknown literal"); 00568 cnf.addLiteral(getCNFLit(e)); 00569 cnf.registerUnit(); 00570 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFAddUnit(*i)); 00571 } 00572 else { 00573 Expr::iterator jend = e.end(); 00574 for (Expr::iterator j = e.begin(); j != jend; ++j) { 00575 DebugAssert(!getCNFLit(*j).isNull(), "Unknown literal"); 00576 cnf.addLiteral(getCNFLit(*j)); 00577 } 00578 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFConvert(e, *i)); 00579 } 00580 } 00581 } 00582 00583 00584 Lit CNF_Manager::addAssumption(const Theorem& thm, CNF_Formula& cnf) 00585 { 00586 if (d_flags["cnf-formula"].getBool()) { 00587 Expr e = thm.getExpr(); 00588 DebugAssert(e.isOr() 00589 || (e.isNot() && e[0].isFalse()) 00590 || (e.isNot() && e[0].isTrue()), 00591 "expr:" + e.toString() + " is not an OR Expr or Ture or False" ); 00592 cnf.newClause(); 00593 if (e.isOr()){ 00594 for (int i = 0; i < e.arity(); i++){ 00595 Lit l = (translateExprRec(e[i], cnf, thm)); 00596 cnf.addLiteral(l); 00597 } 00598 cnf.getCurrentClause().setClauseTheorem(thm); 00599 return translateExprRec(e[0], cnf, thm) ;; 00600 } 00601 else { 00602 Lit l = translateExpr(thm, cnf); 00603 cnf.addLiteral(l); 00604 cnf.registerUnit(); 00605 cnf.getCurrentClause().setClauseTheorem(thm); 00606 return l; 00607 } 00608 } 00609 00610 00611 Lit l = translateExpr(thm, cnf); 00612 cnf.newClause(); 00613 cnf.addLiteral(l); 00614 cnf.registerUnit(); 00615 00616 00617 // if(concreteLit(l) != thm.getExpr()){ 00618 // cout<<"fail addunit 3" << endl; 00619 // } 00620 00621 Theorem newThm = d_rules->CNFAddUnit(thm); 00622 // d_theorems[d_clauseIdNext] = thm; 00623 cnf.getCurrentClause().setClauseTheorem(newThm); // by yeting 00624 /* 00625 cout<<"set clause theorem addassumption" << thm << endl; 00626 cout<<"set clause print" ; 00627 cnf.getCurrentClause().print() ; 00628 cout<<endl; 00629 cout<<"set clause id " << d_clauseIdNext << endl; 00630 */ 00631 return l; 00632 } 00633 00634 00635 Lit CNF_Manager::addLemma(Theorem thm, CNF_Formula& cnf) 00636 { 00637 00638 vector<Theorem> clauses; 00639 d_rules->learnedClauses(thm, clauses, true); 00640 DebugAssert(clauses.size() == 1, "expected single clause"); 00641 00642 Lit l = translateExpr(clauses[0], cnf); 00643 cnf.newClause(); 00644 cnf.addLiteral(l); 00645 cnf.registerUnit(); 00646 00647 00648 // if(concreteLit(l) != clauses[0].getExpr()){ 00649 // cout<<"fail addunit 4" << endl; 00650 // } 00651 00652 Theorem newThm = d_rules->CNFAddUnit(clauses[0]); 00653 // d_theorems.insert(d_clauseIdNext, clause); 00654 cnf.getCurrentClause().setClauseTheorem(newThm); //by yeting 00655 00656 /* 00657 cout<<"set clause theorem addlemma" << thm << endl; 00658 cout<<"set clause print" ; 00659 cnf.getCurrentClause().print() ; 00660 cout<<endl; 00661 cout<<"set clause id " << d_clauseIdNext << endl; 00662 */ 00663 return l; 00664 } 00665