(this commit was certified error- and warning-free by the test-and-commit script.)
#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"
return new SetUserAttributeCommand( d_attr, d_expr );
}
-/* class Simplify */
+/* class SimplifyCommand */
SimplifyCommand::SimplifyCommand(Expr term) throw() :
d_term(term) {
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() :
NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager());
for(std::vector<Expr>::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);
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() {
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<Expr> d_terms;
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;
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
#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) {
{ 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
module PROOF "proof/options.h" Proof
-option proof produce-proofs --proof bool
- turn on proof generation
-
endmodule
#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; }
# 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"
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
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
#include "cvc4autoconfig.h"
#include "util/dump.h"
+#include "smt/modal_exception.h"
+#include "smt/smt_engine.h"
#include <cerrno>
#include <cstring>
}
}
+// 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) \
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);
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);
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
friend class ::CVC4::smt::SmtEnginePrivate;
friend class ::CVC4::smt::SmtScope;
+ friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
StatisticsRegistry* d_statisticsRegistry;
/**
* 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
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?)
*/
projects / cvc5.git / commitdiff