diff options
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 457713597..21526809e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -40,6 +40,7 @@ namespace CVC4 { class Expr; class SmtEngine; class NodeManager; +class Options; namespace context { class Context; @@ -80,12 +81,17 @@ private: public: /** + * Creates an expression manager with default options. + */ + ExprManager(); + + /** * Creates an expression manager. - * @param earlyTypeChecking whether to do type checking early (at Expr - * creation time); only used in debug builds---for other builds, type - * checking is never done early. + * + * @param options the earlyTypeChecking field is used to configure + * whether to do at Expr creation time. */ - explicit ExprManager(bool earlyTypeChecking = true); + explicit ExprManager(const Options&); /** * Destroys the expression manager. No will be deallocated at this point, so |