CVC3  2.4.1
Classes | Namespaces | Typedefs | Enumerations | Functions
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::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

 CVC3
 

Typedefs

typedef long unsigned CVC3::ExprIndex
 Expression index type. More...
 

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.