4 * Created on: Dec 10, 2009
8 #ifndef __CVC4__EXPR_MANAGER_H
9 #define __CVC4__EXPR_MANAGER_H
11 #include "cvc4_config.h"
12 #include "expr/kind.h"
21 class CVC4_PUBLIC ExprManager
{
26 * Creates an expressio manager.
31 * Destroys the expression manager. No will be deallocated at this point, so
32 * any expression references that used to be managed by this expression
33 * manager and are left-over are bad.
38 * Make a unary expression of a given kind (TRUE, FALSE,...).
39 * @param kind the kind of expression
40 * @return the expression
42 Expr
mkExpr(Kind kind
);
45 * Make a unary expression of a given kind (NOT, BVNOT, ...).
46 * @param kind the kind of expression
47 * @return the expression
49 Expr
mkExpr(Kind kind
, const Expr
& child1
);
52 * Make a ternary expression of a given kind (AND, PLUS, ...).
53 * @param kind the kind of expression
54 * @return the expression
56 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
);
58 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
60 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
61 const Expr
& child3
, const Expr
& child4
);
62 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
63 const Expr
& child3
, const Expr
& child4
, const Expr
& child5
);
66 * Make an n-ary expression of given kind given a vector of it's children
67 * @param kind the kind of expression to build
68 * @param children the subexpressions
69 * @return the n-ary expression
71 Expr
mkExpr(Kind kind
, const std::vector
<Expr
>& children
);
73 // variables are special, because duplicates are permitted
78 /** The internal node manager */
82 * Returns the internal node manager. This should only be used by internal
83 * users, i.e. the friend classes.
85 NodeManager
* getNodeManager() const;
87 /** SmtEngine will use all the internals, so it will grab the node manager */
88 friend class SmtEngine
;
93 #endif /* __CVC4__EXPR_MANAGER_H */