Changing NodeBuilder::debugCheckType() to maybeCheckType()

Changing NodeManager/ExprManager constructors to take Options

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