31 #define _CVC3_TRUSTED_
46 SearchEngine::createRules() {
78 "proofByContradiction: pfFalse = : " + pfFalse.
toString());
86 if(!thm.isNull()) u = thm.getProof();
95 pf =
newPf(
"pf_by_contradiction", a,
109 "negIntro: pfFalse = : " + pfFalse.
toString());
119 if(!thm.isNull()) u = thm.getProof();
122 pf =
newPf(
"false_implies_anything", not_a, pfFalse.
getProof());
125 pf =
newPf(
"neg_intro", not_a,
137 const Theorem& not_a_proves_c) {
142 "caseSplit: conclusions differ:\n positive case C = "
143 + c.
toString() +
"\n negative case C = "
164 if (a1 == a3)
return a_proves_c;
165 if (a2 == a4)
return not_a_proves_c;
174 pfs.push_back(
newPf(a1[a].getProof(),
176 pfs.push_back(
newPf(a2[!a].getProof(),
178 pf =
newPf(
"case_split", a, c, pfs);
199 "SearchEngineTheoremProducer::conflictClause: "
200 "Found null theorem");
201 if (!i->isRefl() && !i->isFlagged()) {
203 if (m.count(*i) == 0) {
205 "SearchEngineTheoremProducer::conflictClause: "
206 "literal and gamma sets do not form a complete "
207 "cut of Theorem assumptions. Stray theorem: \n"
222 const vector<Theorem>& gamma) {
224 IF_DEBUG(
if(debugger.trace(
"search proofs")) {
225 ostream& os = debugger.getOS();
227 for(vector<Theorem>::const_iterator i=lits.begin(), iend=lits.end();
229 os << i->getExpr() <<
",\n";
230 os <<
"]\n\ngamma = [";
231 for(vector<Theorem>::const_iterator i=gamma.begin(), iend=gamma.end();
233 os << i->getExpr() <<
",\n";
240 "conflictClause: called while running without assumptions");
245 vector<Expr> literals;
247 literals.reserve(lits.size() + 1);
248 u.reserve(lits.size());
249 const vector<Theorem>::const_iterator iend = lits.end();
250 for(vector<Theorem>::const_iterator i=lits.begin(); i!=iend; ++i) {
251 Expr neg(i->getExpr().negate());
253 literals.push_back(neg);
254 if(
withProof()) u.push_back(i->getProof());
260 for(vector<Theorem>::const_iterator i = gamma.begin();
261 i != gamma.end(); ++i) {
267 for(vector<Theorem>::const_iterator i = lits.begin(); i!=iend; ++i) {
270 "SearchEngineTheoremProducer::conflictClause: "
271 "literal and gamma sets are not disjoint: lit = "
277 TheoremMap::iterator t = m.begin(), tend = m.end();
278 for (; t != tend; ++t) {
280 "SearchEngineTheoremProducer::conflictClause: "
281 "literal or gamma set contains extra element : "
282 + t->first.toString());
289 literals.push_back(thm.
getExpr());
300 for(
size_t i=0, iend=lits.size(); i<iend; ++i) {
301 const Expr& e(lits[i].getExpr());
312 body =
Proof(body.getExpr().substExpr(subst));
313 pf =
newPf(
"conflict_clause",
newPf(u, assump, body));
379 "cutRule called without assumptions activated");
387 exprs.reserve(thmsA.size() + 1);
388 const vector<Theorem>::const_iterator iend = thmsA.end();
389 for(vector<Theorem>::const_iterator i=thmsA.begin(); i!=iend; ++i) {
390 exprs.push_back(i->getExpr());
398 pfs.reserve(thmsA.size() + 1);
399 for(vector<Theorem>::const_iterator i = thmsA.begin(); i != iend; ++i) {
400 pfs.push_back(i->getProof());
402 exprs.push_back(as_prove_b.
getExpr());
403 pfs.push_back(as_prove_b.
getProof());
404 pf =
newPf(
"cut_rule",exprs,pfs);
415 if(visited.
count(e)>0)
420 "skolem constant found in axioms of false theorem: "
455 const std::vector<Theorem>& delta)
457 TRACE(
"skolem",
"=>eliminateSkolemAxioms ", delta.size(),
"{");
460 TRACE(
"skolem",
"eliminateSkolemAxioms",
"" ,
"}");
466 "eliminateSkolemAxiom called on non-false theorem");
469 vector<Theorem>::const_iterator it = delta.begin(), end = delta.end();
470 for(; it!=end; ++it) {
472 "eliminateSkolemAxioms(): Skolem axiom is not "
473 "an IFF: "+it->toString());
474 const Expr& ex = it->getLHS();
476 "Did not receive skolem axioms in Delta"
477 " of eliminateSkolemAxioms" + it->toString());
479 for(
unsigned int j=0; j<ex.getVars().size(); j++) {
480 Expr sk_var(ex.skolemExpr(j));
481 if(sk_var.getType().isBool()) {
484 skolems[sk_var] =
true;
485 TRACE(
"skolem",
">> Eliminating variable: ", sk_var,
"<<");
496 std::vector<Proof>skolemizeLabels;
497 std::vector<Expr> exprs;
498 for(
unsigned int i=0; i<delta.size(); i++)
500 exprs.push_back(delta[i].getExpr());
501 skolemizeLabels.push_back(delta[i].getProof());
503 pf =
newPf(skolemizeLabels, exprs, origFalse);
505 TRACE(
"skolem",
"eliminateSkolemAxioms",
"" ,
"}");
518 "SearchEngineTheoremProducer::unitProp: bad theorem or i="
520 +
" in clause = " + clause.
toString());
523 "SearchEngineTheoremProducer::unitProp: "
524 "wrong number of theorems"
526 +
"\n clause.arity = " +
int2string(e.arity()));
528 for(
unsigned j=0,k=0; j<thms.size(); j++) {
530 Expr ej(e[j]), ek(thms[k].getExpr());
532 "SearchEngineTheoremProducer::unitProp: "
534 "\n thm = " + thms[k].toString() +
535 "\n literal = " + e[j].toString() +
536 "\n clause = " + clause.
toString());
549 exprs.reserve(thms.size() + 1);
550 pfs.reserve(thms.size()+1);
551 const vector<Theorem>::const_iterator iend = thms.end();
552 for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
553 exprs.push_back(i->getExpr());
554 pfs.push_back(i->getProof());
556 exprs.push_back(clause.
getExpr());
558 pf =
newPf(
"unit_prop", exprs, pfs);
570 ((left && b_th.
refutes(andr_e[1])) ||
571 (!left && b_th.
refutes(andr_e[2]))),
572 "SearchEngineTheoremProducer::propAndrAF");
581 exprs.push_back(andr_th.
getExpr());
582 exprs.push_back(b_th.
getExpr());
586 pf =
newPf(
"prop_andr_af", exprs, pfs);
600 "SearchEngineTheoremProducer::propAndrAT");
610 exprs.push_back(andr_th.
getExpr());
611 exprs.push_back(l_th.
getExpr());
612 exprs.push_back(r_th.
getExpr());
616 pf =
newPf(
"prop_andr_at", exprs, pfs);
630 "SearchEngineTheoremProducer::propAndrLRT");
639 exprs.push_back(andr_th.
getExpr());
640 exprs.push_back(a_th.
getExpr());
643 pf =
newPf(
"prop_andr_lrt", exprs, pfs);
646 if (l_th) *l_th =
newTheorem(andr_e[1], a, pf);
647 if (r_th) *r_th =
newTheorem(andr_e[2], a, pf);
658 "SearchEngineTheoremProducer::propAndrLF");
668 exprs.push_back(andr_th.
getExpr());
669 exprs.push_back(a_th.
getExpr());
670 exprs.push_back(r_th.
getExpr());
674 pf =
newPf(
"prop_andr_lf", exprs, pfs);
688 "SearchEngineTheoremProducer::propAndrRF");
698 exprs.push_back(andr_th.
getExpr());
699 exprs.push_back(a_th.
getExpr());
700 exprs.push_back(l_th.
getExpr());
704 pf =
newPf(
"prop_andr_rf", exprs, pfs);
718 ((left && b_th.
refutes(andr_e[1])) ||
719 (!left && b_th.
refutes(andr_e[2]))),
720 "SearchEngineTheoremProducer::confAndrAT");
730 exprs.push_back(andr_th.
getExpr());
731 exprs.push_back(a_th.
getExpr());
732 exprs.push_back(b_th.
getExpr());
737 pf =
newPf(
"conf_andr_at", exprs, pfs);
752 "SearchEngineTheoremProducer::confAndrAF");
767 exprs.push_back(andr_th.
getExpr());
768 exprs.push_back(a_th.
getExpr());
769 exprs.push_back(l_th.
getExpr());
770 exprs.push_back(r_th.
getExpr());
775 pf =
newPf(
"conf_andr_af", exprs, pfs);
790 "SearchEngineTheoremProducer::propIffr: p="
793 case 0: a = 1; b = 2;
break;
794 case 1: a = 0; b = 2;
break;
795 case 2: a = 0; b = 1;
break;
800 bool v0 = a_th.
proves(iffr_e[a]);
801 bool v1 = b_th.
proves(iffr_e[b]);
805 (v0 || a_th.
refutes(iffr_e[a])) &&
806 (v1 || b_th.
refutes(iffr_e[b])),
807 "SearchEngineTheoremProducer::propIffr");
821 exprs.push_back(iffr_th.
getExpr());
822 exprs.push_back(a_th.
getExpr());
823 exprs.push_back(b_th.
getExpr());
827 pf =
newPf(
"prop_iffr", exprs, pfs);
830 return newTheorem(v0 == v1 ? iffr_e[p] : iffr_e[p].negate(), aa, pf);
841 bool v0 = i_th.
proves(iffr_e[0]);
842 bool v1 = l_th.
proves(iffr_e[1]);
843 bool v2 = r_th.
proves(iffr_e[2]);
847 (v0 || i_th.
refutes(iffr_e[0])) &&
848 (v1 || l_th.
refutes(iffr_e[1])) &&
849 (v2 || r_th.
refutes(iffr_e[2])) &&
850 ((v0 && v1 != v2) || (!v0 && v1 == v2)),
851 "SearchEngineTheoremProducer::confIffr");
866 exprs.push_back(iffr_th.
getExpr());
867 exprs.push_back(i_th.
getExpr());
868 exprs.push_back(l_th.
getExpr());
869 exprs.push_back(r_th.
getExpr());
874 pf =
newPf(
"conf_iffr", exprs, pfs);
888 bool v0 = if_th.
proves(iter_e[1]);
889 bool v1 = then_th.
proves(iter_e[left ? 2 : 3]);
893 (v0 || if_th.
refutes(iter_e[1])) &&
894 (v1 || then_th.
refutes(iter_e[left ? 2 : 3])) &&
896 "SearchEngineTheoremProducer::propIterIte");
910 exprs.push_back(iter_th.
getExpr());
911 exprs.push_back(if_th.
getExpr());
912 exprs.push_back(then_th.
getExpr());
916 pf =
newPf(
"prop_iter_ite", exprs, pfs);
919 return newTheorem(v1 ? iter_e[0] : iter_e[0].negate(), a, pf);
932 bool v0 = ite_th.
proves(iter_e[0]);
933 bool v1 = then_th.
proves(iter_e[left ? 2 : 3]);
937 (v0 || ite_th.
refutes(iter_e[0])) &&
938 (v1 || then_th.
refutes(iter_e[left ? 2 : 3])) &&
940 "SearchEngineTheoremProducer::propIterIfThen");
954 exprs.push_back(iter_th.
getExpr());
955 exprs.push_back(ite_th.
getExpr());
956 exprs.push_back(then_th.
getExpr());
959 pfs.push_back(then_th.
getExpr());
960 pf =
newPf(
"prop_iter_if_then", exprs, pfs);
964 *if_th =
newTheorem(left ? iter_e[1].negate() : iter_e[1], a, pf);
966 *else_th =
newTheorem(v0 ? iter_e[left ? 3 : 2] : iter_e[left ? 3 : 2].negate(), a, pf);
976 bool v0 = ite_th.
proves(iter_e[0]);
977 bool v1 = if_th.
proves(iter_e[1]);
981 (v0 || ite_th.
refutes(iter_e[0])) &&
982 (v1 || if_th.
refutes(iter_e[1])),
983 "SearchEngineTheoremProducer::propIterThen");
997 exprs.push_back(iter_th.
getExpr());
998 exprs.push_back(ite_th.
getExpr());
999 exprs.push_back(if_th.
getExpr());
1002 pfs.push_back(if_th.
getExpr());
1003 pf =
newPf(
"prop_iter_then", exprs, pfs);
1007 (v0 ? iter_e[2] : iter_e[2].negate()) :
1008 (v0 ? iter_e[3] : iter_e[3].negate()), a, pf);
1019 bool v0 = ite_th.
proves(iter_e[0]);
1020 bool v1 = then_th.
proves(iter_e[2]);
1021 bool v2 = else_th.
proves(iter_e[3]);
1025 (v0 || ite_th.
refutes(iter_e[0])) &&
1026 (v1 || then_th.
refutes(iter_e[2])) &&
1027 (v2 || else_th.
refutes(iter_e[3])) &&
1028 ((v0 && !v1 && !v2) || (!v0 && v1 && v2)),
1029 "SearchEngineTheoremProducer::confIterThenElse");
1044 exprs.push_back(iter_th.
getExpr());
1045 exprs.push_back(ite_th.
getExpr());
1046 exprs.push_back(then_th.
getExpr());
1047 exprs.push_back(else_th.
getExpr());
1050 pfs.push_back(then_th.
getExpr());
1051 pfs.push_back(else_th.
getExpr());
1052 pf =
newPf(
"conf_iter_then_else", exprs, pfs);
1067 bool v0 = ite_th.
proves(iter_e[0]);
1068 bool v1 = if_th.
proves(iter_e[1]);
1069 bool v2 = then_th.
proves(iter_e[left ? 2 : 3]);
1073 (v0 || ite_th.
refutes(iter_e[0])) &&
1074 (v1 || if_th.
refutes(iter_e[1])) &&
1075 (v2 || then_th.
refutes(iter_e[left ? 2 : 3])) &&
1076 v1 == left && v0 != v2,
1077 "SearchEngineTheoremProducer::confIterThenElse");
1092 exprs.push_back(iter_th.
getExpr());
1093 exprs.push_back(ite_th.
getExpr());
1094 exprs.push_back(if_th.
getExpr());
1095 exprs.push_back(then_th.
getExpr());
1098 pfs.push_back(if_th.
getExpr());
1099 pfs.push_back(then_th.
getExpr());
1100 pf =
newPf(
"conf_iter_then_else", exprs, pfs);
1115 "SearchEngineTheoremProducer::unitProp: "
1116 "bad theorem in clause = "+clause.
toString());
1119 "SearchEngineTheoremProducer::conflictRule: "
1120 "wrong number of theorems"
1122 +
"\n clause.arity = " +
int2string(e.arity()));
1124 for(
unsigned j=0; j<thms.size(); j++) {
1125 Expr ej(e[j]), ek(thms[j].getExpr());
1127 "SearchEngineTheoremProducer::conflictRule: "
1129 "\n thm = " + thms[j].toString() +
1130 "\n literal = " + e[j].toString() +
1131 "\n clause = " + clause.
toString());
1141 exprs.reserve(thms.size() + 1);
1142 pfs.reserve(thms.size()+1);
1143 const vector<Theorem>::const_iterator iend = thms.end();
1144 for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
1145 exprs.push_back(i->getExpr());
1146 pfs.push_back(i->getProof());
1148 exprs.push_back(clause.
getExpr());
1150 pf =
newPf(
"conflict", exprs, pfs);
1191 "SearchEngineTheoremProducer::iteToClauses("+iteExpr.
toString()
1192 +
")\n Argument must be a Boolean ITE");
1194 const Expr& cond = iteExpr[0];
1195 const Expr& t1 = iteExpr[1];
1196 const Expr& t2 = iteExpr[2];
1210 +
")\n Argument must be a Boolean IFF");
1228 const string& ruleName) {
1235 "SearchEngineTheoremProducer::opCNFRule("
1237 "input must be an IFF: thm = " + phiIffVar.
toString());
1239 "SearchEngineTheoremProducer::opCNFRule("
1241 "input phi has wrong kind: thm = " + phiIffVar.
toString());
1243 "SearchEngineTheoremProducer::opCNFRule("
1245 "wrong input thm = " + phiIffVar.
toString());
1249 "SearchEngineTheoremProducer::opCNFRule("
1251 "wrong input thm = " + phiIffVar.
toString());
1257 std::vector<Expr> boundVars;
1258 std::vector<Expr> boundVarsAndLiterals;
1259 std::vector<Expr> equivs;
1267 boundVarsAndLiterals.push_back(*i);
1274 it != itend; it++) {
1276 "SearchEngineTheoremProducer::opCNFRule: " +
1277 (*it).second.toString());
1279 (*it).second[1].isAbsLiteral(),
1280 "SearchEngineTheoremProducer::opCNFRule: " +
1281 (*it).second.toString());
1282 equivs.push_back((*it).second);
1286 "SearchEngineTheoremProducer::opCNFRule: "
1287 "wrong size of boundvars: phi = " + phi.
toString());
1290 "SearchEngineTheoremProducer::opCNFRule: "
1291 "wrong size of boundvars: phi = " + phi.
toString());
1295 if(boundVars.size() > 0)
1313 std::vector<Expr> clauses;
1314 std::vector<Expr> lastClause;
1318 lastClause.push_back(v);
1319 for(;i!=iend; ++i) {
1320 lastClause.push_back(i->
negate());
1322 clauses.push_back(
orExpr(lastClause));
1326 lastClause.push_back(v.
negate());
1327 for(;i!=iend; ++i) {
1329 lastClause.push_back(*i);
1331 clauses.push_back(
orExpr(lastClause));
1335 const Expr& v1 = phi[0];
1336 const Expr& v2 = phi[1];
1340 clauses.push_back(
Expr(
OR, negV, negv1, v2));
1341 clauses.push_back(
Expr(
OR, negV, v1, negv2));
1342 clauses.push_back(
Expr(
OR, v, v1, v2));
1343 clauses.push_back(
Expr(
OR, v, negv1, negv2));
1346 const Expr& v1 = phi[0];
1347 const Expr& v2 = phi[1];
1351 clauses.push_back(
Expr(
OR, negV, negv1, v2));
1352 clauses.push_back(v.
orExpr(v1));
1353 clauses.push_back(v.
orExpr(negv2));
1357 const Expr& v1 = phi[0];
1358 const Expr& v2 = phi[1];
1359 const Expr& v3 = phi[2];
1364 clauses.push_back(
Expr(
OR, negV, negv1, v2));
1365 clauses.push_back(
Expr(
OR, negV, v1, v3));
1366 clauses.push_back(
Expr(
OR, v, negv1, negv2));
1367 clauses.push_back(
Expr(
OR, v, v1, negv3));
1371 DebugAssert(
false,
"SearchEngineTheoremProducer::convertToCNF: "
1372 "bad operator in phi = "+phi.
toString());
1384 vector<Expr>& boundVars) {
1387 unsigned int negationDepth = 0;
1391 while(phi.
isNot()) {
1396 it = localCache.
find(phi);
1398 if(it != localCache.
end()) {
1399 v = ((*it).second)[1];
1400 IF_DEBUG(debugger.counter(
"CNF Local Cache Hits")++;)
1404 boundVars.push_back(v);
1405 localCache[phi] = phi.
iffExpr(v);
1407 if(negationDepth % 2 != 0)
1409 TRACE(
"mycnf",
"findInLocalCache => ", v,
" }");
1422 pf =
newPf(
"minisat_proof", queryExpr, satProof);
1430 std::vector<Expr> assumps;
1435 cout <<
"CVC3 Proof: ";