diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 9 | ||||
-rw-r--r-- | src/smt/options | 81 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 251 | ||||
-rw-r--r-- | src/smt/simplification_mode.cpp | 42 | ||||
-rw-r--r-- | src/smt/simplification_mode.h | 43 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 308 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 23 | ||||
-rw-r--r-- | src/smt/smt_options_template.cpp | 78 |
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 */ |