diff options
author | Tim King <taking@google.com> | 2016-02-02 09:47:34 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-02-02 09:47:34 -0800 |
commit | e21e99b7dfe45f042260db7eb754e25e7108f288 (patch) | |
tree | 689bc1fead54d62b46c75196f8be0fb4b35444c9 /src/smt | |
parent | 18973b31c440d998230aaba3e17bd915b168aa6f (diff) |
Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 1855 | ||||
-rw-r--r-- | src/smt/command.h | 905 | ||||
-rw-r--r-- | src/smt/command.i | 77 | ||||
-rw-r--r-- | src/smt/command_list.cpp | 2 | ||||
-rw-r--r-- | src/smt/dump.cpp | 221 | ||||
-rw-r--r-- | src/smt/dump.h | 123 | ||||
-rw-r--r-- | src/smt/ite_removal.cpp | 190 | ||||
-rw-r--r-- | src/smt/ite_removal.h | 93 | ||||
-rw-r--r-- | src/smt/model.cpp | 55 | ||||
-rw-r--r-- | src/smt/model.h | 78 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
-rw-r--r-- | src/smt/update_ostream.h | 2 |
12 files changed, 3601 insertions, 4 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp new file mode 100644 index 000000000..d6ec0769a --- /dev/null +++ b/src/smt/command.cpp @@ -0,0 +1,1855 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/command.h b/src/smt/command.h new file mode 100644 index 000000000..248e69b0e --- /dev/null +++ b/src/smt/command.h @@ -0,0 +1,905 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/command.i b/src/smt/command.i new file mode 100644 index 000000000..0c050201d --- /dev/null +++ b/src/smt/command.i @@ -0,0 +1,77 @@ +%{ +#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 */ diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp index 3e912d338..2319d9539 100644 --- a/src/smt/command_list.cpp +++ b/src/smt/command_list.cpp @@ -15,9 +15,9 @@ **/ // 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 { diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp new file mode 100644 index 000000000..3b9ec3273 --- /dev/null +++ b/src/smt/dump.cpp @@ -0,0 +1,221 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/dump.h b/src/smt/dump.h new file mode 100644 index 000000000..a6fa899da --- /dev/null +++ b/src/smt/dump.h @@ -0,0 +1,123 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp new file mode 100644 index 000000000..c0c6ed02b --- /dev/null +++ b/src/smt/ite_removal.cpp @@ -0,0 +1,190 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h new file mode 100644 index 000000000..d6d820f89 --- /dev/null +++ b/src/smt/ite_removal.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/model.cpp b/src/smt/model.cpp new file mode 100644 index 000000000..15ecbadfb --- /dev/null +++ b/src/smt/model.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/model.h b/src/smt/model.h new file mode 100644 index 000000000..33a9312a6 --- /dev/null +++ b/src/smt/model.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index df3466d92..850b37fe0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -72,15 +72,15 @@ #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" diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index c5f09a2a9..b87ed69d2 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -28,7 +28,7 @@ #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 { |