31 #define _CVC3_TRUSTED_
46 SearchEngine::createRules() {
57 search_engine = s_eng;
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: ";
virtual void propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)
iterator begin() const
Begin iterator.
void verifyConflict(const Theorem &thm, TheoremMap &m)
API to to a generic proof search engine.
virtual Theorem proofByContradiction(const Expr &a, const Theorem &pfFalse)
Proof by contradiction: .
Data structure of expressions in CVC3.
Theorem newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)
Create a new theorem. See also newRWTheorem() and newReflTheorem()
virtual Theorem confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)
std::map< Theorem, bool, TheoremLess > TheoremMap
Abstract API to the proof search engine.
virtual Theorem eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)
void clearAllFlags() const
Clear the flag attribute in all the theorems.
Expr findInLocalCache(const Expr &i, ExprMap< Expr > &localCache, std::vector< Expr > &boundVars)
checks if phi has v in local cache of opCNFRule, if so reuse v.
Theorem iffToClauses(const Theorem &iff)
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
iterator find(const Expr &e)
void add(const std::vector< Theorem > &thms)
virtual Theorem propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)
virtual Theorem cutRule(const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)
Cut rule: .
virtual Theorem propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)
virtual Theorem propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)
bool isPropAtom() const
True iff expr is not a Bool connective.
bool proves(const Expr &e) const
Check if the flag attribute is set.
bool withProof()
Testing whether to generate proofs.
void print_LFSC(const Expr &pf_expr)
#define DebugAssert(cond, str)
#define CHECK_SOUND(cond, msg)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
virtual Theorem caseSplit(const Expr &a, const Theorem &a_proves_c, const Theorem ¬_a_proves_c)
Case split: .
Theorem impCNFRule(const Theorem &thm)
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
bool withAssumptions()
Testing whether to generate assumptions.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool refutes(const Expr &e) const
Check if the flag attribute is set.
Expr orExpr(const std::vector< Expr > &children)
virtual void propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Op getOp() const
Get operator from expression.
size_t count(const Expr &e) const
const std::string & getKindName(int kind)
Return the name associated with a kind. The kind must already be registered.
std::string toString() const
virtual Theorem unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)
Unit propagation rule: .
std::string toString() const
Print the expression to a string.
bool isFlagged() const
Check if the flag attribute is set.
Expr iffExpr(const Expr &right) const
const Expr & falseExpr()
FALSE Expr.
Expr newLeafExpr(const Op &op)
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
Proof newLabel(const Expr &e)
Create a new proof label (bound variable) for an assumption (formula)
const Expr & getRHS() const
Theorem orCNFRule(const Theorem &thm)
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
virtual Theorem conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)
"Conflict" rule (all literals in a clause become FALSE)
virtual void getUserAssumptions(std::vector< Expr > &assumptions)=0
Get all user assumptions made in this and all previous contexts.
virtual Theorem confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)
const Assumptions & getAssumptionsRef() const
Implementation API to proof rules for the simple search engine.
Theorem opCNFRule(const Theorem &thm, int kind, const std::string &ruleName)
Expr orExpr(const Expr &right) const
Theorem iteToClauses(const Theorem &ite)
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual Theorem confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)
virtual Theorem conflictClause(const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)
Conflict clause rule: .
virtual Theorem propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)
Theorem iteCNFRule(const Theorem &thm)
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
CommonProofRules * d_commonRules
virtual Theorem confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)
const Expr & getLHS() const
Iterator for the Assumptions: points to class Theorem.
API to the proof rules for the Search Engines.
Proof newPf(const std::string &name)
const CLFlags & getFlags() const
virtual Theorem propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)
Type getType() const
Get the type. Recursively compute if necessary.
Theorem iffCNFRule(const Theorem &thm)
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Theorem satProof(const Expr &queryExpr, const Proof &satProof)
static const Assumptions & emptyAssump()
Expr andExpr(const std::vector< Expr > &children)
virtual Theorem propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)
SearchEngine * search_engine
virtual Theorem negIntro(const Expr ¬_a, const Theorem &pfFalse)
Negation introduction: .
virtual Theorem propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)
Expr convertToCNF(const Expr &v, const Expr &phi)
produces the CNF for the formula v <==> phi
void setFlag() const
Set the flag attribute.
void checkSoundNoSkolems(const Expr &e, ExprMap< bool > &visited, const ExprMap< bool > &skolems)
Theorem andCNFRule(const Theorem &thm)
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
virtual Theorem confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)
iterator end() const
End iterator.