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
|
/********************* */
/** expr_manager.h
** Original author: dejan
** Major contributors: 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 <vector>
namespace CVC4 {
class Expr;
class Type;
class BooleanType;
class FunctionType;
class KindType;
class NodeManager;
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_nm;
/**
* 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;
};
}
#endif /* __CVC4__EXPR_MANAGER_H */
|
