1 /*****************************************************************************/
2 /*!
3 *\file cnf_manager.cpp
4 *\brief Implementation of CNF_Manager
5 *
6 * Author: Clark Barrett
7 *
8 * Created: Thu Jan 5 02:30:02 2006
9 *
10 * <hr>
11 *
12 * License to use, copy, modify, sell and/or distribute this software
13 * and its documentation for any purpose is hereby granted without
14 * royalty, subject to the terms and conditions defined in the \ref
15 * LICENSE file provided with this distribution.
16 *
17 * <hr>
18 */
19 /*****************************************************************************/
20
21
22 #include "cnf_manager.h"
23 #include "cnf_rules.h"
24 #include "common_proof_rules.h"
25 #include "theorem_manager.h"
26 #include "vc.h"
27 #include "command_line_flags.h"
28
29
30 using namespace std;
31 using namespace CVC3;
32 using namespace SAT;
33
34
CNF_Manager(TheoremManager * tm,Statistics & statistics,const CLFlags & flags)35 CNF_Manager::CNF_Manager(TheoremManager* tm, Statistics& statistics,
36 const CLFlags& flags)
37 : d_vc(NULL),
38 d_commonRules(tm->getRules()),
39 // d_theorems(tm->getCM()->getCurrentContext()),
40 d_clauseIdNext(0),
41 // d_translated(tm->getCM()->getCurrentContext()),
42 d_bottomScope(-1),
43 d_statistics(statistics),
44 d_flags(flags),
45 d_nullExpr(tm->getEM()->getNullExpr()),
46 d_cnfCallback(NULL)
47 {
48 d_rules = createProofRules(tm, flags);
49 // Push dummy varinfo onto d_varInfo since Var's are indexed from 1 not 0
50 Varinfo v;
51 d_varInfo.push_back(v);
52 if (flags["minimizeClauses"].getBool()) {
53 CLFlags flags = ValidityChecker::createFlags();
54 flags.setFlag("minimizeClauses",false);
55 d_vc = ValidityChecker::create(flags);
56 }
57 }
58
59
~CNF_Manager()60 CNF_Manager::~CNF_Manager()
61 {
62 if (d_vc) delete d_vc;
63 delete d_rules;
64 }
65
66
registerAtom(const Expr & e,const Theorem & thm)67 void CNF_Manager::registerAtom(const Expr& e, const Theorem& thm)
68 {
69 DebugAssert(!e.isRegisteredAtom() || e.isUserRegisteredAtom(), "Atom already registered");
70 if (d_cnfCallback && !e.isRegisteredAtom()) d_cnfCallback->registerAtom(e, thm);
71 }
72
73
replaceITErec(const Expr & e,Var v,bool translateOnly)74 Theorem CNF_Manager::replaceITErec(const Expr& e, Var v, bool translateOnly)
75 {
76 // Quick exit for atomic expressions
77 if (e.isAtomic()) return d_commonRules->reflexivityRule(e);
78
79 // Check cache
80 Theorem thm;
81 bool foundInCache = false;
82 ExprHashMap<Theorem>::iterator iMap = d_iteMap.find(e);
83 if (iMap != d_iteMap.end()) {
84 thm = (*iMap).second;
85 foundInCache = true;
86 }
87
88 if (e.getKind() == ITE) {
89 // Replace non-Bool ITE expressions
90 DebugAssert(!e.getType().isBool(), "Expected non-Bool ITE");
91 // generate e = x for new x
92 if (!foundInCache) thm = d_commonRules->varIntroSkolem(e);
93 Theorem thm2 = d_commonRules->symmetryRule(thm);
94 thm2 = d_commonRules->iffMP(thm2, d_rules->ifLiftRule(thm2.getExpr(), 1));
95 d_translateQueueVars.push_back(v);
96 d_translateQueueThms.push_back(thm2);
97 d_translateQueueFlags.push_back(translateOnly);
98 }
99 else {
100 // Recursively traverse, replacing ITE's
101 vector<Theorem> thms;
102 vector<unsigned> changed;
103 unsigned index = 0;
104 Expr::iterator i, iend;
105 if (foundInCache) {
106 for(i = e.begin(), iend = e.end(); i!=iend; ++i, ++index) {
107 replaceITErec(*i, v, translateOnly);
108 }
109 }
110 else {
111 for(i = e.begin(), iend = e.end(); i!=iend; ++i, ++index) {
112 thm = replaceITErec(*i, v, translateOnly);
113 if (!thm.isRefl()) {
114 thms.push_back(thm);
115 changed.push_back(index);
116 }
117 }
118 if(changed.size() > 0) {
119 thm = d_commonRules->substitutivityRule(e, changed, thms);
120 }
121 else thm = d_commonRules->reflexivityRule(e);
122 }
123 }
124
125 // Update cache and return
126 if (!foundInCache) d_iteMap[e] = thm;
127 return thm;
128 }
129
130
concreteExpr(const CVC3::Expr & e,const Lit & literal)131 Expr CNF_Manager::concreteExpr(const CVC3::Expr& e, const Lit& literal){
132 if ( e.isTrue() || e.isFalse() ||
133 (e.isNot() && (e[0].isTrue() || e[0].isFalse())))
134 return e;
135 else
136 return concreteLit(literal);
137 }
138
concreteThm(const CVC3::Expr & ine)139 Theorem CNF_Manager::concreteThm(const CVC3::Expr& ine){
140 Theorem ret = d_iteMap[ine];
141 if (ret.isNull()) {
142 ret = d_commonRules->reflexivityRule(ine);
143 }
144 return ret;
145 }
146
translateExprRec(const Expr & e,CNF_Formula & cnf,const Theorem & thmIn)147 Lit CNF_Manager::translateExprRec(const Expr& e, CNF_Formula& cnf, const Theorem& thmIn)
148 {
149 if (e.isFalse()) return Lit::getFalse();
150 if (e.isTrue()) return Lit::getTrue();
151 if (e.isNot()) return !translateExprRec(e[0], cnf, thmIn);
152
153 ExprHashMap<Var>::iterator iMap = d_cnfVars.find(e);
154
155 if (e.isTranslated()) {
156 DebugAssert(iMap != d_cnfVars.end(), "Translated expr should be in map");
157 return Lit((*iMap).second);
158 }
159 else e.setTranslated(d_bottomScope);
160
161 Var v(int(d_varInfo.size()));
162 bool translateOnly = false;
163
164 if (iMap != d_cnfVars.end()) {
165 v = (*iMap).second;
166 translateOnly = true;
167 d_varInfo[v].fanouts.clear();
168 }
169 else {
170 d_varInfo.resize(v+1);
171 d_varInfo.back().expr = e;
172 d_cnfVars[e] = v;
173 }
174
175 Expr::iterator i, iend;
176 bool isAnd = false;
177 switch (e.getKind()) {
178 case AND:
179 isAnd = true;
180 case OR: {
181
182 vector<Lit> lits;
183 unsigned idx;
184 for (i = e.begin(), iend = e.end(); i != iend; ++i) {
185 lits.push_back(translateExprRec(*i, cnf, thmIn));
186 }
187
188 vector<Expr> new_chls;
189 vector<Theorem> thms;
190 for (idx = 0; idx < lits.size(); ++idx) {
191 new_chls.push_back(concreteExpr(e[idx],lits[idx]));
192 thms.push_back(concreteThm(e[idx]));
193 }
194
195 Expr after = (isAnd ? Expr(AND,new_chls) : Expr(OR,new_chls)) ;
196
197 // DebugAssert(concreteExpr(e,Lit(v)) == e,"why here");
198
199 for (idx = 0; idx < lits.size(); ++idx) {
200 cnf.newClause();
201 cnf.addLiteral(Lit(v),isAnd);
202 cnf.addLiteral(lits[idx], !isAnd);
203
204 // DebugAssert(concreteExpr(e[idx],lits[idx]) == e[idx], "why here");
205
206 std::string reasonStr = (isAnd ? "and_mid" : "or_mid");
207
208 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, reasonStr, idx,thms)); // by yeting
209 }
210
211 cnf.newClause();
212 cnf.addLiteral(Lit(v),!isAnd);
213 for (idx = 0; idx < lits.size(); ++idx) {
214 cnf.addLiteral(lits[idx], isAnd);
215 }
216
217 std::string reasonStr = (isAnd ? "and_final" : "or_final") ;
218
219 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, reasonStr, 0, thms)); // by yeting
220 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled");
221 break;
222 }
223 case IMPLIES: {
224 Lit arg0 = translateExprRec(e[0], cnf, thmIn);
225 Lit arg1 = translateExprRec(e[1], cnf, thmIn);
226
227 vector<Theorem> thms;
228 thms.push_back(concreteThm(e[0]));
229 thms.push_back(concreteThm(e[1]));
230
231 Expr left = (concreteExpr(e[0],arg0));
232 Expr right = (concreteExpr(e[1],arg1));
233 Expr after = left.impExpr(right);
234
235
236 // DebugAssert(concreteExpr(e, Lit(v)) == e, "why here");
237 // DebugAssert(concreteExpr(e[0], arg0) == e[0], "why here");
238 // DebugAssert(concreteExpr(e[1], arg1) == e[1], "why here");
239
240 cnf.newClause();
241 cnf.addLiteral(Lit(v));
242 cnf.addLiteral(arg0);
243
244 cnf.getCurrentClause().setClauseTheorem( d_rules->CNFtranslate(e, after, "imp", 0,thms)); // by yeting
245
246 cnf.newClause();
247 cnf.addLiteral(Lit(v));
248 cnf.addLiteral(arg1,true);
249
250 cnf.getCurrentClause().setClauseTheorem( d_rules->CNFtranslate(e, after, "imp", 1, thms)); // by yeting
251
252 cnf.newClause();
253 cnf.addLiteral(Lit(v),true);
254 cnf.addLiteral(arg0,true);
255 cnf.addLiteral(arg1);
256
257 cnf.getCurrentClause().setClauseTheorem( d_rules->CNFtranslate(e, after, "imp", 2,thms)); // by yeting
258 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled");
259 break;
260 }
261 case IFF: {
262 Lit arg0 = translateExprRec(e[0], cnf, thmIn);
263 Lit arg1 = translateExprRec(e[1], cnf, thmIn);
264
265 // DebugAssert(concreteExpr(e, Lit(v)) == e, "why here");
266 // DebugAssert(concreteExpr(e[0], arg0) == e[0], "why here");
267 // DebugAssert(concreteExpr(e[1], arg1) == e[1], "why here");
268 vector<Theorem> thms;
269 thms.push_back(concreteThm(e[0]));
270 thms.push_back(concreteThm(e[1]));
271
272 Expr left = (concreteExpr(e[0],arg0));
273 Expr right = (concreteExpr(e[1],arg1));
274 Expr after = left.iffExpr(right);
275
276
277 cnf.newClause();
278 cnf.addLiteral(Lit(v));
279 cnf.addLiteral(arg0);
280 cnf.addLiteral(arg1);
281
282 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "iff", 0, thms)); // by yeting
283
284 cnf.newClause();
285 cnf.addLiteral(Lit(v));
286 cnf.addLiteral(arg0,true);
287 cnf.addLiteral(arg1,true);
288
289 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "iff", 1, thms)); // by yeting
290
291 cnf.newClause();
292 cnf.addLiteral(Lit(v),true);
293 cnf.addLiteral(arg0,true);
294 cnf.addLiteral(arg1);
295
296 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "iff", 2, thms)); // by yeting
297
298 cnf.newClause();
299 cnf.addLiteral(Lit(v),true);
300 cnf.addLiteral(arg0);
301 cnf.addLiteral(arg1,true);
302
303 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "iff", 3, thms)); // by yeting
304 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled");
305 break;
306 }
307 case XOR: {
308
309 Lit arg0 = translateExprRec(e[0], cnf, thmIn);
310 Lit arg1 = translateExprRec(e[1], cnf, thmIn);
311
312 // DebugAssert(concreteExpr(e, Lit(v)) == e, "why here");
313 // DebugAssert(concreteExpr(e[0], arg0) == e[0], "why here");
314 // DebugAssert(concreteExpr(e[1], arg1) == e[1], "why here");
315
316 vector<Theorem> thms;
317 thms.push_back(concreteThm(e[0]));
318 thms.push_back(concreteThm(e[1]));
319
320 Expr left = (concreteExpr(e[0],arg0));
321 Expr right = (concreteExpr(e[1],arg1));
322 Expr after = left.xorExpr(right);
323
324
325 cnf.newClause();
326 cnf.addLiteral(Lit(v),true);
327 cnf.addLiteral(arg0);
328 cnf.addLiteral(arg1);
329
330 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "xor", 0, thms)); // by yeting
331
332 cnf.newClause();
333 cnf.addLiteral(Lit(v),true);
334 cnf.addLiteral(arg0,true);
335 cnf.addLiteral(arg1,true);
336
337 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "xor", 1, thms)); // by yeting
338
339 cnf.newClause();
340 cnf.addLiteral(Lit(v));
341 cnf.addLiteral(arg0,true);
342 cnf.addLiteral(arg1);
343
344 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "xor", 2, thms)); // by yeting
345
346 cnf.newClause();
347 cnf.addLiteral(Lit(v));
348 cnf.addLiteral(arg0);
349 cnf.addLiteral(arg1,true);
350
351 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFtranslate(e, after, "xor", 3,thms)); // by yeting
352 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled");
353 break;
354 }
355 case ITE:
356 {
357
358 Lit arg0 = translateExprRec(e[0], cnf, thmIn);
359 Lit arg1 = translateExprRec(e[1], cnf, thmIn);
360 Lit arg2 = translateExprRec(e[2], cnf, thmIn);
361
362
363 Expr aftere0 = concreteExpr(e[0], arg0);
364 Expr aftere1 = concreteExpr(e[1], arg1);
365 Expr aftere2 = concreteExpr(e[2], arg2);
366
367 vector<Expr> after ;
368 after.push_back(aftere0);
369 after.push_back(aftere1);
370 after.push_back(aftere2);
371
372 Theorem e0thm;
373 Theorem e1thm;
374 Theorem e2thm;
375
376 { e0thm = d_iteMap[e[0]];
377 if (e0thm.isNull()) e0thm = d_commonRules->reflexivityRule(e[0]);
378 e1thm = d_iteMap[e[1]];
379 if (e1thm.isNull()) e1thm = d_commonRules->reflexivityRule(e[1]);
380 e2thm = d_iteMap[e[2]];
381 if (e2thm.isNull()) e2thm = d_commonRules->reflexivityRule(e[2]);
382 }
383
384 vector<Theorem> thms ;
385 thms.push_back(e0thm);
386 thms.push_back(e1thm);
387 thms.push_back(e2thm);
388
389
390
391 cnf.newClause();
392 cnf.addLiteral(Lit(v),true);
393 cnf.addLiteral(arg0);
394 cnf.addLiteral(arg2);
395
396 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 1)); // by yeting
397
398 cnf.newClause();
399 cnf.addLiteral(Lit(v));
400 cnf.addLiteral(arg0);
401 cnf.addLiteral(arg2,true);
402
403 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 2)); // by yeting
404
405 cnf.newClause();
406 cnf.addLiteral(Lit(v));
407 cnf.addLiteral(arg0,true);
408 cnf.addLiteral(arg1,true);
409
410 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 3)); // by yeting
411
412 cnf.newClause();
413 cnf.addLiteral(Lit(v),true);
414 cnf.addLiteral(arg0,true);
415 cnf.addLiteral(arg1);
416
417 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 4)); // by yeting
418
419 cnf.newClause();
420 cnf.addLiteral(Lit(v));
421 cnf.addLiteral(arg1,true);
422 cnf.addLiteral(arg2,true);
423
424 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 5)); // by yeting
425
426 cnf.newClause();
427 cnf.addLiteral(Lit(v),true);
428 cnf.addLiteral(arg1);
429 cnf.addLiteral(arg2);
430
431 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFITEtranslate(e, after,thms, 6)); // by yeting
432 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled");
433 break;
434 }
435 default:
436 {
437 DebugAssert(!e.isAbsAtomicFormula() || d_varInfo[v].expr == e,
438 "Corrupted Varinfo");
439 if (e.isAbsAtomicFormula()) {
440 registerAtom(e, thmIn);
441 return Lit(v);
442 }
443
444 DebugAssert(!d_flags["cnf-formula"].getBool(), "Found impossible case when cnf-formula is enabled");
445
446 Theorem thm = replaceITErec(e, v, translateOnly);
447 const Expr& e2 = thm.getRHS();
448 DebugAssert(e2.isAbsAtomicFormula(), "Expected AbsAtomicFormula");
449 if (e2.isTranslated()) {
450 // Ugly corner case: we happen to create an expression that has been
451 // created before. We remove the current variable and fix up the
452 // translation stack.
453 if (translateOnly) {
454 DebugAssert(v == d_cnfVars[e2], "Expected literal match");
455 }
456 else {
457 d_varInfo.resize(v);
458 while (!d_translateQueueVars.empty() &&
459 d_translateQueueVars.back() == v) {
460 d_translateQueueVars.pop_back();
461 }
462 DebugAssert(d_cnfVars.find(e2) != d_cnfVars.end(),
463 "Expected existing literal");
464 v = d_cnfVars[e2];
465 d_cnfVars[e] = v;
466 while (d_translateQueueVars.size() < d_translateQueueThms.size()) {
467 d_translateQueueVars.push_back(v);
468 }
469 }
470 }
471 else {
472 e2.setTranslated(d_bottomScope);
473 // Corner case: don't register reflexive equality
474 if (!e2.isEq() || e2[0] != e2[1]) registerAtom(e2, thmIn);
475 if (!translateOnly) {
476 if (d_cnfVars.find(e2) == d_cnfVars.end()) {
477 d_varInfo[v].expr = e2;
478 d_cnfVars[e2] = v;
479 }
480 else {
481 // Same corner case in an untranslated expr
482 d_varInfo.resize(v);
483 while (!d_translateQueueVars.empty() &&
484 d_translateQueueVars.back() == v) {
485 d_translateQueueVars.pop_back();
486 }
487 v = d_cnfVars[e2];
488 d_cnfVars[e] = v;
489 while (d_translateQueueVars.size() < d_translateQueueThms.size()) {
490 d_translateQueueVars.push_back(v);
491 }
492 }
493 }
494 }
495 return Lit(v);
496 }
497 }
498
499 // Record fanins / fanouts
500 Lit l;
501 for (i = e.begin(), iend = e.end(); i != iend; ++i) {
502 l = getCNFLit(*i);
503 DebugAssert(!l.isNull(), "Expected non-null literal");
504 if (!translateOnly) d_varInfo[v].fanins.push_back(l);
505 if (l.isVar()) d_varInfo[l.getVar()].fanouts.push_back(v);
506 }
507 return Lit(v);
508 }
509
translateExpr(const Theorem & thmIn,CNF_Formula & cnf)510 Lit CNF_Manager::translateExpr(const Theorem& thmIn, CNF_Formula& cnf)
511 {
512 Lit l;
513 Var v;
514 Expr e = thmIn.getExpr();
515 Theorem thm;
516 bool translateOnly;
517
518 Lit ret = translateExprRec(e, cnf, thmIn);
519
520 while (d_translateQueueVars.size()) {
521 v = d_translateQueueVars.front();
522 d_translateQueueVars.pop_front();
523 thm = d_translateQueueThms.front();
524 d_translateQueueThms.pop_front();
525 translateOnly = d_translateQueueFlags.front();
526 d_translateQueueFlags.pop_front();
527 l = translateExprRec(thm.getExpr(), cnf, thmIn);
528 cnf.newClause();
529 cnf.addLiteral(l);
530 cnf.registerUnit();
531
532 Theorem newThm = d_rules->CNFAddUnit(thm);
533 // d_theorems.insert(d_clauseIdNext, thm);
534 // cnf.getCurrentClause().setClauseTheorem(thmIn); // by yeting
535 cnf.getCurrentClause().setClauseTheorem(newThm); // by yeting
536
537 /*
538 cout<<"set clause theorem 1" << thm << endl;
539 cout<<"set clause theorem 2 " << thmIn << endl;
540 cout<<"set clause print" ; cnf.getCurrentClause().print() ; cout<<endl;
541 cout<<"set clause id " << d_clauseIdNext << endl;
542 */
543 if (!translateOnly) d_varInfo[v].fanins.push_back(l);
544 d_varInfo[l.getVar()].fanouts.push_back(v);
545 }
546 return ret;
547 }
548
549
cons(unsigned lb,unsigned ub,const Expr & e2,vector<unsigned> & newLits)550 void CNF_Manager::cons(unsigned lb, unsigned ub, const Expr& e2, vector<unsigned>& newLits)
551 {
552 if (lb == ub) {
553 newLits.push_back(lb);
554 return;
555 }
556 unsigned new_lb = (ub-lb+1)/2 + lb;
557 unsigned index;
558 QueryResult res;
559 d_vc->push();
560 for (index = new_lb; index <= ub; ++index) {
561 d_vc->assertFormula(e2[index].negate());
562 }
563 res = d_vc->query(d_vc->falseExpr());
564 d_vc->pop();
565 if (res == VALID) {
566 cons(new_lb, ub, e2, newLits);
567 return;
568 }
569
570 unsigned new_ub = new_lb-1;
571 d_vc->push();
572 for (index = lb; index <= new_ub; ++index) {
573 d_vc->assertFormula(e2[index].negate());
574 }
575 res = d_vc->query(d_vc->falseExpr());
576 if (res == VALID) {
577 d_vc->pop();
578 cons(lb, new_ub, e2, newLits);
579 return;
580 }
581
582 cons(new_lb, ub, e2, newLits);
583 d_vc->pop();
584 d_vc->push();
585 for (index = 0; index < newLits.size(); ++index) {
586 d_vc->assertFormula(e2[newLits[index]].negate());
587 }
588 cons(lb, new_ub, e2, newLits);
589 d_vc->pop();
590 }
591
592
convertLemma(const Theorem & thm,CNF_Formula & cnf)593 void CNF_Manager::convertLemma(const Theorem& thm, CNF_Formula& cnf)
594 {
595 DebugAssert(cnf.empty(), "Expected empty cnf");
596 vector<Theorem> clauses;
597
598 d_rules->learnedClauses(thm, clauses, false);
599
600 vector<Theorem>::iterator i = clauses.begin(), iend = clauses.end();
601 for (; i < iend; ++i) {
602 // for dumping lemmas:
603 cnf.newClause();
604 Expr e = (*i).getExpr();
605 if (!e.isOr()) {
606 DebugAssert(!getCNFLit(e).isNull(), "Unknown literal");
607 cnf.addLiteral(getCNFLit(e));
608 cnf.registerUnit();
609 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFAddUnit(*i));
610 }
611 else {
612 Expr::iterator jend = e.end();
613 for (Expr::iterator j = e.begin(); j != jend; ++j) {
614 DebugAssert(!getCNFLit(*j).isNull(), "Unknown literal");
615 cnf.addLiteral(getCNFLit(*j));
616 }
617 cnf.getCurrentClause().setClauseTheorem(d_rules->CNFConvert(e, *i));
618 }
619 }
620 }
621
622
addAssumption(const Theorem & thm,CNF_Formula & cnf)623 Lit CNF_Manager::addAssumption(const Theorem& thm, CNF_Formula& cnf)
624 {
625 if (d_flags["cnf-formula"].getBool()) {
626 Expr e = thm.getExpr();
627 DebugAssert(e.isOr()
628 || (e.isNot() && e[0].isFalse())
629 || (e.isNot() && e[0].isTrue()),
630 "expr:" + e.toString() + " is not an OR Expr or Ture or False" );
631 cnf.newClause();
632 if (e.isOr()){
633 for (int i = 0; i < e.arity(); i++){
634 Lit l = (translateExprRec(e[i], cnf, thm));
635 cnf.addLiteral(l);
636 }
637 cnf.getCurrentClause().setClauseTheorem(thm);
638 return translateExprRec(e[0], cnf, thm) ;;
639 }
640 else {
641 Lit l = translateExpr(thm, cnf);
642 cnf.addLiteral(l);
643 cnf.registerUnit();
644 cnf.getCurrentClause().setClauseTheorem(thm);
645 return l;
646 }
647 }
648
649
650 Lit l = translateExpr(thm, cnf);
651 cnf.newClause();
652 cnf.addLiteral(l);
653 cnf.registerUnit();
654
655
656 // if(concreteLit(l) != thm.getExpr()){
657 // cout<<"fail addunit 3" << endl;
658 // }
659
660 Theorem newThm = d_rules->CNFAddUnit(thm);
661 // d_theorems[d_clauseIdNext] = thm;
662 cnf.getCurrentClause().setClauseTheorem(newThm); // by yeting
663 /*
664 cout<<"set clause theorem addassumption" << thm << endl;
665 cout<<"set clause print" ;
666 cnf.getCurrentClause().print() ;
667 cout<<endl;
668 cout<<"set clause id " << d_clauseIdNext << endl;
669 */
670 return l;
671 }
672
673
addLemma(Theorem thm,CNF_Formula & cnf)674 Lit CNF_Manager::addLemma(Theorem thm, CNF_Formula& cnf)
675 {
676
677 vector<Theorem> clauses;
678 d_rules->learnedClauses(thm, clauses, true);
679 DebugAssert(clauses.size() == 1, "expected single clause");
680
681 Lit l = translateExpr(clauses[0], cnf);
682 cnf.newClause();
683 cnf.addLiteral(l);
684 cnf.registerUnit();
685
686
687 // if(concreteLit(l) != clauses[0].getExpr()){
688 // cout<<"fail addunit 4" << endl;
689 // }
690
691 Theorem newThm = d_rules->CNFAddUnit(clauses[0]);
692 // d_theorems.insert(d_clauseIdNext, clause);
693 cnf.getCurrentClause().setClauseTheorem(newThm); //by yeting
694
695 /*
696 cout<<"set clause theorem addlemma" << thm << endl;
697 cout<<"set clause print" ;
698 cnf.getCurrentClause().print() ;
699 cout<<endl;
700 cout<<"set clause id " << d_clauseIdNext << endl;
701 */
702 return l;
703 }
704
705