24 #define _CVC3_TRUSTED_
42 d_skolemized_thms(tm->getCM()->getCurrentContext()),
43 d_skolemVars(tm->getCM()->getCurrentContext())
72 args.push_back(D_phi.
getExpr());
75 pf =
newPf(
"queryTCC", args, pfs);
86 const std::vector<Expr>& assump,
87 const vector<Theorem>& tccs) {
92 "implIntro3: called while running without assumptions");
99 "implIntro3: number of assumptions ("
100 +
int2string(assump.size())+
") and number of TCCs ("
102 +
") does not match");
103 for(
size_t i=0; i<assump.size(); i++) {
104 const Theorem& thm = phiAssump[assump[i]];
106 "implIntro3: this is not an assumption of phi:\n\n"
107 " a["+
int2string(i)+
"] = "+assump[i].toString()
120 if(assump.size() == 0)
return phi;
128 for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
130 const Theorem& t = phiAssump[*i];
139 args.insert(args.end(), assump.begin(), assump.end());
140 for(vector<Theorem>::const_iterator i=tccs.begin(), iend=tccs.end();
142 args.push_back(i->getExpr());
143 pfs.push_back(i->getProof());
147 pf =
newPf(
"impl_intro_3", args, pfs);
171 "rewriteReflexivity: wrong expression: "
177 "rewriteReflexivity: t[0] has no type: "
179 pf =
newPf(
"rewrite_eq_refl", t[0].getType().getExpr(), t[0]);
181 pf =
newPf(
"rewrite_iff_refl", t[0]);
190 (
"CVC3::CommonTheoremProducer: "
191 "theorem is not an equality or iff:\n "
204 Type t = a1.getType();
207 bool isEquality = !t.
isBool();
222 bool isIff = a1_eq_a2.
isIff();
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];
232 Type t = a1.getType();
234 "rewriteUsingSymmetry: a1 has no type: " + a1.toString());
236 pf =
newPf(
"rewrite_iff_symm", a1, a2);
251 "CVC3::CommonTheoremProducer::transitivityRule:\n "
252 "Wrong premises: first = "
256 "CVC3::CommonTheoremProducer::transitivityRule:\n "
257 "Wrong premises: first = "
271 if(a1 == a2)
return a2_eq_a3;
272 if(a2 == a3)
return a1_eq_a2;
283 bool isEquality = (!t.
isBool());
284 string name((isEquality)?
"eq_trans" :
"iff_trans");
288 "Type is not computed for a1: " + a1.
toString());
290 if(isEquality) args.push_back(t.
getExpr());
296 pf =
newPf(name, args, pfs);
306 accum0(debugger.timer(
"substitutivityRule0 time"));
307 static DebugTimer tmpTimer(debugger.newTimer());
308 static DebugCounter count(debugger.counter(
"substitutivityRule0 calls"));
309 debugger.setCurrentTime(tmpTimer);
315 "Unexpected use of substitutivityRule0");
317 "CVC3::CommonTheoremProducer::substitutivityRule0:\n "
318 "premis is not an equality or IFF: "
337 accum0(debugger.timer(
"substitutivityRule1 time"));
338 static DebugTimer tmpTimer(debugger.newTimer());
339 static DebugCounter count(debugger.counter(
"substitutivityRule1 calls"));
340 debugger.setCurrentTime(tmpTimer);
347 "Unexpected use of substitutivityRule1");
349 "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
350 "premis is not an equality or IFF: "
354 "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
355 "premis is not an equality or IFF: "
365 pf =
newPf(
"basic_subst_op1", e, e2, pfs);
374 const vector<Theorem>& thms) {
377 accum0(debugger.timer(
"substitutivityRule time"));
378 static DebugTimer tmpTimer(debugger.newTimer());
379 static DebugCounter count(debugger.counter(
"substitutivityRule calls"));
380 debugger.setCurrentTime(tmpTimer);
383 unsigned size(thms.size());
392 c.reserve(size); d.reserve(size);
393 for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
398 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
399 "premis is not an equality or IFF: "
400 + i->getExpr().toString()
403 c.push_back(i->getLHS());
404 d.push_back(i->getRHS());
405 if(
withProof()) pfs.push_back(i->getProof());
407 Expr e1(op, c), e2(op, d);
415 pf =
newPf(
"basic_subst_op",e1,e2,pfs);
417 IF_DEBUG(debugger.setElapsed(tmpTimer);
425 const vector<unsigned>& changed,
426 const vector<Theorem>& thms) {
429 accum0(debugger.timer(
"substitutivityRule2 time"));
430 static DebugTimer tmpTimer(debugger.newTimer());
431 static DebugCounter count(debugger.counter(
"substitutivityRule2 calls"));
432 debugger.setCurrentTime(tmpTimer);
434 DebugAssert(changed.size() > 0,
"substitutivityRule2 should not be called");
435 DebugAssert(changed.size() == thms.size(),
"substitutivityRule2: wrong args");
439 unsigned size = e.
arity();
441 unsigned csize = changed.size();
444 if (changed[0] == 0) {
451 DebugAssert(size >= csize,
"Bad call to substitutivityRule2");
455 for(
unsigned j = 0, k = 0; k < size; ++k) {
456 if (j == csize || changed[j] != k) {
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()
468 c.push_back(thms[j].getRHS());
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";
481 "substitutivityRule2 should not be called in this case:\n"
488 for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
493 "CVC3::CommonTheoremProducer::substitutivityRule:\n "
494 "premis is not an equality or IFF: "
495 + i->getExpr().toString());
497 pfs.push_back(i->getProof());
499 pf =
newPf(
"optimized_subst_op",e,e2,pfs);
502 IF_DEBUG(debugger.setElapsed(tmpTimer);
514 int size = e.
arity();
517 DebugAssert(size >= changed,
"Bad call to substitutivityRule");
522 "premise is not an equality or IFF: " + thm.
getExpr().
toString() +
"\n" +
527 for(
int k = 0; k < size; ++ k)
528 if (k != changed) c.push_back(e[k]);
529 else c.push_back(thm.
getRHS());
536 ostream& os = debugger.getOS();
537 os <<
"substitutivityRule: e = " << e <<
"\n e2 = " << e2 <<
endl;
541 DebugAssert(e != e2,
"substitutivityRule should not be called in this case:\ne = "+e.
toString());
566 "CommonTheoremProducer::contraditionRule: "
567 "theorems don't match:\n e = "+e.
toString()
584 pf =
newPf(
"excludedMiddle", e);
615 "CommonTheoremProducer::iffTrueElim: "
616 "theorem is not e<=>TRUE: "+ e.
toString());
629 "CommonTheoremProducer::iffFalseElim: "
630 "theorem is not e<=>FALSE: "+ e.
toString());
644 "CommonTheoremProducer::iffContrapositive: "
645 "theorem is not e1<=>e2: "+ e.
toString());
658 "CommonTheoremProducer::notNotElim: bad theorem: !!e = "
671 "iffMP: not IFF: "+e1_iff_e2.
toString());
673 "iffMP: theorems don't match:\n e1 = " + e1.
toString()
674 +
", e1_iff_e2 = " + e1_iff_e2.
toString());
678 if (e1_iff_e2.
getLHS() == e2)
return e1;
684 pfs.push_back(e1_iff_e2.
getProof());
697 "implMP: not IMPLIES: "+impl.
toString());
699 "implMP: theorems don't match:\n e1 = " + e1.
toString()
700 +
", e1_impl_e2 = " + impl.
toString());
702 const Expr& e2 = impl[1];
710 pfs.push_back(e1_impl_e2.
getProof());
734 vector<Theorem> thms;
745 "andIntro(vector<Theorem>): vector must have more than 1 element");
757 for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
759 kids.push_back(i->getExpr());
763 for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
765 pfs.push_back(i->getProof());
776 const std::vector<Expr>& assump) {
781 "implIntro: called while running without assumptions");
787 for(
size_t i=0; i<assump.size(); i++) {
788 const Theorem& thm = phiAssump[assump[i]];
790 "implIntro: this is not an assumption of phi:\n\n"
791 " a["+
int2string(i)+
"] = "+assump[i].toString()
797 if(assump.size() == 0)
return phi;
803 for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
805 const Theorem& t = phiAssump[*i];
814 args.insert(args.end(), assump.begin(), assump.end());
817 pf =
newPf(
"impl_intro", args, pfs);
829 "CommonTheoremProducer::implContrapositive: thm="
845 "rewriteIteTrue precondition violated");
852 pf =
newPf(
"rewrite_ite_true_iff", e[1], e[2]);
854 pf =
newPf(
"rewrite_ite_true", t.
getExpr(), e[1], e[2]);
867 "rewriteIteFalse precondition violated");
874 pf =
newPf(
"rewrite_ite_false_iff", e[1], e[2]);
876 pf =
newPf(
"rewrite_ite_false", t.
getExpr(), e[1], e[2]);
889 "rewriteIteSame precondition violated");
896 pf =
newPf(
"rewrite_ite_same_iff", e[0], e[1]);
898 pf =
newPf(
"rewrite_ite_same", t.
getExpr(), e[0], e[1]);
910 "notToIff: not NOT: "+not_e.
toString());
929 for (
int i = e.
arity()-2; i >=0; --i) {
930 res = (!e[i]).iffExpr(res);
934 pf =
newPf(
"xorToIff");
946 pf =
newPf(
"rewrite_iff", e[0], e[1]);
951 switch(e[0].getKind()) {
963 switch(e[1].getKind()) {
994 bool isFalse (
false);
997 if (ek.
isFalse()) { isFalse=
true;
break; }
1000 if(newKids.
count(j->negate()) > 0) { isFalse=
true;
break; }
1003 }
else if(!ek.
isTrue()) {
1004 if(newKids.
count(ek.
negate()) > 0) { isFalse=
true;
break; }
1011 else if (newKids.
size() == 1)
1012 res = newKids.
begin()->first;
1017 v.push_back(i->first);
1021 pf =
newPf(
"rewrite_and", e,res);
1033 bool isTrue (
false);
1035 const Expr& ek = *k;
1036 if (ek.
isTrue()) { isTrue=
true;
break; }
1037 else if (ek.
isOr() && ek.
arity() < 10) {
1039 if(newKids.
count(j->negate()) > 0) { isTrue=
true;
break; }
1043 if(newKids.
count(ek.
negate()) > 0) { isTrue=
true;
break; }
1050 else if (newKids.
size() == 1) res = newKids.
begin()->first;
1055 v.push_back(i->first);
1059 pf =
newPf(
"rewrite_or", e, res);
1070 "rewriteNotTrue precondition violated");
1072 pf =
newPf(
"rewrite_not_true");
1082 "rewriteNotFalse precondition violated");
1084 pf =
newPf(
"rewrite_not_false");
1094 "rewriteNotNot precondition violated");
1096 pf =
newPf(
"rewrite_not_not", e[0][0]);
1105 "rewriteNotForall: expr must be NOT FORALL:\n"
1110 pf =
newPf(
"rewrite_not_forall", e);
1120 "rewriteNotExists: expr must be NOT FORALL:\n"
1125 pf =
newPf(
"rewrite_not_exists", e);
1134 const vector<Expr>& boundVars = e.
getVars();
1135 for(
unsigned int i=0; i<boundVars.size(); i++) {
1139 vars.push_back(skolV);
1157 TRACE(
"quantlevel",
"skolemize ", skol,
"");
1158 TRACE(
"quantlevel sko",
"skolemize ", skol,
"");
1159 TRACE(
"quantlevel sko",
"skolemize from org ", e,
"");
1173 const vector<Expr>& boundVars = e.
getVars();
1177 CHECK_SOUND(boundVars.size()==1,
"skolemizeRewriteVar("
1181 const Expr& v = boundVars[0];
1184 CHECK_SOUND(!(v.subExprOf(body[0])),
"skolemizeRewriteVar("
1211 body = phi.
eqExpr(boundVar);
1213 std::vector<Expr> v;
1214 v.push_back(boundVar);
1218 pf =
newPf(
"var_intro", phi, boundVar);
1226 TRACE(
"skolem",
"Skolemizing existential:",
"",
"{");
1230 TRACE(
"skolem",
"Skolemized theorem found in map: ", (*i).second,
"}");
1231 return iffMP(thm, (*i).second);
1234 for(
unsigned int i=0; i<e.
getVars().size(); i++) {
1241 skol =
iffMP(thm, skol);
1243 TRACE(
"skolem",
"skolemized new theorem: ", skol,
"}");
1254 if(i!=iend)
return (*i).second;
1257 const Expr& e2 = thm.getExpr();
1265 skolThm = (*i).second;
1271 thm =
iffMP(thm, skolThm);
1303 "ackermann precondition violated");
1305 int ar = e1.
arity();
1307 hyp =
Expr(e1[0].eqExpr(e2[0]));
1311 for (
int i = 0; i != ar; ++i) {
1312 vec.push_back(e1[i].eqExpr(e2[i]));
1317 pf =
newPf(
"ackermann", e1, e2);
1335 for (; i < e.
arity(); ++i) {
1336 if (e[i].containsTermITE())
break;
1337 kids.push_back(e[i]);
1345 findITE(e[i], condition, t2, e2);
1348 for(
int k = i+1; k < e.
arity(); ++k) {
1349 kids.push_back(e[k]);
1365 Expr cond, thenpart, elsepart;
1367 findITE(e, cond, thenpart, elsepart);
1371 pf =
newPf(
"lift_one_ite", e);
Theorem liftOneITE(const Expr &e)
Theorem notNotElim(const Theorem &e)
iterator begin() const
Begin iterator.
void setSubst() const
Set flag stating that theorem is an instance of substitution.
Theorem newAssumption(const Expr &thm, const Proof &pf, int scope=-1)
Theorem iffTrue(const Theorem &e)
Data structure of expressions in CVC3.
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Theorem rewriteIteSame(const Expr &e)
==> ITE(c, e, e) == e
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Theorem rewriteIteTrue(const Expr &e)
==> ITE(TRUE, e1, e2) == e1
Theorem newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)
Create a new theorem. See also newRWTheorem() and newReflTheorem()
void findITE(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)
Helper function for liftOneITE.
Theorem trueTheorem()
==> TRUE
Theorem excludedMiddle(const Expr &e)
Theorem3 implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)
3-valued implication introduction rule:
void add(const std::vector< Theorem > &thms)
ExprManager * getEM() const
Theorem skolemizeRewrite(const Expr &e)
Theorem rewriteNotExists(const Expr &existsExpr)
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Theorem rewriteNotTrue(const Expr &e)
==> NOT TRUE IFF FALSE
Theorem newReflTheorem(const Expr &e)
Create a reflexivity theorem.
Theorem reflexivityRule(const Expr &a)
MS C++ specific settings.
bool containsTermITE() const
Return whether Expr contains a non-bool type ITE as a sub-term.
bool withProof()
Testing whether to generate proofs.
Expr eqExpr(const Expr &right) const
Theorem ackermann(const Expr &e1, const Expr &e2)
Theorem varIntroRule(const Expr &e)
|- EXISTS x. e = x
#define DebugAssert(cond, str)
Theorem rewriteReflexivity(const Expr &t)
==> (a == a) IFF TRUE
Theorem iffNotFalse(const Theorem &e)
#define CHECK_SOUND(cond, msg)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Theorem contradictionRule(const Theorem &e, const Theorem ¬_e)
Theorem iffTrueElim(const Theorem &e)
bool withAssumptions()
Testing whether to generate assumptions.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
std::vector< Theorem > d_skolem_axioms
Expr orExpr(const std::vector< Expr > &children)
CommonTheoremProducer(TheoremManager *tm)
Expr impExpr(const Expr &right) const
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Theorem3 queryTCC(const Theorem &phi, const Theorem &D_phi)
Convert 2-valued formula to 3-valued by discharging its TCC ( ): .
Op getOp() const
Get operator from expression.
CommonProofRules * createProofRules()
const Expr & getExpr() const
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
size_t count(const Expr &e) const
Theorem varIntroSkolem(const Expr &e)
Retrun a theorem "|- e = v" for a new Skolem constant v.
Theorem andIntro(const Theorem &e1, const Theorem &e2)
e1, e2 ==> AND(e1, e2)
std::string toString() const
Theorem rewriteNotFalse(const Expr &e)
==> NOT FALSE IFF TRUE
Theorem andElim(const Theorem &e, int i)
Theorem rewriteIteFalse(const Expr &e)
==> ITE(FALSE, e1, e2) == e2
std::string toString() const
Print the expression to a string.
Theorem implMP(const Theorem &e1, const Theorem &e1_impl_e2)
Expr skolemExpr(int i) const
Create a Skolem constant for the i'th variable of an existential (*this)
Theorem substitutivityRule(const Expr &e, const Theorem &thm)
Optimized case for expr with one child.
Expr iffExpr(const Expr &right) const
const Expr & falseExpr()
FALSE Expr.
Expr newLeafExpr(const Op &op)
Expr skolemize(const Expr &e)
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
Theorem rewriteNotForall(const Expr &forallExpr)
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
Proof newLabel(const Expr &e)
Create a new proof label (bound variable) for an assumption (formula)
const Expr & getRHS() const
const Expr & trueExpr()
TRUE Expr.
std::string toString() const
const Assumptions & getAssumptionsRef() const
Expr newRatExpr(const Rational &r)
Theorem3 newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)
CDMap< Expr, Theorem > d_skolemized_thms
Theorem skolemizeRewriteVar(const Expr &e)
Special version of skolemizeRewrite for "EXISTS x. t = x".
Expr orExpr(const Expr &right) const
CDMap< Expr, Theorem > d_skolemVars
Mapping of e to "|- e = v" for fresh Skolem vars v.
Theorem iffFalseElim(const Theorem &e)
Theorem xorToIff(const Expr &e)
Theorem newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
Create a rewrite theorem: lhs = rhs.
Theorem symmetryRule(const Theorem &a1_eq_a2)
(same for IFF)
Theorem assumpRule(const Expr &a, int scope=-1)
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(same for IFF)
const Expr & getLHS() const
Theorem implIntro(const Theorem &phi, const std::vector< Expr > &assump)
Implication introduction rule: .
Theorem rewriteIff(const Expr &e)
==> (e1 <=> e2) <=> [simplified expr]
Theorem implContrapositive(const Theorem &thm)
e1 => e2 ==> ~e2 => ~e1
Proof newPf(const std::string &name)
Theorem notToIff(const Theorem ¬_e)
Expr substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
Type getType() const
Get the type. Recursively compute if necessary.
static const Assumptions & emptyAssump()
Expr andExpr(const std::vector< Expr > &children)
Theorem rewriteNotNot(const Expr &e)
==> NOT NOT e IFF e, takes !!e
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
Theorem iffContrapositive(const Theorem &thm)
e1 <=> e2 ==> ~e1 <=> ~e2
const Assumptions & getAssumptionsRef() const
iterator end() const
End iterator.