diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
commit | c00efa92e9d61d808a8346e1d8bb3523e24d8ee2 (patch) | |
tree | 85ecfd0e8770ef539f36ec04afd34a583e75cf38 /src/smt | |
parent | c09fae89b38b525c6e2ab1691be4363d0cb1157b (diff) |
minor interface improvements, compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/options | 24 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 28 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 18 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 24 |
4 files changed, 66 insertions, 28 deletions
diff --git a/src/smt/options b/src/smt/options index 508c03a66..24c8b5e43 100644 --- a/src/smt/options +++ b/src/smt/options @@ -3,14 +3,6 @@ # 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" @@ -18,9 +10,6 @@ common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-inclu 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 --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 @@ -30,11 +19,18 @@ 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" +option expandDefinitions expand-definitions bool :default false + always expand symbol definitions in output +common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands -option checkModels check-models --check-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h" +option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID, double-check that the generated model satisfies all user assertions -common-option produceAssignments produce-assignments --produce-assignments bool +common-option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + turn on proof generation +# this is just a placeholder for later; it doesn't show up in command-line options listings +common-option unsatCores produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + turn on unsat core generation (NOT YET SUPPORTED) +common-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" support the get-assignment command option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h" print format mode for models, see --model-format=help diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index fb6cd84d8..2c20e06bb 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -23,6 +23,8 @@ #include "cvc4autoconfig.h" #include "util/dump.h" +#include "smt/modal_exception.h" +#include "smt/smt_engine.h" #include <cerrno> #include <cstring> @@ -255,6 +257,32 @@ inline ModelFormatMode stringToModelFormatMode(std::string option, std::string o } } +// ensure we haven't started search yet +inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) { + if(smt != NULL && smt->d_fullyInited) { + std::stringstream ss; + ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)"; + throw ModalException(ss.str()); + } +} + +// ensure we are a proof-enabled build of CVC4 +inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { +#ifndef CVC4_PROOF + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_PROOF */ +} + +inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { + if(value) { + throw OptionException("CVC4 does not yet have support for unsatisfiable cores"); + } +} + // This macro is used for setting :regular-output-channel and :diagnostic-output-channel // to redirect a stream. It maintains all attributes set on the stream. #define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 256867d79..55ea09de4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1448,7 +1448,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - if(!options::lazyDefinitionExpansion()) { + { Chat() << "expanding definitions..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); @@ -1764,6 +1764,22 @@ Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) { return d_private->applySubstitutions(e).toExpr(); } +Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) { + Assert(e.getExprManager() == d_exprManager); + SmtScope smts(this); + finalOptionsAreSet(); + doPendingPops(); + if( options::typeChecking() ) { + e.getType(true);// ensure expr is type-checked at this point + } + Trace("smt") << "SMT expandDefinitions(" << e << ")" << endl; + if(Dump.isOn("benchmark")) { + Dump("benchmark") << ExpandDefinitionsCommand(e); + } + hash_map<Node, Node, NodeHashFunction> cache; + return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr(); +} + Expr SmtEngine::getValue(const Expr& e) throw(ModalException, AssertionException) { Assert(e.getExprManager() == d_exprManager); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5b3229dea..9614c8ced 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -75,6 +75,8 @@ namespace smt { class SmtEnginePrivate; class SmtScope; + + void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); }/* CVC4::smt namespace */ // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -261,6 +263,7 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; + friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); StatisticsRegistry* d_statisticsRegistry; @@ -370,8 +373,8 @@ public: /** * Simplify a formula without doing "much" work. Does not involve * the SAT Engine in the simplification, but uses the current - * assertions and the current partial model, if one has been - * constructed. + * definitions, assertions, and the current partial model, if one + * has been constructed. It also involves theory normalization. * * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? @@ -379,6 +382,12 @@ public: Expr simplify(const Expr& e) throw(TypeCheckingException); /** + * Expand the definitions in a term or formula. No other + * simplification or normalization is done. + */ + Expr expandDefinitions(const Expr& e) throw(TypeCheckingException); + + /** * Get the assigned value of an expr (only if immediately preceded * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. @@ -554,17 +563,6 @@ public: } /** - * Used as a predicate for options preprocessor. - */ - static void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) { - if(smt != NULL && smt->d_fullyInited) { - std::stringstream ss; - ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)"; - throw ModalException(ss.str()); - } - } - - /** * print model function (need this?) */ void printModel( std::ostream& out, Model* m ); |