#include <datatype_theorem_producer.h>

Inherits CVC3::DatatypeProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::DatatypeTheoremProducer:

Public Member Functions
	DatatypeTheoremProducer (TheoryDatatype *theoryDatatype)
	Constructor.

Theorem	dummyTheorem (const CDList< Theorem > &facts, const Expr &e)

Theorem	rewriteSelCons (const CDList< Theorem > &facts, const Expr &e)

Theorem	rewriteTestCons (const Expr &e)

Theorem	decompose (const Theorem &e)

Theorem	noCycle (const Expr &e)

Public Member Functions inherited from CVC3::DatatypeProofRules
virtual	~DatatypeProofRules ()

Public Member Functions inherited from CVC3::TheoremProducer
	TheoremProducer (TheoremManager *tm)

virtual	~TheoremProducer ()

bool	withProof ()
	Testing whether to generate proofs.

bool	withAssumptions ()
	Testing whether to generate assumptions.

Proof	newLabel (const Expr &e)
	Create a new proof label (bound variable) for an assumption (formula)

Proof	newPf (const std::string &name)

Proof	newPf (const std::string &name, const Expr &e)

Proof	newPf (const std::string &name, const Proof &pf)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2)

Proof	newPf (const std::string &name, const Expr &e, const Proof &pf)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)

Proof	newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)

Proof	newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)

Proof	newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const std::vector< Expr > &args)

Proof	newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)

Proof	newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)

Proof	newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)

Proof	newPf (const Proof &label, const Expr &frm, const Proof &pf)
	Creating LAMBDA-abstraction (LAMBDA label formula proof)

Proof	newPf (const Proof &label, const Proof &pf)
	Creating LAMBDA-abstraction (LAMBDA label proof).

Proof	newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
	Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf)

Proof	newPf (const std::vector< Proof > &labels, const Proof &pf)

Private Attributes
TheoryDatatype *	d_theoryDatatype

Additional Inherited Members
Protected Member Functions inherited from CVC3::TheoremProducer
Theorem	newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
	Create a new theorem. See also newRWTheorem() and newReflTheorem()

Theorem	newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
	Create a rewrite theorem: lhs = rhs.

Theorem	newReflTheorem (const Expr &e)
	Create a reflexivity theorem.

Theorem	newAssumption (const Expr &thm, const Proof &pf, int scope=-1)

Theorem3	newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)

Theorem3	newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)

void	soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)

Protected Attributes inherited from CVC3::TheoremProducer
TheoremManager *	d_tm

ExprManager *	d_em

const bool *	d_checkProofs

Op	d_pfOp

Expr	d_hole