Make --default-dag-thresh apply to stringstreams

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 442d29ac9781203206da2d328a519990ddf2efaf..a52bc00ac631f331aa1fa0ecc681d2e57250d759 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -654,6 +654,11 @@ public:
         l = options::defaultExprDepth();
       }
       if(l == 0) {
+        // if called from outside the library, we may not have options
+        // available to us at this point (or perhaps the output language
+        // is not set in Options).  Default to something reasonable, but
+        // don't set "l" since that would make it "sticky" for this
+        // stream.
         return s_defaultPrintDepth;
       }
     }
@@ -797,7 +802,17 @@ public:
     if(l == 0) {
       // set the default dag setting on this ostream
       // (offset by one to detect whether default has been set yet)
-      l = s_defaultDag + 1;
+      if(&Options::current() != NULL) {
+        l = options::defaultDagThresh() + 1;
+      }
+      if(l == 0) {
+        // if called from outside the library, we may not have options
+        // available to us at this point (or perhaps the output language
+        // is not set in Options).  Default to something reasonable, but
+        // don't set "l" since that would make it "sticky" for this
+        // stream.
+        return s_defaultDag + 1;
+      }
     }
     return static_cast<size_t>(l - 1);
   }

diff --git a/src/expr/options b/src/expr/options
index cd59e487578c8f4eb2b57699453875eaf9778aaa..223189d1b3b1ec429ee2811d7b90103403819d27 100644 (file)
--- a/src/expr/options
+++ b/src/expr/options
@@ -5,9 +5,9 @@
 
 module EXPR "expr/options.h" Expression package
 
-option defaultExprDepth --default-expr-depth=N int :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
+option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
  print exprs to depth N (0 == default, -1 == no limit)
-option - default-dag-thresh --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-include "expr/options_handlers.h"
+option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h"
  dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
 option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h"
  print types with variables when printing exprs

diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h
index 7a1d73c366c6f164c926ed3955bce03dbd4b6a2a..57c4d1aa4fd9f4ac0c9b98d854de2254237ebc5a 100644 (file)
--- a/src/expr/options_handlers.h
+++ b/src/expr/options_handlers.h
@@ -39,8 +39,7 @@ inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) {
   // intentionally exclude Dump stream from this list
 }
 
-inline void setDefaultDagThresh(std::string option, std::string optarg, SmtEngine* smt) {
-  int dag = atoi(optarg.c_str());
+inline void setDefaultDagThresh(std::string option, int dag, SmtEngine* smt) {
   if(dag < 0) {
     throw OptionException("--default-dag-thresh requires a nonnegative argument.");
   }