CVCL::CoreTheoremProducer Class Reference

#include <core_theorem_producer.h>

Inheritance diagram for CVCL::CoreTheoremProducer:

[legend]Collaboration diagram for CVCL::CoreTheoremProducer:

[legend]List of all members.

Public Member Functions

CoreTheoremProducer (TheoremManager *tm, TheoryCore *core)
virtual ~CoreTheoremProducer ()
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 typePred (const Expr &e)
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
Theorem rewriteLetDecl (const Expr &e)
Replace LETDECL with its definition.
Theorem rewriteConstDef (const Expr &e)
Replace CONSTDEF with its definition.
Theorem rewriteNotAnd (const Expr &e)
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
Theorem rewriteNotOr (const Expr &e)
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
Theorem rewriteNotIff (const Expr &e)
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
Theorem rewriteNotIte (const Expr &e)
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
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 rewriteIteThen (const Expr &e, const Theorem &thenThm)
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
Theorem rewriteIteElse (const Expr &e, const Theorem &elseThm)
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
Theorem rewriteIteBool (const Expr &c, const Expr &e1, const Expr &e2)
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
Theorem orDistributivityRule (const Expr &e)
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
Theorem andDistributivityRule (const Expr &e)
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
Theorem rewriteImplies (const Expr &e)
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
Theorem NotToIte (const Expr &not_e)
==> NOT(e) == ITE(e, FALSE, TRUE)
Theorem OrToIte (const Expr &e)
==> Or(e) == ITE(e[1], TRUE, e[0])
Theorem AndToIte (const Expr &e)
==> And(e) == ITE(e[1], e[0], FALSE)
Theorem IffToIte (const Expr &e)
==> IFF(a,b) == ITE(a, b, !b)
Theorem ImpToIte (const Expr &e)
==> IMPLIES(a,b) == ITE(a, b, TRUE)
Theorem rewriteIteToNot (const Expr &e)
==> ITE(e, FALSE, TRUE) IFF NOT(e)
Theorem rewriteIteToOr (const Expr &e)
==> ITE(a, TRUE, b) IFF OR(a, b)
Theorem rewriteIteToAnd (const Expr &e)
==> ITE(a, b, FALSE) IFF AND(a, b)
Theorem rewriteIteToIff (const Expr &e)
==> ITE(a, b, !b) IFF IFF(a, b)
Theorem rewriteIteToImp (const Expr &e)
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
Theorem rewriteIteCond (const Expr &e)
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
Theorem ifLiftUnaryRule (const Expr &e)
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
Theorem iffOrDistrib (const Expr &iff)
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
Theorem iffAndDistrib (const Expr &iff)
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
Theorem rewriteAndSubterms (const Expr &e, int idx)
(a & b) <=> a & b[a/true]; takes the index of a
Theorem rewriteOrSubterms (const Expr &e, int idx)
(a | b) <=> a | b[a/false]; takes the index of a

Private Attributes

TheoryCore * d_core
pointer to theory core

Detailed Description

Definition at line 48 of file core_theorem_producer.h.

Constructor & Destructor Documentation

CVCL::CoreTheoremProducer::CoreTheoremProducer ( TheoremManager * tm,

TheoryCore * core

) [inline]

Definition at line 54 of file core_theorem_producer.h.

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

Definition at line 56 of file core_theorem_producer.h.

Member Function Documentation

Theorem3 CoreTheoremProducer::queryTCC ( const Theorem & phi,

const Theorem & D_phi

) [virtual]

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}$
.

Implements CVCL::CoreProofRules.
Definition at line 66 of file core_theorem_producer.cpp.
References d_core, CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Theory::getTCC(), CVCL::merge(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem3(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem3 CVCL::CoreTheoremProducer::implIntro3 ( const Theorem3 & phi,

const std::vector< Expr > & assump,

const std::vector< Theorem > & tccs

) [virtual]

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}$

Parameters:

phi is the formula $\phi$

assump is the vector of assumptions $\alpha_1\ldots\alpha_n$

tccs is the vector of TCCs for assumptions $D_{\alpha_1}\ldots D_{\alpha_n}$

Implements CVCL::CoreProofRules.

Theorem CoreTheoremProducer::typePred ( const Expr & e ) [virtual]

e: T ==> |- typePred_T(e) [deriving the type predicate of e]

Implements CVCL::CoreProofRules.
Definition at line 167 of file core_theorem_producer.cpp.
References d_core, CVCL::Type::getExpr(), CVCL::Expr::getType(), CVCL::Theory::getTypePred(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteLetDecl ( const Expr & e ) [virtual]

Replace LETDECL with its definition.
Used only in TheoryCore
Implements CVCL::CoreProofRules.
Definition at line 182 of file core_theorem_producer.cpp.
References CVCL::Expr::getKind(), CVCL::LETDECL, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteConstDef ( const Expr & e ) [virtual]

Replace CONSTDEF with its definition.
Used only in TheoryCore
Implements CVCL::CoreProofRules.
Definition at line 194 of file core_theorem_producer.cpp.
References CVCL::CONSTDEF, CVCL::Expr::getKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteNotAnd ( const Expr & e ) [virtual]

==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)

Implements CVCL::CoreProofRules.
Definition at line 207 of file core_theorem_producer.cpp.
References CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::isAnd(), CVCL::Expr::isNot(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::orExpr(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteNotOr ( const Expr & e ) [virtual]

==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)

Implements CVCL::CoreProofRules.
Definition at line 226 of file core_theorem_producer.cpp.
References CVCL::andExpr(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::isNot(), CVCL::Expr::isOr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteNotIff ( const Expr & e ) [virtual]

==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)

Implements CVCL::CoreProofRules.
Definition at line 244 of file core_theorem_producer.cpp.
References CVCL::Expr::isIff(), CVCL::Expr::isNot(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteNotIte ( const Expr & e ) [virtual]

==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)

Implements CVCL::CoreProofRules.
Definition at line 258 of file core_theorem_producer.cpp.
References CVCL::Expr::isITE(), CVCL::Expr::isNot(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteTrue ( const Expr & e ) [virtual]

==> ITE(TRUE, e1, e2) == e1

Implements CVCL::CoreProofRules.
Definition at line 272 of file core_theorem_producer.cpp.
References CVCL::Type::getExpr(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isITE(), CVCL::Type::isNull(), CVCL::Expr::isTrue(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteFalse ( const Expr & e ) [virtual]

==> ITE(FALSE, e1, e2) == e2

Implements CVCL::CoreProofRules.
Definition at line 295 of file core_theorem_producer.cpp.
References CVCL::Type::getExpr(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isFalse(), CVCL::Expr::isITE(), CVCL::Type::isNull(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteSame ( const Expr & e ) [virtual]

==> ITE(c, e, e) == e

Implements CVCL::CoreProofRules.
Definition at line 317 of file core_theorem_producer.cpp.
References CVCL::Type::getExpr(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isITE(), CVCL::Type::isNull(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteThen ( const Expr & e,

const Theorem & thenThm

) [virtual]

a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)

Implements CVCL::CoreProofRules.
Definition at line 339 of file core_theorem_producer.cpp.
References CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isITE(), CVCL::Type::isNull(), CVCL::Theorem::isRewrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteElse ( const Expr & e,

const Theorem & elseThm

) [virtual]

!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)

Implements CVCL::CoreProofRules.
Definition at line 367 of file core_theorem_producer.cpp.
References CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isITE(), CVCL::Type::isNull(), CVCL::Theorem::isRewrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteBool ( const Expr & c,

const Expr & e1,

const Expr & e2

) [virtual]

==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)

Implements CVCL::CoreProofRules.
Definition at line 395 of file core_theorem_producer.cpp.
References CVCL::Expr::andExpr(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::iteExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::orExpr(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::orDistributivityRule ( const Expr & e ) [virtual]

|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)

Implements CVCL::CoreProofRules.
Definition at line 412 of file core_theorem_producer.cpp.
References CVCL::Expr::andExpr(), CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::isAnd(), CVCL::Expr::isOr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::orExpr(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::andDistributivityRule ( const Expr & e ) [virtual]

|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)

Implements CVCL::CoreProofRules.
Definition at line 456 of file core_theorem_producer.cpp.
References CVCL::andExpr(), CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::isAnd(), CVCL::Expr::isOr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::orExpr(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteImplies ( const Expr & e ) [virtual]

==> IMPLIES(e1,e2) IFF OR(!e1, e2)

Implements CVCL::CoreProofRules.
Definition at line 497 of file core_theorem_producer.cpp.
References CVCL::Expr::isImpl(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::NotToIte ( const Expr & not_e ) [virtual]

==> NOT(e) == ITE(e, FALSE, TRUE)

Implements CVCL::CoreProofRules.
Definition at line 510 of file core_theorem_producer.cpp.
References d_core, CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theory::getCommonRules(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::Expr::isTrue(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::CommonProofRules::rewriteNotFalse(), CVCL::CommonProofRules::rewriteNotTrue(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::OrToIte ( const Expr & e ) [virtual]

==> Or(e) == ITE(e[1], TRUE, e[0])

Implements CVCL::CoreProofRules.
Definition at line 528 of file core_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Expr::getKids(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::Type::isNull(), CVCL::Expr::isOr(), CVCL::Expr::iteExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::AndToIte ( const Expr & e ) [virtual]

==> And(e) == ITE(e[1], e[0], FALSE)

Implements CVCL::CoreProofRules.
Definition at line 567 of file core_theorem_producer.cpp.
References CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Expr::getKids(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::Expr::isAnd(), CVCL::Type::isNull(), CVCL::Expr::iteExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::IffToIte ( const Expr & e ) [virtual]

==> IFF(a,b) == ITE(a, b, !b)

Implements CVCL::CoreProofRules.
Definition at line 608 of file core_theorem_producer.cpp.
References d_core, CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theory::getCommonRules(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::CommonProofRules::reflexivityRule(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::ImpToIte ( const Expr & e ) [virtual]

==> IMPLIES(a,b) == ITE(a, b, TRUE)

Implements CVCL::CoreProofRules.
Definition at line 625 of file core_theorem_producer.cpp.
References d_core, CVCL::TheoremProducer::d_em, CVCL::Theory::getCommonRules(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isImpl(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::CommonProofRules::reflexivityRule(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToNot ( const Expr & e ) [virtual]

==> ITE(e, FALSE, TRUE) IFF NOT(e)

Implements CVCL::CoreProofRules.
Definition at line 642 of file core_theorem_producer.cpp.
References CVCL::Expr::isFalse(), CVCL::Expr::isITE(), CVCL::Expr::isTrue(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToOr ( const Expr & e ) [virtual]

==> ITE(a, TRUE, b) IFF OR(a, b)

Implements CVCL::CoreProofRules.
Definition at line 655 of file core_theorem_producer.cpp.
References CVCL::Expr::isITE(), CVCL::Expr::isTrue(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToAnd ( const Expr & e ) [virtual]

==> ITE(a, b, FALSE) IFF AND(a, b)

Implements CVCL::CoreProofRules.
Definition at line 668 of file core_theorem_producer.cpp.
References CVCL::Expr::isFalse(), CVCL::Expr::isITE(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToIff ( const Expr & e ) [virtual]

==> ITE(a, b, !b) IFF IFF(a, b)

Implements CVCL::CoreProofRules.
Definition at line 681 of file core_theorem_producer.cpp.
References CVCL::Expr::isITE(), CVCL::Expr::negate(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToImp ( const Expr & e ) [virtual]

==> ITE(a, b, TRUE) IFF IMPLIES(a, b)

Implements CVCL::CoreProofRules.
Definition at line 694 of file core_theorem_producer.cpp.
References CVCL::Expr::isITE(), CVCL::Expr::isTrue(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteCond ( const Expr & e ) [virtual]

==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))

Implements CVCL::CoreProofRules.
Definition at line 708 of file core_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Expr::isITE(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::ifLiftUnaryRule ( const Expr & e ) [virtual]

|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))

Implements CVCL::CoreProofRules.
Definition at line 775 of file core_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::getOp(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isITE(), CVCL::Expr::iteExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::iffOrDistrib ( const Expr & iff ) [virtual]

((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'

Implements CVCL::CoreProofRules.
Definition at line 728 of file core_theorem_producer.cpp.
References CVCL::Expr::arity(), b, CVCL::Expr::iffExpr(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::iffAndDistrib ( const Expr & iff ) [virtual]

((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'

Implements CVCL::CoreProofRules.
Definition at line 751 of file core_theorem_producer.cpp.
References CVCL::Expr::arity(), b, CVCL::Expr::iffExpr(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteAndSubterms ( const Expr & e,

int idx

) [virtual]

(a & b) <=> a & b[a/true]; takes the index of a
and rewrites all the other conjuncts.
Implements CVCL::CoreProofRules.
Definition at line 808 of file core_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::TheoremProducer::d_em, CVCL::Expr::getOp(), CVCL::ExprHashMap< Data >::insert(), CVCL::int2string(), CVCL::Expr::isAnd(), CVCL::TheoremProducer::newPf(), CVCL::ExprManager::newRatExpr(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::ExprManager::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteOrSubterms ( const Expr & e,

int idx

) [virtual]

(a | b) <=> a | b[a/false]; takes the index of a
and rewrites all the other disjuncts.
Implements CVCL::CoreProofRules.
Definition at line 835 of file core_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Expr::getOp(), CVCL::ExprHashMap< Data >::insert(), CVCL::int2string(), CVCL::Expr::isOr(), CVCL::TheoremProducer::newPf(), CVCL::ExprManager::newRatExpr(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Member Data Documentation

TheoryCore* CVCL::CoreTheoremProducer::d_core [private]

pointer to theory core

Definition at line 51 of file core_theorem_producer.h.
Referenced by IffToIte(), ImpToIte(), NotToIte(), queryTCC(), and typePred().

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

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

1.4.4