summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r--src/expr/expr_manager_template.h14
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback