summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/Makefile.am9
-rw-r--r--src/smt/options81
-rw-r--r--src/smt/options_handlers.h251
-rw-r--r--src/smt/simplification_mode.cpp42
-rw-r--r--src/smt/simplification_mode.h43
-rw-r--r--src/smt/smt_engine.cpp308
-rw-r--r--src/smt/smt_engine.h23
-rw-r--r--src/smt/smt_options_template.cpp78
8 files changed, 641 insertions, 194 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 5cc0cedd1..9cc236a13 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -12,9 +12,16 @@ libsmt_la_SOURCES = \
smt_engine_scope.h \
modal_exception.h \
bad_option_exception.h \
- no_such_function_exception.h
+ no_such_function_exception.h \
+ simplification_mode.h \
+ simplification_mode.cpp
+
+nodist_libsmt_la_SOURCES = \
+ smt_options.cpp
EXTRA_DIST = \
+ options_handlers.h \
+ smt_options_template.cpp \
bad_option_exception.i \
no_such_function_exception.i \
modal_exception.i \
diff --git a/src/smt/options b/src/smt/options
new file mode 100644
index 000000000..5ee65e50a
--- /dev/null
+++ b/src/smt/options
@@ -0,0 +1,81 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+# FIXME: need to add support for SMT-LIBv2-required options:
+#
+# expand-definitions
+# regular-output-channel
+# diagnostic-output-channel
+# produce-unsat-cores
+#
+
+module SMT "smt/options.h" SMT layer
+
+common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
+ dump preprocessed assertions, etc., see --dump=help
+common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
+ all dumping goes to FILE (instead of stdout)
+
+expert-option lazyDefinitionExpansion --lazy-definition-expansion bool
+ expand define-funs/LAMBDAs lazily
+
+option simplificationMode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
+ choose simplification mode, see --simplification=help
+alias --no-simplification = --simplification=none
+ turn off all simplification (same as --simplification=none)
+
+option doStaticLearning static-learning /--no-static-learning bool :default true
+ use static learning (on by default)
+/turn off static learning (e.g. diamond-breaking)
+
+common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
+ support the get-value and get-model commands
+common-option produceAssignments produce-assignments --produce-assignments bool
+ support the get-assignment command
+
+# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
+# is a mode in which the assertion list must be kept. So it belongs here.
+common-option interactive interactive-mode --interactive bool :read-write
+ force interactive mode
+
+option doITESimp --ite-simp bool :read-write
+ turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
+/turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)
+
+option unconstrainedSimp --unconstrained-simp bool :default false :read-write
+ turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
+/turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
+
+option repeatSimp --repeat-simp bool :read-write
+ make multiple passes with nonclausal simplifier
+/do not make multiple passes with nonclausal simplifier
+
+common-option incrementalSolving incremental -i --incremental bool
+ enable incremental solving
+
+common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long"
+ enable time limiting (give milliseconds)
+common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long"
+ enable time limiting per query (give milliseconds)
+common-option cumulativeResourceLimit --rlimit=N "unsigned long"
+ enable resource limiting
+common-option perCallResourceLimit --rlimit-per=N "unsigned long"
+ enable resource limiting per query
+
+option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
+ replay decisions from file
+option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
+ log decisions and propagations to file
+option replayStream ExprStream*
+
+# portfolio options
+option threads --threads=N unsigned :default 2
+ Total number of threads
+option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h"
+ The input channel to receive notfication events for new lemmas
+option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
+ The output channel to receive notfication events for new lemmas
+
+endmodule
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
new file mode 100644
index 000000000..f111f512b
--- /dev/null
+++ b/src/smt/options_handlers.h
@@ -0,0 +1,251 @@
+/********************* */
+/*! \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 SmtEngine options
+ **
+ ** Custom handlers and predicates for SmtEngine options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__SMT__OPTIONS_HANDLERS_H
+#define __CVC4__SMT__OPTIONS_HANDLERS_H
+
+#include "util/dump.h"
+
+namespace CVC4 {
+namespace smt {
+
+static const std::string dumpHelp = "\
+Dump modes currently supported by the --dump option:\n\
+\n\
+benchmark\n\
++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
+ does not include any declarations or assertions. Implied by all following\n\
+ modes.\n\
+\n\
+declarations\n\
++ Dump declarations. Implied by all following modes.\n\
+\n\
+assertions\n\
++ Output the assertions after non-clausal simplification and static\n\
+ learning phases, but before presolve-time T-lemmas arrive. If\n\
+ non-clausal simplification and static learning are off\n\
+ (--simplification=none --no-static-learning), the output\n\
+ will closely resemble the input (with term-level ITEs removed).\n\
+\n\
+learned\n\
++ Output the assertions after non-clausal simplification, static\n\
+ learning, and presolve-time T-lemmas. This should include all eager\n\
+ T-lemmas (in the form provided by the theory, which my or may not be\n\
+ clausal). Also includes level-0 BCP done by Minisat.\n\
+\n\
+clauses\n\
++ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+ output\n\
+\n\
+state\n\
++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
+ Implied by all \"stateful\" modes below and conflicts with all\n\
+ non-stateful modes below.\n\
+\n\
+t-conflicts [non-stateful]\n\
++ Output correctness queries for all theory conflicts\n\
+\n\
+missed-t-conflicts [stateful]\n\
++ Output completeness queries for theory conflicts\n\
+\n\
+t-propagations [stateful]\n\
++ Output correctness queries for all theory propagations\n\
+\n\
+missed-t-propagations [stateful]\n\
++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
+\n\
+t-lemmas [non-stateful]\n\
++ Output correctness queries for all theory lemmas\n\
+\n\
+t-explanations [non-stateful]\n\
++ Output correctness queries for all theory explanations\n\
+\n\
+bv-rewrites [non-stateful]\n\
++ Output correctness queries for all bitvector rewrites\n\
+\n\
+theory::fullcheck [non-stateful]\n\
++ Output completeness queries for all full-check effort-level theory checks\n\
+\n\
+Dump modes can be combined with multiple uses of --dump. Generally you want\n\
+one from the assertions category (either assertions, learned, or clauses), and\n\
+perhaps one or more stateful or non-stateful modes for checking correctness\n\
+and completeness of decision procedure implementations. Stateful modes dump\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
+\n\
+The --output-language option controls the language used for dumping, and\n\
+this allows you to connect CVC4 to another solver implementation via a UNIX\n\
+pipe to perform on-line checking. The --dump-to option can be used to dump\n\
+to a file.\n\
+";
+
+static const std::string simplificationHelp = "\
+Simplification modes currently supported by the --simplification option:\n\
+\n\
+batch (default) \n\
++ save up all ASSERTions; run nonclausal simplification and clausal\n\
+ (MiniSat) propagation for all of them only after reaching a querying command\n\
+ (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
+\n\
+incremental\n\
++ run nonclausal simplification and clausal propagation at each ASSERT\n\
+ (and at CHECKSAT/QUERY/SUBTYPE)\n\
+\n\
+none\n\
++ do not perform nonclausal simplification\n\
+";
+
+inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_DUMPING
+ char* optargPtr = strdup(optarg.c_str());
+ char* tokstr = optargPtr;
+ char* toksave;
+ while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
+ tokstr = NULL;
+ if(!strcmp(optargPtr, "benchmark")) {
+ } else if(!strcmp(optargPtr, "declarations")) {
+ } else if(!strcmp(optargPtr, "assertions")) {
+ } else if(!strcmp(optargPtr, "learned")) {
+ } else if(!strcmp(optargPtr, "clauses")) {
+ } else if(!strcmp(optargPtr, "t-conflicts") ||
+ !strcmp(optargPtr, "t-lemmas") ||
+ !strcmp(optargPtr, "t-explanations") ||
+ !strcmp(optargPtr, "bv-rewrites") ||
+ !strcmp(optargPtr, "theory::fullcheck")) {
+ // These are "non-state-dumping" modes. If state (SAT decisions,
+ // propagations, etc.) is dumped, it will interfere with the validity
+ // of these generated queries.
+ if(Dump.isOn("state")) {
+ throw OptionException(std::string("dump option `") + optargPtr +
+ "' conflicts with a previous, "
+ "state-dumping dump option. You cannot "
+ "mix stateful and non-stateful dumping modes; "
+ "see --dump help.");
+ } else {
+ Dump.on("no-permit-state");
+ }
+ } else if(!strcmp(optargPtr, "state") ||
+ !strcmp(optargPtr, "missed-t-conflicts") ||
+ !strcmp(optargPtr, "t-propagations") ||
+ !strcmp(optargPtr, "missed-t-propagations")) {
+ // These are "state-dumping" modes. If state (SAT decisions,
+ // propagations, etc.) is not dumped, it will interfere with the
+ // validity of these generated queries.
+ if(Dump.isOn("no-permit-state")) {
+ throw OptionException(std::string("dump option `") + optargPtr +
+ "' conflicts with a previous, "
+ "non-state-dumping dump option. You cannot "
+ "mix stateful and non-stateful dumping modes; "
+ "see --dump help.");
+ } else {
+ Dump.on("state");
+ }
+ } else if(!strcmp(optargPtr, "help")) {
+ puts(dumpHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --dump: `") +
+ optargPtr + "'. Try --dump help.");
+ }
+
+ Dump.on(optargPtr);
+ Dump.on("benchmark");
+ if(strcmp(optargPtr, "benchmark")) {
+ Dump.on("declarations");
+ }
+ }
+ free(optargPtr);
+#else /* CVC4_DUMPING */
+ throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_DUMPING
+ size_t dagSetting = expr::ExprDag::getDag(Dump.getStream());
+ if(optarg == "") {
+ throw OptionException(std::string("Bad file name for --dump-to"));
+ } else if(optarg == "-") {
+ Dump.setStream(DumpOutC::dump_cout);
+ } else {
+ std::ostream* dumpTo = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+ if(!*dumpTo) {
+ throw OptionException(std::string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
+ }
+ Dump.setStream(*dumpTo);
+ }
+ expr::ExprDag::setDag(Dump.getStream(), dagSetting);
+#else /* CVC4_DUMPING */
+ throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "batch") {
+ return SIMPLIFICATION_MODE_BATCH;
+ } else if(optarg == "incremental") {
+ return SIMPLIFICATION_MODE_INCREMENTAL;
+ } else if(optarg == "none") {
+ return SIMPLIFICATION_MODE_NONE;
+ } else if(optarg == "help") {
+ puts(simplificationHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --simplification: `") +
+ optarg + "'. Try --simplification help.");
+ }
+}
+
+inline std::string checkReplayFilename(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_REPLAY
+ if(optarg == "") {
+ throw OptionException(std::string("Bad file name for --replay"));
+ } else {
+ return optarg;
+ }
+#else /* CVC4_REPLAY */
+ throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+inline std::ostream* checkReplayLogFilename(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_REPLAY
+ if(optarg == "") {
+ throw OptionException(std::string("Bad file name for --replay-log"));
+ } else if(optarg == "-") {
+ return &std::cout;
+ } else {
+ std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+ if(!*replayLog) {
+ throw OptionException(std::string("Cannot open replay-log file: `") + optarg + "'");
+ }
+ return replayLog;
+ }
+#else /* CVC4_REPLAY */
+ throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__OPTIONS_HANDLERS_H */
diff --git a/src/smt/simplification_mode.cpp b/src/smt/simplification_mode.cpp
new file mode 100644
index 000000000..7bae74417
--- /dev/null
+++ b/src/smt/simplification_mode.cpp
@@ -0,0 +1,42 @@
+/********************* */
+/*! \file simplification_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "smt/simplification_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
+ switch(mode) {
+ case SIMPLIFICATION_MODE_INCREMENTAL:
+ out << "SIMPLIFICATION_MODE_INCREMENTAL";
+ break;
+ case SIMPLIFICATION_MODE_BATCH:
+ out << "SIMPLIFICATION_MODE_BATCH";
+ break;
+ case SIMPLIFICATION_MODE_NONE:
+ out << "SIMPLIFICATION_MODE_NONE";
+ break;
+ default:
+ out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/smt/simplification_mode.h b/src/smt/simplification_mode.h
new file mode 100644
index 000000000..6e0faafc0
--- /dev/null
+++ b/src/smt/simplification_mode.h
@@ -0,0 +1,43 @@
+/********************* */
+/*! \file simplification_mode.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-2012 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H
+#define __CVC4__SMT__SIMPLIFICATION_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+/** Enumeration of simplification modes (when to simplify). */
+typedef enum {
+ /** Simplify the assertions as they come in */
+ SIMPLIFICATION_MODE_INCREMENTAL,
+ /** Simplify the assertions all together once a check is requested */
+ SIMPLIFICATION_MODE_BATCH,
+ /** Don't do simplification */
+ SIMPLIFICATION_MODE_NONE
+} SimplificationMode;
+
+std::ostream& operator<<(std::ostream& out, SimplificationMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SIMPLIFICATION_MODE_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 81a212edd..0acc53693 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -22,12 +22,16 @@
#include <utility>
#include <sstream>
#include <stack>
+#include <cctype>
+#include <algorithm>
#include <ext/hash_map>
#include "context/cdlist.h"
#include "context/cdhashset.h"
#include "context/context.h"
#include "decision/decision_engine.h"
+#include "decision/decision_mode.h"
+#include "decision/options.h"
#include "expr/command.h"
#include "expr/expr.h"
#include "expr/kind.h"
@@ -45,12 +49,15 @@
#include "util/boolean_simplification.h"
#include "util/configuration.h"
#include "util/exception.h"
-#include "util/options.h"
+#include "smt/options.h"
#include "util/output.h"
#include "util/hash.h"
#include "theory/substitutions.h"
+#include "theory/uf/options.h"
+#include "theory/arith/options.h"
#include "theory/theory_traits.h"
#include "theory/logic_info.h"
+#include "theory/options.h"
#include "theory/booleans/circuit_propagator.h"
#include "util/ite_removal.h"
#include "theory/model.h"
@@ -309,24 +316,24 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
// cleanup ordering issue and Nodes/TNodes. If SAT is popped
// first, some user-context-dependent TNodes might still exist
// with rc == 0.
- if(Options::current()->interactive ||
- Options::current()->incrementalSolving) {
+ if(options::interactive() ||
+ options::incrementalSolving()) {
// In the case of incremental solving, we appear to need these to
// ensure the relevant Nodes remain live.
d_assertionList = new(true) AssertionList(d_userContext);
}
- if(Options::current()->perCallResourceLimit != 0) {
- setResourceLimit(Options::current()->perCallResourceLimit, false);
+ if(options::perCallResourceLimit() != 0) {
+ setResourceLimit(options::perCallResourceLimit(), false);
}
- if(Options::current()->cumulativeResourceLimit != 0) {
- setResourceLimit(Options::current()->cumulativeResourceLimit, true);
+ if(options::cumulativeResourceLimit() != 0) {
+ setResourceLimit(options::cumulativeResourceLimit(), true);
}
- if(Options::current()->perCallMillisecondLimit != 0) {
- setTimeLimit(Options::current()->perCallMillisecondLimit, false);
+ if(options::perCallMillisecondLimit() != 0) {
+ setTimeLimit(options::perCallMillisecondLimit(), false);
}
- if(Options::current()->cumulativeMillisecondLimit != 0) {
- setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
+ if(options::cumulativeMillisecondLimit() != 0) {
+ setTimeLimit(options::cumulativeMillisecondLimit(), true);
}
}
@@ -380,7 +387,7 @@ SmtEngine::~SmtEngine() throw() {
SmtScope smts(this);
try {
- while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) {
+ while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
internalPop();
}
@@ -456,28 +463,28 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
d_logic.lock();
// Set the options for the theoryOf
- if(!Options::current()->theoryOfModeSetByUser) {
+ if(!options::theoryOfMode.wasSetByUser()) {
if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
Theory::setTheoryOfMode(theory::THEORY_OF_TERM_BASED);
} else {
Theory::setTheoryOfMode(theory::THEORY_OF_TYPE_BASED);
}
} else {
- Theory::setTheoryOfMode(Options::current()->theoryOfMode);
+ Theory::setTheoryOfMode(options::theoryOfMode());
}
// by default, symmetry breaker is on only for QF_UF
- if(! Options::current()->ufSymmetryBreakerSetByUser) {
+ if(! options::ufSymmetryBreaker.wasSetByUser()) {
bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
- NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf;
+ options::ufSymmetryBreaker.set(qf_uf);
}
// by default, nonclausal simplification is off for QF_SAT and for quantifiers
- if(! Options::current()->simplificationModeSetByUser) {
+ if(! options::simplificationMode.wasSetByUser()) {
bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
bool quantifiers = d_logic.isQuantified();
Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << std::endl;
- NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat || quantifiers ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
+ options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
}
// If in arrays, set the UF handler to arrays
@@ -487,48 +494,48 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
Theory::setUninterpretedSortOwner(THEORY_UF);
}
// Turn on ite simplification for QF_LIA and QF_AUFBV
- if(! Options::current()->doITESimpSetByUser) {
+ if(! options::doITESimp.wasSetByUser()) {
bool iteSimp = !d_logic.isQuantified() &&
((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areRealsUsed()) ||
(d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)));
Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
- NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
+ options::doITESimp.set(iteSimp);
}
// Turn on multiple-pass non-clausal simplification for QF_AUFBV
- if(! Options::current()->repeatSimpSetByUser) {
+ if(! options::repeatSimp.wasSetByUser()) {
bool repeatSimp = !d_logic.isQuantified() &&
(d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV));
Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
- NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
+ options::repeatSimp.set(repeatSimp);
}
// Turn on unconstrained simplification for QF_AUFBV
- if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
+ if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) {
// bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
- // bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
- bool uncSimp = !Options::current()->incrementalSolving && !d_logic.isQuantified() &&
+ // bool uncSimp = false && !qf_sat && !options::incrementalSolving();
+ bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() &&
(d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
- NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
+ options::unconstrainedSimp.set(uncSimp);
}
// Turn on arith rewrite equalities only for pure arithmetic
- if(! Options::current()->arithRewriteEqSetByUser) {
+ if(! options::arithRewriteEq.wasSetByUser()) {
bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified();
Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
- NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
+ options::arithRewriteEq.set(arithRewriteEq);
}
- if(! Options::current()->arithHeuristicPivotsSetByUser){
+ if(! options::arithHeuristicPivots.wasSetByUser()) {
int16_t heuristicPivots = 5;
- if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
- if(d_logic.isDifferenceLogic()){
+ if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()) {
+ if(d_logic.isDifferenceLogic()) {
heuristicPivots = -1;
- }else if(!d_logic.areIntegersUsed()){
+ } else if(!d_logic.areIntegersUsed()) {
heuristicPivots = 0;
}
}
Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots << std::endl;
- NodeManager::currentNM()->getOptions()->arithHeuristicPivots = heuristicPivots;
+ options::arithHeuristicPivots.set(heuristicPivots);
}
- if(! Options::current()->arithPivotThresholdSetByUser){
+ if(! options::arithPivotThreshold.wasSetByUser()){
uint16_t pivotThreshold = 2;
if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
if(d_logic.isDifferenceLogic()){
@@ -536,24 +543,24 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
}
}
Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold << std::endl;
- NodeManager::currentNM()->getOptions()->arithPivotThreshold = pivotThreshold;
+ options::arithPivotThreshold.set(pivotThreshold);
}
- if(! Options::current()->arithStandardCheckVarOrderPivotsSetByUser){
+ if(! options::arithStandardCheckVarOrderPivots.wasSetByUser()){
int16_t varOrderPivots = -1;
if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
varOrderPivots = 200;
}
Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots << std::endl;
- NodeManager::currentNM()->getOptions()->arithStandardCheckVarOrderPivots = varOrderPivots;
+ options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
}
// Turn off early theory preprocessing if arithRewriteEq is on
- if (NodeManager::currentNM()->getOptions()->arithRewriteEq) {
+ if (options::arithRewriteEq()) {
d_earlyTheoryPP = false;
}
// Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
// and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers
- if(!Options::current()->decisionModeSetByUser) {
- Options::DecisionMode decMode =
+ if(!options::decisionMode.wasSetByUser()) {
+ decision::DecisionMode decMode =
//QF_BV
(not d_logic.isQuantified() &&
d_logic.isPure(THEORY_BV)
@@ -576,8 +583,8 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
) ||
// Quantifiers
d_logic.isQuantified()
- ? Options::DECISION_STRATEGY_JUSTIFICATION
- : Options::DECISION_STRATEGY_INTERNAL;
+ ? decision::DECISION_STRATEGY_JUSTIFICATION
+ : decision::DECISION_STRATEGY_INTERNAL;
bool stoponly =
// QF_AUFLIA
@@ -595,12 +602,12 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
? true : false;
Trace("smt") << "setting decision mode to " << decMode << std::endl;
- NodeManager::currentNM()->getOptions()->decisionMode = decMode;
- NodeManager::currentNM()->getOptions()->decisionOptions.stopOnly = stoponly;
+ options::decisionMode.set(decMode);
+ options::decisionStopOnly.set(stoponly);
}
}
-void SmtEngine::setInfo(const std::string& key, const SExpr& value)
+void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
throw(BadOptionException, ModalException) {
SmtScope smts(this);
@@ -636,15 +643,15 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
}
// Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
- if(key == ":name" ||
- key == ":source" ||
- key == ":category" ||
- key == ":difficulty" ||
- key == ":smt-lib-version" ||
- key == ":notes") {
+ if(key == "name" ||
+ key == "source" ||
+ key == "category" ||
+ key == "difficulty" ||
+ key == "smt-lib-version" ||
+ key == "notes") {
// ignore these
return;
- } else if(key == ":status") {
+ } else if(key == "status") {
string s;
if(value.isAtom()) {
s = value.getValue();
@@ -659,16 +666,24 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
throw BadOptionException();
}
-SExpr SmtEngine::getInfo(const std::string& key) const
+CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
throw(BadOptionException, ModalException) {
SmtScope smts(this);
Trace("smt") << "SMT getInfo(" << key << ")" << endl;
- if(key == ":all-statistics") {
+ if(key == "all-statistics") {
vector<SExpr> stats;
- for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin();
- i != StatisticsRegistry::end();
+ for(StatisticsRegistry::const_iterator i = d_exprManager->getStatisticsRegistry()->begin_();
+ i != d_exprManager->getStatisticsRegistry()->end_();
+ ++i) {
+ vector<SExpr> v;
+ v.push_back((*i)->getName());
+ v.push_back((*i)->getValue());
+ stats.push_back(v);
+ }
+ for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin_();
+ i != d_statisticsRegistry->end_();
++i) {
vector<SExpr> v;
v.push_back((*i)->getName());
@@ -676,21 +691,32 @@ SExpr SmtEngine::getInfo(const std::string& key) const
stats.push_back(v);
}
return stats;
- } else if(key == ":error-behavior") {
+ } else if(key == "error-behavior") {
+ // immediate-exit | continued-execution
return SExpr::Keyword("immediate-exit");
- } else if(key == ":name") {
+ } else if(key == "name") {
return Configuration::getName();
- } else if(key == ":version") {
+ } else if(key == "version") {
return Configuration::getVersionString();
- } else if(key == ":authors") {
+ } else if(key == "authors") {
return Configuration::about();
- } else if(key == ":status") {
- return d_status.asSatisfiabilityResult().toString();
- } else if(key == ":reason-unknown") {
+ } else if(key == "status") {
+ // sat | unsat | unknown
+ switch(d_status.asSatisfiabilityResult().isSat()) {
+ case Result::SAT:
+ return SExpr::Keyword("sat");
+ case Result::UNSAT:
+ return SExpr::Keyword("unsat");
+ default:
+ return SExpr::Keyword("unknown");
+ }
+ } else if(key == "reason-unknown") {
if(!d_status.isNull() && d_status.isUnknown()) {
stringstream ss;
ss << d_status.whyUnknown();
- return SExpr::Keyword(ss.str());
+ string s = ss.str();
+ transform(s.begin(), s.end(), s.begin(), ::tolower);
+ return SExpr::Keyword(s);
} else {
throw ModalException("Can't get-info :reason-unknown when the "
"last result wasn't unknown!");
@@ -700,98 +726,6 @@ SExpr SmtEngine::getInfo(const std::string& key) const
}
}
-void SmtEngine::setOption(const std::string& key, const SExpr& value)
- throw(BadOptionException, ModalException) {
-
- SmtScope smts(this);
-
- Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
- if(Dump.isOn("benchmark")) {
- Dump("benchmark") << SetOptionCommand(key, value);
- }
-
- if(key == ":print-success") {
- if(value.isAtom() && value.getValue() == "false") {
- *Options::current()->out << Command::printsuccess(false);
- } else if(value.isAtom() && value.getValue() == "true") {
- *Options::current()->out << Command::printsuccess(true);
- } else {
- throw BadOptionException();
- }
- } else if(key == ":expand-definitions") {
- throw BadOptionException();
- } else if(key == ":interactive-mode") {
- throw BadOptionException();
- } else if(key == ":regular-output-channel") {
- throw BadOptionException();
- } else if(key == ":diagnostic-output-channel") {
- throw BadOptionException();
- } else if(key == ":random-seed") {
- throw BadOptionException();
- } else if(key == ":verbosity") {
- throw BadOptionException();
- } else {
- // The following options can only be set at the beginning; we throw
- // a ModalException if someone tries.
- if(d_logic.isLocked()) {
- throw ModalException("logic already set; cannot set options");
- }
-
- if(key == ":produce-proofs") {
- throw BadOptionException();
- } else if(key == ":produce-unsat-cores") {
- throw BadOptionException();
- } else if(key == ":produce-models") {
- //throw BadOptionException();
- const_cast<Options*>( Options::s_current )->produceModels = true;
- } else if(key == ":produce-assignments") {
- throw BadOptionException();
- } else {
- throw BadOptionException();
- }
- }
-}
-
-SExpr SmtEngine::getOption(const std::string& key) const
- throw(BadOptionException) {
-
- SmtScope smts(this);
-
- Trace("smt") << "SMT getOption(" << key << ")" << endl;
- if(Dump.isOn("benchmark")) {
- Dump("benchmark") << GetOptionCommand(key);
- }
- if(key == ":print-success") {
- if(Command::printsuccess::getPrintSuccess(*Options::current()->out)) {
- return SExpr("true");
- } else {
- return SExpr("false");
- }
- } else if(key == ":expand-definitions") {
- throw BadOptionException();
- } else if(key == ":interactive-mode") {
- throw BadOptionException();
- } else if(key == ":produce-proofs") {
- throw BadOptionException();
- } else if(key == ":produce-unsat-cores") {
- throw BadOptionException();
- } else if(key == ":produce-models") {
- throw BadOptionException();
- } else if(key == ":produce-assignments") {
- throw BadOptionException();
- } else if(key == ":regular-output-channel") {
- return SExpr("stdout");
- } else if(key == ":diagnostic-output-channel") {
- return SExpr("stderr");
- } else if(key == ":random-seed") {
- throw BadOptionException();
- } else if(key == ":verbosity") {
- throw BadOptionException();
- } else {
- throw BadOptionException();
- }
-}
-
void SmtEngine::defineFunction(Expr func,
const std::vector<Expr>& formals,
Expr formula) {
@@ -805,7 +739,7 @@ void SmtEngine::defineFunction(Expr func,
SmtScope smts(this);
// type check body
- Type formulaType = formula.getType(Options::current()->typeChecking);
+ Type formulaType = formula.getType(options::typeChecking());
Type funcType = func.getType();
// We distinguish here between definitions of constants and functions,
@@ -1151,8 +1085,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd-1];
- if( Options::current()->incrementalSolving ||
- Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL ) {
+ if( options::incrementalSolving() ||
+ options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
// Keep substitutions
SubstitutionMap::iterator pos = d_lastSubstitutionPos;
if(pos == d_topLevelSubstitutions.end()) {
@@ -1306,7 +1240,7 @@ bool SmtEnginePrivate::simplifyAssertions()
Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
- if(Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
+ if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
// Perform non-clausal simplification
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< "performing non-clausal simplification" << endl;
@@ -1338,7 +1272,7 @@ bool SmtEnginePrivate::simplifyAssertions()
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
// ITE simplification
- if(Options::current()->doITESimp) {
+ if(options::doITESimp()) {
simpITE();
}
@@ -1347,7 +1281,7 @@ bool SmtEnginePrivate::simplifyAssertions()
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
// Unconstrained simplification
- if(Options::current()->unconstrainedSimp) {
+ if(options::unconstrainedSimp()) {
unconstrainedSimp();
}
@@ -1355,7 +1289,7 @@ bool SmtEnginePrivate::simplifyAssertions()
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
- if(Options::current()->repeatSimp && Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
+ if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< " doing repeated simplification" << std::endl;
d_assertionsToCheck.swap(d_assertionsToPreprocess);
@@ -1458,7 +1392,7 @@ void SmtEnginePrivate::processAssertions() {
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
- if(!Options::current()->lazyDefinitionExpansion) {
+ if(!options::lazyDefinitionExpansion()) {
Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime);
hash_map<TNode, Node, TNodeHashFunction> cache;
@@ -1480,7 +1414,7 @@ void SmtEnginePrivate::processAssertions() {
bool noConflict = simplifyAssertions();
- if(Options::current()->doStaticLearning) {
+ if(options::doStaticLearning()) {
// Perform static learning
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< "performing static learning" << endl;
@@ -1495,7 +1429,7 @@ void SmtEnginePrivate::processAssertions() {
d_smt.d_numAssertionsPost += d_assertionsToCheck.size();
}
- if(Options::current()->repeatSimp) {
+ if(options::repeatSimp()) {
d_assertionsToCheck.swap(d_assertionsToPreprocess);
noConflict &= simplifyAssertions();
if (noConflict) {
@@ -1583,13 +1517,13 @@ void SmtEnginePrivate::addFormula(TNode n)
d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
// If the mode of processing is incremental prepreocess and assert immediately
- if (Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL) {
+ if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) {
processAssertions();
}
}
void SmtEngine::ensureBoolean(const BoolExpr& e) {
- Type type = e.getType(Options::current()->typeChecking);
+ Type type = e.getType(options::typeChecking());
Type boolType = d_exprManager->booleanType();
if(type != boolType) {
stringstream ss;
@@ -1610,7 +1544,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
- if(d_queryMade && !Options::current()->incrementalSolving) {
+ if(d_queryMade && !options::incrementalSolving()) {
throw ModalException("Cannot make multiple queries unless "
"incremental solving is enabled "
"(try --incremental)");
@@ -1673,7 +1607,7 @@ Result SmtEngine::query(const BoolExpr& e) {
Trace("smt") << "SMT query(" << e << ")" << endl;
- if(d_queryMade && !Options::current()->incrementalSolving) {
+ if(d_queryMade && !options::incrementalSolving()) {
throw ModalException("Cannot make multiple queries unless "
"incremental solving is enabled "
"(try --incremental)");
@@ -1738,7 +1672,7 @@ Expr SmtEngine::simplify(const Expr& e) {
Assert(e.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
- if( Options::current()->typeChecking ) {
+ if( options::typeChecking() ) {
e.getType(true);// ensure expr is type-checked at this point
}
Trace("smt") << "SMT simplify(" << e << ")" << endl;
@@ -1754,13 +1688,13 @@ Expr SmtEngine::getValue(const Expr& e)
SmtScope smts(this);
// ensure expr is type-checked at this point
- Type type = e.getType(Options::current()->typeChecking);
+ Type type = e.getType(options::typeChecking());
Trace("smt") << "SMT getValue(" << e << ")" << endl;
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetValueCommand(e);
}
- if(!Options::current()->produceModels) {
+ if(!options::produceModels()) {
const char* msg =
"Cannot get value when produce-models options is off.";
throw ModalException(msg);
@@ -1799,7 +1733,7 @@ Expr SmtEngine::getValue(const Expr& e)
bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
SmtScope smts(this);
finalOptionsAreSet();
- Type type = e.getType(Options::current()->typeChecking);
+ Type type = e.getType(options::typeChecking());
// must be Boolean
CheckArgument( type.isBoolean(), e,
"expected Boolean-typed variable or function application "
@@ -1813,7 +1747,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
n.getMetaKind() == kind::metakind::VARIABLE ), e,
"expected variable or defined-function application "
"in addToAssignment(),\ngot %s", e.toString().c_str() );
- if(!Options::current()->produceAssignments) {
+ if(!options::produceAssignments()) {
return false;
}
if(d_assignments == NULL) {
@@ -1824,14 +1758,14 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
return true;
}
-SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
+CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
Trace("smt") << "SMT getAssignment()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssignmentCommand();
}
- if(!Options::current()->produceAssignments) {
+ if(!options::produceAssignments()) {
const char* msg =
"Cannot get the current assignment when "
"produce-assignments option is off.";
@@ -1890,7 +1824,7 @@ void SmtEngine::addToModelType( Type& t ){
Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
SmtScope smts(this);
finalOptionsAreSet();
- if( Options::current()->produceModels ) {
+ if( options::produceModels() ) {
d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
}
}
@@ -1899,7 +1833,7 @@ void SmtEngine::addToModelFunction( Expr& e ){
Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
SmtScope smts(this);
finalOptionsAreSet();
- if( Options::current()->produceModels ) {
+ if( options::produceModels() ) {
d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
}
}
@@ -1909,9 +1843,9 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
Trace("smt") << "SMT getModel()" << endl;
SmtScope smts(this);
- if(!Options::current()->produceModels) {
+ if(!options::produceModels()) {
const char* msg =
- "Cannot get value when produce-models options is off.";
+ "Cannot get model when produce-models options is off.";
throw ModalException(msg);
}
if(d_status.isNull() ||
@@ -1934,7 +1868,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
Dump("benchmark") << GetProofCommand();
}
#ifdef CVC4_PROOF
- if(!Options::current()->proof) {
+ if(!options::proof()) {
const char* msg =
"Cannot get a proof when produce-proofs option is off.";
throw ModalException(msg);
@@ -1960,7 +1894,7 @@ vector<Expr> SmtEngine::getAssertions()
}
SmtScope smts(this);
Trace("smt") << "SMT getAssertions()" << endl;
- if(!Options::current()->interactive) {
+ if(!options::interactive()) {
const char* msg =
"Cannot query the current assertion list when not in interactive mode.";
throw ModalException(msg);
@@ -1983,7 +1917,7 @@ void SmtEngine::push() {
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PushCommand();
}
- if(!Options::current()->incrementalSolving) {
+ if(!options::incrementalSolving()) {
throw ModalException("Cannot push when not solving incrementally (use --incremental)");
}
@@ -2006,7 +1940,7 @@ void SmtEngine::pop() {
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PopCommand();
}
- if(!Options::current()->incrementalSolving) {
+ if(!options::incrementalSolving()) {
throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
}
if(d_userContext->getLevel() == 0) {
@@ -2039,7 +1973,7 @@ void SmtEngine::pop() {
void SmtEngine::internalPush() {
Assert(d_fullyInited);
Trace("smt") << "SmtEngine::internalPush()" << endl;
- if(Options::current()->incrementalSolving) {
+ if(options::incrementalSolving()) {
d_private->processAssertions();
d_userContext->push();
d_context->push();
@@ -2050,7 +1984,7 @@ void SmtEngine::internalPush() {
void SmtEngine::internalPop() {
Assert(d_fullyInited);
Trace("smt") << "SmtEngine::internalPop()" << endl;
- if(Options::current()->incrementalSolving) {
+ if(options::incrementalSolving()) {
d_propEngine->pop();
d_context->pop();
d_userContext->pop();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index efb2425a1..5f0511894 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -34,7 +34,7 @@
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
#include "util/hash.h"
-#include "util/options.h"
+#include "options/options.h"
#include "util/result.h"
#include "util/sexpr.h"
#include "util/stats.h"
@@ -302,25 +302,25 @@ public:
/**
* Set information about the script executing.
*/
- void setInfo(const std::string& key, const SExpr& value)
+ void setInfo(const std::string& key, const CVC4::SExpr& value)
throw(BadOptionException, ModalException);
/**
* Query information about the SMT environment.
*/
- SExpr getInfo(const std::string& key) const
+ CVC4::SExpr getInfo(const std::string& key) const
throw(BadOptionException, ModalException);
/**
* Set an aspect of the current SMT execution environment.
*/
- void setOption(const std::string& key, const SExpr& value)
+ void setOption(const std::string& key, const CVC4::SExpr& value)
throw(BadOptionException, ModalException);
/**
* Get an aspect of the current SMT execution environment.
*/
- SExpr getOption(const std::string& key) const
+ CVC4::SExpr getOption(const std::string& key) const
throw(BadOptionException);
/**
@@ -388,7 +388,7 @@ public:
* INVALID query). Only permitted if the SmtEngine is set to
* operate interactively and produce-assignments is on.
*/
- SExpr getAssignment() throw(ModalException, AssertionException);
+ CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
/**
* Add to Model Type. This is used for recording which types should be reported
@@ -552,6 +552,17 @@ public:
}
/**
+ * Used as a predicate for options preprocessor.
+ */
+ static void beforeSearch(std::string option, bool value, SmtEngine* smt) {
+ if(smt->d_queryMade || smt->d_problemExtended) {
+ std::stringstream ss;
+ ss << "cannot change option `" << option << "' after assertions have been made";
+ throw OptionException(ss.str());
+ }
+ }
+
+ /**
* print model function (need this?)
*/
void printModel( std::ostream& out, Model* m );
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
new file mode 100644
index 000000000..8c7fa1abf
--- /dev/null
+++ b/src/smt/smt_options_template.cpp
@@ -0,0 +1,78 @@
+/********************* */
+/*! \file smt_options_template.cpp
+ ** \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 Option handling for SmtEngine
+ **
+ ** Option handling for SmtEngine.
+ **/
+
+#include "smt/smt_engine.h"
+#include "smt/bad_option_exception.h"
+#include "smt/modal_exception.h"
+#include "util/sexpr.h"
+#include "util/dump.h"
+#include "expr/command.h"
+#include "expr/node_manager.h"
+
+#include <string>
+#include <sstream>
+
+${include_all_option_headers}
+${option_handler_includes}
+
+#line 34 "${template}"
+
+using namespace std;
+
+namespace CVC4 {
+
+void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
+ throw(BadOptionException, ModalException) {
+
+ NodeManagerScope nms(d_nodeManager);
+ SmtEngine* const smt = this;
+
+ Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << SetOptionCommand(key, value);
+ }
+
+ stringstream ss;
+ ss << value;
+ string optarg = ss.str();
+
+ ${smt_setoption_handlers}
+
+#line 57 "${template}"
+
+ throw BadOptionException();
+}
+
+CVC4::SExpr SmtEngine::getOption(const std::string& key) const
+ throw(BadOptionException) {
+
+ NodeManagerScope nms(d_nodeManager);
+
+ Trace("smt") << "SMT getOption(" << key << ")" << endl;
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << GetOptionCommand(key);
+ }
+
+ ${smt_getoption_handlers}
+
+#line 74 "${template}"
+
+ throw BadOptionException();
+}
+
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback