theory_arith.h File Reference

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

Include dependency graph for theory_arith.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces

• namespace CVC3

Classes

• class CVC3::TheoryArith

  This theory handles basic linear arithmetic. More...
  

Enumerations

• enum CVC3::ArithKinds {
    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::NEGINF, CVC3::POSINF, CVC3::DARK_SHADOW, CVC3::GRAY_SHADOW,
    CVC3::REAL_CONST
  }

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.

---