CVCL::CoreProofRules Class Reference

#include <core_proof_rules.h>

Inheritance diagram for CVCL::CoreProofRules:

[legend]List of all members.

Public Member Functions

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

Detailed Description

Definition at line 42 of file core_proof_rules.h.

Constructor & Destructor Documentation

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

Destructor.

Definition at line 45 of file core_proof_rules.h.

Member Function Documentation

virtual Theorem3 CVCL::CoreProofRules::queryTCC ( const Theorem & phi,

const Theorem & D_phi

) [pure 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}$
.

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::queryTCC().

virtual Theorem3 CVCL::CoreProofRules::implIntro3 ( const Theorem3 & phi,

const std::vector< Expr > & assump,

const std::vector< Theorem > & tccs

) [pure 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}$

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::implIntro3().

virtual Theorem CVCL::CoreProofRules::typePred ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::setupTerm(), TheoryCore::subtypePredicate(), and TheoryCore::typePred().

virtual Theorem CVCL::CoreProofRules::rewriteLetDecl ( const Expr & e ) [pure virtual]

Replace LETDECL with its definition.
Used only in TheoryCore
Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), and TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteConstDef ( const Expr & e ) [pure virtual]

Replace CONSTDEF with its definition.
Used only in TheoryCore
Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), and TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteNotAnd ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::pushNegation1(), and CVCL::ExprTransform::pushNegationRec().

virtual Theorem CVCL::CoreProofRules::rewriteNotOr ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::pushNegation1(), and CVCL::ExprTransform::pushNegationRec().

virtual Theorem CVCL::CoreProofRules::rewriteNotIff ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.

virtual Theorem CVCL::CoreProofRules::rewriteNotIte ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::pushNegation1(), and CVCL::ExprTransform::pushNegationRec().

virtual Theorem CVCL::CoreProofRules::rewriteIteTrue ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::ite_simplify(), TheoryCore::rewrite(), and TheoryCore::rewriteIte().

virtual Theorem CVCL::CoreProofRules::rewriteIteFalse ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::ite_simplify(), TheoryCore::rewrite(), and TheoryCore::rewriteIte().

virtual Theorem CVCL::CoreProofRules::rewriteIteSame ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite(), TheoryCore::rewriteIte(), and TheoryCore::simplifyOp().

virtual Theorem CVCL::CoreProofRules::rewriteIteThen ( const Expr & e,

const Theorem & thenThm

) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.

virtual Theorem CVCL::CoreProofRules::rewriteIteElse ( const Expr & e,

const Theorem & elseThm

) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.

virtual Theorem CVCL::CoreProofRules::rewriteIteBool ( const Expr & c,

const Expr & e1,

const Expr & e2

) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.

virtual Theorem CVCL::CoreProofRules::orDistributivityRule ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::andDistributivityRule ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteImplies ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), TheoryCore::rewrite(), and TheoryCore::simplifyOp().

virtual Theorem CVCL::CoreProofRules::NotToIte ( const Expr & not_e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::ite_convert().

virtual Theorem CVCL::CoreProofRules::OrToIte ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::ite_convert().

virtual Theorem CVCL::CoreProofRules::AndToIte ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::ite_convert().

virtual Theorem CVCL::CoreProofRules::IffToIte ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::ite_convert().

virtual Theorem CVCL::CoreProofRules::ImpToIte ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by CVCL::ExprTransform::ite_convert().

virtual Theorem CVCL::CoreProofRules::rewriteIteToNot ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteIteToOr ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteIteToAnd ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteIteToIff ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteIteToImp ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteIteCond ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::ifLiftUnaryRule ( const Expr & e ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::simplifyOp().

virtual Theorem CVCL::CoreProofRules::iffOrDistrib ( const Expr & iff ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::iffAndDistrib ( const Expr & iff ) [pure virtual]

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

Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteAndSubterms ( const Expr & e,

int idx

) [pure virtual]

(a & b) <=> a & b[a/true]; takes the index of a
and rewrites all the other conjuncts.
Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

virtual Theorem CVCL::CoreProofRules::rewriteOrSubterms ( const Expr & e,

int idx

) [pure virtual]

(a | b) <=> a | b[a/false]; takes the index of a
and rewrites all the other disjuncts.
Implemented in CVCL::CoreTheoremProducer.
Referenced by TheoryCore::rewrite().

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

core_proof_rules.h

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

1.4.4