CVCL::RefinedArithTheoremProducer Class Reference

#include <refined_arith_theorem_producer.h>

Inheritance diagram for CVCL::RefinedArithTheoremProducer:

[legend]Collaboration diagram for CVCL::RefinedArithTheoremProducer:

[legend]List of all members.

Public Member Functions

• Theorem ltAddR (const Expr &x, const Expr &y, const Expr &z)
• Theorem ltTrans (const Expr &x, const Expr &y, const Expr &z)
• Theorem ltScale (const Expr &x, const Expr &y, const Expr &z)
• Theorem arithmetic (const Expr &lhs, const Expr &rhs)
• Theorem minusDef (const Expr &x, const Expr &y)
• Theorem divideDef (const Expr &x, const Expr &y)
• Theorem distribR (const Expr &x, const Expr &y, const Expr &z)
• Theorem addR (const Theorem &xEy, const Expr &z)
• Theorem addRID (const Expr &x)
• Theorem cancelR (const Expr &x, const Expr &y)
• Theorem addRCancel (const Theorem &t)
• Theorem multZeroL (const Expr &e)
• Expr neg (const Expr &x)
• Expr inv (const Expr &x)
• Expr frac (const Expr &x, const Expr &y)
• Expr plus (const Expr &x, const Expr &y)
• Theorem trans (const Theorem &t1, const Theorem &t2)
• Theorem trans (const Expr &e)
• Theorem symm (const Theorem &t)
• Theorem subst (Op op, const Expr &x, const Theorem &t)
• Theorem subst (Op op, const Theorem &t, const Expr &x)
• Theorem subst (Op op, const Theorem &t1, const Theorem &t2)
• RefinedArithTheoremProducer (VCL *vcl)
• Expr rat (Rational r)

  Create Expr from Rational (for convenience).
  

• Theorem uMinusToMult (const Expr &e)

  ==> -(e) = (-1) * e
  

• Theorem minusToPlus (const Expr &x, const Expr &y)

  ==> x - y = x + (-1) * y
  

• Theorem canonPlus (const Expr &e)

  Canonize (PLUS t1 ... tn).
  

Private Member Functions

• Rational eval (const Expr &rational_expr)
• Theorem addAssoc (const Expr &x, const Expr &y, const Expr &z)
• Theorem multAssoc (const Expr &x, const Expr &y, const Expr &z)
• Theorem addSymm (const Expr &x, const Expr &y)
• Theorem multSymm (const Expr &x, const Expr &y)
• Theorem distribL (const Expr &x, const Expr &y, const Expr &z)
• Theorem addLID (const Expr &x)
• Theorem multLID (const Expr &x)
• Theorem addInvR (const Expr &x)
• Theorem multInvR (const Expr &x)

Private Attributes

• ExprManager * d_em
• TheoryCore * core
• VCL * vcl
• const Expr zero
• const Expr one

---

Detailed Description

Definition at line 63 of file refined_arith_theorem_producer.h.

---

Constructor & Destructor Documentation

CVCL::RefinedArithTheoremProducer::RefinedArithTheoremProducer (  VCL *  vcl  )  [inline]

Definition at line 116 of file refined_arith_theorem_producer.h. References core.

---

Member Function Documentation

Rational RefinedArithTheoremProducer::eval (  const Expr &  rational_expr  )  [private]

Definition at line 366 of file refined_arith_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::DIVIDE, CVCL::Expr::getKind(), CVCL::Expr::getRational(), CVCL::MULT, CVCL::PLUS, CVCL::RATIONAL_EXPR, CVCL::Expr::toString(), and CVCL::UMINUS. Referenced by arithmetic().

Theorem RefinedArithTheoremProducer::addAssoc (  const Expr &  x, const Expr &  y, const Expr &  z )  [private]

Definition at line 102 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::PLUS, and CVCL::TheoremProducer::withProof(). Referenced by cancelR(), multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::multAssoc (  const Expr &  x, const Expr &  y, const Expr &  z )  [private]

Definition at line 124 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::MULT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof().

Theorem RefinedArithTheoremProducer::addSymm (  const Expr &  x, const Expr &  y )  [private]

Definition at line 145 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::PLUS, and CVCL::TheoremProducer::withProof(). Referenced by addRID().

Theorem RefinedArithTheoremProducer::multSymm (  const Expr &  x, const Expr &  y )  [private]

Definition at line 164 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::MULT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof(). Referenced by distribR().

Theorem RefinedArithTheoremProducer::distribL (  const Expr &  x, const Expr &  y, const Expr &  z )  [private]

Definition at line 184 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::MULT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::PLUS, and CVCL::TheoremProducer::withProof(). Referenced by distribR().

Theorem RefinedArithTheoremProducer::addLID (  const Expr &  x  )  [private]

Definition at line 205 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::PLUS, CVCL::TheoremProducer::withProof(), and zero. Referenced by addRID(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::multLID (  const Expr &  x  )  [private]

Definition at line 223 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::MULT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), one, and CVCL::TheoremProducer::withProof(). Referenced by uMinusToMult().

Theorem RefinedArithTheoremProducer::addInvR (  const Expr &  x  )  [private]

Definition at line 241 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::PLUS, CVCL::UMINUS, CVCL::TheoremProducer::withProof(), and zero. Referenced by cancelR(), multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::multInvR (  const Expr &  x  )  [private]

Definition at line 260 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::DIVIDE, CVCL::TheoremManager::getEM(), CVCL::MULT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), one, and CVCL::TheoremProducer::withProof().

Theorem RefinedArithTheoremProducer::ltAddR (  const Expr &  x, const Expr &  y, const Expr &  z )

Definition at line 281 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::IMPLIES, CVCL::LT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::PLUS, and CVCL::TheoremProducer::withProof().

Theorem RefinedArithTheoremProducer::ltTrans (  const Expr &  x, const Expr &  y, const Expr &  z )

Definition at line 304 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::IMPLIES, CVCL::LT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), and CVCL::TheoremProducer::withProof().

Theorem RefinedArithTheoremProducer::ltScale (  const Expr &  x, const Expr &  y, const Expr &  z )

Definition at line 327 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::IMPLIES, CVCL::LT, CVCL::MULT, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::TheoremProducer::withProof(), and zero.

Theorem RefinedArithTheoremProducer::arithmetic (  const Expr &  lhs, const Expr &  rhs )

Definition at line 352 of file refined_arith_theorem_producer.cpp. References eval(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof(). Referenced by multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::minusDef (  const Expr &  x, const Expr &  y )

Definition at line 412 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::TheoremManager::getEM(), CVCL::MINUS, neg(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), plus(), and CVCL::TheoremProducer::withProof(). Referenced by minusToPlus().

Theorem RefinedArithTheoremProducer::divideDef (  const Expr &  x, const Expr &  y )

Definition at line 430 of file refined_arith_theorem_producer.cpp. References CVCL::TheoremProducer::d_tm, CVCL::DIVIDE, CVCL::TheoremManager::getEM(), neg(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), plus(), and CVCL::TheoremProducer::withProof().

Theorem RefinedArithTheoremProducer::distribR (  const Expr &  x, const Expr &  y, const Expr &  z )

Definition at line 488 of file refined_arith_theorem_producer.cpp. References d_em, distribL(), multSymm(), CVCL::PLUS, subst(), and trans(). Referenced by multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::addR (  const Theorem &  xEy, const Expr &  z )

Definition at line 509 of file refined_arith_theorem_producer.cpp. References CVCL::PLUS, and subst(). Referenced by addRCancel(), multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::addRID (  const Expr &  x  )

Definition at line 530 of file refined_arith_theorem_producer.cpp. References addLID(), addSymm(), trans(), and zero. Referenced by cancelR(), multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::cancelR (  const Expr &  x, const Expr &  y )

Definition at line 557 of file refined_arith_theorem_producer.cpp. References addAssoc(), addInvR(), addRID(), neg(), CVCL::PLUS, subst(), and trans(). Referenced by addRCancel().

Theorem RefinedArithTheoremProducer::addRCancel (  const Theorem &  t  )

Definition at line 588 of file refined_arith_theorem_producer.cpp. References addR(), cancelR(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), neg(), symm(), and trans().

Theorem RefinedArithTheoremProducer::multZeroL (  const Expr &  e  )

Definition at line 629 of file refined_arith_theorem_producer.cpp. References addAssoc(), addInvR(), addR(), addRID(), arithmetic(), CVCL::TheoremProducer::d_tm, distribR(), CVCL::TheoremManager::getEM(), CVCL::Theorem::getLHS(), CVCL::MULT, neg(), CVCL::PLUS, subst(), symm(), trans(), and zero. Referenced by uMinusToMult().

Expr RefinedArithTheoremProducer::neg (  const Expr &  x  )

Definition at line 35 of file refined_arith_theorem_producer.cpp. References d_em, and CVCL::UMINUS. Referenced by addRCancel(), cancelR(), divideDef(), minusDef(), multZeroL(), and uMinusToMult().

Expr RefinedArithTheoremProducer::inv (  const Expr &  x  )

Definition at line 39 of file refined_arith_theorem_producer.cpp. References d_em, CVCL::DIVIDE, and one.

Expr RefinedArithTheoremProducer::frac (  const Expr &  x, const Expr &  y )

Definition at line 47 of file refined_arith_theorem_producer.cpp. References d_em, and CVCL::DIVIDE.

Expr RefinedArithTheoremProducer::plus (  const Expr &  x, const Expr &  y )

Definition at line 43 of file refined_arith_theorem_producer.cpp. References d_em, and CVCL::PLUS. Referenced by divideDef(), minusDef(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::trans (  const Theorem &  t1, const Theorem &  t2 )

Definition at line 52 of file refined_arith_theorem_producer.cpp. References core, and CVCL::Theory::transitivityRule(). Referenced by addRCancel(), addRID(), cancelR(), distribR(), minusToPlus(), multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::trans (  const Expr &  e  )

Definition at line 56 of file refined_arith_theorem_producer.cpp. References core, and CVCL::Theory::reflexivityRule().

Theorem RefinedArithTheoremProducer::symm (  const Theorem &  t  )

Definition at line 60 of file refined_arith_theorem_producer.cpp. References core, and CVCL::Theory::symmetryRule(). Referenced by addRCancel(), multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::subst (  Op  op, const Expr &  x, const Theorem &  t )

Definition at line 64 of file refined_arith_theorem_producer.cpp. References core, CVCL::Theory::reflexivityRule(), and CVCL::Theory::substitutivityRule(). Referenced by addR(), cancelR(), distribR(), minusToPlus(), multZeroL(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::subst (  Op  op, const Theorem &  t, const Expr &  x )

Definition at line 71 of file refined_arith_theorem_producer.cpp. References core, CVCL::Theory::reflexivityRule(), and CVCL::Theory::substitutivityRule().

Theorem RefinedArithTheoremProducer::subst (  Op  op, const Theorem &  t1, const Theorem &  t2 )

Definition at line 78 of file refined_arith_theorem_producer.cpp. References core, and CVCL::Theory::substitutivityRule().

Expr CVCL::RefinedArithTheoremProducer::rat (  Rational  r  )  [inline]

Create Expr from Rational (for convenience). Reimplemented from CVCL::ArithTheoremProducer. Definition at line 122 of file refined_arith_theorem_producer.h. References d_em.

Theorem RefinedArithTheoremProducer::uMinusToMult (  const Expr &  e  )  [virtual]

==> -(e) = (-1) * e Reimplemented from CVCL::ArithTheoremProducer. Definition at line 688 of file refined_arith_theorem_producer.cpp. References addAssoc(), addInvR(), addLID(), addR(), addRID(), arithmetic(), distribR(), CVCL::Theorem::getRHS(), CVCL::MULT, multLID(), multZeroL(), neg(), one, CVCL::PLUS, plus(), subst(), symm(), trans(), and zero. Referenced by minusToPlus().

Theorem RefinedArithTheoremProducer::minusToPlus (  const Expr &  x, const Expr &  y )  [virtual]

==> x - y = x + (-1) * y Reimplemented from CVCL::ArithTheoremProducer. Definition at line 731 of file refined_arith_theorem_producer.cpp. References minusDef(), CVCL::PLUS, subst(), trans(), and uMinusToMult().

Theorem RefinedArithTheoremProducer::canonPlus (  const Expr &  e  )  [virtual]

Canonize (PLUS t1 ... tn). Reimplemented from CVCL::ArithTheoremProducer. Definition at line 22 of file refined_arith_theorem_producer.cpp. References CVCL::ArithTheoremProducer::canonPlus(), and std::endl().

---

Member Data Documentation

ExprManager* CVCL::RefinedArithTheoremProducer::d_em [private]

Reimplemented from CVCL::TheoremProducer. Definition at line 66 of file refined_arith_theorem_producer.h. Referenced by distribR(), frac(), inv(), neg(), plus(), and rat().

TheoryCore* CVCL::RefinedArithTheoremProducer::core [private]

Definition at line 67 of file refined_arith_theorem_producer.h. Referenced by RefinedArithTheoremProducer(), subst(), symm(), and trans().

VCL* CVCL::RefinedArithTheoremProducer::vcl [private]

Definition at line 68 of file refined_arith_theorem_producer.h.

const Expr CVCL::RefinedArithTheoremProducer::zero [private]

Definition at line 71 of file refined_arith_theorem_producer.h. Referenced by addInvR(), addLID(), addRID(), ltScale(), multZeroL(), and uMinusToMult().

const Expr CVCL::RefinedArithTheoremProducer::one [private]

Definition at line 71 of file refined_arith_theorem_producer.h. Referenced by inv(), multInvR(), multLID(), and uMinusToMult().

---

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

• refined_arith_theorem_producer.h
• refined_arith_theorem_producer.cpp

---