/*****************************************************************************/
/*!
* \file search_theorem_producer.cpp
* \brief Implementation of the proof rules for the simple search engine
*
* Author: Sergey Berezin
*
* Created: Mon Feb 24 14:51:51 2003
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#include "search.h"
#include "theory_core.h"
#include "theorem_manager.h"
#include "common_proof_rules.h"
#define _CVC3_TRUSTED_
#include "search_theorem_producer.h"
using namespace std;
using namespace CVC3;
/////////////////////////////////////////////////////////////////////////////
// class SearchEngine trusted methods
/////////////////////////////////////////////////////////////////////////////
SearchEngineRules*
SearchEngine::createRules() {
return new SearchEngineTheoremProducer(d_core->getTM());
}
SearchEngineTheoremProducer::SearchEngineTheoremProducer(TheoremManager* tm)
: TheoremProducer(tm), d_commonRules(tm->getRules())
{ }
/////////////////////////////////////////////////////////////////////////////
// Proof rules
/////////////////////////////////////////////////////////////////////////////
// Proof by contradiction: !A |- FALSE ==> |- A. "!A" doesn't
// have to be present in the assumptions.
Theorem
SearchEngineTheoremProducer::proofByContradiction(const Expr& a,
const Theorem& pfFalse) {
if(CHECK_PROOFS)
CHECK_SOUND(pfFalse.getExpr().isFalse(),
"proofByContradiction: pfFalse = : " + pfFalse.toString());
Expr not_a(!a);
Assumptions assump(pfFalse.getAssumptionsRef() - not_a);
Proof pf;
if(withProof()) {
// TODO: optimize with 1 traversal?
Theorem thm(pfFalse.getAssumptionsRef()[not_a]);
Proof u; // proof label for !a
if(!thm.isNull()) u = thm.getProof();
// Proof compaction: if u is Null, use "FALSE => A" rule
if(u.isNull())
pf = newPf("false_implies_anything", a, pfFalse.getProof());
else
pf = newPf("pf_by_contradiction", a,
// LAMBDA-abstraction (LAMBDA (u: !a): pfFalse)
newPf(u, not_a, pfFalse.getProof()));
}
return newTheorem(a, assump, pf);
}
// Similar rule, only negation introduction:
// A |- FALSE ==> !A
Theorem
SearchEngineTheoremProducer::negIntro(const Expr& not_a,
const Theorem& pfFalse) {
if(CHECK_PROOFS) {
CHECK_SOUND(pfFalse.getExpr().isFalse(),
"negIntro: pfFalse = : " + pfFalse.toString());
CHECK_SOUND(not_a.isNot(), "negIntro: not_a = "+not_a.toString());
}
Expr a(not_a[0]);
Assumptions assump(pfFalse.getAssumptionsRef() - a);
Proof pf;
if(withProof()) {
Theorem thm(pfFalse.getAssumptionsRef()[a]);
Proof u; // proof label for 'a'
if(!thm.isNull()) u = thm.getProof();
// Proof compaction: if u is Null, use "FALSE => !A" rule
if(u.isNull())
pf = newPf("false_implies_anything", not_a, pfFalse.getProof());
else
pf = newPf("neg_intro", not_a,
// LAMBDA-abstraction (LAMBDA (u: a): pfFalse)
newPf(u, a, pfFalse.getProof()));
}
return newTheorem(not_a, assump, pf);
}
// Case split: u1:A |- C, u2:!A |- C ==> |- C
Theorem
SearchEngineTheoremProducer::caseSplit(const Expr& a,
const Theorem& a_proves_c,
const Theorem& not_a_proves_c) {
Expr c(a_proves_c.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(c == not_a_proves_c.getExpr(),
"caseSplit: conclusions differ:\n positive case C = "
+ c.toString() + "\n negative case C = "
+ not_a_proves_c.getExpr().toString());
// The opposite assumption should not appear in the theorems
// Actually, this doesn't violate soundness, no reason to check
// CHECK_SOUND(a_proves_c.getAssumptions()[!a].isNull(),
// "caseSplit: wrong assumption: " + (!a).toString()
// +"\n in "+a_proves_c.toString());
// CHECK_SOUND(not_a_proves_c.getAssumptions()[a].isNull(),
// "caseSplit: wrong assumption: " + a.toString()
// +"\n in "+not_a_proves_c.toString());
}
const Assumptions& a1(a_proves_c.getAssumptionsRef());
const Assumptions& a2(not_a_proves_c.getAssumptionsRef());
Assumptions a3 = a1 - a;
Assumptions a4 = a2 - !a;
// Proof compaction: if either theorem proves C without a or !a,
// then just use that theorem. This only works if assumptions are
// active.
if (a1 == a3) return a_proves_c;
if (a2 == a4) return not_a_proves_c;
// No easy way out. Do the work.
Proof pf;
a3.add(a4);
if(withProof()) {
// Create lambda-abstractions
vector<Proof> pfs;
pfs.push_back(newPf(a1[a].getProof(),
a, a_proves_c.getProof()));
pfs.push_back(newPf(a2[!a].getProof(),
!a, not_a_proves_c.getProof()));
pf = newPf("case_split", a, c, pfs);
}
return newTheorem(c, a3, pf);
}
// Conflict clause rule:
// Gamma, A_1,...,A_n |- B ==> Gamma |- (OR B A_1 ... A_n)
// The assumptions A_i are given by the vector 'lits'.
// If B==FALSE, it is omitted from the result.
// NOTE: here "!A_i" means an inverse of A_i, not just a negation.
// That is, if A_i is NOT C, then !A_i is C.
// verification function used by conflictClause
void SearchEngineTheoremProducer::verifyConflict(const Theorem& thm,
TheoremMap& m) {
const Assumptions& a(thm.getAssumptionsRef());
const Assumptions::iterator iend = a.end();
for (Assumptions::iterator i = a.begin();
i != iend; ++i) {
CHECK_SOUND(!i->isNull(),
"SearchEngineTheoremProducer::conflictClause: "
"Found null theorem");
if (!i->isRefl() && !i->isFlagged()) {
i->setFlag();
if (m.count(*i) == 0) {
CHECK_SOUND(!i->isAssump(),
"SearchEngineTheoremProducer::conflictClause: "
"literal and gamma sets do not form a complete "
"cut of Theorem assumptions. Stray theorem: \n"
+i->toString());
verifyConflict(*i, m);
}
else {
m[*i] = true;
}
}
}
}
Theorem
SearchEngineTheoremProducer::
conflictClause(const Theorem& thm, const vector<Theorem>& lits,
const vector<Theorem>& gamma) {
// TRACE("search proofs", "conflictClause(", thm.getExpr(), ") {");
IF_DEBUG(if(debugger.trace("search proofs")) {
ostream& os = debugger.getOS();
os << "lits = [";
for(vector<Theorem>::const_iterator i=lits.begin(), iend=lits.end();
i!=iend; ++i)
os << i->getExpr() << ",\n";
os << "]\n\ngamma = [";
for(vector<Theorem>::const_iterator i=gamma.begin(), iend=gamma.end();
i!=iend; ++i)
os << i->getExpr() << ",\n";
os << "]" << endl;
});
bool checkProofs(CHECK_PROOFS);
// This rule only makes sense when runnnig with assumptions
if(checkProofs) {
CHECK_SOUND(withAssumptions(),
"conflictClause: called while running without assumptions");
}
// Assumptions aOrig(thm.getAssumptions());
vector<Expr> literals;
vector<Proof> u; // Vector of proof labels
literals.reserve(lits.size() + 1);
u.reserve(lits.size());
const vector<Theorem>::const_iterator iend = lits.end();
for(vector<Theorem>::const_iterator i=lits.begin(); i!=iend; ++i) {
Expr neg(i->getExpr().negate());
literals.push_back(neg);
if(withProof()) u.push_back(i->getProof());
}
if(checkProofs) {
TheoremMap m;
// TRACE_MSG("search proofs", "adding gamma to m: {");
for(vector<Theorem>::const_iterator i = gamma.begin();
i != gamma.end(); ++i) {
// TRACE("search proofs", "m[", *i, "]");
m[*i] = false;
}
// TRACE_MSG("search proofs", "}");
for(vector<Theorem>::const_iterator i = lits.begin(); i!=iend; ++i) {
// TRACE("search proofs", "check lit: ", *i, "");
CHECK_SOUND(m.count(*i) == 0,
"SearchEngineTheoremProducer::conflictClause: "
"literal and gamma sets are not disjoint: lit = "
+i->toString());
m[*i] = false;
}
thm.clearAllFlags();
verifyConflict(thm, m);
TheoremMap::iterator t = m.begin(), tend = m.end();
for (; t != tend; ++t) {
CHECK_SOUND(t->second == true,
"SearchEngineTheoremProducer::conflictClause: "
"literal or gamma set contains extra element : "
+ t->first.toString());
}
}
Assumptions a(gamma);
if(!thm.getExpr().isFalse())
literals.push_back(thm.getExpr());
Proof pf;
if(withProof()) {
if(lits.size()>0) {
vector<Expr> assump;
// If assumptions are not leaves, we need to create new
// variables for them and substitute them for their proofs in
// the proof term
ExprHashMap<Expr> subst;
DebugAssert(u.size() == lits.size(), "");
for(size_t i=0, iend=lits.size(); i<iend; ++i) {
const Expr& e(lits[i].getExpr());
assump.push_back(e);
Proof& v = u[i];
if(!v.getExpr().isVar()) {
Proof label = newLabel(e);
subst[v.getExpr()] = label.getExpr();
v = label;
}
}
Proof body(thm.getProof());
if(!subst.empty())
body = Proof(body.getExpr().substExpr(subst));
pf = newPf("conflict_clause", newPf(u, assump, body));
}
else
pf = newPf("false_to_empty_or", thm.getProof());
}
Theorem res(newTheorem(Expr(OR, literals, d_em), a, pf));
// TRACE("search proofs", "conflictClause => ", res.getExpr(), " }");
return res;
}
// Theorem
// SearchEngineTheoremProducer::
// conflictClause(const Theorem& thm, const vector<Expr>& lits) {
// bool checkProofs(CHECK_PROOFS);
// // This rule only makes sense when runnnig with assumptions
// if(checkProofs) {
// CHECK_SOUND(withAssumptions(),
// "conflictClause: called while running without assumptions");
// }
// Assumptions aOrig(thm.getAssumptions());
// vector<Expr> literals;
// vector<Expr> negations;
// vector<Proof> u; // Vector of proof labels
// literals.reserve(lits.size() + 1);
// negations.reserve(lits.size());
// u.reserve(lits.size());
// for(vector<Expr>::const_iterator i=lits.begin(), iend=lits.end();
// i!=iend; ++i) {
// Expr neg(i->isNot()? (*i)[0] : !(*i));
// if(checkProofs)
// CHECK_SOUND(!aOrig[neg].isNull(),
// "SearchEngineTheoremProducer::conflictClause: "
// "literal is not in the set of assumptions: neg = "
// +neg.toString() + "\n Theorem = " + thm.toString());
// literals.push_back(*i);
// negations.push_back(neg);
// if(withProof()) u.push_back(aOrig[neg].getProof());
// }
// Assumptions a = aOrig - negations;
// if(!thm.getExpr().isFalse())
// literals.push_back(thm.getExpr());
// Proof pf;
// if(withProof()) {
// if(lits.size()>0)
// pf = newPf("conflict_clause", newPf(u, literals, thm.getProof()));
// else
// pf = newPf("false_to_empty_or", thm.getProof());
// }
// // Use ExprManager in newExpr, since literals may be empty
// return newTheorem(Expr(d_em, OR, literals), a, pf);
// }
// "Cut" rule: { G_i |- A_i }; G', { A_i } |- B ==> union(G_i)+G' |- B.
Theorem
SearchEngineTheoremProducer::
cutRule(const vector<Theorem>& thmsA,
const Theorem& as_prove_b) {
if(CHECK_PROOFS)
CHECK_SOUND(withAssumptions(),
"cutRule called without assumptions activated");
// Optimization: use only those theorems that occur in B's assumptions.
// *** No, take it back, it's a mis-optimization. Most of the time,
// cutRule is applied when we *know* thmsA are present in the
// assumptions of 'as_proof_b'.
Proof pf;
vector<Expr> exprs;
exprs.reserve(thmsA.size() + 1);
const vector<Theorem>::const_iterator iend = thmsA.end();
for(vector<Theorem>::const_iterator i=thmsA.begin(); i!=iend; ++i) {
exprs.push_back(i->getExpr());
}
Assumptions a(thmsA); // add the As
a.add(as_prove_b.getAssumptionsRef() - exprs); // Add G'
if(withProof()) {
vector<Proof> pfs;
pfs.reserve(thmsA.size() + 1);
for(vector<Theorem>::const_iterator i = thmsA.begin(); i != iend; ++i) {
pfs.push_back(i->getProof());
}
exprs.push_back(as_prove_b.getExpr());
pfs.push_back(as_prove_b.getProof());
pf = newPf("cut_rule",exprs,pfs);
}
return newTheorem(as_prove_b.getExpr(), a, pf);
}
void
SearchEngineTheoremProducer::checkSoundNoSkolems(const Expr& e,
ExprMap<bool>& visited,
const ExprMap<bool>& skolems)
{
if(visited.count(e)>0)
return;
else
visited[e] = true;
CHECK_SOUND(skolems.count(e) == 0,
"skolem constant found in axioms of false theorem: "
+ e.toString());
for(Expr::iterator it = e.begin(), end = e.end(); it!= end; ++it)
checkSoundNoSkolems(*it, visited, skolems);
if(e.getKind() == FORALL || e.getKind() == EXISTS)
checkSoundNoSkolems(e.getBody(), visited, skolems);
}
void
SearchEngineTheoremProducer::checkSoundNoSkolems(const Theorem& t,
ExprMap<bool>& visited,
const ExprMap<bool>& skolems)
{
if(t.isRefl() || t.isFlagged())
return;
t.setFlag();
if(t.isAssump())
checkSoundNoSkolems(t.getExpr(), visited, skolems);
else
{
const Assumptions& a(t.getAssumptionsRef());
Assumptions::iterator it = a.begin(), end = a.end();
for(; it!=end; ++it)
checkSoundNoSkolems(*it, visited, skolems);
}
}
/*! Eliminate skolem axioms:
* Gamma, Delta |- false => Gamma|- false
* where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
* and gamma does not contain any of the skolem constants c.
*/
Theorem
SearchEngineTheoremProducer::eliminateSkolemAxioms(const Theorem& tFalse,
const std::vector<Theorem>& delta)
{
TRACE("skolem", "=>eliminateSkolemAxioms ", delta.size(), "{");
if(delta.empty())
{
TRACE("skolem", "eliminateSkolemAxioms","" , "}");
return tFalse;
}
const Expr& falseExpr = tFalse.getExpr();
if(CHECK_PROOFS) {
CHECK_SOUND(falseExpr.isFalse(),
"eliminateSkolemAxiom called on non-false theorem");
ExprMap<bool> visited;
ExprMap<bool> skolems;
vector<Theorem>::const_iterator it = delta.begin(), end = delta.end();
for(; it!=end; ++it) {
CHECK_SOUND(it->isRewrite(),
"eliminateSkolemAxioms(): Skolem axiom is not "
"an IFF: "+it->toString());
const Expr& ex = it->getLHS();
CHECK_SOUND(ex.isExists(),
"Did not receive skolem axioms in Delta"
" of eliminateSkolemAxioms" + it->toString());
// Collect the Skolem constants for further soundness checks
for(unsigned int j=0; j<ex.getVars().size(); j++) {
Expr sk_var(ex.skolemExpr(j));
if(sk_var.getType().isBool()) {
sk_var = d_em->newLeafExpr(sk_var.mkOp());
}
skolems[sk_var] = true;
TRACE("skolem", ">> Eliminating variable: ", sk_var, "<<");
}
}
tFalse.clearAllFlags();
checkSoundNoSkolems(tFalse, visited, skolems);
}
Proof pf;
if(!withProof()) return tFalse;
else
{
Proof origFalse = tFalse.getProof();
std::vector<Proof>skolemizeLabels;
std::vector<Expr> exprs;
for(unsigned int i=0; i<delta.size(); i++)
{
exprs.push_back(delta[i].getExpr());
skolemizeLabels.push_back(delta[i].getProof());
}
pf = newPf(skolemizeLabels, exprs, origFalse);
}
TRACE("skolem", "eliminateSkolemAxioms","" , "}");
return newTheorem(tFalse.getExpr(), tFalse.getAssumptionsRef(), pf);
}
Theorem
SearchEngineTheoremProducer::unitProp(const std::vector<Theorem>& thms,
const Theorem& clause,
unsigned i) {
Expr e(clause.getExpr());
if(CHECK_PROOFS) {
// Soundness check: first, check the form of the 'clause' theorem
CHECK_SOUND(e.isOr() && e.arity() > (int)i,
"SearchEngineTheoremProducer::unitProp: bad theorem or i="
+int2string(i)+" > arity="+int2string(e.arity())
+" in clause = " + clause.toString());
// Now, check correspondence of thms to the disjunction
CHECK_SOUND(((int)thms.size()) == e.arity() - 1,
"SearchEngineTheoremProducer::unitProp: "
"wrong number of theorems"
"\n thms.size = " + int2string(thms.size())
+"\n clause.arity = " + int2string(e.arity()));
for(unsigned j=0,k=0; j<thms.size(); j++) {
if(j!=i) {
Expr ej(e[j]), ek(thms[k].getExpr());
CHECK_SOUND((ej.isNot() && ej[0] == ek) || (ek.isNot() && ej == ek[0]),
"SearchEngineTheoremProducer::unitProp: "
"wrong theorem["+int2string(k)+"]"
"\n thm = " + thms[k].toString() +
"\n literal = " + e[j].toString() +
"\n clause = " + clause.toString());
k++;
}
}
}
Assumptions a(thms);
a.add(clause);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.reserve(thms.size() + 1);
pfs.reserve(thms.size()+1);
const vector<Theorem>::const_iterator iend = thms.end();
for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
exprs.push_back(i->getExpr());
pfs.push_back(i->getProof());
}
exprs.push_back(clause.getExpr());
pfs.push_back(clause.getProof());
pf = newPf("unit_prop", exprs, pfs);
}
return newTheorem(e[i], a, pf);
}
Theorem
SearchEngineTheoremProducer::propAndrAF(const Theorem& andr_th,
bool left,
const Theorem& b_th) {
const Expr& andr_e(andr_th.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(andr_e.getKind() == AND_R &&
((left && b_th.refutes(andr_e[1])) ||
(!left && b_th.refutes(andr_e[2]))),
"SearchEngineTheoremProducer::propAndrAF");
}
Assumptions a(andr_th, b_th);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(andr_th.getExpr());
exprs.push_back(b_th.getExpr());
pfs.push_back(andr_th.getProof());
pfs.push_back(b_th.getProof());
// can we note which branch to take?
pf = newPf("prop_andr_af", exprs, pfs);
}
return newTheorem(andr_e[0].negate(), a, pf);
}
Theorem
SearchEngineTheoremProducer::propAndrAT(const Theorem& andr_th,
const Theorem& l_th,
const Theorem& r_th) {
const Expr& andr_e(andr_th.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(andr_e.getKind() == AND_R &&
l_th.proves(andr_e[1]) && r_th.proves(andr_e[2]),
"SearchEngineTheoremProducer::propAndrAT");
}
Assumptions a(andr_th, l_th);
a.add(r_th);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(andr_th.getExpr());
exprs.push_back(l_th.getExpr());
exprs.push_back(r_th.getExpr());
pfs.push_back(andr_th.getProof());
pfs.push_back(l_th.getProof());
pfs.push_back(r_th.getProof());
pf = newPf("prop_andr_at", exprs, pfs);
}
return newTheorem(andr_e[0], a, pf);
}
void
SearchEngineTheoremProducer::propAndrLRT(const Theorem& andr_th,
const Theorem& a_th,
Theorem* l_th,
Theorem* r_th) {
const Expr& andr_e(andr_th.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(andr_e.getKind() == AND_R && a_th.proves(andr_e[0]),
"SearchEngineTheoremProducer::propAndrLRT");
}
Assumptions a(andr_th, a_th);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(andr_th.getExpr());
exprs.push_back(a_th.getExpr());
pfs.push_back(andr_th.getProof());
pfs.push_back(a_th.getProof());
pf = newPf("prop_andr_lrt", exprs, pfs);
}
if (l_th) *l_th = newTheorem(andr_e[1], a, pf);
if (r_th) *r_th = newTheorem(andr_e[2], a, pf);
}
Theorem
SearchEngineTheoremProducer::propAndrLF(const Theorem& andr_th,
const Theorem& a_th,
const Theorem& r_th) {
const Expr& andr_e(andr_th.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(andr_e.getKind() == AND_R &&
a_th.refutes(andr_e[0]) && r_th.proves(andr_e[2]),
"SearchEngineTheoremProducer::propAndrLF");
}
Assumptions a(andr_th, a_th);
a.add(r_th);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(andr_th.getExpr());
exprs.push_back(a_th.getExpr());
exprs.push_back(r_th.getExpr());
pfs.push_back(andr_th.getProof());
pfs.push_back(a_th.getProof());
pfs.push_back(r_th.getProof());
pf = newPf("prop_andr_lf", exprs, pfs);
}
return newTheorem(andr_e[1].negate(), a, pf);
}
Theorem
SearchEngineTheoremProducer::propAndrRF(const Theorem& andr_th,
const Theorem& a_th,
const Theorem& l_th) {
const Expr& andr_e(andr_th.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(andr_e.getKind() == AND_R &&
a_th.refutes(andr_e[0]) && l_th.proves(andr_e[1]),
"SearchEngineTheoremProducer::propAndrRF");
}
Assumptions a(andr_th, a_th);
a.add(l_th);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(andr_th.getExpr());
exprs.push_back(a_th.getExpr());
exprs.push_back(l_th.getExpr());
pfs.push_back(andr_th.getProof());
pfs.push_back(a_th.getProof());
pfs.push_back(l_th.getProof());
pf = newPf("prop_andr_rf", exprs, pfs);
}
return newTheorem(andr_e[2].negate(), a, pf);
}
Theorem
SearchEngineTheoremProducer::confAndrAT(const Theorem& andr_th,
const Theorem& a_th,
bool left,
const Theorem& b_th) {
const Expr& andr_e(andr_th.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(andr_e.getKind() == AND_R && a_th.proves(andr_e[0]) &&
((left && b_th.refutes(andr_e[1])) ||
(!left && b_th.refutes(andr_e[2]))),
"SearchEngineTheoremProducer::confAndrAT");
}
Assumptions a(andr_th, a_th);
a.add(b_th);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(andr_th.getExpr());
exprs.push_back(a_th.getExpr());
exprs.push_back(b_th.getExpr());
pfs.push_back(andr_th.getProof());
pfs.push_back(a_th.getProof());
pfs.push_back(b_th.getProof());
// can we note which branch to take?
pf = newPf("conf_andr_at", exprs, pfs);
}
return newTheorem(d_em->falseExpr(), a, pf);
}
Theorem
SearchEngineTheoremProducer::confAndrAF(const Theorem& andr_th,
const Theorem& a_th,
const Theorem& l_th,
const Theorem& r_th) {
const Expr& andr_e(andr_th.getExpr());
if(CHECK_PROOFS) {
CHECK_SOUND(andr_e.getKind() == AND_R && a_th.refutes(andr_e[0]) &&
l_th.proves(andr_e[1]) && r_th.proves(andr_e[2]),
"SearchEngineTheoremProducer::confAndrAF");
}
Assumptions a;
Proof pf;
if(withAssumptions()) {
a.add(andr_th);
a.add(a_th);
a.add(l_th);
a.add(r_th);
}
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(andr_th.getExpr());
exprs.push_back(a_th.getExpr());
exprs.push_back(l_th.getExpr());
exprs.push_back(r_th.getExpr());
pfs.push_back(andr_th.getProof());
pfs.push_back(a_th.getProof());
pfs.push_back(l_th.getProof());
pfs.push_back(r_th.getProof());
pf = newPf("conf_andr_af", exprs, pfs);
}
return newTheorem(d_em->falseExpr(), a, pf);
}
Theorem
SearchEngineTheoremProducer::propIffr(const Theorem& iffr_th,
int p,
const Theorem& a_th,
const Theorem& b_th)
{
int a(-1), b(-1);
if(CHECK_PROOFS)
CHECK_SOUND(p == 0 || p == 1 || p == 2,
"SearchEngineTheoremProducer::propIffr: p="
+int2string(p));
switch (p) {
case 0: a = 1; b = 2; break;
case 1: a = 0; b = 2; break;
case 2: a = 0; b = 1; break;
}
const Expr& iffr_e(iffr_th.getExpr());
bool v0 = a_th.proves(iffr_e[a]);
bool v1 = b_th.proves(iffr_e[b]);
if (CHECK_PROOFS) {
CHECK_SOUND(iffr_e.getKind() == IFF_R &&
(v0 || a_th.refutes(iffr_e[a])) &&
(v1 || b_th.refutes(iffr_e[b])),
"SearchEngineTheoremProducer::propIffr");
}
Assumptions aa;
Proof pf;
if (withAssumptions()) {
aa.add(iffr_th);
aa.add(a_th);
aa.add(b_th);
}
if (withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(iffr_th.getExpr());
exprs.push_back(a_th.getExpr());
exprs.push_back(b_th.getExpr());
pfs.push_back(iffr_th.getProof());
pfs.push_back(a_th.getProof());
pfs.push_back(b_th.getProof());
pf = newPf("prop_iffr", exprs, pfs);
}
return newTheorem(v0 == v1 ? iffr_e[p] : iffr_e[p].negate(), aa, pf);
}
Theorem
SearchEngineTheoremProducer::confIffr(const Theorem& iffr_th,
const Theorem& i_th,
const Theorem& l_th,
const Theorem& r_th)
{
const Expr& iffr_e(iffr_th.getExpr());
bool v0 = i_th.proves(iffr_e[0]);
bool v1 = l_th.proves(iffr_e[1]);
bool v2 = r_th.proves(iffr_e[2]);
if (CHECK_PROOFS) {
CHECK_SOUND(iffr_e.getKind() == IFF_R &&
(v0 || i_th.refutes(iffr_e[0])) &&
(v1 || l_th.refutes(iffr_e[1])) &&
(v2 || r_th.refutes(iffr_e[2])) &&
((v0 && v1 != v2) || (!v0 && v1 == v2)),
"SearchEngineTheoremProducer::confIffr");
}
Assumptions a;
Proof pf;
if (withAssumptions()) {
a.add(iffr_th);
a.add(i_th);
a.add(l_th);
a.add(r_th);
}
if (withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(iffr_th.getExpr());
exprs.push_back(i_th.getExpr());
exprs.push_back(l_th.getExpr());
exprs.push_back(r_th.getExpr());
pfs.push_back(iffr_th.getProof());
pfs.push_back(i_th.getProof());
pfs.push_back(l_th.getProof());
pfs.push_back(r_th.getProof());
pf = newPf("conf_iffr", exprs, pfs);
}
return newTheorem(d_em->falseExpr(), a, pf);
}
Theorem
SearchEngineTheoremProducer::propIterIte(const Theorem& iter_th,
bool left,
const Theorem& if_th,
const Theorem& then_th)
{
const Expr& iter_e(iter_th.getExpr());
bool v0 = if_th.proves(iter_e[1]);
bool v1 = then_th.proves(iter_e[left ? 2 : 3]);
if (CHECK_PROOFS) {
CHECK_SOUND(iter_e.getKind() == ITE_R &&
(v0 || if_th.refutes(iter_e[1])) &&
(v1 || then_th.refutes(iter_e[left ? 2 : 3])) &&
v0 == left,
"SearchEngineTheoremProducer::propIterIte");
}
Assumptions a;
Proof pf;
if (withAssumptions()) {
a.add(iter_th);
a.add(if_th);
a.add(then_th);
}
if (withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(iter_th.getExpr());
exprs.push_back(if_th.getExpr());
exprs.push_back(then_th.getExpr());
pfs.push_back(iter_th.getProof());
pfs.push_back(if_th.getProof());
pfs.push_back(then_th.getProof());
pf = newPf("prop_iter_ite", exprs, pfs);
}
return newTheorem(v1 ? iter_e[0] : iter_e[0].negate(), a, pf);
}
void
SearchEngineTheoremProducer::propIterIfThen(const Theorem& iter_th,
bool left,
const Theorem& ite_th,
const Theorem& then_th,
Theorem* if_th,
Theorem* else_th)
{
const Expr& iter_e(iter_th.getExpr());
bool v0 = ite_th.proves(iter_e[0]);
bool v1 = then_th.proves(iter_e[left ? 2 : 3]);
if (CHECK_PROOFS) {
CHECK_SOUND(iter_e.getKind() == ITE_R &&
(v0 || ite_th.refutes(iter_e[0])) &&
(v1 || then_th.refutes(iter_e[left ? 2 : 3])) &&
v0 != v1,
"SearchEngineTheoremProducer::propIterIfThen");
}
Assumptions a;
Proof pf;
if (withAssumptions()) {
a.add(iter_th);
a.add(ite_th);
a.add(then_th);
}
if (withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(iter_th.getExpr());
exprs.push_back(ite_th.getExpr());
exprs.push_back(then_th.getExpr());
pfs.push_back(iter_th.getProof());
pfs.push_back(ite_th.getProof());
pfs.push_back(then_th.getExpr());
pf = newPf("prop_iter_if_then", exprs, pfs);
}
if (if_th)
*if_th = newTheorem(left ? iter_e[1].negate() : iter_e[1], a, pf);
if (else_th)
*else_th = newTheorem(v0 ? iter_e[left ? 3 : 2] : iter_e[left ? 3 : 2].negate(), a, pf);
}
Theorem
SearchEngineTheoremProducer::propIterThen(const Theorem& iter_th,
const Theorem& ite_th,
const Theorem& if_th)
{
const Expr& iter_e(iter_th.getExpr());
bool v0 = ite_th.proves(iter_e[0]);
bool v1 = if_th.proves(iter_e[1]);
if (CHECK_PROOFS) {
CHECK_SOUND(iter_e.getKind() == ITE_R &&
(v0 || ite_th.refutes(iter_e[0])) &&
(v1 || if_th.refutes(iter_e[1])),
"SearchEngineTheoremProducer::propIterThen");
}
Assumptions a;
Proof pf;
if (withAssumptions()) {
a.add(iter_th);
a.add(ite_th);
a.add(if_th);
}
if (withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(iter_th.getExpr());
exprs.push_back(ite_th.getExpr());
exprs.push_back(if_th.getExpr());
pfs.push_back(iter_th.getProof());
pfs.push_back(ite_th.getProof());
pfs.push_back(if_th.getExpr());
pf = newPf("prop_iter_then", exprs, pfs);
}
return newTheorem(v1 ?
(v0 ? iter_e[2] : iter_e[2].negate()) :
(v0 ? iter_e[3] : iter_e[3].negate()), a, pf);
}
Theorem
SearchEngineTheoremProducer::confIterThenElse(const Theorem& iter_th,
const Theorem& ite_th,
const Theorem& then_th,
const Theorem& else_th)
{
const Expr& iter_e(iter_th.getExpr());
bool v0 = ite_th.proves(iter_e[0]);
bool v1 = then_th.proves(iter_e[2]);
bool v2 = else_th.proves(iter_e[3]);
if (CHECK_PROOFS) {
CHECK_SOUND(iter_e.getKind() == ITE_R &&
(v0 || ite_th.refutes(iter_e[0])) &&
(v1 || then_th.refutes(iter_e[2])) &&
(v2 || else_th.refutes(iter_e[3])) &&
((v0 && !v1 && !v2) || (!v0 && v1 && v2)),
"SearchEngineTheoremProducer::confIterThenElse");
}
Assumptions a;
Proof pf;
if (withAssumptions()) {
a.add(iter_th);
a.add(ite_th);
a.add(then_th);
a.add(else_th);
}
if (withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(iter_th.getExpr());
exprs.push_back(ite_th.getExpr());
exprs.push_back(then_th.getExpr());
exprs.push_back(else_th.getExpr());
pfs.push_back(iter_th.getProof());
pfs.push_back(ite_th.getProof());
pfs.push_back(then_th.getExpr());
pfs.push_back(else_th.getExpr());
pf = newPf("conf_iter_then_else", exprs, pfs);
}
return newTheorem(d_em->falseExpr(), a, pf);
}
Theorem
SearchEngineTheoremProducer::confIterIfThen(const Theorem& iter_th,
bool left,
const Theorem& ite_th,
const Theorem& if_th,
const Theorem& then_th)
{
const Expr& iter_e(iter_th.getExpr());
bool v0 = ite_th.proves(iter_e[0]);
bool v1 = if_th.proves(iter_e[1]);
bool v2 = then_th.proves(iter_e[left ? 2 : 3]);
if (CHECK_PROOFS) {
CHECK_SOUND(iter_e.getKind() == ITE_R &&
(v0 || ite_th.refutes(iter_e[0])) &&
(v1 || if_th.refutes(iter_e[1])) &&
(v2 || then_th.refutes(iter_e[left ? 2 : 3])) &&
v1 == left && v0 != v2,
"SearchEngineTheoremProducer::confIterThenElse");
}
Assumptions a;
Proof pf;
if (withAssumptions()) {
a.add(iter_th);
a.add(ite_th);
a.add(if_th);
a.add(then_th);
}
if (withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.push_back(iter_th.getExpr());
exprs.push_back(ite_th.getExpr());
exprs.push_back(if_th.getExpr());
exprs.push_back(then_th.getExpr());
pfs.push_back(iter_th.getProof());
pfs.push_back(ite_th.getProof());
pfs.push_back(if_th.getExpr());
pfs.push_back(then_th.getExpr());
pf = newPf("conf_iter_then_else", exprs, pfs);
}
return newTheorem(d_em->falseExpr(), a, pf);
}
// "Conflict" rule (all literals in a clause become FALSE)
// { G_j |- !l_j, j in [1..n] } , G |- (OR l_1 ... l_n) ==> FALSE
Theorem
SearchEngineTheoremProducer::conflictRule(const std::vector<Theorem>& thms,
const Theorem& clause) {
Expr e(clause.getExpr());
if(CHECK_PROOFS) {
// Soundness check: first, check the form of the 'clause' theorem
CHECK_SOUND(e.isOr(),
"SearchEngineTheoremProducer::unitProp: "
"bad theorem in clause = "+clause.toString());
// Now, check correspondence of thms to the disjunction
CHECK_SOUND(((int)thms.size()) == e.arity(),
"SearchEngineTheoremProducer::conflictRule: "
"wrong number of theorems"
"\n thms.size = " + int2string(thms.size())
+"\n clause.arity = " + int2string(e.arity()));
for(unsigned j=0; j<thms.size(); j++) {
Expr ej(e[j]), ek(thms[j].getExpr());
CHECK_SOUND((ej.isNot() && ej[0] == ek) || (ek.isNot() && ej == ek[0]),
"SearchEngineTheoremProducer::conflictRule: "
"wrong theorem["+int2string(j)+"]"
"\n thm = " + thms[j].toString() +
"\n literal = " + e[j].toString() +
"\n clause = " + clause.toString());
}
}
Assumptions a(thms);
a.add(clause);
Proof pf;
if(withProof()) {
vector<Proof> pfs;
vector<Expr> exprs;
exprs.reserve(thms.size() + 1);
pfs.reserve(thms.size()+1);
const vector<Theorem>::const_iterator iend = thms.end();
for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
exprs.push_back(i->getExpr());
pfs.push_back(i->getProof());
}
exprs.push_back(clause.getExpr());
pfs.push_back(clause.getProof());
pf = newPf("conflict", exprs, pfs);
}
return newTheorem(d_em->falseExpr(), a, pf);
}
///////////////////////////////////////////////////////////////////////
//// Conjunctive Normal Form (CNF) proof rules
///////////////////////////////////////////////////////////////////////
Theorem
SearchEngineTheoremProducer::andCNFRule(const Theorem& thm) {
return opCNFRule(thm, AND, "and_cnf_rule");
}
Theorem
SearchEngineTheoremProducer::orCNFRule(const Theorem& thm) {
return opCNFRule(thm, OR, "or_cnf_rule");
}
Theorem
SearchEngineTheoremProducer::impCNFRule(const Theorem& thm) {
return opCNFRule(thm, IMPLIES, "implies_cnf_rule");
}
Theorem
SearchEngineTheoremProducer::iffCNFRule(const Theorem& thm) {
return opCNFRule(thm, IFF, "iff_cnf_rule");
}
Theorem
SearchEngineTheoremProducer::iteCNFRule(const Theorem& thm) {
return opCNFRule(thm, ITE, "ite_cnf_rule");
}
Theorem
SearchEngineTheoremProducer::iteToClauses(const Theorem& ite) {
const Expr& iteExpr = ite.getExpr();
if(CHECK_PROOFS) {
CHECK_SOUND(iteExpr.isITE() && iteExpr.getType().isBool(),
"SearchEngineTheoremProducer::iteToClauses("+iteExpr.toString()
+")\n Argument must be a Boolean ITE");
}
const Expr& cond = iteExpr[0];
const Expr& t1 = iteExpr[1];
const Expr& t2 = iteExpr[2];
Proof pf;
if(withProof())
pf = newPf("ite_to_clauses", iteExpr, ite.getProof());
return newTheorem((cond.negate() || t1) && (cond || t2), ite.getAssumptionsRef(), pf);
}
Theorem
SearchEngineTheoremProducer::iffToClauses(const Theorem& iff) {
if(CHECK_PROOFS) {
CHECK_SOUND(iff.isRewrite() && iff.getLHS().getType().isBool(),
"SearchEngineTheoremProducer::iffToClauses("+iff.getExpr().toString()
+")\n Argument must be a Boolean IFF");
}
const Expr& t1 = iff.getLHS();
const Expr& t2 = iff.getRHS();
Proof pf;
if(withProof())
pf = newPf("iff_to_clauses", iff.getExpr(), iff.getProof());
return newTheorem((t1.negate() || t2) && (t1 || t2.negate()), iff.getAssumptionsRef(), pf);
}
/////////////////////////////////////////////////////////////////////////
//// helper functions for CNF (Conjunctive Normal Form) conversion
/////////////////////////////////////////////////////////////////////////
Theorem
SearchEngineTheoremProducer::opCNFRule(const Theorem& thm,
int kind,
const string& ruleName) {
TRACE("mycnf", "opCNFRule["+d_em->getKindName(kind)+"](",
thm.getExpr(), ") {");
ExprMap<Expr> localCache;
if(CHECK_PROOFS) {
Expr phiIffVar = thm.getExpr();
CHECK_SOUND(phiIffVar.isIff(),
"SearchEngineTheoremProducer::opCNFRule("
+d_em->getKindName(kind)+"): "
"input must be an IFF: thm = " + phiIffVar.toString());
CHECK_SOUND(phiIffVar[0].getKind() == kind,
"SearchEngineTheoremProducer::opCNFRule("
+d_em->getKindName(kind)+"): "
"input phi has wrong kind: thm = " + phiIffVar.toString());
CHECK_SOUND(phiIffVar[0] != phiIffVar[1],
"SearchEngineTheoremProducer::opCNFRule("
+d_em->getKindName(kind)+"): "
"wrong input thm = " + phiIffVar.toString());
for(Expr::iterator it=phiIffVar[0].begin(), itend=phiIffVar[0].end();
it!=itend;++it){
CHECK_SOUND(phiIffVar[1] != *it,
"SearchEngineTheoremProducer::opCNFRule("
+d_em->getKindName(kind)+"): "
"wrong input thm = " + phiIffVar.toString());
}
}
const Expr& phi = thm.getExpr()[0];
const Expr& phiVar = thm.getExpr()[1];
std::vector<Expr> boundVars;
std::vector<Expr> boundVarsAndLiterals;
std::vector<Expr> equivs;
for(Expr::iterator i=phi.begin(), iend=phi.end(); i != iend; i++) {
// First, strip the negation and check if the formula is atomic
Expr tmp(*i);
while(tmp.isNot())
tmp = tmp[0];
if(tmp.isPropAtom())
boundVarsAndLiterals.push_back(*i);
else
boundVarsAndLiterals.push_back(findInLocalCache(*i, localCache,
boundVars));
}
for(ExprMap<Expr>::iterator it=localCache.begin(), itend=localCache.end();
it != itend; it++) {
DebugAssert((*it).second.isIff(),
"SearchEngineTheoremProducer::opCNFRule: " +
(*it).second.toString());
DebugAssert(!(*it).second[0].isPropLiteral() &&
(*it).second[1].isAbsLiteral(),
"SearchEngineTheoremProducer::opCNFRule: " +
(*it).second.toString());
equivs.push_back((*it).second);
}
DebugAssert(boundVarsAndLiterals.size() == (unsigned)phi.arity(),
"SearchEngineTheoremProducer::opCNFRule: "
"wrong size of boundvars: phi = " + phi.toString());
DebugAssert(boundVars.size() == equivs.size(),
"SearchEngineTheoremProducer::opCNFRule: "
"wrong size of boundvars: phi = " + phi.toString());
Expr cnfInput = phi.arity() > 0 ? Expr(phi.getOp(), boundVarsAndLiterals) : phi;
Expr result = convertToCNF(phiVar, cnfInput);
if(boundVars.size() > 0)
result =
d_em->newClosureExpr(EXISTS, boundVars, result.andExpr(andExpr(equivs)));
Proof pf;
if(withProof())
pf = newPf(ruleName, thm.getExpr(), thm.getProof());
Theorem res(newTheorem(result, thm.getAssumptionsRef(), pf));
TRACE("mycnf", "opCNFRule["+d_em->getKindName(kind)+"] => ", res.getExpr(),
" }");
return res;
}
//! produces the CNF for the formula v <==> phi
Expr SearchEngineTheoremProducer::convertToCNF(const Expr& v, const Expr & phi) {
//we assume that v \iff phi. v is the newVar corresponding to phi
Expr::iterator i = phi.begin(), iend = phi.end();
std::vector<Expr> clauses;
std::vector<Expr> lastClause;
switch(phi.getKind()) {
case AND: {
const Expr& negV = v.negate();
lastClause.push_back(v);
for(;i!=iend; ++i) {
clauses.push_back(negV.orExpr(*i));
lastClause.push_back(i->negate());
}
clauses.push_back(orExpr(lastClause));
}
break;
case OR:{
lastClause.push_back(v.negate());
for(;i!=iend; ++i) {
clauses.push_back(v.orExpr(i->negate()));
lastClause.push_back(*i);
}
clauses.push_back(orExpr(lastClause));
}
break;
case IFF: {
const Expr& v1 = phi[0];
const Expr& v2 = phi[1];
Expr negV = v.negate();
Expr negv1 = v1.negate();
Expr negv2 = v2.negate();
clauses.push_back(Expr(OR, negV, negv1, v2));
clauses.push_back(Expr(OR, negV, v1, negv2));
clauses.push_back(Expr(OR, v, v1, v2));
clauses.push_back(Expr(OR, v, negv1, negv2));
} break;
case IMPLIES:{
const Expr& v1 = phi[0];
const Expr& v2 = phi[1];
Expr negV = v.negate();
Expr negv1 = v1.negate();
Expr negv2 = v2.negate();
clauses.push_back(Expr(OR, negV, negv1, v2));
clauses.push_back(v.orExpr(v1));
clauses.push_back(v.orExpr(negv2));
}
break;
case ITE: {
const Expr& v1 = phi[0];
const Expr& v2 = phi[1];
const Expr& v3 = phi[2];
const Expr& negV = v.negate();
const Expr& negv1 = v1.negate();
const Expr& negv2 = v2.negate();
const Expr& negv3 = v3.negate();
clauses.push_back(Expr(OR, negV, negv1, v2));
clauses.push_back(Expr(OR, negV, v1, v3));
clauses.push_back(Expr(OR, v, negv1, negv2));
clauses.push_back(Expr(OR, v, v1, negv3));
}
break;
default:
DebugAssert(false, "SearchEngineTheoremProducer::convertToCNF: "
"bad operator in phi = "+phi.toString());
break;
}
return andExpr(clauses);
}
///////////////////////////////////////////////////////////////////////
// helper functions for CNF converters
///////////////////////////////////////////////////////////////////////
Expr SearchEngineTheoremProducer::findInLocalCache(const Expr& i,
ExprMap<Expr>& localCache,
vector<Expr>& boundVars) {
TRACE("mycnf", "findInLocalCache(", i.toString(), ") { ");
Expr boundVar;
unsigned int negationDepth = 0;
ExprMap<Expr>::iterator it;
Expr phi = i;
while(phi.isNot()) {
phi = phi[0];
negationDepth++;
}
it = localCache.find(phi);
Expr v;
if(it != localCache.end()) {
v = ((*it).second)[1];
IF_DEBUG(debugger.counter("CNF Local Cache Hits")++);
}
else {
v = d_em->newBoundVarExpr(i.getType());
boundVars.push_back(v);
localCache[phi] = phi.iffExpr(v);
}
if(negationDepth % 2 != 0)
v = !v;
TRACE("mycnf", "findInLocalCache => ", v, " }");
return v;
}
syntax highlighted by Code2HTML, v. 0.9.1