blob: 5a11e0fbd651579e713319e07bc725e6ce6e9f9c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
/********************* -*- C++ -*- */
/** cvc4_expr.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** Reference-counted encapsulation of a pointer to an expression.
**/
#ifndef __CVC4__EXPR_H
#define __CVC4__EXPR_H
#include <vector>
#include <iostream>
#include <stdint.h>
#include "cvc4_config.h"
#include "expr/kind.h"
namespace CVC4 {
class Expr;
}/* CVC4 namespace */
namespace std {
inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC;
}
namespace CVC4 {
class ExprManager;
namespace expr {
class ExprValue;
}/* CVC4::expr namespace */
using CVC4::expr::ExprValue;
/**
* Encapsulation of an ExprValue pointer. The reference count is
* maintained in the ExprValue.
*/
class CVC4_PUBLIC Expr {
/** A convenient null-valued encapsulated pointer */
static Expr s_null;
/** The referenced ExprValue */
ExprValue* d_ev;
/** This constructor is reserved for use by the Expr package; one
* must construct an Expr using one of the build mechanisms of the
* Expr package.
*
* Increments the reference count. */
explicit Expr(ExprValue*);
friend class ExprBuilder;
friend class ExprManager;
public:
CVC4_PUBLIC Expr(const Expr&);
/** Destructor. Decrements the reference count and, if zero,
* collects the ExprValue. */
CVC4_PUBLIC ~Expr();
Expr& operator=(const Expr&) CVC4_PUBLIC;
/** Access to the encapsulated expression.
* @return the encapsulated expression. */
ExprValue* operator->() const CVC4_PUBLIC;
uint64_t hash() const;
Expr eqExpr(const Expr& right) const;
Expr notExpr() const;
Expr negate() const; // avoid double-negatives
Expr andExpr(const Expr& right) const;
Expr orExpr(const Expr& right) const;
Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
Expr iffExpr(const Expr& right) const;
Expr impExpr(const Expr& right) const;
Expr xorExpr(const Expr& right) const;
Expr plusExpr(const Expr& right) const;
Expr uMinusExpr() const;
Expr multExpr(const Expr& right) const;
inline Kind getKind() const;
inline size_t numChildren() const;
static Expr null() { return s_null; }
typedef Expr* iterator;
typedef Expr const* const_iterator;
inline iterator begin();
inline iterator end();
inline iterator begin() const;
inline iterator end() const;
void toString(std::ostream&) const;
};/* class Expr */
}/* CVC4 namespace */
#include "expr/expr_value.h"
inline std::ostream& std::operator<<(std::ostream& out, CVC4::Expr e) {
e.toString(out);
return out;
}
namespace CVC4 {
inline Kind Expr::getKind() const {
return Kind(d_ev->d_kind);
}
inline void Expr::toString(std::ostream& out) const {
if(d_ev)
d_ev->toString(out);
else out << "null";
}
inline Expr::iterator Expr::begin() {
return d_ev->begin();
}
inline Expr::iterator Expr::end() {
return d_ev->end();
}
inline Expr::iterator Expr::begin() const {
return d_ev->begin();
}
inline Expr::iterator Expr::end() const {
return d_ev->end();
}
inline size_t Expr::numChildren() const {
return d_ev->d_nchildren;
}
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_H */
|
