CVC3::CoreProofRules Class Reference

#include <core_proof_rules.h>

Inheritance diagram for CVC3::CoreProofRules:

[legend]

List of all members.

Public Member Functions

• virtual ~CoreProofRules ()

  Destructor.
  

• 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 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 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 rewriteDistinct (const Expr &e)=0

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

• 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
  

• virtual Theorem dummyTheorem (const Expr &e)=0

  Temporary cheat for building theorems.
  

---

Detailed Description

Definition at line 34 of file core_proof_rules.h.

---

Constructor & Destructor Documentation

virtual CVC3::CoreProofRules::~CoreProofRules

(

)

[inline, virtual]

Destructor.

Definition at line 37 of file core_proof_rules.h.

---

Member Function Documentation

virtual Theorem CVC3::CoreProofRules::typePred

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::setupTerm(), and CVC3::TheoryCore::typePred().

virtual Theorem CVC3::CoreProofRules::rewriteLetDecl

(

const Expr &

e

)

[pure virtual]

Replace LETDECL with its definition.

Used only in TheoryCore

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), and CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::rewriteNotAnd

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().

virtual Theorem CVC3::CoreProofRules::rewriteNotOr

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().

virtual Theorem CVC3::CoreProofRules::rewriteNotIff

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::rewriteNotIte

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().

virtual Theorem CVC3::CoreProofRules::rewriteIteThen	(	const Expr &	e,
		const Theorem &	thenThm
	)			[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::newPPrec().

virtual Theorem CVC3::CoreProofRules::rewriteIteElse	(	const Expr &	e,
		const Theorem &	elseThm
	)			[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::newPPrec().

virtual Theorem CVC3::CoreProofRules::rewriteIteBool	(	const Expr &	c,
		const Expr &	e1,
		const Expr &	e2
	)			[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::orDistributivityRule

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::andDistributivityRule

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::rewriteImplies

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryCore::rewrite(), and CVC3::TheoryCore::simplifyOp().

virtual Theorem CVC3::CoreProofRules::rewriteDistinct

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::NotToIte

(

const Expr &

not_e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::OrToIte

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::AndToIte

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::IffToIte

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::ImpToIte

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::rewriteIteToNot

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::rewriteIteToOr

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::rewriteIteToAnd

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::rewriteIteToIff

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::rewriteIteToImp

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::rewriteIteCond

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite(), and CVC3::ExprTransform::simplifyWithCare().

virtual Theorem CVC3::CoreProofRules::ifLiftUnaryRule

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::iffOrDistrib

(

const Expr &

iff

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::CoreProofRules::iffAndDistrib

(

const Expr &

iff

)

[pure virtual]

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

Implemented in CVC3::CoreTheoremProducer.

virtual Theorem CVC3::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 CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::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 CVC3::CoreTheoremProducer.

Referenced by CVC3::TheoryCore::rewrite().

virtual Theorem CVC3::CoreProofRules::dummyTheorem

(

const Expr &

e

)

[pure virtual]

Temporary cheat for building theorems.

Implemented in CVC3::CoreTheoremProducer.

Referenced by CVC3::ExprTransform::dobryant(), and CVC3::ExprTransform::simplifyWithCare().

---

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

• core_proof_rules.h