#include <common_theorem_producer.h>

Inherits CVC3::CommonProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::CommonTheoremProducer:

Public Member Functions
	CommonTheoremProducer (TheoremManager *tm)

virtual	~CommonTheoremProducer ()

Theorem3	queryTCC (const Theorem &phi, const Theorem &D_phi)
	Convert 2-valued formula to 3-valued by discharging its TCC ( $D_\phi$ ): $\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}} {\Gamma_1,\,\Gamma_2\vdash_3\phi}$ .

Theorem3	implIntro3 (const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)
	3-valued implication introduction rule: $\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}} {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3 (\bigwedge_{i=1}^n\alpha_i)\to\phi}$

Theorem	assumpRule (const Expr &a, int scope=-1)
	$\frac{}{a\vdash a}$

Theorem	reflexivityRule (const Expr &a)
	$\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}$

Theorem	rewriteReflexivity (const Expr &t)
	==> (a == a) IFF TRUE

Theorem	symmetryRule (const Theorem &a1_eq_a2)
	$\frac{a_1=a_2}{a_2=a_1}$ (same for IFF)

Theorem	rewriteUsingSymmetry (const Expr &a1_eq_a2)
	$\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}$

Theorem	transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
	$\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}$ (same for IFF)

Theorem	substitutivityRule (const Expr &e, const Theorem &thm)
	Optimized case for expr with one child.

Theorem	substitutivityRule (const Expr &e, const Theorem &thm1, const Theorem &thm2)
	Optimized case for expr with two children.

Theorem	substitutivityRule (const Op &op, const std::vector< Theorem > &thms)
	$\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}$

Theorem	substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)
	$\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}$ except that only those arguments are given that $c_i\not=d_i$ .

Theorem	substitutivityRule (const Expr &e, const int changed, const Theorem &thm)

Theorem	contradictionRule (const Theorem &e, const Theorem &not_e)
	$\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e} {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}}$

Theorem	excludedMiddle (const Expr &e)

Theorem	iffTrue (const Theorem &e)
	$\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}$

Theorem	iffNotFalse (const Theorem &e)
	$\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}$

Theorem	iffTrueElim (const Theorem &e)
	$\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}$

Theorem	iffFalseElim (const Theorem &e)
	$\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}$

Theorem	iffContrapositive (const Theorem &thm)
	e1 <=> e2 ==> ~e1 <=> ~e2

Theorem	notNotElim (const Theorem &e)
	$\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}$

Theorem	iffMP (const Theorem &e1, const Theorem &e1_iff_e2)
	$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2}$

Theorem	implMP (const Theorem &e1, const Theorem &e1_impl_e2)
	$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2}$

Theorem	andElim (const Theorem &e, int i)
	$\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}$

Theorem	andIntro (const Theorem &e1, const Theorem &e2)
	e1, e2 ==> AND(e1, e2)

Theorem	andIntro (const std::vector< Theorem > &es)
	$\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n} {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i}$

Theorem	implIntro (const Theorem &phi, const std::vector< Expr > &assump)
	Implication introduction rule: $\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi} {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}$ .

Theorem	implContrapositive (const Theorem &thm)
	e1 => e2 ==> ~e2 => ~e1

Theorem	rewriteIteTrue (const Expr &e)
	==> ITE(TRUE, e1, e2) == e1

Theorem	rewriteIteFalse (const Expr &e)
	==> ITE(FALSE, e1, e2) == e2

Theorem	rewriteIteSame (const Expr &e)
	==> ITE(c, e, e) == e

Theorem	notToIff (const Theorem &not_e)
	$\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}$

Theorem	xorToIff (const Expr &e)
	$\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}$

Theorem	rewriteIff (const Expr &e)
	==> (e1 <=> e2) <=> [simplified expr]

Theorem	rewriteAnd (const Expr &e)
	==> AND(e1,e2) IFF [simplified expr]

Theorem	rewriteOr (const Expr &e)
	==> OR(e1,...,en) IFF [simplified expr]

Theorem	rewriteNotTrue (const Expr &e)
	==> NOT TRUE IFF FALSE

Theorem	rewriteNotFalse (const Expr &e)
	==> NOT FALSE IFF TRUE

Theorem	rewriteNotNot (const Expr &e)
	==> NOT NOT e IFF e, takes !!e

Theorem	rewriteNotForall (const Expr &forallExpr)
	==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e

Theorem	rewriteNotExists (const Expr &existsExpr)
	==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e

Expr	skolemize (const Expr &e)

Theorem	skolemizeRewrite (const Expr &e)

Theorem	skolemizeRewriteVar (const Expr &e)
	Special version of skolemizeRewrite for "EXISTS x. t = x".

Theorem	varIntroRule (const Expr &e)
	\|- EXISTS x. e = x

Theorem	skolemize (const Theorem &thm)
	If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm.

Theorem	varIntroSkolem (const Expr &e)
	Retrun a theorem "\|- e = v" for a new Skolem constant v.

Theorem	trueTheorem ()
	==> TRUE

Theorem	rewriteAnd (const Theorem &e)
	AND(e1,e2) ==> [simplified expr].

Theorem	rewriteOr (const Theorem &e)
	OR(e1,...,en) ==> [simplified expr].

Theorem	ackermann (const Expr &e1, const Expr &e2)

Theorem	liftOneITE (const Expr &e)

std::vector< Theorem > &	getSkolemAxioms ()

void	clearSkolemAxioms ()

Public Member Functions inherited from CVC3::CommonProofRules
virtual	~CommonProofRules ()
	Destructor.

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 Member Functions
void	findITE (const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)
	Helper function for liftOneITE.

Private Attributes
std::vector< Theorem >	d_skolem_axioms

CDMap< Expr, Theorem >	d_skolemized_thms

CDMap< Expr, Theorem >	d_skolemVars
	Mapping of e to "\|- e = v" for fresh Skolem vars v.

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

Detailed Description

Definition at line 40 of file common_theorem_producer.h.

Constructor & Destructor Documentation

CommonTheoremProducer::CommonTheoremProducer ( TheoremManager * tm )

Definition at line 40 of file common_theorem_producer.cpp.

virtual CVC3::CommonTheoremProducer::~CommonTheoremProducer ( )

inlinevirtual

Definition at line 60 of file common_theorem_producer.h.

Member Function Documentation

void CommonTheoremProducer::findITE	(	const Expr &	e,
		Expr &	condition,
		Expr &	thenpart,
		Expr &	elsepart
	)

private

Helper function for liftOneITE.

Definition at line 1322 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::containsTermITE(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Type::isBool(), and CVC3::Expr::isITE().

Referenced by liftOneITE().

Theorem3 CommonTheoremProducer::queryTCC	(	const Theorem &	phi,
		const Theorem &	D_phi
	)

virtual

Convert 2-valued formula to 3-valued by discharging its TCC ( $D_\phi$ ):

$\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}} {\Gamma_1,\,\Gamma_2\vdash_3\phi}$

.

Implements CVC3::CommonProofRules.

Definition at line 55 of file common_theorem_producer.cpp.

References CVC3::Assumptions::add(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem3(), and CVC3::TheoremProducer::withProof().

Theorem3 CommonTheoremProducer::implIntro3	(	const Theorem3 &	phi,
		const std::vector< Expr > &	assump,
		const std::vector< Theorem > &	tccs
	)

virtual

3-valued implication introduction rule:

$\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}} {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3 (\bigwedge_{i=1}^n\alpha_i)\to\phi}$

Parameters

phi	is the formula $\phi$
assump	is the vector of assumptions $\alpha_1\ldots\alpha_n$
tccs	is the vector of TCCs for assumptions $D_{\alpha_1}\ldots D_{\alpha_n}$

Implements CVC3::CommonProofRules.

Definition at line 85 of file common_theorem_producer.cpp.

References CVC3::Assumptions::add(), CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem3::getAssumptionsRef(), CVC3::Theorem3::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem3::getProof(), CVC3::Expr::impExpr(), CVC3::int2string(), CVC3::Theorem::isAssump(), CVC3::Theorem::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem3(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::assumpRule	(	const Expr &	a,
		int	scope = `-1`
	)

virtual

$\frac{}{a\vdash a}$

Implements CVC3::CommonProofRules.

Definition at line 154 of file common_theorem_producer.cpp.

References CVC3::TheoremProducer::newAssumption(), CVC3::TheoremProducer::newLabel(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::reflexivityRule ( const Expr & a )

virtual

$\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}$

Implements CVC3::CommonProofRules.

Definition at line 162 of file common_theorem_producer.cpp.

References CVC3::TheoremProducer::newReflTheorem().

Referenced by rewriteIff(), rewriteUsingSymmetry(), substitutivityRule(), symmetryRule(), transitivityRule(), and trueTheorem().

Theorem CommonTheoremProducer::rewriteReflexivity ( const Expr & a_eq_a )

virtual

==> (a == a) IFF TRUE

Implements CVC3::CommonProofRules.

Definition at line 168 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Referenced by rewriteIff().

Theorem CommonTheoremProducer::symmetryRule ( const Theorem & a1_eq_a2 )

virtual

$\frac{a_1=a_2}{a_2=a_1}$

(same for IFF)

Implements CVC3::CommonProofRules.

Definition at line 187 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Type::isBool(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteUsingSymmetry ( const Expr & a1_eq_a2 )

virtual

$\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}$

Implements CVC3::CommonProofRules.

Definition at line 221 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::iffExpr(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::Type::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), and CVC3::TheoremProducer::withProof().

Referenced by rewriteIff().

Theorem CommonTheoremProducer::transitivityRule	(	const Theorem &	a1_eq_a2,
		const Theorem &	a2_eq_a3
	)

virtual

$\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}$

(same for IFF)

Implements CVC3::CommonProofRules.

Definition at line 245 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Type::isNull(), CVC3::Theorem::isNull(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::substitutivityRule	(	const Expr &	e,
		const Theorem &	thm
	)

virtual

Optimized case for expr with one child.

Implements CVC3::CommonProofRules.

Definition at line 302 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::Theorem::isRefl(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::setSubst(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by substitutivityRule().

Theorem CommonTheoremProducer::substitutivityRule	(	const Expr &	e,
		const Theorem &	thm1,
		const Theorem &	thm2
	)

virtual

Optimized case for expr with two children.

Implements CVC3::CommonProofRules.

Definition at line 332 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::Theorem::isRefl(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::setSubst(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::substitutivityRule	(	const Op &	op,
		const std::vector< Theorem > &	thms
	)

virtual

$\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}$

Implements CVC3::CommonProofRules.

Definition at line 373 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_tm, CVC3::TheoremManager::getEM(), IF_DEBUG, CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Theorem::setSubst(), CVC3::Op::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::substitutivityRule	(	const Expr &	e,
		const std::vector< unsigned > &	changed,
		const std::vector< Theorem > &	thms
	)

virtual

$\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}$

except that only those arguments are given that $c_i\not=d_i$ .

Parameters

e	is the original expression $op(c_1,\ldots,c_n)$ .
changed	is the vector of indices of changed kids
thms	are the theorems for the changed kids.

Implements CVC3::CommonProofRules.

Definition at line 424 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Expr::getOp(), IF_DEBUG, CVC3::Theorem::isRefl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Theorem::setSubst(), substitutivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::substitutivityRule	(	const Expr &	e,
		const int	changed,
		const Theorem &	thm
	)

virtual

Theorem CommonTheoremProducer::contradictionRule	(	const Theorem &	e,
		const Theorem &	not_e
	)

virtual

$\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e} {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}}$

Implements CVC3::CommonProofRules.

Definition at line 561 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::excludedMiddle ( const Expr & e )

virtual

Implements CVC3::CommonProofRules.

Definition at line 580 of file common_theorem_producer.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::orExpr(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffTrue ( const Theorem & e )

virtual

$\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}$

Implements CVC3::CommonProofRules.

Definition at line 591 of file common_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffNotFalse ( const Theorem & e )

virtual

$\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}$

Implements CVC3::CommonProofRules.

Definition at line 602 of file common_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffTrueElim ( const Theorem & e )

virtual

$\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}$

Implements CVC3::CommonProofRules.

Definition at line 612 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Referenced by trueTheorem().

Theorem CommonTheoremProducer::iffFalseElim ( const Theorem & e )

virtual

$\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}$

Implements CVC3::CommonProofRules.

Definition at line 626 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::isFalse(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffContrapositive ( const Theorem & thm )

virtual

e1 <=> e2 ==> ~e1 <=> ~e2

$\frac{\Gamma\vdash e_1\Leftrightarrow e_2} {\Gamma\vdash\sim e_1\Leftrightarrow\sim e_2}$

Where ~e is the inverse of e (that is, ~(!e') = e').

Implements CVC3::CommonProofRules.

Definition at line 641 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Theorem::isRewrite(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::notNotElim ( const Theorem & not_not_e )

virtual

$\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}$

Implements CVC3::CommonProofRules.

Definition at line 655 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffMP	(	const Theorem &	e1,
		const Theorem &	e1_iff_e2
	)

virtual

$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2}$

Implements CVC3::CommonProofRules.

Definition at line 667 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Referenced by rewriteAnd(), rewriteOr(), skolemize(), and varIntroSkolem().

Theorem CommonTheoremProducer::implMP	(	const Theorem &	e1,
		const Theorem &	e1_impl_e2
	)

virtual

$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2}$

Implements CVC3::CommonProofRules.

Definition at line 692 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::andElim	(	const Theorem &	e,
		int	i
	)

virtual

$\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}$

Implements CVC3::CommonProofRules.

Definition at line 718 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::int2string(), CVC3::Expr::isAnd(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::andIntro	(	const Theorem &	e1,
		const Theorem &	e2
	)

virtual

e1, e2 ==> AND(e1, e2)

Implements CVC3::CommonProofRules.

Definition at line 733 of file common_theorem_producer.cpp.

Theorem CommonTheoremProducer::andIntro ( const std::vector< Theorem > & es )

virtual

$\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n} {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i}$

Implements CVC3::CommonProofRules.

Definition at line 741 of file common_theorem_producer.cpp.

References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::implIntro	(	const Theorem &	phi,
		const std::vector< Expr > &	assump
	)

virtual

Implication introduction rule:

$\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi} {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}$

.

Parameters

phi	is the formula $\phi$
assump	is the vector of assumptions $\alpha_1\ldots\alpha_n$

Implements CVC3::CommonProofRules.

Definition at line 775 of file common_theorem_producer.cpp.

References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::impExpr(), CVC3::int2string(), CVC3::Theorem::isAssump(), CVC3::Theorem::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::implContrapositive ( const Theorem & thm )

virtual

e1 => e2 ==> ~e2 => ~e1

$\frac{\Gamma\vdash e_1\Rightarrow e_2} {\Gamma\vdash\sim e_2\Rightarrow\sim e_1}$

Where ~e is the inverse of e (that is, ~(!e') = e').

Implements CVC3::CommonProofRules.

Definition at line 825 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteIteTrue ( const Expr & e )

virtual

==> ITE(TRUE, e1, e2) == e1

Implements CVC3::CommonProofRules.

Definition at line 841 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteIteFalse ( const Expr & e )

virtual

==> ITE(FALSE, e1, e2) == e2

Implements CVC3::CommonProofRules.

Definition at line 863 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteIteSame ( const Expr & e )

virtual

==> ITE(c, e, e) == e

Implements CVC3::CommonProofRules.

Definition at line 885 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::notToIff ( const Theorem & not_e )

virtual

$\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}$

Implements CVC3::CommonProofRules.

Definition at line 906 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::xorToIff ( const Expr & e )

virtual

$\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}$

Implements CVC3::CommonProofRules.

Definition at line 922 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isXor(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteIff ( const Expr & e )

virtual

==> (e1 <=> e2) <=> [simplified expr]

Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc.

Implements CVC3::CommonProofRules.

Definition at line 941 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), FALSE_EXPR, CVC3::ExprManager::falseExpr(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), NOT, reflexivityRule(), rewriteReflexivity(), rewriteUsingSymmetry(), TRUE_EXPR, and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteAnd ( const Expr & e )

virtual

==> AND(e1,e2) IFF [simplified expr]

Implements CVC3::CommonProofRules.

Definition at line 989 of file common_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprMap< Data >::size(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Referenced by rewriteAnd().

Theorem CommonTheoremProducer::rewriteOr ( const Expr & e )

virtual

==> OR(e1,...,en) IFF [simplified expr]

Implements CVC3::CommonProofRules.

Definition at line 1028 of file common_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isFalse(), CVC3::Expr::isOr(), CVC3::Expr::isTrue(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), CVC3::ExprMap< Data >::size(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Referenced by rewriteOr().

Theorem CommonTheoremProducer::rewriteNotTrue ( const Expr & e )

virtual

==> NOT TRUE IFF FALSE

Implements CVC3::CommonProofRules.

Definition at line 1066 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isNot(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotFalse ( const Expr & e )

virtual

==> NOT FALSE IFF TRUE

Implements CVC3::CommonProofRules.

Definition at line 1078 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotNot ( const Expr & e )

virtual

==> NOT NOT e IFF e, takes !!e

Implements CVC3::CommonProofRules.

Definition at line 1090 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotForall ( const Expr & forallExpr )

virtual

==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e

Implements CVC3::CommonProofRules.

Definition at line 1102 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), EXISTS, CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotExists ( const Expr & existsExpr )

virtual

==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e

Implements CVC3::CommonProofRules.

Definition at line 1117 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), FORALL, CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::Expr::isExists(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Expr CommonTheoremProducer::skolemize ( const Expr & e )

virtual

Implements CVC3::CommonProofRules.

Definition at line 1131 of file common_theorem_producer.cpp.

References CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::Expr::skolemExpr(), and CVC3::Expr::substExpr().

Referenced by skolemizeRewrite().

Theorem CommonTheoremProducer::skolemizeRewrite ( const Expr & e )

virtual

skolem rewrite rule: Introduces axiom |- Exists(x) phi(x) <=> phi(c) where c is a constant defined by the expression Exists(x) phi(x)

Implements CVC3::CommonProofRules.

Definition at line 1145 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isExists(), CVC3::TheoremProducer::newLabel(), CVC3::TheoremProducer::newRWTheorem(), skolemize(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().

Referenced by skolemize().

Theorem CommonTheoremProducer::skolemizeRewriteVar ( const Expr & e )

virtual

Special version of skolemizeRewrite for "EXISTS x. t = x".

Implements CVC3::CommonProofRules.

Definition at line 1165 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getBody(), CVC3::Expr::getOp(), CVC3::Expr::getVars(), CVC3::Expr::iffExpr(), CVC3::Expr::isEq(), CVC3::Expr::isExists(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newLabel(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::skolemExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by varIntroSkolem().

Theorem CommonTheoremProducer::varIntroRule ( const Expr & e )

virtual

|- EXISTS x. e = x

Implements CVC3::CommonProofRules.

Definition at line 1202 of file common_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), EXISTS, CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Referenced by varIntroSkolem().

Theorem CommonTheoremProducer::skolemize ( const Theorem & thm )

virtual

If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm.

Parameters

thm	is the Theorem(EXISTS x: phi(x))

Implements CVC3::CommonProofRules.

Definition at line 1223 of file common_theorem_producer.cpp.

References d_skolem_axioms, d_skolemized_thms, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), iffMP(), CVC3::CDMap< Key, Data, HashFcn >::insert(), CVC3::Expr::isExists(), CVC3::Expr::skolemExpr(), skolemizeRewrite(), and TRACE.

Theorem CommonTheoremProducer::varIntroSkolem ( const Expr & e )

virtual

Retrun a theorem "|- e = v" for a new Skolem constant v.

This is equivalent to skolemize(d_core->varIntroRule(e)), only more efficient.

Implements CVC3::CommonProofRules.

Definition at line 1250 of file common_theorem_producer.cpp.

References d_skolem_axioms, d_skolemized_thms, d_skolemVars, DebugAssert, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::Expr::getVars(), iffMP(), CVC3::CDMap< Key, Data, HashFcn >::insert(), CVC3::Expr::isExists(), skolemizeRewriteVar(), CVC3::Expr::toString(), and varIntroRule().

Theorem CommonTheoremProducer::trueTheorem ( )

virtual

==> TRUE

Implements CVC3::CommonProofRules.

Definition at line 1280 of file common_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, iffTrueElim(), reflexivityRule(), and CVC3::ExprManager::trueExpr().

Theorem CommonTheoremProducer::rewriteAnd ( const Theorem & e )

virtual

AND(e1,e2) ==> [simplified expr].

Implements CVC3::CommonProofRules.

Definition at line 1286 of file common_theorem_producer.cpp.

References CVC3::Theorem::getExpr(), iffMP(), and rewriteAnd().

Theorem CommonTheoremProducer::rewriteOr ( const Theorem & e )

virtual

OR(e1,...,en) ==> [simplified expr].

Implements CVC3::CommonProofRules.

Definition at line 1292 of file common_theorem_producer.cpp.

References CVC3::Theorem::getExpr(), iffMP(), and rewriteOr().

Theorem CommonTheoremProducer::ackermann	(	const Expr &	e1,
		const Expr &	e2
	)

virtual

Implements CVC3::CommonProofRules.

Definition at line 1298 of file common_theorem_producer.cpp.

References AND, CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getOp(), CVC3::Expr::isApply(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CommonTheoremProducer::liftOneITE ( const Expr & e )

virtual

Implements CVC3::CommonProofRules.

Definition at line 1359 of file common_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::containsTermITE(), CVC3::Assumptions::emptyAssump(), findITE(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

std::vector<Theorem>& CVC3::CommonTheoremProducer::getSkolemAxioms ( )

inlinevirtual

Implements CVC3::CommonProofRules.

Definition at line 126 of file common_theorem_producer.h.

References d_skolem_axioms.

void CVC3::CommonTheoremProducer::clearSkolemAxioms ( )

inlinevirtual

Implements CVC3::CommonProofRules.

Definition at line 127 of file common_theorem_producer.h.

References d_skolem_axioms.

Member Data Documentation

std::vector<Theorem> CVC3::CommonTheoremProducer::d_skolem_axioms

private

Definition at line 46 of file common_theorem_producer.h.

Referenced by clearSkolemAxioms(), getSkolemAxioms(), skolemize(), and varIntroSkolem().

CDMap<Expr, Theorem> CVC3::CommonTheoremProducer::d_skolemized_thms

private

Definition at line 50 of file common_theorem_producer.h.

Referenced by skolemize(), and varIntroSkolem().

CDMap<Expr, Theorem> CVC3::CommonTheoremProducer::d_skolemVars

private

Mapping of e to "|- e = v" for fresh Skolem vars v.

Definition at line 53 of file common_theorem_producer.h.

Referenced by varIntroSkolem().

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

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation