CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
type.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file type.h
4
*
5
* Author: Clark Barrett
6
*
7
* Created: Thu Dec 12 12:53:28 2002
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
*/
19
/*****************************************************************************/
20
21
// expr.h Has to be included outside of #ifndef, since it sources us
22
// recursively (read comments in expr_value.h).
23
#ifndef _cvc3__expr_h_
24
#include "
expr.h
"
25
#endif
26
27
#ifndef _cvc3__include__type_h_
28
#define _cvc3__include__type_h_
29
30
namespace
CVC3 {
31
32
#include "
os.h
"
33
34
///////////////////////////////////////////////////////////////////////////////
35
// //
36
// Class: Type //
37
// Author: Clark Barrett //
38
// Created: Thu Dec 12 12:53:34 2002 //
39
// Description: Wrapper around expr for api //
40
// //
41
///////////////////////////////////////////////////////////////////////////////
42
class
CVC_DLL
Type
{
43
Expr d_expr;
44
45
public
:
46
Type
() {}
47
Type
(
Expr
expr);
48
//! Special constructor that doesn't check if expr is a type
49
//TODO: make this private
50
Type
(
const
Type
& type) :d_expr(type.d_expr) {}
51
Type
(
Expr
expr,
bool
dummy) :d_expr(expr) {}
52
const
Expr
&
getExpr
()
const
{
return
d_expr; }
53
54
// Reasoning about children
55
int
arity
()
const
{
return
d_expr.arity(); }
56
Type
operator[]
(
int
i)
const
{
return
Type
(d_expr[i]); }
57
58
// Core testers
59
bool
isNull
()
const
{
return
d_expr.isNull(); }
60
bool
isBool
()
const
{
return
d_expr.getKind() ==
BOOLEAN
; }
61
bool
isSubtype
()
const
{
return
d_expr.getKind() ==
SUBTYPE
; }
62
bool
isFunction
()
const
{
return
d_expr.getKind() ==
ARROW
; }
63
//! Return cardinality of type
64
Cardinality
card
()
const
{
return
d_expr.typeCard(); }
65
//! Return nth (starting with 0) element in a finite type
66
/*! Returns NULL Expr if unable to compute nth element
67
*/
68
Expr
enumerateFinite
(
Unsigned
n)
const
{
return
d_expr.
typeEnumerateFinite
(n); }
69
//! Return size of a finite type; returns 0 if size cannot be determined
70
Unsigned
sizeFinite
()
const
{
return
d_expr.typeSizeFinite(); }
71
72
// Core constructors
73
static
Type
typeBool
(
ExprManager
* em) {
return
Type
(em->
boolExpr
(),
true
); }
74
static
Type
anyType
(
ExprManager
* em) {
return
Type
(em->
newLeafExpr
(
ANY_TYPE
)); }
75
static
Type
funType(
const
std::vector<Type>& typeDom,
const
Type
& typeRan);
76
Type
funType(
const
Type
& typeRan)
const
77
{
return
Type
(
Expr
(
ARROW
, d_expr, typeRan.
d_expr
)); }
78
79
// Printing
80
std::string
toString
()
const
{
return
getExpr().toString(); }
81
};
82
83
inline
bool
operator==
(
const
Type
& t1,
const
Type
& t2)
84
{
return
t1.
getExpr
() == t2.
getExpr
(); }
85
86
inline
bool
operator!=
(
const
Type
& t1,
const
Type
& t2)
87
{
return
t1.
getExpr
() != t2.
getExpr
(); }
88
89
// Printing
90
inline
std::ostream&
operator<<
(std::ostream& os,
const
Type
& t) {
91
return
os << t.
getExpr
();
92
}
93
94
}
95
96
#endif
Generated on Sun Aug 5 2012 13:19:08 for CVC3 by
1.8.1.2