CVCL::CommonProofRules Class Reference

#include <common_proof_rules.h>

Inheritance diagram for CVCL::CommonProofRules:

[legend]List of all members.

Public Member Functions

virtual ~CommonProofRules ()
Destructor.
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 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 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 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 notToIff (const Theorem &not_e)=0
$\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}$
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

Detailed Description

Definition at line 54 of file common_proof_rules.h.

Constructor & Destructor Documentation

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

Destructor.

Definition at line 57 of file common_proof_rules.h.

Member Function Documentation

virtual Theorem CVCL::CommonProofRules::assumpRule ( const Expr & a,

int scope = -1

) [pure virtual]

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchSat::assertLit(), CVCL::SearchSat::check(), CVCL::ExprTransform::ite_simplify(), CVCL::SearchImplBase::newIntAssumption(), CVCL::SearchSat::newUserAssumption(), and CVCL::SearchImplBase::newUserAssumption().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::CoreTheoremProducer::IffToIte(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::ExprTransform::ite_convert(), CVCL::ExprTransform::preprocess(), CVCL::ExprTransform::pushNegation(), CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), CVCL::Theory::reflexivityRule(), CVCL::SearchImplBase::replaceITE(), SAT::CNF_Manager::replaceITErec(), TheoryCore::rewrite(), and TheoryCore::setupTerm().

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

==> (a == a) IFF TRUE

Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::rewriteLitCore().

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

$\frac{a_1=a_2}{a_2=a_1}$
(same for IFF)

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::applyCNFRules(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchImplBase::enqueueCNFrec(), SAT::CNF_Manager::replaceITErec(), and CVCL::Theory::symmetryRule().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::assertFormula(), and TheoryCore::rewriteLitCore().

virtual Theorem CVCL::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 CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::applyCNFRules(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchImplBase::findInCNFCache(), CVCL::ExprTransform::ite_convert(), CVCL::ExprTransform::ite_simplify(), CVCL::ExprTransform::preprocess(), CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), CVCL::SearchImplBase::replaceITE(), and CVCL::Theory::transitivityRule().

virtual Theorem CVCL::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 CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::applyCNFRules(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::ExprTransform::ite_convert(), CVCL::ExprTransform::ite_simplify(), CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), SAT::CNF_Manager::replaceITErec(), CVCL::Theory::simplifyOp(), CVCL::Theory::substitutivityRule(), and CVCL::Theory::updateHelper().

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

Implemented in CVCL::CommonTheoremProducer.

virtual Theorem CVCL::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 CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchEngineFast::addLiteralFact(), TheoryCore::assertFormula(), TheoryCore::processEquality(), and CVCL::SearchEngineFast::recordFact().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::assertFormula(), CVCL::ExprTransform::ite_simplify(), CVCL::TheoryArith::rewrite(), and TheoryCore::simplifyFullRec().

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

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

Implemented in CVCL::CommonTheoremProducer.

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::processUpdates(), TheoryCore::registerAtom(), CVCL::SearchEngineFast::split(), and CVCL::TheoryUF::update().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::assertFormula(), TheoryCore::processEquality(), TheoryCore::processUpdates(), TheoryCore::registerAtom(), and CVCL::SearchEngineFast::split().

virtual Theorem CVCL::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 CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchImplBase::findInCNFCache(), and TheoryCore::rewriteLiteral().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::enqueueCNFrec(), and CVCL::SearchEngineFast::split().

virtual Theorem CVCL::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 CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchSimple::checkValidRec(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchEngineFast::fixConflict(), CVCL::Theory::iffMP(), CVCL::ExprTransform::preprocess(), CVCL::SearchImplBase::replaceITE(), and SAT::CNF_Manager::replaceITErec().

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

virtual Theorem CVCL::CommonProofRules::andElim ( const Theorem & e,

int i

) [pure virtual]

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchImplBase::applyCNFRules(), TheoryCore::assertFactCore(), CVCL::SearchImplBase::enqueueCNFrec(), TheoryCore::processEquality(), and CVCL::TheoryArith::processIntEq().

virtual Theorem CVCL::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 CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchSimple::addNonLiteralFact(), CVCL::TheoryArith::processSimpleIntEq(), and TheoryCore::subtypePredicate().

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

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

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

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::assertFormula(), and TheoryCore::checkSat().

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

==> (e1 <=> e2) <=> [simplified expr]
Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc.
Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::rewrite(), and CVCL::TheoryBitvector::rewriteBoolean().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::Theory::computeTCC(), CVCL::Theory::rewriteAnd(), and TheoryCore::subtypePredicate().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchEngineFast::fixConflict(), and CVCL::Theory::rewriteOr().

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

==> NOT TRUE IFF FALSE

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::CoreTheoremProducer::NotToIte(), CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), CVCL::TheoryBitvector::rewriteBoolean(), and TheoryCore::rewriteLitCore().

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

==> NOT FALSE IFF TRUE

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::CoreTheoremProducer::NotToIte(), CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), CVCL::TheoryBitvector::rewriteBoolean(), and TheoryCore::rewriteLitCore().

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

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::findInCNFCache(), CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), CVCL::TheoryBitvector::rewriteBoolean(), and TheoryCore::rewriteLitCore().

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

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

Implemented in CVCL::CommonTheoremProducer.

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

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

Implemented in CVCL::CommonTheoremProducer.

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::SearchEngineFast::bcp(), TheoryCore::processEquality(), and CVCL::TheoryArith::processSimpleIntEq().

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

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

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

Implemented in CVCL::CommonTheoremProducer.

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

|- EXISTS x. e = x

Implemented in CVCL::CommonTheoremProducer.

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

virtual Theorem CVCL::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 CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::applyCNFRules(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::TheoryArray::renameExpr(), CVCL::SearchImplBase::replaceITE(), and SAT::CNF_Manager::replaceITErec().

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

==> TRUE

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchSat::check(), and CVCL::SearchSimple::SearchSimple().

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

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

Implemented in CVCL::CommonTheoremProducer.

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

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

Implemented in CVCL::CommonTheoremProducer.

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::processResult().

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

Implemented in CVCL::CommonTheoremProducer.
Referenced by CVCL::SearchImplBase::checkValid().

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

common_proof_rules.h

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

1.4.4