From: Morgan Deters Date: Thu, 7 Feb 2013 20:28:20 +0000 (-0500) Subject: Make --default-dag-thresh apply to stringstreams X-Git-Tag: cvc5-1.0.0~7391^2~12 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6c20b80eb836a3b44f15835f91d6d1d7af342df;p=cvc5.git Make --default-dag-thresh apply to stringstreams --- diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 442d29ac9..a52bc00ac 100644 --- 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(l - 1); } diff --git a/src/expr/options b/src/expr/options index cd59e4875..223189d1b 100644 --- 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 7a1d73c36..57c4d1aa4 100644 --- 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."); }