#include "options/language.h"
#include "options/set_language.h"
#include "sha1.hpp"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "word.h"
using namespace std;
#include "options/language.h"
#include "options/set_language.h"
#include "sha1.hpp"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "word.h"
using namespace std;
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
using namespace CVC4;
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
using namespace CVC4;
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
using namespace CVC4;
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
using namespace std;
using namespace CVC4;
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
using namespace CVC4;
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
using namespace CVC4;
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
using namespace std;
using namespace CVC4;
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "theory/logic_info.h"
using namespace std;
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
using namespace std;
using namespace CVC4;
prop/sat_solver_factory.cpp \
smt/boolean_terms.cpp \
smt/boolean_terms.h \
+ smt/command.cpp \
+ smt/command.h \
smt/command_list.cpp \
smt/command_list.h \
+ smt/dump.cpp \
+ smt/dump.h \
+ smt/ite_removal.cpp \
+ smt/ite_removal.h \
smt/logic_exception.h \
smt/logic_request.cpp \
smt/logic_request.h \
smt/managed_ostreams.cpp \
smt/managed_ostreams.h \
+ smt/model.cpp \
+ smt/model.h \
smt/model_postprocessor.cpp \
smt/model_postprocessor.h \
smt/smt_engine.cpp \
include/cvc4parser_private.h \
include/cvc4parser_public.h \
mksubdirs \
+ smt/command.i \
smt/logic_exception.i \
smt/smt_engine.i \
proof/unsat_core.i \
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "util/bitvector.h"
#include "util/hash.h"
#include "util/integer.h"
#include "expr/expr.h"
#include "expr/type.h"
#include "options/option_exception.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "util/bitvector.h"
#include "util/integer.h"
#include "util/sexpr.h"
%include "options/option_exception.i"
%include "options/options.i"
%include "parser/cvc4parser.i"
+%include "smt/command.i"
%include "smt/logic_exception.i"
-%include "smt_util/command.i"
%include "theory/logic_info.i"
// Tim: This should come after "theory/logic_info.i".
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/sat_solver_types.h"
+#include "smt/ite_removal.h"
#include "smt/smt_engine_scope.h"
-#include "smt_util/ite_removal.h"
using namespace std;
using namespace CVC4::prop;
#define __CVC4__DECISION__DECISION_STRATEGY_H
#include "prop/sat_solver_types.h"
-#include "smt_util/ite_removal.h"
+#include "smt/ite_removal.h"
namespace CVC4 {
#include "expr/node_manager.h"
#include "options/decision_options.h"
#include "theory/rewriter.h"
-#include "smt_util/ite_removal.h"
+#include "smt/ite_removal.h"
#include "smt/smt_statistics_registry.h"
namespace CVC4 {
#include <cvc4/options/options.h>
#include <cvc4/parser/parser.h>
#include <cvc4/parser/parser_builder.h>
+#include <cvc4/smt/command.h>
#include <cvc4/smt/smt_engine.h>
-#include <cvc4/smt_util/command.h>
#include <cvc4/util/integer.h>
#include <cvc4/util/rational.h>
#include <string>
#include "main/main.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
namespace CVC4 {
#include "expr/expr_manager.h"
#include "options/options.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
#include "util/statistics_registry.h"
namespace CVC4 {
#include "main/portfolio.h"
#include "options/options.h"
#include "options/set_language.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/parser_exception.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "util/result.h"
#include "util/statistics_registry.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "smt/command.h"
#include "theory/logic_info.h"
-#include "smt_util/command.h"
using namespace std;
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/parser_exception.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
#include "util/result.h"
#include "util/statistics.h"
#include <utility>
#include "options/options.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
#include "util/statistics_registry.h"
namespace CVC4 {
#include "parser/smt2/smt2_input.h"
#include "parser/smt2/sygus_input.h"
#include "parser/tptp/tptp_input.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
using namespace CVC4;
#include "options/set_language.h"
#include "parser/antlr_tracing.h"
#include "parser/parser.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "util/subrange_bound.h"
namespace CVC4 {
#include "expr/type.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
#include "options/options.h"
#include "parser/input.h"
#include "parser/parser_exception.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "util/resource_manager.h"
using namespace std;
#include <stdint.h>
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "parser/parser.h"
#include "parser/antlr_tracing.h"
}
#include "expr/type.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "parser/parser.h"
#include "parser/smt1/smt1.h"
#include "parser/parser.h"
#include "parser/antlr_tracing.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
namespace CVC4 {
class Expr;
#include "parser/parser.h"
#include "parser/smt1/smt1.h"
#include "parser/smt2/smt2_input.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "util/bitvector.h"
// ANTLR defines these, which is really bad!
// files. See the documentation in "parser/antlr_undefines.h" for more details.
#include "parser/antlr_undefines.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "parser/parser.h"
#include "parser/tptp/tptp.h"
#include "parser/antlr_tracing.h"
#include <ext/hash_set>
#include "parser/parser.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "util/hash.h"
namespace CVC4 {
#include "expr/node_manager_attributes.h" // for VarNameAttr
#include "options/language.h" // for LANG_AST
#include "printer/dagification_visitor.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "smt_util/node_visitor.h"
#include "theory/substitutions.h"
#include "options/language.h" // for LANG_AST
#include "printer/dagification_visitor.h"
#include "options/smt_options.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
#include "smt_util/node_visitor.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/substitutions.h"
#include "expr/node.h"
#include "options/language.h"
-#include "smt_util/command.h"
-#include "smt_util/model.h"
+#include "smt/command.h"
+#include "smt/model.h"
#include "util/sexpr.h"
namespace CVC4 {
#include "expr/expr.h" // for ExprSetDepth etc..
#include "expr/node_manager.h" // for VarNameAttr
#include "options/language.h" // for LANG_AST
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
#include "expr/expr.h" // for ExprSetDepth etc..
#include "expr/node_manager.h" // for VarNameAttr
#include "options/language.h" // for LANG_AST
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace std;
#include "expr/expr_iomanip.h"
#include "options/base_options.h"
#include "printer/printer.h"
+#include "smt/command.h"
#include "smt/smt_engine_scope.h"
-#include "smt_util/command.h"
namespace CVC4 {
#include "prop/minisat/minisat.h"
#include "prop/prop_engine.h"
#include "prop/theory_proxy.h"
+#include "smt/command.h"
#include "smt/smt_engine_scope.h"
-#include "smt_util/command.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
#include "prop/minisat/minisat.h"
#include "prop/minisat/mtl/Sort.h"
#include "prop/theory_proxy.h"
-#include "smt_util/command.h"
using namespace CVC4::prop;
for (int l = trail_lim.size() - level; l > 0; --l) {
context->pop();
if(Dump.isOn("state")) {
- Dump("state") << PopCommand();
+ proxy->dumpStatePop();
}
}
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
vardata[x].trail_index = -1;
- if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0)
+ if ((phase_saving > 1 ||
+ ((phase_saving == 1) && c > trail_lim.last())
+ ) && ((polarity[x] & 0x2) == 0)) {
polarity[x] = sign(trail[c]);
+ }
insertVarOrder(x);
}
qhead = trail_lim[level];
#include "prop/minisat/mtl/Heap.h"
#include "prop/minisat/mtl/Vec.h"
#include "prop/minisat/utils/Options.h"
-#include "smt_util/command.h"
#include "theory/theory.h"
#include "prop/sat_solver_factory.h"
#include "prop/theory_proxy.h"
#include "smt/smt_statistics_registry.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
#include "util/resource_manager.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "proof/cnf_proof.h"
+#include "smt/command.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/lemma_input_channel.h"
#include "smt_util/lemma_output_channel.h"
-#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
#include "util/statistics_registry.h"
return d_decisionEngine->getPolarity(var);
}
+void TheoryProxy::dumpStatePop() {
+ if(Dump.isOn("state")) {
+ Dump("state") << PopCommand();
+ }
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
SatValue getDecisionPolarity(SatVariable var);
+ /** Shorthand for Dump("state") << PopCommand() */
+ void dumpStatePop();
+
private:
/** The prop engine we are using. */
PropEngine* d_propEngine;
--- /dev/null
+/********************* */
+/*! \file command.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of command objects.
+ **
+ ** Implementation of command objects.
+ **/
+
+#include "smt/command.h"
+
+#include <exception>
+#include <iostream>
+#include <iterator>
+#include <sstream>
+#include <utility>
+#include <vector>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "expr/expr_iomanip.h"
+#include "expr/node.h"
+#include "options/options.h"
+#include "options/smt_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/model.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "util/sexpr.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
+const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
+const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted();
+
+std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
+ 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) {
+ out << "null";
+ } else {
+ out << *c;
+ }
+ return out;
+}
+
+std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() {
+ s.toStream(out, Node::setlanguage::getLanguage(out));
+ return out;
+}
+
+ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
+ if(s == NULL) {
+ out << "null";
+ } else {
+ out << *s;
+ }
+ return out;
+}
+
+/* class Command */
+
+Command::Command() throw() : d_commandStatus(NULL), d_muted(false) {
+}
+
+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()) {
+ delete d_commandStatus;
+ }
+}
+
+bool Command::ok() const throw() {
+ // either we haven't run the command yet, or it ran successfully
+ 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::interrupted() const throw() {
+ return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
+}
+
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+ invoke(smtEngine);
+ if(!(isMuted() && ok())) {
+ printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
+ }
+}
+
+std::string Command::toString() const throw() {
+ 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() {
+ Printer::getPrinter(language)->toStream(out, this);
+}
+
+void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ 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;
+}
+
+void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
+ /* 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 */
+
+EchoCommand::EchoCommand(std::string output) throw() :
+ d_output(output) {
+}
+
+std::string EchoCommand::getOutput() const throw() {
+ return d_output;
+}
+
+void EchoCommand::invoke(SmtEngine* smtEngine) throw() {
+ /* we don't have an output stream here, nothing to do */
+ d_commandStatus = CommandSuccess::instance();
+}
+
+void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+ out << 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);
+}
+
+Command* EchoCommand::clone() const {
+ return new EchoCommand(d_output);
+}
+
+std::string EchoCommand::getCommandName() const throw() {
+ return "echo";
+}
+
+/* class AssertCommand */
+
+AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() :
+ d_expr(e), d_inUnsatCore(inUnsatCore) {
+}
+
+Expr AssertCommand::getExpr() const throw() {
+ return d_expr;
+}
+
+void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->assertFormula(d_expr, d_inUnsatCore);
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
+ } 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_expr, d_inUnsatCore);
+}
+
+std::string AssertCommand::getCommandName() const throw() {
+ return "assert";
+}
+
+/* class PushCommand */
+
+void PushCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->push();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
+ } 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 throw() {
+ return "push";
+}
+
+/* class PopCommand */
+
+void PopCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->pop();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new PopCommand();
+}
+
+Command* PopCommand::clone() const {
+ return new PopCommand();
+}
+
+std::string PopCommand::getCommandName() const throw() {
+ return "pop";
+}
+
+/* class CheckSatCommand */
+
+CheckSatCommand::CheckSatCommand() throw() :
+ d_expr() {
+}
+
+CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() :
+ d_expr(expr), d_inUnsatCore(inUnsatCore) {
+}
+
+Expr CheckSatCommand::getExpr() const throw() {
+ return d_expr;
+}
+
+void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ d_result = smtEngine->checkSat(d_expr);
+ d_commandStatus = CommandSuccess::instance();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Result CheckSatCommand::getResult() const throw() {
+ return d_result;
+}
+
+void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ out << d_result << endl;
+ }
+}
+
+Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+ 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 CheckSatCommand::getCommandName() const throw() {
+ return "check-sat";
+}
+
+/* class QueryCommand */
+
+QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() :
+ d_expr(e), d_inUnsatCore(inUnsatCore) {
+}
+
+Expr QueryCommand::getExpr() const throw() {
+ return d_expr;
+}
+
+void QueryCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ d_result = smtEngine->query(d_expr);
+ d_commandStatus = CommandSuccess::instance();
+ } 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 throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ out << d_result << endl;
+ }
+}
+
+Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), 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 throw() {
+ return "query";
+}
+
+/* class ResetCommand */
+
+void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->reset();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new ResetCommand();
+}
+
+Command* ResetCommand::clone() const {
+ return new ResetCommand();
+}
+
+std::string ResetCommand::getCommandName() const throw() {
+ return "reset";
+}
+
+/* class ResetAssertionsCommand */
+
+void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->resetAssertions();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new ResetAssertionsCommand();
+}
+
+Command* ResetAssertionsCommand::clone() const {
+ return new ResetAssertionsCommand();
+}
+
+std::string ResetAssertionsCommand::getCommandName() const throw() {
+ return "reset-assertions";
+}
+
+/* class QuitCommand */
+
+void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
+ Dump("benchmark") << *this;
+ d_commandStatus = CommandSuccess::instance();
+}
+
+Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new QuitCommand();
+}
+
+Command* QuitCommand::clone() const {
+ return new QuitCommand();
+}
+
+std::string QuitCommand::getCommandName() const throw() {
+ return "exit";
+}
+
+/* class CommentCommand */
+
+CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
+}
+
+std::string CommentCommand::getComment() const throw() {
+ return d_comment;
+}
+
+void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
+ Dump("benchmark") << *this;
+ d_commandStatus = CommandSuccess::instance();
+}
+
+Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new CommentCommand(d_comment);
+}
+
+Command* CommentCommand::clone() const {
+ return new CommentCommand(d_comment);
+}
+
+std::string CommentCommand::getCommandName() const throw() {
+ return "comment";
+}
+
+/* class CommandSequence */
+
+CommandSequence::CommandSequence() throw() :
+ d_index(0) {
+}
+
+CommandSequence::~CommandSequence() throw() {
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ delete d_commandSequence[i];
+ }
+}
+
+void CommandSequence::addCommand(Command* cmd) throw() {
+ d_commandSequence.push_back(cmd);
+}
+
+void CommandSequence::clear() throw() {
+ d_commandSequence.clear();
+}
+
+void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
+ for(; d_index < d_commandSequence.size(); ++d_index) {
+ d_commandSequence[d_index]->invoke(smtEngine);
+ if(! d_commandSequence[d_index]->ok()) {
+ // abort execution
+ d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
+ return;
+ }
+ delete d_commandSequence[d_index];
+ }
+
+ AlwaysAssert(d_commandStatus == NULL);
+ d_commandStatus = CommandSuccess::instance();
+}
+
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+ for(; d_index < d_commandSequence.size(); ++d_index) {
+ d_commandSequence[d_index]->invoke(smtEngine, out);
+ if(! d_commandSequence[d_index]->ok()) {
+ // abort execution
+ d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
+ return;
+ }
+ delete d_commandSequence[d_index];
+ }
+
+ AlwaysAssert(d_commandStatus == NULL);
+ 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 {
+ CommandSequence* seq = new CommandSequence();
+ 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() {
+ return d_commandSequence.begin();
+}
+
+CommandSequence::const_iterator CommandSequence::end() const throw() {
+ return d_commandSequence.end();
+}
+
+CommandSequence::iterator CommandSequence::begin() throw() {
+ return d_commandSequence.begin();
+}
+
+CommandSequence::iterator CommandSequence::end() throw() {
+ return d_commandSequence.end();
+}
+
+std::string CommandSequence::getCommandName() const throw() {
+ return "sequence";
+}
+
+/* class DeclarationSequenceCommand */
+
+/* class DeclarationDefinitionCommand */
+
+DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() :
+ d_symbol(id) {
+}
+
+std::string DeclarationDefinitionCommand::getSymbol() const throw() {
+ return d_symbol;
+}
+
+/* class DeclareFunctionCommand */
+
+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){
+}
+
+Expr DeclareFunctionCommand::getFunction() const throw() {
+ return d_func;
+}
+
+Type DeclareFunctionCommand::getType() const throw() {
+ return d_type;
+}
+
+bool DeclareFunctionCommand::getPrintInModel() const throw() {
+ return d_printInModel;
+}
+
+bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() {
+ return d_printInModelSetByUser;
+}
+
+void DeclareFunctionCommand::setPrintInModel( bool p ) {
+ d_printInModel = p;
+ d_printInModelSetByUser = true;
+}
+
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+ 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);
+ dfc->d_printInModel = d_printInModel;
+ dfc->d_printInModelSetByUser = d_printInModelSetByUser;
+ return dfc;
+}
+
+std::string DeclareFunctionCommand::getCommandName() const throw() {
+ 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) {
+}
+
+size_t DeclareTypeCommand::getArity() const throw() {
+ return d_arity;
+}
+
+Type DeclareTypeCommand::getType() const throw() {
+ return d_type;
+}
+
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+ d_commandStatus = CommandSuccess::instance();
+}
+
+Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) {
+ return new DeclareTypeCommand(d_symbol, d_arity,
+ d_type.exportTo(exprManager, variableMap));
+}
+
+Command* DeclareTypeCommand::clone() const {
+ return new DeclareTypeCommand(d_symbol, d_arity, d_type);
+}
+
+std::string DeclareTypeCommand::getCommandName() const throw() {
+ return "declare-sort";
+}
+
+/* class DefineTypeCommand */
+
+DefineTypeCommand::DefineTypeCommand(const std::string& id,
+ Type t) throw() :
+ DeclarationDefinitionCommand(id),
+ d_params(),
+ d_type(t) {
+}
+
+DefineTypeCommand::DefineTypeCommand(const std::string& id,
+ const std::vector<Type>& params,
+ Type t) throw() :
+ DeclarationDefinitionCommand(id),
+ d_params(params),
+ d_type(t) {
+}
+
+const std::vector<Type>& DefineTypeCommand::getParameters() const throw() {
+ return d_params;
+}
+
+Type DefineTypeCommand::getType() const throw() {
+ return d_type;
+}
+
+void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+ 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* DefineTypeCommand::clone() const {
+ return new DefineTypeCommand(d_symbol, d_params, d_type);
+}
+
+std::string DefineTypeCommand::getCommandName() const throw() {
+ return "define-sort";
+}
+
+/* class DefineFunctionCommand */
+
+DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
+ Expr func,
+ Expr formula) throw() :
+ DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_formals(),
+ d_formula(formula) {
+}
+
+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() {
+ return d_formals;
+}
+
+Expr DefineFunctionCommand::getFormula() const throw() {
+ return d_formula;
+}
+
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ if(!d_func.isNull()) {
+ smtEngine->defineFunction(d_func, d_formals, d_formula);
+ }
+ d_commandStatus = CommandSuccess::instance();
+ } 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);
+}
+
+std::string DefineFunctionCommand::getCommandName() const throw() {
+ return "define-fun";
+}
+
+/* class DefineNamedFunctionCommand */
+
+DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
+ Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula) throw() :
+ DefineFunctionCommand(id, func, formals, formula) {
+}
+
+void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+ 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();
+}
+
+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);
+}
+
+Command* DefineNamedFunctionCommand::clone() const {
+ return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+}
+
+/* class SetUserAttribute */
+
+SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() :
+ d_attr( attr ), d_expr( expr ){
+}
+
+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() );
+}
+
+SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
+ const std::string& value ) throw() :
+ d_attr( attr ), d_expr( expr ), d_str_value( value ){
+}
+
+void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
+ try {
+ if(!d_expr.isNull()) {
+ smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
+ }
+ d_commandStatus = CommandSuccess::instance();
+ } 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* 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 SetUserAttributeCommand::getCommandName() const throw() {
+ return "set-user-attribute";
+}
+
+/* class SimplifyCommand */
+
+SimplifyCommand::SimplifyCommand(Expr term) throw() :
+ d_term(term) {
+}
+
+Expr SimplifyCommand::getTerm() const throw() {
+ return d_term;
+}
+
+void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
+ 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());
+ }
+}
+
+Expr SimplifyCommand::getResult() const throw() {
+ return d_result;
+}
+
+void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ out << d_result << endl;
+ }
+}
+
+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;
+}
+
+Command* SimplifyCommand::clone() const {
+ SimplifyCommand* c = new SimplifyCommand(d_term);
+ c->d_result = d_result;
+ return c;
+}
+
+std::string SimplifyCommand::getCommandName() const throw() {
+ return "simplify";
+}
+
+/* class ExpandDefinitionsCommand */
+
+ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() :
+ d_term(term) {
+}
+
+Expr ExpandDefinitionsCommand::getTerm() const throw() {
+ return d_term;
+}
+
+void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() {
+ d_result = smtEngine->expandDefinitions(d_term);
+ d_commandStatus = CommandSuccess::instance();
+}
+
+Expr ExpandDefinitionsCommand::getResult() const throw() {
+ return d_result;
+}
+
+void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ out << d_result << endl;
+ }
+}
+
+Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
+ c->d_result = d_result.exportTo(exprManager, variableMap);
+ return c;
+}
+
+Command* ExpandDefinitionsCommand::clone() const {
+ ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
+ c->d_result = d_result;
+ return c;
+}
+
+std::string ExpandDefinitionsCommand::getCommandName() const throw() {
+ return "expand-definitions";
+}
+
+/* class GetValueCommand */
+
+GetValueCommand::GetValueCommand(Expr term) throw() :
+ 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");
+}
+
+const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
+ return d_terms;
+}
+
+void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
+ 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());
+ }
+ d_result = em->mkExpr(kind::SEXPR, result);
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
+ } 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 throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } 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 {
+ 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) throw() {
+ try {
+ d_result = smtEngine->getAssignment();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
+ } 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 throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ out << d_result << endl;
+ }
+}
+
+Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ 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() {
+ return "get-assignment";
+}
+
+/* class GetModelCommand */
+
+GetModelCommand::GetModelCommand() throw() {
+}
+
+void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ d_result = smtEngine->getModel();
+ d_smtEngine = smtEngine;
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+/* Model is private to the library -- for now
+Model* GetModelCommand::getResult() const throw() {
+ return d_result;
+}
+*/
+
+void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ out << *d_result;
+ }
+}
+
+Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ 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;
+ return c;
+}
+
+std::string GetModelCommand::getCommandName() const throw() {
+ return "get-model";
+}
+
+/* class GetProofCommand */
+
+GetProofCommand::GetProofCommand() throw() {
+}
+
+void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ d_smtEngine = smtEngine;
+ d_result = smtEngine->getProof();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Proof* GetProofCommand::getResult() const throw() {
+ return d_result;
+}
+
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ smt::SmtScope scope(d_smtEngine);
+ d_result->toStream(out);
+ }
+}
+
+Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ GetProofCommand* c = new GetProofCommand();
+ c->d_result = d_result;
+ c->d_smtEngine = d_smtEngine;
+ return c;
+}
+
+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";
+}
+
+/* class GetInstantiationsCommand */
+
+GetInstantiationsCommand::GetInstantiationsCommand() throw() {
+}
+
+void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ d_smtEngine = smtEngine;
+ d_commandStatus = CommandSuccess::instance();
+ } 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 throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ d_smtEngine->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 {
+ GetInstantiationsCommand* c = new GetInstantiationsCommand();
+ //c->d_result = d_result;
+ c->d_smtEngine = d_smtEngine;
+ return c;
+}
+
+std::string GetInstantiationsCommand::getCommandName() const throw() {
+ return "get-instantiations";
+}
+
+/* class GetSynthSolutionCommand */
+
+GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
+}
+
+void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ d_smtEngine = smtEngine;
+ d_commandStatus = CommandSuccess::instance();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ d_smtEngine->printSynthSolution(out);
+ }
+}
+
+Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
+ c->d_smtEngine = d_smtEngine;
+ return c;
+}
+
+Command* GetSynthSolutionCommand::clone() const {
+ GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
+ c->d_smtEngine = d_smtEngine;
+ return c;
+}
+
+std::string GetSynthSolutionCommand::getCommandName() const throw() {
+ return "get-instantiations";
+}
+
+/* class GetUnsatCoreCommand */
+
+GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
+}
+
+GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
+}
+
+void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ d_result = smtEngine->getUnsatCore();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ d_result.toStream(out, d_names);
+ }
+}
+
+const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() {
+ // 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);
+ c->d_result = d_result;
+ return c;
+}
+
+std::string GetUnsatCoreCommand::getCommandName() const throw() {
+ return "get-unsat-core";
+}
+
+/* class GetAssertionsCommand */
+
+GetAssertionsCommand::GetAssertionsCommand() throw() {
+}
+
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ stringstream ss;
+ const vector<Expr> v = smtEngine->getAssertions();
+ ss << "(\n";
+ copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+ ss << ")\n";
+ d_result = ss.str();
+ d_commandStatus = CommandSuccess::instance();
+ } 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 throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else {
+ out << d_result;
+ }
+}
+
+Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ 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 throw() {
+ return "get-assertions";
+}
+
+/* class SetBenchmarkStatusCommand */
+
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
+ d_status(status) {
+}
+
+BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
+ return d_status;
+}
+
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ stringstream ss;
+ ss << d_status;
+ SExpr status = SExpr(ss.str());
+ smtEngine->setInfo("status", status);
+ d_commandStatus = CommandSuccess::instance();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new SetBenchmarkStatusCommand(d_status);
+}
+
+Command* SetBenchmarkStatusCommand::clone() const {
+ return new SetBenchmarkStatusCommand(d_status);
+}
+
+std::string SetBenchmarkStatusCommand::getCommandName() const throw() {
+ return "set-info";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
+ d_logic(logic) {
+}
+
+std::string SetBenchmarkLogicCommand::getLogic() const throw() {
+ return d_logic;
+}
+
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->setLogic(d_logic);
+ d_commandStatus = CommandSuccess::instance();
+ } 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 {
+ return new SetBenchmarkLogicCommand(d_logic);
+}
+
+std::string SetBenchmarkLogicCommand::getCommandName() const throw() {
+ return "set-logic";
+}
+
+/* class SetInfoCommand */
+
+SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
+ d_flag(flag),
+ d_sexpr(sexpr) {
+}
+
+std::string SetInfoCommand::getFlag() const throw() {
+ return d_flag;
+}
+
+SExpr SetInfoCommand::getSExpr() const throw() {
+ return d_sexpr;
+}
+
+void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->setInfo(d_flag, d_sexpr);
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnrecognizedOptionException&) {
+ // As per SMT-LIB spec, silently accept unknown set-info keys
+ d_commandStatus = CommandSuccess::instance();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ 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 */
+
+GetInfoCommand::GetInfoCommand(std::string flag) throw() :
+ d_flag(flag) {
+}
+
+std::string GetInfoCommand::getFlag() const throw() {
+ return d_flag;
+}
+
+void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ vector<SExpr> v;
+ v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
+ v.push_back(smtEngine->getInfo(d_flag));
+ stringstream ss;
+ 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&) {
+ d_commandStatus = new CommandUnsupported();
+ } 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 throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else if(d_result != "") {
+ out << d_result << endl;
+ }
+}
+
+Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ 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 throw() {
+ return "get-info";
+}
+
+/* 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;
+}
+
+SExpr SetOptionCommand::getSExpr() const throw() {
+ return d_sexpr;
+}
+
+void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
+ try {
+ smtEngine->setOption(d_flag, d_sexpr);
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnrecognizedOptionException&) {
+ d_commandStatus = new CommandUnsupported();
+ } catch(exception& e) {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new SetOptionCommand(d_flag, d_sexpr);
+}
+
+Command* SetOptionCommand::clone() const {
+ return new SetOptionCommand(d_flag, d_sexpr);
+}
+
+std::string SetOptionCommand::getCommandName() const throw() {
+ return "set-option";
+}
+
+/* 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) throw() {
+ try {
+ SExpr res = smtEngine->getOption(d_flag);
+ d_result = res.toString();
+ d_commandStatus = CommandSuccess::instance();
+ } catch(UnrecognizedOptionException&) {
+ d_commandStatus = new CommandUnsupported();
+ } 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 throw() {
+ if(! ok()) {
+ this->Command::printResult(out, verbosity);
+ } else if(d_result != "") {
+ out << d_result << endl;
+ }
+}
+
+Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ 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 throw() {
+ return "get-option";
+}
+
+/* class DatatypeDeclarationCommand */
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
+ d_datatypes() {
+ d_datatypes.push_back(datatype);
+}
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
+ d_datatypes(datatypes) {
+}
+
+const std::vector<DatatypeType>&
+DatatypeDeclarationCommand::getDatatypes() const throw() {
+ return d_datatypes;
+}
+
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
+ d_commandStatus = CommandSuccess::instance();
+}
+
+Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ throw ExportUnsupportedException
+ ("export of DatatypeDeclarationCommand unsupported");
+}
+
+Command* DatatypeDeclarationCommand::clone() const {
+ return new DatatypeDeclarationCommand(d_datatypes);
+}
+
+std::string DatatypeDeclarationCommand::getCommandName() const throw() {
+ 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) throw() {
+ 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) throw() {
+ 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!]";
+ }
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file command.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the command pattern on SmtEngines.
+ **
+ ** Implementation of the command pattern on SmtEngines. Command
+ ** objects are generated by the parser (typically) to implement the
+ ** commands in parsed input (see Parser::parseNextCommand()), or by
+ ** client code.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__COMMAND_H
+#define __CVC4__COMMAND_H
+
+#include <iosfwd>
+#include <map>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "expr/datatype.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+#include "expr/variable_type_map.h"
+#include "proof/unsat_core.h"
+#include "util/proof.h"
+#include "util/result.h"
+#include "util/sexpr.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+class Command;
+class CommandStatus;
+class Model;
+
+std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
+
+/** The status an SMT benchmark can have */
+enum BenchmarkStatus {
+ /** Benchmark is satisfiable */
+ SMT_SATISFIABLE,
+ /** Benchmark is unsatisfiable */
+ SMT_UNSATISFIABLE,
+ /** The status of the benchmark is unknown */
+ SMT_UNKNOWN
+};/* enum BenchmarkStatus */
+
+std::ostream& operator<<(std::ostream& out,
+ BenchmarkStatus status) throw() CVC4_PUBLIC;
+
+/**
+ * IOStream manipulator to print success messages or not.
+ *
+ * out << Command::printsuccess(false) << CommandSuccess();
+ *
+ * prints nothing, but
+ *
+ * out << Command::printsuccess(true) << CommandSuccess();
+ *
+ * prints a success message (in a manner appropriate for the current
+ * output language).
+ */
+class CVC4_PUBLIC CommandPrintSuccess {
+ /**
+ * The allocated index in ios_base for our depth setting.
+ */
+ static const int s_iosIndex;
+
+ /**
+ * The default setting, for ostreams that haven't yet had a
+ * setdepth() applied to them.
+ */
+ static const int s_defaultPrintSuccess = false;
+
+ /**
+ * When this manipulator is used, the setting is stored here.
+ */
+ bool d_printSuccess;
+
+public:
+ /**
+ * Construct a CommandPrintSuccess with the given setting.
+ */
+ CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}
+
+ inline void applyPrintSuccess(std::ostream& out) throw() {
+ out.iword(s_iosIndex) = d_printSuccess;
+ }
+
+ static inline bool getPrintSuccess(std::ostream& out) throw() {
+ return out.iword(s_iosIndex);
+ }
+
+ static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
+ out.iword(s_iosIndex) = printSuccess;
+ }
+
+ /**
+ * Set the print-success state on the output stream for the current
+ * stack scope. This makes sure the old state is reset on the
+ * stream after normal OR exceptional exit from the scope, using the
+ * RAII C++ idiom.
+ */
+ class Scope {
+ std::ostream& d_out;
+ bool d_oldPrintSuccess;
+
+ public:
+
+ inline Scope(std::ostream& out, bool printSuccess) throw() :
+ d_out(out),
+ d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
+ CommandPrintSuccess::setPrintSuccess(out, printSuccess);
+ }
+
+ inline ~Scope() throw() {
+ CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
+ }
+
+ };/* class CommandPrintSuccess::Scope */
+
+};/* class CommandPrintSuccess */
+
+/**
+ * Sets the default print-success setting when pretty-printing an Expr
+ * to an ostream. Use like this:
+ *
+ * // let out be an ostream, e an Expr
+ * out << Expr::setdepth(n) << e << endl;
+ *
+ * The depth stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
+ cps.applyPrintSuccess(out);
+ return out;
+}
+
+class CVC4_PUBLIC CommandStatus {
+protected:
+ // shouldn't construct a CommandStatus (use a derived class)
+ CommandStatus() throw() {}
+public:
+ virtual ~CommandStatus() throw() {}
+ void toStream(std::ostream& out,
+ OutputLanguage language = language::output::LANG_AUTO) const throw();
+ virtual CommandStatus& clone() const = 0;
+};/* class CommandStatus */
+
+class CVC4_PUBLIC CommandSuccess : public CommandStatus {
+ static const CommandSuccess* s_instance;
+public:
+ static const CommandSuccess* instance() throw() { return s_instance; }
+ CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandInterrupted : public CommandStatus {
+ static const CommandInterrupted* s_instance;
+public:
+ static const CommandInterrupted* instance() throw() { return s_instance; }
+ CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); }
+};/* class CommandInterrupted */
+
+class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
+public:
+ CommandStatus& clone() const { return *new CommandUnsupported(*this); }
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandFailure : public CommandStatus {
+ std::string d_message;
+public:
+ CommandFailure(std::string message) throw() : d_message(message) {}
+ CommandFailure& clone() const { return *new CommandFailure(*this); }
+ ~CommandFailure() throw() {}
+ std::string getMessage() const throw() { return d_message; }
+};/* class CommandFailure */
+
+class CVC4_PUBLIC Command {
+protected:
+ /**
+ * This field contains a command status if the command has been
+ * invoked, or NULL if it has not. This field is either a
+ * dynamically-allocated pointer, or it's a pointer to the singleton
+ * CommandSuccess instance. Doing so is somewhat asymmetric, but
+ * it avoids the need to dynamically allocate memory in the common
+ * case of a successful command.
+ */
+ const CommandStatus* d_commandStatus;
+
+ /**
+ * True if this command is "muted"---i.e., don't print "success" on
+ * successful execution.
+ */
+ bool d_muted;
+
+public:
+ typedef CommandPrintSuccess printsuccess;
+
+ Command() throw();
+ Command(const Command& cmd);
+
+ virtual ~Command() throw();
+
+ virtual void invoke(SmtEngine* smtEngine) throw() = 0;
+ virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+
+ virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const throw();
+
+ std::string toString() const throw();
+
+ virtual std::string getCommandName() const throw() = 0;
+
+ /**
+ * If false, instruct this Command not to print a success message.
+ */
+ void setMuted(bool muted) throw() { d_muted = muted; }
+
+ /**
+ * Determine whether this Command will print a success message.
+ */
+ bool isMuted() throw() { return d_muted; }
+
+ /**
+ * Either the command hasn't run yet, or it completed successfully
+ * (CommandSuccess, not CommandUnsupported or CommandFailure).
+ */
+ bool ok() const throw();
+
+ /**
+ * The command completed in a failure state (CommandFailure, not
+ * CommandSuccess or CommandUnsupported).
+ */
+ bool fail() const throw();
+
+ /**
+ * The command was ran but was interrupted due to resource limiting.
+ */
+ bool interrupted() const throw();
+
+ /** Get the command status (it's NULL if we haven't run yet). */
+ const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
+
+ virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+
+ /**
+ * Maps this Command into one for a different ExprManager, using
+ * variableMap for the translation and extending it with any new
+ * mappings.
+ */
+ virtual Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) = 0;
+
+ /**
+ * Clone this Command (make a shallow copy).
+ */
+ virtual Command* clone() const = 0;
+
+protected:
+ class ExportTransformer {
+ ExprManager* d_exprManager;
+ ExprManagerMapCollection& d_variableMap;
+ public:
+ ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) :
+ d_exprManager(exprManager),
+ d_variableMap(variableMap) {
+ }
+ Expr operator()(Expr e) {
+ return e.exportTo(d_exprManager, d_variableMap);
+ }
+ Type operator()(Type t) {
+ return t.exportTo(d_exprManager, d_variableMap);
+ }
+ };/* class Command::ExportTransformer */
+};/* class Command */
+
+/**
+ * EmptyCommands are the residue of a command after the parser handles
+ * them (and there's nothing left to do).
+ */
+class CVC4_PUBLIC EmptyCommand : public Command {
+protected:
+ std::string d_name;
+public:
+ EmptyCommand(std::string name = "") throw();
+ ~EmptyCommand() throw() {}
+ std::string getName() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class EmptyCommand */
+
+class CVC4_PUBLIC EchoCommand : public Command {
+protected:
+ std::string d_output;
+public:
+ EchoCommand(std::string output = "") throw();
+ ~EchoCommand() throw() {}
+ std::string getOutput() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class EchoCommand */
+
+class CVC4_PUBLIC AssertCommand : public Command {
+protected:
+ Expr d_expr;
+ bool d_inUnsatCore;
+public:
+ AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
+ ~AssertCommand() throw() {}
+ Expr getExpr() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class AssertCommand */
+
+class CVC4_PUBLIC PushCommand : public Command {
+public:
+ ~PushCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class PushCommand */
+
+class CVC4_PUBLIC PopCommand : public Command {
+public:
+ ~PopCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class PopCommand */
+
+class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
+protected:
+ std::string d_symbol;
+public:
+ DeclarationDefinitionCommand(const std::string& id) throw();
+ ~DeclarationDefinitionCommand() throw() {}
+ virtual void invoke(SmtEngine* smtEngine) throw() = 0;
+ std::string getSymbol() const throw();
+};/* class DeclarationDefinitionCommand */
+
+class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
+protected:
+ Expr d_func;
+ Type d_type;
+ bool d_printInModel;
+ bool d_printInModelSetByUser;
+public:
+ DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw();
+ ~DeclareFunctionCommand() throw() {}
+ Expr getFunction() const throw();
+ Type getType() const throw();
+ bool getPrintInModel() const throw();
+ bool getPrintInModelSetByUser() const throw();
+ void setPrintInModel( bool p );
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class DeclareFunctionCommand */
+
+class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
+protected:
+ size_t d_arity;
+ Type d_type;
+public:
+ DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
+ ~DeclareTypeCommand() throw() {}
+ size_t getArity() const throw();
+ Type getType() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class DeclareTypeCommand */
+
+class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
+protected:
+ std::vector<Type> d_params;
+ Type d_type;
+public:
+ DefineTypeCommand(const std::string& id, Type t) throw();
+ DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
+ ~DefineTypeCommand() throw() {}
+ const std::vector<Type>& getParameters() const throw();
+ Type getType() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class DefineTypeCommand */
+
+class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
+protected:
+ Expr d_func;
+ std::vector<Expr> d_formals;
+ Expr d_formula;
+public:
+ DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
+ DefineFunctionCommand(const std::string& id, Expr func,
+ const std::vector<Expr>& formals, Expr formula) throw();
+ ~DefineFunctionCommand() throw() {}
+ Expr getFunction() const throw();
+ const std::vector<Expr>& getFormals() const throw();
+ Expr getFormula() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class DefineFunctionCommand */
+
+/**
+ * This differs from DefineFunctionCommand only in that it instructs
+ * the SmtEngine to "remember" this function for later retrieval with
+ * getAssignment(). Used for :named attributes in SMT-LIBv2.
+ */
+class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
+public:
+ DefineNamedFunctionCommand(const std::string& id, Expr func,
+ const std::vector<Expr>& formals, Expr formula) throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+};/* class DefineNamedFunctionCommand */
+
+/**
+ * The command when an attribute is set by a user. In SMT-LIBv2 this is done
+ * via the syntax (! expr :attr)
+ */
+class CVC4_PUBLIC SetUserAttributeCommand : public Command {
+protected:
+ std::string d_attr;
+ Expr d_expr;
+ std::vector<Expr> d_expr_values;
+ std::string d_str_value;
+public:
+ SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
+ SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw();
+ SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw();
+ ~SetUserAttributeCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class SetUserAttributeCommand */
+
+class CVC4_PUBLIC CheckSatCommand : public Command {
+protected:
+ Expr d_expr;
+ Result d_result;
+ bool d_inUnsatCore;
+public:
+ CheckSatCommand() throw();
+ CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
+ ~CheckSatCommand() throw() {}
+ Expr getExpr() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Result getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class CheckSatCommand */
+
+class CVC4_PUBLIC QueryCommand : public Command {
+protected:
+ Expr d_expr;
+ Result d_result;
+ bool d_inUnsatCore;
+public:
+ QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
+ ~QueryCommand() throw() {}
+ Expr getExpr() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Result getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class QueryCommand */
+
+// this is TRANSFORM in the CVC presentation language
+class CVC4_PUBLIC SimplifyCommand : public Command {
+protected:
+ Expr d_term;
+ Expr d_result;
+public:
+ SimplifyCommand(Expr term) throw();
+ ~SimplifyCommand() throw() {}
+ Expr getTerm() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Expr getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class SimplifyCommand */
+
+class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
+protected:
+ Expr d_term;
+ Expr d_result;
+public:
+ ExpandDefinitionsCommand(Expr term) throw();
+ ~ExpandDefinitionsCommand() throw() {}
+ Expr getTerm() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Expr getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class ExpandDefinitionsCommand */
+
+class CVC4_PUBLIC GetValueCommand : public Command {
+protected:
+ std::vector<Expr> d_terms;
+ Expr d_result;
+public:
+ GetValueCommand(Expr term) throw();
+ GetValueCommand(const std::vector<Expr>& terms) throw();
+ ~GetValueCommand() throw() {}
+ const std::vector<Expr>& getTerms() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Expr getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetValueCommand */
+
+class CVC4_PUBLIC GetAssignmentCommand : public Command {
+protected:
+ SExpr d_result;
+public:
+ GetAssignmentCommand() throw();
+ ~GetAssignmentCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ SExpr getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetAssignmentCommand */
+
+class CVC4_PUBLIC GetModelCommand : public Command {
+protected:
+ Model* d_result;
+ SmtEngine* d_smtEngine;
+public:
+ GetModelCommand() throw();
+ ~GetModelCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ // Model is private to the library -- for now
+ //Model* getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetModelCommand */
+
+class CVC4_PUBLIC GetProofCommand : public Command {
+protected:
+ Proof* d_result;
+ SmtEngine* d_smtEngine;
+public:
+ GetProofCommand() throw();
+ ~GetProofCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ Proof* getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetProofCommand */
+
+class CVC4_PUBLIC GetInstantiationsCommand : public Command {
+protected:
+ //Instantiations* d_result;
+ SmtEngine* d_smtEngine;
+public:
+ GetInstantiationsCommand() throw();
+ ~GetInstantiationsCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ //Instantiations* getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetInstantiationsCommand */
+
+class CVC4_PUBLIC GetSynthSolutionCommand : public Command {
+protected:
+ SmtEngine* d_smtEngine;
+public:
+ GetSynthSolutionCommand() throw();
+ ~GetSynthSolutionCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetSynthSolutionCommand */
+
+class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
+protected:
+ UnsatCore d_result;
+ std::map<Expr, std::string> d_names;
+public:
+ GetUnsatCoreCommand() throw();
+ GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw();
+ ~GetUnsatCoreCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ const UnsatCore& getUnsatCore() const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetUnsatCoreCommand */
+
+class CVC4_PUBLIC GetAssertionsCommand : public Command {
+protected:
+ std::string d_result;
+public:
+ GetAssertionsCommand() throw();
+ ~GetAssertionsCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ std::string getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetAssertionsCommand */
+
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
+protected:
+ BenchmarkStatus d_status;
+public:
+ SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
+ ~SetBenchmarkStatusCommand() throw() {}
+ BenchmarkStatus getStatus() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class SetBenchmarkStatusCommand */
+
+class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
+protected:
+ std::string d_logic;
+public:
+ SetBenchmarkLogicCommand(std::string logic) throw();
+ ~SetBenchmarkLogicCommand() throw() {}
+ std::string getLogic() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class SetBenchmarkLogicCommand */
+
+class CVC4_PUBLIC SetInfoCommand : public Command {
+protected:
+ std::string d_flag;
+ SExpr d_sexpr;
+public:
+ SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
+ ~SetInfoCommand() throw() {}
+ std::string getFlag() const throw();
+ SExpr getSExpr() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class SetInfoCommand */
+
+class CVC4_PUBLIC GetInfoCommand : public Command {
+protected:
+ std::string d_flag;
+ std::string d_result;
+public:
+ GetInfoCommand(std::string flag) throw();
+ ~GetInfoCommand() throw() {}
+ std::string getFlag() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ std::string getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetInfoCommand */
+
+class CVC4_PUBLIC SetOptionCommand : public Command {
+protected:
+ std::string d_flag;
+ SExpr d_sexpr;
+public:
+ SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
+ ~SetOptionCommand() throw() {}
+ std::string getFlag() const throw();
+ SExpr getSExpr() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class SetOptionCommand */
+
+class CVC4_PUBLIC GetOptionCommand : public Command {
+protected:
+ std::string d_flag;
+ std::string d_result;
+public:
+ GetOptionCommand(std::string flag) throw();
+ ~GetOptionCommand() throw() {}
+ std::string getFlag() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ std::string getResult() const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class GetOptionCommand */
+
+class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
+private:
+ std::vector<DatatypeType> d_datatypes;
+public:
+ DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
+ ~DatatypeDeclarationCommand() throw() {}
+ DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
+ const std::vector<DatatypeType>& getDatatypes() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class DatatypeDeclarationCommand */
+
+class CVC4_PUBLIC RewriteRuleCommand : public Command {
+public:
+ typedef std::vector< std::vector< Expr > > Triggers;
+protected:
+ typedef std::vector< Expr > VExpr;
+ VExpr d_vars;
+ VExpr d_guards;
+ Expr d_head;
+ Expr d_body;
+ Triggers d_triggers;
+public:
+ RewriteRuleCommand(const std::vector<Expr>& vars,
+ const std::vector<Expr>& guards,
+ Expr head,
+ Expr body,
+ const Triggers& d_triggers) throw();
+ RewriteRuleCommand(const std::vector<Expr>& vars,
+ Expr head,
+ Expr body) throw();
+ ~RewriteRuleCommand() throw() {}
+ const std::vector<Expr>& getVars() const throw();
+ const std::vector<Expr>& getGuards() const throw();
+ Expr getHead() const throw();
+ Expr getBody() const throw();
+ const Triggers& getTriggers() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class RewriteRuleCommand */
+
+class CVC4_PUBLIC PropagateRuleCommand : public Command {
+public:
+ typedef std::vector< std::vector< Expr > > Triggers;
+protected:
+ typedef std::vector< Expr > VExpr;
+ VExpr d_vars;
+ VExpr d_guards;
+ VExpr d_heads;
+ Expr d_body;
+ Triggers d_triggers;
+ bool d_deduction;
+public:
+ PropagateRuleCommand(const std::vector<Expr>& vars,
+ const std::vector<Expr>& guards,
+ const std::vector<Expr>& heads,
+ Expr body,
+ const Triggers& d_triggers,
+ /* true if we want a deduction rule */
+ bool d_deduction = false) throw();
+ PropagateRuleCommand(const std::vector<Expr>& vars,
+ const std::vector<Expr>& heads,
+ Expr body,
+ bool d_deduction = false) throw();
+ ~PropagateRuleCommand() throw() {}
+ const std::vector<Expr>& getVars() const throw();
+ const std::vector<Expr>& getGuards() const throw();
+ const std::vector<Expr>& getHeads() const throw();
+ Expr getBody() const throw();
+ const Triggers& getTriggers() const throw();
+ bool isDeduction() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class PropagateRuleCommand */
+
+class CVC4_PUBLIC ResetCommand : public Command {
+public:
+ ResetCommand() throw() {}
+ ~ResetCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class ResetCommand */
+
+class CVC4_PUBLIC ResetAssertionsCommand : public Command {
+public:
+ ResetAssertionsCommand() throw() {}
+ ~ResetAssertionsCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class ResetAssertionsCommand */
+
+class CVC4_PUBLIC QuitCommand : public Command {
+public:
+ QuitCommand() throw() {}
+ ~QuitCommand() throw() {}
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class QuitCommand */
+
+class CVC4_PUBLIC CommentCommand : public Command {
+ std::string d_comment;
+public:
+ CommentCommand(std::string comment) throw();
+ ~CommentCommand() throw() {}
+ std::string getComment() const throw();
+ void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class CommentCommand */
+
+class CVC4_PUBLIC CommandSequence : public Command {
+private:
+ /** All the commands to be executed (in sequence) */
+ std::vector<Command*> d_commandSequence;
+ /** Next command to be executed */
+ unsigned int d_index;
+public:
+ CommandSequence() throw();
+ ~CommandSequence() throw();
+
+ void addCommand(Command* cmd) throw();
+ void clear() throw();
+
+ void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+
+ typedef std::vector<Command*>::iterator iterator;
+ typedef std::vector<Command*>::const_iterator const_iterator;
+
+ const_iterator begin() const throw();
+ const_iterator end() const throw();
+
+ iterator begin() throw();
+ iterator end() throw();
+
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class CommandSequence */
+
+class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
+public:
+ ~DeclarationSequence() throw() {}
+};/* class DeclarationSequence */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__COMMAND_H */
--- /dev/null
+%{
+#include "smt/command.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const Command&) throw();
+%ignore CVC4::operator<<(std::ostream&, const Command*) throw();
+%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw();
+%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw();
+%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw();
+%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw();
+
+%ignore CVC4::GetProofCommand;
+%ignore CVC4::CommandPrintSuccess::Scope;
+
+#ifdef SWIGJAVA
+
+// Instead of CommandSequence::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%ignore CVC4::CommandSequence::begin();
+%ignore CVC4::CommandSequence::end();
+%ignore CVC4::CommandSequence::begin() const;
+%ignore CVC4::CommandSequence::end() const;
+%extend CVC4::CommandSequence {
+ CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() {
+ return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self);
+ }
+}
+
+// CommandSequence is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "
+ public void remove() {
+ throw new java.lang.UnsupportedOperationException();
+ }
+
+ public edu.nyu.acsys.CVC4.Command next() {
+ if(hasNext()) {
+ return getNext();
+ } else {
+ throw new java.util.NoSuchElementException();
+ }
+ }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private";
+
+// map the types appropriately
+%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject";
+%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
+%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
+%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; }
+
+#endif /* SWIGJAVA */
+
+%include "smt/command.h"
+
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>;
+
+#endif /* SWIGJAVA */
**/
// we include both of these to make sure they agree on the typedef
+#include "smt/command.h"
#include "smt/command_list.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
namespace CVC4 {
namespace smt {
--- /dev/null
+/********************* */
+/*! \file dump.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Dump utility classes and functions
+ **
+ ** Dump utility classes and functions.
+ **/
+#include "smt/dump.h"
+
+#include "base/output.h"
+
+namespace CVC4 {
+
+DumpC DumpChannel CVC4_PUBLIC;
+
+std::ostream& DumpC::setStream(std::ostream* os) {
+ ::CVC4::DumpOutChannel.setStream(os);
+ return *os;
+}
+std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); }
+std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); }
+
+
+void DumpC::setDumpFromString(const std::string& optarg) {
+#ifdef CVC4_DUMPING
+ char* optargPtr = strdup(optarg.c_str());
+ char* tokstr = optargPtr;
+ char* toksave;
+ while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
+ tokstr = NULL;
+ if(!strcmp(optargPtr, "benchmark")) {
+ } else if(!strcmp(optargPtr, "declarations")) {
+ } else if(!strcmp(optargPtr, "assertions")) {
+ Dump.on("assertions:post-everything");
+ } else if(!strncmp(optargPtr, "assertions:", 11)) {
+ const char* p = optargPtr + 11;
+ if(!strncmp(p, "pre-", 4)) {
+ p += 4;
+ } else if(!strncmp(p, "post-", 5)) {
+ p += 5;
+ } else {
+ throw OptionException(std::string("don't know how to dump `") +
+ optargPtr + "'. Please consult --dump help.");
+ }
+ if(!strcmp(p, "everything")) {
+ } else if(!strcmp(p, "definition-expansion")) {
+ } else if(!strcmp(p, "boolean-terms")) {
+ } else if(!strcmp(p, "constrain-subtypes")) {
+ } else if(!strcmp(p, "substitution")) {
+ } else if(!strcmp(p, "strings-pp")) {
+ } else if(!strcmp(p, "skolem-quant")) {
+ } else if(!strcmp(p, "simplify")) {
+ } else if(!strcmp(p, "static-learning")) {
+ } else if(!strcmp(p, "ite-removal")) {
+ } else if(!strcmp(p, "repeat-simplify")) {
+ } else if(!strcmp(p, "rewrite-apply-to-const")) {
+ } else if(!strcmp(p, "theory-preprocessing")) {
+ } else if(!strcmp(p, "nonclausal")) {
+ } else if(!strcmp(p, "theorypp")) {
+ } else if(!strcmp(p, "itesimp")) {
+ } else if(!strcmp(p, "unconstrained")) {
+ } else if(!strcmp(p, "repeatsimp")) {
+ } else {
+ throw OptionException(std::string("don't know how to dump `") +
+ optargPtr + "'. Please consult --dump help.");
+ }
+ Dump.on("assertions");
+ } else if(!strcmp(optargPtr, "skolems")) {
+ } else if(!strcmp(optargPtr, "clauses")) {
+ } else if(!strcmp(optargPtr, "t-conflicts") ||
+ !strcmp(optargPtr, "t-lemmas") ||
+ !strcmp(optargPtr, "t-explanations") ||
+ !strcmp(optargPtr, "bv-rewrites") ||
+ !strcmp(optargPtr, "theory::fullcheck")) {
+ // These are "non-state-dumping" modes. If state (SAT decisions,
+ // propagations, etc.) is dumped, it will interfere with the validity
+ // of these generated queries.
+ if(Dump.isOn("state")) {
+ throw OptionException(std::string("dump option `") + optargPtr +
+ "' conflicts with a previous, "
+ "state-dumping dump option. You cannot "
+ "mix stateful and non-stateful dumping modes; "
+ "see --dump help.");
+ } else {
+ Dump.on("no-permit-state");
+ }
+ } else if(!strcmp(optargPtr, "state") ||
+ !strcmp(optargPtr, "missed-t-conflicts") ||
+ !strcmp(optargPtr, "t-propagations") ||
+ !strcmp(optargPtr, "missed-t-propagations")) {
+ // These are "state-dumping" modes. If state (SAT decisions,
+ // propagations, etc.) is not dumped, it will interfere with the
+ // validity of these generated queries.
+ if(Dump.isOn("no-permit-state")) {
+ throw OptionException(std::string("dump option `") + optargPtr +
+ "' conflicts with a previous, "
+ "non-state-dumping dump option. You cannot "
+ "mix stateful and non-stateful dumping modes; "
+ "see --dump help.");
+ } else {
+ Dump.on("state");
+ }
+ } else if(!strcmp(optargPtr, "help")) {
+ puts(s_dumpHelp.c_str());
+ exit(1);
+ } else if(!strcmp(optargPtr, "bv-abstraction")) {
+ Dump.on("bv-abstraction");
+ } else if(!strcmp(optargPtr, "bv-algebraic")) {
+ Dump.on("bv-algebraic");
+ } else {
+ throw OptionException(std::string("unknown option for --dump: `") +
+ optargPtr + "'. Try --dump help.");
+ }
+
+ Dump.on(optargPtr);
+ Dump.on("benchmark");
+ if(strcmp(optargPtr, "benchmark")) {
+ Dump.on("declarations");
+ if(strcmp(optargPtr, "declarations")) {
+ Dump.on("skolems");
+ }
+ }
+ }
+ free(optargPtr);
+#else /* CVC4_DUMPING */
+ throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+
+const std::string DumpC::s_dumpHelp = "\
+Dump modes currently supported by the --dump option:\n\
+\n\
+benchmark\n\
++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
+ does not include any declarations or assertions. Implied by all following\n\
+ modes.\n\
+\n\
+declarations\n\
++ Dump user declarations. Implied by all following modes.\n\
+\n\
+skolems\n\
++ Dump internally-created skolem variable declarations. These can\n\
+ arise from preprocessing simplifications, existential elimination,\n\
+ and a number of other things. Implied by all following modes.\n\
+\n\
+assertions\n\
++ Output the assertions after preprocessing and before clausification.\n\
+ Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
+ where PASS is one of the preprocessing passes: definition-expansion\n\
+ boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
+ simplify static-learning ite-removal repeat-simplify\n\
+ rewrite-apply-to-const theory-preprocessing.\n\
+ PASS can also be the special value \"everything\", in which case the\n\
+ assertions are printed before any preprocessing (with\n\
+ \"assertions:pre-everything\") or after all preprocessing completes\n\
+ (with \"assertions:post-everything\").\n\
+\n\
+clauses\n\
++ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+ output\n\
+\n\
+state\n\
++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
+ Implied by all \"stateful\" modes below and conflicts with all\n\
+ non-stateful modes below.\n\
+\n\
+t-conflicts [non-stateful]\n\
++ Output correctness queries for all theory conflicts\n\
+\n\
+missed-t-conflicts [stateful]\n\
++ Output completeness queries for theory conflicts\n\
+\n\
+t-propagations [stateful]\n\
++ Output correctness queries for all theory propagations\n\
+\n\
+missed-t-propagations [stateful]\n\
++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
+\n\
+t-lemmas [non-stateful]\n\
++ Output correctness queries for all theory lemmas\n\
+\n\
+t-explanations [non-stateful]\n\
++ Output correctness queries for all theory explanations\n\
+\n\
+bv-rewrites [non-stateful]\n\
++ Output correctness queries for all bitvector rewrites\n\
+\n\
+bv-abstraction [non-stateful]\n\
++ Output correctness queries for all bv abstraction \n\
+\n\
+bv-algebraic [non-stateful]\n\
++ Output correctness queries for bv algebraic solver. \n\
+\n\
+theory::fullcheck [non-stateful]\n \
++ Output completeness queries for all full-check effort-level theory checks\n\
+\n\
+Dump modes can be combined with multiple uses of --dump. Generally you want\n\
+one from the assertions category (either assertions or clauses), and\n\
+perhaps one or more stateful or non-stateful modes for checking correctness\n\
+and completeness of decision procedure implementations. Stateful modes dump\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
+\n\
+The --output-language option controls the language used for dumping, and\n\
+this allows you to connect CVC4 to another solver implementation via a UNIX\n\
+pipe to perform on-line checking. The --dump-to option can be used to dump\n\
+to a file.\n\
+";
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file dump.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Dump utility classes and functions
+ **
+ ** Dump utility classes and functions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__DUMP_H
+#define __CVC4__DUMP_H
+
+#include "base/output.h"
+#include "smt/command.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC CVC4dumpstream {
+
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ std::ostream* d_os;
+#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
+
+#ifdef CVC4_PORTFOLIO
+ CommandSequence* d_commands;
+#endif /* CVC4_PORTFOLIO */
+
+public:
+ CVC4dumpstream() throw()
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
+ : d_os(NULL), d_commands(NULL)
+#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ : d_os(NULL)
+#elif defined(CVC4_PORTFOLIO)
+ : d_commands(NULL)
+#endif /* CVC4_PORTFOLIO */
+ { }
+
+ CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw()
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
+ : d_os(&os), d_commands(&commands)
+#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ : d_os(&os)
+#elif defined(CVC4_PORTFOLIO)
+ : d_commands(&commands)
+#endif /* CVC4_PORTFOLIO */
+ { }
+
+ CVC4dumpstream& operator<<(const Command& c) {
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ if(d_os != NULL) {
+ (*d_os) << c << std::endl;
+ }
+#endif
+#if defined(CVC4_PORTFOLIO)
+ if(d_commands != NULL) {
+ d_commands->addCommand(c.clone());
+ }
+#endif
+ return *this;
+ }
+};/* class CVC4dumpstream */
+
+/** The dump class */
+class CVC4_PUBLIC DumpC {
+ std::set<std::string> d_tags;
+ CommandSequence d_commands;
+
+ static const std::string s_dumpHelp;
+
+public:
+ CVC4dumpstream operator()(const char* tag) {
+ if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+ return CVC4dumpstream(getStream(), d_commands);
+ } else {
+ return CVC4dumpstream();
+ }
+ }
+
+ CVC4dumpstream operator()(std::string tag) {
+ if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+ return CVC4dumpstream(getStream(), d_commands);
+ } else {
+ return CVC4dumpstream();
+ }
+ }
+
+ void clear() { d_commands.clear(); }
+ const CommandSequence& getCommands() const { return d_commands; }
+
+ bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+ bool on (std::string tag) { d_tags.insert(tag); return true; }
+ bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+ bool off(std::string tag) { d_tags.erase (tag); return false; }
+ bool off() { d_tags.clear(); return false; }
+
+ bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+ bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+ std::ostream& setStream(std::ostream* os);
+ std::ostream& getStream();
+ std::ostream* getStreamPointer();
+
+ void setDumpFromString(const std::string& optarg);
+};/* class DumpC */
+
+/** The dump singleton */
+extern DumpC DumpChannel CVC4_PUBLIC;
+
+#define Dump ::CVC4::DumpChannel
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DUMP_H */
--- /dev/null
+/********************* */
+/*! \file ite_removal.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: Tim King, Morgan Deters
+ ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Removal of term ITEs
+ **
+ ** Removal of term ITEs.
+ **/
+#include "smt/ite_removal.h"
+
+#include <vector>
+
+#include "proof/proof_manager.h"
+#include "theory/ite_utilities.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+RemoveITE::RemoveITE(context::UserContext* u)
+ : d_iteCache(u)
+{
+ d_containsVisitor = new theory::ContainsTermITEVisitor();
+}
+
+RemoveITE::~RemoveITE(){
+ delete d_containsVisitor;
+}
+
+void RemoveITE::garbageCollect(){
+ d_containsVisitor->garbageCollect();
+}
+
+theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
+ return d_containsVisitor;
+}
+
+size_t RemoveITE::collectedCacheSizes() const{
+ return d_containsVisitor->cache_size() + d_iteCache.size();
+}
+
+void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
+{
+ size_t n = output.size();
+ for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
+ // Do this in two steps to avoid Node problems(?)
+ // Appears related to bug 512, splitting this into two lines
+ // fixes the bug on clang on Mac OS
+ Node itesRemoved = run(output[i], output, iteSkolemMap, false);
+ // In some calling contexts, not necessary to report dependence information.
+ if(reportDeps && options::unsatCores()) {
+ // new assertions have a dependence on the node
+ PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
+ while(n < output.size()) {
+ PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
+ ++n;
+ }
+ }
+ output[i] = itesRemoved;
+ }
+}
+
+bool RemoveITE::containsTermITE(TNode e) const {
+ return d_containsVisitor->containsTermITE(e);
+}
+
+Node RemoveITE::run(TNode node, std::vector<Node>& output,
+ IteSkolemMap& iteSkolemMap, bool inQuant) {
+ // Current node
+ Debug("ite") << "removeITEs(" << node << ")" << endl;
+
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
+ // The result may be cached already
+ std::pair<Node, bool> cacheKey(node, inQuant);
+ NodeManager *nodeManager = NodeManager::currentNM();
+ ITECache::const_iterator i = d_iteCache.find(cacheKey);
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ Debug("ite") << "removeITEs: in-cache: " << cached << endl;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
+ }
+
+ // If an ITE replace it
+ if(node.getKind() == kind::ITE) {
+ TypeNode nodeType = node.getType();
+ if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
+ Node skolem;
+ // Make the skolem to represent the ITE
+ skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
+
+ // The new assertion
+ Node newAssertion =
+ nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
+ skolem.eqNode(node[2]));
+ Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
+
+ // Attach the skolem
+ d_iteCache.insert(cacheKey, skolem);
+
+ // Remove ITEs from the new assertion, rewrite it and push it to the output
+ newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
+
+ iteSkolemMap[skolem] = output.size();
+ output.push_back(newAssertion);
+
+ // The representation is now the skolem
+ return skolem;
+ }
+ }
+
+ // If not an ITE, go deep
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Remove the ITEs from the children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = run(*it, output, iteSkolemMap, inQuant);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache.insert(cacheKey, cached);
+ return cached;
+ } else {
+ d_iteCache.insert(cacheKey, Node::null());
+ return node;
+ }
+}
+
+Node RemoveITE::replace(TNode node, bool inQuant) const {
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
+ // Check the cache
+ NodeManager *nodeManager = NodeManager::currentNM();
+ ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
+ }
+
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Replace in children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = replace(*it, inQuant);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ return nodeManager->mkNode(node.getKind(), newChildren);
+ } else {
+ return node;
+ }
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file ite_removal.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters
+ ** Minor contributors (to current version): Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Removal of term ITEs
+ **
+ ** Removal of term ITEs.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+
+#include "context/cdinsert_hashmap.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "smt/dump.h"
+#include "util/bool.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+
+namespace theory {
+ class ContainsTermITEVisitor;
+}/* CVC4::theory namespace */
+
+typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
+
+class RemoveITE {
+ typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
+ ITECache d_iteCache;
+
+
+public:
+
+ RemoveITE(context::UserContext* u);
+ ~RemoveITE();
+
+ /**
+ * Removes the ITE nodes by introducing skolem variables. All
+ * additional assertions are pushed into assertions. iteSkolemMap
+ * contains a map from introduced skolem variables to the index in
+ * assertions containing the new Boolean ite created in conjunction
+ * with that skolem variable.
+ *
+ * With reportDeps true, report reasoning dependences to the proof
+ * manager (for unsat cores).
+ */
+ void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
+
+ /**
+ * Removes the ITE from the node by introducing skolem
+ * variables. All additional assertions are pushed into
+ * assertions. iteSkolemMap contains a map from introduced skolem
+ * variables to the index in assertions containing the new Boolean
+ * ite created in conjunction with that skolem variable.
+ */
+ Node run(TNode node, std::vector<Node>& additionalAssertions,
+ IteSkolemMap& iteSkolemMap, bool inQuant);
+
+ /**
+ * Substitute under node using pre-existing cache. Do not remove
+ * any ITEs not seen during previous runs.
+ */
+ Node replace(TNode node, bool inQuant = false) const;
+
+ /** Returns true if e contains a term ite. */
+ bool containsTermITE(TNode e) const;
+
+ /** Returns the collected size of the caches. */
+ size_t collectedCacheSizes() const;
+
+ /** Garbage collects non-context dependent data-structures. */
+ void garbageCollect();
+
+ /** Return the RemoveITE's containsVisitor. */
+ theory::ContainsTermITEVisitor* getContainsVisitor();
+
+private:
+ theory::ContainsTermITEVisitor* d_containsVisitor;
+
+};/* class RemoveTTE */
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file model.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief implementation of Model class
+ **/
+
+#include "smt/model.h"
+
+#include <vector>
+
+#include "expr/expr_iomanip.h"
+#include "options/base_options.h"
+#include "printer/printer.h"
+#include "smt/command.h"
+#include "smt/command_list.h"
+#include "smt/smt_engine_scope.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const Model& m) {
+ smt::SmtScope smts(&m.d_smt);
+ expr::ExprDag::Scope scope(out, false);
+ Printer::getPrinter(options::outputLanguage())->toStream(out, m);
+ return out;
+}
+
+Model::Model() :
+ d_smt(*smt::currentSmtEngine()) {
+}
+
+size_t Model::getNumCommands() const {
+ return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
+}
+
+const Command* Model::getCommand(size_t i) const {
+ Assert(i < getNumCommands());
+ // index the global commands first, then the locals
+ if(i < d_smt.d_modelGlobalCommands.size()) {
+ return d_smt.d_modelGlobalCommands[i];
+ } else {
+ return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
+ }
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file model.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MODEL_H
+#define __CVC4__MODEL_H
+
+#include <iosfwd>
+#include <vector>
+
+#include "expr/expr.h"
+#include "util/cardinality.h"
+
+namespace CVC4 {
+
+class Command;
+class SmtEngine;
+class Model;
+
+std::ostream& operator<<(std::ostream&, const Model&);
+
+class Model {
+ friend std::ostream& operator<<(std::ostream&, const Model&);
+ friend class SmtEngine;
+
+ /** the input name (file name, etc.) this model is associated to */
+ std::string d_inputName;
+
+protected:
+ /** The SmtEngine we're associated with */
+ SmtEngine& d_smt;
+
+ /** construct the base class; users cannot do this, only CVC4 internals */
+ Model();
+
+public:
+ /** virtual destructor */
+ virtual ~Model() { }
+ /** get number of commands to report */
+ size_t getNumCommands() const;
+ /** get command */
+ const Command* getCommand(size_t i) const;
+ /** get the smt engine that this model is hooked up to */
+ SmtEngine* getSmtEngine() { return &d_smt; }
+ /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
+ const SmtEngine* getSmtEngine() const { return &d_smt; }
+ /** get the input name (file name, etc.) this model is associated to */
+ std::string getInputName() const { return d_inputName; }
+
+public:
+ /** get value for expression */
+ virtual Expr getValue(Expr expr) const = 0;
+ /** get cardinality for sort */
+ virtual Cardinality getCardinality(Type t) const = 0;
+};/* class Model */
+
+class ModelBuilder {
+public:
+ ModelBuilder() { }
+ virtual ~ModelBuilder() { }
+ virtual void buildModel(Model* m, bool fullModel) = 0;
+};/* class ModelBuilder */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MODEL_H */
#include "proof/unsat_core.h"
#include "prop/prop_engine.h"
#include "smt/boolean_terms.h"
+#include "smt/command.h"
#include "smt/command_list.h"
+#include "smt/ite_removal.h"
#include "smt/logic_request.h"
#include "smt/managed_ostreams.h"
#include "smt/model_postprocessor.h"
#include "smt/smt_engine_scope.h"
#include "smt/update_ostream.h"
#include "smt_util/boolean_simplification.h"
-#include "smt_util/command.h"
-#include "smt_util/ite_removal.h"
#include "smt_util/nary_builder.h"
#include "smt_util/node_visitor.h"
#include "theory/arith/pseudoboolean_proc.h"
#include "options/language.h"
#include "options/set_language.h"
#include "options/base_options.h"
-#include "smt_util/dump.h"
+#include "smt/dump.h"
namespace CVC4 {
Makefile.in \
boolean_simplification.cpp \
boolean_simplification.h \
- command.cpp \
- command.h \
- dump.cpp \
- dump.h \
- ite_removal.cpp \
- ite_removal.h \
lemma_channels.cpp \
lemma_channels.h \
lemma_input_channel.h \
lemma_output_channel.h \
- model.cpp \
- model.h \
nary_builder.cpp \
nary_builder.h \
node_visitor.h
-
-EXTRA_DIST = \
- command.i
-
+++ /dev/null
-/********************* */
-/*! \file command.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of command objects.
- **
- ** Implementation of command objects.
- **/
-
-#include "smt_util/command.h"
-
-#include <exception>
-#include <iostream>
-#include <iterator>
-#include <sstream>
-#include <utility>
-#include <vector>
-
-#include "base/cvc4_assert.h"
-#include "base/output.h"
-#include "expr/expr_iomanip.h"
-#include "expr/node.h"
-#include "options/options.h"
-#include "options/smt_options.h"
-#include "printer/printer.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "smt_util/dump.h"
-#include "smt_util/model.h"
-#include "util/sexpr.h"
-
-using namespace std;
-
-namespace CVC4 {
-
-const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
-const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
-const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted();
-
-std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
- 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) {
- out << "null";
- } else {
- out << *c;
- }
- return out;
-}
-
-std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() {
- s.toStream(out, Node::setlanguage::getLanguage(out));
- return out;
-}
-
-ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
- if(s == NULL) {
- out << "null";
- } else {
- out << *s;
- }
- return out;
-}
-
-/* class Command */
-
-Command::Command() throw() : d_commandStatus(NULL), d_muted(false) {
-}
-
-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()) {
- delete d_commandStatus;
- }
-}
-
-bool Command::ok() const throw() {
- // either we haven't run the command yet, or it ran successfully
- 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::interrupted() const throw() {
- return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
-}
-
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
- invoke(smtEngine);
- if(!(isMuted() && ok())) {
- printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
- }
-}
-
-std::string Command::toString() const throw() {
- 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() {
- Printer::getPrinter(language)->toStream(out, this);
-}
-
-void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- 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;
-}
-
-void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
- /* 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 */
-
-EchoCommand::EchoCommand(std::string output) throw() :
- d_output(output) {
-}
-
-std::string EchoCommand::getOutput() const throw() {
- return d_output;
-}
-
-void EchoCommand::invoke(SmtEngine* smtEngine) throw() {
- /* we don't have an output stream here, nothing to do */
- d_commandStatus = CommandSuccess::instance();
-}
-
-void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
- out << 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);
-}
-
-Command* EchoCommand::clone() const {
- return new EchoCommand(d_output);
-}
-
-std::string EchoCommand::getCommandName() const throw() {
- return "echo";
-}
-
-/* class AssertCommand */
-
-AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() :
- d_expr(e), d_inUnsatCore(inUnsatCore) {
-}
-
-Expr AssertCommand::getExpr() const throw() {
- return d_expr;
-}
-
-void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->assertFormula(d_expr, d_inUnsatCore);
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } 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_expr, d_inUnsatCore);
-}
-
-std::string AssertCommand::getCommandName() const throw() {
- return "assert";
-}
-
-/* class PushCommand */
-
-void PushCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->push();
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } 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 throw() {
- return "push";
-}
-
-/* class PopCommand */
-
-void PopCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->pop();
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new PopCommand();
-}
-
-Command* PopCommand::clone() const {
- return new PopCommand();
-}
-
-std::string PopCommand::getCommandName() const throw() {
- return "pop";
-}
-
-/* class CheckSatCommand */
-
-CheckSatCommand::CheckSatCommand() throw() :
- d_expr() {
-}
-
-CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() :
- d_expr(expr), d_inUnsatCore(inUnsatCore) {
-}
-
-Expr CheckSatCommand::getExpr() const throw() {
- return d_expr;
-}
-
-void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- d_result = smtEngine->checkSat(d_expr);
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Result CheckSatCommand::getResult() const throw() {
- return d_result;
-}
-
-void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result << endl;
- }
-}
-
-Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
- 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 CheckSatCommand::getCommandName() const throw() {
- return "check-sat";
-}
-
-/* class QueryCommand */
-
-QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() :
- d_expr(e), d_inUnsatCore(inUnsatCore) {
-}
-
-Expr QueryCommand::getExpr() const throw() {
- return d_expr;
-}
-
-void QueryCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- d_result = smtEngine->query(d_expr);
- d_commandStatus = CommandSuccess::instance();
- } 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 throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result << endl;
- }
-}
-
-Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), 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 throw() {
- return "query";
-}
-
-/* class ResetCommand */
-
-void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->reset();
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new ResetCommand();
-}
-
-Command* ResetCommand::clone() const {
- return new ResetCommand();
-}
-
-std::string ResetCommand::getCommandName() const throw() {
- return "reset";
-}
-
-/* class ResetAssertionsCommand */
-
-void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->resetAssertions();
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new ResetAssertionsCommand();
-}
-
-Command* ResetAssertionsCommand::clone() const {
- return new ResetAssertionsCommand();
-}
-
-std::string ResetAssertionsCommand::getCommandName() const throw() {
- return "reset-assertions";
-}
-
-/* class QuitCommand */
-
-void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("benchmark") << *this;
- d_commandStatus = CommandSuccess::instance();
-}
-
-Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new QuitCommand();
-}
-
-Command* QuitCommand::clone() const {
- return new QuitCommand();
-}
-
-std::string QuitCommand::getCommandName() const throw() {
- return "exit";
-}
-
-/* class CommentCommand */
-
-CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
-}
-
-std::string CommentCommand::getComment() const throw() {
- return d_comment;
-}
-
-void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("benchmark") << *this;
- d_commandStatus = CommandSuccess::instance();
-}
-
-Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new CommentCommand(d_comment);
-}
-
-Command* CommentCommand::clone() const {
- return new CommentCommand(d_comment);
-}
-
-std::string CommentCommand::getCommandName() const throw() {
- return "comment";
-}
-
-/* class CommandSequence */
-
-CommandSequence::CommandSequence() throw() :
- d_index(0) {
-}
-
-CommandSequence::~CommandSequence() throw() {
- for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
- delete d_commandSequence[i];
- }
-}
-
-void CommandSequence::addCommand(Command* cmd) throw() {
- d_commandSequence.push_back(cmd);
-}
-
-void CommandSequence::clear() throw() {
- d_commandSequence.clear();
-}
-
-void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
- for(; d_index < d_commandSequence.size(); ++d_index) {
- d_commandSequence[d_index]->invoke(smtEngine);
- if(! d_commandSequence[d_index]->ok()) {
- // abort execution
- d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
- return;
- }
- delete d_commandSequence[d_index];
- }
-
- AlwaysAssert(d_commandStatus == NULL);
- d_commandStatus = CommandSuccess::instance();
-}
-
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
- for(; d_index < d_commandSequence.size(); ++d_index) {
- d_commandSequence[d_index]->invoke(smtEngine, out);
- if(! d_commandSequence[d_index]->ok()) {
- // abort execution
- d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
- return;
- }
- delete d_commandSequence[d_index];
- }
-
- AlwaysAssert(d_commandStatus == NULL);
- 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 {
- CommandSequence* seq = new CommandSequence();
- 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() {
- return d_commandSequence.begin();
-}
-
-CommandSequence::const_iterator CommandSequence::end() const throw() {
- return d_commandSequence.end();
-}
-
-CommandSequence::iterator CommandSequence::begin() throw() {
- return d_commandSequence.begin();
-}
-
-CommandSequence::iterator CommandSequence::end() throw() {
- return d_commandSequence.end();
-}
-
-std::string CommandSequence::getCommandName() const throw() {
- return "sequence";
-}
-
-/* class DeclarationSequenceCommand */
-
-/* class DeclarationDefinitionCommand */
-
-DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() :
- d_symbol(id) {
-}
-
-std::string DeclarationDefinitionCommand::getSymbol() const throw() {
- return d_symbol;
-}
-
-/* class DeclareFunctionCommand */
-
-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){
-}
-
-Expr DeclareFunctionCommand::getFunction() const throw() {
- return d_func;
-}
-
-Type DeclareFunctionCommand::getType() const throw() {
- return d_type;
-}
-
-bool DeclareFunctionCommand::getPrintInModel() const throw() {
- return d_printInModel;
-}
-
-bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() {
- return d_printInModelSetByUser;
-}
-
-void DeclareFunctionCommand::setPrintInModel( bool p ) {
- d_printInModel = p;
- d_printInModelSetByUser = true;
-}
-
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- 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);
- dfc->d_printInModel = d_printInModel;
- dfc->d_printInModelSetByUser = d_printInModelSetByUser;
- return dfc;
-}
-
-std::string DeclareFunctionCommand::getCommandName() const throw() {
- 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) {
-}
-
-size_t DeclareTypeCommand::getArity() const throw() {
- return d_arity;
-}
-
-Type DeclareTypeCommand::getType() const throw() {
- return d_type;
-}
-
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- d_commandStatus = CommandSuccess::instance();
-}
-
-Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) {
- return new DeclareTypeCommand(d_symbol, d_arity,
- d_type.exportTo(exprManager, variableMap));
-}
-
-Command* DeclareTypeCommand::clone() const {
- return new DeclareTypeCommand(d_symbol, d_arity, d_type);
-}
-
-std::string DeclareTypeCommand::getCommandName() const throw() {
- return "declare-sort";
-}
-
-/* class DefineTypeCommand */
-
-DefineTypeCommand::DefineTypeCommand(const std::string& id,
- Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_params(),
- d_type(t) {
-}
-
-DefineTypeCommand::DefineTypeCommand(const std::string& id,
- const std::vector<Type>& params,
- Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_params(params),
- d_type(t) {
-}
-
-const std::vector<Type>& DefineTypeCommand::getParameters() const throw() {
- return d_params;
-}
-
-Type DefineTypeCommand::getType() const throw() {
- return d_type;
-}
-
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- 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* DefineTypeCommand::clone() const {
- return new DefineTypeCommand(d_symbol, d_params, d_type);
-}
-
-std::string DefineTypeCommand::getCommandName() const throw() {
- return "define-sort";
-}
-
-/* class DefineFunctionCommand */
-
-DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
- Expr func,
- Expr formula) throw() :
- DeclarationDefinitionCommand(id),
- d_func(func),
- d_formals(),
- d_formula(formula) {
-}
-
-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() {
- return d_formals;
-}
-
-Expr DefineFunctionCommand::getFormula() const throw() {
- return d_formula;
-}
-
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- if(!d_func.isNull()) {
- smtEngine->defineFunction(d_func, d_formals, d_formula);
- }
- d_commandStatus = CommandSuccess::instance();
- } 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);
-}
-
-std::string DefineFunctionCommand::getCommandName() const throw() {
- return "define-fun";
-}
-
-/* class DefineNamedFunctionCommand */
-
-DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula) throw() :
- DefineFunctionCommand(id, func, formals, formula) {
-}
-
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- 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();
-}
-
-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);
-}
-
-Command* DefineNamedFunctionCommand::clone() const {
- return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
-}
-
-/* class SetUserAttribute */
-
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() :
- d_attr( attr ), d_expr( expr ){
-}
-
-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() );
-}
-
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
- const std::string& value ) throw() :
- d_attr( attr ), d_expr( expr ), d_str_value( value ){
-}
-
-void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
- try {
- if(!d_expr.isNull()) {
- smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
- }
- d_commandStatus = CommandSuccess::instance();
- } 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* 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 SetUserAttributeCommand::getCommandName() const throw() {
- return "set-user-attribute";
-}
-
-/* class SimplifyCommand */
-
-SimplifyCommand::SimplifyCommand(Expr term) throw() :
- d_term(term) {
-}
-
-Expr SimplifyCommand::getTerm() const throw() {
- return d_term;
-}
-
-void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
- 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());
- }
-}
-
-Expr SimplifyCommand::getResult() const throw() {
- return d_result;
-}
-
-void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result << endl;
- }
-}
-
-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;
-}
-
-Command* SimplifyCommand::clone() const {
- SimplifyCommand* c = new SimplifyCommand(d_term);
- c->d_result = d_result;
- return c;
-}
-
-std::string SimplifyCommand::getCommandName() const throw() {
- return "simplify";
-}
-
-/* class ExpandDefinitionsCommand */
-
-ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() :
- d_term(term) {
-}
-
-Expr ExpandDefinitionsCommand::getTerm() const throw() {
- return d_term;
-}
-
-void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() {
- d_result = smtEngine->expandDefinitions(d_term);
- d_commandStatus = CommandSuccess::instance();
-}
-
-Expr ExpandDefinitionsCommand::getResult() const throw() {
- return d_result;
-}
-
-void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result << endl;
- }
-}
-
-Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
- c->d_result = d_result.exportTo(exprManager, variableMap);
- return c;
-}
-
-Command* ExpandDefinitionsCommand::clone() const {
- ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
- c->d_result = d_result;
- return c;
-}
-
-std::string ExpandDefinitionsCommand::getCommandName() const throw() {
- return "expand-definitions";
-}
-
-/* class GetValueCommand */
-
-GetValueCommand::GetValueCommand(Expr term) throw() :
- 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");
-}
-
-const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
- return d_terms;
-}
-
-void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
- 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());
- }
- d_result = em->mkExpr(kind::SEXPR, result);
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } 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 throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } 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 {
- 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) throw() {
- try {
- d_result = smtEngine->getAssignment();
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } 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 throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result << endl;
- }
-}
-
-Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- 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() {
- return "get-assignment";
-}
-
-/* class GetModelCommand */
-
-GetModelCommand::GetModelCommand() throw() {
-}
-
-void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- d_result = smtEngine->getModel();
- d_smtEngine = smtEngine;
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-/* Model is private to the library -- for now
-Model* GetModelCommand::getResult() const throw() {
- return d_result;
-}
-*/
-
-void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << *d_result;
- }
-}
-
-Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- 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;
- return c;
-}
-
-std::string GetModelCommand::getCommandName() const throw() {
- return "get-model";
-}
-
-/* class GetProofCommand */
-
-GetProofCommand::GetProofCommand() throw() {
-}
-
-void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- d_smtEngine = smtEngine;
- d_result = smtEngine->getProof();
- d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
- d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Proof* GetProofCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- smt::SmtScope scope(d_smtEngine);
- d_result->toStream(out);
- }
-}
-
-Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetProofCommand* c = new GetProofCommand();
- c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
-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";
-}
-
-/* class GetInstantiationsCommand */
-
-GetInstantiationsCommand::GetInstantiationsCommand() throw() {
-}
-
-void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- d_smtEngine = smtEngine;
- d_commandStatus = CommandSuccess::instance();
- } 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 throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- d_smtEngine->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 {
- GetInstantiationsCommand* c = new GetInstantiationsCommand();
- //c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
-std::string GetInstantiationsCommand::getCommandName() const throw() {
- return "get-instantiations";
-}
-
-/* class GetSynthSolutionCommand */
-
-GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
-}
-
-void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- d_smtEngine = smtEngine;
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- d_smtEngine->printSynthSolution(out);
- }
-}
-
-Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
-Command* GetSynthSolutionCommand::clone() const {
- GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
-std::string GetSynthSolutionCommand::getCommandName() const throw() {
- return "get-instantiations";
-}
-
-/* class GetUnsatCoreCommand */
-
-GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
-}
-
-GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
-}
-
-void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- d_result = smtEngine->getUnsatCore();
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- d_result.toStream(out, d_names);
- }
-}
-
-const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() {
- // 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);
- c->d_result = d_result;
- return c;
-}
-
-std::string GetUnsatCoreCommand::getCommandName() const throw() {
- return "get-unsat-core";
-}
-
-/* class GetAssertionsCommand */
-
-GetAssertionsCommand::GetAssertionsCommand() throw() {
-}
-
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- stringstream ss;
- const vector<Expr> v = smtEngine->getAssertions();
- ss << "(\n";
- copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
- ss << ")\n";
- d_result = ss.str();
- d_commandStatus = CommandSuccess::instance();
- } 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 throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else {
- out << d_result;
- }
-}
-
-Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- 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 throw() {
- return "get-assertions";
-}
-
-/* class SetBenchmarkStatusCommand */
-
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
- d_status(status) {
-}
-
-BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
- return d_status;
-}
-
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- stringstream ss;
- ss << d_status;
- SExpr status = SExpr(ss.str());
- smtEngine->setInfo("status", status);
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new SetBenchmarkStatusCommand(d_status);
-}
-
-Command* SetBenchmarkStatusCommand::clone() const {
- return new SetBenchmarkStatusCommand(d_status);
-}
-
-std::string SetBenchmarkStatusCommand::getCommandName() const throw() {
- return "set-info";
-}
-
-/* class SetBenchmarkLogicCommand */
-
-SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
- d_logic(logic) {
-}
-
-std::string SetBenchmarkLogicCommand::getLogic() const throw() {
- return d_logic;
-}
-
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->setLogic(d_logic);
- d_commandStatus = CommandSuccess::instance();
- } 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 {
- return new SetBenchmarkLogicCommand(d_logic);
-}
-
-std::string SetBenchmarkLogicCommand::getCommandName() const throw() {
- return "set-logic";
-}
-
-/* class SetInfoCommand */
-
-SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
- d_flag(flag),
- d_sexpr(sexpr) {
-}
-
-std::string SetInfoCommand::getFlag() const throw() {
- return d_flag;
-}
-
-SExpr SetInfoCommand::getSExpr() const throw() {
- return d_sexpr;
-}
-
-void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->setInfo(d_flag, d_sexpr);
- d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
- // As per SMT-LIB spec, silently accept unknown set-info keys
- d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- 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 */
-
-GetInfoCommand::GetInfoCommand(std::string flag) throw() :
- d_flag(flag) {
-}
-
-std::string GetInfoCommand::getFlag() const throw() {
- return d_flag;
-}
-
-void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- vector<SExpr> v;
- v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
- v.push_back(smtEngine->getInfo(d_flag));
- stringstream ss;
- 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&) {
- d_commandStatus = new CommandUnsupported();
- } 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 throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else if(d_result != "") {
- out << d_result << endl;
- }
-}
-
-Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- 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 throw() {
- return "get-info";
-}
-
-/* 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;
-}
-
-SExpr SetOptionCommand::getSExpr() const throw() {
- return d_sexpr;
-}
-
-void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
- try {
- smtEngine->setOption(d_flag, d_sexpr);
- d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
- d_commandStatus = new CommandUnsupported();
- } catch(exception& e) {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new SetOptionCommand(d_flag, d_sexpr);
-}
-
-Command* SetOptionCommand::clone() const {
- return new SetOptionCommand(d_flag, d_sexpr);
-}
-
-std::string SetOptionCommand::getCommandName() const throw() {
- return "set-option";
-}
-
-/* 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) throw() {
- try {
- SExpr res = smtEngine->getOption(d_flag);
- d_result = res.toString();
- d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
- d_commandStatus = new CommandUnsupported();
- } 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 throw() {
- if(! ok()) {
- this->Command::printResult(out, verbosity);
- } else if(d_result != "") {
- out << d_result << endl;
- }
-}
-
-Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- 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 throw() {
- return "get-option";
-}
-
-/* class DatatypeDeclarationCommand */
-
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
- d_datatypes() {
- d_datatypes.push_back(datatype);
-}
-
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
- d_datatypes(datatypes) {
-}
-
-const std::vector<DatatypeType>&
-DatatypeDeclarationCommand::getDatatypes() const throw() {
- return d_datatypes;
-}
-
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
- d_commandStatus = CommandSuccess::instance();
-}
-
-Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- throw ExportUnsupportedException
- ("export of DatatypeDeclarationCommand unsupported");
-}
-
-Command* DatatypeDeclarationCommand::clone() const {
- return new DatatypeDeclarationCommand(d_datatypes);
-}
-
-std::string DatatypeDeclarationCommand::getCommandName() const throw() {
- 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) throw() {
- 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) throw() {
- 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!]";
- }
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file command.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of the command pattern on SmtEngines.
- **
- ** Implementation of the command pattern on SmtEngines. Command
- ** objects are generated by the parser (typically) to implement the
- ** commands in parsed input (see Parser::parseNextCommand()), or by
- ** client code.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__COMMAND_H
-#define __CVC4__COMMAND_H
-
-#include <iosfwd>
-#include <map>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#include "expr/datatype.h"
-#include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/variable_type_map.h"
-#include "proof/unsat_core.h"
-#include "util/proof.h"
-#include "util/result.h"
-#include "util/sexpr.h"
-
-namespace CVC4 {
-
-class SmtEngine;
-class Command;
-class CommandStatus;
-class Model;
-
-std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
-
-/** The status an SMT benchmark can have */
-enum BenchmarkStatus {
- /** Benchmark is satisfiable */
- SMT_SATISFIABLE,
- /** Benchmark is unsatisfiable */
- SMT_UNSATISFIABLE,
- /** The status of the benchmark is unknown */
- SMT_UNKNOWN
-};/* enum BenchmarkStatus */
-
-std::ostream& operator<<(std::ostream& out,
- BenchmarkStatus status) throw() CVC4_PUBLIC;
-
-/**
- * IOStream manipulator to print success messages or not.
- *
- * out << Command::printsuccess(false) << CommandSuccess();
- *
- * prints nothing, but
- *
- * out << Command::printsuccess(true) << CommandSuccess();
- *
- * prints a success message (in a manner appropriate for the current
- * output language).
- */
-class CVC4_PUBLIC CommandPrintSuccess {
- /**
- * The allocated index in ios_base for our depth setting.
- */
- static const int s_iosIndex;
-
- /**
- * The default setting, for ostreams that haven't yet had a
- * setdepth() applied to them.
- */
- static const int s_defaultPrintSuccess = false;
-
- /**
- * When this manipulator is used, the setting is stored here.
- */
- bool d_printSuccess;
-
-public:
- /**
- * Construct a CommandPrintSuccess with the given setting.
- */
- CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}
-
- inline void applyPrintSuccess(std::ostream& out) throw() {
- out.iword(s_iosIndex) = d_printSuccess;
- }
-
- static inline bool getPrintSuccess(std::ostream& out) throw() {
- return out.iword(s_iosIndex);
- }
-
- static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
- out.iword(s_iosIndex) = printSuccess;
- }
-
- /**
- * Set the print-success state on the output stream for the current
- * stack scope. This makes sure the old state is reset on the
- * stream after normal OR exceptional exit from the scope, using the
- * RAII C++ idiom.
- */
- class Scope {
- std::ostream& d_out;
- bool d_oldPrintSuccess;
-
- public:
-
- inline Scope(std::ostream& out, bool printSuccess) throw() :
- d_out(out),
- d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
- CommandPrintSuccess::setPrintSuccess(out, printSuccess);
- }
-
- inline ~Scope() throw() {
- CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
- }
-
- };/* class CommandPrintSuccess::Scope */
-
-};/* class CommandPrintSuccess */
-
-/**
- * Sets the default print-success setting when pretty-printing an Expr
- * to an ostream. Use like this:
- *
- * // let out be an ostream, e an Expr
- * out << Expr::setdepth(n) << e << endl;
- *
- * The depth stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
- cps.applyPrintSuccess(out);
- return out;
-}
-
-class CVC4_PUBLIC CommandStatus {
-protected:
- // shouldn't construct a CommandStatus (use a derived class)
- CommandStatus() throw() {}
-public:
- virtual ~CommandStatus() throw() {}
- void toStream(std::ostream& out,
- OutputLanguage language = language::output::LANG_AUTO) const throw();
- virtual CommandStatus& clone() const = 0;
-};/* class CommandStatus */
-
-class CVC4_PUBLIC CommandSuccess : public CommandStatus {
- static const CommandSuccess* s_instance;
-public:
- static const CommandSuccess* instance() throw() { return s_instance; }
- CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
-};/* class CommandSuccess */
-
-class CVC4_PUBLIC CommandInterrupted : public CommandStatus {
- static const CommandInterrupted* s_instance;
-public:
- static const CommandInterrupted* instance() throw() { return s_instance; }
- CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); }
-};/* class CommandInterrupted */
-
-class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
-public:
- CommandStatus& clone() const { return *new CommandUnsupported(*this); }
-};/* class CommandSuccess */
-
-class CVC4_PUBLIC CommandFailure : public CommandStatus {
- std::string d_message;
-public:
- CommandFailure(std::string message) throw() : d_message(message) {}
- CommandFailure& clone() const { return *new CommandFailure(*this); }
- ~CommandFailure() throw() {}
- std::string getMessage() const throw() { return d_message; }
-};/* class CommandFailure */
-
-class CVC4_PUBLIC Command {
-protected:
- /**
- * This field contains a command status if the command has been
- * invoked, or NULL if it has not. This field is either a
- * dynamically-allocated pointer, or it's a pointer to the singleton
- * CommandSuccess instance. Doing so is somewhat asymmetric, but
- * it avoids the need to dynamically allocate memory in the common
- * case of a successful command.
- */
- const CommandStatus* d_commandStatus;
-
- /**
- * True if this command is "muted"---i.e., don't print "success" on
- * successful execution.
- */
- bool d_muted;
-
-public:
- typedef CommandPrintSuccess printsuccess;
-
- Command() throw();
- Command(const Command& cmd);
-
- virtual ~Command() throw();
-
- virtual void invoke(SmtEngine* smtEngine) throw() = 0;
- virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
-
- virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
- OutputLanguage language = language::output::LANG_AUTO) const throw();
-
- std::string toString() const throw();
-
- virtual std::string getCommandName() const throw() = 0;
-
- /**
- * If false, instruct this Command not to print a success message.
- */
- void setMuted(bool muted) throw() { d_muted = muted; }
-
- /**
- * Determine whether this Command will print a success message.
- */
- bool isMuted() throw() { return d_muted; }
-
- /**
- * Either the command hasn't run yet, or it completed successfully
- * (CommandSuccess, not CommandUnsupported or CommandFailure).
- */
- bool ok() const throw();
-
- /**
- * The command completed in a failure state (CommandFailure, not
- * CommandSuccess or CommandUnsupported).
- */
- bool fail() const throw();
-
- /**
- * The command was ran but was interrupted due to resource limiting.
- */
- bool interrupted() const throw();
-
- /** Get the command status (it's NULL if we haven't run yet). */
- const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
-
- virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
-
- /**
- * Maps this Command into one for a different ExprManager, using
- * variableMap for the translation and extending it with any new
- * mappings.
- */
- virtual Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) = 0;
-
- /**
- * Clone this Command (make a shallow copy).
- */
- virtual Command* clone() const = 0;
-
-protected:
- class ExportTransformer {
- ExprManager* d_exprManager;
- ExprManagerMapCollection& d_variableMap;
- public:
- ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) :
- d_exprManager(exprManager),
- d_variableMap(variableMap) {
- }
- Expr operator()(Expr e) {
- return e.exportTo(d_exprManager, d_variableMap);
- }
- Type operator()(Type t) {
- return t.exportTo(d_exprManager, d_variableMap);
- }
- };/* class Command::ExportTransformer */
-};/* class Command */
-
-/**
- * EmptyCommands are the residue of a command after the parser handles
- * them (and there's nothing left to do).
- */
-class CVC4_PUBLIC EmptyCommand : public Command {
-protected:
- std::string d_name;
-public:
- EmptyCommand(std::string name = "") throw();
- ~EmptyCommand() throw() {}
- std::string getName() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class EmptyCommand */
-
-class CVC4_PUBLIC EchoCommand : public Command {
-protected:
- std::string d_output;
-public:
- EchoCommand(std::string output = "") throw();
- ~EchoCommand() throw() {}
- std::string getOutput() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class EchoCommand */
-
-class CVC4_PUBLIC AssertCommand : public Command {
-protected:
- Expr d_expr;
- bool d_inUnsatCore;
-public:
- AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
- ~AssertCommand() throw() {}
- Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class AssertCommand */
-
-class CVC4_PUBLIC PushCommand : public Command {
-public:
- ~PushCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class PushCommand */
-
-class CVC4_PUBLIC PopCommand : public Command {
-public:
- ~PopCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class PopCommand */
-
-class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
-protected:
- std::string d_symbol;
-public:
- DeclarationDefinitionCommand(const std::string& id) throw();
- ~DeclarationDefinitionCommand() throw() {}
- virtual void invoke(SmtEngine* smtEngine) throw() = 0;
- std::string getSymbol() const throw();
-};/* class DeclarationDefinitionCommand */
-
-class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
-protected:
- Expr d_func;
- Type d_type;
- bool d_printInModel;
- bool d_printInModelSetByUser;
-public:
- DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw();
- ~DeclareFunctionCommand() throw() {}
- Expr getFunction() const throw();
- Type getType() const throw();
- bool getPrintInModel() const throw();
- bool getPrintInModelSetByUser() const throw();
- void setPrintInModel( bool p );
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DeclareFunctionCommand */
-
-class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
-protected:
- size_t d_arity;
- Type d_type;
-public:
- DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
- ~DeclareTypeCommand() throw() {}
- size_t getArity() const throw();
- Type getType() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DeclareTypeCommand */
-
-class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
-protected:
- std::vector<Type> d_params;
- Type d_type;
-public:
- DefineTypeCommand(const std::string& id, Type t) throw();
- DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
- ~DefineTypeCommand() throw() {}
- const std::vector<Type>& getParameters() const throw();
- Type getType() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DefineTypeCommand */
-
-class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
-protected:
- Expr d_func;
- std::vector<Expr> d_formals;
- Expr d_formula;
-public:
- DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
- DefineFunctionCommand(const std::string& id, Expr func,
- const std::vector<Expr>& formals, Expr formula) throw();
- ~DefineFunctionCommand() throw() {}
- Expr getFunction() const throw();
- const std::vector<Expr>& getFormals() const throw();
- Expr getFormula() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DefineFunctionCommand */
-
-/**
- * This differs from DefineFunctionCommand only in that it instructs
- * the SmtEngine to "remember" this function for later retrieval with
- * getAssignment(). Used for :named attributes in SMT-LIBv2.
- */
-class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
-public:
- DefineNamedFunctionCommand(const std::string& id, Expr func,
- const std::vector<Expr>& formals, Expr formula) throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
-};/* class DefineNamedFunctionCommand */
-
-/**
- * The command when an attribute is set by a user. In SMT-LIBv2 this is done
- * via the syntax (! expr :attr)
- */
-class CVC4_PUBLIC SetUserAttributeCommand : public Command {
-protected:
- std::string d_attr;
- Expr d_expr;
- std::vector<Expr> d_expr_values;
- std::string d_str_value;
-public:
- SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
- SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw();
- SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw();
- ~SetUserAttributeCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetUserAttributeCommand */
-
-class CVC4_PUBLIC CheckSatCommand : public Command {
-protected:
- Expr d_expr;
- Result d_result;
- bool d_inUnsatCore;
-public:
- CheckSatCommand() throw();
- CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
- ~CheckSatCommand() throw() {}
- Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class CheckSatCommand */
-
-class CVC4_PUBLIC QueryCommand : public Command {
-protected:
- Expr d_expr;
- Result d_result;
- bool d_inUnsatCore;
-public:
- QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
- ~QueryCommand() throw() {}
- Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class QueryCommand */
-
-// this is TRANSFORM in the CVC presentation language
-class CVC4_PUBLIC SimplifyCommand : public Command {
-protected:
- Expr d_term;
- Expr d_result;
-public:
- SimplifyCommand(Expr term) throw();
- ~SimplifyCommand() throw() {}
- Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SimplifyCommand */
-
-class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
-protected:
- Expr d_term;
- Expr d_result;
-public:
- ExpandDefinitionsCommand(Expr term) throw();
- ~ExpandDefinitionsCommand() throw() {}
- Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class ExpandDefinitionsCommand */
-
-class CVC4_PUBLIC GetValueCommand : public Command {
-protected:
- std::vector<Expr> d_terms;
- Expr d_result;
-public:
- GetValueCommand(Expr term) throw();
- GetValueCommand(const std::vector<Expr>& terms) throw();
- ~GetValueCommand() throw() {}
- const std::vector<Expr>& getTerms() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetValueCommand */
-
-class CVC4_PUBLIC GetAssignmentCommand : public Command {
-protected:
- SExpr d_result;
-public:
- GetAssignmentCommand() throw();
- ~GetAssignmentCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- SExpr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetAssignmentCommand */
-
-class CVC4_PUBLIC GetModelCommand : public Command {
-protected:
- Model* d_result;
- SmtEngine* d_smtEngine;
-public:
- GetModelCommand() throw();
- ~GetModelCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- // Model is private to the library -- for now
- //Model* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetModelCommand */
-
-class CVC4_PUBLIC GetProofCommand : public Command {
-protected:
- Proof* d_result;
- SmtEngine* d_smtEngine;
-public:
- GetProofCommand() throw();
- ~GetProofCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- Proof* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetProofCommand */
-
-class CVC4_PUBLIC GetInstantiationsCommand : public Command {
-protected:
- //Instantiations* d_result;
- SmtEngine* d_smtEngine;
-public:
- GetInstantiationsCommand() throw();
- ~GetInstantiationsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- //Instantiations* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetInstantiationsCommand */
-
-class CVC4_PUBLIC GetSynthSolutionCommand : public Command {
-protected:
- SmtEngine* d_smtEngine;
-public:
- GetSynthSolutionCommand() throw();
- ~GetSynthSolutionCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetSynthSolutionCommand */
-
-class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
-protected:
- UnsatCore d_result;
- std::map<Expr, std::string> d_names;
-public:
- GetUnsatCoreCommand() throw();
- GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw();
- ~GetUnsatCoreCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- const UnsatCore& getUnsatCore() const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetUnsatCoreCommand */
-
-class CVC4_PUBLIC GetAssertionsCommand : public Command {
-protected:
- std::string d_result;
-public:
- GetAssertionsCommand() throw();
- ~GetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetAssertionsCommand */
-
-class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
-protected:
- BenchmarkStatus d_status;
-public:
- SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
- ~SetBenchmarkStatusCommand() throw() {}
- BenchmarkStatus getStatus() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetBenchmarkStatusCommand */
-
-class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
-protected:
- std::string d_logic;
-public:
- SetBenchmarkLogicCommand(std::string logic) throw();
- ~SetBenchmarkLogicCommand() throw() {}
- std::string getLogic() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetBenchmarkLogicCommand */
-
-class CVC4_PUBLIC SetInfoCommand : public Command {
-protected:
- std::string d_flag;
- SExpr d_sexpr;
-public:
- SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
- ~SetInfoCommand() throw() {}
- std::string getFlag() const throw();
- SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetInfoCommand */
-
-class CVC4_PUBLIC GetInfoCommand : public Command {
-protected:
- std::string d_flag;
- std::string d_result;
-public:
- GetInfoCommand(std::string flag) throw();
- ~GetInfoCommand() throw() {}
- std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetInfoCommand */
-
-class CVC4_PUBLIC SetOptionCommand : public Command {
-protected:
- std::string d_flag;
- SExpr d_sexpr;
-public:
- SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
- ~SetOptionCommand() throw() {}
- std::string getFlag() const throw();
- SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetOptionCommand */
-
-class CVC4_PUBLIC GetOptionCommand : public Command {
-protected:
- std::string d_flag;
- std::string d_result;
-public:
- GetOptionCommand(std::string flag) throw();
- ~GetOptionCommand() throw() {}
- std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class GetOptionCommand */
-
-class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
-private:
- std::vector<DatatypeType> d_datatypes;
-public:
- DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
- ~DatatypeDeclarationCommand() throw() {}
- DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
- const std::vector<DatatypeType>& getDatatypes() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DatatypeDeclarationCommand */
-
-class CVC4_PUBLIC RewriteRuleCommand : public Command {
-public:
- typedef std::vector< std::vector< Expr > > Triggers;
-protected:
- typedef std::vector< Expr > VExpr;
- VExpr d_vars;
- VExpr d_guards;
- Expr d_head;
- Expr d_body;
- Triggers d_triggers;
-public:
- RewriteRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& guards,
- Expr head,
- Expr body,
- const Triggers& d_triggers) throw();
- RewriteRuleCommand(const std::vector<Expr>& vars,
- Expr head,
- Expr body) throw();
- ~RewriteRuleCommand() throw() {}
- const std::vector<Expr>& getVars() const throw();
- const std::vector<Expr>& getGuards() const throw();
- Expr getHead() const throw();
- Expr getBody() const throw();
- const Triggers& getTriggers() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class RewriteRuleCommand */
-
-class CVC4_PUBLIC PropagateRuleCommand : public Command {
-public:
- typedef std::vector< std::vector< Expr > > Triggers;
-protected:
- typedef std::vector< Expr > VExpr;
- VExpr d_vars;
- VExpr d_guards;
- VExpr d_heads;
- Expr d_body;
- Triggers d_triggers;
- bool d_deduction;
-public:
- PropagateRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& guards,
- const std::vector<Expr>& heads,
- Expr body,
- const Triggers& d_triggers,
- /* true if we want a deduction rule */
- bool d_deduction = false) throw();
- PropagateRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& heads,
- Expr body,
- bool d_deduction = false) throw();
- ~PropagateRuleCommand() throw() {}
- const std::vector<Expr>& getVars() const throw();
- const std::vector<Expr>& getGuards() const throw();
- const std::vector<Expr>& getHeads() const throw();
- Expr getBody() const throw();
- const Triggers& getTriggers() const throw();
- bool isDeduction() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class PropagateRuleCommand */
-
-class CVC4_PUBLIC ResetCommand : public Command {
-public:
- ResetCommand() throw() {}
- ~ResetCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class ResetCommand */
-
-class CVC4_PUBLIC ResetAssertionsCommand : public Command {
-public:
- ResetAssertionsCommand() throw() {}
- ~ResetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class ResetAssertionsCommand */
-
-class CVC4_PUBLIC QuitCommand : public Command {
-public:
- QuitCommand() throw() {}
- ~QuitCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class QuitCommand */
-
-class CVC4_PUBLIC CommentCommand : public Command {
- std::string d_comment;
-public:
- CommentCommand(std::string comment) throw();
- ~CommentCommand() throw() {}
- std::string getComment() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class CommentCommand */
-
-class CVC4_PUBLIC CommandSequence : public Command {
-private:
- /** All the commands to be executed (in sequence) */
- std::vector<Command*> d_commandSequence;
- /** Next command to be executed */
- unsigned int d_index;
-public:
- CommandSequence() throw();
- ~CommandSequence() throw();
-
- void addCommand(Command* cmd) throw();
- void clear() throw();
-
- void invoke(SmtEngine* smtEngine) throw();
- void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
-
- typedef std::vector<Command*>::iterator iterator;
- typedef std::vector<Command*>::const_iterator const_iterator;
-
- const_iterator begin() const throw();
- const_iterator end() const throw();
-
- iterator begin() throw();
- iterator end() throw();
-
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class CommandSequence */
-
-class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
-public:
- ~DeclarationSequence() throw() {}
-};/* class DeclarationSequence */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__COMMAND_H */
+++ /dev/null
-%{
-#include "smt_util/command.h"
-
-#ifdef SWIGJAVA
-
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
-
-#endif /* SWIGJAVA */
-%}
-
-%ignore CVC4::operator<<(std::ostream&, const Command&) throw();
-%ignore CVC4::operator<<(std::ostream&, const Command*) throw();
-%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw();
-%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw();
-%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw();
-%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw();
-
-%ignore CVC4::GetProofCommand;
-%ignore CVC4::CommandPrintSuccess::Scope;
-
-#ifdef SWIGJAVA
-
-// Instead of CommandSequence::begin() and end(), create an
-// iterator() method on the Java side that returns a Java-style
-// Iterator.
-%ignore CVC4::CommandSequence::begin();
-%ignore CVC4::CommandSequence::end();
-%ignore CVC4::CommandSequence::begin() const;
-%ignore CVC4::CommandSequence::end() const;
-%extend CVC4::CommandSequence {
- CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() {
- return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self);
- }
-}
-
-// CommandSequence is "iterable" on the Java side
-%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>";
-
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>";
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "
- public void remove() {
- throw new java.lang.UnsupportedOperationException();
- }
-
- public edu.nyu.acsys.CVC4.Command next() {
- if(hasNext()) {
- return getNext();
- } else {
- throw new java.util.NoSuchElementException();
- }
- }
-"
-// getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private";
-
-// map the types appropriately
-%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject";
-%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
-%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
-%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; }
-
-#endif /* SWIGJAVA */
-
-%include "smt_util/command.h"
-
-#ifdef SWIGJAVA
-
-%include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
-
-%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>;
-
-#endif /* SWIGJAVA */
+++ /dev/null
-/********************* */
-/*! \file dump.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Dump utility classes and functions
- **
- ** Dump utility classes and functions.
- **/
-#include "smt_util/dump.h"
-
-#include "base/output.h"
-
-namespace CVC4 {
-
-DumpC DumpChannel CVC4_PUBLIC;
-
-std::ostream& DumpC::setStream(std::ostream* os) {
- ::CVC4::DumpOutChannel.setStream(os);
- return *os;
-}
-std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); }
-std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); }
-
-
-void DumpC::setDumpFromString(const std::string& optarg) {
-#ifdef CVC4_DUMPING
- char* optargPtr = strdup(optarg.c_str());
- char* tokstr = optargPtr;
- char* toksave;
- while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
- tokstr = NULL;
- if(!strcmp(optargPtr, "benchmark")) {
- } else if(!strcmp(optargPtr, "declarations")) {
- } else if(!strcmp(optargPtr, "assertions")) {
- Dump.on("assertions:post-everything");
- } else if(!strncmp(optargPtr, "assertions:", 11)) {
- const char* p = optargPtr + 11;
- if(!strncmp(p, "pre-", 4)) {
- p += 4;
- } else if(!strncmp(p, "post-", 5)) {
- p += 5;
- } else {
- throw OptionException(std::string("don't know how to dump `") +
- optargPtr + "'. Please consult --dump help.");
- }
- if(!strcmp(p, "everything")) {
- } else if(!strcmp(p, "definition-expansion")) {
- } else if(!strcmp(p, "boolean-terms")) {
- } else if(!strcmp(p, "constrain-subtypes")) {
- } else if(!strcmp(p, "substitution")) {
- } else if(!strcmp(p, "strings-pp")) {
- } else if(!strcmp(p, "skolem-quant")) {
- } else if(!strcmp(p, "simplify")) {
- } else if(!strcmp(p, "static-learning")) {
- } else if(!strcmp(p, "ite-removal")) {
- } else if(!strcmp(p, "repeat-simplify")) {
- } else if(!strcmp(p, "rewrite-apply-to-const")) {
- } else if(!strcmp(p, "theory-preprocessing")) {
- } else if(!strcmp(p, "nonclausal")) {
- } else if(!strcmp(p, "theorypp")) {
- } else if(!strcmp(p, "itesimp")) {
- } else if(!strcmp(p, "unconstrained")) {
- } else if(!strcmp(p, "repeatsimp")) {
- } else {
- throw OptionException(std::string("don't know how to dump `") +
- optargPtr + "'. Please consult --dump help.");
- }
- Dump.on("assertions");
- } else if(!strcmp(optargPtr, "skolems")) {
- } else if(!strcmp(optargPtr, "clauses")) {
- } else if(!strcmp(optargPtr, "t-conflicts") ||
- !strcmp(optargPtr, "t-lemmas") ||
- !strcmp(optargPtr, "t-explanations") ||
- !strcmp(optargPtr, "bv-rewrites") ||
- !strcmp(optargPtr, "theory::fullcheck")) {
- // These are "non-state-dumping" modes. If state (SAT decisions,
- // propagations, etc.) is dumped, it will interfere with the validity
- // of these generated queries.
- if(Dump.isOn("state")) {
- throw OptionException(std::string("dump option `") + optargPtr +
- "' conflicts with a previous, "
- "state-dumping dump option. You cannot "
- "mix stateful and non-stateful dumping modes; "
- "see --dump help.");
- } else {
- Dump.on("no-permit-state");
- }
- } else if(!strcmp(optargPtr, "state") ||
- !strcmp(optargPtr, "missed-t-conflicts") ||
- !strcmp(optargPtr, "t-propagations") ||
- !strcmp(optargPtr, "missed-t-propagations")) {
- // These are "state-dumping" modes. If state (SAT decisions,
- // propagations, etc.) is not dumped, it will interfere with the
- // validity of these generated queries.
- if(Dump.isOn("no-permit-state")) {
- throw OptionException(std::string("dump option `") + optargPtr +
- "' conflicts with a previous, "
- "non-state-dumping dump option. You cannot "
- "mix stateful and non-stateful dumping modes; "
- "see --dump help.");
- } else {
- Dump.on("state");
- }
- } else if(!strcmp(optargPtr, "help")) {
- puts(s_dumpHelp.c_str());
- exit(1);
- } else if(!strcmp(optargPtr, "bv-abstraction")) {
- Dump.on("bv-abstraction");
- } else if(!strcmp(optargPtr, "bv-algebraic")) {
- Dump.on("bv-algebraic");
- } else {
- throw OptionException(std::string("unknown option for --dump: `") +
- optargPtr + "'. Try --dump help.");
- }
-
- Dump.on(optargPtr);
- Dump.on("benchmark");
- if(strcmp(optargPtr, "benchmark")) {
- Dump.on("declarations");
- if(strcmp(optargPtr, "declarations")) {
- Dump.on("skolems");
- }
- }
- }
- free(optargPtr);
-#else /* CVC4_DUMPING */
- throw OptionException("The dumping feature was disabled in this build of CVC4.");
-#endif /* CVC4_DUMPING */
-}
-
-
-const std::string DumpC::s_dumpHelp = "\
-Dump modes currently supported by the --dump option:\n\
-\n\
-benchmark\n\
-+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
- does not include any declarations or assertions. Implied by all following\n\
- modes.\n\
-\n\
-declarations\n\
-+ Dump user declarations. Implied by all following modes.\n\
-\n\
-skolems\n\
-+ Dump internally-created skolem variable declarations. These can\n\
- arise from preprocessing simplifications, existential elimination,\n\
- and a number of other things. Implied by all following modes.\n\
-\n\
-assertions\n\
-+ Output the assertions after preprocessing and before clausification.\n\
- Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
- where PASS is one of the preprocessing passes: definition-expansion\n\
- boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
- simplify static-learning ite-removal repeat-simplify\n\
- rewrite-apply-to-const theory-preprocessing.\n\
- PASS can also be the special value \"everything\", in which case the\n\
- assertions are printed before any preprocessing (with\n\
- \"assertions:pre-everything\") or after all preprocessing completes\n\
- (with \"assertions:post-everything\").\n\
-\n\
-clauses\n\
-+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
- output\n\
-\n\
-state\n\
-+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
- Implied by all \"stateful\" modes below and conflicts with all\n\
- non-stateful modes below.\n\
-\n\
-t-conflicts [non-stateful]\n\
-+ Output correctness queries for all theory conflicts\n\
-\n\
-missed-t-conflicts [stateful]\n\
-+ Output completeness queries for theory conflicts\n\
-\n\
-t-propagations [stateful]\n\
-+ Output correctness queries for all theory propagations\n\
-\n\
-missed-t-propagations [stateful]\n\
-+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
-\n\
-t-lemmas [non-stateful]\n\
-+ Output correctness queries for all theory lemmas\n\
-\n\
-t-explanations [non-stateful]\n\
-+ Output correctness queries for all theory explanations\n\
-\n\
-bv-rewrites [non-stateful]\n\
-+ Output correctness queries for all bitvector rewrites\n\
-\n\
-bv-abstraction [non-stateful]\n\
-+ Output correctness queries for all bv abstraction \n\
-\n\
-bv-algebraic [non-stateful]\n\
-+ Output correctness queries for bv algebraic solver. \n\
-\n\
-theory::fullcheck [non-stateful]\n \
-+ Output completeness queries for all full-check effort-level theory checks\n\
-\n\
-Dump modes can be combined with multiple uses of --dump. Generally you want\n\
-one from the assertions category (either assertions or clauses), and\n\
-perhaps one or more stateful or non-stateful modes for checking correctness\n\
-and completeness of decision procedure implementations. Stateful modes dump\n\
-the contextual assertions made by the core solver (all decisions and\n\
-propagations as assertions; that affects the validity of the resulting\n\
-correctness and completeness queries, so of course stateful and non-stateful\n\
-modes cannot be mixed in the same run.\n\
-\n\
-The --output-language option controls the language used for dumping, and\n\
-this allows you to connect CVC4 to another solver implementation via a UNIX\n\
-pipe to perform on-line checking. The --dump-to option can be used to dump\n\
-to a file.\n\
-";
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file dump.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Dump utility classes and functions
- **
- ** Dump utility classes and functions.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__DUMP_H
-#define __CVC4__DUMP_H
-
-#include "base/output.h"
-#include "smt_util/command.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC CVC4dumpstream {
-
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
- std::ostream* d_os;
-#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
-
-#ifdef CVC4_PORTFOLIO
- CommandSequence* d_commands;
-#endif /* CVC4_PORTFOLIO */
-
-public:
- CVC4dumpstream() throw()
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
- : d_os(NULL), d_commands(NULL)
-#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
- : d_os(NULL)
-#elif defined(CVC4_PORTFOLIO)
- : d_commands(NULL)
-#endif /* CVC4_PORTFOLIO */
- { }
-
- CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw()
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
- : d_os(&os), d_commands(&commands)
-#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
- : d_os(&os)
-#elif defined(CVC4_PORTFOLIO)
- : d_commands(&commands)
-#endif /* CVC4_PORTFOLIO */
- { }
-
- CVC4dumpstream& operator<<(const Command& c) {
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
- if(d_os != NULL) {
- (*d_os) << c << std::endl;
- }
-#endif
-#if defined(CVC4_PORTFOLIO)
- if(d_commands != NULL) {
- d_commands->addCommand(c.clone());
- }
-#endif
- return *this;
- }
-};/* class CVC4dumpstream */
-
-/** The dump class */
-class CVC4_PUBLIC DumpC {
- std::set<std::string> d_tags;
- CommandSequence d_commands;
-
- static const std::string s_dumpHelp;
-
-public:
- CVC4dumpstream operator()(const char* tag) {
- if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
- return CVC4dumpstream(getStream(), d_commands);
- } else {
- return CVC4dumpstream();
- }
- }
-
- CVC4dumpstream operator()(std::string tag) {
- if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- return CVC4dumpstream(getStream(), d_commands);
- } else {
- return CVC4dumpstream();
- }
- }
-
- void clear() { d_commands.clear(); }
- const CommandSequence& getCommands() const { return d_commands; }
-
- bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
- bool on (std::string tag) { d_tags.insert(tag); return true; }
- bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
- bool off(std::string tag) { d_tags.erase (tag); return false; }
- bool off() { d_tags.clear(); return false; }
-
- bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
- bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
-
- std::ostream& setStream(std::ostream* os);
- std::ostream& getStream();
- std::ostream* getStreamPointer();
-
- void setDumpFromString(const std::string& optarg);
-};/* class DumpC */
-
-/** The dump singleton */
-extern DumpC DumpChannel CVC4_PUBLIC;
-
-#define Dump ::CVC4::DumpChannel
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__DUMP_H */
+++ /dev/null
-/********************* */
-/*! \file ite_removal.cpp
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Removal of term ITEs
- **
- ** Removal of term ITEs.
- **/
-#include "smt_util/ite_removal.h"
-
-#include <vector>
-
-#include "proof/proof_manager.h"
-#include "smt_util/command.h"
-#include "theory/ite_utilities.h"
-
-using namespace CVC4;
-using namespace std;
-
-namespace CVC4 {
-
-RemoveITE::RemoveITE(context::UserContext* u)
- : d_iteCache(u)
-{
- d_containsVisitor = new theory::ContainsTermITEVisitor();
-}
-
-RemoveITE::~RemoveITE(){
- delete d_containsVisitor;
-}
-
-void RemoveITE::garbageCollect(){
- d_containsVisitor->garbageCollect();
-}
-
-theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
- return d_containsVisitor;
-}
-
-size_t RemoveITE::collectedCacheSizes() const{
- return d_containsVisitor->cache_size() + d_iteCache.size();
-}
-
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
-{
- size_t n = output.size();
- for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
- // Do this in two steps to avoid Node problems(?)
- // Appears related to bug 512, splitting this into two lines
- // fixes the bug on clang on Mac OS
- Node itesRemoved = run(output[i], output, iteSkolemMap, false);
- // In some calling contexts, not necessary to report dependence information.
- if(reportDeps && options::unsatCores()) {
- // new assertions have a dependence on the node
- PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
- while(n < output.size()) {
- PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
- ++n;
- }
- }
- output[i] = itesRemoved;
- }
-}
-
-bool RemoveITE::containsTermITE(TNode e) const {
- return d_containsVisitor->containsTermITE(e);
-}
-
-Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap, bool inQuant) {
- // Current node
- Debug("ite") << "removeITEs(" << node << ")" << endl;
-
- if(node.isVar() || node.isConst() ||
- (options::biasedITERemoval() && !containsTermITE(node))){
- return Node(node);
- }
-
- // The result may be cached already
- std::pair<Node, bool> cacheKey(node, inQuant);
- NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::const_iterator i = d_iteCache.find(cacheKey);
- if(i != d_iteCache.end()) {
- Node cached = (*i).second;
- Debug("ite") << "removeITEs: in-cache: " << cached << endl;
- return cached.isNull() ? Node(node) : cached;
- }
-
- // Remember that we're inside a quantifier
- if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
- inQuant = true;
- }
-
- // If an ITE replace it
- if(node.getKind() == kind::ITE) {
- TypeNode nodeType = node.getType();
- if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
- Node skolem;
- // Make the skolem to represent the ITE
- skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
-
- // The new assertion
- Node newAssertion =
- nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
- skolem.eqNode(node[2]));
- Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
-
- // Attach the skolem
- d_iteCache.insert(cacheKey, skolem);
-
- // Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
-
- iteSkolemMap[skolem] = output.size();
- output.push_back(newAssertion);
-
- // The representation is now the skolem
- return skolem;
- }
- }
-
- // If not an ITE, go deep
- vector<Node> newChildren;
- bool somethingChanged = false;
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- newChildren.push_back(node.getOperator());
- }
- // Remove the ITEs from the children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, iteSkolemMap, inQuant);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
-
- // If changes, we rewrite
- if(somethingChanged) {
- Node cached = nodeManager->mkNode(node.getKind(), newChildren);
- d_iteCache.insert(cacheKey, cached);
- return cached;
- } else {
- d_iteCache.insert(cacheKey, Node::null());
- return node;
- }
-}
-
-Node RemoveITE::replace(TNode node, bool inQuant) const {
- if(node.isVar() || node.isConst() ||
- (options::biasedITERemoval() && !containsTermITE(node))){
- return Node(node);
- }
-
- // Check the cache
- NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
- if(i != d_iteCache.end()) {
- Node cached = (*i).second;
- return cached.isNull() ? Node(node) : cached;
- }
-
- // Remember that we're inside a quantifier
- if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
- inQuant = true;
- }
-
- vector<Node> newChildren;
- bool somethingChanged = false;
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- newChildren.push_back(node.getOperator());
- }
- // Replace in children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = replace(*it, inQuant);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
-
- // If changes, we rewrite
- if(somethingChanged) {
- return nodeManager->mkNode(node.getKind(), newChildren);
- } else {
- return node;
- }
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file ite_removal.h
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Removal of term ITEs
- **
- ** Removal of term ITEs.
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include <vector>
-
-#include "context/cdinsert_hashmap.h"
-#include "context/context.h"
-#include "expr/node.h"
-#include "smt_util/dump.h"
-#include "util/bool.h"
-#include "util/hash.h"
-
-namespace CVC4 {
-
-namespace theory {
- class ContainsTermITEVisitor;
-}/* CVC4::theory namespace */
-
-typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
-
-class RemoveITE {
- typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
- ITECache d_iteCache;
-
-
-public:
-
- RemoveITE(context::UserContext* u);
- ~RemoveITE();
-
- /**
- * Removes the ITE nodes by introducing skolem variables. All
- * additional assertions are pushed into assertions. iteSkolemMap
- * contains a map from introduced skolem variables to the index in
- * assertions containing the new Boolean ite created in conjunction
- * with that skolem variable.
- *
- * With reportDeps true, report reasoning dependences to the proof
- * manager (for unsat cores).
- */
- void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
-
- /**
- * Removes the ITE from the node by introducing skolem
- * variables. All additional assertions are pushed into
- * assertions. iteSkolemMap contains a map from introduced skolem
- * variables to the index in assertions containing the new Boolean
- * ite created in conjunction with that skolem variable.
- */
- Node run(TNode node, std::vector<Node>& additionalAssertions,
- IteSkolemMap& iteSkolemMap, bool inQuant);
-
- /**
- * Substitute under node using pre-existing cache. Do not remove
- * any ITEs not seen during previous runs.
- */
- Node replace(TNode node, bool inQuant = false) const;
-
- /** Returns true if e contains a term ite. */
- bool containsTermITE(TNode e) const;
-
- /** Returns the collected size of the caches. */
- size_t collectedCacheSizes() const;
-
- /** Garbage collects non-context dependent data-structures. */
- void garbageCollect();
-
- /** Return the RemoveITE's containsVisitor. */
- theory::ContainsTermITEVisitor* getContainsVisitor();
-
-private:
- theory::ContainsTermITEVisitor* d_containsVisitor;
-
-};/* class RemoveTTE */
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file model.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief implementation of Model class
- **/
-
-#include "smt_util/model.h"
-
-#include <vector>
-
-#include "expr/expr_iomanip.h"
-#include "options/base_options.h"
-#include "printer/printer.h"
-#include "smt/command_list.h"
-#include "smt/smt_engine_scope.h"
-#include "smt_util/command.h"
-
-using namespace std;
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, const Model& m) {
- smt::SmtScope smts(&m.d_smt);
- expr::ExprDag::Scope scope(out, false);
- Printer::getPrinter(options::outputLanguage())->toStream(out, m);
- return out;
-}
-
-Model::Model() :
- d_smt(*smt::currentSmtEngine()) {
-}
-
-size_t Model::getNumCommands() const {
- return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
-}
-
-const Command* Model::getCommand(size_t i) const {
- Assert(i < getNumCommands());
- // index the global commands first, then the locals
- if(i < d_smt.d_modelGlobalCommands.size()) {
- return d_smt.d_modelGlobalCommands[i];
- } else {
- return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
- }
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file model.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Model class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__MODEL_H
-#define __CVC4__MODEL_H
-
-#include <iosfwd>
-#include <vector>
-
-#include "expr/expr.h"
-#include "util/cardinality.h"
-
-namespace CVC4 {
-
-class Command;
-class SmtEngine;
-class Model;
-
-std::ostream& operator<<(std::ostream&, const Model&);
-
-class Model {
- friend std::ostream& operator<<(std::ostream&, const Model&);
- friend class SmtEngine;
-
- /** the input name (file name, etc.) this model is associated to */
- std::string d_inputName;
-
-protected:
- /** The SmtEngine we're associated with */
- SmtEngine& d_smt;
-
- /** construct the base class; users cannot do this, only CVC4 internals */
- Model();
-
-public:
- /** virtual destructor */
- virtual ~Model() { }
- /** get number of commands to report */
- size_t getNumCommands() const;
- /** get command */
- const Command* getCommand(size_t i) const;
- /** get the smt engine that this model is hooked up to */
- SmtEngine* getSmtEngine() { return &d_smt; }
- /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
- const SmtEngine* getSmtEngine() const { return &d_smt; }
- /** get the input name (file name, etc.) this model is associated to */
- std::string getInputName() const { return d_inputName; }
-
-public:
- /** get value for expression */
- virtual Expr getValue(Expr expr) const = 0;
- /** get cardinality for sort */
- virtual Cardinality getCardinality(Type t) const = 0;
-};/* class Model */
-
-class ModelBuilder {
-public:
- ModelBuilder() { }
- virtual ~ModelBuilder() { }
- virtual void buildModel(Model* m, bool fullModel) = 0;
-};/* class ModelBuilder */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__MODEL_H */
#include "expr/kind.h"
#include "options/arrays_options.h"
#include "options/smt_options.h"
+#include "smt/command.h"
#include "smt/logic_exception.h"
#include "smt/smt_statistics_registry.h"
-#include "smt_util/command.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
#include "proof/theory_proof.h"
#include "theory/bv/abstraction.h"
#include "options/bv_options.h"
-#include "smt_util/dump.h"
+#include "smt/dump.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
#include <sstream>
#include "context/context.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
#include "util/statistics_registry.h"
#include "theory/quantifiers/ceg_instantiator.h"
#include "options/quantifiers_options.h"
-#include "smt_util/ite_removal.h"
+#include "smt/ite_removal.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/theory_arith_private.h"
#include "theory/quantifiers/inst_strategy_cbqi.h"
#include "options/quantifiers_options.h"
-#include "smt_util/ite_removal.h"
+#include "smt/ite_removal.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/theory_arith_private.h"
#include "options/strings_options.h"
#include "smt/logic_exception.h"
#include "smt/smt_statistics_registry.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_rewriter.h"
#include "theory/strings/type_enumerator.h"
#include "options/options.h"
#include "options/theory_options.h"
#include "options/theoryof_mode.h"
+#include "smt/command.h"
+#include "smt/dump.h"
#include "smt/logic_request.h"
-#include "smt_util/command.h"
-#include "smt_util/dump.h"
#include "theory/logic_info.h"
#include "theory/output_channel.h"
#include "theory/valuation.h"
#include "options/quantifiers_options.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
+#include "smt/ite_removal.h"
#include "smt/logic_exception.h"
-#include "smt_util/ite_removal.h"
#include "smt_util/lemma_output_channel.h"
#include "smt_util/node_visitor.h"
#include "theory/arith/arith_ite_utils.h"
#include "options/options.h"
#include "options/smt_options.h"
#include "prop/prop_engine.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
#include "smt_util/lemma_channels.h"
#include "theory/atom_requests.h"
#include "theory/bv/bv_to_bool.h"
#ifndef __CVC4__THEORY__THEORY_MODEL_H
#define __CVC4__THEORY__THEORY_MODEL_H
-#include "smt_util/model.h"
+#include "smt/model.h"
#include "theory/uf/equality_engine.h"
#include "theory/rep_set.h"
#include "theory/substitutions.h"
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace CVC4;
using namespace CVC4::parser;
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "smt/command.h"
#include "smt/smt_engine.h"
-#include "smt_util/command.h"
using namespace CVC4;
using namespace CVC4::parser;
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/smt2/smt2.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
using namespace CVC4;
#include "options/language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu;
projects / cvc5.git / commitdiff