diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-28 21:12:02 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-28 21:12:02 +0000 |
commit | d2ff1974a7cd87d841e1bcaeb0d93665f70d9259 (patch) | |
tree | 6f35a4d1f191739fe9f1c2c237f6ede3ed5c99ab /src/expr/expr_manager_template.h | |
parent | c39254b98c010397fa5b2da9513d7b3451d682d7 (diff) |
Changing NodeBuilder::debugCheckType() to maybeCheckType()
Changing NodeManager/ExprManager constructors to take 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 |