00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 #define _CVC3_TRUSTED_
00025
00026
00027 #include "common_theorem_producer.h"
00028
00029
00030 using namespace CVC3;
00031 using namespace std;
00032
00033
00034
00035 CommonProofRules* TheoremManager::createProofRules() {
00036 return new CommonTheoremProducer(this);
00037 }
00038
00039
00040 CommonTheoremProducer::CommonTheoremProducer(TheoremManager* tm)
00041 : TheoremProducer(tm),
00042 d_skolemized_thms(tm->getCM()->getCurrentContext()),
00043 d_skolemVars(tm->getCM()->getCurrentContext())
00044 {}
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054 Theorem3
00055 CommonTheoremProducer::queryTCC(const Theorem& phi, const Theorem& D_phi) {
00056 Proof pf;
00057
00058
00059
00060
00061
00062
00063
00064
00065
00066 Assumptions a = phi.getAssumptionsRef();
00067 a.add(D_phi);
00068 if(withProof()) {
00069 vector<Expr> args;
00070 vector<Proof> pfs;
00071 args.push_back(phi.getExpr());
00072 args.push_back(D_phi.getExpr());
00073 pfs.push_back(phi.getProof());
00074 pfs.push_back(D_phi.getProof());
00075 pf = newPf("queryTCC", args, pfs);
00076 }
00077 return newTheorem3(phi.getExpr(), a, pf);
00078 }
00079
00080
00081
00082
00083
00084 Theorem3
00085 CommonTheoremProducer::implIntro3(const Theorem3& phi,
00086 const std::vector<Expr>& assump,
00087 const vector<Theorem>& tccs) {
00088 bool checkProofs(CHECK_PROOFS);
00089
00090 if(checkProofs) {
00091 CHECK_SOUND(withAssumptions(),
00092 "implIntro3: called while running without assumptions");
00093 }
00094
00095 const Assumptions& phiAssump = phi.getAssumptionsRef();
00096
00097 if(checkProofs) {
00098 CHECK_SOUND(assump.size() == tccs.size(),
00099 "implIntro3: number of assumptions ("
00100 +int2string(assump.size())+") and number of TCCs ("
00101 +int2string(tccs.size())
00102 +") does not match");
00103 for(size_t i=0; i<assump.size(); i++) {
00104 const Theorem& thm = phiAssump[assump[i]];
00105 CHECK_SOUND(!thm.isNull() && thm.isAssump(),
00106 "implIntro3: this is not an assumption of phi:\n\n"
00107 " a["+int2string(i)+"] = "+assump[i].toString()
00108 +"\n\n phi = "+phi.getExpr().toString());
00109
00110
00111
00112
00113
00114
00115
00116 }
00117 }
00118
00119
00120 if(assump.size() == 0) return phi;
00121
00122 Assumptions a(phiAssump - assump);
00123 Assumptions b(tccs);
00124 a.add(b);
00125 Proof pf;
00126 if(withProof()) {
00127 vector<Proof> u;
00128 for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
00129 i!=iend; ++i) {
00130 const Theorem& t = phiAssump[*i];
00131 u.push_back(t.getProof());
00132 }
00133
00134
00135
00136 vector<Expr> args;
00137 vector<Proof> pfs;
00138 args.push_back(phi.getExpr());
00139 args.insert(args.end(), assump.begin(), assump.end());
00140 for(vector<Theorem>::const_iterator i=tccs.begin(), iend=tccs.end();
00141 i!=iend; ++i) {
00142 args.push_back(i->getExpr());
00143 pfs.push_back(i->getProof());
00144 }
00145
00146 pfs.push_back(newPf(u, assump, phi.getProof()));
00147 pf = newPf("impl_intro_3", args, pfs);
00148 }
00149 Expr conj(andExpr(assump));
00150 return newTheorem3(conj.impExpr(phi.getExpr()), a, pf);
00151 }
00152
00153
00154 Theorem CommonTheoremProducer::assumpRule(const Expr& e, int scope) {
00155
00156 Proof pf;
00157 if(withProof()) pf = newLabel(e);
00158 return newAssumption(e, pf, scope);
00159 }
00160
00161
00162 Theorem CommonTheoremProducer::reflexivityRule(const Expr& a) {
00163 return newReflTheorem(a);
00164 }
00165
00166
00167
00168 Theorem CommonTheoremProducer::rewriteReflexivity(const Expr& t) {
00169 if(CHECK_PROOFS)
00170 CHECK_SOUND((t.isEq() || t.isIff()) && t[0] == t[1],
00171 "rewriteReflexivity: wrong expression: "
00172 + t.toString());
00173 Proof pf;
00174 if(withProof()) {
00175 if(t.isEq()) {
00176 DebugAssert(!t[0].getType().isNull(),
00177 "rewriteReflexivity: t[0] has no type: "
00178 + t[0].toString());
00179 pf = newPf("rewrite_eq_refl", t[0].getType().getExpr(), t[0]);
00180 } else
00181 pf = newPf("rewrite_iff_refl", t[0]);
00182 }
00183 return newRWTheorem(t, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
00184 }
00185
00186
00187 Theorem CommonTheoremProducer::symmetryRule(const Theorem& a1_eq_a2) {
00188 if(CHECK_PROOFS)
00189 CHECK_SOUND(a1_eq_a2.isRewrite(),
00190 ("CVC3::CommonTheoremProducer: "
00191 "theorem is not an equality or iff:\n "
00192 + a1_eq_a2.getExpr().toString()).c_str());
00193 const Expr& a1 = a1_eq_a2.getLHS();
00194 const Expr& a2 = a1_eq_a2.getRHS();
00195
00196 Proof pf;
00197
00198
00199
00200
00201 if(a1 == a2) return reflexivityRule(a1);
00202
00203 if(withProof()) {
00204 Type t = a1.getType();
00205
00206 IF_DEBUG(a1_eq_a2.getExpr().getType());
00207 bool isEquality = !t.isBool();
00208 if(isEquality) {
00209 vector<Expr> args;
00210 args.push_back(t.getExpr());
00211 args.push_back(a1);
00212 args.push_back(a2);
00213 pf = newPf("eq_symm", args, a1_eq_a2.getProof());
00214 } else
00215 pf = newPf("iff_symm", a1, a2, a1_eq_a2.getProof());
00216 }
00217 return newRWTheorem(a2, a1, a1_eq_a2.getAssumptionsRef(), pf);
00218 }
00219
00220
00221 Theorem CommonTheoremProducer::rewriteUsingSymmetry(const Expr& a1_eq_a2) {
00222 bool isIff = a1_eq_a2.isIff();
00223 if(CHECK_PROOFS)
00224 CHECK_SOUND(a1_eq_a2.isEq() || isIff, "rewriteUsingSymmetry precondition violated");
00225 const Expr& a1 = a1_eq_a2[0];
00226 const Expr& a2 = a1_eq_a2[1];
00227
00228 if(a1 == a2) return reflexivityRule(a1_eq_a2);
00229
00230 Proof pf;
00231 if(withProof()) {
00232 Type t = a1.getType();
00233 DebugAssert(!t.isNull(),
00234 "rewriteUsingSymmetry: a1 has no type: " + a1.toString());
00235 if(isIff)
00236 pf = newPf("rewrite_iff_symm", a1, a2);
00237 else {
00238 pf = newPf("rewrite_eq_symm", t.getExpr(), a1, a2);
00239 }
00240 }
00241 return newRWTheorem(a1_eq_a2, isIff ? a2.iffExpr(a1) : a2.eqExpr(a1), Assumptions::emptyAssump(), pf);
00242 }
00243
00244
00245 Theorem CommonTheoremProducer::transitivityRule(const Theorem& a1_eq_a2,
00246 const Theorem& a2_eq_a3) {
00247 DebugAssert(!a1_eq_a2.isNull(), "transitivityRule()");
00248 DebugAssert(!a2_eq_a3.isNull(), "transitivityRule()");
00249 if(CHECK_PROOFS) {
00250 CHECK_SOUND(a1_eq_a2.isRewrite() && a2_eq_a3.isRewrite(),
00251 "CVC3::CommonTheoremProducer::transitivityRule:\n "
00252 "Wrong premises: first = "
00253 + a1_eq_a2.getExpr().toString() + ", second = "
00254 + a2_eq_a3.getExpr().toString());
00255 CHECK_SOUND(a1_eq_a2.getRHS() == a2_eq_a3.getLHS(),
00256 "CVC3::CommonTheoremProducer::transitivityRule:\n "
00257 "Wrong premises: first = "
00258 + a1_eq_a2.getExpr().toString() + ", second = "
00259 + a2_eq_a3.getExpr().toString());
00260 }
00261 const Expr& a1 = a1_eq_a2.getLHS();
00262 const Expr& a2 = a1_eq_a2.getRHS();
00263 const Expr& a3 = a2_eq_a3.getRHS();
00264
00265
00266
00267
00268
00269 if(a1 == a3) return reflexivityRule(a1);
00270
00271 if(a1 == a2) return a2_eq_a3;
00272 if(a2 == a3) return a1_eq_a2;
00273
00274
00275
00276
00277
00278 Proof pf;
00279 Assumptions a(a1_eq_a2, a2_eq_a3);
00280
00281 if(withProof()) {
00282 Type t = a1.getType();
00283 bool isEquality = (!t.isBool());
00284 string name((isEquality)? "eq_trans" : "iff_trans");
00285 vector<Expr> args;
00286 vector<Proof> pfs;
00287 DebugAssert(!t.isNull(), "transitivityRule: "
00288 "Type is not computed for a1: " + a1.toString());
00289
00290 if(isEquality) args.push_back(t.getExpr());
00291 args.push_back(a1);
00292 args.push_back(a2);
00293 args.push_back(a3);
00294 pfs.push_back(a1_eq_a2.getProof());
00295 pfs.push_back(a2_eq_a3.getProof());
00296 pf = newPf(name, args, pfs);
00297 }
00298 return newRWTheorem(a1, a3, a, pf);
00299 }
00300
00301
00302 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00303 const Theorem& thm) {
00304 IF_DEBUG
00305 (static DebugTimer
00306 accum0(debugger.timer("substitutivityRule0 time"));
00307 static DebugTimer tmpTimer(debugger.newTimer());
00308 static DebugCounter count(debugger.counter("substitutivityRule0 calls"));
00309 debugger.setCurrentTime(tmpTimer);
00310 count++);
00311
00312
00313 if(CHECK_PROOFS) {
00314 CHECK_SOUND(e.arity() == 1 && e[0] == thm.getLHS(),
00315 "Unexpected use of substitutivityRule0");
00316 CHECK_SOUND(thm.isRewrite(),
00317 "CVC3::CommonTheoremProducer::substitutivityRule0:\n "
00318 "premis is not an equality or IFF: "
00319 + thm.getExpr().toString()
00320 + "\n expr = " + e.toString());
00321 }
00322 Expr e2(e.getOp(), thm.getRHS());
00323 Proof pf;
00324 if(withProof())
00325 pf = newPf("basic_subst_op0",e,thm.getProof());
00326 return newRWTheorem(e, e2, thm.getAssumptionsRef(), pf);
00327 }
00328
00329
00330 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00331 const Theorem& thm1,
00332 const Theorem& thm2) {
00333 IF_DEBUG
00334 (static DebugTimer
00335 accum0(debugger.timer("substitutivityRule1 time"));
00336 static DebugTimer tmpTimer(debugger.newTimer());
00337 static DebugCounter count(debugger.counter("substitutivityRule1 calls"));
00338 debugger.setCurrentTime(tmpTimer);
00339 count++);
00340
00341
00342 if(CHECK_PROOFS) {
00343 CHECK_SOUND(e.arity() == 2 && e[0] == thm1.getLHS() &&
00344 e[1] == thm2.getLHS(),
00345 "Unexpected use of substitutivityRule1");
00346 CHECK_SOUND(thm1.isRewrite(),
00347 "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
00348 "premis is not an equality or IFF: "
00349 + thm1.getExpr().toString()
00350 + "\n expr = " + e.toString());
00351 CHECK_SOUND(thm2.isRewrite(),
00352 "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
00353 "premis is not an equality or IFF: "
00354 + thm2.getExpr().toString()
00355 + "\n expr = " + e.toString());
00356 }
00357 Expr e2(e.getOp(), thm1.getRHS(), thm2.getRHS());
00358 Proof pf;
00359 if(withProof()) {
00360 vector<Proof> pfs;
00361 pfs.push_back(thm1.getProof());
00362 pfs.push_back(thm2.getProof());
00363 pf = newPf("basic_subst_op1", e, pfs);
00364 }
00365 return newRWTheorem(e, e2, Assumptions(thm1, thm2), pf);
00366 }
00367
00368
00369 Theorem CommonTheoremProducer::substitutivityRule(const Op& op,
00370 const vector<Theorem>& thms) {
00371 IF_DEBUG
00372 (static DebugTimer
00373 accum0(debugger.timer("substitutivityRule time"));
00374 static DebugTimer tmpTimer(debugger.newTimer());
00375 static DebugCounter count(debugger.counter("substitutivityRule calls"));
00376 debugger.setCurrentTime(tmpTimer);
00377 count++);
00378
00379 unsigned size(thms.size());
00380 if(size == 0)
00381 return reflexivityRule(d_tm->getEM()->newLeafExpr(op));
00382
00383
00384 vector<Expr> c, d;
00385 vector<Proof> pfs;
00386
00387
00388 c.reserve(size); d.reserve(size);
00389 for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
00390 i != iend; ++i) {
00391
00392 if(CHECK_PROOFS)
00393 CHECK_SOUND(i->isRewrite(),
00394 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
00395 "premis is not an equality or IFF: "
00396 + i->getExpr().toString()
00397 + "\n op = " + op.toString());
00398
00399 c.push_back(i->getLHS());
00400 d.push_back(i->getRHS());
00401 if(withProof()) pfs.push_back(i->getProof());
00402 }
00403 Expr e1(op, c), e2(op, d);
00404
00405 if(e1 == e2) return reflexivityRule(e1);
00406
00407 Assumptions a(thms);
00408 Proof pf;
00409 if(withProof())
00410
00411 pf = newPf("basic_subst_op",e1,e2,pfs);
00412 Theorem res = newRWTheorem(e1, e2, a, pf);
00413 IF_DEBUG(debugger.setElapsed(tmpTimer);
00414 accum0 += tmpTimer);
00415 return res;
00416 }
00417
00418
00419 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00420 const vector<unsigned>& changed,
00421 const vector<Theorem>& thms) {
00422 IF_DEBUG
00423 (static DebugTimer
00424 accum0(debugger.timer("substitutivityRule2 time"));
00425 static DebugTimer tmpTimer(debugger.newTimer());
00426 static DebugCounter count(debugger.counter("substitutivityRule2 calls"));
00427 debugger.setCurrentTime(tmpTimer);
00428 count++);
00429 DebugAssert(changed.size() > 0, "substitutivityRule2 should not be called");
00430 DebugAssert(changed.size() == thms.size(), "substitutivityRule2: wrong args");
00431
00432
00433
00434 unsigned size = e.arity();
00435 if (size == 1) return substitutivityRule(e, thms.back());
00436 unsigned csize = changed.size();
00437 if (size == 2) {
00438 if (csize == 2) return substitutivityRule(e, thms[0], thms[1]);
00439 if (changed[0] == 0) {
00440 return substitutivityRule(e, thms[0], reflexivityRule(e[1]));
00441 }
00442 else {
00443 return substitutivityRule(e, reflexivityRule(e[0]), thms[0]);
00444 }
00445 }
00446 DebugAssert(size >= csize, "Bad call to substitutivityRule2");
00447
00448 vector<Expr> c;
00449 bool checkProofs(CHECK_PROOFS);
00450 for(unsigned j = 0, k = 0; k < size; ++k) {
00451 if (j == csize || changed[j] != k) {
00452 c.push_back(e[k]);
00453 continue;
00454 }
00455
00456 if(checkProofs)
00457 CHECK_SOUND(thms[j].isRewrite() && thms[j].getLHS() == e[k],
00458 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
00459 "premis is not an equality or IFF: "
00460 + thms[j].getExpr().toString()
00461 + "\n e = " + e.toString());
00462
00463 c.push_back(thms[j].getRHS());
00464 ++j;
00465 }
00466 Expr e2(e.getOp(), c);
00467 IF_DEBUG(if(e == e2) {
00468 ostream& os = debugger.getOS();
00469 os << "substitutivityRule2: e = " << e << "\n e2 = " << e2
00470 << "\n changed kids: [\n";
00471 for(unsigned j=0; j<changed.size(); j++)
00472 os << " (" << changed[j] << ") " << thms[j] << "\n";
00473 os << "]\n";
00474 });
00475 DebugAssert(e != e2,
00476 "substitutivityRule2 should not be called in this case:\n"
00477 "e = "+e.toString());
00478
00479 Proof pf;
00480 Assumptions a(thms);
00481 if(withProof()) {
00482 vector<Proof> pfs;
00483 for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
00484 i != iend; ++i) {
00485
00486 if(CHECK_PROOFS)
00487 CHECK_SOUND(i->isRewrite(),
00488 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
00489 "premis is not an equality or IFF: "
00490 + i->getExpr().toString());
00491
00492 pfs.push_back(i->getProof());
00493 }
00494 pf = newPf("optimized_subst_op",e,e2,pfs);
00495 }
00496 Theorem res = newRWTheorem(e, e2, a, pf);
00497 IF_DEBUG(debugger.setElapsed(tmpTimer);
00498 accum0 += tmpTimer);
00499 return res;
00500 }
00501
00502
00503 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00504 const int changed,
00505 const Theorem& thm)
00506 {
00507
00508 int size = e.arity();
00509
00510
00511 DebugAssert(size >= changed, "Bad call to substitutivityRule");
00512
00513
00514 if(CHECK_PROOFS)
00515 CHECK_SOUND(thm.isRewrite() && thm.getLHS() == e[changed], "CVC3::CommonTheoremProducer::substitutivityRule:\n "
00516 "premise is not an equality or IFF: " + thm.getExpr().toString() + "\n" +
00517 "e = " + e.toString());
00518
00519
00520 vector<Expr> c;
00521 for(int k = 0; k < size; ++ k)
00522 if (k != changed) c.push_back(e[k]);
00523 else c.push_back(thm.getRHS());
00524
00525
00526 Expr e2(e.getOp(), c);
00527
00528
00529 IF_DEBUG(if(e == e2) {
00530 ostream& os = debugger.getOS();
00531 os << "substitutivityRule: e = " << e << "\n e2 = " << e2 << endl;
00532 });
00533
00534
00535 DebugAssert(e != e2, "substitutivityRule should not be called in this case:\ne = "+e.toString());
00536
00537
00538 Proof pf;
00539 Assumptions a(thm);
00540 if(withProof()) {
00541
00542 if(CHECK_PROOFS)
00543 CHECK_SOUND(thm.isRewrite(), "CVC3::CommonTheoremProducer::substitutivityRule:\npremise is not an equality or IFF: " + thm.getExpr().toString());
00544 pf = newPf("optimized_subst_op2",e,e2,thm.getProof());
00545 }
00546
00547
00548 return newRWTheorem(e, e2, a, pf);;
00549 }
00550
00551
00552
00553 Theorem CommonTheoremProducer::contradictionRule(const Theorem& e,
00554 const Theorem& not_e) {
00555 Proof pf;
00556 if(CHECK_PROOFS)
00557 CHECK_SOUND(!e.getExpr() == not_e.getExpr(),
00558 "CommonTheoremProducer::contraditionRule: "
00559 "theorems don't match:\n e = "+e.toString()
00560 +"\n not_e = "+not_e.toString());
00561 Assumptions a(e, not_e);
00562 if(withProof()) {
00563 vector<Proof> pfs;
00564 pfs.push_back(e.getProof());
00565 pfs.push_back(not_e.getProof());
00566 pf = newPf("contradition", e.getExpr(), pfs);
00567 }
00568 return newTheorem(d_em->falseExpr(), a, pf);
00569 }
00570
00571
00572 Theorem CommonTheoremProducer::excludedMiddle(const Expr& e)
00573 {
00574 Proof pf;
00575 if (withProof()) {
00576 pf = newPf("excludedMiddle", e);
00577 }
00578 return newTheorem(e.orExpr(!e), Assumptions::emptyAssump(), pf);
00579 }
00580
00581
00582
00583 Theorem CommonTheoremProducer::iffTrue(const Theorem& e)
00584 {
00585 Proof pf;
00586 if(withProof()) {
00587 pf = newPf("iff_true", e.getExpr(), e.getProof());
00588 }
00589 return newRWTheorem(e.getExpr(), d_em->trueExpr(), e.getAssumptionsRef(), pf);
00590 }
00591
00592
00593
00594 Theorem CommonTheoremProducer::iffNotFalse(const Theorem& e) {
00595 Proof pf;
00596 if(withProof()) {
00597 pf = newPf("iff_not_false", e.getExpr(), e.getProof());
00598 }
00599 return newRWTheorem(!e.getExpr(), d_em->falseExpr(), e.getAssumptionsRef(), pf);
00600 }
00601
00602
00603
00604 Theorem CommonTheoremProducer::iffTrueElim(const Theorem& e) {
00605 if(CHECK_PROOFS)
00606 CHECK_SOUND(e.isRewrite() && e.getRHS().isTrue(),
00607 "CommonTheoremProducer::iffTrueElim: "
00608 "theorem is not e<=>TRUE: "+ e.toString());
00609 Proof pf;
00610 if(withProof()) {
00611 pf = newPf("iff_true_elim", e.getLHS(), e.getProof());
00612 }
00613 return newTheorem(e.getLHS(), e.getAssumptionsRef(), pf);
00614 }
00615
00616
00617
00618 Theorem CommonTheoremProducer::iffFalseElim(const Theorem& e) {
00619 if(CHECK_PROOFS)
00620 CHECK_SOUND(e.isRewrite() && e.getRHS().isFalse(),
00621 "CommonTheoremProducer::iffFalseElim: "
00622 "theorem is not e<=>FALSE: "+ e.toString());
00623 const Expr& lhs = e.getLHS();
00624 Proof pf;
00625 if(withProof()) {
00626 pf = newPf("iff_false_elim", lhs, e.getProof());
00627 }
00628 return newTheorem(!lhs, e.getAssumptionsRef(), pf);
00629 }
00630
00631
00632
00633 Theorem CommonTheoremProducer::iffContrapositive(const Theorem& e) {
00634 if(CHECK_PROOFS)
00635 CHECK_SOUND(e.isRewrite() && e.getRHS().getType().isBool(),
00636 "CommonTheoremProducer::iffContrapositive: "
00637 "theorem is not e1<=>e2: "+ e.toString());
00638 Proof pf;
00639 if(withProof()) {
00640 pf = newPf("iff_contrapositive", e.getExpr(), e.getProof());
00641 }
00642 return newRWTheorem(e.getLHS().negate(),e.getRHS().negate(), e.getAssumptionsRef(), pf);
00643 }
00644
00645
00646
00647 Theorem CommonTheoremProducer::notNotElim(const Theorem& not_not_e) {
00648 if(CHECK_PROOFS)
00649 CHECK_SOUND(not_not_e.getExpr().isNot() && not_not_e.getExpr()[0].isNot(),
00650 "CommonTheoremProducer::notNotElim: bad theorem: !!e = "
00651 + not_not_e.toString());
00652 Proof pf;
00653 if(withProof())
00654 pf = newPf("not_not_elim", not_not_e.getExpr(), not_not_e.getProof());
00655 return newTheorem(not_not_e.getExpr()[0][0], not_not_e.getAssumptionsRef(), pf);
00656 }
00657
00658
00659 Theorem CommonTheoremProducer::iffMP(const Theorem& e1, const Theorem& e1_iff_e2)
00660 {
00661 if(CHECK_PROOFS) {
00662 CHECK_SOUND(e1_iff_e2.isRewrite(),
00663 "iffMP: not IFF: "+e1_iff_e2.toString());
00664 CHECK_SOUND(e1.getExpr() == (e1_iff_e2.getLHS()),
00665 "iffMP: theorems don't match:\n e1 = " + e1.toString()
00666 + ", e1_iff_e2 = " + e1_iff_e2.toString());
00667 }
00668 const Expr& e2(e1_iff_e2.getRHS());
00669
00670 if (e1_iff_e2.getLHS() == e2) return e1;
00671 Proof pf;
00672 Assumptions a(e1, e1_iff_e2);
00673 if(withProof()) {
00674 vector<Proof> pfs;
00675 pfs.push_back(e1.getProof());
00676 pfs.push_back(e1_iff_e2.getProof());
00677 pf = newPf("iff_mp", e1.getExpr(), e2, pfs);
00678 }
00679 return newTheorem(e2, a, pf);
00680 }
00681
00682
00683
00684 Theorem CommonTheoremProducer::implMP(const Theorem& e1,
00685 const Theorem& e1_impl_e2) {
00686 const Expr& impl = e1_impl_e2.getExpr();
00687 if(CHECK_PROOFS) {
00688 CHECK_SOUND(impl.isImpl() && impl.arity()==2,
00689 "implMP: not IMPLIES: "+impl.toString());
00690 CHECK_SOUND(e1.getExpr() == impl[0],
00691 "implMP: theorems don't match:\n e1 = " + e1.toString()
00692 + ", e1_impl_e2 = " + impl.toString());
00693 }
00694 const Expr& e2 = impl[1];
00695
00696 if (impl[0] == e2) return e1;
00697 Proof pf;
00698 Assumptions a(e1, e1_impl_e2);
00699 if(withProof()) {
00700 vector<Proof> pfs;
00701 pfs.push_back(e1.getProof());
00702 pfs.push_back(e1_impl_e2.getProof());
00703 pf = newPf("impl_mp", e1.getExpr(), e2, pfs);
00704 }
00705 return newTheorem(e2, a, pf);
00706 }
00707
00708
00709
00710 Theorem CommonTheoremProducer::andElim(const Theorem& e, int i) {
00711 if(CHECK_PROOFS) {
00712 CHECK_SOUND(e.getExpr().isAnd(), "andElim: not an AND: " + e.toString());
00713 CHECK_SOUND(i < e.getExpr().arity(), "andElim: i = " + int2string(i)
00714 + " >= arity = " + int2string(e.getExpr().arity())
00715 + " in " + e.toString());
00716 }
00717 Proof pf;
00718 if(withProof())
00719 pf = newPf("andE", d_em->newRatExpr(i), e.getExpr(), e.getProof());
00720 return newTheorem(e.getExpr()[i], e.getAssumptionsRef(), pf);
00721 }
00722
00723
00724
00725 Theorem CommonTheoremProducer::andIntro(const Theorem& e1, const Theorem& e2) {
00726 vector<Theorem> thms;
00727 thms.push_back(e1);
00728 thms.push_back(e2);
00729 return andIntro(thms);
00730 }
00731
00732
00733 Theorem CommonTheoremProducer::andIntro(const vector<Theorem>& es) {
00734 Proof pf;
00735 if(CHECK_PROOFS)
00736 CHECK_SOUND(es.size() > 0,
00737 "andIntro(vector<Theorem>): vector must be non-empty");
00738 Assumptions a(es);
00739 if(withProof()) {
00740 vector<Proof> pfs;
00741 for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
00742 i!=iend; ++i)
00743 pfs.push_back(i->getProof());
00744 pf = newPf("andI", pfs);
00745 }
00746 vector<Expr> kids;
00747 for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
00748 i!=iend; ++i)
00749 kids.push_back(i->getExpr());
00750 return newTheorem(andExpr(kids), a, pf);
00751 }
00752
00753
00754
00755
00756
00757 Theorem CommonTheoremProducer::implIntro(const Theorem& phi,
00758 const std::vector<Expr>& assump) {
00759 bool checkProofs(CHECK_PROOFS);
00760
00761 if(checkProofs) {
00762 CHECK_SOUND(withAssumptions(),
00763 "implIntro: called while running without assumptions");
00764 }
00765
00766 const Assumptions& phiAssump = phi.getAssumptionsRef();
00767
00768 if(checkProofs) {
00769 for(size_t i=0; i<assump.size(); i++) {
00770 const Theorem& thm = phiAssump[assump[i]];
00771 CHECK_SOUND(!thm.isNull() && thm.isAssump(),
00772 "implIntro: this is not an assumption of phi:\n\n"
00773 " a["+int2string(i)+"] = "+assump[i].toString()
00774 +"\n\n phi = "+phi.getExpr().toString());
00775 }
00776 }
00777
00778
00779 if(assump.size() == 0) return phi;
00780
00781 Assumptions a(phiAssump - assump);
00782 Proof pf;
00783 if(withProof()) {
00784 vector<Proof> u;
00785 for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
00786 i!=iend; ++i) {
00787 const Theorem& t = phiAssump[*i];
00788 u.push_back(t.getProof());
00789 }
00790
00791
00792
00793 vector<Expr> args;
00794 vector<Proof> pfs;
00795 args.push_back(phi.getExpr());
00796 args.insert(args.end(), assump.begin(), assump.end());
00797
00798 pfs.push_back(newPf(u, assump, phi.getProof()));
00799 pf = newPf("impl_intro", args, pfs);
00800 }
00801 Expr conj(andExpr(assump));
00802 return newTheorem(conj.impExpr(phi.getExpr()), a, pf);
00803 }
00804
00805
00806
00807 Theorem CommonTheoremProducer::implContrapositive(const Theorem& thm) {
00808 const Expr& impl = thm.getExpr();
00809 if(CHECK_PROOFS) {
00810 CHECK_SOUND(impl.isImpl() && impl.arity()==2,
00811 "CommonTheoremProducer::implContrapositive: thm="
00812 +impl.toString());
00813 }
00814 Proof pf;
00815 if(withProof())
00816 pf = newPf("impl_contrapositive", impl, thm.getProof());
00817 return newTheorem(impl[1].negate().impExpr(impl[0].negate()), thm.getAssumptionsRef(), pf);
00818 }
00819
00820
00821
00822 Theorem CommonTheoremProducer::notToIff(const Theorem& not_e)
00823 {
00824 if(CHECK_PROOFS)
00825 CHECK_SOUND(not_e.getExpr().isNot(),
00826 "notToIff: not NOT: "+not_e.toString());
00827
00828
00829 Expr e(not_e.getExpr()[0]);
00830 Proof pf;
00831 if(withProof())
00832 pf=newPf("not_to_iff", e, not_e.getProof());
00833 return newRWTheorem(e, d_em->falseExpr(), not_e.getAssumptionsRef(), pf);
00834 }
00835
00836
00837
00838 Theorem CommonTheoremProducer::xorToIff(const Expr& e)
00839 {
00840 if(CHECK_PROOFS) {
00841 CHECK_SOUND(e.isXor(), "xorToIff precondition violated");
00842 CHECK_SOUND(e.arity() == 2, "Expected XOR of arity 2");
00843 }
00844 Proof pf;
00845 if(withProof()) {
00846 pf = newPf("xorToIff");
00847 }
00848 return newRWTheorem(e, e[0].iffExpr(!e[1]), Assumptions::emptyAssump(), pf);
00849 }
00850
00851
00852
00853 Theorem CommonTheoremProducer::rewriteIff(const Expr& e) {
00854 Proof pf;
00855 if(CHECK_PROOFS)
00856 CHECK_SOUND(e.isIff(), "rewriteIff precondition violated");
00857 if(withProof()) {
00858 pf = newPf("rewrite_iff", e[0], e[1]);
00859 }
00860
00861 if(e[0] == e[1]) return rewriteReflexivity(e);
00862
00863 switch(e[0].getKind()) {
00864 case TRUE_EXPR:
00865 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
00866 case FALSE_EXPR:
00867 return newRWTheorem(e, !e[1], Assumptions::emptyAssump() ,pf);
00868 case NOT:
00869 if(e[0][0]==e[1])
00870 return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00871 break;
00872 default: break;
00873 }
00874
00875 switch(e[1].getKind()) {
00876 case TRUE_EXPR:
00877 return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
00878 case FALSE_EXPR:
00879 return newRWTheorem(e, !e[0], Assumptions::emptyAssump(), pf);
00880 case NOT:
00881 if(e[0]==e[1][0])
00882 return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00883 break;
00884 default:
00885 break;
00886 }
00887
00888 if(e[0] < e[1])
00889 return rewriteUsingSymmetry(e);
00890 else
00891 return reflexivityRule(e);
00892 }
00893
00894
00895
00896
00897
00898
00899
00900
00901 Theorem CommonTheoremProducer::rewriteAnd(const Expr& e) {
00902 if(CHECK_PROOFS)
00903 CHECK_SOUND(e.isAnd(), "rewriteAnd: bad Expr: " + e.toString());
00904 Proof pf;
00905 ExprMap<bool> newKids;
00906 bool isFalse (false);
00907 for (Expr::iterator k=e.begin(), kend=e.end(); !isFalse && k != kend; ++k) {
00908 const Expr& ek = *k;
00909 if (ek.isFalse()) { isFalse=true; break; }
00910 if (ek.isAnd() && ek.arity() < 10) {
00911 for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
00912 if(newKids.count(j->negate()) > 0) { isFalse=true; break; }
00913 newKids[*j]=true;
00914 }
00915 } else if(!ek.isTrue()) {
00916 if(newKids.count(ek.negate()) > 0) { isFalse=true; break; }
00917 newKids[ek]=true;
00918 }
00919 }
00920 Expr res;
00921 if (isFalse) res = d_em->falseExpr();
00922 else if (newKids.size() == 0) res = d_em->trueExpr();
00923 else if (newKids.size() == 1)
00924 res = newKids.begin()->first;
00925 else {
00926 vector<Expr> v;
00927 for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
00928 i!=iend; ++i)
00929 v.push_back(i->first);
00930 res = andExpr(v);
00931 }
00932 if(withProof()) {
00933 pf = newPf("rewrite_and", e,res);
00934 }
00935 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
00936 }
00937
00938
00939
00940 Theorem CommonTheoremProducer::rewriteOr(const Expr& e) {
00941 if(CHECK_PROOFS)
00942 CHECK_SOUND(e.isOr(), "rewriteOr: bad Expr: " + e.toString());
00943 Proof pf;
00944 ExprMap<bool> newKids;
00945 bool isTrue (false);
00946 for (Expr::iterator k=e.begin(), kend=e.end(); !isTrue && k != kend; ++k) {
00947 const Expr& ek = *k;
00948 if (ek.isTrue()) { isTrue=true; break; }
00949 else if (ek.isOr() && ek.arity() < 10) {
00950 for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
00951 if(newKids.count(j->negate()) > 0) { isTrue=true; break; }
00952 newKids[*j]=true;
00953 }
00954 } else if(!ek.isFalse()) {
00955 if(newKids.count(ek.negate()) > 0) { isTrue=true; break; }
00956 newKids[ek]=true;
00957 }
00958 }
00959 Expr res;
00960 if (isTrue) res = d_em->trueExpr();
00961 else if (newKids.size() == 0) res = d_em->falseExpr();
00962 else if (newKids.size() == 1) res = newKids.begin()->first;
00963 else {
00964 vector<Expr> v;
00965 for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
00966 i!=iend; ++i)
00967 v.push_back(i->first);
00968 res = orExpr(v);
00969 }
00970 if(withProof()) {
00971 pf = newPf("rewrite_or", e, res);
00972 }
00973 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
00974 }
00975
00976
00977
00978 Theorem CommonTheoremProducer::rewriteNotTrue(const Expr& e) {
00979 Proof pf;
00980 if(CHECK_PROOFS)
00981 CHECK_SOUND(e.isNot() && e[0].isTrue(),
00982 "rewriteNotTrue precondition violated");
00983 if(withProof())
00984 pf = newPf("rewrite_not_true");
00985 return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00986 }
00987
00988
00989
00990 Theorem CommonTheoremProducer::rewriteNotFalse(const Expr& e) {
00991 Proof pf;
00992 if(CHECK_PROOFS)
00993 CHECK_SOUND(e.isNot() && e[0].isFalse(),
00994 "rewriteNotFalse precondition violated");
00995 if(withProof())
00996 pf = newPf("rewrite_not_false");
00997 return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
00998 }
00999
01000
01001
01002 Theorem CommonTheoremProducer::rewriteNotNot(const Expr& e) {
01003 Proof pf;
01004 if(CHECK_PROOFS)
01005 CHECK_SOUND(e.isNot() && e[0].isNot(),
01006 "rewriteNotNot precondition violated");
01007 if(withProof())
01008 pf = newPf("rewrite_not_not", e[0][0]);
01009 return newRWTheorem(e, e[0][0], Assumptions::emptyAssump(), pf);
01010 }
01011
01012
01013
01014 Theorem CommonTheoremProducer::rewriteNotForall(const Expr& e) {
01015 if(CHECK_PROOFS) {
01016 CHECK_SOUND(e.isNot() && e[0].isForall(),
01017 "rewriteNotForall: expr must be NOT FORALL:\n"
01018 +e.toString());
01019 }
01020 Proof pf;
01021 if(withProof())
01022 pf = newPf("rewrite_not_forall", e);
01023 return newRWTheorem(e, d_em->newClosureExpr(EXISTS, e[0].getVars(),
01024 !e[0].getBody()), Assumptions::emptyAssump(), pf);
01025 }
01026
01027
01028
01029 Theorem CommonTheoremProducer::rewriteNotExists(const Expr& e) {
01030 if(CHECK_PROOFS) {
01031 CHECK_SOUND(e.isNot() && e[0].isExists(),
01032 "rewriteNotExists: expr must be NOT FORALL:\n"
01033 +e.toString());
01034 }
01035 Proof pf;
01036 if(withProof())
01037 pf = newPf("rewrite_not_exists", e);
01038 return newRWTheorem(e, d_em->newClosureExpr(FORALL, e[0].getVars(),
01039 !e[0].getBody()), Assumptions::emptyAssump(), pf);
01040 }
01041
01042
01043 Expr CommonTheoremProducer::skolemize(const Expr& e)
01044 {
01045 vector<Expr> vars;
01046 const vector<Expr>& boundVars = e.getVars();
01047 for(unsigned int i=0; i<boundVars.size(); i++) {
01048 Expr skolV(e.skolemExpr(i));
01049 Type tp(e.getVars()[i].getType());
01050 skolV.setType(tp);
01051 vars.push_back(skolV);
01052 }
01053 return(e.getBody().substExpr(boundVars, vars));
01054 }
01055
01056
01057 Theorem CommonTheoremProducer::skolemizeRewrite(const Expr& e)
01058 {
01059 Proof pf;
01060 if(CHECK_PROOFS) {
01061 CHECK_SOUND(e.isExists(), "skolemize rewrite called on non-existential: "
01062 + e.toString());
01063 }
01064 Expr skol = skolemize(e);
01065 if(withProof()) {
01066 Expr rw(e.iffExpr(skol));
01067 pf = newLabel(rw);
01068 }
01069 TRACE("quantlevel", "skolemize ", skol, "");
01070 return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
01071
01072 }
01073
01074
01075 Theorem CommonTheoremProducer::skolemizeRewriteVar(const Expr& e)
01076 {
01077 Proof pf;
01078 if(CHECK_PROOFS) {
01079 CHECK_SOUND(e.isExists(), "skolemizeRewriteVar("
01080 +e.toString()+")");
01081 }
01082
01083 const vector<Expr>& boundVars = e.getVars();
01084 const Expr& body = e.getBody();
01085
01086 if(CHECK_PROOFS) {
01087 CHECK_SOUND(boundVars.size()==1, "skolemizeRewriteVar("
01088 +e.toString()+")");
01089 CHECK_SOUND(body.isEq() || body.isIff(), "skolemizeRewriteVar("
01090 +e.toString()+")");
01091 const Expr& v = boundVars[0];
01092 CHECK_SOUND(body[1] == v, "skolemizeRewriteVar("
01093 +e.toString()+")");
01094 CHECK_SOUND(!(v.subExprOf(body[0])), "skolemizeRewriteVar("
01095 +e.toString()+")");
01096 }
01097
01098 Expr skolV(e.skolemExpr(0));
01099 Type tp(e.getVars()[0].getType());
01100 skolV.setType(tp);
01101
01102 Expr skol = Expr(body.getOp(), body[0], skolV);
01103
01104 if(withProof()) {
01105 Expr rw(e.iffExpr(skol));
01106 pf = newLabel(rw);
01107 }
01108 return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
01109 }
01110
01111
01112 Theorem CommonTheoremProducer::varIntroRule(const Expr& phi) {
01113
01114 Proof pf;
01115 const Expr boundVar = d_em->newBoundVarExpr(phi.getType());
01116
01117 Expr body;
01118 if(phi.getType().isBool())
01119 body = phi.iffExpr(boundVar);
01120 else
01121 body = phi.eqExpr(boundVar);
01122
01123 std::vector<Expr> v;
01124 v.push_back(boundVar);
01125 const Expr result = d_em->newClosureExpr(EXISTS, v, body);
01126
01127 if(withProof())
01128 pf = newPf("var_intro", phi, boundVar);
01129 return newTheorem(result, Assumptions::emptyAssump(), pf);
01130 }
01131
01132
01133 Theorem CommonTheoremProducer::skolemize(const Theorem& thm) {
01134 const Expr& e = thm.getExpr();
01135 if(e.isExists()) {
01136 TRACE("skolem", "Skolemizing existential:", "", "{");
01137 CDMap<Expr, Theorem>::iterator i=d_skolemized_thms.find(e),
01138 iend=d_skolemized_thms.end();
01139 if(i!=iend) {
01140 TRACE("skolem", "Skolemized theorem found in map: ", (*i).second, "}");
01141 return iffMP(thm, (*i).second);
01142 }
01143 Theorem skol = skolemizeRewrite(e);
01144 for(unsigned int i=0; i<e.getVars().size(); i++) {
01145 Expr skolV(e.skolemExpr(i));
01146 Type tp(e.getVars()[i].getType());
01147 skolV.setType(tp);
01148 }
01149 d_skolem_axioms.push_back(skol);
01150 d_skolemized_thms.insert(e, skol, 0);
01151 skol = iffMP(thm, skol);
01152 TRACE("skolem", "skolemized new theorem: ", skol, "}");
01153 return skol;
01154 }
01155 return thm;
01156 }
01157
01158
01159 Theorem CommonTheoremProducer::varIntroSkolem(const Expr& e) {
01160
01161 CDMap<Expr, Theorem>::iterator i=d_skolemVars.find(e),
01162 iend=d_skolemVars.end();
01163 if(i!=iend) return (*i).second;
01164
01165 Theorem thm = varIntroRule(e);
01166 const Expr& e2 = thm.getExpr();
01167 DebugAssert(e2.isExists() && e2.getVars().size()==1, "varIntroSkolem: e2 = "
01168 +e2.toString());
01169 Theorem skolThm;
01170
01171 CDMap<Expr, Theorem>::iterator j=d_skolemized_thms.find(e2),
01172 jend=d_skolemized_thms.end();
01173 if(j!=jend) {
01174 skolThm = (*i).second;
01175 } else {
01176 skolThm = skolemizeRewriteVar(e2);
01177 d_skolem_axioms.push_back(skolThm);
01178 d_skolemized_thms.insert(e2, skolThm, 0);
01179 }
01180 thm = iffMP(thm, skolThm);
01181 d_skolemVars.insert(e, thm, 0);
01182 return thm;
01183 }
01184
01185
01186
01187
01188
01189 Theorem CommonTheoremProducer::trueTheorem()
01190 {
01191 return iffTrueElim(reflexivityRule(d_em->trueExpr()));
01192 }
01193
01194
01195 Theorem CommonTheoremProducer::rewriteAnd(const Theorem& e)
01196 {
01197 return iffMP(e, rewriteAnd(e.getExpr()));
01198 }
01199
01200
01201 Theorem CommonTheoremProducer::rewriteOr(const Theorem& e)
01202 {
01203 return iffMP(e, rewriteOr(e.getExpr()));
01204 }
01205
01206
01207 Theorem CommonTheoremProducer::ackermann(const Expr& e1, const Expr& e2)
01208 {
01209 Proof pf;
01210 if(CHECK_PROOFS)
01211 CHECK_SOUND(e1.isApply() && e2.isApply() && e1.getOp() == e2.getOp(),
01212 "ackermann precondition violated");
01213 Expr hyp;
01214 int ar = e1.arity();
01215 if (ar == 1) {
01216 hyp = Expr(e1[0].eqExpr(e2[0]));
01217 }
01218 else {
01219 vector<Expr> vec;
01220 for (int i = 0; i != ar; ++i) {
01221 vec.push_back(e1[i].eqExpr(e2[i]));
01222 }
01223 hyp = Expr(AND, vec);
01224 }
01225 if(withProof())
01226 pf = newPf("ackermann", e1, e2);
01227 return newTheorem(hyp.impExpr(e1.eqExpr(e2)), Assumptions::emptyAssump(), pf);
01228 }