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 Theorem learnedClause (const Theorem &thm)=0

  Learned clause rule:

  

  .
  

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

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

---

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

---