1 /********************* */
3 ** Original author: dejan
4 ** Major contributors: mdeters
5 ** Minor contributors (to current version): taking
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** Public-facing expression manager interface.
16 #ifndef __CVC4__EXPR_MANAGER_H
17 #define __CVC4__EXPR_MANAGER_H
19 #include "cvc4_config.h"
20 #include "expr/kind.h"
29 class CVC4_PUBLIC ExprManager
{
34 * Creates an expression manager.
39 * Destroys the expression manager. No will be deallocated at this point, so
40 * any expression references that used to be managed by this expression
41 * manager and are left-over are bad.
46 * Make a unary expression of a given kind (TRUE, FALSE,...).
47 * @param kind the kind of expression
48 * @return the expression
50 Expr
mkExpr(Kind kind
);
53 * Make a unary expression of a given kind (NOT, BVNOT, ...).
54 * @param kind the kind of expression
55 * @return the expression
57 Expr
mkExpr(Kind kind
, const Expr
& child1
);
60 * Make a binary expression of a given kind (AND, PLUS, ...).
61 * @param kind the kind of expression
62 * @param child1 the first child of the new expression
63 * @param child2 the second child of the new expression
64 * @return the expression
66 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
);
68 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
70 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
71 const Expr
& child3
, const Expr
& child4
);
72 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
73 const Expr
& child3
, const Expr
& child4
, const Expr
& child5
);
76 * Make an n-ary expression of given kind given a vector of it's children
77 * @param kind the kind of expression to build
78 * @param children the subexpressions
79 * @return the n-ary expression
81 Expr
mkExpr(Kind kind
, const std::vector
<Expr
>& children
);
83 // variables are special, because duplicates are permitted
88 /** The internal node manager */
92 * Returns the internal node manager. This should only be used by internal
93 * users, i.e. the friend classes.
95 NodeManager
* getNodeManager() const;
97 /** SmtEngine will use all the internals, so it will grab the node manager */
98 friend class SmtEngine
;
103 #endif /* __CVC4__EXPR_MANAGER_H */