2 files changed, 30 insertions, 27 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f2c45eab9..c1d49d8c8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -26,11 +26,8 @@
 #include <utility>
 #include <vector>
 
-#include "options/boolean_term_conversion_mode.h"
-#include "options/decision_mode.h"
 #include "base/exception.h"
 #include "base/modal_exception.h"
-#include "options/option_exception.h"
 #include "base/output.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
@@ -46,12 +43,16 @@
 #include "expr/resource_manager.h"
 #include "options/arith_options.h"
 #include "options/arrays_options.h"
+#include "options/base_options.h"
+#include "options/boolean_term_conversion_mode.h"
 #include "options/booleans_options.h"
 #include "options/booleans_options.h"
 #include "options/bv_options.h"
 #include "options/datatypes_options.h"
+#include "options/decision_mode.h"
 #include "options/decision_options.h"
 #include "options/main_options.h"
+#include "options/option_exception.h"
 #include "options/options_handler_interface.h"
 #include "options/printer_options.h"
 #include "options/prop_options.h"
@@ -65,8 +66,8 @@
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
 #include "proof/proof_manager.h"
-#include "proof/unsat_core.h"
 #include "proof/theory_proof.h"
+#include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
 #include "smt/boolean_terms.h"
 #include "smt/command_list.h"
@@ -74,8 +75,8 @@
 #include "smt/model_postprocessor.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_options_handler.h"
-#include "smt_util/command.h"
 #include "smt_util/boolean_simplification.h"
+#include "smt_util/command.h"
 #include "smt_util/ite_removal.h"
 #include "smt_util/nary_builder.h"
 #include "smt_util/node_visitor.h"
diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp
index 371cdcddd..e1a19d48b 100644
--- a/src/smt/smt_options_handler.cpp
+++ b/src/smt/smt_options_handler.cpp
@@ -25,6 +25,7 @@
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "cvc4autoconfig.h"
+#include "expr/expr_iomanip.h"
 #include "expr/metakind.h"
 #include "expr/node_manager.h"
 #include "expr/resource_manager.h"
@@ -32,6 +33,7 @@
 #include "options/arith_heuristic_pivot_rule.h"
 #include "options/arith_propagation_mode.h"
 #include "options/arith_unate_lemma_mode.h"
+#include "options/base_options.h"
 #include "options/boolean_term_conversion_mode.h"
 #include "options/bv_bitblast_mode.h"
 #include "options/bv_options.h"
@@ -1219,9 +1221,9 @@ void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw(
     bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
     OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \
     __channel_set; \
-    __channel_get << Expr::dag(dagSetting); \
-    __channel_get << Expr::setdepth(exprDepthSetting); \
-    __channel_get << Expr::printtypes(printtypesSetting); \
+    __channel_get << expr::ExprDag(dagSetting);      \
+    __channel_get << expr::ExprSetDepth(exprDepthSetting); \
+    __channel_get << expr::ExprPrintTypes(printtypesSetting); \
     __channel_get << language::SetLanguage(languageSetting); \
   }
 
@@ -1418,12 +1420,12 @@ void SmtOptionsHandler::setDefaultExprDepth(std::string option, int depth) {
     throw OptionException("--default-expr-depth requires a positive argument, or -1.");
   }
 
-  Debug.getStream() << Expr::setdepth(depth);
-  Trace.getStream() << Expr::setdepth(depth);
-  Notice.getStream() << Expr::setdepth(depth);
-  Chat.getStream() << Expr::setdepth(depth);
-  Message.getStream() << Expr::setdepth(depth);
-  Warning.getStream() << Expr::setdepth(depth);
+  Debug.getStream() << expr::ExprSetDepth(depth);
+  Trace.getStream() << expr::ExprSetDepth(depth);
+  Notice.getStream() << expr::ExprSetDepth(depth);
+  Chat.getStream() << expr::ExprSetDepth(depth);
+  Message.getStream() << expr::ExprSetDepth(depth);
+  Warning.getStream() << expr::ExprSetDepth(depth);
   // intentionally exclude Dump stream from this list
 }
 
@@ -1432,22 +1434,22 @@ void SmtOptionsHandler::setDefaultDagThresh(std::string option, int dag) {
     throw OptionException("--default-dag-thresh requires a nonnegative argument.");
   }
 
-  Debug.getStream() << Expr::dag(dag);
-  Trace.getStream() << Expr::dag(dag);
-  Notice.getStream() << Expr::dag(dag);
-  Chat.getStream() << Expr::dag(dag);
-  Message.getStream() << Expr::dag(dag);
-  Warning.getStream() << Expr::dag(dag);
-  Dump.getStream() << Expr::dag(dag);
+  Debug.getStream() << expr::ExprDag(dag);
+  Trace.getStream() << expr::ExprDag(dag);
+  Notice.getStream() << expr::ExprDag(dag);
+  Chat.getStream() << expr::ExprDag(dag);
+  Message.getStream() << expr::ExprDag(dag);
+  Warning.getStream() << expr::ExprDag(dag);
+  Dump.getStream() << expr::ExprDag(dag);
 }
 
 void SmtOptionsHandler::setPrintExprTypes(std::string option) {
-  Debug.getStream() << Expr::printtypes(true);
-  Trace.getStream() << Expr::printtypes(true);
-  Notice.getStream() << Expr::printtypes(true);
-  Chat.getStream() << Expr::printtypes(true);
-  Message.getStream() << Expr::printtypes(true);
-  Warning.getStream() << Expr::printtypes(true);
+  Debug.getStream() << expr::ExprPrintTypes(true);
+  Trace.getStream() << expr::ExprPrintTypes(true);
+  Notice.getStream() << expr::ExprPrintTypes(true);
+  Chat.getStream() << expr::ExprPrintTypes(true);
+  Message.getStream() << expr::ExprPrintTypes(true);
+  Warning.getStream() << expr::ExprPrintTypes(true);
   // intentionally exclude Dump stream from this list
 }