/*! \file command.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Francois Bobot
+ ** Tim King, Morgan Deters, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
#include <utility>
#include <vector>
-#include "base/cvc4_assert.h"
+#include "api/cvc4cpp.h"
+#include "base/check.h"
#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/node.h"
+#include "expr/symbol_manager.h"
+#include "expr/type.h"
#include "options/options.h"
#include "options/smt_options.h"
#include "printer/printer.h"
+#include "proof/unsat_core.h"
#include "smt/dump.h"
#include "smt/model.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "util/sexpr.h"
+#include "util/utility.h"
using namespace std;
const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
-const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted();
+const CommandInterrupted* CommandInterrupted::s_instance =
+ new CommandInterrupted();
-std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
+std::ostream& operator<<(std::ostream& out, const Command& c)
+{
c.toStream(out,
Node::setdepth::getDepth(out),
- Node::printtypes::getPrintTypes(out),
Node::dag::getDag(out),
Node::setlanguage::getLanguage(out));
return out;
}
-ostream& operator<<(ostream& out, const Command* c) throw() {
- if(c == NULL) {
+ostream& operator<<(ostream& out, const Command* c)
+{
+ if (c == NULL)
+ {
out << "null";
- } else {
+ }
+ else
+ {
out << *c;
}
return out;
}
-std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() {
+std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
+{
s.toStream(out, Node::setlanguage::getLanguage(out));
return out;
}
-ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
- if(s == NULL) {
+ostream& operator<<(ostream& out, const CommandStatus* s)
+{
+ if (s == NULL)
+ {
out << "null";
- } else {
+ }
+ else
+ {
out << *s;
}
return out;
}
-/* class Command */
+/* output stream insertion operator for benchmark statuses */
+std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
+{
+ switch (status)
+ {
+ case SMT_SATISFIABLE: return out << "sat";
+
+ case SMT_UNSATISFIABLE: return out << "unsat";
+
+ case SMT_UNKNOWN: return out << "unknown";
+
+ default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
+ }
+}
+
+/* -------------------------------------------------------------------------- */
+/* class CommandPrintSuccess */
+/* -------------------------------------------------------------------------- */
+
+void CommandPrintSuccess::applyPrintSuccess(std::ostream& out)
+{
+ out.iword(s_iosIndex) = d_printSuccess;
+}
+
+bool CommandPrintSuccess::getPrintSuccess(std::ostream& out)
+{
+ return out.iword(s_iosIndex);
+}
+
+void CommandPrintSuccess::setPrintSuccess(std::ostream& out, bool printSuccess)
+{
+ out.iword(s_iosIndex) = printSuccess;
+}
+
+std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
+{
+ cps.applyPrintSuccess(out);
+ return out;
+}
+
+/* -------------------------------------------------------------------------- */
+/* class Command */
+/* -------------------------------------------------------------------------- */
+
+Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
-Command::Command() throw() : d_commandStatus(NULL), d_muted(false) {
+Command::Command(const api::Solver* solver)
+ : d_commandStatus(nullptr), d_muted(false)
+{
}
-Command::Command(const Command& cmd) {
- d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
+Command::Command(const Command& cmd)
+{
+ d_commandStatus =
+ (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
d_muted = cmd.d_muted;
}
-Command::~Command() throw() {
- if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) {
+Command::~Command()
+{
+ if (d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance())
+ {
delete d_commandStatus;
}
}
-bool Command::ok() const throw() {
+bool Command::ok() const
+{
// either we haven't run the command yet, or it ran successfully
- return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
+ return d_commandStatus == NULL
+ || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
}
-bool Command::fail() const throw() {
- return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
+bool Command::fail() const
+{
+ return d_commandStatus != NULL
+ && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
}
-bool Command::interrupted() const throw() {
- return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
+bool Command::interrupted() const
+{
+ return d_commandStatus != NULL
+ && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
}
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
- invoke(smtEngine);
- if(!(isMuted() && ok())) {
- printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
+void Command::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out)
+{
+ invoke(solver, sm);
+ if (!(isMuted() && ok()))
+ {
+ printResult(
+ out,
+ std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
}
}
-std::string Command::toString() const throw() {
+std::string Command::toString() const
+{
std::stringstream ss;
toStream(ss);
return ss.str();
}
-void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag,
- OutputLanguage language) const throw() {
- Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag);
-}
-
-void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() {
+void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
+{
Printer::getPrinter(language)->toStream(out, this);
}
-void Command::printResult(std::ostream& out, uint32_t verbosity) const {
- if(d_commandStatus != NULL) {
- if((!ok() && verbosity >= 1) || verbosity >= 2) {
+void Command::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (d_commandStatus != NULL)
+ {
+ if ((!ok() && verbosity >= 1) || verbosity >= 2)
+ {
out << *d_commandStatus;
}
}
}
-/* class EmptyCommand */
-
-EmptyCommand::EmptyCommand(std::string name) throw() :
- d_name(name) {
-}
-
-std::string EmptyCommand::getName() const throw() {
- return d_name;
-}
+/* -------------------------------------------------------------------------- */
+/* class EmptyCommand */
+/* -------------------------------------------------------------------------- */
-void EmptyCommand::invoke(SmtEngine* smtEngine) {
+EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
+std::string EmptyCommand::getName() const { return d_name; }
+void EmptyCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
/* empty commands have no implementation */
d_commandStatus = CommandSuccess::instance();
}
-Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new EmptyCommand(d_name);
-}
-
-Command* EmptyCommand::clone() const {
- return new EmptyCommand(d_name);
-}
-
-std::string EmptyCommand::getCommandName() const throw() {
- return "empty";
-}
-
-/* class EchoCommand */
+Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
+std::string EmptyCommand::getCommandName() const { return "empty"; }
-EchoCommand::EchoCommand(std::string output) throw() :
- d_output(output) {
+void EmptyCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
}
-std::string EchoCommand::getOutput() const throw() {
- return d_output;
-}
+/* -------------------------------------------------------------------------- */
+/* class EchoCommand */
+/* -------------------------------------------------------------------------- */
-void EchoCommand::invoke(SmtEngine* smtEngine) {
+EchoCommand::EchoCommand(std::string output) : d_output(output) {}
+std::string EchoCommand::getOutput() const { return d_output; }
+void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
/* we don't have an output stream here, nothing to do */
d_commandStatus = CommandSuccess::instance();
}
-void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) {
+void EchoCommand::invoke(api::Solver* solver,
+ SymbolManager* sm,
+ std::ostream& out)
+{
out << d_output << std::endl;
+ Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
+ << std::endl;
d_commandStatus = CommandSuccess::instance();
- printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
-}
-
-Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new EchoCommand(d_output);
+ printResult(
+ out,
+ std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
}
-Command* EchoCommand::clone() const {
- return new EchoCommand(d_output);
-}
+Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
+std::string EchoCommand::getCommandName() const { return "echo"; }
-std::string EchoCommand::getCommandName() const throw() {
- return "echo";
+void EchoCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
}
-/* class AssertCommand */
+/* -------------------------------------------------------------------------- */
+/* class AssertCommand */
+/* -------------------------------------------------------------------------- */
-AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() :
- d_expr(e), d_inUnsatCore(inUnsatCore) {
+AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore)
+ : d_term(t), d_inUnsatCore(inUnsatCore)
+{
}
-Expr AssertCommand::getExpr() const throw() {
- return d_expr;
-}
-
-void AssertCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->assertFormula(d_expr, d_inUnsatCore);
+api::Term AssertCommand::getTerm() const { return d_term; }
+void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->getSmtEngine()->assertFormula(d_term.getNode(), d_inUnsatCore);
d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+Command* AssertCommand::clone() const
+{
+ return new AssertCommand(d_term, d_inUnsatCore);
}
-Command* AssertCommand::clone() const {
- return new AssertCommand(d_expr, d_inUnsatCore);
-}
+std::string AssertCommand::getCommandName() const { return "assert"; }
-std::string AssertCommand::getCommandName() const throw() {
- return "assert";
+void AssertCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdAssert(out, d_term.getNode());
}
-/* class PushCommand */
+/* -------------------------------------------------------------------------- */
+/* class PushCommand */
+/* -------------------------------------------------------------------------- */
-void PushCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->push();
+void PushCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->push();
d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new PushCommand();
+Command* PushCommand::clone() const { return new PushCommand(); }
+std::string PushCommand::getCommandName() const { return "push"; }
+
+void PushCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdPush(out);
}
-Command* PushCommand::clone() const {
- return new PushCommand();
+/* -------------------------------------------------------------------------- */
+/* class PopCommand */
+/* -------------------------------------------------------------------------- */
+
+void PopCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->pop();
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (UnsafeInterruptException& e)
+ {
+ d_commandStatus = new CommandInterrupted();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
}
-std::string PushCommand::getCommandName() const throw() {
- return "push";
+Command* PopCommand::clone() const { return new PopCommand(); }
+std::string PopCommand::getCommandName() const { return "pop"; }
+
+void PopCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdPop(out);
}
-/* class PopCommand */
+/* -------------------------------------------------------------------------- */
+/* class CheckSatCommand */
+/* -------------------------------------------------------------------------- */
+
+CheckSatCommand::CheckSatCommand() : d_term() {}
+
+CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {}
+
+api::Term CheckSatCommand::getTerm() const { return d_term; }
+void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
+ << std::endl;
+ try
+ {
+ d_result =
+ d_term.isNull() ? solver->checkSat() : solver->checkSatAssuming(d_term);
-void PopCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->pop();
d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new PopCommand();
+api::Result CheckSatCommand::getResult() const { return d_result; }
+void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out, verbosity);
+ }
+ else
+ {
+ Trace("dtview::command") << "* RESULT: " << d_result << std::endl;
+ out << d_result << endl;
+ }
}
-Command* PopCommand::clone() const {
- return new PopCommand();
+Command* CheckSatCommand::clone() const
+{
+ CheckSatCommand* c = new CheckSatCommand(d_term);
+ c->d_result = d_result;
+ return c;
}
-std::string PopCommand::getCommandName() const throw() {
- return "pop";
+std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
+
+void CheckSatCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdCheckSat(out, d_term.getNode());
}
-/* class CheckSatCommand */
+/* -------------------------------------------------------------------------- */
+/* class CheckSatAssumingCommand */
+/* -------------------------------------------------------------------------- */
-CheckSatCommand::CheckSatCommand() throw() :
- d_expr() {
+CheckSatAssumingCommand::CheckSatAssumingCommand(api::Term term)
+ : d_terms({term})
+{
}
-CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() :
- d_expr(expr), d_inUnsatCore(inUnsatCore) {
+CheckSatAssumingCommand::CheckSatAssumingCommand(
+ const std::vector<api::Term>& terms)
+ : d_terms(terms)
+{
}
-Expr CheckSatCommand::getExpr() const throw() {
- return d_expr;
+const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const
+{
+ return d_terms;
}
-void CheckSatCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->checkSat(d_expr);
+void CheckSatAssumingCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
+ << " )~" << std::endl;
+ try
+ {
+ d_result = solver->checkSatAssuming(d_terms);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Result CheckSatCommand::getResult() const throw() {
+api::Result CheckSatAssumingCommand::getResult() const
+{
+ Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
return d_result;
}
-void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void CheckSatAssumingCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+Command* CheckSatAssumingCommand::clone() const
+{
+ CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms);
c->d_result = d_result;
return c;
}
-Command* CheckSatCommand::clone() const {
- CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore);
- c->d_result = d_result;
- return c;
+std::string CheckSatAssumingCommand::getCommandName() const
+{
+ return "check-sat-assuming";
}
-std::string CheckSatCommand::getCommandName() const throw() {
- return "check-sat";
+void CheckSatAssumingCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(
+ out, api::termVectorToNodes(d_terms));
}
-/* class QueryCommand */
-
-QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() :
- d_expr(e), d_inUnsatCore(inUnsatCore) {
-}
+/* -------------------------------------------------------------------------- */
+/* class QueryCommand */
+/* -------------------------------------------------------------------------- */
-Expr QueryCommand::getExpr() const throw() {
- return d_expr;
+QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore)
+ : d_term(t), d_inUnsatCore(inUnsatCore)
+{
}
-void QueryCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->query(d_expr);
+api::Term QueryCommand::getTerm() const { return d_term; }
+void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_result = solver->checkEntailed(d_term);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Result QueryCommand::getResult() const throw() {
- return d_result;
-}
-
-void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+api::Result QueryCommand::getResult() const { return d_result; }
+void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+Command* QueryCommand::clone() const
+{
+ QueryCommand* c = new QueryCommand(d_term, d_inUnsatCore);
c->d_result = d_result;
return c;
}
-Command* QueryCommand::clone() const {
- QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore);
- c->d_result = d_result;
- return c;
+std::string QueryCommand::getCommandName() const { return "query"; }
+
+void QueryCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdQuery(out, d_term.getNode());
}
-std::string QueryCommand::getCommandName() const throw() {
- return "query";
+/* -------------------------------------------------------------------------- */
+/* class DeclareSygusVarCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
+ api::Term var,
+ api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_var(var), d_sort(sort)
+{
}
+api::Term DeclareSygusVarCommand::getVar() const { return d_var; }
+api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }
-/* class CheckSynthCommand */
+void DeclareSygusVarCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ d_commandStatus = CommandSuccess::instance();
+}
-CheckSynthCommand::CheckSynthCommand() throw() :
- d_expr() {
+Command* DeclareSygusVarCommand::clone() const
+{
+ return new DeclareSygusVarCommand(d_symbol, d_var, d_sort);
}
-CheckSynthCommand::CheckSynthCommand(const Expr& expr, bool inUnsatCore) throw() :
- d_expr(expr), d_inUnsatCore(inUnsatCore) {
+std::string DeclareSygusVarCommand::getCommandName() const
+{
+ return "declare-var";
}
-Expr CheckSynthCommand::getExpr() const throw() {
- return d_expr;
+void DeclareSygusVarCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareVar(
+ out, d_var.getNode(), d_sort.getTypeNode());
}
-void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->checkSynth(d_expr);
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
+/* -------------------------------------------------------------------------- */
+/* class SynthFunCommand */
+/* -------------------------------------------------------------------------- */
+
+SynthFunCommand::SynthFunCommand(const std::string& id,
+ api::Term fun,
+ const std::vector<api::Term>& vars,
+ api::Sort sort,
+ bool isInv,
+ api::Grammar* g)
+ : DeclarationDefinitionCommand(id),
+ d_fun(fun),
+ d_vars(vars),
+ d_sort(sort),
+ d_isInv(isInv),
+ d_grammar(g)
+{
}
-Result CheckSynthCommand::getResult() const throw() {
- return d_result;
+api::Term SynthFunCommand::getFunction() const { return d_fun; }
+
+const std::vector<api::Term>& SynthFunCommand::getVars() const
+{
+ return d_vars;
}
-void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result << endl;
- }
+api::Sort SynthFunCommand::getSort() const { return d_sort; }
+bool SynthFunCommand::isInv() const { return d_isInv; }
+
+const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
+
+void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ d_commandStatus = CommandSuccess::instance();
}
-Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
- c->d_result = d_result;
- return c;
+Command* SynthFunCommand::clone() const
+{
+ return new SynthFunCommand(
+ d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
}
-Command* CheckSynthCommand::clone() const {
- CheckSynthCommand* c = new CheckSynthCommand(d_expr, d_inUnsatCore);
- c->d_result = d_result;
- return c;
+std::string SynthFunCommand::getCommandName() const
+{
+ return d_isInv ? "synth-inv" : "synth-fun";
}
-std::string CheckSynthCommand::getCommandName() const throw() {
- return "check-synth";
+void SynthFunCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ std::vector<Node> nodeVars = termVectorToNodes(d_vars);
+ Printer::getPrinter(language)->toStreamCmdSynthFun(
+ out,
+ d_symbol,
+ nodeVars,
+ d_sort.getTypeNode(),
+ d_isInv,
+ d_grammar->resolve().getTypeNode());
}
+/* -------------------------------------------------------------------------- */
+/* class SygusConstraintCommand */
+/* -------------------------------------------------------------------------- */
-/* class ResetCommand */
+SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
+{
+}
-void ResetCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->reset();
+void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->addSygusConstraint(d_term);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new ResetCommand();
+api::Term SygusConstraintCommand::getTerm() const { return d_term; }
+
+Command* SygusConstraintCommand::clone() const
+{
+ return new SygusConstraintCommand(d_term);
+}
+
+std::string SygusConstraintCommand::getCommandName() const
+{
+ return "constraint";
}
-Command* ResetCommand::clone() const {
- return new ResetCommand();
+void SygusConstraintCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdConstraint(out, d_term.getNode());
}
-std::string ResetCommand::getCommandName() const throw() {
- return "reset";
+/* -------------------------------------------------------------------------- */
+/* class SygusInvConstraintCommand */
+/* -------------------------------------------------------------------------- */
+
+SygusInvConstraintCommand::SygusInvConstraintCommand(
+ const std::vector<api::Term>& predicates)
+ : d_predicates(predicates)
+{
}
-/* class ResetAssertionsCommand */
+SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv,
+ const api::Term& pre,
+ const api::Term& trans,
+ const api::Term& post)
+ : SygusInvConstraintCommand(std::vector<api::Term>{inv, pre, trans, post})
+{
+}
-void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->resetAssertions();
+void SygusInvConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->addSygusInvConstraint(
+ d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new ResetAssertionsCommand();
+const std::vector<api::Term>& SygusInvConstraintCommand::getPredicates() const
+{
+ return d_predicates;
}
-Command* ResetAssertionsCommand::clone() const {
- return new ResetAssertionsCommand();
+Command* SygusInvConstraintCommand::clone() const
+{
+ return new SygusInvConstraintCommand(d_predicates);
}
-std::string ResetAssertionsCommand::getCommandName() const throw() {
- return "reset-assertions";
+std::string SygusInvConstraintCommand::getCommandName() const
+{
+ return "inv-constraint";
}
-/* class QuitCommand */
+void SygusInvConstraintCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdInvConstraint(
+ out,
+ d_predicates[0].getNode(),
+ d_predicates[1].getNode(),
+ d_predicates[2].getNode(),
+ d_predicates[3].getNode());
+}
-void QuitCommand::invoke(SmtEngine* smtEngine) {
- Dump("benchmark") << *this;
- d_commandStatus = CommandSuccess::instance();
+/* -------------------------------------------------------------------------- */
+/* class CheckSynthCommand */
+/* -------------------------------------------------------------------------- */
+
+void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_result = solver->checkSynth();
+ d_commandStatus = CommandSuccess::instance();
+ d_solution.clear();
+ // check whether we should print the status
+ if (!d_result.isUnsat()
+ || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
+ || options::sygusOut() == options::SygusSolutionOutMode::STATUS)
+ {
+ if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD)
+ {
+ d_solution << "(fail)" << endl;
+ }
+ else
+ {
+ d_solution << d_result << endl;
+ }
+ }
+ // check whether we should print the solution
+ if (d_result.isUnsat()
+ && options::sygusOut() != options::SygusSolutionOutMode::STATUS)
+ {
+ // printing a synthesis solution is a non-constant
+ // method, since it invokes a sophisticated algorithm
+ // (Figure 5 of Reynolds et al. CAV 2015).
+ // Hence, we must call here print solution here,
+ // instead of during printResult.
+ solver->printSynthSolution(d_solution);
+ }
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+api::Result CheckSynthCommand::getResult() const { return d_result; }
+void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out, verbosity);
+ }
+ else
+ {
+ out << d_solution.str();
+ }
+}
+
+Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
+
+std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
+
+void CheckSynthCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
}
-Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new QuitCommand();
+/* -------------------------------------------------------------------------- */
+/* class ResetCommand */
+/* -------------------------------------------------------------------------- */
+
+void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->getSmtEngine()->reset();
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
}
-Command* QuitCommand::clone() const {
- return new QuitCommand();
+Command* ResetCommand::clone() const { return new ResetCommand(); }
+std::string ResetCommand::getCommandName() const { return "reset"; }
+
+void ResetCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdReset(out);
}
-std::string QuitCommand::getCommandName() const throw() {
- return "exit";
+/* -------------------------------------------------------------------------- */
+/* class ResetAssertionsCommand */
+/* -------------------------------------------------------------------------- */
+
+void ResetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->resetAssertions();
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
}
-/* class CommentCommand */
+Command* ResetAssertionsCommand::clone() const
+{
+ return new ResetAssertionsCommand();
+}
-CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
+std::string ResetAssertionsCommand::getCommandName() const
+{
+ return "reset-assertions";
}
-std::string CommentCommand::getComment() const throw() {
- return d_comment;
+void ResetAssertionsCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
}
-void CommentCommand::invoke(SmtEngine* smtEngine) {
+/* -------------------------------------------------------------------------- */
+/* class QuitCommand */
+/* -------------------------------------------------------------------------- */
+
+void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
-Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new CommentCommand(d_comment);
-}
+Command* QuitCommand::clone() const { return new QuitCommand(); }
+std::string QuitCommand::getCommandName() const { return "exit"; }
-Command* CommentCommand::clone() const {
- return new CommentCommand(d_comment);
+void QuitCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdQuit(out);
}
-std::string CommentCommand::getCommandName() const throw() {
- return "comment";
+/* -------------------------------------------------------------------------- */
+/* class CommentCommand */
+/* -------------------------------------------------------------------------- */
+
+CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
+std::string CommentCommand::getComment() const { return d_comment; }
+void CommentCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ Dump("benchmark") << *this;
+ d_commandStatus = CommandSuccess::instance();
}
-/* class CommandSequence */
+Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
+std::string CommentCommand::getCommandName() const { return "comment"; }
-CommandSequence::CommandSequence() throw() :
- d_index(0) {
+void CommentCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
}
-CommandSequence::~CommandSequence() throw() {
- for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+/* -------------------------------------------------------------------------- */
+/* class CommandSequence */
+/* -------------------------------------------------------------------------- */
+
+CommandSequence::CommandSequence() : d_index(0) {}
+CommandSequence::~CommandSequence()
+{
+ for (unsigned i = d_index; i < d_commandSequence.size(); ++i)
+ {
delete d_commandSequence[i];
}
}
-void CommandSequence::addCommand(Command* cmd) throw() {
+void CommandSequence::addCommand(Command* cmd)
+{
d_commandSequence.push_back(cmd);
}
-void CommandSequence::clear() throw() {
- d_commandSequence.clear();
-}
-
-void CommandSequence::invoke(SmtEngine* smtEngine) {
- for(; d_index < d_commandSequence.size(); ++d_index) {
- d_commandSequence[d_index]->invoke(smtEngine);
- if(! d_commandSequence[d_index]->ok()) {
+void CommandSequence::clear() { d_commandSequence.clear(); }
+void CommandSequence::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ for (; d_index < d_commandSequence.size(); ++d_index)
+ {
+ d_commandSequence[d_index]->invoke(solver, sm);
+ if (!d_commandSequence[d_index]->ok())
+ {
// abort execution
d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
return;
d_commandStatus = CommandSuccess::instance();
}
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
- for(; d_index < d_commandSequence.size(); ++d_index) {
- d_commandSequence[d_index]->invoke(smtEngine, out);
- if(! d_commandSequence[d_index]->ok()) {
+void CommandSequence::invoke(api::Solver* solver,
+ SymbolManager* sm,
+ std::ostream& out)
+{
+ for (; d_index < d_commandSequence.size(); ++d_index)
+ {
+ d_commandSequence[d_index]->invoke(solver, sm, out);
+ if (!d_commandSequence[d_index]->ok())
+ {
// abort execution
d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
return;
d_commandStatus = CommandSuccess::instance();
}
-Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- CommandSequence* seq = new CommandSequence();
- for(iterator i = begin(); i != end(); ++i) {
- Command* cmd_to_export = *i;
- Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
- seq->addCommand(cmd);
- Debug("export") << "[export] so far converted: " << seq << endl;
- }
- seq->d_index = d_index;
- return seq;
-}
-
-Command* CommandSequence::clone() const {
+Command* CommandSequence::clone() const
+{
CommandSequence* seq = new CommandSequence();
- for(const_iterator i = begin(); i != end(); ++i) {
+ for (const_iterator i = begin(); i != end(); ++i)
+ {
seq->addCommand((*i)->clone());
}
seq->d_index = d_index;
return seq;
}
-CommandSequence::const_iterator CommandSequence::begin() const throw() {
+CommandSequence::const_iterator CommandSequence::begin() const
+{
return d_commandSequence.begin();
}
-CommandSequence::const_iterator CommandSequence::end() const throw() {
+CommandSequence::const_iterator CommandSequence::end() const
+{
return d_commandSequence.end();
}
-CommandSequence::iterator CommandSequence::begin() throw() {
+CommandSequence::iterator CommandSequence::begin()
+{
return d_commandSequence.begin();
}
-CommandSequence::iterator CommandSequence::end() throw() {
+CommandSequence::iterator CommandSequence::end()
+{
return d_commandSequence.end();
}
-std::string CommandSequence::getCommandName() const throw() {
- return "sequence";
-}
-
-/* class DeclarationSequenceCommand */
-
-/* class DeclarationDefinitionCommand */
+std::string CommandSequence::getCommandName() const { return "sequence"; }
-DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() :
- d_symbol(id) {
+void CommandSequence::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
+ d_commandSequence);
}
-std::string DeclarationDefinitionCommand::getSymbol() const throw() {
- return d_symbol;
+/* -------------------------------------------------------------------------- */
+/* class DeclarationSequence */
+/* -------------------------------------------------------------------------- */
+
+void DeclarationSequence::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
+ out, d_commandSequence);
}
-/* class DeclareFunctionCommand */
+/* -------------------------------------------------------------------------- */
+/* class DeclarationDefinitionCommand */
+/* -------------------------------------------------------------------------- */
-DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_func(func),
- d_type(t),
- d_printInModel(true),
- d_printInModelSetByUser(false){
+DeclarationDefinitionCommand::DeclarationDefinitionCommand(
+ const std::string& id)
+ : d_symbol(id)
+{
}
-Expr DeclareFunctionCommand::getFunction() const throw() {
- return d_func;
-}
+std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
-Type DeclareFunctionCommand::getType() const throw() {
- return d_type;
-}
+/* -------------------------------------------------------------------------- */
+/* class DeclareFunctionCommand */
+/* -------------------------------------------------------------------------- */
-bool DeclareFunctionCommand::getPrintInModel() const throw() {
- return d_printInModel;
+DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
+ api::Term func,
+ api::Sort sort)
+ : DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_sort(sort),
+ d_printInModel(true),
+ d_printInModelSetByUser(false)
+{
}
-bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() {
+api::Term DeclareFunctionCommand::getFunction() const { return d_func; }
+api::Sort DeclareFunctionCommand::getSort() const { return d_sort; }
+bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; }
+bool DeclareFunctionCommand::getPrintInModelSetByUser() const
+{
return d_printInModelSetByUser;
}
-void DeclareFunctionCommand::setPrintInModel( bool p ) {
+void DeclareFunctionCommand::setPrintInModel(bool p)
+{
d_printInModel = p;
d_printInModelSetByUser = true;
}
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
d_commandStatus = CommandSuccess::instance();
}
-Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) {
- DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap),
- d_type.exportTo(exprManager, variableMap));
- dfc->d_printInModel = d_printInModel;
- dfc->d_printInModelSetByUser = d_printInModelSetByUser;
- return dfc;
-}
-
-Command* DeclareFunctionCommand::clone() const {
- DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type);
+Command* DeclareFunctionCommand::clone() const
+{
+ DeclareFunctionCommand* dfc =
+ new DeclareFunctionCommand(d_symbol, d_func, d_sort);
dfc->d_printInModel = d_printInModel;
dfc->d_printInModelSetByUser = d_printInModelSetByUser;
return dfc;
}
-std::string DeclareFunctionCommand::getCommandName() const throw() {
+std::string DeclareFunctionCommand::getCommandName() const
+{
return "declare-fun";
}
-/* class DeclareTypeCommand */
-
-DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_arity(arity),
- d_type(t) {
+void DeclareFunctionCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareFunction(
+ out, d_func.toString(), d_sort.getTypeNode());
}
-size_t DeclareTypeCommand::getArity() const throw() {
- return d_arity;
-}
+/* -------------------------------------------------------------------------- */
+/* class DeclareSortCommand */
+/* -------------------------------------------------------------------------- */
-Type DeclareTypeCommand::getType() const throw() {
- return d_type;
+DeclareSortCommand::DeclareSortCommand(const std::string& id,
+ size_t arity,
+ api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_arity(arity), d_sort(sort)
+{
}
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
+size_t DeclareSortCommand::getArity() const { return d_arity; }
+api::Sort DeclareSortCommand::getSort() const { return d_sort; }
+void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
d_commandStatus = CommandSuccess::instance();
}
-Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) {
- return new DeclareTypeCommand(d_symbol, d_arity,
- d_type.exportTo(exprManager, variableMap));
+Command* DeclareSortCommand::clone() const
+{
+ return new DeclareSortCommand(d_symbol, d_arity, d_sort);
}
-Command* DeclareTypeCommand::clone() const {
- return new DeclareTypeCommand(d_symbol, d_arity, d_type);
+std::string DeclareSortCommand::getCommandName() const
+{
+ return "declare-sort";
}
-std::string DeclareTypeCommand::getCommandName() const throw() {
- return "declare-sort";
+void DeclareSortCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareType(
+ out, d_sort.toString(), d_arity, d_sort.getTypeNode());
}
-/* class DefineTypeCommand */
+/* -------------------------------------------------------------------------- */
+/* class DefineSortCommand */
+/* -------------------------------------------------------------------------- */
-DefineTypeCommand::DefineTypeCommand(const std::string& id,
- Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_params(),
- d_type(t) {
+DefineSortCommand::DefineSortCommand(const std::string& id, api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_params(), d_sort(sort)
+{
}
-DefineTypeCommand::DefineTypeCommand(const std::string& id,
- const std::vector<Type>& params,
- Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_params(params),
- d_type(t) {
+DefineSortCommand::DefineSortCommand(const std::string& id,
+ const std::vector<api::Sort>& params,
+ api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort)
+{
}
-const std::vector<Type>& DefineTypeCommand::getParameters() const throw() {
+const std::vector<api::Sort>& DefineSortCommand::getParameters() const
+{
return d_params;
}
-Type DefineTypeCommand::getType() const throw() {
- return d_type;
-}
-
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
+api::Sort DefineSortCommand::getSort() const { return d_sort; }
+void DefineSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
d_commandStatus = CommandSuccess::instance();
}
-Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- vector<Type> params;
- transform(d_params.begin(), d_params.end(), back_inserter(params),
- ExportTransformer(exprManager, variableMap));
- Type type = d_type.exportTo(exprManager, variableMap);
- return new DefineTypeCommand(d_symbol, params, type);
+Command* DefineSortCommand::clone() const
+{
+ return new DefineSortCommand(d_symbol, d_params, d_sort);
}
-Command* DefineTypeCommand::clone() const {
- return new DefineTypeCommand(d_symbol, d_params, d_type);
-}
+std::string DefineSortCommand::getCommandName() const { return "define-sort"; }
-std::string DefineTypeCommand::getCommandName() const throw() {
- return "define-sort";
+void DefineSortCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDefineType(
+ out,
+ d_symbol,
+ api::sortVectorToTypeNodes(d_params),
+ d_sort.getTypeNode());
}
-/* class DefineFunctionCommand */
-
-DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
- Expr func,
- Expr formula) throw() :
- DeclarationDefinitionCommand(id),
- d_func(func),
- d_formals(),
- d_formula(formula) {
-}
+/* -------------------------------------------------------------------------- */
+/* class DefineFunctionCommand */
+/* -------------------------------------------------------------------------- */
DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula) throw() :
- DeclarationDefinitionCommand(id),
- d_func(func),
- d_formals(formals),
- d_formula(formula) {
-}
-
-Expr DefineFunctionCommand::getFunction() const throw() {
- return d_func;
-}
-
-const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() {
+ api::Term func,
+ api::Term formula,
+ bool global)
+ : DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_formals(),
+ d_formula(formula),
+ d_global(global)
+{
+}
+
+DefineFunctionCommand::DefineFunctionCommand(
+ const std::string& id,
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
+ bool global)
+ : DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_formals(formals),
+ d_formula(formula),
+ d_global(global)
+{
+}
+
+api::Term DefineFunctionCommand::getFunction() const { return d_func; }
+const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
+{
return d_formals;
}
-Expr DefineFunctionCommand::getFormula() const throw() {
- return d_formula;
-}
-
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
- try {
- if(!d_func.isNull()) {
- smtEngine->defineFunction(d_func, d_formals, d_formula);
+api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
+void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ if (!d_func.isNull())
+ {
+ solver->defineFun(d_func, d_formals, d_formula, d_global);
}
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
- vector<Expr> formals;
- transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
- ExportTransformer(exprManager, variableMap));
- Expr formula = d_formula.exportTo(exprManager, variableMap);
- return new DefineFunctionCommand(d_symbol, func, formals, formula);
+Command* DefineFunctionCommand::clone() const
+{
+ return new DefineFunctionCommand(
+ d_symbol, d_func, d_formals, d_formula, d_global);
}
-Command* DefineFunctionCommand::clone() const {
- return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+std::string DefineFunctionCommand::getCommandName() const
+{
+ return "define-fun";
}
-std::string DefineFunctionCommand::getCommandName() const throw() {
- return "define-fun";
+void DefineFunctionCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDefineFunction(
+ out,
+ d_func.toString(),
+ api::termVectorToNodes(d_formals),
+ d_func.getNode().getType().getRangeType(),
+ d_formula.getNode());
}
-/* class DefineNamedFunctionCommand */
+/* -------------------------------------------------------------------------- */
+/* class DefineFunctionRecCommand */
+/* -------------------------------------------------------------------------- */
-DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula) throw() :
- DefineFunctionCommand(id, func, formals, formula) {
-}
+DefineFunctionRecCommand::DefineFunctionRecCommand(
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
- this->DefineFunctionCommand::invoke(smtEngine);
- if(!d_func.isNull() && d_func.getType().isBoolean()) {
- smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
- }
- d_commandStatus = CommandSuccess::instance();
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
+ bool global)
+ : d_global(global)
+{
+ d_funcs.push_back(func);
+ d_formals.push_back(formals);
+ d_formulas.push_back(formula);
}
-Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- Expr func = d_func.exportTo(exprManager, variableMap);
- vector<Expr> formals;
- transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
- ExportTransformer(exprManager, variableMap));
- Expr formula = d_formula.exportTo(exprManager, variableMap);
- return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
-}
+DefineFunctionRecCommand::DefineFunctionRecCommand(
-Command* DefineNamedFunctionCommand::clone() const {
- return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+ const std::vector<api::Term>& funcs,
+ const std::vector<std::vector<api::Term>>& formals,
+ const std::vector<api::Term>& formulas,
+ bool global)
+ : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global)
+{
}
-/* class SetUserAttribute */
-
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() :
- d_attr( attr ), d_expr( expr ){
+const std::vector<api::Term>& DefineFunctionRecCommand::getFunctions() const
+{
+ return d_funcs;
}
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
- std::vector<Expr>& values ) throw() :
- d_attr( attr ), d_expr( expr ){
- d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() );
+const std::vector<std::vector<api::Term>>&
+DefineFunctionRecCommand::getFormals() const
+{
+ return d_formals;
}
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
- const std::string& value ) throw() :
- d_attr( attr ), d_expr( expr ), d_str_value( value ){
+const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
+{
+ return d_formulas;
}
-void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) {
- try {
- if(!d_expr.isNull()) {
- smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
- }
+void DefineFunctionRecCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){
- Expr expr = d_expr.exportTo(exprManager, variableMap);
- SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value );
- c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
- return c;
+Command* DefineFunctionRecCommand::clone() const
+{
+ return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global);
}
-Command* SetUserAttributeCommand::clone() const{
- SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value );
- c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
- return c;
+std::string DefineFunctionRecCommand::getCommandName() const
+{
+ return "define-fun-rec";
}
-std::string SetUserAttributeCommand::getCommandName() const throw() {
- return "set-user-attribute";
+void DefineFunctionRecCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ std::vector<std::vector<Node>> formals;
+ formals.reserve(d_formals.size());
+ for (const std::vector<api::Term>& formal : d_formals)
+ {
+ formals.push_back(api::termVectorToNodes(formal));
+ }
+
+ Printer::getPrinter(language)->toStreamCmdDefineFunctionRec(
+ out,
+ api::termVectorToNodes(d_funcs),
+ formals,
+ api::termVectorToNodes(d_formulas));
+}
+/* -------------------------------------------------------------------------- */
+/* class DeclareHeapCommand */
+/* -------------------------------------------------------------------------- */
+DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort)
+ : d_locSort(locSort), d_dataSort(dataSort)
+{
}
-/* class SimplifyCommand */
+api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
+api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }
-SimplifyCommand::SimplifyCommand(Expr term) throw() :
- d_term(term) {
+void DeclareHeapCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ solver->declareSeparationHeap(d_locSort, d_dataSort);
}
-Expr SimplifyCommand::getTerm() const throw() {
- return d_term;
+Command* DeclareHeapCommand::clone() const
+{
+ return new DeclareHeapCommand(d_locSort, d_dataSort);
}
-void SimplifyCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->simplify(d_term);
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
+std::string DeclareHeapCommand::getCommandName() const
+{
+ return "declare-heap";
}
-Expr SimplifyCommand::getResult() const throw() {
- return d_result;
+void DeclareHeapCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareHeap(
+ out, d_locSort.getTypeNode(), d_dataSort.getTypeNode());
}
-void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result << endl;
- }
+/* -------------------------------------------------------------------------- */
+/* class SetUserAttributeCommand */
+/* -------------------------------------------------------------------------- */
+
+SetUserAttributeCommand::SetUserAttributeCommand(
+ const std::string& attr,
+ api::Term term,
+ const std::vector<api::Term>& termValues,
+ const std::string& strValue)
+ : d_attr(attr), d_term(term), d_termValues(termValues), d_strValue(strValue)
+{
}
-Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
- c->d_result = d_result.exportTo(exprManager, variableMap);
- return c;
+SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
+ api::Term term)
+ : SetUserAttributeCommand(attr, term, {}, "")
+{
}
-Command* SimplifyCommand::clone() const {
- SimplifyCommand* c = new SimplifyCommand(d_term);
- c->d_result = d_result;
- return c;
+SetUserAttributeCommand::SetUserAttributeCommand(
+ const std::string& attr,
+ api::Term term,
+ const std::vector<api::Term>& values)
+ : SetUserAttributeCommand(attr, term, values, "")
+{
}
-std::string SimplifyCommand::getCommandName() const throw() {
- return "simplify";
+SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
+ api::Term term,
+ const std::string& value)
+ : SetUserAttributeCommand(attr, term, {}, value)
+{
}
-/* class ExpandDefinitionsCommand */
+void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ if (!d_term.isNull())
+ {
+ solver->getSmtEngine()->setUserAttribute(
+ d_attr,
+ d_term.getExpr(),
+ api::termVectorToExprs(d_termValues),
+ d_strValue);
+ }
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
-ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() :
- d_term(term) {
+Command* SetUserAttributeCommand::clone() const
+{
+ return new SetUserAttributeCommand(d_attr, d_term, d_termValues, d_strValue);
}
-Expr ExpandDefinitionsCommand::getTerm() const throw() {
- return d_term;
+std::string SetUserAttributeCommand::getCommandName() const
+{
+ return "set-user-attribute";
}
-void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) {
- d_result = smtEngine->expandDefinitions(d_term);
- d_commandStatus = CommandSuccess::instance();
+void SetUserAttributeCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
+ out, d_attr, d_term.getNode());
}
-Expr ExpandDefinitionsCommand::getResult() const throw() {
- return d_result;
+/* -------------------------------------------------------------------------- */
+/* class SimplifyCommand */
+/* -------------------------------------------------------------------------- */
+
+SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {}
+api::Term SimplifyCommand::getTerm() const { return d_term; }
+void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_result = solver->simplify(d_term);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (UnsafeInterruptException& e)
+ {
+ d_commandStatus = new CommandInterrupted();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
}
-void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+api::Term SimplifyCommand::getResult() const { return d_result; }
+void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ 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);
+Command* SimplifyCommand::clone() const
+{
+ SimplifyCommand* c = new SimplifyCommand(d_term);
c->d_result = d_result;
return c;
}
-std::string ExpandDefinitionsCommand::getCommandName() const throw() {
- return "expand-definitions";
+std::string SimplifyCommand::getCommandName() const { return "simplify"; }
+
+void SimplifyCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term.getNode());
}
-/* class GetValueCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetValueCommand */
+/* -------------------------------------------------------------------------- */
-GetValueCommand::GetValueCommand(Expr term) throw() :
- d_terms() {
+GetValueCommand::GetValueCommand(api::Term term) : d_terms()
+{
d_terms.push_back(term);
}
-GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() :
- d_terms(terms) {
- PrettyCheckArgument(terms.size() >= 1, terms,
- "cannot get-value of an empty set of terms");
+GetValueCommand::GetValueCommand(const std::vector<api::Term>& terms)
+ : d_terms(terms)
+{
+ PrettyCheckArgument(
+ terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
}
-const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
+const std::vector<api::Term>& GetValueCommand::getTerms() const
+{
return d_terms;
}
-
-void GetValueCommand::invoke(SmtEngine* smtEngine) {
- try {
- vector<Expr> result;
- ExprManager* em = smtEngine->getExprManager();
- NodeManager* nm = NodeManager::fromExprManager(em);
- for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
- Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
- smt::SmtScope scope(smtEngine);
- Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
- Node value = Node::fromExpr(smtEngine->getValue(*i));
- if(value.getType().isInteger() && request.getType() == nm->realType()) {
- // Need to wrap in special marker so that output printers know this
- // is an integer-looking constant that really should be output as
- // a rational. Necessary for SMT-LIB standards compliance, but ugly.
- value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
- nm->mkConst(AscriptionType(em->realType())), value);
- }
- result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
+void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ std::vector<api::Term> result = solver->getValue(d_terms);
+ Assert(result.size() == d_terms.size());
+ for (int i = 0, size = d_terms.size(); i < size; i++)
+ {
+ api::Term request = d_terms[i];
+ api::Term value = result[i];
+ result[i] = solver->mkTerm(api::SEXPR, request, value);
}
- d_result = em->mkExpr(kind::SEXPR, result);
+ d_result = solver->mkTerm(api::SEXPR, result);
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (api::CVC4ApiRecoverableException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Expr GetValueCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+api::Term GetValueCommand::getResult() const { return d_result; }
+void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
expr::ExprDag::Scope scope(out, false);
out << d_result << endl;
}
}
-Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- vector<Expr> exportedTerms;
- for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
- exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
- }
- GetValueCommand* c = new GetValueCommand(exportedTerms);
- c->d_result = d_result.exportTo(exprManager, variableMap);
- return c;
-}
-
-Command* GetValueCommand::clone() const {
+Command* GetValueCommand::clone() const
+{
GetValueCommand* c = new GetValueCommand(d_terms);
c->d_result = d_result;
return c;
}
-std::string GetValueCommand::getCommandName() const throw() {
- return "get-value";
-}
-
-/* class GetAssignmentCommand */
-
-GetAssignmentCommand::GetAssignmentCommand() throw() {
-}
-
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->getAssignment();
+std::string GetValueCommand::getCommandName() const { return "get-value"; }
+
+void GetValueCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetValue(
+ out, api::termVectorToNodes(d_terms));
+}
+
+/* -------------------------------------------------------------------------- */
+/* class GetAssignmentCommand */
+/* -------------------------------------------------------------------------- */
+
+GetAssignmentCommand::GetAssignmentCommand() {}
+void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ std::map<api::Term, std::string> enames = sm->getExpressionNames();
+ std::vector<api::Term> terms;
+ std::vector<std::string> names;
+ for (const std::pair<const api::Term, std::string>& e : enames)
+ {
+ terms.push_back(e.first);
+ names.push_back(e.second);
+ }
+ // Must use vector version of getValue to ensure error is thrown regardless
+ // of whether terms is empty.
+ std::vector<api::Term> values = solver->getValue(terms);
+ Assert(values.size() == names.size());
+ std::vector<SExpr> sexprs;
+ for (size_t i = 0, nterms = terms.size(); i < nterms; i++)
+ {
+ std::vector<SExpr> ss;
+ ss.emplace_back(SExpr::Keyword(names[i]));
+ ss.emplace_back(SExpr::Keyword(values[i].toString()));
+ sexprs.emplace_back(ss);
+ }
+ d_result = SExpr(sexprs);
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (api::CVC4ApiRecoverableException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-SExpr GetAssignmentCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+SExpr GetAssignmentCommand::getResult() const { return d_result; }
+void GetAssignmentCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetAssignmentCommand::clone() const
+{
GetAssignmentCommand* c = new GetAssignmentCommand();
c->d_result = d_result;
return c;
}
-Command* GetAssignmentCommand::clone() const {
- GetAssignmentCommand* c = new GetAssignmentCommand();
- c->d_result = d_result;
- return c;
-}
-
-std::string GetAssignmentCommand::getCommandName() const throw() {
+std::string GetAssignmentCommand::getCommandName() const
+{
return "get-assignment";
}
-/* class GetModelCommand */
+void GetAssignmentCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
+}
-GetModelCommand::GetModelCommand() throw()
- : d_result(nullptr), d_smtEngine(nullptr) {}
+/* -------------------------------------------------------------------------- */
+/* class GetModelCommand */
+/* -------------------------------------------------------------------------- */
-void GetModelCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->getModel();
- d_smtEngine = smtEngine;
+GetModelCommand::GetModelCommand() : d_result(nullptr) {}
+void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_result = solver->getSmtEngine()->getModel();
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
/* Model is private to the library -- for now
-Model* GetModelCommand::getResult() const throw() {
+Model* GetModelCommand::getResult() const {
return d_result;
}
*/
-void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << *d_result;
}
}
-Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetModelCommand::clone() const
+{
GetModelCommand* c = new GetModelCommand();
c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
return c;
}
-Command* GetModelCommand::clone() const {
- GetModelCommand* c = new GetModelCommand();
- c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
+std::string GetModelCommand::getCommandName() const { return "get-model"; }
+
+void GetModelCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetModel(out);
+}
+
+/* -------------------------------------------------------------------------- */
+/* class BlockModelCommand */
+/* -------------------------------------------------------------------------- */
+
+BlockModelCommand::BlockModelCommand() {}
+void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->blockModel();
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (api::CVC4ApiRecoverableException& e)
+ {
+ d_commandStatus = new CommandRecoverableFailure(e.what());
+ }
+ catch (UnsafeInterruptException& e)
+ {
+ d_commandStatus = new CommandInterrupted();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* BlockModelCommand::clone() const
+{
+ BlockModelCommand* c = new BlockModelCommand();
return c;
}
-std::string GetModelCommand::getCommandName() const throw() {
- return "get-model";
+std::string BlockModelCommand::getCommandName() const { return "block-model"; }
+
+void BlockModelCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdBlockModel(out);
}
-/* class GetProofCommand */
+/* -------------------------------------------------------------------------- */
+/* class BlockModelValuesCommand */
+/* -------------------------------------------------------------------------- */
-GetProofCommand::GetProofCommand() throw()
- : d_result(nullptr), d_smtEngine(nullptr) {}
+BlockModelValuesCommand::BlockModelValuesCommand(
+ const std::vector<api::Term>& terms)
+ : d_terms(terms)
+{
+ PrettyCheckArgument(terms.size() >= 1,
+ terms,
+ "cannot block-model-values of an empty set of terms");
+}
-void GetProofCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_smtEngine = smtEngine;
- d_result = smtEngine->getProof();
+const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const
+{
+ return d_terms;
+}
+void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->blockModelValues(d_terms);
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Proof* GetProofCommand::getResult() const throw() {
- return d_result;
+Command* BlockModelValuesCommand::clone() const
+{
+ BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
+ return c;
}
-void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- smt::SmtScope scope(d_smtEngine);
- d_result->toStream(out);
- }
+std::string BlockModelValuesCommand::getCommandName() const
+{
+ return "block-model-values";
}
-Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetProofCommand* c = new GetProofCommand();
- c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
- return c;
+void BlockModelValuesCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdBlockModelValues(
+ out, api::termVectorToNodes(d_terms));
}
-Command* GetProofCommand::clone() const {
+/* -------------------------------------------------------------------------- */
+/* class GetProofCommand */
+/* -------------------------------------------------------------------------- */
+
+GetProofCommand::GetProofCommand() {}
+void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ Unimplemented() << "Unimplemented get-proof\n";
+}
+
+Command* GetProofCommand::clone() const
+{
GetProofCommand* c = new GetProofCommand();
- c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
return c;
}
-std::string GetProofCommand::getCommandName() const throw() {
- return "get-proof";
-}
+std::string GetProofCommand::getCommandName() const { return "get-proof"; }
-/* class GetInstantiationsCommand */
+void GetProofCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetProof(out);
+}
-GetInstantiationsCommand::GetInstantiationsCommand() throw()
- : d_smtEngine(nullptr) {}
+/* -------------------------------------------------------------------------- */
+/* class GetInstantiationsCommand */
+/* -------------------------------------------------------------------------- */
-void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_smtEngine = smtEngine;
+GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
+void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_solver = solver;
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-//Instantiations* GetInstantiationsCommand::getResult() const throw() {
-// return d_result;
-//}
-
-void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetInstantiationsCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
- d_smtEngine->printInstantiations(out);
+ }
+ else
+ {
+ d_solver->printInstantiations(out);
}
}
-Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetInstantiationsCommand* c = new GetInstantiationsCommand();
- //c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
-Command* GetInstantiationsCommand::clone() const {
+Command* GetInstantiationsCommand::clone() const
+{
GetInstantiationsCommand* c = new GetInstantiationsCommand();
- //c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
+ // c->d_result = d_result;
+ c->d_solver = d_solver;
return c;
}
-std::string GetInstantiationsCommand::getCommandName() const throw() {
+std::string GetInstantiationsCommand::getCommandName() const
+{
return "get-instantiations";
}
-/* class GetSynthSolutionCommand */
+void GetInstantiationsCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
+}
-GetSynthSolutionCommand::GetSynthSolutionCommand() throw()
- : d_smtEngine(nullptr) {}
+/* -------------------------------------------------------------------------- */
+/* class GetSynthSolutionCommand */
+/* -------------------------------------------------------------------------- */
-void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_smtEngine = smtEngine;
+GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
+void GetSynthSolutionCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_solver = solver;
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetSynthSolutionCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
- d_smtEngine->printSynthSolution(out);
+ }
+ else
+ {
+ d_solver->printSynthSolution(out);
}
}
-Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetSynthSolutionCommand::clone() const
+{
GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
- c->d_smtEngine = d_smtEngine;
+ c->d_solver = d_solver;
return c;
}
-Command* GetSynthSolutionCommand::clone() const {
- GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
- c->d_smtEngine = d_smtEngine;
+std::string GetSynthSolutionCommand::getCommandName() const
+{
+ return "get-synth-solution";
+}
+
+void GetSynthSolutionCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetSynthSolution(out);
+}
+
+/* -------------------------------------------------------------------------- */
+/* class GetInterpolCommand */
+/* -------------------------------------------------------------------------- */
+
+GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj)
+ : d_name(name), d_conj(conj), d_resultStatus(false)
+{
+}
+GetInterpolCommand::GetInterpolCommand(const std::string& name,
+ api::Term conj,
+ api::Grammar* g)
+ : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
+{
+}
+
+api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
+
+const api::Grammar* GetInterpolCommand::getGrammar() const
+{
+ return d_sygus_grammar;
+}
+
+api::Term GetInterpolCommand::getResult() const { return d_result; }
+
+void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ if (d_sygus_grammar == nullptr)
+ {
+ d_resultStatus = solver->getInterpolant(d_conj, d_result);
+ }
+ else
+ {
+ d_resultStatus =
+ solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
+ }
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetInterpolCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out, verbosity);
+ }
+ else
+ {
+ expr::ExprDag::Scope scope(out, false);
+ if (d_resultStatus)
+ {
+ out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+ << std::endl;
+ }
+ else
+ {
+ out << "none" << std::endl;
+ }
+ }
+}
+
+Command* GetInterpolCommand::clone() const
+{
+ GetInterpolCommand* c =
+ new GetInterpolCommand(d_name, d_conj, d_sygus_grammar);
+ c->d_result = d_result;
+ c->d_resultStatus = d_resultStatus;
return c;
}
-std::string GetSynthSolutionCommand::getCommandName() const throw() {
- return "get-instantiations";
+std::string GetInterpolCommand::getCommandName() const
+{
+ return "get-interpol";
+}
+
+void GetInterpolCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetInterpol(
+ out, d_name, d_conj.getNode(), d_sygus_grammar->resolve().getTypeNode());
}
-/* class GetQuantifierEliminationCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetAbductCommand */
+/* -------------------------------------------------------------------------- */
-GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() throw() :
- d_expr() {
+GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj)
+ : d_name(name), d_conj(conj), d_resultStatus(false)
+{
+}
+GetAbductCommand::GetAbductCommand(const std::string& name,
+ api::Term conj,
+ api::Grammar* g)
+ : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
+{
}
-GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw() :
- d_expr(expr), d_doFull(doFull) {
+api::Term GetAbductCommand::getConjecture() const { return d_conj; }
+
+const api::Grammar* GetAbductCommand::getGrammar() const
+{
+ return d_sygus_grammar;
}
-Expr GetQuantifierEliminationCommand::getExpr() const throw() {
- return d_expr;
+std::string GetAbductCommand::getAbductName() const { return d_name; }
+api::Term GetAbductCommand::getResult() const { return d_result; }
+
+void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ if (d_sygus_grammar == nullptr)
+ {
+ d_resultStatus = solver->getAbduct(d_conj, d_result);
+ }
+ else
+ {
+ d_resultStatus = solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
+ }
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
}
-bool GetQuantifierEliminationCommand::getDoFull() const throw() {
- return d_doFull;
+
+void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out, verbosity);
+ }
+ else
+ {
+ expr::ExprDag::Scope scope(out, false);
+ if (d_resultStatus)
+ {
+ out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+ << std::endl;
+ }
+ else
+ {
+ out << "none" << std::endl;
+ }
+ }
+}
+
+Command* GetAbductCommand::clone() const
+{
+ GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar);
+ c->d_result = d_result;
+ c->d_resultStatus = d_resultStatus;
+ return c;
}
-void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
+std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
+
+void GetAbductCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetAbduct(
+ out, d_name, d_conj.getNode(), d_sygus_grammar->resolve().getTypeNode());
+}
+
+/* -------------------------------------------------------------------------- */
+/* class GetQuantifierEliminationCommand */
+/* -------------------------------------------------------------------------- */
+
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
+ : d_term(), d_doFull(true)
+{
+}
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
+ const api::Term& term, bool doFull)
+ : d_term(term), d_doFull(doFull)
+{
+}
+
+api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
+bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
+void GetQuantifierEliminationCommand::invoke(api::Solver* solver,
+ SymbolManager* sm)
+{
+ try
+ {
+ if (d_doFull)
+ {
+ d_result = solver->getQuantifierElimination(d_term);
+ }
+ else
+ {
+ d_result = solver->getQuantifierEliminationDisjunct(d_term);
+ }
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Expr GetQuantifierEliminationCommand::getResult() const throw() {
+api::Term GetQuantifierEliminationCommand::getResult() const
+{
return d_result;
}
-
-void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetQuantifierEliminationCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* GetQuantifierEliminationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr.exportTo(exprManager, variableMap), d_doFull);
+Command* GetQuantifierEliminationCommand::clone() const
+{
+ GetQuantifierEliminationCommand* c =
+ new GetQuantifierEliminationCommand(d_term, d_doFull);
c->d_result = d_result;
return c;
}
-Command* GetQuantifierEliminationCommand::clone() const {
- GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr, d_doFull);
- c->d_result = d_result;
- return c;
+std::string GetQuantifierEliminationCommand::getCommandName() const
+{
+ return d_doFull ? "get-qe" : "get-qe-disjunct";
}
-std::string GetQuantifierEliminationCommand::getCommandName() const throw() {
- return d_doFull ? "get-qe" : "get-qe-disjunct";
+void GetQuantifierEliminationCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
+ out, d_term.getNode());
+}
+
+/* -------------------------------------------------------------------------- */
+/* class GetUnsatAssumptionsCommand */
+/* -------------------------------------------------------------------------- */
+
+GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
+
+void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_result = solver->getUnsatAssumptions();
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (api::CVC4ApiRecoverableException& e)
+ {
+ d_commandStatus = new CommandRecoverableFailure(e.what());
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+std::vector<api::Term> GetUnsatAssumptionsCommand::getResult() const
+{
+ return d_result;
+}
+
+void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out, verbosity);
+ }
+ else
+ {
+ container_to_stream(out, d_result, "(", ")\n", " ");
+ }
}
-/* class GetUnsatCoreCommand */
+Command* GetUnsatAssumptionsCommand::clone() const
+{
+ GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
+ c->d_result = d_result;
+ return c;
+}
-GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
+std::string GetUnsatAssumptionsCommand::getCommandName() const
+{
+ return "get-unsat-assumptions";
}
-GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
+void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
}
-void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) {
- try {
- d_result = smtEngine->getUnsatCore();
+/* -------------------------------------------------------------------------- */
+/* class GetUnsatCoreCommand */
+/* -------------------------------------------------------------------------- */
+
+GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {}
+void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_sm = sm;
+ d_result = solver->getUnsatCore();
+
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (api::CVC4ApiRecoverableException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetUnsatCoreCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
- d_result.toStream(out, d_names);
+ }
+ else
+ {
+ if (options::dumpUnsatCoresFull())
+ {
+ // use the assertions
+ UnsatCore ucr(api::termVectorToNodes(d_result));
+ ucr.toStream(out);
+ }
+ else
+ {
+ // otherwise, use the names
+ std::vector<std::string> names;
+ d_sm->getExpressionNames(d_result, names, true);
+ UnsatCore ucr(names);
+ ucr.toStream(out);
+ }
}
}
-const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() {
+const std::vector<api::Term>& GetUnsatCoreCommand::getUnsatCore() const
+{
// of course, this will be empty if the command hasn't been invoked yet
return d_result;
}
-Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
- c->d_result = d_result;
- return c;
-}
-
-Command* GetUnsatCoreCommand::clone() const {
- GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
+Command* GetUnsatCoreCommand::clone() const
+{
+ GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
+ c->d_sm = d_sm;
c->d_result = d_result;
return c;
}
-std::string GetUnsatCoreCommand::getCommandName() const throw() {
+std::string GetUnsatCoreCommand::getCommandName() const
+{
return "get-unsat-core";
}
-/* class GetAssertionsCommand */
-
-GetAssertionsCommand::GetAssertionsCommand() throw() {
+void GetUnsatCoreCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
}
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
- try {
+/* -------------------------------------------------------------------------- */
+/* class GetAssertionsCommand */
+/* -------------------------------------------------------------------------- */
+
+GetAssertionsCommand::GetAssertionsCommand() {}
+void GetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
stringstream ss;
- const vector<Expr> v = smtEngine->getAssertions();
+ const vector<api::Term> v = solver->getAssertions();
ss << "(\n";
- copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+ copy(v.begin(), v.end(), ostream_iterator<api::Term>(ss, "\n"));
ss << ")\n";
d_result = ss.str();
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-std::string GetAssertionsCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+std::string GetAssertionsCommand::getResult() const { return d_result; }
+void GetAssertionsCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result;
}
}
-Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetAssertionsCommand::clone() const
+{
GetAssertionsCommand* c = new GetAssertionsCommand();
c->d_result = d_result;
return c;
}
-Command* GetAssertionsCommand::clone() const {
- GetAssertionsCommand* c = new GetAssertionsCommand();
- c->d_result = d_result;
- return c;
+std::string GetAssertionsCommand::getCommandName() const
+{
+ return "get-assertions";
}
-std::string GetAssertionsCommand::getCommandName() const throw() {
- return "get-assertions";
+void GetAssertionsCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
}
-/* class SetBenchmarkStatusCommand */
+/* -------------------------------------------------------------------------- */
+/* class SetBenchmarkStatusCommand */
+/* -------------------------------------------------------------------------- */
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
- d_status(status) {
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
+ : d_status(status)
+{
}
-BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
+BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
+{
return d_status;
}
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
- try {
+void SetBenchmarkStatusCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
stringstream ss;
ss << d_status;
- SExpr status = SExpr(ss.str());
- smtEngine->setInfo("status", status);
+ solver->setInfo("status", ss.str());
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* SetBenchmarkStatusCommand::clone() const
+{
return new SetBenchmarkStatusCommand(d_status);
}
-Command* SetBenchmarkStatusCommand::clone() const {
- return new SetBenchmarkStatusCommand(d_status);
-}
-
-std::string SetBenchmarkStatusCommand::getCommandName() const throw() {
+std::string SetBenchmarkStatusCommand::getCommandName() const
+{
return "set-info";
}
-/* class SetBenchmarkLogicCommand */
+void SetBenchmarkStatusCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Result::Sat status = Result::SAT_UNKNOWN;
+ switch (d_status)
+ {
+ case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break;
+ case BenchmarkStatus::SMT_UNSATISFIABLE: status = Result::UNSAT; break;
+ case BenchmarkStatus::SMT_UNKNOWN: status = Result::SAT_UNKNOWN; break;
+ }
-SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
- d_logic(logic) {
+ Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, status);
}
-std::string SetBenchmarkLogicCommand::getLogic() const throw() {
- return d_logic;
+/* -------------------------------------------------------------------------- */
+/* class SetBenchmarkLogicCommand */
+/* -------------------------------------------------------------------------- */
+
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
+ : d_logic(logic)
+{
}
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->setLogic(d_logic);
+std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
+void SetBenchmarkLogicCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->setLogic(d_logic);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new SetBenchmarkLogicCommand(d_logic);
-}
-
-Command* SetBenchmarkLogicCommand::clone() const {
+Command* SetBenchmarkLogicCommand::clone() const
+{
return new SetBenchmarkLogicCommand(d_logic);
}
-std::string SetBenchmarkLogicCommand::getCommandName() const throw() {
+std::string SetBenchmarkLogicCommand::getCommandName() const
+{
return "set-logic";
}
-/* class SetInfoCommand */
-
-SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
- d_flag(flag),
- d_sexpr(sexpr) {
+void SetBenchmarkLogicCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
}
-std::string SetInfoCommand::getFlag() const throw() {
- return d_flag;
-}
+/* -------------------------------------------------------------------------- */
+/* class SetInfoCommand */
+/* -------------------------------------------------------------------------- */
-SExpr SetInfoCommand::getSExpr() const throw() {
- return d_sexpr;
+SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
+ : d_flag(flag), d_sexpr(sexpr)
+{
}
-void SetInfoCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->setInfo(d_flag, d_sexpr);
+std::string SetInfoCommand::getFlag() const { return d_flag; }
+SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
+void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->getSmtEngine()->setInfo(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
// As per SMT-LIB spec, silently accept unknown set-info keys
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* SetInfoCommand::clone() const
+{
return new SetInfoCommand(d_flag, d_sexpr);
}
-Command* SetInfoCommand::clone() const {
- return new SetInfoCommand(d_flag, d_sexpr);
-}
-
-std::string SetInfoCommand::getCommandName() const throw() {
- return "set-info";
-}
-
-/* class GetInfoCommand */
+std::string SetInfoCommand::getCommandName() const { return "set-info"; }
-GetInfoCommand::GetInfoCommand(std::string flag) throw() :
- d_flag(flag) {
+void SetInfoCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_sexpr);
}
-std::string GetInfoCommand::getFlag() const throw() {
- return d_flag;
-}
+/* -------------------------------------------------------------------------- */
+/* class GetInfoCommand */
+/* -------------------------------------------------------------------------- */
-void GetInfoCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
+std::string GetInfoCommand::getFlag() const { return d_flag; }
+void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
vector<SExpr> v;
v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
- v.push_back(smtEngine->getInfo(d_flag));
+ v.emplace_back(solver->getSmtEngine()->getInfo(d_flag));
stringstream ss;
- if(d_flag == "all-options" || d_flag == "all-statistics") {
+ if (d_flag == "all-options" || d_flag == "all-statistics")
+ {
ss << PrettySExprs(true);
}
ss << SExpr(v);
d_result = ss.str();
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
d_commandStatus = new CommandUnsupported();
- } catch(exception& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
+ d_commandStatus = new CommandRecoverableFailure(e.what());
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-std::string GetInfoCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+std::string GetInfoCommand::getResult() const { return d_result; }
+void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else if(d_result != "") {
+ }
+ else if (d_result != "")
+ {
out << d_result << endl;
}
}
-Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetInfoCommand::clone() const
+{
GetInfoCommand* c = new GetInfoCommand(d_flag);
c->d_result = d_result;
return c;
}
-Command* GetInfoCommand::clone() const {
- GetInfoCommand* c = new GetInfoCommand(d_flag);
- c->d_result = d_result;
- return c;
-}
+std::string GetInfoCommand::getCommandName() const { return "get-info"; }
-std::string GetInfoCommand::getCommandName() const throw() {
- return "get-info";
+void GetInfoCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
}
-/* class SetOptionCommand */
-
-SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
- d_flag(flag),
- d_sexpr(sexpr) {
-}
-
-std::string SetOptionCommand::getFlag() const throw() {
- return d_flag;
-}
+/* -------------------------------------------------------------------------- */
+/* class SetOptionCommand */
+/* -------------------------------------------------------------------------- */
-SExpr SetOptionCommand::getSExpr() const throw() {
- return d_sexpr;
+SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
+ : d_flag(flag), d_sexpr(sexpr)
+{
}
-void SetOptionCommand::invoke(SmtEngine* smtEngine) {
- try {
- smtEngine->setOption(d_flag, d_sexpr);
+std::string SetOptionCommand::getFlag() const { return d_flag; }
+SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
+void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ solver->getSmtEngine()->setOption(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
d_commandStatus = new CommandUnsupported();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* SetOptionCommand::clone() const
+{
return new SetOptionCommand(d_flag, d_sexpr);
}
-Command* SetOptionCommand::clone() const {
- return new SetOptionCommand(d_flag, d_sexpr);
-}
+std::string SetOptionCommand::getCommandName() const { return "set-option"; }
-std::string SetOptionCommand::getCommandName() const throw() {
- return "set-option";
+void SetOptionCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_sexpr);
}
-/* class GetOptionCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetOptionCommand */
+/* -------------------------------------------------------------------------- */
-GetOptionCommand::GetOptionCommand(std::string flag) throw() :
- d_flag(flag) {
-}
-
-std::string GetOptionCommand::getFlag() const throw() {
- return d_flag;
-}
-
-void GetOptionCommand::invoke(SmtEngine* smtEngine) {
- try {
- SExpr res = smtEngine->getOption(d_flag);
- d_result = res.toString();
+GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
+std::string GetOptionCommand::getFlag() const { return d_flag; }
+void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_result = solver->getOption(d_flag);
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
d_commandStatus = new CommandUnsupported();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-std::string GetOptionCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+std::string GetOptionCommand::getResult() const { return d_result; }
+void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else if(d_result != "") {
+ }
+ else if (d_result != "")
+ {
out << d_result << endl;
}
}
-Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetOptionCommand::clone() const
+{
GetOptionCommand* c = new GetOptionCommand(d_flag);
c->d_result = d_result;
return c;
}
-Command* GetOptionCommand::clone() const {
- GetOptionCommand* c = new GetOptionCommand(d_flag);
- c->d_result = d_result;
- return c;
-}
+std::string GetOptionCommand::getCommandName() const { return "get-option"; }
-std::string GetOptionCommand::getCommandName() const throw() {
- return "get-option";
+void GetOptionCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
}
-/* class DatatypeDeclarationCommand */
+/* -------------------------------------------------------------------------- */
+/* class DatatypeDeclarationCommand */
+/* -------------------------------------------------------------------------- */
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
- d_datatypes() {
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(
+ const api::Sort& datatype)
+ : d_datatypes()
+{
d_datatypes.push_back(datatype);
}
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
- d_datatypes(datatypes) {
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(
+ const std::vector<api::Sort>& datatypes)
+ : d_datatypes(datatypes)
+{
}
-const std::vector<DatatypeType>&
-DatatypeDeclarationCommand::getDatatypes() const throw() {
+const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const
+{
return d_datatypes;
}
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
+void DatatypeDeclarationCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
d_commandStatus = CommandSuccess::instance();
}
-Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- throw ExportUnsupportedException
- ("export of DatatypeDeclarationCommand unsupported");
-}
-
-Command* DatatypeDeclarationCommand::clone() const {
+Command* DatatypeDeclarationCommand::clone() const
+{
return new DatatypeDeclarationCommand(d_datatypes);
}
-std::string DatatypeDeclarationCommand::getCommandName() const throw() {
+std::string DatatypeDeclarationCommand::getCommandName() const
+{
return "declare-datatypes";
}
-/* class RewriteRuleCommand */
-
-RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& guards,
- Expr head, Expr body,
- const Triggers& triggers) throw() :
- d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) {
-}
-
-RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
- Expr head, Expr body) throw() :
- d_vars(vars), d_head(head), d_body(body) {
-}
-
-const std::vector<Expr>& RewriteRuleCommand::getVars() const throw() {
- return d_vars;
-}
-
-const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() {
- return d_guards;
-}
-
-Expr RewriteRuleCommand::getHead() const throw() {
- return d_head;
-}
-
-Expr RewriteRuleCommand::getBody() const throw() {
- return d_body;
-}
-
-const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() {
- return d_triggers;
-}
-
-void RewriteRuleCommand::invoke(SmtEngine* smtEngine) {
- try {
- ExprManager* em = smtEngine->getExprManager();
- /** build vars list */
- Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
- /** build guards list */
- Expr guards;
- if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
- else if(d_guards.size() == 1) guards = d_guards[0];
- else guards = em->mkExpr(kind::AND,d_guards);
- /** build expression */
- Expr expr;
- if( d_triggers.empty() ){
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body);
- } else {
- /** build triggers list */
- std::vector<Expr> vtriggers;
- vtriggers.reserve(d_triggers.size());
- for(Triggers::const_iterator i = d_triggers.begin(),
- end = d_triggers.end(); i != end; ++i){
- vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
- }
- Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers);
- }
- smtEngine->assertFormula(expr);
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- /** Convert variables */
- VExpr vars; vars.reserve(d_vars.size());
- for(VExpr::iterator i = d_vars.begin(), end = d_vars.end();
- i == end; ++i){
- vars.push_back(i->exportTo(exprManager, variableMap));
- };
- /** Convert guards */
- VExpr guards; guards.reserve(d_guards.size());
- for(VExpr::iterator i = d_guards.begin(), end = d_guards.end();
- i == end; ++i){
- guards.push_back(i->exportTo(exprManager, variableMap));
- };
- /** Convert triggers */
- Triggers triggers; triggers.resize(d_triggers.size());
- for(size_t i = 0, end = d_triggers.size();
- i < end; ++i){
- triggers[i].reserve(d_triggers[i].size());
- for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end();
- j == jend; ++i){
- triggers[i].push_back(j->exportTo(exprManager, variableMap));
- };
- };
- /** Convert head and body */
- Expr head = d_head.exportTo(exprManager, variableMap);
- Expr body = d_body.exportTo(exprManager, variableMap);
- /** Create the converted rules */
- return new RewriteRuleCommand(vars, guards, head, body, triggers);
-}
-
-Command* RewriteRuleCommand::clone() const {
- return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
-}
-
-std::string RewriteRuleCommand::getCommandName() const throw() {
- return "rewrite-rule";
-}
-
-/* class PropagateRuleCommand */
-
-PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& guards,
- const std::vector<Expr>& heads,
- Expr body,
- const Triggers& triggers,
- bool deduction) throw() :
- d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) {
-}
-
-PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& heads,
- Expr body,
- bool deduction) throw() :
- d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) {
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() {
- return d_vars;
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() {
- return d_guards;
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() {
- return d_heads;
-}
-
-Expr PropagateRuleCommand::getBody() const throw() {
- return d_body;
-}
-
-const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() {
- return d_triggers;
-}
-
-bool PropagateRuleCommand::isDeduction() const throw() {
- return d_deduction;
-}
-
-void PropagateRuleCommand::invoke(SmtEngine* smtEngine) {
- try {
- ExprManager* em = smtEngine->getExprManager();
- /** build vars list */
- Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
- /** build guards list */
- Expr guards;
- if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
- else if(d_guards.size() == 1) guards = d_guards[0];
- else guards = em->mkExpr(kind::AND,d_guards);
- /** build heads list */
- Expr heads;
- if(d_heads.size() == 1) heads = d_heads[0];
- else heads = em->mkExpr(kind::AND,d_heads);
- /** build expression */
- Expr expr;
- if( d_triggers.empty() ){
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body);
- } else {
- /** build triggers list */
- std::vector<Expr> vtriggers;
- vtriggers.reserve(d_triggers.size());
- for(Triggers::const_iterator i = d_triggers.begin(),
- end = d_triggers.end(); i != end; ++i){
- vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
- }
- Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers);
- }
- smtEngine->assertFormula(expr);
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- /** Convert variables */
- VExpr vars; vars.reserve(d_vars.size());
- for(VExpr::iterator i = d_vars.begin(), end = d_vars.end();
- i == end; ++i){
- vars.push_back(i->exportTo(exprManager, variableMap));
- };
- /** Convert guards */
- VExpr guards; guards.reserve(d_guards.size());
- for(VExpr::iterator i = d_guards.begin(), end = d_guards.end();
- i == end; ++i){
- guards.push_back(i->exportTo(exprManager, variableMap));
- };
- /** Convert heads */
- VExpr heads; heads.reserve(d_heads.size());
- for(VExpr::iterator i = d_heads.begin(), end = d_heads.end();
- i == end; ++i){
- heads.push_back(i->exportTo(exprManager, variableMap));
- };
- /** Convert triggers */
- Triggers triggers; triggers.resize(d_triggers.size());
- for(size_t i = 0, end = d_triggers.size();
- i < end; ++i){
- triggers[i].reserve(d_triggers[i].size());
- for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end();
- j == jend; ++i){
- triggers[i].push_back(j->exportTo(exprManager, variableMap));
- };
- };
- /** Convert head and body */
- Expr body = d_body.exportTo(exprManager, variableMap);
- /** Create the converted rules */
- return new PropagateRuleCommand(vars, guards, heads, body, triggers);
-}
-
-Command* PropagateRuleCommand::clone() const {
- return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers);
-}
-
-std::string PropagateRuleCommand::getCommandName() const throw() {
- return "propagate-rule";
-}
-
-/* output stream insertion operator for benchmark statuses */
-std::ostream& operator<<(std::ostream& out,
- BenchmarkStatus status) throw() {
- switch(status) {
-
- case SMT_SATISFIABLE:
- return out << "sat";
-
- case SMT_UNSATISFIABLE:
- return out << "unsat";
-
- case SMT_UNKNOWN:
- return out << "unknown";
-
- default:
- return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
- }
+void DatatypeDeclarationCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
+ out, api::sortVectorToTypeNodes(d_datatypes));
}
-}/* CVC4 namespace */
+} // namespace CVC4
projects / cvc5.git / blobdiff