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
|
/********************* */
/** expr_manager.h
** Original author: dejan
** Major contributors: cconway, mdeters
** Minor contributors (to current version): taking
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 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.
**
** Public-facing expression manager interface.
**/
#ifndef __CVC4__EXPR_MANAGER_H
#define __CVC4__EXPR_MANAGER_H
#include "cvc4_config.h"
#include "expr/kind.h"
#include "expr/node_manager.h"
#include <vector>
namespace CVC4 {
class Expr;
class Type;
class BooleanType;
class FunctionType;
class KindType;
class SmtEngine;
class CVC4_PUBLIC ExprManager {
public:
/**
* Creates an expression manager.
*/
ExprManager();
/**
* Destroys the expression manager. No will be deallocated at this point, so
* any expression references that used to be managed by this expression
* manager and are left-over are bad.
*/
~ExprManager();
/** Get the type for booleans. */
const BooleanType* booleanType();
/** Get the type for sorts. */
const KindType* kindType();
/**
* Make a unary expression of a given kind (TRUE, FALSE,...).
* @param kind the kind of expression
* @return the expression
*/
Expr mkExpr(Kind kind);
/**
* Make a unary expression of a given kind (NOT, BVNOT, ...).
* @param kind the kind of expression
* @return the expression
*/
Expr mkExpr(Kind kind, const Expr& child1);
/**
* Make a binary expression of a given kind (AND, PLUS, ...).
* @param kind the kind of expression
* @param child1 the first child of the new expression
* @param child2 the second child of the new expression
* @return the expression
*/
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3);
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4);
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4, const Expr& child5);
/**
* Make an n-ary expression of given kind given a vector of it's children
* @param kind the kind of expression to build
* @param children the subexpressions
* @return the n-ary expression
*/
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
/** Make a function type from domain to range. */
const FunctionType*
mkFunctionType(const Type* domain,
const Type* range);
/** Make a function type with input types from argTypes. */
const FunctionType*
mkFunctionType(const std::vector<const Type*>& argTypes,
const Type* range);
/** Make a new sort with the given name. */
const Type* mkSort(std::string name);
// variables are special, because duplicates are permitted
Expr mkVar(const Type* type, std::string name);
Expr mkVar(const Type* type);
private:
/** The internal node manager */
NodeManager* d_nodeManager;
/**
* Returns the internal node manager. This should only be used by internal
* users, i.e. the friend classes.
*/
NodeManager* getNodeManager() const;
/** SmtEngine will use all the internals, so it will grab the node manager */
friend class SmtEngine;
/** ExprManagerScope reaches in to get the NodeManager */
friend class ExprManagerScope;
};
}/* CVC4 namespace */
#include "expr/expr.h"
namespace CVC4 {
/**
* A wrapper (essentially) for NodeManagerScope. Without this, we'd
* need Expr to be a friend of ExprManager.
*/
class ExprManagerScope {
NodeManagerScope d_nms;
public:
inline ExprManagerScope(const Expr& e) :
d_nms(e.getExprManager() == NULL ?
NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
}
};
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_MANAGER_H */
|
