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 "datatype_theorem_producer.h"
00028 #include "theory_datatype.h"
00029 #include "theory_core.h"
00030
00031
00032 using namespace std;
00033 using namespace CVC3;
00034
00035
00036
00037
00038
00039
00040
00041 DatatypeProofRules*
00042 TheoryDatatype::createProofRules() {
00043 return new DatatypeTheoremProducer(this);
00044 }
00045
00046
00047
00048
00049
00050
00051
00052 Theorem DatatypeTheoremProducer::dummyTheorem(const CDList<Theorem>& facts,
00053 const Expr& e) {
00054 vector<Theorem> thmVec;
00055 for (unsigned i = 0; i < facts.size(); ++i)
00056 thmVec.push_back(facts[i]);
00057 Assumptions a(thmVec);
00058 Proof pf;
00059 return newTheorem(e, a, pf);
00060 }
00061
00062
00063 Theorem DatatypeTheoremProducer::rewriteSelCons(const CDList<Theorem>& facts,
00064 const Expr& e) {
00065 if (CHECK_PROOFS) {
00066 CHECK_SOUND(isSelector(e), "Selector expected");
00067 CHECK_SOUND(d_theoryDatatype->canCollapse(e), "Expected canCollapse");
00068 }
00069 Proof pf;
00070 Expr t;
00071
00072 pair<Expr, unsigned> selectorInfo =
00073 d_theoryDatatype->getSelectorInfo(e.getOpExpr());
00074 if (isConstructor(e[0]) &&
00075 selectorInfo.first == getConstructor(e[0])) {
00076 t = e[0][selectorInfo.second];
00077 }
00078 else {
00079 Expr selTypeExpr = e.getOpExpr().getType().getExpr();
00080 Type type = Type(selTypeExpr[selTypeExpr.arity()-1]);
00081 t = d_theoryDatatype->getConstant(type);
00082 }
00083
00084 if (withProof()) pf = newPf("rewriteSelCons", e, t);
00085
00086 if (!isConstructor(e[0])) {
00087 vector<Theorem> thmVec;
00088 for (unsigned i = 0; i < facts.size(); ++i)
00089 thmVec.push_back(facts[i]);
00090 Assumptions a(thmVec);
00091 return newRWTheorem(e, t, a, pf);
00092 }
00093 else {
00094 return newRWTheorem(e, t, Assumptions::emptyAssump(), pf);
00095 }
00096 }
00097
00098
00099 Theorem DatatypeTheoremProducer::rewriteTestCons(const Expr& e) {
00100 if (CHECK_PROOFS) {
00101 CHECK_SOUND(isTester(e), "Tester expected");
00102 CHECK_SOUND(isConstructor(e[0]), "Expected Test(Cons)");
00103 }
00104 Proof pf;
00105 Expr t;
00106 Expr cons = d_theoryDatatype->getConsForTester(e.getOpExpr());
00107 if (cons == getConstructor(e[0])) {
00108 t = d_theoryDatatype->trueExpr();
00109 }
00110 else {
00111 t = d_theoryDatatype->falseExpr();
00112 }
00113 if (withProof()) pf = newPf("rewriteTestCons", e, t);
00114 return newRWTheorem(e, t, Assumptions::emptyAssump(), pf);
00115 }
00116
00117
00118 Theorem DatatypeTheoremProducer::decompose(const Theorem& e) {
00119 if (CHECK_PROOFS) {
00120 CHECK_SOUND(e.isRewrite(), "decompose: expected rewrite");
00121 }
00122 const Expr& lhs = e.getLHS();
00123 const Expr& rhs = e.getRHS();
00124 if(CHECK_PROOFS) {
00125 CHECK_SOUND(isConstructor(lhs) && isConstructor(rhs) &&
00126 lhs.isApply() && rhs.isApply() &&
00127 lhs.getOpExpr() == rhs.getOpExpr() &&
00128 lhs.arity() > 0 && lhs.arity() == rhs.arity(),
00129 "decompose precondition violated");
00130 }
00131 Assumptions a(e);
00132 Proof pf;
00133 Expr res = lhs[0].eqExpr(rhs[0]);
00134 if (lhs.arity() > 1) {
00135 vector<Expr> args;
00136 args.push_back(res);
00137 for (int i = 1; i < lhs.arity(); ++i) {
00138 args.push_back(lhs[i].eqExpr(rhs[i]));
00139 }
00140 res = andExpr(args);
00141 }
00142 if (withProof()) pf = newPf("decompose", e.getProof());
00143 return newTheorem(res, a, pf);
00144 }
00145
00146
00147 Theorem DatatypeTheoremProducer::noCycle(const Expr& e) {
00148 if (CHECK_PROOFS) {
00149 CHECK_SOUND(isConstructor(e) && e.isApply() && e.arity() > 0,
00150 "noCycle: expected constructor with children");
00151 }
00152 Proof pf;
00153
00154 Type t = e.getOpExpr().getType();
00155 t = t[t.arity()-1];
00156 const Op& reach = d_theoryDatatype->getReachablePredicate(t);
00157
00158 vector<Expr> args;
00159 args.push_back(!Expr(reach, e, e));
00160 for (int i = 0; i < e.arity(); ++i) {
00161 if (isDatatype(e[i].getType()) &&
00162 d_theoryDatatype->getReachablePredicate(e[i].getType()) == reach)
00163 args.push_back(Expr(reach, e, e[i]));
00164 }
00165
00166 if (withProof()) pf = newPf("noCycle", e);
00167 return newTheorem(andExpr(args), Assumptions::emptyAssump(), pf);
00168 }