diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 4 | ||||
-rw-r--r-- | src/expr/command.cpp | 10 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 4 | ||||
-rw-r--r-- | src/expr/expr_template.h | 10 | ||||
-rw-r--r-- | src/expr/node_builder.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 10 | ||||
-rw-r--r-- | src/expr/node_manager.h | 16 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 8 | ||||
-rw-r--r-- | src/expr/options | 25 | ||||
-rw-r--r-- | src/expr/options_handlers.h | 72 |
11 files changed, 138 insertions, 29 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 6baa4613f..38cb8250c 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -56,6 +56,7 @@ EXTRA_DIST = \ expr_template.h \ expr_template.cpp \ type_checker_template.cpp \ + options_handlers.h \ mkkind \ mkmetakind \ mkexpr \ @@ -154,3 +155,6 @@ type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/theory/.su $< \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) + +.PHONY: builts +builts: $(BUILT_SOURCES) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 12830a618..c127aca75 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -902,7 +902,7 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { stringstream ss; ss << d_status; SExpr status = ss.str(); - smtEngine->setInfo(":status", status); + smtEngine->setInfo("status", status); d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -1074,7 +1074,13 @@ std::string GetOptionCommand::getFlag() const throw() { void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { try { - d_result = smtEngine->getOption(d_flag).getValue(); + vector<SExpr> v; + v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); + v.push_back(smtEngine->getOption(d_flag)); + stringstream ss; + + ss << SExpr(v); + d_result = ss.str(); d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { d_commandStatus = new CommandUnsupported(); diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 25578399f..a8491c937 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -20,7 +20,7 @@ #include "expr/expr_manager.h" #include "expr/variable_type_map.h" #include "context/context.h" -#include "util/options.h" +#include "options/options.h" #include "util/stats.h" #include <map> @@ -126,7 +126,7 @@ ExprManager::~ExprManager() throw() { } } -const Options* ExprManager::getOptions() const { +const Options& ExprManager::getOptions() const { return d_nodeManager->getOptions(); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index fdc1e1159..b762da3ea 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -42,7 +42,7 @@ namespace CVC4 { class Expr; class SmtEngine; class NodeManager; -struct Options; +class Options; class IntStat; class ExprManagerMapCollection; @@ -124,7 +124,7 @@ public: ~ExprManager() throw(); /** Get this node manager's options */ - const Options* getOptions() const; + const Options& getOptions() const; /** Get the type for booleans */ BooleanType booleanType() const; diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index dc82daec4..a2e861118 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -36,7 +36,7 @@ ${includes} #include "util/exception.h" #include "util/language.h" #include "util/hash.h" -#include "util/options.h" +#include "expr/options.h" // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the @@ -683,8 +683,8 @@ public: long& l = out.iword(s_iosIndex); if(l == 0) { // set the default print depth on this ostream - if(Options::current() != NULL) { - l = Options::current()->defaultExprDepth; + if(&Options::current() != NULL) { + l = options::defaultExprDepth(); } if(l == 0) { l = s_defaultPrintDepth; @@ -909,8 +909,8 @@ public: if(l == 0) { // set the default language on this ostream // (offset by one to detect whether default has been set yet) - if(Options::current() != NULL) { - l = Options::current()->outputLanguage + 1; + if(&Options::current() != NULL) { + l = options::outputLanguage() + 1; } if(l <= 0 || l > language::output::LANG_MAX) { // if called from outside the library, we may not have options diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index fcb503d37..fa9b1c011 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -742,7 +742,7 @@ public: #include "expr/node.h" #include "expr/node_manager.h" -#include "util/options.h" +#include "expr/options.h" namespace CVC4 { @@ -1301,7 +1301,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const throw(TypeCheckingExceptionPrivate, AssertionException) { /* force an immediate type check, if early type checking is enabled and the current node isn't a variable or constant */ - if( d_nm->getOptions()->earlyTypeChecking ) { + if( d_nm->getOptions()[options::earlyTypeChecking] ) { kind::MetaKind mk = n.getMetaKind(); if( mk != kind::metakind::VARIABLE && mk != kind::metakind::CONSTANT ) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 1abcf398b..fc2eec774 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -21,7 +21,7 @@ #include "expr/node_manager.h" #include "util/Assert.h" -#include "util/options.h" +#include "options/options.h" #include "util/stats.h" #include "util/tls.h" @@ -82,7 +82,7 @@ struct NVReclaim { NodeManager::NodeManager(context::Context* ctxt, ExprManager* exprManager) : - d_options(), + d_options(new Options()), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), d_attrManager(ctxt), @@ -92,11 +92,10 @@ NodeManager::NodeManager(context::Context* ctxt, init(); } - NodeManager::NodeManager(context::Context* ctxt, ExprManager* exprManager, const Options& options) : - d_options(options), + d_options(new Options(options)), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), d_attrManager(ctxt), @@ -154,6 +153,7 @@ NodeManager::~NodeManager() { } delete d_statisticsRegistry; + delete d_options; } void NodeManager::reclaimZombies() { @@ -253,7 +253,7 @@ TypeNode NodeManager::getType(TNode n, bool check) Debug("getType") << "getting type for " << n << std::endl; - if(needsCheck && !d_options.earlyTypeChecking) { + if(needsCheck && !(*d_options)[options::earlyTypeChecking]) { /* Iterate and compute the children bottom up. This avoids stack overflows in computeType() when the Node graph is really deep, which should only affect us when we're type checking lazily. */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6c34eb4a3..501a0f4fd 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -41,7 +41,7 @@ #include "util/subrange_bound.h" #include "util/configuration_private.h" #include "util/tls.h" -#include "util/options.h" +#include "options/options.h" namespace CVC4 { @@ -83,7 +83,7 @@ class NodeManager { static CVC4_THREADLOCAL(NodeManager*) s_current; - Options d_options; + Options* d_options; StatisticsRegistry* d_statisticsRegistry; NodeValuePool d_nodeValuePool; @@ -267,13 +267,13 @@ public: static NodeManager* currentNM() { return s_current; } /** Get this node manager's options (const version) */ - const Options* getOptions() const { - return &d_options; + const Options& getOptions() const { + return *d_options; } /** Get this node manager's options (non-const version) */ - Options* getOptions() { - return &d_options; + Options& getOptions() { + return *d_options; } /** Get this node manager's statistics registry */ @@ -791,14 +791,14 @@ public: // Expr is destructed, there's no active node manager. //Assert(nm != NULL); NodeManager::s_current = nm; - Options::s_current = nm ? &nm->d_options : NULL; + Options::s_current = nm ? nm->d_options : NULL; Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; - Options::s_current = d_oldNodeManager ? &d_oldNodeManager->d_options : NULL; + Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; Debug("current") << "node manager scope: " << "returning to " << NodeManager::s_current << "\n"; } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index dbf706c45..587f3873b 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -25,6 +25,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "util/language.h" +#include "options/options.h" #include "printer/printer.h" #include <sstream> @@ -37,11 +38,12 @@ NodeValue NodeValue::s_null(0); string NodeValue::toString() const { stringstream ss; - OutputLanguage outputLanguage = (this == &s_null) ? language::output::LANG_AST : Options::current()->outputLanguage; + + OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AST : options::outputLanguage(); toStream(ss, -1, false, - outputLanguage == language::output::LANG_AUTO ? + outlang == language::output::LANG_AUTO ? language::output::LANG_AST : - outputLanguage); + outlang); return ss.str(); } diff --git a/src/expr/options b/src/expr/options new file mode 100644 index 000000000..24810962e --- /dev/null +++ b/src/expr/options @@ -0,0 +1,25 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module EXPR "expr/options.h" Expression package + +option defaultExprDepth --default-expr-depth=N int :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h" + print exprs to depth N (0 == default, -1 == no limit) +option - --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-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 + +option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :default USE_EARLY_TYPE_CHECKING_BY_DEFAULT + type check expressions immediately on creation (debug builds only) +/type check expressions only when necessary (default) + +# --no-type-checking will override any --early-type-checking or --lazy-type-checking option +# --lazy-type-checking is linked because earlyTypeChecking should be set false too +option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking + never type check expressions + +endmodule + diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h new file mode 100644 index 000000000..a17445188 --- /dev/null +++ b/src/expr/options_handlers.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Custom handlers and predicates for expression package options + ** + ** Custom handlers and predicates for expression package options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EXPR__OPTIONS_HANDLERS_H +#define __CVC4__EXPR__OPTIONS_HANDLERS_H + +#include "util/output.h" +#include "util/dump.h" + +namespace CVC4 { +namespace expr { + +inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) { + if(depth < -1) { + 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); + // intentionally exclude Dump stream from this list +} + +inline void setDefaultDagThresh(std::string option, std::string optarg, SmtEngine* smt) { + int dag = atoi(optarg.c_str()); + if(dag < 0) { + 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); +} + +inline void setPrintExprTypes(std::string option, SmtEngine* smt) { + 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); + // intentionally exclude Dump stream from this list +} + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__OPTIONS_HANDLERS_H */ |