CVC3
2.4.1
|
Classes | |
class | CVC3::SearchEngineRules |
API to the proof rules for the Search Engines. More... |
Functions | |
virtual | CVC3::SearchEngineRules::~SearchEngineRules () |
Destructor. | |
virtual Theorem | CVC3::SearchEngineRules::eliminateSkolemAxioms (const Theorem &tFalse, const std::vector< Theorem > &delta)=0 |
virtual Theorem | CVC3::SearchEngineRules::proofByContradiction (const Expr &a, const Theorem &pfFalse)=0 |
Proof by contradiction:
| |
virtual Theorem | CVC3::SearchEngineRules::negIntro (const Expr ¬_a, const Theorem &pfFalse)=0 |
Negation introduction:
| |
virtual Theorem | CVC3::SearchEngineRules::caseSplit (const Expr &a, const Theorem &a_proves_c, const Theorem ¬_a_proves_c)=0 |
Case split:
| |
virtual Theorem | CVC3::SearchEngineRules::conflictClause (const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)=0 |
Conflict clause rule:
| |
virtual Theorem | CVC3::SearchEngineRules::cutRule (const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)=0 |
Cut rule:
| |
virtual Theorem | CVC3::SearchEngineRules::unitProp (const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0 |
Unit propagation rule:
| |
virtual Theorem | CVC3::SearchEngineRules::conflictRule (const std::vector< Theorem > &thms, const Theorem &clause)=0 |
"Conflict" rule (all literals in a clause become FALSE)
| |
virtual Theorem | CVC3::SearchEngineRules::propAndrAF (const Theorem &andr_th, bool left, const Theorem &b_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::propAndrAT (const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)=0 |
virtual void | CVC3::SearchEngineRules::propAndrLRT (const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::propAndrLF (const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::propAndrRF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::confAndrAT (const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::confAndrAF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::propIffr (const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::confIffr (const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::propIterIte (const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)=0 |
virtual void | CVC3::SearchEngineRules::propIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::propIterThen (const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::confIterThenElse (const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::confIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)=0 |
virtual Theorem | CVC3::SearchEngineRules::andCNFRule (const Theorem &thm)=0 |
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v]. | |
virtual Theorem | CVC3::SearchEngineRules::orCNFRule (const Theorem &thm)=0 |
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]. | |
virtual Theorem | CVC3::SearchEngineRules::impCNFRule (const Theorem &thm)=0 |
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v] | |
virtual Theorem | CVC3::SearchEngineRules::iffCNFRule (const Theorem &thm)=0 |
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v] | |
virtual Theorem | CVC3::SearchEngineRules::iteCNFRule (const Theorem &thm)=0 |
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]. | |
virtual Theorem | CVC3::SearchEngineRules::iteToClauses (const Theorem &ite)=0 |
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2) | |
virtual Theorem | CVC3::SearchEngineRules::iffToClauses (const Theorem &iff)=0 |
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2) | |
virtual Theorem | CVC3::SearchEngineRules::satProof (const Expr &queryExpr, const Proof &satProof)=0 |
|
inlinevirtual |
Destructor.
Definition at line 41 of file search_rules.h.
|
pure virtual |
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.
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::processResult().
|
pure virtual |
Proof by contradiction:
.
does not have to be present in the assumptions.
a | is the assumption A |
pfFalse | is the theorem ![]() |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::processResult().
|
pure virtual |
Negation introduction:
.
not_a | is the formula ![]() ![]() ![]() ![]() |
pfFalse | is the theorem ![]() |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::processResult().
|
pure virtual |
Case split:
.
a | is the assumption A to split on |
a_proves_c | is the theorem ![]() |
not_a_proves_c | is the theorem ![]() |
Implemented in CVC3::SearchEngineTheoremProducer.
|
pure virtual |
Conflict clause rule:
.
thm | is the theorem ![]() |
lits | is the vector of literals Ai. They must be present in the set of assumptions of thm. |
gamma | FIXME: document this!! |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchEngineFast::analyzeUIPs().
|
pure virtual |
Cut rule:
.
thmsA | is a vector of theorems ![]() |
as_prove_b | is the theorem ![]() |
Implemented in CVC3::SearchEngineTheoremProducer.
|
pure virtual |
Unit propagation rule:
.
clause | is the proof of the clause ![]() |
i | is the index (0..n-1) of the literal to be unit-propagated |
thms | is the vector of theorems ![]() |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Variable::deriveThmRec(), and CVC3::SearchEngineFast::unitPropagation().
|
pure virtual |
"Conflict" rule (all literals in a clause become FALSE)
clause | is the proof of the clause ![]() |
thms | is the vector of theorems ![]() |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Variable::deriveThmRec(), and CVC3::SearchEngineFast::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::Circuit::propagate().
|
pure virtual |
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules().
|
pure virtual |
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules().
|
pure virtual |
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules().
|
pure virtual |
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules().
|
pure virtual |
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules().
|
pure virtual |
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::enqueueCNFrec().
|
pure virtual |
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
Implemented in CVC3::SearchEngineTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules().
|
pure virtual |
Implemented in CVC3::SearchEngineTheoremProducer.