CVC3::CommonProofRules Class Reference

#include <common_proof_rules.h>

Inheritance diagram for CVC3::CommonProofRules:

[legend]List of all members.

Public Member Functions

virtual ~CommonProofRules ()
Destructor.
virtual Theorem3 queryTCC (const Theorem &phi, const Theorem &D_phi)=0
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}$
.
virtual Theorem3 implIntro3 (const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)=0
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}$
virtual Theorem assumpRule (const Expr &a, int scope=-1)=0
$\frac{}{a\vdash a}$
virtual Theorem reflexivityRule (const Expr &a)=0
$\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}$
virtual Theorem rewriteReflexivity (const Expr &a_eq_a)=0
==> (a == a) IFF TRUE
virtual Theorem symmetryRule (const Theorem &a1_eq_a2)=0
$\frac{a_1=a_2}{a_2=a_1}$
(same for IFF)
virtual Theorem rewriteUsingSymmetry (const Expr &a1_eq_a2)=0
$\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}$
virtual Theorem transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0
$\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}$
(same for IFF)
virtual Theorem substitutivityRule (const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
virtual Theorem substitutivityRule (const Expr &e, const Theorem &thm1, const Theorem &thm2)=0
Optimized case for expr with two children.
virtual Theorem substitutivityRule (const Op &op, const std::vector< Theorem > &thms)=0
$\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}$
virtual Theorem substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)=0
$\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$ .
virtual Theorem substitutivityRule (const Expr &e, const int changed, const Theorem &thm)=0
virtual Theorem contradictionRule (const Theorem &e, const Theorem &not_e)=0
$\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e} {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}}$
virtual Theorem excludedMiddle (const Expr &e)=0
virtual Theorem iffTrue (const Theorem &e)=0
$\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}$
virtual Theorem iffNotFalse (const Theorem &e)=0
$\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}$
virtual Theorem iffTrueElim (const Theorem &e)=0
$\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}$
virtual Theorem iffFalseElim (const Theorem &e)=0
$\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}$
virtual Theorem iffContrapositive (const Theorem &thm)=0
e1 <=> e2 ==> ~e1 <=> ~e2
virtual Theorem notNotElim (const Theorem &not_not_e)=0
$\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}$
virtual Theorem iffMP (const Theorem &e1, const Theorem &e1_iff_e2)=0
$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2}$
virtual Theorem implMP (const Theorem &e1, const Theorem &e1_impl_e2)=0
$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2}$
virtual Theorem andElim (const Theorem &e, int i)=0
$\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}$
virtual Theorem andIntro (const Theorem &e1, const Theorem &e2)=0
$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash e_2} {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2}$
virtual Theorem andIntro (const std::vector< Theorem > &es)=0
$\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}$
virtual Theorem implIntro (const Theorem &phi, const std::vector< Expr > &assump)=0
Implication introduction rule:
$\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi} {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}$
.
virtual Theorem implContrapositive (const Theorem &thm)=0
e1 => e2 ==> ~e2 => ~e1
virtual Theorem rewriteIteTrue (const Expr &e)=0
==> ITE(TRUE, e1, e2) == e1
virtual Theorem rewriteIteFalse (const Expr &e)=0
==> ITE(FALSE, e1, e2) == e2
virtual Theorem rewriteIteSame (const Expr &e)=0
==> ITE(c, e, e) == e
virtual Theorem notToIff (const Theorem &not_e)=0
$\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}$
virtual Theorem xorToIff (const Expr &e)=0
$\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}$
virtual Theorem rewriteIff (const Expr &e)=0
==> (e1 <=> e2) <=> [simplified expr]
virtual Theorem rewriteAnd (const Expr &e)=0
==> AND(e1,e2) IFF [simplified expr]
virtual Theorem rewriteOr (const Expr &e)=0
==> OR(e1,...,en) IFF [simplified expr]
virtual Theorem rewriteNotTrue (const Expr &e)=0
==> NOT TRUE IFF FALSE
virtual Theorem rewriteNotFalse (const Expr &e)=0
==> NOT FALSE IFF TRUE
virtual Theorem rewriteNotNot (const Expr &e)=0
==> NOT NOT e IFF e, takes !!e
virtual Theorem rewriteNotForall (const Expr &forallExpr)=0
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
virtual Theorem rewriteNotExists (const Expr &existsExpr)=0
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
virtual Expr skolemize (const Expr &e)=0
virtual Theorem skolemizeRewrite (const Expr &e)=0
virtual Theorem skolemizeRewriteVar (const Expr &e)=0
Special version of skolemizeRewrite for "EXISTS x. t = x".
virtual Theorem varIntroRule (const Expr &e)=0
|- EXISTS x. e = x
virtual Theorem skolemize (const Theorem &thm)=0
If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm.
virtual Theorem varIntroSkolem (const Expr &e)=0
Retrun a theorem "|- e = v" for a new Skolem constant v.
virtual Theorem trueTheorem ()=0
==> TRUE
virtual Theorem rewriteAnd (const Theorem &e)=0
AND(e1,e2) ==> [simplified expr].
virtual Theorem rewriteOr (const Theorem &e)=0
OR(e1,...,en) ==> [simplified expr].
virtual std::vector< Theorem > & getSkolemAxioms ()=0
virtual void clearSkolemAxioms ()=0
virtual Theorem ackermann (const Expr &e1, const Expr &e2)=0
virtual Theorem liftOneITE (const Expr &e)=0

Detailed Description

Definition at line 46 of file common_proof_rules.h.

Constructor & Destructor Documentation

virtual CVC3::CommonProofRules::~CommonProofRules ( ) [inline, virtual]

Destructor.

Definition at line 49 of file common_proof_rules.h.

Member Function Documentation

virtual Theorem3 CVC3::CommonProofRules::queryTCC	(	const Theorem &	phi,
		const Theorem &	D_phi
	)			`[pure 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}$

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::VCL::query().

virtual Theorem3 CVC3::CommonProofRules::implIntro3	(	const Theorem3 &	phi,
		const std::vector< Expr > &	assump,
		const std::vector< Theorem > &	tccs
	)			`[pure 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}$

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::VCL::deriveClosure().

virtual Theorem CVC3::CommonProofRules::assumpRule	(	const Expr &	a,
		int	scope = `-1`
	)			`[pure virtual]`

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchSat::assertLit(), CVC3::SearchSat::check(), CVC3::SearchImplBase::newIntAssumption(), CVC3::ExprTransform::newPPrec(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), and CVC3::CompleteInstPreProcessor::simplifyQuant().

virtual Theorem CVC3::CommonProofRules::reflexivityRule ( const Expr & a ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::rewriteReflexivity ( const Expr & a_eq_a ) [pure virtual]

==> (a == a) IFF TRUE

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::rewriteCore(), and CVC3::TheoryCore::rewriteLitCore().

virtual Theorem CVC3::CommonProofRules::symmetryRule ( const Theorem & a1_eq_a2 ) [pure virtual]

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

(same for IFF)

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::enqueueCNFrec(), SAT::CNF_Manager::replaceITErec(), and CVC3::Theory::symmetryRule().

virtual Theorem CVC3::CommonProofRules::rewriteUsingSymmetry ( const Expr & a1_eq_a2 ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::assertFormula(), CVC3::TheoryArray::rewrite(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::rewriteLitCore(), and CVC3::TheoryCore::update().

virtual Theorem CVC3::CommonProofRules::transitivityRule	(	const Theorem &	a1_eq_a2,
		const Theorem &	a2_eq_a3
	)			`[pure virtual]`

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

(same for IFF)

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::findInCNFCache(), CVC3::ExprTransform::newPPrec(), CVC3::ExprTransform::preprocess(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::SearchImplBase::replaceITE(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::substitute(), and CVC3::Theory::transitivityRule().

virtual Theorem CVC3::CommonProofRules::substitutivityRule	(	const Expr &	e,
		const Theorem &	thm
	)			`[pure virtual]`

Optimized case for expr with one child.

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryArith3::assertFact(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::Theory::findReduce(), CVC3::ExprTransform::newPPrec(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryCore::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), CVC3::Theory::substitutivityRule(), CVC3::TheoryCore::update(), and CVC3::Theory::updateHelper().

virtual Theorem CVC3::CommonProofRules::substitutivityRule	(	const Expr &	e,
		const Theorem &	thm1,
		const Theorem &	thm2
	)			`[pure virtual]`

Optimized case for expr with two children.

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::substitutivityRule	(	const Op &	op,
		const std::vector< Theorem > &	thms
	)			`[pure 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)}$

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::substitutivityRule	(	const Expr &	e,
		const std::vector< unsigned > &	changed,
		const std::vector< Theorem > &	thms
	)			`[pure 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.

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::substitutivityRule	(	const Expr &	e,
		const int	changed,
		const Theorem &	thm
	)			`[pure virtual]`

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::contradictionRule	(	const Theorem &	e,
		const Theorem &	not_e
	)			`[pure virtual]`

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchEngineFast::addLiteralFact(), and CVC3::SearchEngineFast::recordFact().

virtual Theorem CVC3::CommonProofRules::excludedMiddle ( const Expr & e ) [pure virtual]

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchSat::addSplitter().

virtual Theorem CVC3::CommonProofRules::iffTrue ( const Theorem & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::assertFormula(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryCore::setFindLiteral(), and CVC3::TheoryCore::simplifyOp().

virtual Theorem CVC3::CommonProofRules::iffNotFalse ( const Theorem & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::iffTrueElim ( const Theorem & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::setFindLiteral(), CVC3::SearchEngineFast::split(), CVC3::TheoryUF::update(), and CVC3::TheoryCore::update().

virtual Theorem CVC3::CommonProofRules::iffFalseElim ( const Theorem & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::processUpdates(), CVC3::TheoryCore::registerAtom(), CVC3::SearchEngineFast::split(), and CVC3::TheoryCore::update().

virtual Theorem CVC3::CommonProofRules::iffContrapositive ( const Theorem & thm ) [pure 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').

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::findInCNFCache(), and CVC3::TheoryCore::rewriteLiteral().

virtual Theorem CVC3::CommonProofRules::notNotElim ( const Theorem & not_not_e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchEngineFast::split().

virtual Theorem CVC3::CommonProofRules::iffMP	(	const Theorem &	e1,
		const Theorem &	e1_iff_e2
	)			`[pure virtual]`

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theory::iffMP(), CVC3::ExprTransform::preprocess(), CVC3::SearchImplBase::replaceITE(), and SAT::CNF_Manager::replaceITErec().

virtual Theorem CVC3::CommonProofRules::implMP	(	const Theorem &	e1,
		const Theorem &	e1_impl_e2
	)			`[pure virtual]`

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryArithOld::addToBuffer(), and CVC3::TheoryArithOld::registerAtom().

virtual Theorem CVC3::CommonProofRules::andElim	(	const Theorem &	e,
		int	i
	)			`[pure virtual]`

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryCore::checkSolved(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryBitvector::solve().

virtual Theorem CVC3::CommonProofRules::andIntro	(	const Theorem &	e1,
		const Theorem &	e2
	)			`[pure virtual]`

$\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash e_2} {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2}$

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchSimple::addNonLiteralFact(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), and CVC3::TheoryArith3::solvedForm().

virtual Theorem CVC3::CommonProofRules::andIntro ( const std::vector< Theorem > & es ) [pure 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}$

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::implIntro	(	const Theorem &	phi,
		const std::vector< Expr > &	assump
	)			`[pure 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$

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::implContrapositive ( const Theorem & thm ) [pure 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').

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::rewriteIteTrue ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::Theory::rewriteIte().

virtual Theorem CVC3::CommonProofRules::rewriteIteFalse ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::Theory::rewriteIte().

virtual Theorem CVC3::CommonProofRules::rewriteIteSame ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::Theory::rewriteIte(), and CVC3::TheoryCore::simplifyOp().

virtual Theorem CVC3::CommonProofRules::notToIff ( const Theorem & not_e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::setFindLiteral().

virtual Theorem CVC3::CommonProofRules::xorToIff ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CommonProofRules::rewriteIff ( const Expr & e ) [pure virtual]

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

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite(), and CVC3::TheoryBitvector::rewriteBoolean().

virtual Theorem CVC3::CommonProofRules::rewriteAnd ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryBitvector::computeTCC(), CVC3::Theory::computeTCC(), and CVC3::Theory::rewriteAnd().

virtual Theorem CVC3::CommonProofRules::rewriteOr ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchEngineFast::fixConflict(), and CVC3::Theory::rewriteOr().

virtual Theorem CVC3::CommonProofRules::rewriteNotTrue ( const Expr & e ) [pure virtual]

==> NOT TRUE IFF FALSE

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::CoreTheoremProducer::NotToIte(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryBitvector::rewriteBoolean(), and CVC3::TheoryCore::rewriteLitCore().

virtual Theorem CVC3::CommonProofRules::rewriteNotFalse ( const Expr & e ) [pure virtual]

==> NOT FALSE IFF TRUE

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::rewriteNotNot ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::findInCNFCache(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryCore::rewriteCore(), and CVC3::TheoryCore::rewriteLitCore().

virtual Theorem CVC3::CommonProofRules::rewriteNotForall ( const Expr & forallExpr ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::rewriteNotExists ( const Expr & existsExpr ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

virtual Expr CVC3::CommonProofRules::skolemize ( const Expr & e ) [pure virtual]

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryCore::assertFormula(), CVC3::SearchEngineFast::bcp(), CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryBitvector::solve().

virtual Theorem CVC3::CommonProofRules::skolemizeRewrite ( const Expr & e ) [pure 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)

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::skolemizeRewriteVar ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::varIntroRule ( const Expr & e ) [pure virtual]

|- EXISTS x. e = x

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::TheoryArithNew::getVariableIntroThm().

virtual Theorem CVC3::CommonProofRules::skolemize ( const Theorem & thm ) [pure 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))

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::varIntroSkolem ( const Expr & e ) [pure virtual]

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

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

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryArray::renameExpr(), CVC3::SearchImplBase::replaceITE(), SAT::CNF_Manager::replaceITErec(), and CVC3::TheoryArithOld::TheoryArithOld().

virtual Theorem CVC3::CommonProofRules::trueTheorem ( ) [pure virtual]

==> TRUE

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchSat::check(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::VCL::query(), and CVC3::SearchSimple::SearchSimple().

virtual Theorem CVC3::CommonProofRules::rewriteAnd ( const Theorem & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::rewriteOr ( const Theorem & e ) [pure virtual]

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

Implemented in CVC3::CommonTheoremProducer.

virtual std::vector<Theorem>& CVC3::CommonProofRules::getSkolemAxioms ( ) [pure virtual]

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::processResult().

virtual void CVC3::CommonProofRules::clearSkolemAxioms ( ) [pure virtual]

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::SearchImplBase::checkValid().

virtual Theorem CVC3::CommonProofRules::ackermann	(	const Expr &	e1,
		const Expr &	e2
	)			`[pure virtual]`

Implemented in CVC3::CommonTheoremProducer.

virtual Theorem CVC3::CommonProofRules::liftOneITE ( const Expr & e ) [pure virtual]

Implemented in CVC3::CommonTheoremProducer.

Referenced by CVC3::ExprTransform::newPPrec(), and CVC3::ExprTransform::simplifyWithCare().

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

common_proof_rules.h

Generated on Wed Nov 18 16:14:37 2009 for CVC3 by

1.5.2