CVC3
2.4.1
|
API to the proof rules for the Search Engines. More...
#include <search_rules.h>
Public Member Functions | |
virtual | ~SearchEngineRules () |
Destructor. More... | |
virtual Theorem | eliminateSkolemAxioms (const Theorem &tFalse, const std::vector< Theorem > &delta)=0 |
virtual Theorem | proofByContradiction (const Expr &a, const Theorem &pfFalse)=0 |
Proof by contradiction:
. More... | |
virtual Theorem | negIntro (const Expr ¬_a, const Theorem &pfFalse)=0 |
Negation introduction:
. More... | |
virtual Theorem | caseSplit (const Expr &a, const Theorem &a_proves_c, const Theorem ¬_a_proves_c)=0 |
Case split:
. More... | |
virtual Theorem | conflictClause (const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)=0 |
Conflict clause rule:
. More... | |
virtual Theorem | cutRule (const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)=0 |
Cut rule:
. More... | |
virtual Theorem | unitProp (const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0 |
Unit propagation rule:
. More... | |
virtual Theorem | conflictRule (const std::vector< Theorem > &thms, const Theorem &clause)=0 |
"Conflict" rule (all literals in a clause become FALSE)
| |
virtual Theorem | propAndrAF (const Theorem &andr_th, bool left, const Theorem &b_th)=0 |
virtual Theorem | propAndrAT (const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)=0 |
virtual void | propAndrLRT (const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)=0 |
virtual Theorem | propAndrLF (const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)=0 |
virtual Theorem | propAndrRF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)=0 |
virtual Theorem | confAndrAT (const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)=0 |
virtual Theorem | confAndrAF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)=0 |
virtual Theorem | propIffr (const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)=0 |
virtual Theorem | confIffr (const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)=0 |
virtual Theorem | propIterIte (const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)=0 |
virtual void | propIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)=0 |
virtual Theorem | propIterThen (const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)=0 |
virtual Theorem | confIterThenElse (const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)=0 |
virtual Theorem | confIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)=0 |
virtual Theorem | andCNFRule (const Theorem &thm)=0 |
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v]. More... | |
virtual Theorem | orCNFRule (const Theorem &thm)=0 |
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]. More... | |
virtual Theorem | impCNFRule (const Theorem &thm)=0 |
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v] More... | |
virtual Theorem | iffCNFRule (const Theorem &thm)=0 |
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v] More... | |
virtual Theorem | iteCNFRule (const Theorem &thm)=0 |
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]. More... | |
virtual Theorem | iteToClauses (const Theorem &ite)=0 |
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2) More... | |
virtual Theorem | iffToClauses (const Theorem &iff)=0 |
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2) More... | |
virtual Theorem | satProof (const Expr &queryExpr, const Proof &satProof)=0 |
API to the proof rules for the Search Engines.
Definition at line 35 of file search_rules.h.