From c00efa92e9d61d808a8346e1d8bb3523e24d8ee2 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 15 Sep 2012 22:41:03 +0000 Subject: [PATCH] minor interface improvements, compliance fixes (this commit was certified error- and warning-free by the test-and-commit script.) --- src/expr/command.cpp | 86 +++++++++++++++++++++++++++++++++++++- src/expr/command.h | 27 ++++++++++++ src/options/mkoptions | 4 +- src/parser/smt2/Smt2.g | 2 +- src/proof/options | 3 -- src/proof/proof.h | 2 +- src/smt/options | 24 +++++------ src/smt/options_handlers.h | 28 +++++++++++++ src/smt/smt_engine.cpp | 18 +++++++- src/smt/smt_engine.h | 24 +++++------ 10 files changed, 181 insertions(+), 37 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 1e4a266a5..53ca266f4 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -26,6 +26,8 @@ #include "expr/command.h" #include "smt/smt_engine.h" #include "options/options.h" +#include "smt/options.h" +#include "smt/smt_engine_scope.h" #include "util/output.h" #include "util/dump.h" #include "util/sexpr.h" @@ -691,7 +693,7 @@ Command* SetUserAttributeCommand::clone() const{ return new SetUserAttributeCommand( d_attr, d_expr ); } -/* class Simplify */ +/* class SimplifyCommand */ SimplifyCommand::SimplifyCommand(Expr term) throw() : d_term(term) { @@ -730,6 +732,45 @@ Command* SimplifyCommand::clone() const { return c; } +/* class ExpandDefinitionsCommand */ + +ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() : + d_term(term) { +} + +Expr ExpandDefinitionsCommand::getTerm() const throw() { + return d_term; +} + +void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() { + d_result = smtEngine->expandDefinitions(d_term); + d_commandStatus = CommandSuccess::instance(); +} + +Expr ExpandDefinitionsCommand::getResult() const throw() { + return d_result; +} + +void ExpandDefinitionsCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } +} + +Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* ExpandDefinitionsCommand::clone() const { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); + c->d_result = d_result; + return c; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) throw() : @@ -752,7 +793,10 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager()); for(std::vector::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); - result.push_back(nm->mkNode(kind::TUPLE, Node::fromExpr(*i), Node::fromExpr(smtEngine->getValue(*i)))); + smt::SmtScope scope(smtEngine); + Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); + Node value = Node::fromExpr(smtEngine->getValue(*i)); + result.push_back(nm->mkNode(kind::TUPLE, request, value)); } Node n = nm->mkNode(kind::TUPLE, result); d_result = nm->toExpr(n); @@ -908,6 +952,44 @@ Command* GetProofCommand::clone() const { return c; } +/* class GetUnsatCoreCommand */ + +GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { +} + +void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { + /* + try { + d_result = smtEngine->getUnsatCore(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } + */ + d_commandStatus = new CommandFailure("unsat cores not supported yet"); +} + +void GetUnsatCoreCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + //do nothing -- unsat cores not yet supported + // d_result->toStream(out); + } +} + +Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + //c->d_result = d_result; + return c; +} + +Command* GetUnsatCoreCommand::clone() const { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + //c->d_result = d_result; + return c; +} + /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 70e71a111..5786f4e71 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -475,6 +475,21 @@ public: Command* clone() const; };/* class SimplifyCommand */ +class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + ExpandDefinitionsCommand(Expr term) throw(); + ~ExpandDefinitionsCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class ExpandDefinitionsCommand */ + class CVC4_PUBLIC GetValueCommand : public Command { protected: std::vector d_terms; @@ -531,6 +546,18 @@ public: Command* clone() const; };/* class GetProofCommand */ +class CVC4_PUBLIC GetUnsatCoreCommand : public Command { +protected: + //UnsatCore* d_result; +public: + GetUnsatCoreCommand() throw(); + ~GetUnsatCoreCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class GetUnsatCoreCommand */ + class CVC4_PUBLIC GetAssertionsCommand : public Command { protected: std::string d_result; diff --git a/src/options/mkoptions b/src/options/mkoptions index 73a2b94a3..500f5373f 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -518,7 +518,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r preemptGetopt(extra_argc, extra_argv, \"$link\");" done fi - if [ "$type" = bool -a -n "$cases" -o -n "$cases_alternate" ]; then + if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then run_handlers= if [ -n "$handlers" ]; then echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2 @@ -713,7 +713,7 @@ template <> void Options::assignBool(options::${internal}__option_t, std::string #line $lineno \"$kf\" Trace(\"options\") << \"user assigned option $internal\" << std::endl; }" - elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o "$cases_alternate" -o "$smtname" ]; then + elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then all_custom_handlers="${all_custom_handlers} #line $lineno \"$kf\" template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 867250c0f..5950f568f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -302,7 +302,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetProofCommand; } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { UNSUPPORTED("unsat cores not yet supported"); } + { cmd = new GetUnsatCoreCommand; } | /* push */ PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL diff --git a/src/proof/options b/src/proof/options index f00c8fc75..af4ffeb93 100644 --- a/src/proof/options +++ b/src/proof/options @@ -5,7 +5,4 @@ module PROOF "proof/options.h" Proof -option proof produce-proofs --proof bool - turn on proof generation - endmodule diff --git a/src/proof/proof.h b/src/proof/proof.h index 4b76d70ae..4ce621e43 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -19,7 +19,7 @@ #ifndef __CVC4__PROOF__PROOF_H #define __CVC4__PROOF__PROOF_H -#include "proof/options.h" +#include "smt/options.h" #ifdef CVC4_PROOF # define PROOF(x) if(options::proof()) { x; } 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 #include @@ -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 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,14 +373,20 @@ 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? */ 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 @@ -553,17 +562,6 @@ public: return d_status; } - /** - * 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?) */ -- 2.30.2