CVC3
cnf_manager.cpp
Go to the documentation of this file.
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 
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 
61 {
62  if (d_vc) delete d_vc;
63  delete d_rules;
64 }
65 
66 
67 void CNF_Manager::registerAtom(const Expr& e, const Theorem& thm)
68 {
69  DebugAssert(!e.isRegisteredAtom() || e.isUserRegisteredAtom(), "Atom already registered");
71 }
72 
73 
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;
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 
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 
140  Theorem ret = d_iteMap[ine];
141  if (ret.isNull()) {
142  ret = d_commonRules->reflexivityRule(ine);
143  }
144  return ret;
145 }
146 
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 
154 
155  if (e.isTranslated()) {
156  DebugAssert(iMap != d_cnfVars.end(), "Translated expr should be in map");
157  return Lit((*iMap).second);
158  }
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  }
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 {
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 
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 
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 
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();
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  }
618  }
619  }
620 }
621 
622 
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  }
638  return translateExprRec(e[0], cnf, thm) ;;
639  }
640  else {
641  Lit l = translateExpr(thm, cnf);
642  cnf.addLiteral(l);
643  cnf.registerUnit();
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 
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