23 #ifndef _cvc3__expr_h_
27 #ifndef _cvc3__include__type_h_
28 #define _cvc3__include__type_h_
55 int arity()
const {
return d_expr.arity(); }
59 bool isNull()
const {
return d_expr.isNull(); }
75 static Type funType(
const std::vector<Type>& typeDom,
const Type& typeRan);
80 std::string
toString()
const {
return getExpr().toString(); }
Data structure of expressions in CVC3.
Cardinality card() const
Return cardinality of type.
ostream & operator<<(ostream &os, const Expr &e)
const Expr & boolExpr()
BOOLEAN Expr.
MS C++ specific settings.
bool operator==(const Expr &e1, const Expr &e2)
const Expr & getExpr() const
Type(Expr expr, bool dummy)
Type(const Type &type)
Special constructor that doesn't check if expr is a type.
Expr enumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Expr typeEnumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Abstraction over different operating systems.
Expr newLeafExpr(const Op &op)
std::string toString() const
static Type anyType(ExprManager *em)
bool operator!=(const Expr &e1, const Expr &e2)
Definition of the API to expression package. See class Expr for details.
Unsigned sizeFinite() const
Return size of a finite type; returns 0 if size cannot be determined.
Cardinality
Enum for cardinality of types.
static Type typeBool(ExprManager *em)
Type operator[](int i) const
Type funType(const Type &typeRan) const