CVC3
|
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 | ExprHashMap< Data > |
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) |
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.