CVC3::CommonTheoremProducer Class Reference

#include <common_theorem_producer.h>

Inheritance diagram for CVC3::CommonTheoremProducer:

Inheritance graph
[legend]
Collaboration diagram for CVC3::CommonTheoremProducer:

Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


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 (  )  [inline, virtual]

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:
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 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(), CVC3::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:
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 CVC3::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 (  )  [inline, virtual]

Implements CVC3::CommonProofRules.

Definition at line 126 of file common_theorem_producer.h.

References d_skolem_axioms.

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

Implements CVC3::CommonProofRules.

Definition at line 127 of file common_theorem_producer.h.

References d_skolem_axioms.


Member Data Documentation

Definition at line 50 of file common_theorem_producer.h.

Referenced by skolemize(), and varIntroSkolem().

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:

Generated on Thu Oct 15 22:25:24 2009 for CVC3 by  doxygen 1.5.8