CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
CVC3::CommonTheoremProducer Class Reference

#include <common_theorem_producer.h>

Inheritance diagram for CVC3::CommonTheoremProducer:
CVC3::CommonProofRules CVC3::TheoremProducer

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

Definition at line 40 of file common_theorem_producer.cpp.

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::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::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::notToIff ( const Theorem not_e) [virtual]
Theorem CommonTheoremProducer::xorToIff ( const Expr e) [virtual]
Theorem CommonTheoremProducer::rewriteOr ( 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]

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::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.

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().

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]
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.

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: