00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include "cnf_manager.h"
00023
00024 #define _CVC3_TRUSTED_
00025 #include "cnf_theorem_producer.h"
00026
00027
00028 using namespace std;
00029 using namespace CVC3;
00030 using namespace SAT;
00031
00032
00033
00034
00035
00036
00037
00038 CNF_Rules* CNF_Manager::createProofRules(TheoremManager* tm) {
00039 return new CNF_TheoremProducer(tm);
00040 }
00041
00042
00043
00044
00045
00046
00047
00048 Theorem CNF_TheoremProducer::learnedClause(const Theorem& thm)
00049 {
00050 IF_DEBUG(if(debugger.trace("cnf proofs")) {
00051 ostream& os = debugger.getOS();
00052 os << "learnedClause {" << endl;
00053 os << thm;
00054 });
00055
00056 if(CHECK_PROOFS) {
00057 CHECK_SOUND(withAssumptions(),
00058 "learnedClause: called while running without assumptions");
00059 }
00060
00061 vector<Expr> assumptions;
00062
00063 thm.getLeafAssumptions(assumptions, true );
00064
00065 vector<Expr>::iterator iend = assumptions.end();
00066 for (vector<Expr>::iterator i = assumptions.begin();
00067 i != iend; ++i) {
00068 DebugAssert(i->isAbsLiteral(), "Expected only literal assumptions");
00069 }
00070
00071 if (!thm.getExpr().isFalse())
00072 assumptions.push_back(thm.getExpr());
00073
00074 Proof pf;
00075
00076 if(withProof()) {
00077 pf = newPf("learned_clause", thm.getProof());
00078 }
00079
00080
00081 DebugAssert(assumptions.size() > 0, "Expected at least one entry");
00082
00083 Theorem thm2;
00084 if (assumptions.size() == 1) {
00085 thm2 = newTheorem(assumptions[0], Assumptions::emptyAssump(), pf);
00086 }
00087 else {
00088 thm2 = newTheorem(Expr(OR, assumptions), Assumptions::emptyAssump(), pf);
00089 }
00090 thm2.setQuantLevel(thm.getQuantLevel());
00091 return thm2;
00092 }
00093
00094
00095 Theorem CNF_TheoremProducer::ifLiftRule(const Expr& e, int itePos) {
00096 if(CHECK_PROOFS) {
00097 CHECK_SOUND(e.getType().isBool(),
00098 "CNF_TheoremProducer::ifLiftRule("
00099 "input must be a Predicate: e = " + e.toString()+")");
00100 CHECK_SOUND(itePos >= 0, "itePos negative"+int2string(itePos));
00101 CHECK_SOUND(e.arity() > itePos && e[itePos].isITE(),
00102 "CNF_TheoremProducer::ifLiftRule("
00103 "input does not have an ITE: e = " + e.toString()+")");
00104 }
00105 const Expr& ite = e[itePos];
00106 const Expr& cond = ite[0];
00107 const Expr& t1 = ite[1];
00108 const Expr& t2 = ite[2];
00109
00110 if(CHECK_PROOFS) {
00111 CHECK_SOUND(cond.getType().isBool(),
00112 "CNF_TheoremProducer::ifLiftRule("
00113 "input does not have an ITE: e = " + e.toString()+")");
00114 }
00115
00116 vector<Expr> k1 = e.getKids();
00117 Op op(e.getOp());
00118
00119 k1[itePos] = t1;
00120 Expr pred1 = Expr(op, k1);
00121
00122 k1[itePos] = t2;
00123 Expr pred2 = Expr(op, k1);
00124
00125 Expr resultITE = cond.iteExpr(pred1, pred2);
00126
00127 Proof pf;
00128 if (withProof())
00129 pf = newPf("if_lift_rule", e, d_em->newRatExpr(itePos));
00130 return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf);
00131 }