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