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
40 class CoreSatAPI_implBase :public TheoryCore::CoreSatAPI {
41 SearchImplBase* d_se;
42 public:
CoreSatAPI_implBase(SearchImplBase * se)43 CoreSatAPI_implBase(SearchImplBase* se) : d_se(se) {}
~CoreSatAPI_implBase()44 virtual ~CoreSatAPI_implBase() {}
addLemma(const Theorem & thm,int priority,bool atBottomScope)45 virtual void addLemma(const Theorem& thm, int priority, bool atBottomScope)
46 { d_se->addFact(thm); }
addAssumption(const Expr & assump)47 virtual Theorem addAssumption(const Expr& assump)
48 { return d_se->newIntAssumption(assump); }
addSplitter(const Expr & e,int priority)49 virtual void addSplitter(const Expr& e, int priority)
50 { d_se->addSplitter(e, priority); }
51 virtual bool check(const Expr& e);
52 };
53
check(const Expr & e)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
Splitter(const Literal & lit)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
Splitter(const SearchImplBase::Splitter & s)81 SearchImplBase::Splitter::Splitter(const SearchImplBase::Splitter& s)
82 : d_lit(s.d_lit) {
83 d_lit.count()++;
84 TRACE("Splitter", "Splitter[copy](", d_lit, ")");
85 }
86
87 // Assignment
88 SearchImplBase::Splitter&
operator =(const SearchImplBase::Splitter & s)89 SearchImplBase::Splitter::operator=(const SearchImplBase::Splitter& s) {
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
~Splitter()99 SearchImplBase::Splitter::~Splitter() {
100 d_lit.count()--;
101 TRACE("Splitter", "~Splitter(", d_lit, ")");
102 }
103
104
105
106 //! Constructor
SearchImplBase(TheoryCore * core)107 SearchImplBase::SearchImplBase(TheoryCore* core)
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]");)
126 d_coreSatAPI_implBase = new CoreSatAPI_implBase(this);
127 core->registerCoreSatAPI(d_coreSatAPI_implBase);
128 }
129
130
131 //! Destructor
~SearchImplBase()132 SearchImplBase::~SearchImplBase()
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.
newUserAssumption(const Expr & e)141 Theorem SearchImplBase::newUserAssumption(const Expr& e) {
142 Theorem thm;
143 CDMap<Expr,Theorem>::iterator i(d_assumptions.find(e));
144 IF_DEBUG(if(debugger.trace("search verbose")) {
145 ostream& os(debugger.getOS());
146 os << "d_assumptions = [";
147 for(CDMap<Expr,Theorem>::iterator i=d_assumptions.begin(),
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.
newIntAssumption(const Expr & e)170 Theorem SearchImplBase::newIntAssumption(const Expr& e) {
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
newIntAssumption(const Theorem & thm)179 void SearchImplBase::newIntAssumption(const Theorem& thm) {
180 DebugAssert(!d_assumptions.count(thm.getExpr()),
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
getUserAssumptions(vector<Expr> & assumptions)189 void SearchImplBase::getUserAssumptions(vector<Expr>& assumptions)
190 {
191 for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
192 iend=d_assumptions.orderedEnd(); i!=iend; ++i)
193 if ((*i).first.isUserAssumption()) assumptions.push_back((*i).first);
194 }
195
196
getInternalAssumptions(std::vector<Expr> & assumptions)197 void SearchImplBase::getInternalAssumptions(std::vector<Expr>& assumptions)
198 {
199 for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
200 iend=d_assumptions.orderedEnd(); i!=iend; ++i)
201 if ((*i).first.isIntAssumption()) assumptions.push_back((*i).first);
202 }
203
204
getAssumptions(std::vector<Expr> & assumptions)205 void SearchImplBase::getAssumptions(std::vector<Expr>& assumptions)
206 {
207 for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
208 iend=d_assumptions.orderedEnd(); i!=iend; ++i)
209 assumptions.push_back((*i).first);
210 }
211
212
isAssumption(const Expr & e)213 bool SearchImplBase::isAssumption(const Expr& e) {
214 return d_assumptions.count(e) > 0;
215 }
216
217
addCNFFact(const Theorem & thm,bool fromCore)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
addFact(const Theorem & thm)231 void SearchImplBase::addFact(const Theorem& thm) {
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
addSplitter(const Expr & e,int priority)241 void SearchImplBase::addSplitter(const Expr& e, int priority) {
242 DebugAssert(e.isAbsLiteral(), "SearchImplBase::addSplitter("+e.toString()+")");
243 d_dpSplitters.push_back(Splitter(newLiteral(e)));
244 }
245
246
getCounterExample(vector<Expr> & assertions,bool inOrder)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
getProof()282 SearchImplBase::getProof()
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&
getAssumptionsUsed()297 SearchImplBase::getAssumptionsUsed()
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
306 if(d_lastValid.isNull()) return Assumptions::emptyAssump();
307 return d_lastValid.getAssumptionsRef();
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 */
processResult(const Theorem & res,const Expr & e)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
329 d_lastCounterExample.erase(!e);
330 if (e.isNot()) d_lastCounterExample.erase(e[0]);
331 } else {
332 // Proved valid
333 Theorem res2 =
334 d_rules->eliminateSkolemAxioms(res, d_commonRules->getSkolemAxioms());
335 if(e.isNot())
336 d_lastValid = d_rules->negIntro(e, res2);
337 else
338 d_lastValid = d_rules->proofByContradiction(e, res2);
339 d_lastCounterExample.clear(); // Reset counterexample
340 }
341 }
342
343
checkValid(const Expr & e,Theorem & result)344 QueryResult SearchImplBase::checkValid(const Expr& e, Theorem& result) {
345 d_commonRules->clearSkolemAxioms();
346 QueryResult qres = checkValidInternal(e);
347 result = d_lastValid;
348 return qres;
349 }
350
351
restart(const Expr & e,Theorem & result)352 QueryResult SearchImplBase::restart(const Expr& e, Theorem& result) {
353 QueryResult qres = restartInternal(e);
354 result = d_lastValid;
355 return qres;
356 }
357
358
359 void
enqueueCNF(const Theorem & beta)360 SearchImplBase::enqueueCNF(const Theorem& beta) {
361 TRACE("mycnf", "enqueueCNF(", beta, ") {");
362 if(*d_origFormulaOption)
363 addCNFFact(beta);
364
365 enqueueCNFrec(beta);
366 TRACE_MSG("mycnf", "enqueueCNF => }");
367 }
368
369
370 void
enqueueCNFrec(const Theorem & beta)371 SearchImplBase::enqueueCNFrec(const Theorem& beta) {
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));
402 DebugAssert(!*d_ifLiftOption || theta.isAbsLiteral(),
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()) {
479 DebugAssert(!*d_ifLiftOption || thm.getRHS().isAbsLiteral(),
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
applyCNFRules(const Theorem & thm)563 SearchImplBase::applyCNFRules(const Theorem& thm) {
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();
572 DebugAssert(rhs.isAbsLiteral(),
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
582 CDMap<Expr,bool>::iterator it = d_applyCNFRulesCache.find(lhs);
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
isClause(const Expr & e)687 bool SearchImplBase::isClause(const Expr& e) {
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
isPropClause(const Expr & e)699 SearchImplBase::isPropClause(const Expr& e) {
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
isGoodSplitter(const Expr & e)711 SearchImplBase::isGoodSplitter(const Expr& e) {
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
addToCNFCache(const Theorem & thm)723 SearchImplBase::addToCNFCache(const Theorem& thm) {
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()) {
738 t = d_commonRules->iffContrapositive(thm);
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);
745 d_cnfCache.insert(phi, t, d_bottomScope);
746 }
747
748
749 Theorem
findInCNFCache(const Expr & e)750 SearchImplBase::findInCNFCache(const Expr& e) {
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 }
759 CDMap<Expr,Theorem>::iterator it = d_cnfCache.find(phi);
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
replaceITE(const Expr & e)804 SearchImplBase::replaceITE(const Expr& e) {
805 TRACE("replaceITE","replaceITE(", e, ") { ");
806 Theorem res;
807
808 CDMap<Expr,Theorem>::iterator i=d_replaceITECache.find(e),
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 }
847