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

#include <core_theorem_producer.h>

Inherits CVC3::CoreProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::CoreTheoremProducer:
Collaboration graph

Public Member Functions

 CoreTheoremProducer (TheoremManager *tm, TheoryCore *core)
 
virtual ~CoreTheoremProducer ()
 
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 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 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 rewriteDistinct (const Expr &e)
 ==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
 
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
 
Theorem dummyTheorem (const Expr &e)
 Temporary cheat for building theorems.
 
- Public Member Functions inherited from CVC3::CoreProofRules
virtual ~CoreProofRules ()
 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 Attributes

TheoryCored_core
 pointer to theory core
 

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 core_theorem_producer.h.

Constructor & Destructor Documentation

CVC3::CoreTheoremProducer::CoreTheoremProducer ( TheoremManager tm,
TheoryCore core 
)
inline

Definition at line 46 of file core_theorem_producer.h.

virtual CVC3::CoreTheoremProducer::~CoreTheoremProducer ( )
inlinevirtual

Definition at line 48 of file core_theorem_producer.h.

Member Function Documentation

Theorem CoreTheoremProducer::typePred ( const Expr e)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 52 of file core_theorem_producer.cpp.

References CVC3::Assumptions::emptyAssump(), and CVC3::Expr::getType().

Theorem CoreTheoremProducer::rewriteLetDecl ( const Expr e)
virtual

Replace LETDECL with its definition.

Used only in TheoryCore

Implements CVC3::CoreProofRules.

Definition at line 64 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), LETDECL, and CVC3::Expr::toString().

Theorem CoreTheoremProducer::rewriteNotAnd ( const Expr e)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 75 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isNot(), CVC3::orExpr(), and CVC3::Expr::toString().

Theorem CoreTheoremProducer::rewriteNotOr ( const Expr e)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 93 of file core_theorem_producer.cpp.

References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), and CVC3::Expr::toString().

Theorem CoreTheoremProducer::rewriteNotIff ( const Expr e)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 110 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isIff(), and CVC3::Expr::isNot().

Theorem CoreTheoremProducer::rewriteNotIte ( const Expr e)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 123 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), and CVC3::Expr::isNot().

Theorem CoreTheoremProducer::rewriteIteThen ( const Expr e,
const Theorem thenThm 
)
virtual
Theorem CoreTheoremProducer::rewriteIteElse ( const Expr e,
const Theorem elseThm 
)
virtual
Theorem CoreTheoremProducer::rewriteIteBool ( const Expr c,
const Expr e1,
const Expr e2 
)
virtual
Theorem CoreTheoremProducer::orDistributivityRule ( const Expr e)
virtual
Theorem CoreTheoremProducer::andDistributivityRule ( const Expr e)
virtual
Theorem CoreTheoremProducer::rewriteImplies ( const Expr e)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 285 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), and CVC3::Expr::isImpl().

Theorem CoreTheoremProducer::rewriteDistinct ( const Expr e)
virtual
Theorem CoreTheoremProducer::NotToIte ( const Expr not_e)
virtual
Theorem CoreTheoremProducer::OrToIte ( const Expr e)
virtual
Theorem CoreTheoremProducer::AndToIte ( const Expr e)
virtual
Theorem CoreTheoremProducer::IffToIte ( const Expr e)
virtual
Theorem CoreTheoremProducer::ImpToIte ( const Expr e)
virtual
Theorem CoreTheoremProducer::rewriteIteToNot ( const Expr e)
virtual
Theorem CoreTheoremProducer::rewriteIteToOr ( const Expr e)
virtual
Theorem CoreTheoremProducer::rewriteIteToAnd ( const Expr e)
virtual
Theorem CoreTheoremProducer::rewriteIteToIff ( const Expr e)
virtual
Theorem CoreTheoremProducer::rewriteIteToImp ( const Expr e)
virtual
Theorem CoreTheoremProducer::rewriteIteCond ( const Expr e)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 516 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), and CVC3::Expr::toString().

Theorem CoreTheoremProducer::ifLiftUnaryRule ( const Expr e)
virtual
Theorem CoreTheoremProducer::iffOrDistrib ( const Expr iff)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 543 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isIff(), and CVC3::Expr::toString().

Theorem CoreTheoremProducer::iffAndDistrib ( const Expr iff)
virtual

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

Implements CVC3::CoreProofRules.

Definition at line 565 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isIff(), and CVC3::Expr::toString().

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

Definition at line 621 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::ExprHashMap< Data >::insert(), CVC3::int2string(), CVC3::Expr::isAnd(), and CVC3::Expr::toString().

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

Definition at line 647 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::ExprHashMap< Data >::insert(), CVC3::int2string(), CVC3::Expr::isOr(), and CVC3::Expr::toString().

Theorem CoreTheoremProducer::dummyTheorem ( const Expr e)
virtual

Temporary cheat for building theorems.

Implements CVC3::CoreProofRules.

Definition at line 670 of file core_theorem_producer.cpp.

References CVC3::Assumptions::emptyAssump().

Member Data Documentation

TheoryCore* CVC3::CoreTheoremProducer::d_core
private

pointer to theory core

Definition at line 43 of file core_theorem_producer.h.


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