CVC3
search_impl_base.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_impl_base.cpp
4  *
5  * Author: Clark Barrett, Vijay Ganesh (CNF Converter)
6  *
7  * Created: Fri Jan 17 14:19:54 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "search_impl_base.h"
23 #include "theory.h"
24 #include "eval_exception.h"
25 #include "search_rules.h"
26 #include "variable.h"
27 #include "command_line_flags.h"
28 #include "statistics.h"
29 #include "theorem_manager.h"
30 #include "expr_transform.h"
31 #include "assumptions.h"
32 
33 
34 using namespace std;
35 
36 
37 namespace CVC3 {
38 
39 
42  public:
44  virtual ~CoreSatAPI_implBase() {}
45  virtual void addLemma(const Theorem& thm, int priority, bool atBottomScope)
46  { d_se->addFact(thm); }
47  virtual Theorem addAssumption(const Expr& assump)
48  { return d_se->newIntAssumption(assump); }
49  virtual void addSplitter(const Expr& e, int priority)
50  { d_se->addSplitter(e, priority); }
51  virtual bool check(const Expr& e);
52  };
53 
54 bool CoreSatAPI_implBase::check(const Expr& e)
55 {
56  Theorem thm;
57  int scope = d_se->theoryCore()->getCM()->scopeLevel();
58  d_se->theoryCore()->getCM()->push();
59  QueryResult res = d_se->checkValid(e, thm);
60  d_se->theoryCore()->getCM()->popto(scope);
61  return res == VALID;
62 }
63 
64 
65 
66 }
67 
68 
69 using namespace CVC3;
70 
71 
72 // class SearchImplBase::Splitter methods
73 
74 // Constructor
75 SearchImplBase::Splitter::Splitter(const Literal& lit): d_lit(lit) {
76 d_lit.count()++;
77  TRACE("Splitter", "Splitter(", d_lit, ")");
78 }
79 
80 // Copy constructor
82  : d_lit(s.d_lit) {
83  d_lit.count()++;
84  TRACE("Splitter", "Splitter[copy](", d_lit, ")");
85 }
86 
87 // Assignment
90  if(this == &s) return *this; // Self-assignment
91  d_lit.count()--;
92  d_lit = s.d_lit;
93  d_lit.count()++;
94  TRACE("Splitter", "Splitter[assign](", d_lit, ")");
95  return *this;
96 }
97 
98 // Destructor
100  d_lit.count()--;
101  TRACE("Splitter", "~Splitter(", d_lit, ")");
102 }
103 
104 
105 
106 //! Constructor
108  : SearchEngine(core),
109  d_bottomScope(core->getCM()->getCurrentContext()),
110  d_dpSplitters(core->getCM()->getCurrentContext()),
111  d_lastValid(d_commonRules->trueTheorem()),
112  d_assumptions(core->getCM()->getCurrentContext()),
113  d_cnfCache(core->getCM()->getCurrentContext()),
114  d_cnfVars(core->getCM()->getCurrentContext()),
115  d_cnfOption(&(core->getFlags()["cnf"].getBool())),
116  d_ifLiftOption(&(core->getFlags()["iflift"].getBool())),
117  d_ignoreCnfVarsOption(&(core->getFlags()["ignore-cnf-vars"].getBool())),
118  d_origFormulaOption(&(core->getFlags()["orig-formula"].getBool())),
119  d_enqueueCNFCache(core->getCM()->getCurrentContext()),
120  d_applyCNFRulesCache(core->getCM()->getCurrentContext()),
121  d_replaceITECache(core->getCM()->getCurrentContext())
122 {
123  d_vm = new VariableManager(core->getCM(), d_rules,
124  core->getFlags()["mm"].getString());
125  IF_DEBUG(d_assumptions.setName("CDList[SearchImplBase::d_assumptions]");)
128 }
129 
130 
131 //! Destructor
133 {
134  delete d_coreSatAPI_implBase;
135  delete d_vm;
136 }
137 
138 
139 // Returns a new theorem if e has not already been asserted, otherwise returns
140 // a NULL theorem.
142  Theorem thm;
144  IF_DEBUG(if(debugger.trace("search verbose")) {
145  ostream& os(debugger.getOS());
146  os << "d_assumptions = [";
148  iend=d_assumptions.end(); i!=iend; ++i) {
149  debugger.getOS() << "(" << (*i).first << " => " << (*i).second << "), ";
150  }
151  os << "]" << endl;
152  })
153  if(i!=d_assumptions.end()) {
154  TRACE("search verbose", "newUserAssumption(", e,
155  "): assumption already exists");
156  } else {
157  thm = d_commonRules->assumpRule(e);
158  d_assumptions[e] = thm;
159  e.setUserAssumption();
160  TRACE("search verbose", "newUserAssumption(", thm,
161  "): created new assumption");
162  }
163  if (!thm.isNull()) d_core->addFact(d_core->getExprTrans()->preprocess(thm));
164  return thm;
165 }
166 
167 
168 // Same as newUserAssertion, except it's an error to assert something that's
169 // already been asserted.
171  Theorem thm = d_commonRules->assumpRule(e);
172  Expr atom = e.isNot() ? e[0] : e;
173  thm.setQuantLevel(theoryCore()->getQuantLevelForTerm(atom));
174  newIntAssumption(thm);
175  return thm;
176 }
177 
178 
181  "newIntAssumption: repeated assertion: "+thm.getExpr().toString());
182  d_assumptions[thm.getExpr()] = thm;
183  thm.getExpr().setIntAssumption();
184  TRACE("search verbose", "newIntAssumption(", thm,
185  "): new assumption");
186 }
187 
188 
189 void SearchImplBase::getUserAssumptions(vector<Expr>& assumptions)
190 {
192  iend=d_assumptions.orderedEnd(); i!=iend; ++i)
193  if ((*i).first.isUserAssumption()) assumptions.push_back((*i).first);
194 }
195 
196 
197 void SearchImplBase::getInternalAssumptions(std::vector<Expr>& assumptions)
198 {
200  iend=d_assumptions.orderedEnd(); i!=iend; ++i)
201  if ((*i).first.isIntAssumption()) assumptions.push_back((*i).first);
202 }
203 
204 
205 void SearchImplBase::getAssumptions(std::vector<Expr>& assumptions)
206 {
208  iend=d_assumptions.orderedEnd(); i!=iend; ++i)
209  assumptions.push_back((*i).first);
210 }
211 
212 
214  return d_assumptions.count(e) > 0;
215 }
216 
217 
218 void SearchImplBase::addCNFFact(const Theorem& thm, bool fromCore) {
219  TRACE("addCNFFact", "addCNFFact(", thm.getExpr(), ") {");
220  if(thm.isAbsLiteral()) {
221  addLiteralFact(thm);
222  // These literals are derived, and should also be reported to the core.
223  if(!fromCore) d_core->enqueueFact(thm);
224  } else {
225  addNonLiteralFact(thm);
226  }
227  TRACE_MSG("addCNFFact", "addCNFFact => }");
228 }
229 
230 
232  TRACE("search addFact", "SearchImplBase::addFact(", thm.getExpr(), ") {");
233  if(*d_cnfOption)
234  enqueueCNF(thm);
235  else
236  addCNFFact(thm, true);
237  TRACE_MSG("search addFact", "SearchImplBase::addFact => }");
238 }
239 
240 
241 void SearchImplBase::addSplitter(const Expr& e, int priority) {
242  DebugAssert(e.isAbsLiteral(), "SearchImplBase::addSplitter("+e.toString()+")");
244 }
245 
246 
247 void SearchImplBase::getCounterExample(vector<Expr>& assertions, bool inOrder)
248 {
249  if(!d_core->getTM()->withAssumptions())
250  throw EvalException
251  ("Method getCounterExample() (or command COUNTEREXAMPLE) cannot be used\n"
252  " without assumptions activated");
253  if(!d_lastValid.isNull())
254  throw EvalException
255  ("Method getCounterExample() (or command COUNTEREXAMPLE)\n"
256  " must be called only after failed QUERY");
257  getInternalAssumptions(assertions);
258  /*
259 
260  if(!d_lastCounterExample.empty()) {
261  if (inOrder) {
262  for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
263  iend=d_assumptions.orderedEnd(); i!=iend; ++i) {
264  if (d_lastCounterExample.find((*i).first) != d_lastCounterExample.end()) {
265  assertions.push_back((*i).first);
266  }
267  }
268  DebugAssert(assertions.size()==d_lastCounterExample.size(),
269  "getCounterExample: missing assertion");
270  }
271  else {
272  ExprHashMap<bool>::iterator i=d_lastCounterExample.begin(),
273  iend = d_lastCounterExample.end();
274  for(; i!=iend; ++i) assertions.push_back((*i).first);
275  }
276  }
277  */
278 }
279 
280 
281 Proof
283 {
284  if(!d_core->getTM()->withProof())
285  throw EvalException
286  ("DUMP_PROOF cannot be used without proofs activated");
287  if(d_lastValid.isNull())
288  throw EvalException
289  ("DUMP_PROOF must be called only after successful QUERY");
290  // Double-check for optimized version
291  if(d_lastValid.isNull()) return Proof();
292  return d_lastValid.getProof();
293 }
294 
295 
296 const Assumptions&
298 {
299  if(!d_core->getTM()->withAssumptions())
300  throw EvalException
301  ("DUMP_ASSUMPTIONS cannot be used without assumptions activated");
302  if(d_lastValid.isNull())
303  throw EvalException
304  ("DUMP_ASSUMPTIONS must be called only after successful QUERY");
305  // Double-check for optimized version
308 }
309 
310 /*!
311  * Given a proof of FALSE ('res') from an assumption 'e', derive the
312  * proof of the inverse of e.
313  *
314  * \param res is a proof of FALSE
315  * \param e is the assumption used in the above proof
316  */
317 void SearchImplBase::processResult(const Theorem& res, const Expr& e)
318 {
319  // Result must be either Null (== SAT) or false (== unSAT)
320  DebugAssert(res.isNull() || res.getExpr().isFalse(),
321  "processResult: bad input"
322  + res.toString());
323  if(res.isNull()) {
324  // Didn't prove valid (if CVC-lite is complete, it means invalid).
325  // The assumptions for the counterexample must have been already
326  // set by checkSAT().
327  d_lastValid = Theorem(); // Reset last proof
328  // Remove !e, keep just the counterexample
330  if (e.isNot()) d_lastCounterExample.erase(e[0]);
331  } else {
332  // Proved valid
333  Theorem res2 =
335  if(e.isNot())
336  d_lastValid = d_rules->negIntro(e, res2);
337  else
339  d_lastCounterExample.clear(); // Reset counterexample
340  }
341 }
342 
343 
347  result = d_lastValid;
348  return qres;
349 }
350 
351 
353  QueryResult qres = restartInternal(e);
354  result = d_lastValid;
355  return qres;
356 }
357 
358 
359 void
361  TRACE("mycnf", "enqueueCNF(", beta, ") {");
363  addCNFFact(beta);
364 
365  enqueueCNFrec(beta);
366  TRACE_MSG("mycnf", "enqueueCNF => }");
367 }
368 
369 
370 void
372  Theorem theta = beta;
373 
374  TRACE("mycnf","enqueueCNFrec(", theta.getExpr(), ") { ");
375  TRACE("cnf-clauses", "enqueueCNF call", theta.getExpr(), "");
376  // The theorem scope shouldn't be higher than current
377  DebugAssert(theta.getScope() <= scopeLevel(),
378  "\n theta.getScope()="+int2string(theta.getScope())
379  +"\n scopeLevel="+int2string(scopeLevel())
380  +"\n e = "+theta.getExpr().toString());
381 
382  Expr thetaExpr = theta.getExpr();
383 
384  if(d_enqueueCNFCache.count(thetaExpr) > 0) {
385  TRACE_MSG("mycnf", "enqueueCNFrec[cached] => }");
386  return;
387  }
388 
389  d_enqueueCNFCache[thetaExpr] = true;
390 
391  // // Strip double negations first
392  while(thetaExpr.isNot() && thetaExpr[0].isNot()) {
393  theta = d_commonRules->notNotElim(theta);
394  thetaExpr = theta.getExpr();
395  // Cache all the derived theorems too
396  d_enqueueCNFCache[thetaExpr] = true;
397  }
398 
399  // Check for a propositional literal
400  if(thetaExpr.isPropLiteral()) {
401  theta = d_commonRules->iffMP(theta, replaceITE(thetaExpr));
403  "Must be a literal: theta = "
404  +theta.getExpr().toString());
405  addCNFFact(theta);
406  TRACE_MSG("mycnf", "enqueueCNFrec[literal] => }");
407  TRACE("cnf-clauses", "literal with proofs(", theta.getExpr(), ")");
408  return;
409  }
410 
411  thetaExpr = theta.getExpr();
412  // Obvious optimizations for AND and OR
413  switch(thetaExpr.getKind()) {
414  case AND:
415  // Split up the top-level conjunction and translate individually
416  for(int i=0; i<thetaExpr.arity(); i++)
417  enqueueCNFrec(d_commonRules->andElim(theta, i));
418  TRACE_MSG("mycnf", "enqueueCNFrec[AND] => }");
419  return;
420  case OR: {
421  // Check if we are already in CNF (ignoring ITEs in the terms),
422  // and if we are, translate term ITEs on the way
423  bool cnf(true);
424  TRACE("bv mycnf", "enqueueCNFrec[OR] ( ", theta.getExpr().toString(), ")");
425  for(Expr::iterator i=thetaExpr.begin(),iend=thetaExpr.end();
426  i!=iend && cnf; i++) {
427  if(!(*i).isPropLiteral())
428  cnf = false;
429  }
430  if(cnf) {
431  vector<Theorem> thms;
432  vector<unsigned int> changed;
433  unsigned int cc=0;
434  for(Expr::iterator i=thetaExpr.begin(),iend=thetaExpr.end();
435  i!=iend; i++,cc++) {
436  Theorem thm = replaceITE(*i);
437  if(thm.getLHS() != thm.getRHS()) {
438  thms.push_back(thm);
439  changed.push_back(cc);
440  }
441  }
442  if(changed.size() > 0) {
443  Theorem rewrite =
444  d_commonRules->substitutivityRule(theta.getExpr(), changed, thms);
445  theta = d_commonRules->iffMP(theta, rewrite);
446  }
447  addCNFFact(theta);
448  TRACE_MSG("mycnf", "enqueueCNFrec[cnf] => }");
449  return;
450  }
451  break;
452  }
453  case IFF: { // Check for "var <=> phi" and "phi <=> var"
454  const Expr& t0 = thetaExpr[0];
455  const Expr& t1 = thetaExpr[1];
456  if(t1.isPropLiteral()) {
457  if(!t1.isAbsLiteral())
458  theta = d_commonRules->transitivityRule(theta, replaceITE(t1));
459  applyCNFRules(theta);
460  return;
461  } else if(thetaExpr[0].isPropLiteral()) {
462  theta = d_commonRules->symmetryRule(theta);
463  if(!t0.isAbsLiteral())
464  theta = d_commonRules->transitivityRule(theta, replaceITE(t0));
465  applyCNFRules(theta);
466  return;
467  }
468  break;
469  }
470  case ITE:
471  if(thetaExpr[0].isPropLiteral() && thetaExpr[1].isPropLiteral()
472  && thetaExpr[2].isPropLiteral()) {
473  // Replace ITEs
474  vector<Theorem> thms;
475  vector<unsigned int> changed;
476  for(int c=0, cend=thetaExpr.arity(); c<cend; ++c) {
477  Theorem thm = replaceITE(thetaExpr[c]);
478  if(thm.getLHS() != thm.getRHS()) {
480  "thm = "+thm.getExpr().toString());
481  thms.push_back(thm);
482  changed.push_back(c);
483  }
484  }
485  if(changed.size() > 0) {
486  Theorem rewrite =
487  d_commonRules->substitutivityRule(theta.getExpr(), changed, thms);
488  theta = d_commonRules->iffMP(theta, rewrite);
489  }
490  // Convert to clauses
491  Theorem thm = d_rules->iteToClauses(theta);
492  DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2,
493  "enqueueCNFrec [ITE over literals]\n thm = "
494  +thm.getExpr().toString());
495  addCNFFact(d_commonRules->andElim(thm, 0));
496  addCNFFact(d_commonRules->andElim(thm, 1));
497  return;
498  }
499  break;
500  default:
501  break;
502  }
503 
504  // Now do the real work
505  Theorem res = findInCNFCache(theta.getExpr());
506  if(!res.isNull()) {
507  Theorem thm = d_commonRules->iffMP(theta, res);
508  DebugAssert(thm.isAbsLiteral(), "thm = "+thm.getExpr().toString());
509  addCNFFact(thm);
510  TRACE("cnf-clauses", "enqueueCNFrec call[cache hit]:(",
511  thm.getExpr(), ")");
512  applyCNFRules(res);
513  TRACE_MSG("mycnf", "enqueueCNFrec[cached] => }");
514  return;
515  }
516 
517  // std::vector<Theorem> clauses;
518  Theorem result;
519  // (\phi <==> v)
520  result = d_commonRules->varIntroSkolem(theta.getExpr());
521 
522  TRACE("mycnf", "enqueueCNFrec: varIntroSkolem => ", result.getExpr(),
523  " @ "+int2string(result.getScope())
524  +" (current="+int2string(scopeLevel())+")");
525 
526  //result = skolemize(result, false);
527 
528  TRACE("mycnf", "enqueueCNFrec: skolemize => ", result.getExpr(),
529  " @ "+int2string(result.getScope())
530  +" (current="+int2string(scopeLevel())+")");
531  DebugAssert(result.isRewrite(),
532  "SearchImplBase::CNF(): result = "+result.toString());
533  DebugAssert(!result.getLHS().isPropLiteral() &&
534  result.getRHS().isPropLiteral(),
535  "SearchImplBase::CNF(): result = "+result.toString());
536  DebugAssert(result.getLHS() == theta.getExpr(),
537  "SearchImplBase::CNF(): result = "+result.toString()
538  +"\n theta = "+theta.toString());
539 
540  //enqueue v
541  Theorem var(d_commonRules->iffMP(theta, result));
542  // Add variable to the set of CNF vars
543  d_cnfVars[var.getExpr()] = true;
544  TRACE("mycnf", "enqueueCNFrec: theta = ", theta.getExpr(),
545  " @ "+int2string(theta.getScope())
546  +" (current="+int2string(scopeLevel())+")");
547  TRACE("mycnf", "enqueueCNFrec: var = ", var.getExpr(),
548  " @ "+int2string(var.getScope())
549  +" (current="+int2string(scopeLevel())+")");
550  DebugAssert(var.isAbsLiteral(), "var = "+var.getExpr().toString());
551  addCNFFact(var);
552  // phi <=> v
553  addToCNFCache(result);
554  applyCNFRules(result);
555  TRACE_MSG("mycnf", "enqueueCNFrec => }");
556 }
557 
558 
559 /*!
560  * \param thm is the input of the form phi <=> v
561  */
562 void
564  TRACE("mycnf", "applyCNFRules(", thm.getExpr(), ") { ");
565 
566  Theorem result = thm;
567  DebugAssert(result.isRewrite(),
568  "SearchImplBase::applyCNFRules: input must be an iff: " +
569  result.getExpr().toString());
570  Expr lhs = result.getLHS();
571  Expr rhs = result.getRHS();
573  "SearchImplBase::applyCNFRules: rhs of input must be literal: " +
574  result.getExpr().toString());
575 
576  // Eliminate negation first
577  while(result.getLHS().isNot())
578  result = d_commonRules->iffContrapositive(result);
579  lhs = result.getLHS();
580  rhs = result.getRHS();
581 
583  if(it == d_applyCNFRulesCache.end())
584  d_applyCNFRulesCache[lhs] = true;
585  else {
586  TRACE_MSG("mycnf","applyCNFRules[temp cache] => }");
587  return;
588  }
589 
590  // Catch the trivial case v1 <=> v2
591  if(lhs.isPropLiteral()) {
592  if(!lhs.isAbsLiteral()) {
593  Theorem replaced = d_commonRules->symmetryRule(replaceITE(lhs));
594  result = d_commonRules->transitivityRule(replaced, result);
595  lhs = result.getLHS();
596  DebugAssert(rhs == result.getRHS(),
597  "applyCNFRules [literal lhs]\n result = "
598  +result.getExpr().toString()
599  +"\n rhs = "+rhs.toString());
600  }
601  Theorem thm = d_rules->iffToClauses(result);
602  DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2,
603  "applyCNFRules [literal lhs]\n thm = "
604  +thm.getExpr().toString());
605  addCNFFact(d_commonRules->andElim(thm, 0));
606  addCNFFact(d_commonRules->andElim(thm, 1));
607  return;
608  }
609 
610  // Check the kids in e[0], replace them with cache[e[0][i]], rebuild thm
611  vector<unsigned> changed;
612  vector<Theorem> substitutions;
613  int c=0;
614  for(Expr::iterator j = lhs.begin(), jend = lhs.end(); j!=jend; ++c,++j) {
615  const Expr& phi = *j;
616  if(!phi.isPropLiteral()) {
617  Theorem phiIffVar = findInCNFCache(phi);
618  if(phiIffVar.isNull()) {
619  // Create a new variable for this child
620  phiIffVar = d_commonRules->varIntroSkolem(phi);
621  addToCNFCache(phiIffVar);
622  }
623  DebugAssert(phiIffVar.isRewrite(),
624  "SearchImplBase::applyCNFRules: result = " +
625  result.toString());
626  DebugAssert(phi == phiIffVar.getLHS(),
627  "SearchImplBase::applyCNFRules:\n phi = " +
628  phi.toString()
629  + "\n\n phiIffVar = " + phiIffVar.toString());
630  DebugAssert(phiIffVar.getRHS().isAbsLiteral(),
631  "SearchImplBase::applyCNFRules: phiIffVar = " +
632  phiIffVar.toString());
633  changed.push_back(c);
634  substitutions.push_back(phiIffVar);
635  applyCNFRules(phiIffVar);
636  }
637  }
638  if(changed.size() > 0) {
639  Theorem subst =
640  d_commonRules->substitutivityRule(lhs, changed, substitutions);
641  subst = d_commonRules->symmetryRule(subst);
642  result = d_commonRules->transitivityRule(subst, result);
643  }
644 
645  switch(result.getLHS().getKind()) {
646  case AND:
647  result = d_rules->andCNFRule(result);
648  break;
649  case OR:
650  result = d_rules->orCNFRule(result);
651  break;
652  case IFF:
653  result = d_rules->iffCNFRule(result);
654  break;
655  case IMPLIES:
656  result = d_rules->impCNFRule(result);
657  break;
658  case ITE:
659  result = d_rules->iteCNFRule(result);
660  break;
661  default:
662  DebugAssert(false,
663  "SearchImplBase::applyCNFRules: "
664  "the input operator must be and|or|iff|imp|ite\n result = " +
665  result.getLHS().toString());
666  break;
667  }
668 
669  // FIXME: eliminate this once debugged
670  Theorem clauses(result);
671 
672  // Enqueue the clauses
673  DebugAssert(!clauses.isNull(), "Oops!..");
674  DebugAssert(clauses.getExpr().isAnd(), "clauses = "
675  +clauses.getExpr().toString());
676 
677  // The clauses may containt term ITEs, and we need to translate those
678 
679  for(int i=0, iend=clauses.getExpr().arity(); i<iend; ++i) {
680  Theorem clause(d_commonRules->andElim(clauses,i));
681  addCNFFact(clause);
682  }
683  TRACE_MSG("mycnf","applyCNFRules => }");
684 }
685 
686 
688  if(e.isAbsLiteral()) return true;
689  if(!e.isOr()) return false;
690 
691  bool cnf(true);
692  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend && cnf; ++i)
693  cnf = (*i).isAbsLiteral();
694  return cnf;
695 }
696 
697 
698 bool
700  if(e.isPropLiteral()) return true;
701  if(!e.isOr()) return false;
702 
703  bool cnf(true);
704  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend && cnf; ++i)
705  cnf = (*i).isPropLiteral();
706  return cnf;
707 }
708 
709 
710 bool
712  if(!*d_ignoreCnfVarsOption) return true;
713  TRACE("isGoodSplitter", "isGoodSplitter(", e, ") {");
714  // Check for var being an auxiliary CNF variable
715  const Expr& var = e.isNot()? e[0] : e;
716  bool res(!isCNFVar(var));
717  TRACE("isGoodSplitter", "isGoodSplitter => ", res? "true" : "false", " }");
718  return res;
719 }
720 
721 
722 void
724  TRACE("mycnf", "addToCNFCache(", thm.getExpr(), ")");
725 
726  d_core->getStatistics().counter("CNF New Vars")++;
727 
728  Theorem result = thm;
729  DebugAssert(result.isRewrite(),
730  "SearchImplBase::addToCNFCache: input must be an iff: " +
731  result.getExpr().toString());
732  // Record the CNF variable
733  d_cnfVars[thm.getRHS()] = true;
734 
735  Theorem t(thm);
736  Expr phi = thm.getLHS();
737  while(phi.isNot()) {
739  phi = phi[0];
740  }
741  DebugAssert(d_cnfCache.count(phi) == 0,
742  "thm = "+thm.getExpr().toString() +
743  "\n t = "+ t.getExpr().toString());
744  //d_cnfCache.insert(phi, t);
746 }
747 
748 
749 Theorem
751  TRACE("mycnf", "findInCNFCache(", e, ") { ");
752  Expr phi(e);
753 
754  int numNegs(0);
755  // Strip all the top-level negations from e
756  while(phi.isNot()) {
757  phi = phi[0]; numNegs++;
758  }
760  if(it != d_cnfCache.end()) {
761  // IF_DEBUG(debugger.counter("CNF cache hits")++;)
762  d_core->getStatistics().counter("CNF cache hits")++;
763  Theorem thm = (*it).second;
764 
765  DebugAssert(thm.isRewrite() && thm.getLHS() == phi,
766  "SearchImplBase::findInCNFCache: thm must be an iff: " +
767  thm.getExpr().toString());
768 
769  // Now put all the negations back. If the number of negations is
770  // odd, first transform phi<=>v into !phi<=>!v. Then apply
771  // !!phi<=>phi rewrite as many times as needed.
772  if(numNegs % 2 != 0) {
773  thm = d_commonRules->iffContrapositive(thm);
774  numNegs--;
775  }
776  for(; numNegs > 0; numNegs-=2) {
777  Theorem t = d_commonRules->rewriteNotNot(!!(thm.getLHS()));
778  thm = d_commonRules->transitivityRule(t,thm);
779  }
780 
781  DebugAssert(numNegs == 0, "numNegs = "+int2string(numNegs));
782  TRACE("mycnf", "findInCNFCache => ", thm.getExpr(), " }");
783  return thm;
784  }
785  TRACE_MSG("mycnf", "findInCNFCache => null }");
786  return Theorem();
787 }
788 
789 /*!
790  * Strategy:
791  *
792  * For a given atomic formula phi(ite(c, t1, t2)) which depends on a
793  * term ITE, generate an equisatisfiable formula:
794  *
795  * phi(x) & ite(c, t1=x, t2=x),
796  *
797  * where x is a new variable.
798  *
799  * The phi(x) part will be generated by the caller, and our job is to
800  * assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem
801  * phi(ite(c, t1, t2)) <=> phi(x).
802  */
803 Theorem
805  TRACE("replaceITE","replaceITE(", e, ") { ");
806  Theorem res;
807 
809  iend=d_replaceITECache.end();
810  if(i!=iend) {
811  TRACE("replaceITE", "replaceITE[cached] => ", (*i).second, " }");
812  return (*i).second;
813  }
814 
815  if(e.isAbsLiteral())
816  res = d_core->rewriteLiteral(e);
817  else
818  res = d_commonRules->reflexivityRule(e);
819 
820 
821  // If 'res' is e<=>phi, and the resulting formula phi is not a
822  // literal, introduce a new variable x, enqueue phi<=>x, and return
823  // e<=>x.
824  if(!res.getRHS().isPropLiteral()) {
825  Theorem varThm(findInCNFCache(res.getRHS()));
826  if(varThm.isNull()) {
827  varThm = d_commonRules->varIntroSkolem(res.getRHS());
828  Theorem var;
829  if(res.isRewrite())
830  var = d_commonRules->transitivityRule(res,varThm);
831  else
832  var = d_commonRules->iffMP(res,varThm);
833  //d_cnfVars[var.getExpr()] = true;
834  //addCNFFact(var);
835  addToCNFCache(varThm);
836  }
837  applyCNFRules(varThm);
838  //enqueueCNFrec(varThm);
839  res = d_commonRules->transitivityRule(res, varThm);
840  }
841 
842  d_replaceITECache[e] = res;
843 
844  TRACE("replaceITE", "replaceITE => ", res, " }");
845  return res;
846 }