theory_arith.h File Reference

Go to the source code of this file.

Namespaces

• namespace CVCL

Classes

• class CVCL::TheoryArith

  This theory handles basic linear arithmetic. More...
  

• class CVCL::TheoryArith::FreeConst

  Data class for the strongest free constant in separation inqualities. More...
  

• class CVCL::TheoryArith::Ineq

  Private class for an inequality in the Fourier-Motzkin database. More...
  

• class CVCL::TheoryArith::VarOrderGraph

Enumerations

• enum ArithKinds {
    REAL = 3000, INT, SUBRANGE, UMINUS,
    PLUS, MINUS, MULT, DIVIDE,
    POW, INTDIV, MOD, LT,
    LE, GT, GE, IS_INTEGER,
    NEGINF, POSINF, DARK_SHADOW, GRAY_SHADOW
  }
• enum ArithLang {
    NOT_USED = 0, TERMS_ONLY, DIFF_ONLY, LINEAR,
    NONLINEAR
  }

  Used to keep track of which subset of arith is being used. More...
  

Functions

• bool isReal (Type t)
• bool isInt (Type t)
• bool isRational (const Expr &e)
• bool isUMinus (const Expr &e)
• bool isPlus (const Expr &e)
• bool isMinus (const Expr &e)
• bool isMult (const Expr &e)
• bool isDivide (const Expr &e)
• bool isLT (const Expr &e)
• bool isLE (const Expr &e)
• bool isGT (const Expr &e)
• bool isGE (const Expr &e)
• bool isDarkShadow (const Expr &e)
• bool isIneq (const Expr &e)
• bool isIntPred (const Expr &e)
• Expr uminusExpr (const Expr &child)
• Expr plusExpr (const Expr &left, const Expr &right)
• Expr plusExpr (const std::vector< Expr > &children)
• Expr minusExpr (const Expr &left, const Expr &right)
• Expr multExpr (const Expr &left, const Expr &right)
• Expr multExpr (const std::vector< Expr > &children)

  a Mult expr with two or more children
  

• Expr powExpr (const Expr &pow, const Expr &base)

  Power (x^n, or base^{pow}) expressions.
  

• Expr divideExpr (const Expr &left, const Expr &right)
• Expr ltExpr (const Expr &left, const Expr &right)
• Expr leExpr (const Expr &left, const Expr &right)
• Expr gtExpr (const Expr &left, const Expr &right)
• Expr geExpr (const Expr &left, const Expr &right)
• Expr operator- (const Expr &child)
• Expr operator+ (const Expr &left, const Expr &right)
• Expr operator- (const Expr &left, const Expr &right)
• Expr operator * (const Expr &left, const Expr &right)
• Expr operator/ (const Expr &left, const Expr &right)

---

Detailed Description

Author: Clark Barrett

Created: Fri Jan 17 18:34:55 2003

---

Copyright (C) 2003 by the Board of Trustees of Leland Stanford Junior University and by New York University.

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution. In particular:

• The above copyright notice and this permission notice must appear in all copies of the software and related documentation.

• THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK.

---

Definition in file theory_arith.h.

---

Enumeration Type Documentation

enum ArithKinds

Enumeration values: REAL  INT  SUBRANGE  UMINUS  PLUS  MINUS  MULT  DIVIDE  POW  INTDIV  MOD  LT  LE  GT  GE  IS_INTEGER  NEGINF  POSINF  DARK_SHADOW  GRAY_SHADOW  Definition at line 43 of file theory_arith.h.

enum ArithLang

Used to keep track of which subset of arith is being used. Enumeration values: NOT_USED  TERMS_ONLY  DIFF_ONLY  LINEAR  NONLINEAR  Definition at line 68 of file theory_arith.h. Referenced by CVCL::TheoryArith::getLangUsed().

---

Function Documentation

bool isReal (  Type  t  )  [inline]

Definition at line 376 of file theory_arith.h. References CVCL::Type::getExpr(), and CVCL::Expr::getKind(). Referenced by CVCL::TheorySimulate::computeType(), CVCL::TheoryArith::isIntegerThm(), CVCL::TheoryArith::processRealEq(), and CVCL::TheoryArith::refineCounterExample().

bool isInt (  Type  t  )  [inline]

Definition at line 377 of file theory_arith.h. References CVCL::Type::getExpr(), and CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::computeType(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::print(), and CVCL::TheoryArith::projectInequalities().

bool isRational (  const Expr &  e  )  [inline]

Definition at line 380 of file theory_arith.h. References CVCL::Expr::isRational(). Referenced by CVCL::ArithTheoremProducer::canonDivideConst(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonDivideVar(), CVCL::ArithTheoremProducer::canonInvertConst(), CVCL::ArithTheoremProducer::canonMultConstConst(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultConstTerm(), CVCL::ArithTheoremProducer::canonMultTermConst(), CVCL::TheoryArith::computeModel(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::TheoryArith::findRationalBound(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::lessThanVar(), CVCL::TheoryArith::normalize(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::separateMonomial(), CVCL::TheoryArith::setup(), and CVCL::TheoryArith::updateSubsumptionDB().

bool isUMinus (  const Expr &  e  )  [inline]

Definition at line 381 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::isSyntacticRational(), and CVCL::TheoryArith::isSyntacticUMinusVar().

bool isPlus (  const Expr &  e  )  [inline]

Definition at line 382 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::addToBuffer(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::TheoryArith::computeNormalFactor(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::create_t2(), CVCL::ArithTheoremProducer::create_t3(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::pickMonomial(), CVCL::TheoryArith::print(), CVCL::TheoryArith::processBuffer(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::separateMonomial(), CVCL::ArithTheoremProducer::substitute(), and CVCL::TheoryArith::updateSubsumptionDB().

bool isMinus (  const Expr &  e  )  [inline]

Definition at line 383 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::print().

bool isMult (  const Expr &  e  )  [inline]

Definition at line 384 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::TheoryArith::computeNormalFactor(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::isSyntacticUMinusVar(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ArithTheoremProducer::monomialMulF(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryArith::separateMonomial(), and CVCL::ArithTheoremProducer::substitute().

bool isDivide (  const Expr &  e  )  [inline]

Definition at line 385 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::ArithTheoremProducer::eqElimIntRule(), and CVCL::TheoryArith::isSyntacticRational().

bool isLT (  const Expr &  e  )  [inline]

Definition at line 386 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), CVCL::TheoryArith::findBounds(), CVCL::isIneq(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::isStale(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::projectInequalities(), CVCL::ArithTheoremProducer::realShadow(), CVCL::TheoryArith::setup(), and CVCL::TheoryArith::updateSubsumptionDB().

bool isLE (  const Expr &  e  )  [inline]

Definition at line 387 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::isIneq(), CVCL::TheoryArith::isolateVariable(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::projectInequalities(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::TheoryArith::setup(), and CVCL::TheoryArith::updateSubsumptionDB().

bool isGT (  const Expr &  e  )  [inline]

Definition at line 388 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::ArithTheoremProducer::flipInequality(), CVCL::isIneq(), CVCL::ArithTheoremProducer::negatedInequality(), and CVCL::TheoryArith::rewrite().

bool isGE (  const Expr &  e  )  [inline]

Definition at line 389 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::ArithTheoremProducer::flipInequality(), CVCL::isIneq(), and CVCL::TheoryArith::rewrite().

bool isDarkShadow (  const Expr &  e  )  [inline]

Definition at line 390 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::expandDarkShadow(), and CVCL::TheoryArith::setup().

bool isIneq (  const Expr &  e  )  [inline]

Definition at line 391 of file theory_arith.h. References CVCL::isGE(), CVCL::isGT(), CVCL::isLE(), and CVCL::isLT(). Referenced by CVCL::TheoryArith::freeConstIneq(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::TheoryArith::normalize(), CVCL::TheoryArith::print(), CVCL::TheoryArith::rewrite(), and CVCL::TheoryArith::update().

bool isIntPred (  const Expr &  e  )  [inline]

Definition at line 393 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), and CVCL::ArithTheoremProducer::lessThanToLE().

Expr uminusExpr (  const Expr &  child  )  [inline]

Definition at line 396 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::operator-(), and CVCL::TheoryArith::parseExprOp().

Expr plusExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 398 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::create_t2(), CVCL::ArithTheoremProducer::create_t3(), CVCL::TheoryArith::parseExprOp(), CVCL::ArithTheoremProducer::substitute(), and CVCL::TheoryArith::updateSubsumptionDB().

Expr plusExpr (  const std::vector< Expr > &  children  )  [inline]

Definition at line 400 of file theory_arith.h. References CVCL::newExpr(), and CVCL::PLUS. Referenced by CVCL::operator+().

Expr minusExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 404 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::operator-(), and CVCL::TheoryArith::parseExprOp().

Expr multExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 406 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ArithTheoremProducer::monomialMulF(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryArith::separateMonomial(), and CVCL::ArithTheoremProducer::simplifiedMultExpr().

Expr multExpr (  const std::vector< Expr > &  children  )  [inline]

a Mult expr with two or more children Definition at line 410 of file theory_arith.h. References CVCL::MULT, and CVCL::newExpr(). Referenced by CVCL::operator *().

Expr powExpr (  const Expr &  pow, const Expr &  base )  [inline]

Power (x^n, or base^{pow}) expressions. Definition at line 415 of file theory_arith.h. References CVCL::newExpr(), and CVCL::pow(). Referenced by CVCL::ArithTheoremProducer::canonInvertLeaf(), CVCL::ArithTheoremProducer::canonInvertPow(), CVCL::ArithTheoremProducer::canonMultLeafLeaf(), CVCL::ArithTheoremProducer::canonMultLeafOrPowMult(), CVCL::ArithTheoremProducer::canonMultPowLeaf(), CVCL::ArithTheoremProducer::canonMultPowPow(), CVCL::TheoryArith::parseExprOp(), and CVCL::VCL::powExpr().

Expr divideExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 418 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::VCL::divideExpr(), CVCL::operator/(), and CVCL::TheoryArith::parseExprOp().

Expr ltExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 420 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::VCL::ltExpr(), and CVCL::TheoryArith::parseExprOp().

Expr leExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 422 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::TheoryArith::computeTypePred(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::VCL::leExpr(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::TheoryArith::parseExprOp(), and CVCL::TheoryArith::updateSubsumptionDB().

Expr gtExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 424 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::VCL::gtExpr(), and CVCL::TheoryArith::parseExprOp().

Expr geExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 426 of file theory_arith.h. References CVCL::Expr::getEM(), and CVCL::newExpr(). Referenced by CVCL::VCL::geExpr(), and CVCL::TheoryArith::parseExprOp().

Expr operator- (  const Expr &  child  )  [inline]

Definition at line 429 of file theory_arith.h. References CVCL::uminusExpr().

Expr operator+ (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 431 of file theory_arith.h. References CVCL::plusExpr().

Expr operator- (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 433 of file theory_arith.h. References CVCL::minusExpr().

Expr operator * (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 435 of file theory_arith.h. References CVCL::multExpr(). Referenced by CVCL::_Hashtable_const_iterator< _Key, _Data >::operator->(), CVCL::_Hashtable_iterator< _Key, _Data >::operator->(), and CVCL::Assumptions::iterator::operator->().

Expr operator/ (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 437 of file theory_arith.h. References CVCL::divideExpr().

---