Proof Rules for the Search Engines

Classes

• class CVC3::CNF_Rules

  API to the CNF proof rules. More...
  

Functions

• virtual CVC3::CNF_Rules::~CNF_Rules ()

  Destructor.
  

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

  Learned clause rule:

  

  .
  

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

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

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

---

Function Documentation

virtual CVC3::CNF_Rules::~CNF_Rules

(

)

[inline, virtual, inherited]

Destructor.

Definition at line 40 of file cnf_rules.h.

virtual void CVC3::CNF_Rules::learnedClauses	(	const Theorem &	thm,
		std::vector< Theorem > &	,
		bool	newLemma
	)			[pure virtual, inherited]

Learned clause rule:

.

Parameters:

thm

is the theorem Each and should be literals can also be

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::addLemma(), and SAT::CNF_Manager::convertLemma().

virtual Theorem CVC3::CNF_Rules::ifLiftRule	(	const Expr &	e,
		int	itePos
	)			[pure virtual, inherited]

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

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::replaceITErec().

virtual Theorem CVC3::CNF_Rules::CNFAddUnit

(

const Theorem &

thm

)

[pure virtual, inherited]

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), and SAT::CNF_Manager::translateExpr().

virtual Theorem CVC3::CNF_Rules::CNFConvert	(	const Expr &	e,
		const Theorem &	thm
	)			[pure virtual, inherited]

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::convertLemma().

virtual Theorem CVC3::CNF_Rules::CNFtranslate	(	const Expr &	before,
		const Expr &	after,
		std::string	reason,
		int	pos
	)			[pure virtual, inherited]

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::translateExprRec().

virtual Theorem CVC3::CNF_Rules::CNFITEtranslate	(	const Expr &	before,
		const std::vector< Expr > &	after,
		const std::vector< Theorem > &	thms,
		int	pos
	)			[pure virtual, inherited]

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::translateExprRec().