CVC3::SearchEngineRules Class Reference
[Proof Rules for the Search Engines]

API to the proof rules for the Search Engines. More...

#include <search_rules.h>

Inheritance diagram for CVC3::SearchEngineRules:

[legend]

List of all members.

Public Member Functions

• virtual ~SearchEngineRules ()

  Destructor.
  

• 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:

  

  .
  

• virtual Theorem negIntro (const Expr &not_a, const Theorem &pfFalse)=0

  Negation introduction:

  

  .
  

• virtual Theorem caseSplit (const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)=0

  Case split:

  

  .
  

• virtual Theorem conflictClause (const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)=0

  Conflict clause rule:

  

  .
  

• virtual Theorem cutRule (const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)=0

  Cut rule:

  

  .
  

• virtual Theorem unitProp (const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0

  Unit propagation rule:

  

  .
  

• 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].
  

• virtual Theorem orCNFRule (const Theorem &thm)=0

  OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
  

• virtual Theorem impCNFRule (const Theorem &thm)=0

  (x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
  

• virtual Theorem iffCNFRule (const Theorem &thm)=0

  (x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
  

• virtual Theorem iteCNFRule (const Theorem &thm)=0

  ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
  

• virtual Theorem iteToClauses (const Theorem &ite)=0

  ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2).
  

• virtual Theorem iffToClauses (const Theorem &iff)=0

  e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
  

• virtual Theorem satProof (const Expr &queryExpr, const Proof &satProof)=0

---

Detailed Description

API to the proof rules for the Search Engines.

Definition at line 35 of file search_rules.h.

---

The documentation for this class was generated from the following file:

• search_rules.h