1 /*****************************************************************************/
2 /*!
3 *\file common_theorem_producer.cpp
4 *\brief Implementation of common proof rules
5 *
6 * Author: Clark Barrett
7 *
8 * Created: Wed Jan 11 16:10:15 2006
9 *
10 * <hr>
11 *
12 * License to use, copy, modify, sell and/or distribute this software
13 * and its documentation for any purpose is hereby granted without
14 * royalty, subject to the terms and conditions defined in the \ref
15 * LICENSE file provided with this distribution.
16 *
17 * <hr>
18 *
19 */
20 /*****************************************************************************/
21
22
23 // This code is trusted
24 #define _CVC3_TRUSTED_
25
26
27 #include "common_theorem_producer.h"
28
29
30 using namespace CVC3;
31 using namespace std;
32
33
34 // The trusted method of TheoremManager which creates this theorem producer
createProofRules()35 CommonProofRules* TheoremManager::createProofRules() {
36 return new CommonTheoremProducer(this);
37 }
38
39
CommonTheoremProducer(TheoremManager * tm)40 CommonTheoremProducer::CommonTheoremProducer(TheoremManager* tm)
41 : TheoremProducer(tm),
42 d_skolemized_thms(tm->getCM()->getCurrentContext()),
43 d_skolemVars(tm->getCM()->getCurrentContext())
44 {}
45
46
47 ////////////////////////////////////////////////////////////////////////
48 // TCC rules (3-valued logic)
49 ////////////////////////////////////////////////////////////////////////
50
51 // G1 |- phi G2 |- D_phi
52 // -------------------------
53 // G1,G2 |-_3 phi
54 Theorem3
queryTCC(const Theorem & phi,const Theorem & D_phi)55 CommonTheoremProducer::queryTCC(const Theorem& phi, const Theorem& D_phi) {
56 Proof pf;
57 // if(CHECK_PROOFS)
58 // CHECK_SOUND(D_phi.getExpr() == d_core->getTCC(phi.getExpr()),
59 // "CoreTheoremProducer::queryTCC: "
60 // "bad TCC for a formula:\n\n "
61 // +phi.getExpr().toString()
62 // +"\n\n TCC must be the following:\n\n "
63 // +d_core->getTCC(phi.getExpr()).toString()
64 // +"\n\nBut given this as a TCC:\n\n "
65 // +D_phi.getExpr().toString());
66 Assumptions a = phi.getAssumptionsRef();
67 a.add(D_phi);
68 if(withProof()) {
69 vector<Expr> args;
70 vector<Proof> pfs;
71 args.push_back(phi.getExpr());
72 args.push_back(D_phi.getExpr());
73 pfs.push_back(phi.getProof());
74 pfs.push_back(D_phi.getProof());
75 pf = newPf("queryTCC", args, pfs);
76 }
77 return newTheorem3(phi.getExpr(), a, pf);
78 }
79
80
81 // G0,a1,...,an |-_3 phi G1 |- D_a1 ... Gn |- D_an
82 // -------------------------------------------------
83 // G0,G1,...,Gn |-_3 (a1 & ... & an) -> phi
84 Theorem3
implIntro3(const Theorem3 & phi,const std::vector<Expr> & assump,const vector<Theorem> & tccs)85 CommonTheoremProducer::implIntro3(const Theorem3& phi,
86 const std::vector<Expr>& assump,
87 const vector<Theorem>& tccs) {
88 bool checkProofs(CHECK_PROOFS);
89 // This rule only makes sense when runnnig with assumptions
90 if(checkProofs) {
91 CHECK_SOUND(withAssumptions(),
92 "implIntro3: called while running without assumptions");
93 }
94
95 const Assumptions& phiAssump = phi.getAssumptionsRef();
96
97 if(checkProofs) {
98 CHECK_SOUND(assump.size() == tccs.size(),
99 "implIntro3: number of assumptions ("
100 +int2string(assump.size())+") and number of TCCs ("
101 +int2string(tccs.size())
102 +") does not match");
103 for(size_t i=0; i<assump.size(); i++) {
104 const Theorem& thm = phiAssump[assump[i]];
105 CHECK_SOUND(!thm.isNull() && thm.isAssump(),
106 "implIntro3: this is not an assumption of phi:\n\n"
107 " a["+int2string(i)+"] = "+assump[i].toString()
108 +"\n\n phi = "+phi.getExpr().toString());
109 // CHECK_SOUND(tccs[i].getExpr() == d_core->getTCC(assump[i]),
110 // "implIntro3: Assumption does not match its TCC:\n\n"
111 // " a["+int2string(i)+"] = "+assump[i].toString()
112 // +" TCC(a["+int2string(i)+"]) = "
113 // +d_core->getTCC(assump[i]).toString()
114 // +"\n\n tccs["+int2string(i)+"] = "
115 // +tccs[i].getExpr().toString());
116 }
117 }
118
119 // Proof compaction: trivial derivation
120 if(assump.size() == 0) return phi;
121
122 Assumptions a(phiAssump - assump);
123 Assumptions b(tccs);
124 a.add(b);
125 Proof pf;
126 if(withProof()) {
127 vector<Proof> u; // Proof labels for assumptions
128 for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
129 i!=iend; ++i) {
130 const Theorem& t = phiAssump[*i];
131 u.push_back(t.getProof());
132 }
133 // Arguments to the proof rule:
134 // impl_intro_3(phi, a1,...,an,tcc1,...tccn,pf_tcc1,...pf_tccn,
135 // [lambda(a1,...,an): pf_phi])
136 vector<Expr> args;
137 vector<Proof> pfs;
138 args.push_back(phi.getExpr());
139 args.insert(args.end(), assump.begin(), assump.end());
140 for(vector<Theorem>::const_iterator i=tccs.begin(), iend=tccs.end();
141 i!=iend; ++i) {
142 args.push_back(i->getExpr());
143 pfs.push_back(i->getProof());
144 }
145 // Lambda-abstraction of pf_phi
146 pfs.push_back(newPf(u, assump, phi.getProof()));
147 pf = newPf("impl_intro_3", args, pfs);
148 }
149 Expr conj(andExpr(assump));
150 return newTheorem3(conj.impExpr(phi.getExpr()), a, pf);
151 }
152
153
assumpRule(const Expr & e,int scope)154 Theorem CommonTheoremProducer::assumpRule(const Expr& e, int scope) {
155 // TRACE("assump", "assumpRule(", e, ")");
156 Proof pf;
157 if(withProof()) pf = newLabel(e);
158 return newAssumption(e, pf, scope);
159 }
160
161
reflexivityRule(const Expr & a)162 Theorem CommonTheoremProducer::reflexivityRule(const Expr& a) {
163 return newReflTheorem(a);
164 }
165
166
167 // ==> (a == a) IFF TRUE
rewriteReflexivity(const Expr & t)168 Theorem CommonTheoremProducer::rewriteReflexivity(const Expr& t) {
169 if(CHECK_PROOFS)
170 CHECK_SOUND((t.isEq() || t.isIff()) && t[0] == t[1],
171 "rewriteReflexivity: wrong expression: "
172 + t.toString());
173 Proof pf;
174 if(withProof()) {
175 if(t.isEq()) {
176 DebugAssert(!t[0].getType().isNull(),
177 "rewriteReflexivity: t[0] has no type: "
178 + t[0].toString());
179 pf = newPf("rewrite_eq_refl", t[0].getType().getExpr(), t[0]);
180 } else
181 pf = newPf("rewrite_iff_refl", t[0]);
182 }
183 return newRWTheorem(t, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
184 }
185
186
symmetryRule(const Theorem & a1_eq_a2)187 Theorem CommonTheoremProducer::symmetryRule(const Theorem& a1_eq_a2) {
188 if(CHECK_PROOFS)
189 CHECK_SOUND(a1_eq_a2.isRewrite(),
190 ("CVC3::CommonTheoremProducer: "
191 "theorem is not an equality or iff:\n "
192 + a1_eq_a2.getExpr().toString()).c_str());
193 const Expr& a1 = a1_eq_a2.getLHS();
194 const Expr& a2 = a1_eq_a2.getRHS();
195
196 Proof pf;
197 /////////////////////////////////////////////////////////////////////////
198 //// Proof compaction
199 /////////////////////////////////////////////////////////////////////////
200 // If a1 == a2, use reflexivity
201 if(a1 == a2) return reflexivityRule(a1);
202 // Otherwise, do the work
203 if(withProof()) {
204 Type t = a1.getType();
205 // Check the types
206 IF_DEBUG(a1_eq_a2.getExpr().getType();)
207 bool isEquality = !t.isBool();
208 if(isEquality) {
209 vector<Expr> args;
210 args.push_back(t.getExpr());
211 args.push_back(a1);
212 args.push_back(a2);
213 pf = newPf("eq_symm", args, a1_eq_a2.getProof());
214 } else
215 pf = newPf("iff_symm", a1, a2, a1_eq_a2.getProof());
216 }
217 return newRWTheorem(a2, a1, Assumptions(a1_eq_a2), pf);
218 }
219
220
rewriteUsingSymmetry(const Expr & a1_eq_a2)221 Theorem CommonTheoremProducer::rewriteUsingSymmetry(const Expr& a1_eq_a2) {
222 bool isIff = a1_eq_a2.isIff();
223 if(CHECK_PROOFS)
224 CHECK_SOUND(a1_eq_a2.isEq() || isIff, "rewriteUsingSymmetry precondition violated");
225 const Expr& a1 = a1_eq_a2[0];
226 const Expr& a2 = a1_eq_a2[1];
227 // Proof compaction: if a1 == a2, use reflexivity
228 if(a1 == a2) return reflexivityRule(a1_eq_a2);
229 // Otherwise, do the work
230 Proof pf;
231 if(withProof()) {
232 Type t = a1.getType();
233 DebugAssert(!t.isNull(),
234 "rewriteUsingSymmetry: a1 has no type: " + a1.toString());
235 if(isIff)
236 pf = newPf("rewrite_iff_symm", a1, a2);
237 else {
238 pf = newPf("rewrite_eq_symm", t.getExpr(), a1, a2);
239 }
240 }
241 return newRWTheorem(a1_eq_a2, isIff ? a2.iffExpr(a1) : a2.eqExpr(a1), Assumptions::emptyAssump(), pf);
242 }
243
244
transitivityRule(const Theorem & a1_eq_a2,const Theorem & a2_eq_a3)245 Theorem CommonTheoremProducer::transitivityRule(const Theorem& a1_eq_a2,
246 const Theorem& a2_eq_a3) {
247 DebugAssert(!a1_eq_a2.isNull(), "transitivityRule()");
248 DebugAssert(!a2_eq_a3.isNull(), "transitivityRule()");
249 if(CHECK_PROOFS) {
250 CHECK_SOUND(a1_eq_a2.isRewrite() && a2_eq_a3.isRewrite(),
251 "CVC3::CommonTheoremProducer::transitivityRule:\n "
252 "Wrong premises: first = "
253 + a1_eq_a2.getExpr().toString() + ", second = "
254 + a2_eq_a3.getExpr().toString());
255 CHECK_SOUND(a1_eq_a2.getRHS() == a2_eq_a3.getLHS(),
256 "CVC3::CommonTheoremProducer::transitivityRule:\n "
257 "Wrong premises: first = "
258 + a1_eq_a2.getExpr().toString() + ", second = "
259 + a2_eq_a3.getExpr().toString());
260 }
261 const Expr& a1 = a1_eq_a2.getLHS();
262 const Expr& a2 = a1_eq_a2.getRHS();
263 const Expr& a3 = a2_eq_a3.getRHS();
264
265 /////////////////////////////////////////////////////////////////////////
266 //// Proof compaction
267 /////////////////////////////////////////////////////////////////////////
268 // if a1 == a3, use reflexivity (and lose all assumptions)
269 if(a1 == a3) return reflexivityRule(a1);
270 // if a1 == a2, or if a2 == a3, use only the non-trivial part
271 if(a1 == a2) return a2_eq_a3;
272 if(a2 == a3) return a1_eq_a2;
273
274 ////////////////////////////////////////////////////////////////////////
275 //// No shortcuts. Do the work.
276 ////////////////////////////////////////////////////////////////////////
277
278 Proof pf;
279 Assumptions a(a1_eq_a2, a2_eq_a3);
280 // Build the proof
281 if(withProof()) {
282 Type t = a1.getType();
283 bool isEquality = (!t.isBool());
284 string name((isEquality)? "eq_trans" : "iff_trans");
285 vector<Expr> args;
286 vector<Proof> pfs;
287 DebugAssert(!t.isNull(), "transitivityRule: "
288 "Type is not computed for a1: " + a1.toString());
289 // Type argument is needed only for equality
290 if(isEquality) args.push_back(t.getExpr());
291 args.push_back(a1);
292 args.push_back(a2);
293 args.push_back(a3);
294 pfs.push_back(a1_eq_a2.getProof());
295 pfs.push_back(a2_eq_a3.getProof());
296 pf = newPf(name, args, pfs);
297 }
298 return newRWTheorem(a1, a3, a, pf);
299 }
300
301
substitutivityRule(const Expr & e,const Theorem & thm)302 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
303 const Theorem& thm) {
304 IF_DEBUG
305 (static DebugTimer
306 accum0(debugger.timer("substitutivityRule0 time"));
307 static DebugTimer tmpTimer(debugger.newTimer());
308 static DebugCounter count(debugger.counter("substitutivityRule0 calls"));
309 debugger.setCurrentTime(tmpTimer);
310 count++;)
311
312 // Check that t is c == d or c IFF d
313 if(CHECK_PROOFS) {
314 CHECK_SOUND(e.arity() == 1 && e[0] == thm.getLHS(),
315 "Unexpected use of substitutivityRule0");
316 CHECK_SOUND(thm.isRewrite(),
317 "CVC3::CommonTheoremProducer::substitutivityRule0:\n "
318 "premis is not an equality or IFF: "
319 + thm.getExpr().toString()
320 + "\n expr = " + e.toString());
321 }
322 Expr e2(e.getOp(), thm.getRHS());
323 Proof pf;
324 if(withProof())
325 pf = newPf("basic_subst_op0",e, e2,thm.getProof());
326 Theorem res = newRWTheorem(e, e2, Assumptions(thm), pf);
327 if (!res.isRefl()) res.setSubst();
328 return res;
329 }
330
331
substitutivityRule(const Expr & e,const Theorem & thm1,const Theorem & thm2)332 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
333 const Theorem& thm1,
334 const Theorem& thm2) {
335 IF_DEBUG
336 (static DebugTimer
337 accum0(debugger.timer("substitutivityRule1 time"));
338 static DebugTimer tmpTimer(debugger.newTimer());
339 static DebugCounter count(debugger.counter("substitutivityRule1 calls"));
340 debugger.setCurrentTime(tmpTimer);
341 count++;)
342
343 // Check that t is c == d or c IFF d
344 if(CHECK_PROOFS) {
345 CHECK_SOUND(e.arity() == 2 && e[0] == thm1.getLHS() &&
346 e[1] == thm2.getLHS(),
347 "Unexpected use of substitutivityRule1");
348 CHECK_SOUND(thm1.isRewrite(),
349 "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
350 "premis is not an equality or IFF: "
351 + thm1.getExpr().toString()
352 + "\n expr = " + e.toString());
353 CHECK_SOUND(thm2.isRewrite(),
354 "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
355 "premis is not an equality or IFF: "
356 + thm2.getExpr().toString()
357 + "\n expr = " + e.toString());
358 }
359 Expr e2(e.getOp(), thm1.getRHS(), thm2.getRHS());
360 Proof pf;
361 if(withProof()) {
362 vector<Proof> pfs;
363 pfs.push_back(thm1.getProof());
364 pfs.push_back(thm2.getProof());
365 pf = newPf("basic_subst_op1", e, e2, pfs);
366 }
367 Theorem res = newRWTheorem(e, e2, Assumptions(thm1, thm2), pf);
368 if (!res.isRefl()) res.setSubst();
369 return res;
370 }
371
372
substitutivityRule(const Op & op,const vector<Theorem> & thms)373 Theorem CommonTheoremProducer::substitutivityRule(const Op& op,
374 const vector<Theorem>& thms) {
375 IF_DEBUG
376 (static DebugTimer
377 accum0(debugger.timer("substitutivityRule time"));
378 static DebugTimer tmpTimer(debugger.newTimer());
379 static DebugCounter count(debugger.counter("substitutivityRule calls"));
380 debugger.setCurrentTime(tmpTimer);
381 count++;)
382 // Check for trivial case: no theorems, return (op == op)
383 unsigned size(thms.size());
384 if(size == 0)
385 return reflexivityRule(d_tm->getEM()->newLeafExpr(op));
386 // Check that theorems are of the form c_i == d_i and collect
387 // vectors of c_i's and d_i's and the vector of proofs
388 vector<Expr> c, d;
389 vector<Proof> pfs;
390 // Reserve memory for argument vectors. Do not reserve memory for
391 // pfs, they are rarely used and slow anyway.
392 c.reserve(size); d.reserve(size);
393 for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
394 i != iend; ++i) {
395 // Check that t is c == d or c IFF d
396 if(CHECK_PROOFS)
397 CHECK_SOUND(i->isRewrite(),
398 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
399 "premis is not an equality or IFF: "
400 + i->getExpr().toString()
401 + "\n op = " + op.toString());
402 // Collect the pieces
403 c.push_back(i->getLHS());
404 d.push_back(i->getRHS());
405 if(withProof()) pfs.push_back(i->getProof());
406 }
407 Expr e1(op, c), e2(op, d);
408 // Proof compaction: if e1 == e2, use reflexivity
409 if(e1 == e2) return reflexivityRule(e1);
410 // Otherwise, do the work
411 Assumptions a(thms);
412 Proof pf;
413 if(withProof())
414 // FIXME: this rule is not directly expressible in flea
415 pf = newPf("basic_subst_op",e1,e2,pfs);
416 Theorem res = newRWTheorem(e1, e2, a, pf);
417 IF_DEBUG(debugger.setElapsed(tmpTimer);
418 accum0 += tmpTimer;)
419 res.setSubst();
420 return res;
421 }
422
423
substitutivityRule(const Expr & e,const vector<unsigned> & changed,const vector<Theorem> & thms)424 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
425 const vector<unsigned>& changed,
426 const vector<Theorem>& thms) {
427 IF_DEBUG
428 (static DebugTimer
429 accum0(debugger.timer("substitutivityRule2 time"));
430 static DebugTimer tmpTimer(debugger.newTimer());
431 static DebugCounter count(debugger.counter("substitutivityRule2 calls"));
432 debugger.setCurrentTime(tmpTimer);
433 count++;)
434 DebugAssert(changed.size() > 0, "substitutivityRule2 should not be called");
435 DebugAssert(changed.size() == thms.size(), "substitutivityRule2: wrong args");
436
437 // Check that theorems are of the form c_i == d_i and collect
438 // vectors of c_i's and d_i's and the vector of proofs
439 unsigned size = e.arity();
440 if (size == 1) return substitutivityRule(e, thms.back());
441 unsigned csize = changed.size();
442 if (size == 2) {
443 if (csize == 2) return substitutivityRule(e, thms[0], thms[1]);
444 if (changed[0] == 0) {
445 return substitutivityRule(e, thms[0], reflexivityRule(e[1]));
446 }
447 else {
448 return substitutivityRule(e, reflexivityRule(e[0]), thms[0]);
449 }
450 }
451 DebugAssert(size >= csize, "Bad call to substitutivityRule2");
452
453 vector<Expr> c;
454 bool checkProofs(CHECK_PROOFS);
455 for(unsigned j = 0, k = 0; k < size; ++k) {
456 if (j == csize || changed[j] != k) {
457 c.push_back(e[k]);
458 continue;
459 }
460 // Check that t is c == d or c IFF d
461 if(checkProofs)
462 CHECK_SOUND(thms[j].isRewrite() && thms[j].getLHS() == e[k],
463 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
464 "premis is not an equality or IFF: "
465 + thms[j].getExpr().toString()
466 + "\n e = " + e.toString());
467 // Collect the pieces
468 c.push_back(thms[j].getRHS());
469 ++j;
470 }
471 Expr e2(e.getOp(), c);
472 IF_DEBUG(if(e == e2) {
473 ostream& os = debugger.getOS();
474 os << "substitutivityRule2: e = " << e << "\n e2 = " << e2
475 << "\n changed kids: [\n";
476 for(unsigned j=0; j<changed.size(); j++)
477 os << " (" << changed[j] << ") " << thms[j] << "\n";
478 os << "]\n";
479 })
480 DebugAssert(e != e2,
481 "substitutivityRule2 should not be called in this case:\n"
482 "e = "+e.toString());
483
484 Proof pf;
485 Assumptions a(thms);
486 if(withProof()) {
487 vector<Proof> pfs;
488 for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
489 i != iend; ++i) {
490 // Check that t is c == d or c IFF d
491 if(CHECK_PROOFS)
492 CHECK_SOUND(i->isRewrite(),
493 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
494 "premis is not an equality or IFF: "
495 + i->getExpr().toString());
496 // + "\n op = " + ((Op) e.getOp).toString());
497 pfs.push_back(i->getProof());
498 }
499 pf = newPf("optimized_subst_op",e,e2,pfs);
500 }
501 Theorem res = newRWTheorem(e, e2, a, pf);
502 IF_DEBUG(debugger.setElapsed(tmpTimer);
503 accum0 += tmpTimer;)
504 if (!res.isRefl()) res.setSubst();
505 return res;
506 }
507
508
substitutivityRule(const Expr & e,const int changed,const Theorem & thm)509 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
510 const int changed,
511 const Theorem& thm)
512 {
513 // Get the arity of the expression
514 int size = e.arity();
515
516 // The changed must be within the arity
517 DebugAssert(size >= changed, "Bad call to substitutivityRule");
518
519 // Check that t is c == d or c IFF d
520 if(CHECK_PROOFS)
521 CHECK_SOUND(thm.isRewrite() && thm.getLHS() == e[changed], "CVC3::CommonTheoremProducer::substitutivityRule:\n "
522 "premise is not an equality or IFF: " + thm.getExpr().toString() + "\n" +
523 "e = " + e.toString());
524
525 // Collect the new sub-expressions
526 vector<Expr> c;
527 for(int k = 0; k < size; ++ k)
528 if (k != changed) c.push_back(e[k]);
529 else c.push_back(thm.getRHS());
530
531 // Construct the new expression
532 Expr e2(e.getOp(), c);
533
534 // Check if they are the same
535 IF_DEBUG(if(e == e2) {
536 ostream& os = debugger.getOS();
537 os << "substitutivityRule: e = " << e << "\n e2 = " << e2 << endl;
538 })
539
540 // The new expressions must not be equal
541 DebugAssert(e != e2, "substitutivityRule should not be called in this case:\ne = "+e.toString());
542
543 // Construct the proof object
544 Proof pf;
545 Assumptions a(thm);
546 if(withProof()) {
547 // Check that t is c == d or c IFF d
548 if(CHECK_PROOFS)
549 CHECK_SOUND(thm.isRewrite(), "CVC3::CommonTheoremProducer::substitutivityRule:\npremise is not an equality or IFF: " + thm.getExpr().toString());
550 pf = newPf("optimized_subst_op2",e,e2,thm.getProof());
551 }
552
553 // Return the resulting theorem
554 Theorem res = newRWTheorem(e, e2, a, pf);;
555 res.setSubst();
556 return res;
557 }
558
559
560 // |- e, |- !e ==> |- FALSE
contradictionRule(const Theorem & e,const Theorem & not_e)561 Theorem CommonTheoremProducer::contradictionRule(const Theorem& e,
562 const Theorem& not_e) {
563 Proof pf;
564 if(CHECK_PROOFS)
565 CHECK_SOUND(!e.getExpr() == not_e.getExpr(),
566 "CommonTheoremProducer::contraditionRule: "
567 "theorems don't match:\n e = "+e.toString()
568 +"\n not_e = "+not_e.toString());
569 Assumptions a(e, not_e);
570 if(withProof()) {
571 vector<Proof> pfs;
572 pfs.push_back(e.getProof());
573 pfs.push_back(not_e.getProof());
574 pf = newPf("contradition", e.getExpr(), pfs);
575 }
576 return newTheorem(d_em->falseExpr(), a, pf);
577 }
578
579
excludedMiddle(const Expr & e)580 Theorem CommonTheoremProducer::excludedMiddle(const Expr& e)
581 {
582 Proof pf;
583 if (withProof()) {
584 pf = newPf("excludedMiddle", e);
585 }
586 return newTheorem(e.orExpr(!e), Assumptions::emptyAssump(), pf);
587 }
588
589
590 // e ==> e IFF TRUE
iffTrue(const Theorem & e)591 Theorem CommonTheoremProducer::iffTrue(const Theorem& e)
592 {
593 Proof pf;
594 if(withProof()) {
595 pf = newPf("iff_true", e.getExpr(), e.getProof());
596 }
597 return newRWTheorem(e.getExpr(), d_em->trueExpr(), Assumptions(e), pf);
598 }
599
600
601 // e ==> !e IFF FALSE
iffNotFalse(const Theorem & e)602 Theorem CommonTheoremProducer::iffNotFalse(const Theorem& e) {
603 Proof pf;
604 if(withProof()) {
605 pf = newPf("iff_not_false", e.getExpr(), e.getProof());
606 }
607 return newRWTheorem(!e.getExpr(), d_em->falseExpr(), Assumptions(e), pf);
608 }
609
610
611 // e IFF TRUE ==> e
iffTrueElim(const Theorem & e)612 Theorem CommonTheoremProducer::iffTrueElim(const Theorem& e) {
613 if(CHECK_PROOFS)
614 CHECK_SOUND(e.isRewrite() && e.getRHS().isTrue(),
615 "CommonTheoremProducer::iffTrueElim: "
616 "theorem is not e<=>TRUE: "+ e.toString());
617 Proof pf;
618 if(withProof()) {
619 pf = newPf("iff_true_elim", e.getLHS(), e.getProof());
620 }
621 return newTheorem(e.getLHS(), Assumptions(e), pf);
622 }
623
624
625 // e IFF FALSE ==> !e
iffFalseElim(const Theorem & e)626 Theorem CommonTheoremProducer::iffFalseElim(const Theorem& e) {
627 if(CHECK_PROOFS)
628 CHECK_SOUND(e.isRewrite() && e.getRHS().isFalse(),
629 "CommonTheoremProducer::iffFalseElim: "
630 "theorem is not e<=>FALSE: "+ e.toString());
631 const Expr& lhs = e.getLHS();
632 Proof pf;
633 if(withProof()) {
634 pf = newPf("iff_false_elim", lhs, e.getProof());
635 }
636 return newTheorem(!lhs, Assumptions(e), pf);
637 }
638
639
640 // e1 <=> e2 ==> ~e1 <=> ~e2
iffContrapositive(const Theorem & e)641 Theorem CommonTheoremProducer::iffContrapositive(const Theorem& e) {
642 if(CHECK_PROOFS)
643 CHECK_SOUND(e.isRewrite() && e.getRHS().getType().isBool(),
644 "CommonTheoremProducer::iffContrapositive: "
645 "theorem is not e1<=>e2: "+ e.toString());
646 Proof pf;
647 if(withProof()) {
648 pf = newPf("iff_contrapositive", e.getExpr(), e.getProof());
649 }
650 return newRWTheorem(e.getLHS().negate(),e.getRHS().negate(), Assumptions(e), pf);
651 }
652
653
654 // !!e ==> e
notNotElim(const Theorem & not_not_e)655 Theorem CommonTheoremProducer::notNotElim(const Theorem& not_not_e) {
656 if(CHECK_PROOFS)
657 CHECK_SOUND(not_not_e.getExpr().isNot() && not_not_e.getExpr()[0].isNot(),
658 "CommonTheoremProducer::notNotElim: bad theorem: !!e = "
659 + not_not_e.toString());
660 Proof pf;
661 if(withProof())
662 pf = newPf("not_not_elim", not_not_e.getExpr(), not_not_e.getProof());
663 return newTheorem(not_not_e.getExpr()[0][0], Assumptions(not_not_e), pf);
664 }
665
666
iffMP(const Theorem & e1,const Theorem & e1_iff_e2)667 Theorem CommonTheoremProducer::iffMP(const Theorem& e1, const Theorem& e1_iff_e2)
668 {
669 if(CHECK_PROOFS) {
670 CHECK_SOUND(e1_iff_e2.isRewrite(),
671 "iffMP: not IFF: "+e1_iff_e2.toString());
672 CHECK_SOUND(e1.getExpr() == (e1_iff_e2.getLHS()),
673 "iffMP: theorems don't match:\n e1 = " + e1.toString()
674 + ", e1_iff_e2 = " + e1_iff_e2.toString());
675 }
676 const Expr& e2(e1_iff_e2.getRHS());
677 // Avoid e1.getExpr(), it may cause unneeded Expr creation
678 if (e1_iff_e2.getLHS() == e2) return e1;
679 Proof pf;
680 Assumptions a(e1, e1_iff_e2);
681 if(withProof()) {
682 vector<Proof> pfs;
683 pfs.push_back(e1.getProof());
684 pfs.push_back(e1_iff_e2.getProof());
685 pf = newPf("iff_mp", e1.getExpr(), e2, pfs);
686 }
687 return newTheorem(e2, a, pf);
688 }
689
690
691 // e1 AND (e1 IMPLIES e2) ==> e2
implMP(const Theorem & e1,const Theorem & e1_impl_e2)692 Theorem CommonTheoremProducer::implMP(const Theorem& e1,
693 const Theorem& e1_impl_e2) {
694 const Expr& impl = e1_impl_e2.getExpr();
695 if(CHECK_PROOFS) {
696 CHECK_SOUND(impl.isImpl() && impl.arity()==2,
697 "implMP: not IMPLIES: "+impl.toString());
698 CHECK_SOUND(e1.getExpr() == impl[0],
699 "implMP: theorems don't match:\n e1 = " + e1.toString()
700 + ", e1_impl_e2 = " + impl.toString());
701 }
702 const Expr& e2 = impl[1];
703 // Avoid e1.getExpr(), it may cause unneeded Expr creation
704 // if (impl[0] == e2) return e1; // this line commented by yeting because of proof translation
705 Proof pf;
706 Assumptions a(e1, e1_impl_e2);
707 if(withProof()) {
708 vector<Proof> pfs;
709 pfs.push_back(e1.getProof());
710 pfs.push_back(e1_impl_e2.getProof());
711 pf = newPf("impl_mp", e1.getExpr(), e2, pfs);
712 }
713 return newTheorem(e2, a, pf);
714 }
715
716
717 // AND(e_0,...e_{n-1}) ==> e_i
andElim(const Theorem & e,int i)718 Theorem CommonTheoremProducer::andElim(const Theorem& e, int i) {
719 if(CHECK_PROOFS) {
720 CHECK_SOUND(e.getExpr().isAnd(), "andElim: not an AND: " + e.toString());
721 CHECK_SOUND(i < e.getExpr().arity(), "andElim: i = " + int2string(i)
722 + " >= arity = " + int2string(e.getExpr().arity())
723 + " in " + e.toString());
724 }
725 Proof pf;
726 if(withProof())
727 pf = newPf("andE", d_em->newRatExpr(i), e.getExpr(), e.getProof());
728 return newTheorem(e.getExpr()[i], Assumptions(e), pf);
729 }
730
731
732 //! e1, e2 ==> AND(e1, e2)
andIntro(const Theorem & e1,const Theorem & e2)733 Theorem CommonTheoremProducer::andIntro(const Theorem& e1, const Theorem& e2) {
734 vector<Theorem> thms;
735 thms.push_back(e1);
736 thms.push_back(e2);
737 return andIntro(thms);
738 }
739
740
andIntro(const vector<Theorem> & es)741 Theorem CommonTheoremProducer::andIntro(const vector<Theorem>& es) {
742 Proof pf;
743 if(CHECK_PROOFS)
744 CHECK_SOUND(es.size() > 1,
745 "andIntro(vector<Theorem>): vector must have more than 1 element");
746 Assumptions a(es);
747 /*
748 if(withProof()) {
749 vector<Proof> pfs;
750 for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
751 i!=iend; ++i)
752 pfs.push_back(i->getProof());
753 // pf = newPf("andI", andExpr(kids), pfs);
754 }
755 */
756 vector<Expr> kids;
757 for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
758 i!=iend; ++i)
759 kids.push_back(i->getExpr());
760
761 if(withProof()) {
762 vector<Proof> pfs;
763 for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
764 i!=iend; ++i)
765 pfs.push_back(i->getProof());
766 pf = newPf("andI", andExpr(kids), pfs);
767 }
768 return newTheorem(andExpr(kids), a, pf);
769 }
770
771
772 // G,a1,...,an |- phi
773 // -------------------------------------------------
774 // G |- (a1 & ... & an) -> phi
implIntro(const Theorem & phi,const std::vector<Expr> & assump)775 Theorem CommonTheoremProducer::implIntro(const Theorem& phi,
776 const std::vector<Expr>& assump) {
777 bool checkProofs(CHECK_PROOFS);
778 // This rule only makes sense when runnnig with assumptions
779 if(checkProofs) {
780 CHECK_SOUND(withAssumptions(),
781 "implIntro: called while running without assumptions");
782 }
783
784 const Assumptions& phiAssump = phi.getAssumptionsRef();
785
786 if(checkProofs) {
787 for(size_t i=0; i<assump.size(); i++) {
788 const Theorem& thm = phiAssump[assump[i]];
789 CHECK_SOUND(!thm.isNull() && thm.isAssump(),
790 "implIntro: this is not an assumption of phi:\n\n"
791 " a["+int2string(i)+"] = "+assump[i].toString()
792 +"\n\n phi = "+phi.getExpr().toString());
793 }
794 }
795
796 // Proof compaction: trivial derivation
797 if(assump.size() == 0) return phi;
798
799 Assumptions a(phiAssump - assump);
800 Proof pf;
801 if(withProof()) {
802 vector<Proof> u; // Proof labels for assumptions
803 for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
804 i!=iend; ++i) {
805 const Theorem& t = phiAssump[*i];
806 u.push_back(t.getProof());
807 }
808 // Arguments to the proof rule:
809 // impl_intro_3(phi, a1,...,an,tcc1,...tccn,pf_tcc1,...pf_tccn,
810 // [lambda(a1,...,an): pf_phi])
811 vector<Expr> args;
812 vector<Proof> pfs;
813 args.push_back(phi.getExpr());
814 args.insert(args.end(), assump.begin(), assump.end());
815 // Lambda-abstraction of pf_phi
816 pfs.push_back(newPf(u, assump, phi.getProof()));
817 pf = newPf("impl_intro", args, pfs);
818 }
819 Expr conj(andExpr(assump));
820 return newTheorem(conj.impExpr(phi.getExpr()), a, pf);
821 }
822
823
824 // e1 => e2 ==> ~e2 => ~e1
implContrapositive(const Theorem & thm)825 Theorem CommonTheoremProducer::implContrapositive(const Theorem& thm) {
826 const Expr& impl = thm.getExpr();
827 if(CHECK_PROOFS) {
828 CHECK_SOUND(impl.isImpl() && impl.arity()==2,
829 "CommonTheoremProducer::implContrapositive: thm="
830 +impl.toString());
831 }
832 Proof pf;
833 if(withProof())
834 pf = newPf("impl_contrapositive", impl, thm.getProof());
835 return newTheorem(impl[1].negate().impExpr(impl[0].negate()), Assumptions(thm), pf);
836 }
837
838
839 // ==> ITE(TRUE, e1, e2) == e1
840 Theorem
rewriteIteTrue(const Expr & e)841 CommonTheoremProducer::rewriteIteTrue(const Expr& e) {
842 Proof pf;
843 if(CHECK_PROOFS)
844 CHECK_SOUND(e.isITE() && e[0].isTrue(),
845 "rewriteIteTrue precondition violated");
846 if(withProof()) {
847 Type t = e[1].getType();
848 DebugAssert(!t.isNull(), "rewriteIteTrue: e1 has no type: "
849 + e[1].toString());
850 bool useIff = t.isBool();
851 if(useIff)
852 pf = newPf("rewrite_ite_true_iff", e[1], e[2]);
853 else {
854 pf = newPf("rewrite_ite_true", t.getExpr(), e[1], e[2]);
855 }
856 }
857 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
858 }
859
860
861 // ==> ITE(FALSE, e1, e2) == e2
862 Theorem
rewriteIteFalse(const Expr & e)863 CommonTheoremProducer::rewriteIteFalse(const Expr& e) {
864 Proof pf;
865 if(CHECK_PROOFS)
866 CHECK_SOUND(e.isITE() && e[0].isFalse(),
867 "rewriteIteFalse precondition violated");
868 if(withProof()) {
869 Type t = e[1].getType();
870 DebugAssert(!t.isNull(), "rewriteIteFalse: e1 has no type: "
871 + e[1].toString());
872 bool useIff = t.isBool();
873 if(useIff)
874 pf = newPf("rewrite_ite_false_iff", e[1], e[2]);
875 else {
876 pf = newPf("rewrite_ite_false", t.getExpr(), e[1], e[2]);
877 }
878 }
879 return newRWTheorem(e, e[2], Assumptions::emptyAssump(), pf);
880 }
881
882
883 // ==> ITE(c, e, e) == e
884 Theorem
rewriteIteSame(const Expr & e)885 CommonTheoremProducer::rewriteIteSame(const Expr& e) {
886 Proof pf;
887 if(CHECK_PROOFS)
888 CHECK_SOUND(e.isITE() && e[1] == e[2],
889 "rewriteIteSame precondition violated");
890 if(withProof()) {
891 Type t = e[1].getType();
892 DebugAssert(!t.isNull(), "rewriteIteSame: e[1] has no type: "
893 + e[1].toString());
894 bool useIff = t.isBool();
895 if(useIff)
896 pf = newPf("rewrite_ite_same_iff", e[0], e[1]);
897 else {
898 pf = newPf("rewrite_ite_same", t.getExpr(), e[0], e[1]);
899 }
900 }
901 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
902 }
903
904
905 // NOT e ==> e IFF FALSE
notToIff(const Theorem & not_e)906 Theorem CommonTheoremProducer::notToIff(const Theorem& not_e)
907 {
908 if(CHECK_PROOFS)
909 CHECK_SOUND(not_e.getExpr().isNot(),
910 "notToIff: not NOT: "+not_e.toString());
911
912 // Make it an atomic rule (more efficient)
913 Expr e(not_e.getExpr()[0]);
914 Proof pf;
915 if(withProof())
916 pf=newPf("not_to_iff", e, not_e.getProof());
917 return newRWTheorem(e, d_em->falseExpr(), Assumptions(not_e), pf);
918 }
919
920
921 // e1 XOR e2 ==> e1 IFF (NOT e2)
xorToIff(const Expr & e)922 Theorem CommonTheoremProducer::xorToIff(const Expr& e)
923 {
924 if(CHECK_PROOFS) {
925 CHECK_SOUND(e.isXor(), "xorToIff precondition violated");
926 CHECK_SOUND(e.arity() >= 2, "Expected XOR of arity >= 2");
927 }
928 Expr res = e[e.arity()-1];
929 for (int i = e.arity()-2; i >=0; --i) {
930 res = (!e[i]).iffExpr(res);
931 }
932 Proof pf;
933 if(withProof()) {
934 pf = newPf("xorToIff");
935 }
936 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
937 }
938
939
940 // ==> IFF(e1,e2) IFF <simplified expr>
rewriteIff(const Expr & e)941 Theorem CommonTheoremProducer::rewriteIff(const Expr& e) {
942 Proof pf;
943 if(CHECK_PROOFS)
944 CHECK_SOUND(e.isIff(), "rewriteIff precondition violated");
945 if(withProof()) {
946 pf = newPf("rewrite_iff", e[0], e[1]);
947 }
948
949 if(e[0] == e[1]) return rewriteReflexivity(e);
950
951 switch(e[0].getKind()) {
952 case TRUE_EXPR:
953 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
954 case FALSE_EXPR:
955 return newRWTheorem(e, !e[1], Assumptions::emptyAssump() ,pf);
956 case NOT:
957 if(e[0][0]==e[1])
958 return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
959 break;
960 default: break;
961 }
962
963 switch(e[1].getKind()) {
964 case TRUE_EXPR:
965 return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
966 case FALSE_EXPR:
967 return newRWTheorem(e, !e[0], Assumptions::emptyAssump(), pf);
968 case NOT:
969 if(e[0]==e[1][0])
970 return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
971 break;
972 default:
973 break;
974 }
975
976 if(e[0] < e[1])
977 return rewriteUsingSymmetry(e);
978 else
979 return reflexivityRule(e);
980 }
981
982
983 // ==> AND(e_1,...,e_n) IFF <simplified expr>
984 // 1) if e_i = FALSE then return FALSE
985 // 2) if e_i = TRUE, remove it from children
986 // 3) if e_i = AND(f_1,...,f_m) then AND(e_1,...,e_{i-1},f_1,...,f_m,e_{i+1},...,e_n)
987 // 4) if n=0 return TRUE
988 // 5) if n=1 return e_1
rewriteAnd(const Expr & e)989 Theorem CommonTheoremProducer::rewriteAnd(const Expr& e) {
990 if(CHECK_PROOFS)
991 CHECK_SOUND(e.isAnd(), "rewriteAnd: bad Expr: " + e.toString());
992 Proof pf;
993 ExprMap<bool> newKids;
994 bool isFalse (false);
995 for (Expr::iterator k=e.begin(), kend=e.end(); !isFalse && k != kend; ++k) {
996 const Expr& ek = *k;
997 if (ek.isFalse()) { isFalse=true; break; }
998 if (ek.isAnd() && ek.arity() < 10) {
999 for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
1000 if(newKids.count(j->negate()) > 0) { isFalse=true; break; }
1001 newKids[*j]=true;
1002 }
1003 } else if(!ek.isTrue()) {
1004 if(newKids.count(ek.negate()) > 0) { isFalse=true; break; }
1005 newKids[ek]=true;
1006 }
1007 }
1008 Expr res;
1009 if (isFalse) res = d_em->falseExpr();
1010 else if (newKids.size() == 0) res = d_em->trueExpr(); // All newKids were TRUE
1011 else if (newKids.size() == 1)
1012 res = newKids.begin()->first; // The only child
1013 else {
1014 vector<Expr> v;
1015 for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
1016 i!=iend; ++i)
1017 v.push_back(i->first);
1018 res = andExpr(v);
1019 }
1020 if(withProof()) {
1021 pf = newPf("rewrite_and", e,res);
1022 }
1023 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1024 }
1025
1026
1027 // ==> OR(e1,e2) IFF <simplified expr>
rewriteOr(const Expr & e)1028 Theorem CommonTheoremProducer::rewriteOr(const Expr& e) {
1029 if(CHECK_PROOFS)
1030 CHECK_SOUND(e.isOr(), "rewriteOr: bad Expr: " + e.toString());
1031 Proof pf;
1032 ExprMap<bool> newKids;
1033 bool isTrue (false);
1034 for (Expr::iterator k=e.begin(), kend=e.end(); !isTrue && k != kend; ++k) {
1035 const Expr& ek = *k;
1036 if (ek.isTrue()) { isTrue=true; break; }
1037 else if (ek.isOr() && ek.arity() < 10) {
1038 for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
1039 if(newKids.count(j->negate()) > 0) { isTrue=true; break; }
1040 newKids[*j]=true;
1041 }
1042 } else if(!ek.isFalse()) {
1043 if(newKids.count(ek.negate()) > 0) { isTrue=true; break; }
1044 newKids[ek]=true;
1045 }
1046 }
1047 Expr res;
1048 if (isTrue) res = d_em->trueExpr();
1049 else if (newKids.size() == 0) res = d_em->falseExpr(); // All kids were FALSE
1050 else if (newKids.size() == 1) res = newKids.begin()->first; // The only child
1051 else {
1052 vector<Expr> v;
1053 for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
1054 i!=iend; ++i)
1055 v.push_back(i->first);
1056 res = orExpr(v);
1057 }
1058 if(withProof()) {
1059 pf = newPf("rewrite_or", e, res);
1060 }
1061 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1062 }
1063
1064
1065 // ==> NOT TRUE IFF FALSE
rewriteNotTrue(const Expr & e)1066 Theorem CommonTheoremProducer::rewriteNotTrue(const Expr& e) {
1067 Proof pf;
1068 if(CHECK_PROOFS)
1069 CHECK_SOUND(e.isNot() && e[0].isTrue(),
1070 "rewriteNotTrue precondition violated");
1071 if(withProof())
1072 pf = newPf("rewrite_not_true");
1073 return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
1074 }
1075
1076
1077 // ==> NOT FALSE IFF TRUE
rewriteNotFalse(const Expr & e)1078 Theorem CommonTheoremProducer::rewriteNotFalse(const Expr& e) {
1079 Proof pf;
1080 if(CHECK_PROOFS)
1081 CHECK_SOUND(e.isNot() && e[0].isFalse(),
1082 "rewriteNotFalse precondition violated");
1083 if(withProof())
1084 pf = newPf("rewrite_not_false");
1085 return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
1086 }
1087
1088
1089 // ==> (NOT NOT e) IFF e, takes !!e
rewriteNotNot(const Expr & e)1090 Theorem CommonTheoremProducer::rewriteNotNot(const Expr& e) {
1091 Proof pf;
1092 if(CHECK_PROOFS)
1093 CHECK_SOUND(e.isNot() && e[0].isNot(),
1094 "rewriteNotNot precondition violated");
1095 if(withProof())
1096 pf = newPf("rewrite_not_not", e[0][0]);
1097 return newRWTheorem(e, e[0][0], Assumptions::emptyAssump(), pf);
1098 }
1099
1100
1101 //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
rewriteNotForall(const Expr & e)1102 Theorem CommonTheoremProducer::rewriteNotForall(const Expr& e) {
1103 if(CHECK_PROOFS) {
1104 CHECK_SOUND(e.isNot() && e[0].isForall(),
1105 "rewriteNotForall: expr must be NOT FORALL:\n"
1106 +e.toString());
1107 }
1108 Proof pf;
1109 if(withProof())
1110 pf = newPf("rewrite_not_forall", e);
1111 return newRWTheorem(e, d_em->newClosureExpr(EXISTS, e[0].getVars(),
1112 !e[0].getBody()), Assumptions::emptyAssump(), pf);
1113 }
1114
1115
1116 //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
rewriteNotExists(const Expr & e)1117 Theorem CommonTheoremProducer::rewriteNotExists(const Expr& e) {
1118 if(CHECK_PROOFS) {
1119 CHECK_SOUND(e.isNot() && e[0].isExists(),
1120 "rewriteNotExists: expr must be NOT FORALL:\n"
1121 +e.toString());
1122 }
1123 Proof pf;
1124 if(withProof())
1125 pf = newPf("rewrite_not_exists", e);
1126 return newRWTheorem(e, d_em->newClosureExpr(FORALL, e[0].getVars(),
1127 !e[0].getBody()), Assumptions::emptyAssump(), pf);
1128 }
1129
1130
skolemize(const Expr & e)1131 Expr CommonTheoremProducer::skolemize(const Expr& e)
1132 {
1133 vector<Expr> vars;
1134 const vector<Expr>& boundVars = e.getVars();
1135 for(unsigned int i=0; i<boundVars.size(); i++) {
1136 Expr skolV(e.skolemExpr(i));
1137 Type tp(e.getVars()[i].getType());
1138 skolV.setType(tp);
1139 vars.push_back(skolV);
1140 }
1141 return(e.getBody().substExpr(boundVars, vars));
1142 }
1143
1144
skolemizeRewrite(const Expr & e)1145 Theorem CommonTheoremProducer::skolemizeRewrite(const Expr& e)
1146 {
1147 Proof pf;
1148 if(CHECK_PROOFS) {
1149 CHECK_SOUND(e.isExists(), "skolemize rewrite called on non-existential: "
1150 + e.toString());
1151 }
1152 Expr skol = skolemize(e);
1153 if(withProof()) {
1154 Expr rw(e.iffExpr(skol));
1155 pf = newLabel(rw);
1156 }
1157 TRACE("quantlevel", "skolemize ", skol, "");
1158 TRACE("quantlevel sko", "skolemize ", skol, "");
1159 TRACE("quantlevel sko", "skolemize from org ", e, "");
1160 return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
1161
1162 }
1163
1164
skolemizeRewriteVar(const Expr & e)1165 Theorem CommonTheoremProducer::skolemizeRewriteVar(const Expr& e)
1166 {
1167 Proof pf;
1168 if(CHECK_PROOFS) {
1169 CHECK_SOUND(e.isExists(), "skolemizeRewriteVar("
1170 +e.toString()+")");
1171 }
1172
1173 const vector<Expr>& boundVars = e.getVars();
1174 const Expr& body = e.getBody();
1175
1176 if(CHECK_PROOFS) {
1177 CHECK_SOUND(boundVars.size()==1, "skolemizeRewriteVar("
1178 +e.toString()+")");
1179 CHECK_SOUND(body.isEq() || body.isIff(), "skolemizeRewriteVar("
1180 +e.toString()+")");
1181 const Expr& v = boundVars[0];
1182 CHECK_SOUND(body[1] == v, "skolemizeRewriteVar("
1183 +e.toString()+")");
1184 CHECK_SOUND(!(v.subExprOf(body[0])), "skolemizeRewriteVar("
1185 +e.toString()+")");
1186 }
1187 // Create the Skolem constant appropriately
1188 Expr skolV(e.skolemExpr(0));
1189 Type tp(e.getVars()[0].getType());
1190 skolV.setType(tp);
1191 // Skolemized expression
1192 Expr skol = Expr(body.getOp(), body[0], skolV);
1193
1194 if(withProof()) {
1195 Expr rw(e.iffExpr(skol));
1196 pf = newLabel(rw);
1197 }
1198 return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
1199 }
1200
1201
varIntroRule(const Expr & phi)1202 Theorem CommonTheoremProducer::varIntroRule(const Expr& phi) {
1203 // This rule is sound for all expressions phi
1204 Proof pf;
1205 const Expr boundVar = d_em->newBoundVarExpr(phi.getType());
1206
1207 Expr body;
1208 if(phi.getType().isBool())
1209 body = phi.iffExpr(boundVar);
1210 else
1211 body = phi.eqExpr(boundVar);
1212
1213 std::vector<Expr> v;
1214 v.push_back(boundVar);
1215 const Expr result = d_em->newClosureExpr(EXISTS, v, body);
1216
1217 if(withProof())
1218 pf = newPf("var_intro", phi, boundVar);
1219 return newTheorem(result, Assumptions::emptyAssump(), pf);
1220 }
1221
1222
skolemize(const Theorem & thm)1223 Theorem CommonTheoremProducer::skolemize(const Theorem& thm) {
1224 const Expr& e = thm.getExpr();
1225 if(e.isExists()) {
1226 TRACE("skolem", "Skolemizing existential:", "", "{");
1227 CDMap<Expr, Theorem>::iterator i=d_skolemized_thms.find(e),
1228 iend=d_skolemized_thms.end();
1229 if(i!=iend) {
1230 TRACE("skolem", "Skolemized theorem found in map: ", (*i).second, "}");
1231 return iffMP(thm, (*i).second);
1232 }
1233 Theorem skol = skolemizeRewrite(e);
1234 for(unsigned int i=0; i<e.getVars().size(); i++) {
1235 Expr skolV(e.skolemExpr(i));
1236 Type tp(e.getVars()[i].getType());
1237 skolV.setType(tp);
1238 }
1239 d_skolem_axioms.push_back(skol);
1240 d_skolemized_thms.insert(e, skol, 0);//d_coreSatAPI->getBottomScope());
1241 skol = iffMP(thm, skol);
1242
1243 TRACE("skolem", "skolemized new theorem: ", skol, "}");
1244 return skol;
1245 }
1246 return thm;
1247 }
1248
1249
varIntroSkolem(const Expr & e)1250 Theorem CommonTheoremProducer::varIntroSkolem(const Expr& e) {
1251 // First, look up the cache
1252 CDMap<Expr, Theorem>::iterator i=d_skolemVars.find(e),
1253 iend=d_skolemVars.end();
1254 if(i!=iend) return (*i).second;
1255 // Not in cache; create a new one
1256 Theorem thm = varIntroRule(e);
1257 const Expr& e2 = thm.getExpr();
1258 DebugAssert(e2.isExists() && e2.getVars().size()==1, "varIntroSkolem: e2 = "
1259 +e2.toString());
1260 Theorem skolThm;
1261 // Check if we have a corresponding skolemized version already
1262 CDMap<Expr, Theorem>::iterator j=d_skolemized_thms.find(e2),
1263 jend=d_skolemized_thms.end();
1264 if(j!=jend) {
1265 skolThm = (*i).second;
1266 } else {
1267 skolThm = skolemizeRewriteVar(e2);
1268 d_skolem_axioms.push_back(skolThm);
1269 d_skolemized_thms.insert(e2, skolThm, 0); //d_coreSatAPI->getBottomScope());
1270 }
1271 thm = iffMP(thm, skolThm);
1272 d_skolemVars.insert(e, thm, 0); //d_coreSatAPI->getBottomScope());
1273 return thm;
1274 }
1275
1276
1277 // Derived Rules
1278
1279
trueTheorem()1280 Theorem CommonTheoremProducer::trueTheorem()
1281 {
1282 return iffTrueElim(reflexivityRule(d_em->trueExpr()));
1283 }
1284
1285
rewriteAnd(const Theorem & e)1286 Theorem CommonTheoremProducer::rewriteAnd(const Theorem& e)
1287 {
1288 return iffMP(e, rewriteAnd(e.getExpr()));
1289 }
1290
1291
rewriteOr(const Theorem & e)1292 Theorem CommonTheoremProducer::rewriteOr(const Theorem& e)
1293 {
1294 return iffMP(e, rewriteOr(e.getExpr()));
1295 }
1296
1297
ackermann(const Expr & e1,const Expr & e2)1298 Theorem CommonTheoremProducer::ackermann(const Expr& e1, const Expr& e2)
1299 {
1300 Proof pf;
1301 if(CHECK_PROOFS)
1302 CHECK_SOUND(e1.isApply() && e2.isApply() && e1.getOp() == e2.getOp(),
1303 "ackermann precondition violated");
1304 Expr hyp;
1305 int ar = e1.arity();
1306 if (ar == 1) {
1307 hyp = Expr(e1[0].eqExpr(e2[0]));
1308 }
1309 else {
1310 vector<Expr> vec;
1311 for (int i = 0; i != ar; ++i) {
1312 vec.push_back(e1[i].eqExpr(e2[i]));
1313 }
1314 hyp = Expr(AND, vec);
1315 }
1316 if(withProof())
1317 pf = newPf("ackermann", e1, e2);
1318 return newTheorem(hyp.impExpr(e1.eqExpr(e2)), Assumptions::emptyAssump(), pf);
1319 }
1320
1321
findITE(const Expr & e,Expr & condition,Expr & thenpart,Expr & elsepart)1322 void CommonTheoremProducer::findITE(const Expr& e, Expr& condition, Expr& thenpart, Expr& elsepart)
1323 {
1324 if (!e.getType().isBool() && e.isITE()) {
1325 condition = e[0];
1326 if (!condition.containsTermITE()) {
1327 thenpart = e[1];
1328 elsepart = e[2];
1329 return;
1330 }
1331 }
1332
1333 vector<Expr> kids;
1334 int i = 0;
1335 for (; i < e.arity(); ++i) {
1336 if (e[i].containsTermITE()) break;
1337 kids.push_back(e[i]);
1338 }
1339
1340 if(CHECK_PROOFS) {
1341 CHECK_SOUND(i < e.arity(), "could not find ITE");
1342 }
1343
1344 Expr t2, e2;
1345 findITE(e[i], condition, t2, e2);
1346
1347 kids.push_back(t2);
1348 for(int k = i+1; k < e.arity(); ++k) {
1349 kids.push_back(e[k]);
1350 }
1351
1352 thenpart = Expr(e.getOp(), kids);
1353
1354 kids[i] = e2;
1355 elsepart = Expr(e.getOp(), kids);
1356 }
1357
1358
liftOneITE(const Expr & e)1359 Theorem CommonTheoremProducer::liftOneITE(const Expr& e) {
1360
1361 if(CHECK_PROOFS) {
1362 CHECK_SOUND(e.containsTermITE(), "CommonTheoremProducer::liftOneITE: bad input" + e.toString());
1363 }
1364
1365 Expr cond, thenpart, elsepart;
1366
1367 findITE(e, cond, thenpart, elsepart);
1368
1369 Proof pf;
1370 if(withProof())
1371 pf = newPf("lift_one_ite", e);
1372
1373 return newRWTheorem(e, cond.iteExpr(thenpart, elsepart), Assumptions::emptyAssump(), pf);
1374 }
1375