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

API to the CNF proof rules. More...

#include <cnf_rules.h>

Inheritance diagram for CVC3::CNF_Rules:

[legend]

List of all members.

Public Member Functions

• virtual ~CNF_Rules ()

  Destructor.
  

• virtual void learnedClauses (const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0

  Learned clause rule:

  

  .
  

• virtual Theorem ifLiftRule (const Expr &e, int itePos)=0

  |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
  

• virtual Theorem CNFAddUnit (const Theorem &thm)=0
• virtual Theorem CNFConvert (const Expr &e, const Theorem &thm)=0
• virtual Theorem CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos)=0
• virtual Theorem CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0

---

Detailed Description

API to the CNF proof rules.

Definition at line 34 of file cnf_rules.h.

---

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

• cnf_rules.h