CVC3  2.4.1
search_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_theorem_producer.cpp
4  * \brief Implementation of the proof rules for the simple search engine
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Mon Feb 24 14:51:51 2003
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 "search.h"
23 #include "theory_core.h"
24 #include "theorem_manager.h"
25 #include "common_proof_rules.h"
26 #include "command_line_flags.h"
27 #include "theory_arith.h"
28 // UNCOMMENT THIS FOR LFSC
29 #include "LFSCPrinter.h" // by liana for LFSC conversion
30 
31 #define _CVC3_TRUSTED_
33 
34 
35 using namespace std;
36 using namespace CVC3;
37 
38 
39 /////////////////////////////////////////////////////////////////////////////
40 // class SearchEngine trusted methods
41 /////////////////////////////////////////////////////////////////////////////
42 
43 
44 
46 SearchEngine::createRules() {
47  return new SearchEngineTheoremProducer(d_core->getTM());
48 }
49 
50 
51 // hack for printing original assumptions in LFSC by liana
52 bool lfsc_called = false;
54 
56 SearchEngine::createRules(SearchEngine* s_eng) {
57  search_engine = s_eng;
58  return new SearchEngineTheoremProducer(d_core->getTM());
59 }
60 
61 
62 SearchEngineTheoremProducer::SearchEngineTheoremProducer(TheoremManager* tm)
63  : TheoremProducer(tm), d_commonRules(tm->getRules())
64 { }
65 
66 
67 /////////////////////////////////////////////////////////////////////////////
68 // Proof rules
69 /////////////////////////////////////////////////////////////////////////////
70 
71 // Proof by contradiction: !A |- FALSE ==> |- A. "!A" doesn't
72 // have to be present in the assumptions.
73 Theorem
75  const Theorem& pfFalse) {
76  if(CHECK_PROOFS)
77  CHECK_SOUND(pfFalse.getExpr().isFalse(),
78  "proofByContradiction: pfFalse = : " + pfFalse.toString());
79  Expr not_a(!a);
80  Assumptions assump(pfFalse.getAssumptionsRef() - not_a);
81  Proof pf;
82  if(withProof()) {
83  // TODO: optimize with 1 traversal?
84  Theorem thm(pfFalse.getAssumptionsRef()[not_a]);
85  Proof u; // proof label for !aLFSCL
86  if(!thm.isNull()) u = thm.getProof();
87  // Proof compaction: if u is Null, use "FALSE => A" rule
88  if(u.isNull()){
89  pf = newPf("false_implies_anything", a, pfFalse.getProof());
90  if(!lfsc_called){
91  satProof(a, pf);
92  }
93  }
94  else
95  pf = newPf("pf_by_contradiction", a,
96  // LAMBDA-abstraction (LAMBDA (u: !a): pfFalse)
97  newPf(u, not_a, pfFalse.getProof()));
98  }
99  return newTheorem(a, assump, pf);
100 }
101 
102 // Similar rule, only negation introduction:
103 // A |- FALSE ==> !A
104 Theorem
106  const Theorem& pfFalse) {
107  if(CHECK_PROOFS) {
108  CHECK_SOUND(pfFalse.getExpr().isFalse(),
109  "negIntro: pfFalse = : " + pfFalse.toString());
110  CHECK_SOUND(not_a.isNot(), "negIntro: not_a = "+not_a.toString());
111  }
112 
113  Expr a(not_a[0]);
114  Assumptions assump(pfFalse.getAssumptionsRef() - a);
115  Proof pf;
116  if(withProof()) {
117  Theorem thm(pfFalse.getAssumptionsRef()[a]);
118  Proof u; // proof label for 'a'
119  if(!thm.isNull()) u = thm.getProof();
120  // Proof compaction: if u is Null, use "FALSE => !A" rule
121  if(u.isNull())
122  pf = newPf("false_implies_anything", not_a, pfFalse.getProof());
123 
124  else
125  pf = newPf("neg_intro", not_a,
126  // LAMBDA-abstraction (LAMBDA (u: a): pfFalse)
127  newPf(u, a, pfFalse.getProof()));
128  }
129  return newTheorem(not_a, assump, pf);
130 }
131 
132 
133 // Case split: u1:A |- C, u2:!A |- C ==> |- C
134 Theorem
136  const Theorem& a_proves_c,
137  const Theorem& not_a_proves_c) {
138  Expr c(a_proves_c.getExpr());
139 
140  if(CHECK_PROOFS) {
141  CHECK_SOUND(c == not_a_proves_c.getExpr(),
142  "caseSplit: conclusions differ:\n positive case C = "
143  + c.toString() + "\n negative case C = "
144  + not_a_proves_c.getExpr().toString());
145  // The opposite assumption should not appear in the theorems
146  // Actually, this doesn't violate soundness, no reason to check
147 // CHECK_SOUND(a_proves_c.getAssumptions()[!a].isNull(),
148 // "caseSplit: wrong assumption: " + (!a).toString()
149 // +"\n in "+a_proves_c.toString());
150 // CHECK_SOUND(not_a_proves_c.getAssumptions()[a].isNull(),
151 // "caseSplit: wrong assumption: " + a.toString()
152 // +"\n in "+not_a_proves_c.toString());
153  }
154 
155  const Assumptions& a1(a_proves_c.getAssumptionsRef());
156  const Assumptions& a2(not_a_proves_c.getAssumptionsRef());
157  Assumptions a3 = a1 - a;
158  Assumptions a4 = a2 - !a;
159 
160  // Proof compaction: if either theorem proves C without a or !a,
161  // then just use that theorem. This only works if assumptions are
162  // active.
163 
164  if (a1 == a3) return a_proves_c;
165  if (a2 == a4) return not_a_proves_c;
166 
167  // No easy way out. Do the work.
168  Proof pf;
169  a3.add(a4);
170 
171  if(withProof()) {
172  // Create lambda-abstractions
173  vector<Proof> pfs;
174  pfs.push_back(newPf(a1[a].getProof(),
175  a, a_proves_c.getProof()));
176  pfs.push_back(newPf(a2[!a].getProof(),
177  !a, not_a_proves_c.getProof()));
178  pf = newPf("case_split", a, c, pfs);
179  }
180  return newTheorem(c, a3, pf);
181 }
182 
183 // Conflict clause rule:
184 // Gamma, A_1,...,A_n |- B ==> Gamma |- (OR B A_1 ... A_n)
185 // The assumptions A_i are given by the vector 'lits'.
186 // If B==FALSE, it is omitted from the result.
187 
188 // NOTE: here "!A_i" means an inverse of A_i, not just a negation.
189 // That is, if A_i is NOT C, then !A_i is C.
190 
191 // verification function used by conflictClause
193  TheoremMap& m) {
194  const Assumptions& a(thm.getAssumptionsRef());
195  const Assumptions::iterator iend = a.end();
196  for (Assumptions::iterator i = a.begin();
197  i != iend; ++i) {
198  CHECK_SOUND(!i->isNull(),
199  "SearchEngineTheoremProducer::conflictClause: "
200  "Found null theorem");
201  if (!i->isRefl() && !i->isFlagged()) {
202  i->setFlag();
203  if (m.count(*i) == 0) {
204  CHECK_SOUND(!i->isAssump(),
205  "SearchEngineTheoremProducer::conflictClause: "
206  "literal and gamma sets do not form a complete "
207  "cut of Theorem assumptions. Stray theorem: \n"
208  +i->toString());
209  verifyConflict(*i, m);
210  }
211  else {
212  m[*i] = true;
213  }
214  }
215  }
216 }
217 
218 
219 Theorem
221 conflictClause(const Theorem& thm, const vector<Theorem>& lits,
222  const vector<Theorem>& gamma) {
223  // TRACE("search proofs", "conflictClause(", thm.getExpr(), ") {");
224  IF_DEBUG(if(debugger.trace("search proofs")) {
225  ostream& os = debugger.getOS();
226  os << "lits = [";
227  for(vector<Theorem>::const_iterator i=lits.begin(), iend=lits.end();
228  i!=iend; ++i)
229  os << i->getExpr() << ",\n";
230  os << "]\n\ngamma = [";
231  for(vector<Theorem>::const_iterator i=gamma.begin(), iend=gamma.end();
232  i!=iend; ++i)
233  os << i->getExpr() << ",\n";
234  os << "]" << endl;
235  });
236  bool checkProofs(CHECK_PROOFS);
237  // This rule only makes sense when runnnig with assumptions
238  if(checkProofs) {
240  "conflictClause: called while running without assumptions");
241  }
242 
243  // Assumptions aOrig(thm.getAssumptions());
244 
245  vector<Expr> literals;
246  vector<Proof> u; // Vector of proof labels
247  literals.reserve(lits.size() + 1);
248  u.reserve(lits.size());
249  const vector<Theorem>::const_iterator iend = lits.end();
250  for(vector<Theorem>::const_iterator i=lits.begin(); i!=iend; ++i) {
251  Expr neg(i->getExpr().negate());
252 
253  literals.push_back(neg);
254  if(withProof()) u.push_back(i->getProof());
255  }
256 
257  if(checkProofs) {
258  TheoremMap m;
259  // TRACE_MSG("search proofs", "adding gamma to m: {");
260  for(vector<Theorem>::const_iterator i = gamma.begin();
261  i != gamma.end(); ++i) {
262  // TRACE("search proofs", "m[", *i, "]");
263  m[*i] = false;
264  }
265  // TRACE_MSG("search proofs", "}");
266 
267  for(vector<Theorem>::const_iterator i = lits.begin(); i!=iend; ++i) {
268  // TRACE("search proofs", "check lit: ", *i, "");
269  CHECK_SOUND(m.count(*i) == 0,
270  "SearchEngineTheoremProducer::conflictClause: "
271  "literal and gamma sets are not disjoint: lit = "
272  +i->toString());
273  m[*i] = false;
274  }
275  thm.clearAllFlags();
276  verifyConflict(thm, m);
277  TheoremMap::iterator t = m.begin(), tend = m.end();
278  for (; t != tend; ++t) {
279  CHECK_SOUND(t->second == true,
280  "SearchEngineTheoremProducer::conflictClause: "
281  "literal or gamma set contains extra element : "
282  + t->first.toString());
283  }
284  }
285 
286  Assumptions a(gamma);
287 
288  if(!thm.getExpr().isFalse())
289  literals.push_back(thm.getExpr());
290 
291  Proof pf;
292  if(withProof()) {
293  if(lits.size()>0) {
294  vector<Expr> assump;
295  // If assumptions are not leaves, we need to create new
296  // variables for them and substitute them for their proofs in
297  // the proof term
298  ExprHashMap<Expr> subst;
299  DebugAssert(u.size() == lits.size(), "");
300  for(size_t i=0, iend=lits.size(); i<iend; ++i) {
301  const Expr& e(lits[i].getExpr());
302  assump.push_back(e);
303  Proof& v = u[i];
304  if(!v.getExpr().isVar()) {
305  Proof label = newLabel(e);
306  subst[v.getExpr()] = label.getExpr();
307  v = label;
308  }
309  }
310  Proof body(thm.getProof());
311  if(!subst.empty())
312  body = Proof(body.getExpr().substExpr(subst));
313  pf = newPf("conflict_clause", newPf(u, assump, body));
314  }
315  else
316  pf = newPf("false_to_empty_or", thm.getProof());
317  }
318  Theorem res(newTheorem(Expr(OR, literals, d_em), a, pf));
319  // TRACE("search proofs", "conflictClause => ", res.getExpr(), " }");
320  return res;
321 }
322 
323 
324 // Theorem
325 // SearchEngineTheoremProducer::
326 // conflictClause(const Theorem& thm, const vector<Expr>& lits) {
327 // bool checkProofs(CHECK_PROOFS);
328 // // This rule only makes sense when runnnig with assumptions
329 // if(checkProofs) {
330 // CHECK_SOUND(withAssumptions(),
331 // "conflictClause: called while running without assumptions");
332 // }
333 
334 // Assumptions aOrig(thm.getAssumptions());
335 
336 // vector<Expr> literals;
337 // vector<Expr> negations;
338 // vector<Proof> u; // Vector of proof labels
339 // literals.reserve(lits.size() + 1);
340 // negations.reserve(lits.size());
341 // u.reserve(lits.size());
342 // for(vector<Expr>::const_iterator i=lits.begin(), iend=lits.end();
343 // i!=iend; ++i) {
344 // Expr neg(i->isNot()? (*i)[0] : !(*i));
345 // if(checkProofs)
346 // CHECK_SOUND(!aOrig[neg].isNull(),
347 // "SearchEngineTheoremProducer::conflictClause: "
348 // "literal is not in the set of assumptions: neg = "
349 // +neg.toString() + "\n Theorem = " + thm.toString());
350 // literals.push_back(*i);
351 // negations.push_back(neg);
352 // if(withProof()) u.push_back(aOrig[neg].getProof());
353 // }
354 
355 // Assumptions a = aOrig - negations;
356 
357 // if(!thm.getExpr().isFalse())
358 // literals.push_back(thm.getExpr());
359 
360 // Proof pf;
361 // if(withProof()) {
362 // if(lits.size()>0)
363 // pf = newPf("conflict_clause", newPf(u, literals, thm.getProof()));
364 // else
365 // pf = newPf("false_to_empty_or", thm.getProof());
366 // }
367 // // Use ExprManager in newExpr, since literals may be empty
368 // return newTheorem(Expr(d_em, OR, literals), a, pf);
369 // }
370 
371 
372 // "Cut" rule: { G_i |- A_i }; G', { A_i } |- B ==> union(G_i)+G' |- B.
373 Theorem
375 cutRule(const vector<Theorem>& thmsA,
376  const Theorem& as_prove_b) {
377  if(CHECK_PROOFS)
379  "cutRule called without assumptions activated");
380  // Optimization: use only those theorems that occur in B's assumptions.
381  // *** No, take it back, it's a mis-optimization. Most of the time,
382  // cutRule is applied when we *know* thmsA are present in the
383  // assumptions of 'as_proof_b'.
384 
385  Proof pf;
386  vector<Expr> exprs;
387  exprs.reserve(thmsA.size() + 1);
388  const vector<Theorem>::const_iterator iend = thmsA.end();
389  for(vector<Theorem>::const_iterator i=thmsA.begin(); i!=iend; ++i) {
390  exprs.push_back(i->getExpr());
391  }
392 
393  Assumptions a(thmsA); // add the As
394  a.add(as_prove_b.getAssumptionsRef() - exprs); // Add G'
395 
396  if(withProof()) {
397  vector<Proof> pfs;
398  pfs.reserve(thmsA.size() + 1);
399  for(vector<Theorem>::const_iterator i = thmsA.begin(); i != iend; ++i) {
400  pfs.push_back(i->getProof());
401  }
402  exprs.push_back(as_prove_b.getExpr());
403  pfs.push_back(as_prove_b.getProof());
404  pf = newPf("cut_rule",exprs,pfs);
405  }
406  return newTheorem(as_prove_b.getExpr(), a, pf);
407 }
408 
409 
410 void
412  ExprMap<bool>& visited,
413  const ExprMap<bool>& skolems)
414 {
415  if(visited.count(e)>0)
416  return;
417  else
418  visited[e] = true;
419  CHECK_SOUND(skolems.count(e) == 0,
420  "skolem constant found in axioms of false theorem: "
421  + e.toString());
422  for(Expr::iterator it = e.begin(), end = e.end(); it!= end; ++it)
423  checkSoundNoSkolems(*it, visited, skolems);
424  if(e.getKind() == FORALL || e.getKind() == EXISTS)
425  checkSoundNoSkolems(e.getBody(), visited, skolems);
426 }
427 
428 void
430  ExprMap<bool>& visited,
431  const ExprMap<bool>& skolems)
432 {
433  if(t.isRefl() || t.isFlagged())
434  return;
435  t.setFlag();
436  if(t.isAssump())
437  checkSoundNoSkolems(t.getExpr(), visited, skolems);
438  else
439  {
440  const Assumptions& a(t.getAssumptionsRef());
441  Assumptions::iterator it = a.begin(), end = a.end();
442  for(; it!=end; ++it)
443  checkSoundNoSkolems(*it, visited, skolems);
444  }
445 }
446 
447 /*! Eliminate skolem axioms:
448  * Gamma, Delta |- false => Gamma|- false
449  * where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
450  * and gamma does not contain any of the skolem constants c.
451  */
452 
453 Theorem
455  const std::vector<Theorem>& delta)
456 {
457  TRACE("skolem", "=>eliminateSkolemAxioms ", delta.size(), "{");
458  if(delta.empty())
459  {
460  TRACE("skolem", "eliminateSkolemAxioms","" , "}");
461  return tFalse;
462  }
463  const Expr& falseExpr = tFalse.getExpr();
464  if(CHECK_PROOFS) {
465  CHECK_SOUND(falseExpr.isFalse(),
466  "eliminateSkolemAxiom called on non-false theorem");
467  ExprMap<bool> visited;
468  ExprMap<bool> skolems;
469  vector<Theorem>::const_iterator it = delta.begin(), end = delta.end();
470  for(; it!=end; ++it) {
471  CHECK_SOUND(it->isRewrite(),
472  "eliminateSkolemAxioms(): Skolem axiom is not "
473  "an IFF: "+it->toString());
474  const Expr& ex = it->getLHS();
475  CHECK_SOUND(ex.isExists(),
476  "Did not receive skolem axioms in Delta"
477  " of eliminateSkolemAxioms" + it->toString());
478  // Collect the Skolem constants for further soundness checks
479  for(unsigned int j=0; j<ex.getVars().size(); j++) {
480  Expr sk_var(ex.skolemExpr(j));
481  if(sk_var.getType().isBool()) {
482  sk_var = d_em->newLeafExpr(sk_var.mkOp());
483  }
484  skolems[sk_var] = true;
485  TRACE("skolem", ">> Eliminating variable: ", sk_var, "<<");
486  }
487  }
488  tFalse.clearAllFlags();
489  checkSoundNoSkolems(tFalse, visited, skolems);
490  }
491  Proof pf;
492  if(!withProof()) return tFalse;
493  else
494  {
495  Proof origFalse = tFalse.getProof();
496  std::vector<Proof>skolemizeLabels;
497  std::vector<Expr> exprs;
498  for(unsigned int i=0; i<delta.size(); i++)
499  {
500  exprs.push_back(delta[i].getExpr());
501  skolemizeLabels.push_back(delta[i].getProof());
502  }
503  pf = newPf(skolemizeLabels, exprs, origFalse);
504  }
505  TRACE("skolem", "eliminateSkolemAxioms","" , "}");
506  return newTheorem(tFalse.getExpr(), tFalse.getAssumptionsRef(), pf);
507 }
508 
509 
510 Theorem
511 SearchEngineTheoremProducer::unitProp(const std::vector<Theorem>& thms,
512  const Theorem& clause,
513  unsigned i) {
514  Expr e(clause.getExpr());
515  if(CHECK_PROOFS) {
516  // Soundness check: first, check the form of the 'clause' theorem
517  CHECK_SOUND(e.isOr() && e.arity() > (int)i,
518  "SearchEngineTheoremProducer::unitProp: bad theorem or i="
519  +int2string(i)+" > arity="+int2string(e.arity())
520  +" in clause = " + clause.toString());
521  // Now, check correspondence of thms to the disjunction
522  CHECK_SOUND(((int)thms.size()) == e.arity() - 1,
523  "SearchEngineTheoremProducer::unitProp: "
524  "wrong number of theorems"
525  "\n thms.size = " + int2string(thms.size())
526  +"\n clause.arity = " + int2string(e.arity()));
527 
528  for(unsigned j=0,k=0; j<thms.size(); j++) {
529  if(j!=i) {
530  Expr ej(e[j]), ek(thms[k].getExpr());
531  CHECK_SOUND((ej.isNot() && ej[0] == ek) || (ek.isNot() && ej == ek[0]),
532  "SearchEngineTheoremProducer::unitProp: "
533  "wrong theorem["+int2string(k)+"]"
534  "\n thm = " + thms[k].toString() +
535  "\n literal = " + e[j].toString() +
536  "\n clause = " + clause.toString());
537  k++;
538  }
539  }
540  }
541 
542  Assumptions a(thms);
543  a.add(clause);
544  Proof pf;
545 
546  if(withProof()) {
547  vector<Proof> pfs;
548  vector<Expr> exprs;
549  exprs.reserve(thms.size() + 1);
550  pfs.reserve(thms.size()+1);
551  const vector<Theorem>::const_iterator iend = thms.end();
552  for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
553  exprs.push_back(i->getExpr());
554  pfs.push_back(i->getProof());
555  }
556  exprs.push_back(clause.getExpr());
557  pfs.push_back(clause.getProof());
558  pf = newPf("unit_prop", exprs, pfs);
559  }
560  return newTheorem(e[i], a, pf);
561 }
562 
563 Theorem
565  bool left,
566  const Theorem& b_th) {
567  const Expr& andr_e(andr_th.getExpr());
568  if(CHECK_PROOFS) {
569  CHECK_SOUND(andr_e.getKind() == AND_R &&
570  ((left && b_th.refutes(andr_e[1])) ||
571  (!left && b_th.refutes(andr_e[2]))),
572  "SearchEngineTheoremProducer::propAndrAF");
573  }
574 
575  Assumptions a(andr_th, b_th);
576  Proof pf;
577 
578  if(withProof()) {
579  vector<Proof> pfs;
580  vector<Expr> exprs;
581  exprs.push_back(andr_th.getExpr());
582  exprs.push_back(b_th.getExpr());
583  pfs.push_back(andr_th.getProof());
584  pfs.push_back(b_th.getProof());
585  // can we note which branch to take?
586  pf = newPf("prop_andr_af", exprs, pfs);
587  }
588 
589  return newTheorem(andr_e[0].negate(), a, pf);
590 }
591 
592 Theorem
594  const Theorem& l_th,
595  const Theorem& r_th) {
596  const Expr& andr_e(andr_th.getExpr());
597  if(CHECK_PROOFS) {
598  CHECK_SOUND(andr_e.getKind() == AND_R &&
599  l_th.proves(andr_e[1]) && r_th.proves(andr_e[2]),
600  "SearchEngineTheoremProducer::propAndrAT");
601  }
602 
603  Assumptions a(andr_th, l_th);
604  a.add(r_th);
605  Proof pf;
606 
607  if(withProof()) {
608  vector<Proof> pfs;
609  vector<Expr> exprs;
610  exprs.push_back(andr_th.getExpr());
611  exprs.push_back(l_th.getExpr());
612  exprs.push_back(r_th.getExpr());
613  pfs.push_back(andr_th.getProof());
614  pfs.push_back(l_th.getProof());
615  pfs.push_back(r_th.getProof());
616  pf = newPf("prop_andr_at", exprs, pfs);
617  }
618 
619  return newTheorem(andr_e[0], a, pf);
620 }
621 
622 void
624  const Theorem& a_th,
625  Theorem* l_th,
626  Theorem* r_th) {
627  const Expr& andr_e(andr_th.getExpr());
628  if(CHECK_PROOFS) {
629  CHECK_SOUND(andr_e.getKind() == AND_R && a_th.proves(andr_e[0]),
630  "SearchEngineTheoremProducer::propAndrLRT");
631  }
632 
633  Assumptions a(andr_th, a_th);
634  Proof pf;
635 
636  if(withProof()) {
637  vector<Proof> pfs;
638  vector<Expr> exprs;
639  exprs.push_back(andr_th.getExpr());
640  exprs.push_back(a_th.getExpr());
641  pfs.push_back(andr_th.getProof());
642  pfs.push_back(a_th.getProof());
643  pf = newPf("prop_andr_lrt", exprs, pfs);
644  }
645 
646  if (l_th) *l_th = newTheorem(andr_e[1], a, pf);
647  if (r_th) *r_th = newTheorem(andr_e[2], a, pf);
648 }
649 
650 Theorem
652  const Theorem& a_th,
653  const Theorem& r_th) {
654  const Expr& andr_e(andr_th.getExpr());
655  if(CHECK_PROOFS) {
656  CHECK_SOUND(andr_e.getKind() == AND_R &&
657  a_th.refutes(andr_e[0]) && r_th.proves(andr_e[2]),
658  "SearchEngineTheoremProducer::propAndrLF");
659  }
660 
661  Assumptions a(andr_th, a_th);
662  a.add(r_th);
663  Proof pf;
664 
665  if(withProof()) {
666  vector<Proof> pfs;
667  vector<Expr> exprs;
668  exprs.push_back(andr_th.getExpr());
669  exprs.push_back(a_th.getExpr());
670  exprs.push_back(r_th.getExpr());
671  pfs.push_back(andr_th.getProof());
672  pfs.push_back(a_th.getProof());
673  pfs.push_back(r_th.getProof());
674  pf = newPf("prop_andr_lf", exprs, pfs);
675  }
676 
677  return newTheorem(andr_e[1].negate(), a, pf);
678 }
679 
680 Theorem
682  const Theorem& a_th,
683  const Theorem& l_th) {
684  const Expr& andr_e(andr_th.getExpr());
685  if(CHECK_PROOFS) {
686  CHECK_SOUND(andr_e.getKind() == AND_R &&
687  a_th.refutes(andr_e[0]) && l_th.proves(andr_e[1]),
688  "SearchEngineTheoremProducer::propAndrRF");
689  }
690 
691  Assumptions a(andr_th, a_th);
692  a.add(l_th);
693  Proof pf;
694 
695  if(withProof()) {
696  vector<Proof> pfs;
697  vector<Expr> exprs;
698  exprs.push_back(andr_th.getExpr());
699  exprs.push_back(a_th.getExpr());
700  exprs.push_back(l_th.getExpr());
701  pfs.push_back(andr_th.getProof());
702  pfs.push_back(a_th.getProof());
703  pfs.push_back(l_th.getProof());
704  pf = newPf("prop_andr_rf", exprs, pfs);
705  }
706 
707  return newTheorem(andr_e[2].negate(), a, pf);
708 }
709 
710 Theorem
712  const Theorem& a_th,
713  bool left,
714  const Theorem& b_th) {
715  const Expr& andr_e(andr_th.getExpr());
716  if(CHECK_PROOFS) {
717  CHECK_SOUND(andr_e.getKind() == AND_R && a_th.proves(andr_e[0]) &&
718  ((left && b_th.refutes(andr_e[1])) ||
719  (!left && b_th.refutes(andr_e[2]))),
720  "SearchEngineTheoremProducer::confAndrAT");
721  }
722 
723  Assumptions a(andr_th, a_th);
724  a.add(b_th);
725  Proof pf;
726 
727  if(withProof()) {
728  vector<Proof> pfs;
729  vector<Expr> exprs;
730  exprs.push_back(andr_th.getExpr());
731  exprs.push_back(a_th.getExpr());
732  exprs.push_back(b_th.getExpr());
733  pfs.push_back(andr_th.getProof());
734  pfs.push_back(a_th.getProof());
735  pfs.push_back(b_th.getProof());
736  // can we note which branch to take?
737  pf = newPf("conf_andr_at", exprs, pfs);
738  }
739 
740  return newTheorem(d_em->falseExpr(), a, pf);
741 }
742 
743 Theorem
745  const Theorem& a_th,
746  const Theorem& l_th,
747  const Theorem& r_th) {
748  const Expr& andr_e(andr_th.getExpr());
749  if(CHECK_PROOFS) {
750  CHECK_SOUND(andr_e.getKind() == AND_R && a_th.refutes(andr_e[0]) &&
751  l_th.proves(andr_e[1]) && r_th.proves(andr_e[2]),
752  "SearchEngineTheoremProducer::confAndrAF");
753  }
754 
755  Assumptions a;
756  Proof pf;
757  if(withAssumptions()) {
758  a.add(andr_th);
759  a.add(a_th);
760  a.add(l_th);
761  a.add(r_th);
762  }
763 
764  if(withProof()) {
765  vector<Proof> pfs;
766  vector<Expr> exprs;
767  exprs.push_back(andr_th.getExpr());
768  exprs.push_back(a_th.getExpr());
769  exprs.push_back(l_th.getExpr());
770  exprs.push_back(r_th.getExpr());
771  pfs.push_back(andr_th.getProof());
772  pfs.push_back(a_th.getProof());
773  pfs.push_back(l_th.getProof());
774  pfs.push_back(r_th.getProof());
775  pf = newPf("conf_andr_af", exprs, pfs);
776  }
777 
778  return newTheorem(d_em->falseExpr(), a, pf);
779 }
780 
781 Theorem
783  int p,
784  const Theorem& a_th,
785  const Theorem& b_th)
786 {
787  int a(-1), b(-1);
788  if(CHECK_PROOFS)
789  CHECK_SOUND(p == 0 || p == 1 || p == 2,
790  "SearchEngineTheoremProducer::propIffr: p="
791  +int2string(p));
792  switch (p) {
793  case 0: a = 1; b = 2; break;
794  case 1: a = 0; b = 2; break;
795  case 2: a = 0; b = 1; break;
796  }
797 
798  const Expr& iffr_e(iffr_th.getExpr());
799 
800  bool v0 = a_th.proves(iffr_e[a]);
801  bool v1 = b_th.proves(iffr_e[b]);
802 
803  if (CHECK_PROOFS) {
804  CHECK_SOUND(iffr_e.getKind() == IFF_R &&
805  (v0 || a_th.refutes(iffr_e[a])) &&
806  (v1 || b_th.refutes(iffr_e[b])),
807  "SearchEngineTheoremProducer::propIffr");
808  }
809 
810  Assumptions aa;
811  Proof pf;
812  if (withAssumptions()) {
813  aa.add(iffr_th);
814  aa.add(a_th);
815  aa.add(b_th);
816  }
817 
818  if (withProof()) {
819  vector<Proof> pfs;
820  vector<Expr> exprs;
821  exprs.push_back(iffr_th.getExpr());
822  exprs.push_back(a_th.getExpr());
823  exprs.push_back(b_th.getExpr());
824  pfs.push_back(iffr_th.getProof());
825  pfs.push_back(a_th.getProof());
826  pfs.push_back(b_th.getProof());
827  pf = newPf("prop_iffr", exprs, pfs);
828  }
829 
830  return newTheorem(v0 == v1 ? iffr_e[p] : iffr_e[p].negate(), aa, pf);
831 }
832 
833 Theorem
835  const Theorem& i_th,
836  const Theorem& l_th,
837  const Theorem& r_th)
838 {
839  const Expr& iffr_e(iffr_th.getExpr());
840 
841  bool v0 = i_th.proves(iffr_e[0]);
842  bool v1 = l_th.proves(iffr_e[1]);
843  bool v2 = r_th.proves(iffr_e[2]);
844 
845  if (CHECK_PROOFS) {
846  CHECK_SOUND(iffr_e.getKind() == IFF_R &&
847  (v0 || i_th.refutes(iffr_e[0])) &&
848  (v1 || l_th.refutes(iffr_e[1])) &&
849  (v2 || r_th.refutes(iffr_e[2])) &&
850  ((v0 && v1 != v2) || (!v0 && v1 == v2)),
851  "SearchEngineTheoremProducer::confIffr");
852  }
853 
854  Assumptions a;
855  Proof pf;
856  if (withAssumptions()) {
857  a.add(iffr_th);
858  a.add(i_th);
859  a.add(l_th);
860  a.add(r_th);
861  }
862 
863  if (withProof()) {
864  vector<Proof> pfs;
865  vector<Expr> exprs;
866  exprs.push_back(iffr_th.getExpr());
867  exprs.push_back(i_th.getExpr());
868  exprs.push_back(l_th.getExpr());
869  exprs.push_back(r_th.getExpr());
870  pfs.push_back(iffr_th.getProof());
871  pfs.push_back(i_th.getProof());
872  pfs.push_back(l_th.getProof());
873  pfs.push_back(r_th.getProof());
874  pf = newPf("conf_iffr", exprs, pfs);
875  }
876 
877  return newTheorem(d_em->falseExpr(), a, pf);
878 }
879 
880 Theorem
882  bool left,
883  const Theorem& if_th,
884  const Theorem& then_th)
885 {
886  const Expr& iter_e(iter_th.getExpr());
887 
888  bool v0 = if_th.proves(iter_e[1]);
889  bool v1 = then_th.proves(iter_e[left ? 2 : 3]);
890 
891  if (CHECK_PROOFS) {
892  CHECK_SOUND(iter_e.getKind() == ITE_R &&
893  (v0 || if_th.refutes(iter_e[1])) &&
894  (v1 || then_th.refutes(iter_e[left ? 2 : 3])) &&
895  v0 == left,
896  "SearchEngineTheoremProducer::propIterIte");
897  }
898 
899  Assumptions a;
900  Proof pf;
901  if (withAssumptions()) {
902  a.add(iter_th);
903  a.add(if_th);
904  a.add(then_th);
905  }
906 
907  if (withProof()) {
908  vector<Proof> pfs;
909  vector<Expr> exprs;
910  exprs.push_back(iter_th.getExpr());
911  exprs.push_back(if_th.getExpr());
912  exprs.push_back(then_th.getExpr());
913  pfs.push_back(iter_th.getProof());
914  pfs.push_back(if_th.getProof());
915  pfs.push_back(then_th.getProof());
916  pf = newPf("prop_iter_ite", exprs, pfs);
917  }
918 
919  return newTheorem(v1 ? iter_e[0] : iter_e[0].negate(), a, pf);
920 }
921 
922 void
924  bool left,
925  const Theorem& ite_th,
926  const Theorem& then_th,
927  Theorem* if_th,
928  Theorem* else_th)
929 {
930  const Expr& iter_e(iter_th.getExpr());
931 
932  bool v0 = ite_th.proves(iter_e[0]);
933  bool v1 = then_th.proves(iter_e[left ? 2 : 3]);
934 
935  if (CHECK_PROOFS) {
936  CHECK_SOUND(iter_e.getKind() == ITE_R &&
937  (v0 || ite_th.refutes(iter_e[0])) &&
938  (v1 || then_th.refutes(iter_e[left ? 2 : 3])) &&
939  v0 != v1,
940  "SearchEngineTheoremProducer::propIterIfThen");
941  }
942 
943  Assumptions a;
944  Proof pf;
945  if (withAssumptions()) {
946  a.add(iter_th);
947  a.add(ite_th);
948  a.add(then_th);
949  }
950 
951  if (withProof()) {
952  vector<Proof> pfs;
953  vector<Expr> exprs;
954  exprs.push_back(iter_th.getExpr());
955  exprs.push_back(ite_th.getExpr());
956  exprs.push_back(then_th.getExpr());
957  pfs.push_back(iter_th.getProof());
958  pfs.push_back(ite_th.getProof());
959  pfs.push_back(then_th.getExpr());
960  pf = newPf("prop_iter_if_then", exprs, pfs);
961  }
962 
963  if (if_th)
964  *if_th = newTheorem(left ? iter_e[1].negate() : iter_e[1], a, pf);
965  if (else_th)
966  *else_th = newTheorem(v0 ? iter_e[left ? 3 : 2] : iter_e[left ? 3 : 2].negate(), a, pf);
967 }
968 
969 Theorem
971  const Theorem& ite_th,
972  const Theorem& if_th)
973 {
974  const Expr& iter_e(iter_th.getExpr());
975 
976  bool v0 = ite_th.proves(iter_e[0]);
977  bool v1 = if_th.proves(iter_e[1]);
978 
979  if (CHECK_PROOFS) {
980  CHECK_SOUND(iter_e.getKind() == ITE_R &&
981  (v0 || ite_th.refutes(iter_e[0])) &&
982  (v1 || if_th.refutes(iter_e[1])),
983  "SearchEngineTheoremProducer::propIterThen");
984  }
985 
986  Assumptions a;
987  Proof pf;
988  if (withAssumptions()) {
989  a.add(iter_th);
990  a.add(ite_th);
991  a.add(if_th);
992  }
993 
994  if (withProof()) {
995  vector<Proof> pfs;
996  vector<Expr> exprs;
997  exprs.push_back(iter_th.getExpr());
998  exprs.push_back(ite_th.getExpr());
999  exprs.push_back(if_th.getExpr());
1000  pfs.push_back(iter_th.getProof());
1001  pfs.push_back(ite_th.getProof());
1002  pfs.push_back(if_th.getExpr());
1003  pf = newPf("prop_iter_then", exprs, pfs);
1004  }
1005 
1006  return newTheorem(v1 ?
1007  (v0 ? iter_e[2] : iter_e[2].negate()) :
1008  (v0 ? iter_e[3] : iter_e[3].negate()), a, pf);
1009 }
1010 
1011 Theorem
1013  const Theorem& ite_th,
1014  const Theorem& then_th,
1015  const Theorem& else_th)
1016 {
1017  const Expr& iter_e(iter_th.getExpr());
1018 
1019  bool v0 = ite_th.proves(iter_e[0]);
1020  bool v1 = then_th.proves(iter_e[2]);
1021  bool v2 = else_th.proves(iter_e[3]);
1022 
1023  if (CHECK_PROOFS) {
1024  CHECK_SOUND(iter_e.getKind() == ITE_R &&
1025  (v0 || ite_th.refutes(iter_e[0])) &&
1026  (v1 || then_th.refutes(iter_e[2])) &&
1027  (v2 || else_th.refutes(iter_e[3])) &&
1028  ((v0 && !v1 && !v2) || (!v0 && v1 && v2)),
1029  "SearchEngineTheoremProducer::confIterThenElse");
1030  }
1031 
1032  Assumptions a;
1033  Proof pf;
1034  if (withAssumptions()) {
1035  a.add(iter_th);
1036  a.add(ite_th);
1037  a.add(then_th);
1038  a.add(else_th);
1039  }
1040 
1041  if (withProof()) {
1042  vector<Proof> pfs;
1043  vector<Expr> exprs;
1044  exprs.push_back(iter_th.getExpr());
1045  exprs.push_back(ite_th.getExpr());
1046  exprs.push_back(then_th.getExpr());
1047  exprs.push_back(else_th.getExpr());
1048  pfs.push_back(iter_th.getProof());
1049  pfs.push_back(ite_th.getProof());
1050  pfs.push_back(then_th.getExpr());
1051  pfs.push_back(else_th.getExpr());
1052  pf = newPf("conf_iter_then_else", exprs, pfs);
1053  }
1054 
1055  return newTheorem(d_em->falseExpr(), a, pf);
1056 }
1057 
1058 Theorem
1060  bool left,
1061  const Theorem& ite_th,
1062  const Theorem& if_th,
1063  const Theorem& then_th)
1064 {
1065  const Expr& iter_e(iter_th.getExpr());
1066 
1067  bool v0 = ite_th.proves(iter_e[0]);
1068  bool v1 = if_th.proves(iter_e[1]);
1069  bool v2 = then_th.proves(iter_e[left ? 2 : 3]);
1070 
1071  if (CHECK_PROOFS) {
1072  CHECK_SOUND(iter_e.getKind() == ITE_R &&
1073  (v0 || ite_th.refutes(iter_e[0])) &&
1074  (v1 || if_th.refutes(iter_e[1])) &&
1075  (v2 || then_th.refutes(iter_e[left ? 2 : 3])) &&
1076  v1 == left && v0 != v2,
1077  "SearchEngineTheoremProducer::confIterThenElse");
1078  }
1079 
1080  Assumptions a;
1081  Proof pf;
1082  if (withAssumptions()) {
1083  a.add(iter_th);
1084  a.add(ite_th);
1085  a.add(if_th);
1086  a.add(then_th);
1087  }
1088 
1089  if (withProof()) {
1090  vector<Proof> pfs;
1091  vector<Expr> exprs;
1092  exprs.push_back(iter_th.getExpr());
1093  exprs.push_back(ite_th.getExpr());
1094  exprs.push_back(if_th.getExpr());
1095  exprs.push_back(then_th.getExpr());
1096  pfs.push_back(iter_th.getProof());
1097  pfs.push_back(ite_th.getProof());
1098  pfs.push_back(if_th.getExpr());
1099  pfs.push_back(then_th.getExpr());
1100  pf = newPf("conf_iter_then_else", exprs, pfs);
1101  }
1102 
1103  return newTheorem(d_em->falseExpr(), a, pf);
1104 }
1105 
1106 // "Conflict" rule (all literals in a clause become FALSE)
1107 // { G_j |- !l_j, j in [1..n] } , G |- (OR l_1 ... l_n) ==> FALSE
1108 Theorem
1109 SearchEngineTheoremProducer::conflictRule(const std::vector<Theorem>& thms,
1110  const Theorem& clause) {
1111  Expr e(clause.getExpr());
1112  if(CHECK_PROOFS) {
1113  // Soundness check: first, check the form of the 'clause' theorem
1114  CHECK_SOUND(e.isOr(),
1115  "SearchEngineTheoremProducer::unitProp: "
1116  "bad theorem in clause = "+clause.toString());
1117  // Now, check correspondence of thms to the disjunction
1118  CHECK_SOUND(((int)thms.size()) == e.arity(),
1119  "SearchEngineTheoremProducer::conflictRule: "
1120  "wrong number of theorems"
1121  "\n thms.size = " + int2string(thms.size())
1122  +"\n clause.arity = " + int2string(e.arity()));
1123 
1124  for(unsigned j=0; j<thms.size(); j++) {
1125  Expr ej(e[j]), ek(thms[j].getExpr());
1126  CHECK_SOUND((ej.isNot() && ej[0] == ek) || (ek.isNot() && ej == ek[0]),
1127  "SearchEngineTheoremProducer::conflictRule: "
1128  "wrong theorem["+int2string(j)+"]"
1129  "\n thm = " + thms[j].toString() +
1130  "\n literal = " + e[j].toString() +
1131  "\n clause = " + clause.toString());
1132  }
1133  }
1134 
1135  Assumptions a(thms);
1136  a.add(clause);
1137  Proof pf;
1138  if(withProof()) {
1139  vector<Proof> pfs;
1140  vector<Expr> exprs;
1141  exprs.reserve(thms.size() + 1);
1142  pfs.reserve(thms.size()+1);
1143  const vector<Theorem>::const_iterator iend = thms.end();
1144  for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
1145  exprs.push_back(i->getExpr());
1146  pfs.push_back(i->getProof());
1147  }
1148  exprs.push_back(clause.getExpr());
1149  pfs.push_back(clause.getProof());
1150  pf = newPf("conflict", exprs, pfs);
1151  }
1152  return newTheorem(d_em->falseExpr(), a, pf);
1153 }
1154 
1155 
1156 ///////////////////////////////////////////////////////////////////////
1157 //// Conjunctive Normal Form (CNF) proof rules
1158 ///////////////////////////////////////////////////////////////////////
1159 Theorem
1161  return opCNFRule(thm, AND, "and_cnf_rule");
1162 }
1163 
1164 Theorem
1166  return opCNFRule(thm, OR, "or_cnf_rule");
1167 }
1168 
1169 Theorem
1171  return opCNFRule(thm, IMPLIES, "implies_cnf_rule");
1172 }
1173 
1174 Theorem
1176  return opCNFRule(thm, IFF, "iff_cnf_rule");
1177 }
1178 
1179 Theorem
1181  return opCNFRule(thm, ITE, "ite_cnf_rule");
1182 }
1183 
1184 
1185 Theorem
1187  const Expr& iteExpr = ite.getExpr();
1188 
1189  if(CHECK_PROOFS) {
1190  CHECK_SOUND(iteExpr.isITE() && iteExpr.getType().isBool(),
1191  "SearchEngineTheoremProducer::iteToClauses("+iteExpr.toString()
1192  +")\n Argument must be a Boolean ITE");
1193  }
1194  const Expr& cond = iteExpr[0];
1195  const Expr& t1 = iteExpr[1];
1196  const Expr& t2 = iteExpr[2];
1197 
1198  Proof pf;
1199  if(withProof())
1200  pf = newPf("ite_to_clauses", iteExpr, ite.getProof());
1201  return newTheorem((cond.negate() || t1) && (cond || t2), ite.getAssumptionsRef(), pf);
1202 }
1203 
1204 
1205 Theorem
1207  if(CHECK_PROOFS) {
1208  CHECK_SOUND(iff.isRewrite() && iff.getLHS().getType().isBool(),
1209  "SearchEngineTheoremProducer::iffToClauses("+iff.getExpr().toString()
1210  +")\n Argument must be a Boolean IFF");
1211  }
1212  const Expr& t1 = iff.getLHS();
1213  const Expr& t2 = iff.getRHS();
1214 
1215  Proof pf;
1216  if(withProof())
1217  pf = newPf("iff_to_clauses", iff.getExpr(), iff.getProof());
1218  return newTheorem((t1.negate() || t2) && (t1 || t2.negate()), iff.getAssumptionsRef(), pf);
1219 }
1220 
1221 
1222 /////////////////////////////////////////////////////////////////////////
1223 //// helper functions for CNF (Conjunctive Normal Form) conversion
1224 /////////////////////////////////////////////////////////////////////////
1225 Theorem
1227  int kind,
1228  const string& ruleName) {
1229  TRACE("mycnf", "opCNFRule["+d_em->getKindName(kind)+"](",
1230  thm.getExpr(), ") {");
1231  ExprMap<Expr> localCache;
1232  if(CHECK_PROOFS) {
1233  Expr phiIffVar = thm.getExpr();
1234  CHECK_SOUND(phiIffVar.isIff(),
1235  "SearchEngineTheoremProducer::opCNFRule("
1236  +d_em->getKindName(kind)+"): "
1237  "input must be an IFF: thm = " + phiIffVar.toString());
1238  CHECK_SOUND(phiIffVar[0].getKind() == kind,
1239  "SearchEngineTheoremProducer::opCNFRule("
1240  +d_em->getKindName(kind)+"): "
1241  "input phi has wrong kind: thm = " + phiIffVar.toString());
1242  CHECK_SOUND(phiIffVar[0] != phiIffVar[1],
1243  "SearchEngineTheoremProducer::opCNFRule("
1244  +d_em->getKindName(kind)+"): "
1245  "wrong input thm = " + phiIffVar.toString());
1246  for(Expr::iterator it=phiIffVar[0].begin(), itend=phiIffVar[0].end();
1247  it!=itend;++it){
1248  CHECK_SOUND(phiIffVar[1] != *it,
1249  "SearchEngineTheoremProducer::opCNFRule("
1250  +d_em->getKindName(kind)+"): "
1251  "wrong input thm = " + phiIffVar.toString());
1252  }
1253  }
1254  const Expr& phi = thm.getExpr()[0];
1255  const Expr& phiVar = thm.getExpr()[1];
1256 
1257  std::vector<Expr> boundVars;
1258  std::vector<Expr> boundVarsAndLiterals;
1259  std::vector<Expr> equivs;
1260  for(Expr::iterator i=phi.begin(), iend=phi.end(); i != iend; i++) {
1261  // First, strip the negation and check if the formula is atomic
1262  Expr tmp(*i);
1263  while(tmp.isNot())
1264  tmp = tmp[0];
1265 
1266  if(tmp.isPropAtom())
1267  boundVarsAndLiterals.push_back(*i);
1268  else
1269  boundVarsAndLiterals.push_back(findInLocalCache(*i, localCache,
1270  boundVars));
1271  }
1272 
1273  for(ExprMap<Expr>::iterator it=localCache.begin(), itend=localCache.end();
1274  it != itend; it++) {
1275  DebugAssert((*it).second.isIff(),
1276  "SearchEngineTheoremProducer::opCNFRule: " +
1277  (*it).second.toString());
1278  DebugAssert(!(*it).second[0].isPropLiteral() &&
1279  (*it).second[1].isAbsLiteral(),
1280  "SearchEngineTheoremProducer::opCNFRule: " +
1281  (*it).second.toString());
1282  equivs.push_back((*it).second);
1283  }
1284 
1285  DebugAssert(boundVarsAndLiterals.size() == (unsigned)phi.arity(),
1286  "SearchEngineTheoremProducer::opCNFRule: "
1287  "wrong size of boundvars: phi = " + phi.toString());
1288 
1289  DebugAssert(boundVars.size() == equivs.size(),
1290  "SearchEngineTheoremProducer::opCNFRule: "
1291  "wrong size of boundvars: phi = " + phi.toString());
1292 
1293  Expr cnfInput = phi.arity() > 0 ? Expr(phi.getOp(), boundVarsAndLiterals) : phi;
1294  Expr result = convertToCNF(phiVar, cnfInput);
1295  if(boundVars.size() > 0)
1296  result =
1297  d_em->newClosureExpr(EXISTS, boundVars, result.andExpr(andExpr(equivs)));
1298 
1299  Proof pf;
1300  if(withProof())
1301  pf = newPf(ruleName, thm.getExpr(), thm.getProof());
1302  Theorem res(newTheorem(result, thm.getAssumptionsRef(), pf));
1303  TRACE("mycnf", "opCNFRule["+d_em->getKindName(kind)+"] => ", res.getExpr(),
1304  " }");
1305  return res;
1306 }
1307 
1308 //! produces the CNF for the formula v <==> phi
1310  //we assume that v \iff phi. v is the newVar corresponding to phi
1311 
1312  Expr::iterator i = phi.begin(), iend = phi.end();
1313  std::vector<Expr> clauses;
1314  std::vector<Expr> lastClause;
1315  switch(phi.getKind()) {
1316  case AND: {
1317  const Expr& negV = v.negate();
1318  lastClause.push_back(v);
1319  for(;i!=iend; ++i) {
1320  lastClause.push_back(i->negate());
1321  }
1322  clauses.push_back(orExpr(lastClause));
1323  }
1324  break;
1325  case OR:{
1326  lastClause.push_back(v.negate());
1327  for(;i!=iend; ++i) {
1328  clauses.push_back(v.orExpr(i->negate()));
1329  lastClause.push_back(*i);
1330  }
1331  clauses.push_back(orExpr(lastClause));
1332  }
1333  break;
1334  case IFF: {
1335  const Expr& v1 = phi[0];
1336  const Expr& v2 = phi[1];
1337  Expr negV = v.negate();
1338  Expr negv1 = v1.negate();
1339  Expr negv2 = v2.negate();
1340  clauses.push_back(Expr(OR, negV, negv1, v2));
1341  clauses.push_back(Expr(OR, negV, v1, negv2));
1342  clauses.push_back(Expr(OR, v, v1, v2));
1343  clauses.push_back(Expr(OR, v, negv1, negv2));
1344  } break;
1345  case IMPLIES:{
1346  const Expr& v1 = phi[0];
1347  const Expr& v2 = phi[1];
1348  Expr negV = v.negate();
1349  Expr negv1 = v1.negate();
1350  Expr negv2 = v2.negate();
1351  clauses.push_back(Expr(OR, negV, negv1, v2));
1352  clauses.push_back(v.orExpr(v1));
1353  clauses.push_back(v.orExpr(negv2));
1354  }
1355  break;
1356  case ITE: {
1357  const Expr& v1 = phi[0];
1358  const Expr& v2 = phi[1];
1359  const Expr& v3 = phi[2];
1360  const Expr& negV = v.negate();
1361  const Expr& negv1 = v1.negate();
1362  const Expr& negv2 = v2.negate();
1363  const Expr& negv3 = v3.negate();
1364  clauses.push_back(Expr(OR, negV, negv1, v2));
1365  clauses.push_back(Expr(OR, negV, v1, v3));
1366  clauses.push_back(Expr(OR, v, negv1, negv2));
1367  clauses.push_back(Expr(OR, v, v1, negv3));
1368  }
1369  break;
1370  default:
1371  DebugAssert(false, "SearchEngineTheoremProducer::convertToCNF: "
1372  "bad operator in phi = "+phi.toString());
1373  break;
1374  }
1375  return andExpr(clauses);
1376 }
1377 
1378 ///////////////////////////////////////////////////////////////////////
1379 // helper functions for CNF converters
1380 ///////////////////////////////////////////////////////////////////////
1381 
1383  ExprMap<Expr>& localCache,
1384  vector<Expr>& boundVars) {
1385  TRACE("mycnf", "findInLocalCache(", i.toString(), ") { ");
1386  Expr boundVar;
1387  unsigned int negationDepth = 0;
1389 
1390  Expr phi = i;
1391  while(phi.isNot()) {
1392  phi = phi[0];
1393  negationDepth++;
1394  }
1395 
1396  it = localCache.find(phi);
1397  Expr v;
1398  if(it != localCache.end()) {
1399  v = ((*it).second)[1];
1400  IF_DEBUG(debugger.counter("CNF Local Cache Hits")++;)
1401  }
1402  else {
1403  v = d_em->newBoundVarExpr(i.getType());
1404  boundVars.push_back(v);
1405  localCache[phi] = phi.iffExpr(v);
1406  }
1407  if(negationDepth % 2 != 0)
1408  v = !v;
1409  TRACE("mycnf", "findInLocalCache => ", v, " }");
1410  return v;
1411 }
1412 
1413 
1414 
1415 // for LFSC proof style, by yeting
1416 
1417 
1418 // theorem for minisat generated proofs, by yeting
1420  Proof pf;
1421  if(withProof())
1422  pf = newPf("minisat_proof", queryExpr, satProof);
1423 
1424  if ((d_tm->getFlags()["lfsc-mode"]).getInt()!= 0)
1425  {
1426  // UNCOMMENT THIS FOR LFSC
1427 
1428  if(!lfsc_called){
1429  int lfscm = (d_tm->getFlags()["lfsc-mode"]).getInt();
1430  std::vector<Expr> assumps;
1431  search_engine->getUserAssumptions(assumps);
1432 
1433  Expr pf_expr = pf.getExpr()[2] ;
1434  if( lfscm == -1 ){
1435  cout << "CVC3 Proof: ";
1436  cout << pf.getExpr() << endl;
1437  }else{
1438  LFSCPrinter* lfsc_printer = new LFSCPrinter(pf_expr, queryExpr, assumps, lfscm, d_commonRules);
1439  lfsc_printer->print_LFSC(pf_expr);
1440  lfsc_called = true;
1441  exit( 0 );
1442  }
1443  }
1444 
1445  }
1446 
1447  return newTheorem(queryExpr, Assumptions::emptyAssump() , pf);
1448 }
1449 
1450 
1451 // LocalWords: clc
int arity() const
Definition: expr.h:1201
bool isIff() const
Definition: expr.h:424
virtual void propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)
iterator begin() const
Begin iterator.
Definition: expr.h:1211
void verifyConflict(const Theorem &thm, TheoremMap &m)
API to to a generic proof search engine.
Definition: search.h:50
virtual Theorem proofByContradiction(const Expr &a, const Theorem &pfFalse)
Proof by contradiction: .
Data structure of expressions in CVC3.
Definition: expr.h:133
Definition: kinds.h:75
Theorem newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)
Create a new theorem. See also newRWTheorem() and newReflTheorem()
virtual Theorem confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)
std::map< Theorem, bool, TheoremLess > TheoremMap
Definition: theorem.h:402
Abstract API to the proof search engine.
virtual Theorem eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)
void clearAllFlags() const
Clear the flag attribute in all the theorems.
Definition: theorem.cpp:422
Expr findInLocalCache(const Expr &i, ExprMap< Expr > &localCache, std::vector< Expr > &boundVars)
checks if phi has v in local cache of opCNFRule, if so reuse v.
bool empty() const
Definition: expr_map.h:305
bool isITE() const
Definition: expr.h:423
Theorem iffToClauses(const Theorem &iff)
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
iterator find(const Expr &e)
Definition: expr_map.h:194
void add(const std::vector< Theorem > &thms)
virtual Theorem propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)
virtual Theorem cutRule(const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)
Cut rule: .
Definition: kinds.h:84
bool isFalse() const
Definition: expr.h:355
virtual Theorem propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)
virtual Theorem propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)
bool isPropAtom() const
True iff expr is not a Bool connective.
Definition: expr.h:411
STL namespace.
Definition: kinds.h:85
iterator begin()
Definition: expr_map.h:190
bool proves(const Expr &e) const
Check if the flag attribute is set.
Definition: theorem.h:259
bool withProof()
Testing whether to generate proofs.
bool isBool() const
Definition: type.h:60
void print_LFSC(const Expr &pf_expr)
Definition: LFSCPrinter.cpp:26
#define DebugAssert(cond, str)
Definition: debug.h:408
#define CHECK_SOUND(cond, msg)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Definition: expr_manager.h:506
virtual Theorem caseSplit(const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)
Case split: .
#define CHECK_PROOFS
Theorem impCNFRule(const Theorem &thm)
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
bool withAssumptions()
Testing whether to generate assumptions.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool refutes(const Expr &e) const
Check if the flag attribute is set.
Definition: theorem.h:252
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
virtual void propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Definition: expr_manager.h:484
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
bool isNot() const
Definition: expr.h:420
size_t count(const Expr &e) const
Definition: expr_map.h:173
const std::string & getKindName(int kind)
Return the name associated with a kind. The kind must already be registered.
Definition: kinds.h:76
std::string toString() const
Definition: theorem.h:404
virtual Theorem unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)
Unit propagation rule: .
Expr getExpr() const
Definition: proof.h:46
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
TheoremManager * d_tm
static int left(int i)
Definition: minisat_heap.h:53
bool isFlagged() const
Check if the flag attribute is set.
Definition: theorem.cpp:416
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
const Expr & falseExpr()
FALSE Expr.
Definition: expr_manager.h:278
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
Expr negate() const
Definition: expr.h:937
Definition: kinds.h:68
int getKind() const
Definition: expr.h:1168
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
Proof newLabel(const Expr &e)
Create a new proof label (bound variable) for an assumption (formula)
const Expr & getRHS() const
Definition: theorem.cpp:246
Theorem orCNFRule(const Theorem &thm)
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
virtual Theorem conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)
"Conflict" rule (all literals in a clause become FALSE)
#define IF_DEBUG(code)
Definition: debug.h:406
virtual void getUserAssumptions(std::vector< Expr > &assumptions)=0
Get all user assumptions made in this and all previous contexts.
virtual Theorem confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Definition: kinds.h:71
Implementation API to proof rules for the simple search engine.
Expr getExpr() const
Definition: theorem.cpp:230
Theorem opCNFRule(const Theorem &thm, int kind, const std::string &ruleName)
Expr orExpr(const Expr &right) const
Definition: expr.h:951
Theorem iteToClauses(const Theorem &ite)
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual Theorem confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)
Definition: kinds.h:77
virtual Theorem conflictClause(const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)
Conflict clause rule: .
virtual Theorem propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)
Theorem iteCNFRule(const Theorem &thm)
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
bool isVar() const
Definition: expr.h:1005
virtual Theorem confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)
bool isRefl() const
Definition: theorem.h:171
const Expr & getLHS() const
Definition: theorem.cpp:240
Iterator for the Assumptions: points to class Theorem.
Definition: assumptions.h:118
Definition: kinds.h:81
API to the proof rules for the Search Engines.
Definition: search_rules.h:35
Proof newPf(const std::string &name)
const CLFlags & getFlags() const
virtual Theorem propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)
Definition: expr.cpp:35
Definition: kinds.h:99
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool isRewrite() const
Definition: theorem.cpp:224
bool isAssump() const
Definition: theorem.cpp:395
Theorem iffCNFRule(const Theorem &thm)
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Theorem satProof(const Expr &queryExpr, const Proof &satProof)
bool lfsc_called
static const Assumptions & emptyAssump()
Definition: assumptions.h:83
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
iterator end()
Definition: expr_map.h:191
virtual Theorem propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)
Definition: kinds.h:67
SearchEngine * search_engine
virtual Theorem negIntro(const Expr &not_a, const Theorem &pfFalse)
Negation introduction: .
virtual Theorem propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)
Expr convertToCNF(const Expr &v, const Expr &phi)
produces the CNF for the formula v <==> phi
Definition: kinds.h:70
void setFlag() const
Set the flag attribute.
Definition: theorem.cpp:429
void checkSoundNoSkolems(const Expr &e, ExprMap< bool > &visited, const ExprMap< bool > &skolems)
Theorem andCNFRule(const Theorem &thm)
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
virtual Theorem confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)
iterator end() const
End iterator.
Definition: expr.h:1217