expr.h File Reference

Definition of the API to expression package. See class Expr for details. More...

#include <stdlib.h>
#include <sstream>
#include <set>
#include <functional>
#include <iterator>
#include <map>
#include "os.h"
#include "compat_hash_map.h"
#include "compat_hash_set.h"
#include "rational.h"
#include "kinds.h"
#include "cdo.h"
#include "cdflags.h"
#include "lang.h"
#include "memory_manager.h"

Go to the source code of this file.

Classes

• class CVC3::Expr

  Data structure of expressions in CVC3. More...
  

• class CVC3::Expr::iterator
• class CVC3::Expr::iterator::Proxy

  Postfix increment requires a Proxy object to hold the intermediate value for dereferencing. More...
  

Namespaces

• namespace CVC3

Typedefs

• typedef long unsigned CVC3::ExprIndex

  Expression index type.
  

Enumerations

• enum CVC3::ExprValueType {
    CVC3::EXPR_VALUE, CVC3::EXPR_NODE, CVC3::EXPR_APPLY, CVC3::EXPR_STRING,
    CVC3::EXPR_RATIONAL, CVC3::EXPR_SKOLEM, CVC3::EXPR_UCONST, CVC3::EXPR_SYMBOL,
    CVC3::EXPR_BOUND_VAR, CVC3::EXPR_CLOSURE, CVC3::EXPR_VALUE_TYPE_LAST
  }

  Type ID of each ExprValue subclass.

  More...
  

• enum CVC3::Cardinality { CVC3::CARD_FINITE, CVC3::CARD_INFINITE, CVC3::CARD_UNKNOWN }

  Enum for cardinality of types.

  More...
  

Functions

• Expr CVC3::andExpr (const std::vector< Expr > &children)
• Expr CVC3::orExpr (const std::vector< Expr > &children)
• bool CVC3::operator== (const Expr &e1, const Expr &e2)
• bool CVC3::operator!= (const Expr &e1, const Expr &e2)
• bool CVC3::operator< (const Expr &e1, const Expr &e2)
• bool CVC3::operator<= (const Expr &e1, const Expr &e2)
• bool CVC3::operator> (const Expr &e1, const Expr &e2)
• bool CVC3::operator>= (const Expr &e1, const Expr &e2)

---

Detailed Description

Definition of the API to expression package. See class Expr for details.

Author: Clark Barrett

Created: Tue Nov 26 00:27:40 2002

---

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 expr.h.