CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 *\file cnf_theorem_producer.cpp 00004 *\brief Implementation of CNF_TheoremProducer 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Thu Jan 5 05:49:24 2006 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 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 // class CNF_Manager trusted methods 00035 ///////////////////////////////////////////////////////////////////////////// 00036 00037 00038 CNF_Rules* CNF_Manager::createProofRules(TheoremManager* tm, const CLFlags& flags) { 00039 return new CNF_TheoremProducer(tm, flags); 00040 } 00041 00042 00043 ///////////////////////////////////////////////////////////////////////////// 00044 // Proof rules 00045 ///////////////////////////////////////////////////////////////////////////// 00046 00047 00048 00049 void CNF_TheoremProducer::getSmartClauses(const Theorem& thm, vector<Theorem>& clauses) 00050 { 00051 // DebugAssert(!thm.getExpr().isDeductionLiteral(), "Expected unproved expr"); 00052 vector<Theorem> assumptions; 00053 thm.clearAllFlags(); 00054 thm.GetSatAssumptions(assumptions); 00055 Proof pf; 00056 if (withProof()) { 00057 pf = newPf("learned_clause", thm.getProof()); 00058 } 00059 Theorem thm2; 00060 vector<Expr> TempVec; 00061 00062 if (!thm.getExpr().isFalse()) { 00063 TempVec.push_back(thm.getExpr()); 00064 } 00065 for (vector<Theorem>::size_type i = 0; i < assumptions.size(); i++) { 00066 if (thm.getExpr() == assumptions[i].getExpr()) { 00067 // skip this clause as it is trivial 00068 if (!(assumptions[i].isAssump())) { 00069 getSmartClauses(assumptions[i], clauses); 00070 } 00071 return; 00072 } 00073 TempVec.push_back(assumptions[i].getExpr().negate()); 00074 } 00075 00076 if (TempVec.size() == 1){ 00077 thm2 = newTheorem(TempVec[0], Assumptions::emptyAssump(), pf); 00078 } 00079 else if (TempVec.size() > 1) { 00080 thm2 = newTheorem(Expr(OR, TempVec), Assumptions::emptyAssump(), pf); 00081 } 00082 else { 00083 FatalAssert(false, "Should be unreachable"); 00084 } 00085 thm2.setQuantLevel(thm.getQuantLevel()); 00086 clauses.push_back(thm2); 00087 // thm.getExpr().setDeductionLiteral(); 00088 00089 for (vector<Theorem>::iterator itr = assumptions.begin(); itr != assumptions.end(); itr++) { 00090 if (!((*itr).isAssump())) {// && !(*itr).getExpr().isDeductionLiteral()) { 00091 getSmartClauses((*itr), clauses); 00092 } 00093 } 00094 } 00095 00096 00097 void CNF_TheoremProducer::learnedClauses(const Theorem& thm, 00098 vector<Theorem>& clauses, 00099 bool newLemma) 00100 { 00101 IF_DEBUG(if(debugger.trace("cnf proofs")) { 00102 ostream& os = debugger.getOS(); 00103 os << "learnedClause {" << endl; 00104 os << thm; 00105 }) 00106 00107 if (!newLemma && d_smartClauses) { 00108 getSmartClauses(thm, clauses); 00109 return; 00110 } 00111 00112 // if (newLemma || d_flags["dynack"].getInt() <= 0) { 00113 // if (NewClausel == true) { 00114 // return; 00115 // } 00116 00117 vector<Expr> assumptions; 00118 Proof pf; 00119 thm.getLeafAssumptions(assumptions, true /*negate*/); 00120 00121 vector<Expr>::iterator iend = assumptions.end(); 00122 for (vector<Expr>::iterator i = assumptions.begin(); 00123 i != iend; ++i) { 00124 DebugAssert(i->isAbsLiteral(), "Expected only literal assumptions"); 00125 } 00126 00127 if (!thm.getExpr().isFalse()) 00128 assumptions.push_back(thm.getExpr()); 00129 00130 DebugAssert(assumptions.size() > 0, "Expected at least one entry"); 00131 00132 Theorem thm2; 00133 if (assumptions.size() == 1) { 00134 if(withProof()) { 00135 pf = newPf("learned_clause", assumptions[0], thm.getProof()); 00136 } 00137 thm2 = newTheorem(assumptions[0], Assumptions::emptyAssump(), pf); 00138 } 00139 else { 00140 Expr clauseExpr = Expr(OR, assumptions); 00141 if(withProof()) { 00142 pf = newPf("learned_clause", clauseExpr, thm.getProof()); 00143 } 00144 thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf); 00145 } 00146 thm2.setQuantLevel(thm.getQuantLevel()); 00147 clauses.push_back(thm2); 00148 // } 00149 // else { 00150 00151 // vector<Expr> congruences; 00152 00153 // thm.getAssumptionsAndCong(assumptions, congruences, true /*negate*/); 00154 00155 // vector<Expr>::iterator i = assumptions.begin(), iend = assumptions.end(); 00156 // for (; i != iend; ++i) { 00157 // DebugAssert(i->isAbsLiteral(), "Expected only literal assumptions"); 00158 // } 00159 00160 // if (!thm.getExpr().isFalse()) 00161 // assumptions.push_back(thm.getExpr()); 00162 00163 // if(withProof()) { 00164 // pf = newPf("learned_clause", thm.getProof()); 00165 // } 00166 00167 // DebugAssert(assumptions.size() > 0, "Expected at least one entry"); 00168 00169 // Theorem thm2; 00170 // if (assumptions.size() == 1) { 00171 // Expr clauseExpr = assumptions[0]; 00172 // if(withProof()) { 00173 // pf = newPf("learned_clause", clauseExpr, thm.getProof()); 00174 // } 00175 // thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf); 00176 // } 00177 // else { 00178 // Expr clauseExpr = Expr(OR, assumptions); 00179 // if(withProof()) { 00180 // pf = newPf("learned_clause", clauseExpr, thm.getProof()); 00181 // } 00182 // thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf); 00183 // } 00184 // thm2.setQuantLevel(thm.getQuantLevel()); 00185 // clauses.push_back(thm2); 00186 00187 // for (i = congruences.begin(), iend = congruences.end(); i != iend; ++i) { 00188 // if (withProof()) { 00189 // pf = newPf("congruence", *i); 00190 // } 00191 // thm2 = newTheorem(*i, Assumptions::emptyAssump(), pf); 00192 // thm2.setQuantLevel(thm.getQuantLevel()); 00193 // clauses.push_back(thm2); 00194 // } 00195 // } 00196 } 00197 00198 00199 Theorem CNF_TheoremProducer::ifLiftRule(const Expr& e, int itePos) { 00200 if(CHECK_PROOFS) { 00201 CHECK_SOUND(e.getType().isBool(), 00202 "CNF_TheoremProducer::ifLiftRule(" 00203 "input must be a Predicate: e = " + e.toString()+")"); 00204 CHECK_SOUND(itePos >= 0, "itePos negative"+int2string(itePos)); 00205 CHECK_SOUND(e.arity() > itePos && e[itePos].isITE(), 00206 "CNF_TheoremProducer::ifLiftRule(" 00207 "input does not have an ITE: e = " + e.toString()+")"); 00208 } 00209 const Expr& ite = e[itePos]; 00210 const Expr& cond = ite[0]; 00211 const Expr& t1 = ite[1]; 00212 const Expr& t2 = ite[2]; 00213 00214 if(CHECK_PROOFS) { 00215 CHECK_SOUND(cond.getType().isBool(), 00216 "CNF_TheoremProducer::ifLiftRule(" 00217 "input does not have an ITE: e = " + e.toString()+")"); 00218 } 00219 00220 vector<Expr> k1 = e.getKids(); 00221 Op op(e.getOp()); 00222 00223 k1[itePos] = t1; 00224 Expr pred1 = Expr(op, k1); 00225 00226 k1[itePos] = t2; 00227 Expr pred2 = Expr(op, k1); 00228 00229 Expr resultITE = cond.iteExpr(pred1, pred2); 00230 00231 Proof pf; 00232 if (withProof()) 00233 pf = newPf("if_lift_rule", e, resultITE, d_em->newRatExpr(itePos)); 00234 return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf); 00235 } 00236 00237 Theorem CNF_TheoremProducer::CNFtranslate(const Expr& before, 00238 const Expr& after, 00239 std::string reason, 00240 int pos) { 00241 //well, this is assert the e as a theorem without any justification. 00242 //change this as soon as possible 00243 00244 Proof pf; 00245 if (withProof()){ 00246 vector<Expr> chs ; 00247 chs.push_back(before); 00248 chs.push_back(after); 00249 chs.push_back(d_em->newRatExpr(pos)); 00250 pf = newPf("CNF", d_em->newStringExpr(reason), chs ); 00251 } 00252 return newTheorem(after, Assumptions::emptyAssump(), pf); 00253 } 00254 00255 Theorem CNF_TheoremProducer::CNFITEtranslate(const Expr& before, 00256 const vector<Expr>& after, 00257 const vector<Theorem>& thms, 00258 int pos){ 00259 DebugAssert(3 == after.size(), "why this happens"); 00260 DebugAssert(3 == thms.size(), "why this happens"); 00261 00262 Proof pf; 00263 if (withProof()){ 00264 DebugAssert(thms[0].getRHS() == after[0] , "this never happens"); 00265 DebugAssert(thms[1].getRHS() == after[1] , "this never happens"); 00266 DebugAssert(thms[2].getRHS() == after[2] , "this never happens"); 00267 DebugAssert(thms[0].getLHS() == before[0] , "this never happens"); 00268 DebugAssert(thms[1].getLHS() == before[1] , "this never happens"); 00269 DebugAssert(thms[2].getLHS() == before[2] , "this never happens"); 00270 00271 vector<Expr> chs ; 00272 chs.push_back(before); 00273 chs.push_back(after[0]); 00274 chs.push_back(after[1]); 00275 chs.push_back(after[2]); 00276 chs.push_back(d_em->newRatExpr(pos)); 00277 vector<Proof> pfs; 00278 pfs.push_back(thms[0].getProof()); 00279 pfs.push_back(thms[1].getProof()); 00280 pfs.push_back(thms[2].getProof()); 00281 pf = newPf("CNFITE", chs, pfs ); 00282 } 00283 00284 Expr newe0 = after[0]; 00285 Expr afterExpr = newe0.iteExpr(after[1],after[2]); 00286 //we should produce a newRWTheorm whenever possible and then use iffmp rule to get the desired result 00287 return newTheorem(afterExpr, Assumptions(thms), pf); 00288 } 00289 00290 00291 00292 00293 00294 // because the way of cnf translation, add unit means the theorem from other parts of cvc3, not from cnf translation 00295 Theorem CNF_TheoremProducer::CNFAddUnit(const Theorem& thm){ 00296 00297 //wrap the thm so the hol light translator know this 00298 Proof pf; 00299 if (withProof()){ 00300 pf = newPf("cnf_add_unit", thm.getExpr(), thm.getProof() ); 00301 } 00302 return newTheorem(thm.getExpr(), thm.getAssumptionsRef(), pf); 00303 } 00304 00305 Theorem CNF_TheoremProducer::CNFConvert(const Expr& e, const Theorem& thm){ 00306 00307 //wrap the thm so the hol light translator know this 00308 Proof pf; 00309 if (withProof()){ 00310 pf = newPf("cnf_convert", e, thm.getExpr(), thm.getProof() ); 00311 } 00312 DebugAssert(thm.getExpr().isOr(),"convert is not or exprs"); 00313 return newTheorem(thm.getExpr(), thm.getAssumptionsRef(), pf); 00314 } 00315 00316