24 #define _CVC3_TRUSTED_
49 void CNF_TheoremProducer::getSmartClauses(
const Theorem& thm, vector<Theorem>& clauses)
52 vector<Theorem> assumptions;
63 TempVec.push_back(thm.
getExpr());
67 if (thm.
getExpr() == assumptions[i].getExpr()) {
69 if (!(assumptions[i].isAssump())) {
70 getSmartClauses(assumptions[i], clauses);
74 TempVec.push_back(assumptions[i].getExpr().negate());
75 pfs.push_back(assumptions[i].getProof());
79 if (TempVec.size() == 1){
81 pf = newPf(
"learned_clause_smart", TempVec[0], pfs);
83 thm2 = newTheorem(TempVec[0], Assumptions::emptyAssump(), pf);
85 else if (TempVec.size() > 1) {
87 pf = newPf(
"learned_clause_smart",
Expr(
OR, TempVec), pfs);
89 thm2 = newTheorem(
Expr(
OR, TempVec), Assumptions::emptyAssump(), pf);
95 clauses.push_back(thm2);
98 for (vector<Theorem>::iterator itr = assumptions.begin(); itr != assumptions.end(); itr++) {
99 if (!((*itr).isAssump())) {
100 getSmartClauses((*itr), clauses);
106 void CNF_TheoremProducer::learnedClauses(
const Theorem& thm,
107 vector<Theorem>& clauses,
110 IF_DEBUG(
if(debugger.trace(
"cnf proofs")) {
111 ostream& os = debugger.getOS();
112 os <<
"learnedClause {" <<
endl;
116 if (!newLemma && d_smartClauses) {
117 getSmartClauses(thm, clauses);
126 vector<Expr> assumptions;
130 vector<Expr>::iterator iend = assumptions.end();
131 for (vector<Expr>::iterator i = assumptions.begin();
133 DebugAssert(i->isAbsLiteral(),
"Expected only literal assumptions");
137 assumptions.push_back(thm.
getExpr());
139 DebugAssert(assumptions.size() > 0,
"Expected at least one entry");
142 if (assumptions.size() == 1) {
144 pf = newPf(
"learned_clause", thm.
getProof());
146 thm2 = newTheorem(assumptions[0], Assumptions::emptyAssump(), pf);
151 pf = newPf(
"learned_clause", thm.
getProof());
153 thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf);
156 clauses.push_back(thm2);
208 Theorem CNF_TheoremProducer::ifLiftRule(
const Expr& e,
int itePos) {
211 "CNF_TheoremProducer::ifLiftRule("
212 "input must be a Predicate: e = " + e.
toString()+
")");
215 "CNF_TheoremProducer::ifLiftRule("
216 "input does not have an ITE: e = " + e.
toString()+
")");
218 const Expr& ite = e[itePos];
219 const Expr& cond = ite[0];
220 const Expr& t1 = ite[1];
221 const Expr& t2 = ite[2];
225 "CNF_TheoremProducer::ifLiftRule("
226 "input does not have an ITE: e = " + e.
toString()+
")");
242 pf = newPf(
"if_lift_rule", e, resultITE, d_em->newRatExpr(itePos));
243 return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf);
250 const vector<Theorem>& thms) {
257 chs.push_back(d_em->newStringExpr(reason));
258 chs.push_back(before);
259 chs.push_back(after);
260 chs.push_back(d_em->newRatExpr(pos));
262 for(vector<Theorem>::const_iterator i = thms.begin(), iend= thms.end();
264 pfs.push_back((*i).getProof());
266 pf = newPf(
"CNF", chs, pfs );
272 const vector<Expr>& after,
273 const vector<Theorem>& thms,
275 DebugAssert(3 == after.size(),
"why this happens");
280 DebugAssert(thms[0].getRHS() == after[0] ,
"this never happens");
281 DebugAssert(thms[1].getRHS() == after[1] ,
"this never happens");
282 DebugAssert(thms[2].getRHS() == after[2] ,
"this never happens");
283 DebugAssert(thms[0].getLHS() == before[0] ,
"this never happens");
284 DebugAssert(thms[1].getLHS() == before[1] ,
"this never happens");
285 DebugAssert(thms[2].getLHS() == before[2] ,
"this never happens");
288 chs.push_back(before);
289 chs.push_back(after[0]);
290 chs.push_back(after[1]);
291 chs.push_back(after[2]);
292 chs.push_back(d_em->newRatExpr(pos));
294 pfs.push_back(thms[0].getProof());
295 pfs.push_back(thms[1].getProof());
296 pfs.push_back(thms[2].getProof());
297 pf = newPf(
"CNFITE", chs, pfs );
300 Expr newe0 = after[0];
303 return newTheorem(afterExpr,
Assumptions(thms), pf);