CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
expr_op.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file expr_op.h
4
* \brief Class Op representing the Expr's operator.
5
*
6
* Author: Sergey Berezin
7
*
8
* Created: Fri Feb 7 15:14:42 2003
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*
19
*/
20
/*****************************************************************************/
21
22
// expr.h Has to be included outside of #ifndef, since it sources us
23
// recursively (read comments in expr_value.h).
24
#ifndef _cvc3__expr_h_
25
#include "
expr.h
"
26
#endif
27
28
#ifndef _cvc3__expr_op_h_
29
#define _cvc3__expr_op_h_
30
31
namespace
CVC3 {
32
33
class
ExprManager;
34
35
///////////////////////////////////////////////////////////////////////////////
36
// //
37
// Class: Op //
38
// Author: Clark Barrett //
39
// Created: Wed Nov 27 15:50:38 2002 //
40
// Description: Encapsulates all possible Expr operators (including UFUNC) //
41
// and allows switching on the kind. //
42
// Kinds should be registered with ExprManager. //
43
//
44
// Technically, class Op is not part of Expr; it is provided as an
45
// abstraction for the user. So, building an Expr from an Op is less
46
// efficient than building the same Expr directly from the kind.
47
///////////////////////////////////////////////////////////////////////////////
48
class
Op
{
49
friend
class
Expr
;
50
friend
class
ExprApply
;
51
friend
class
ExprApplyTmp
;
52
friend
class ::CInterface;
53
54
int
d_kind
;
55
Expr
d_expr
;
56
57
// Disallow silent conversion of expr to op
58
//! Constructor for operators
59
Op
(
const
Expr
& e):
d_kind
(
APPLY
),
d_expr
(e) { }
60
61
public
:
62
/////////////////////////////////////////////////////////////////////////
63
// Public methods
64
/////////////////////////////////////////////////////////////////////////
65
66
Op
() :
d_kind
(
NULL_KIND
) { }
67
// Construct an operator from a kind.
68
Op
(
int
kind) :
d_kind
(kind),
d_expr
()
69
{
DebugAssert
(kind !=
APPLY
,
"APPLY cannot be an operator on its own"
); }
70
// Copy constructor
71
Op
(
const
Op
& op):
d_kind
(op.
d_kind
),
d_expr
(op.
d_expr
) { }
72
// A constructor that rebuilds the Op for the given ExprManager
73
Op
(
ExprManager
* em,
const
Op
& op);
74
// Destructor (does nothing)
75
~Op
() { }
76
// Assignment operator
77
Op
&
operator=
(
const
Op
& op);
78
79
// Check if Op is NULL
80
bool
isNull
()
const
{
return
d_kind
==
NULL_KIND
; }
81
// Return the kind of the operator
82
int
getKind
()
const
{
return
d_kind
; }
83
// Return the expr associated with this operator if applicable.
84
const
Expr
&
getExpr
()
const
85
{
DebugAssert
(
d_kind
==
APPLY
,
"Expected APPLY"
);
return
d_expr
; }
86
87
// Printing functions.
88
89
std::string
toString
()
const
;
90
friend
std::ostream&
operator<<
(std::ostream& os,
const
Op
& op) {
91
return
os <<
"Op("
<< op.
d_kind
<<
" "
<< op.
d_expr
<<
")"
;
92
}
93
friend
bool
operator==
(
const
Op
& op1,
const
Op
& op2) {
94
return
op1.
d_kind
== op2.
d_kind
&& op1.
d_expr
== op2.
d_expr
;
95
}
96
97
};
// end of class Op
98
99
100
}
// end of namespace CVC3
101
102
#endif
Generated on Mon Aug 6 2012 09:40:04 for CVC3 by
1.8.1.1