CVC3::CoreTheoremProducer Class Reference

#include <core_theorem_producer.h>

Inheritance diagram for CVC3::CoreTheoremProducer:

[legend]Collaboration diagram for CVC3::CoreTheoremProducer:

[legend]List of all members.

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.
  

Private Attributes

• TheoryCore * d_core

  pointer to theory core
  

---

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

(

)

[inline, virtual]

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 d_core, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Theory::getTypePred(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

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(), CVC3::LETDECL, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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::isAnd(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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::isNot(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

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(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteThen	(	const Expr &	e,
		const Theorem &	thenThm
	)			[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 136 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteElse	(	const Expr &	e,
		const Theorem &	elseThm
	)			[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 161 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::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 CVC3::CoreProofRules.

Definition at line 186 of file core_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::orDistributivityRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 202 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::andDistributivityRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 245 of file core_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteDistinct

(

const Expr &

e

)

[virtual]

==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])

Implements CVC3::CoreProofRules.

Definition at line 297 of file core_theorem_producer.cpp.

References CVC3::AND, CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::DISTINCT, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getEM(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::NotToIte

(

const Expr &

not_e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 328 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_core, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Theory::getCommonRules(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CommonProofRules::rewriteNotFalse(), CVC3::CommonProofRules::rewriteNotTrue(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::OrToIte

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 345 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getKids(), CVC3::Expr::getType(), CVC3::Type::isNull(), CVC3::Expr::isOr(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::AndToIte

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 383 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getKids(), CVC3::Expr::getType(), CVC3::Expr::isAnd(), CVC3::Type::isNull(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::IffToIte

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 423 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_core, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Theory::getCommonRules(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CommonProofRules::reflexivityRule(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::ImpToIte

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 439 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_core, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Theory::getCommonRules(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CommonProofRules::reflexivityRule(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToNot

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 455 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToOr

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 467 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToAnd

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 479 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToIff

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 491 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::rewriteIteToImp

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 503 of file core_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isITE(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem CoreTheoremProducer::ifLiftUnaryRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::CoreProofRules.

Definition at line 588 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::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 CVC3::CoreProofRules.

Definition at line 621 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprHashMap< Data >::insert(), CVC3::Expr::isAnd(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::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 CVC3::CoreProofRules.

Definition at line 647 of file core_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::ExprHashMap< Data >::insert(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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(), and CVC3::TheoremProducer::newTheorem().

---

Member Data Documentation

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

pointer to theory core

Definition at line 43 of file core_theorem_producer.h.

Referenced by IffToIte(), ImpToIte(), NotToIte(), and typePred().

---

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

• core_theorem_producer.h
• core_theorem_producer.cpp

---