summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am4
-rw-r--r--src/expr/command.cpp10
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_manager_template.h4
-rw-r--r--src/expr/expr_template.h10
-rw-r--r--src/expr/node_builder.h4
-rw-r--r--src/expr/node_manager.cpp10
-rw-r--r--src/expr/node_manager.h16
-rw-r--r--src/expr/node_value.cpp8
-rw-r--r--src/expr/options25
-rw-r--r--src/expr/options_handlers.h72
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback