theory_arith.h File Reference

#include "theory.h"
#include "cdmap.h"

Go to the source code of this file.

Classes

• class CVC3::TheoryArith

  This theory handles basic linear arithmetic. More...
  

Namespaces

• namespace CVC3

Enumerations

• enum CVC3::ArithKinds {
    CVC3::REAL_CONST = 30, CVC3::NEGINF = 31, CVC3::POSINF = 32, CVC3::REAL = 3000,
    CVC3::INT, CVC3::SUBRANGE, CVC3::UMINUS, CVC3::PLUS,
    CVC3::MINUS, CVC3::MULT, CVC3::DIVIDE, CVC3::POW,
    CVC3::INTDIV, CVC3::MOD, CVC3::LT, CVC3::LE,
    CVC3::GT, CVC3::GE, CVC3::IS_INTEGER, CVC3::DARK_SHADOW,
    CVC3::GRAY_SHADOW
  }

Functions

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

  a Mult expr with two or more children
  

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

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

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

---

Detailed Description

Author: Clark Barrett

Created: Fri Jan 17 18:34:55 2003

---

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.

---

Definition in file theory_arith.h.