CVCL::CommonTheoremProducer Class Reference

#include <common_theorem_producer.h>

Inheritance diagram for CVCL::CommonTheoremProducer:

[legend]Collaboration diagram for CVCL::CommonTheoremProducer:

[legend]List of all members.

Public Member Functions

CommonTheoremProducer (TheoremManager *tm)
virtual ~CommonTheoremProducer ()
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 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 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 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 notToIff (const Theorem &not_e)
$\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}$
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].
std::vector< Theorem > & getSkolemAxioms ()
void clearSkolemAxioms ()

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.

Detailed Description

Definition at line 48 of file common_theorem_producer.h.

Constructor & Destructor Documentation

CommonTheoremProducer::CommonTheoremProducer ( TheoremManager * tm )

Definition at line 48 of file common_theorem_producer.cpp.

virtual CVCL::CommonTheoremProducer::~CommonTheoremProducer ( ) [inline, virtual]

Definition at line 65 of file common_theorem_producer.h.

Member Function Documentation

Theorem CommonTheoremProducer::assumpRule ( const Expr & a,

int scope = -1

) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 55 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::newAssumption(), CVCL::TheoremProducer::newLabel(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::reflexivityRule ( const Expr & a ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 63 of file common_theorem_producer.cpp.
References CVCL::Type::getExpr(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Type::isNull(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newReflTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().
Referenced by rewriteIff(), rewriteUsingSymmetry(), symmetryRule(), transitivityRule(), and trueTheorem().

Theorem CommonTheoremProducer::rewriteReflexivity ( const Expr & t ) [virtual]

==> (a == a) IFF TRUE

Implements CVCL::CommonProofRules.
Definition at line 78 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::Expr::isEq(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 98 of file common_theorem_producer.cpp.
References CVCL::Theorem::getAssumptionsCopy(), CVCL::Type::getExpr(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), IF_DEBUG(), CVCL::Type::isBool(), CVCL::Theorem::isRewrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), reflexivityRule(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteUsingSymmetry ( const Expr & a1_eq_a2 ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 134 of file common_theorem_producer.cpp.
References CVCL::Expr::eqExpr(), CVCL::Type::getExpr(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Expr::isEq(), CVCL::Expr::isIff(), CVCL::Type::isNull(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), reflexivityRule(), CVCL::Expr::toString(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 159 of file common_theorem_producer.cpp.
References CVCL::Type::getExpr(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Type::isNull(), CVCL::Theorem::isNull(), CVCL::Theorem::isRewrite(), CVCL::merge(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), reflexivityRule(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CVCL::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 CVCL::CommonProofRules.

Theorem CVCL::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 $c_i=d_i$ for the changed kids.

Implements CVCL::CommonProofRules.

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 CVCL::CommonProofRules.
Definition at line 344 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::merge(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffTrue ( const Theorem & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 365 of file common_theorem_producer.cpp.
References CVCL::Assumptions::copy(), CVCL::TheoremProducer::d_em, CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::ExprManager::trueExpr(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffNotFalse ( const Theorem & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 378 of file common_theorem_producer.cpp.
References CVCL::Assumptions::copy(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::iffTrueElim ( const Theorem & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 390 of file common_theorem_producer.cpp.
References CVCL::Assumptions::copy(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Theorem::isRewrite(), CVCL::Expr::isTrue(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().
Referenced by trueTheorem().

Theorem CommonTheoremProducer::iffFalseElim ( const Theorem & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 406 of file common_theorem_producer.cpp.
References CVCL::Assumptions::copy(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::isFalse(), CVCL::Theorem::isRewrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 423 of file common_theorem_producer.cpp.
References CVCL::Assumptions::copy(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Theorem::isRewrite(), CVCL::Expr::negate(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::notNotElim ( const Theorem & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 439 of file common_theorem_producer.cpp.
References CVCL::Theorem::getAssumptionsCopy(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::isNot(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 453 of file common_theorem_producer.cpp.
References CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Theorem::isRewrite(), CVCL::merge(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 479 of file common_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::isImpl(), CVCL::merge(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::andElim ( const Theorem & e,

int i

) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 506 of file common_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Assumptions::copy(), CVCL::TheoremProducer::d_em, CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::int2string(), CVCL::Expr::isAnd(), CVCL::TheoremProducer::newPf(), CVCL::ExprManager::newRatExpr(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::andIntro ( const Theorem & e1,

const Theorem & e2

) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 524 of file common_theorem_producer.cpp.

Theorem CVCL::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 CVCL::CommonProofRules.

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 CVCL::CommonProofRules.
Definition at line 559 of file common_theorem_producer.cpp.
References CVCL::andExpr(), CVCL::Theorem::getAssumptionsRef(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::impExpr(), CVCL::int2string(), CVCL::Theorem::isAssump(), CVCL::Theorem::isNull(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 609 of file common_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Theorem::getAssumptionsCopy(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::isImpl(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::notToIff ( const Theorem & not_e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 626 of file common_theorem_producer.cpp.
References CVCL::Assumptions::copy(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::isNot(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteIff ( const Expr & e ) [virtual]

==> (e1 <=> e2) <=> [simplified expr]
Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc.
Implements CVCL::CommonProofRules.
Definition at line 644 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::FALSE, CVCL::ExprManager::falseExpr(), CVCL::Expr::getKind(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::NOT, reflexivityRule(), rewriteReflexivity(), rewriteUsingSymmetry(), CVCL::TRUE, and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteAnd ( const Expr & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 693 of file common_theorem_producer.cpp.
References CVCL::andExpr(), CVCL::ExprMap< Data >::begin(), CVCL::Expr::begin(), CVCL::ExprMap< Data >::count(), CVCL::TheoremProducer::d_em, CVCL::ExprMap< Data >::end(), CVCL::Expr::end(), CVCL::ExprManager::falseExpr(), CVCL::Expr::isAnd(), CVCL::Expr::isFalse(), CVCL::Expr::isTrue(), CVCL::Expr::negate(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::ExprMap< Data >::size(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().
Referenced by rewriteAnd().

Theorem CommonTheoremProducer::rewriteOr ( const Expr & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 733 of file common_theorem_producer.cpp.
References CVCL::ExprMap< Data >::begin(), CVCL::Expr::begin(), CVCL::ExprMap< Data >::count(), CVCL::TheoremProducer::d_em, CVCL::ExprMap< Data >::end(), CVCL::Expr::end(), CVCL::ExprManager::falseExpr(), CVCL::Expr::isFalse(), CVCL::Expr::isOr(), CVCL::Expr::isTrue(), CVCL::Expr::negate(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::orExpr(), CVCL::ExprMap< Data >::size(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().
Referenced by rewriteOr().

Theorem CommonTheoremProducer::rewriteNotTrue ( const Expr & e ) [virtual]

==> NOT TRUE IFF FALSE

Implements CVCL::CommonProofRules.
Definition at line 772 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Expr::isNot(), CVCL::Expr::isTrue(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotFalse ( const Expr & e ) [virtual]

==> NOT FALSE IFF TRUE

Implements CVCL::CommonProofRules.
Definition at line 785 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotNot ( const Expr & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 798 of file common_theorem_producer.cpp.
References CVCL::Expr::isNot(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotForall ( const Expr & forallExpr ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 811 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::EXISTS, CVCL::Expr::getBody(), CVCL::Expr::getVars(), CVCL::Expr::isForall(), CVCL::Expr::isNot(), CVCL::ExprManager::newClosureExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CommonTheoremProducer::rewriteNotExists ( const Expr & existsExpr ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 827 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::FORALL, CVCL::Expr::getBody(), CVCL::Expr::getVars(), CVCL::Expr::isExists(), CVCL::Expr::isNot(), CVCL::ExprManager::newClosureExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Expr CommonTheoremProducer::skolemize ( const Expr & e ) [virtual]

Implements CVCL::CommonProofRules.
Definition at line 842 of file common_theorem_producer.cpp.
References CVCL::Expr::getBody(), CVCL::Expr::getVars(), CVCL::Expr::setType(), CVCL::Expr::skolemExpr(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 856 of file common_theorem_producer.cpp.
References CVCL::Expr::iffExpr(), CVCL::Expr::isExists(), CVCL::TheoremProducer::newLabel(), CVCL::TheoremProducer::newRWTheorem(), skolemize(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().
Referenced by skolemize().

Theorem CommonTheoremProducer::skolemizeRewriteVar ( const Expr & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 874 of file common_theorem_producer.cpp.
References CVCL::Expr::getBody(), CVCL::Expr::getOp(), CVCL::Expr::getVars(), CVCL::Expr::iffExpr(), CVCL::Expr::isEq(), CVCL::Expr::isExists(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newLabel(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::setType(), CVCL::Expr::skolemExpr(), CVCL::Expr::subExprOf(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().
Referenced by varIntroSkolem().

Theorem CommonTheoremProducer::varIntroRule ( const Expr & e ) [virtual]

|- EXISTS x. e = x

Implements CVCL::CommonProofRules.
Definition at line 912 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::Expr::eqExpr(), CVCL::EXISTS, CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::ExprManager::newBoundVarExpr(), CVCL::ExprManager::newClosureExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 933 of file common_theorem_producer.cpp.
References d_skolem_axioms, d_skolemized_thms, CVCL::CDMap< Key, Data, HashFcn >::end(), CVCL::CDMap< Key, Data, HashFcn >::find(), CVCL::Theorem::getExpr(), CVCL::Expr::getVars(), iffMP(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::Expr::isExists(), CVCL::Expr::setType(), CVCL::Expr::skolemExpr(), skolemizeRewrite(), and CVCL::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 CVCL::CommonProofRules.
Definition at line 959 of file common_theorem_producer.cpp.
References d_skolem_axioms, d_skolemized_thms, d_skolemVars, CVCL::CDMap< Key, Data, HashFcn >::end(), CVCL::CDMap< Key, Data, HashFcn >::find(), CVCL::Theorem::getExpr(), CVCL::Expr::getVars(), iffMP(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::Expr::isExists(), skolemizeRewriteVar(), CVCL::Expr::toString(), and varIntroRule().

Theorem CommonTheoremProducer::trueTheorem ( ) [virtual]

==> TRUE

Implements CVCL::CommonProofRules.
Definition at line 989 of file common_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, iffTrueElim(), reflexivityRule(), and CVCL::ExprManager::trueExpr().

Theorem CommonTheoremProducer::rewriteAnd ( const Theorem & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 995 of file common_theorem_producer.cpp.
References CVCL::Theorem::getExpr(), iffMP(), and rewriteAnd().

Theorem CommonTheoremProducer::rewriteOr ( const Theorem & e ) [virtual]

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

Implements CVCL::CommonProofRules.
Definition at line 1001 of file common_theorem_producer.cpp.
References CVCL::Theorem::getExpr(), iffMP(), and rewriteOr().

std::vector<Theorem>& CVCL::CommonTheoremProducer::getSkolemAxioms ( ) [inline, virtual]

Implements CVCL::CommonProofRules.
Definition at line 112 of file common_theorem_producer.h.
References d_skolem_axioms.

void CVCL::CommonTheoremProducer::clearSkolemAxioms ( ) [inline, virtual]

Implements CVCL::CommonProofRules.
Definition at line 113 of file common_theorem_producer.h.
References d_skolem_axioms.

Member Data Documentation

std::vector<Theorem> CVCL::CommonTheoremProducer::d_skolem_axioms [private]

Definition at line 54 of file common_theorem_producer.h.
Referenced by clearSkolemAxioms(), getSkolemAxioms(), skolemize(), and varIntroSkolem().

CDMap<Expr, Theorem> CVCL::CommonTheoremProducer::d_skolemized_thms [private]

Definition at line 58 of file common_theorem_producer.h.
Referenced by skolemize(), and varIntroSkolem().

CDMap<Expr, Theorem> CVCL::CommonTheoremProducer::d_skolemVars [private]

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

Definition at line 61 of file common_theorem_producer.h.
Referenced by varIntroSkolem().

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

Generated on Thu Apr 13 16:57:45 2006 for CVC Lite by

1.4.4