CVC3
Public Member Functions | Private Member Functions | Private Attributes | List of all members
CVC3::CommonTheoremProducer Class Reference

#include <common_theorem_producer.h>

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

Collaboration diagram for CVC3::CommonTheoremProducer:
Collaboration graph

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< Theoremd_skolem_axioms
 
CDMap< Expr, Theoremd_skolemized_thms
 
CDMap< Expr, Theoremd_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
TheoremManagerd_tm
 
ExprManagerd_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
Theorem3 CommonTheoremProducer::queryTCC ( const Theorem phi,
const Theorem D_phi 
)
virtual
Theorem3 CommonTheoremProducer::implIntro3 ( const Theorem3 phi,
const std::vector< Expr > &  assump,
const std::vector< Theorem > &  tccs 
)
virtual
Theorem CommonTheoremProducer::assumpRule ( const Expr a,
int  scope = -1 
)
virtual
Theorem CommonTheoremProducer::reflexivityRule ( const Expr a)
virtual
Theorem CommonTheoremProducer::rewriteReflexivity ( const Expr a_eq_a)
virtual
Theorem CommonTheoremProducer::symmetryRule ( const Theorem a1_eq_a2)
virtual
Theorem CommonTheoremProducer::rewriteUsingSymmetry ( const Expr a1_eq_a2)
virtual
Theorem CommonTheoremProducer::transitivityRule ( const Theorem a1_eq_a2,
const Theorem a2_eq_a3 
)
virtual
Theorem CommonTheoremProducer::substitutivityRule ( const Expr e,
const Theorem thm 
)
virtual
Theorem CommonTheoremProducer::substitutivityRule ( const Expr e,
const Theorem thm1,
const Theorem thm2 
)
virtual
Theorem CommonTheoremProducer::substitutivityRule ( const Op op,
const std::vector< Theorem > &  thms 
)
virtual
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
eis the original expression $op(c_1,\ldots,c_n)$.
changedis the vector of indices of changed kids
thmsare the theorems $c_i=d_i$ 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
Theorem CommonTheoremProducer::excludedMiddle ( const Expr e)
virtual
Theorem CommonTheoremProducer::iffTrue ( const Theorem e)
virtual
Theorem CommonTheoremProducer::iffNotFalse ( const Theorem e)
virtual
Theorem CommonTheoremProducer::iffTrueElim ( const Theorem e)
virtual
Theorem CommonTheoremProducer::iffFalseElim ( const Theorem e)
virtual
Theorem CommonTheoremProducer::iffContrapositive ( const Theorem thm)
virtual
Theorem CommonTheoremProducer::notNotElim ( const Theorem not_not_e)
virtual
Theorem CommonTheoremProducer::iffMP ( const Theorem e1,
const Theorem e1_iff_e2 
)
virtual
Theorem CommonTheoremProducer::implMP ( const Theorem e1,
const Theorem e1_impl_e2 
)
virtual
Theorem CommonTheoremProducer::andElim ( const Theorem e,
int  i 
)
virtual
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
Theorem CommonTheoremProducer::implIntro ( const Theorem phi,
const std::vector< Expr > &  assump 
)
virtual
Theorem CommonTheoremProducer::implContrapositive ( const Theorem thm)
virtual
Theorem CommonTheoremProducer::rewriteIteTrue ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteIteFalse ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteIteSame ( const Expr e)
virtual
Theorem CommonTheoremProducer::notToIff ( const Theorem not_e)
virtual
Theorem CommonTheoremProducer::xorToIff ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteIff ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteAnd ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteOr ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteNotTrue ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteNotFalse ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteNotNot ( const Expr e)
virtual
Theorem CommonTheoremProducer::rewriteNotForall ( const Expr forallExpr)
virtual
Theorem CommonTheoremProducer::rewriteNotExists ( const Expr existsExpr)
virtual
Expr CommonTheoremProducer::skolemize ( const Expr e)
virtual
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
Theorem CommonTheoremProducer::varIntroRule ( const Expr e)
virtual
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
thmis 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
Theorem CommonTheoremProducer::trueTheorem ( )
virtual
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
Theorem CommonTheoremProducer::liftOneITE ( const Expr e)
virtual
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
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: