diff options
Diffstat (limited to 'src/expr/expr_manager.h')
-rw-r--r-- | src/expr/expr_manager.h | 29 |
1 files changed, 26 insertions, 3 deletions
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 32aa41dfe..41766d64b 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -23,6 +23,10 @@ namespace CVC4 { class Expr; +class Type; +class BooleanType; +class FunctionType; +class KindType; class NodeManager; class SmtEngine; @@ -42,6 +46,11 @@ public: */ ~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 @@ -80,14 +89,28 @@ public: */ 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(); + Expr mkVar(const Type* type); private: - /** The internal node manager */ NodeManager* d_nm; - + BooleanType* d_booleanType; + KindType* d_kindType; + /** * Returns the internal node manager. This should only be used by internal * users, i.e. the friend classes. |