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_util | |
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_util')
-rw-r--r-- | src/smt_util/Makefile.am | 12 | ||||
-rw-r--r-- | src/smt_util/command.cpp | 1855 | ||||
-rw-r--r-- | src/smt_util/command.h | 905 | ||||
-rw-r--r-- | src/smt_util/command.i | 77 | ||||
-rw-r--r-- | src/smt_util/dump.cpp | 221 | ||||
-rw-r--r-- | src/smt_util/dump.h | 123 | ||||
-rw-r--r-- | src/smt_util/ite_removal.cpp | 192 | ||||
-rw-r--r-- | src/smt_util/ite_removal.h | 93 | ||||
-rw-r--r-- | src/smt_util/model.cpp | 55 | ||||
-rw-r--r-- | src/smt_util/model.h | 78 |
10 files changed, 0 insertions, 3611 deletions
diff --git a/src/smt_util/Makefile.am b/src/smt_util/Makefile.am index ae1ea1f70..46f6493a9 100644 --- a/src/smt_util/Makefile.am +++ b/src/smt_util/Makefile.am @@ -10,23 +10,11 @@ libsmtutil_la_SOURCES = \ Makefile.in \ boolean_simplification.cpp \ boolean_simplification.h \ - command.cpp \ - command.h \ - dump.cpp \ - dump.h \ - ite_removal.cpp \ - ite_removal.h \ lemma_channels.cpp \ lemma_channels.h \ lemma_input_channel.h \ lemma_output_channel.h \ - model.cpp \ - model.h \ nary_builder.cpp \ nary_builder.h \ node_visitor.h - -EXTRA_DIST = \ - command.i - diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp deleted file mode 100644 index 83298836f..000000000 --- a/src/smt_util/command.cpp +++ /dev/null @@ -1,1855 +0,0 @@ -/********************* */ -/*! \file command.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of command objects. - ** - ** Implementation of command objects. - **/ - -#include "smt_util/command.h" - -#include <exception> -#include <iostream> -#include <iterator> -#include <sstream> -#include <utility> -#include <vector> - -#include "base/cvc4_assert.h" -#include "base/output.h" -#include "expr/expr_iomanip.h" -#include "expr/node.h" -#include "options/options.h" -#include "options/smt_options.h" -#include "printer/printer.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt_util/dump.h" -#include "smt_util/model.h" -#include "util/sexpr.h" - -using namespace std; - -namespace CVC4 { - -const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); -const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); -const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); - -std::ostream& operator<<(std::ostream& out, const Command& c) throw() { - c.toStream(out, - Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out), - Node::dag::getDag(out), - Node::setlanguage::getLanguage(out)); - return out; -} - -ostream& operator<<(ostream& out, const Command* c) throw() { - if(c == NULL) { - out << "null"; - } else { - out << *c; - } - return out; -} - -std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { - s.toStream(out, Node::setlanguage::getLanguage(out)); - return out; -} - -ostream& operator<<(ostream& out, const CommandStatus* s) throw() { - if(s == NULL) { - out << "null"; - } else { - out << *s; - } - return out; -} - -/* class Command */ - -Command::Command() throw() : d_commandStatus(NULL), d_muted(false) { -} - -Command::Command(const Command& cmd) { - d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone(); - d_muted = cmd.d_muted; -} - -Command::~Command() throw() { - if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) { - delete d_commandStatus; - } -} - -bool Command::ok() const throw() { - // either we haven't run the command yet, or it ran successfully - return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL; -} - -bool Command::fail() const throw() { - return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL; -} - -bool Command::interrupted() const throw() { - return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL; -} - -void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - invoke(smtEngine); - if(!(isMuted() && ok())) { - printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); - } -} - -std::string Command::toString() const throw() { - std::stringstream ss; - toStream(ss); - return ss.str(); -} - -void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag, - OutputLanguage language) const throw() { - Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag); -} - -void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { - Printer::getPrinter(language)->toStream(out, this); -} - -void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(d_commandStatus != NULL) { - if((!ok() && verbosity >= 1) || verbosity >= 2) { - out << *d_commandStatus; - } - } -} - -/* class EmptyCommand */ - -EmptyCommand::EmptyCommand(std::string name) throw() : - d_name(name) { -} - -std::string EmptyCommand::getName() const throw() { - return d_name; -} - -void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { - /* empty commands have no implementation */ - d_commandStatus = CommandSuccess::instance(); -} - -Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new EmptyCommand(d_name); -} - -Command* EmptyCommand::clone() const { - return new EmptyCommand(d_name); -} - -std::string EmptyCommand::getCommandName() const throw() { - return "empty"; -} - -/* class EchoCommand */ - -EchoCommand::EchoCommand(std::string output) throw() : - d_output(output) { -} - -std::string EchoCommand::getOutput() const throw() { - return d_output; -} - -void EchoCommand::invoke(SmtEngine* smtEngine) throw() { - /* we don't have an output stream here, nothing to do */ - d_commandStatus = CommandSuccess::instance(); -} - -void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - out << d_output << std::endl; - d_commandStatus = CommandSuccess::instance(); - printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); -} - -Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new EchoCommand(d_output); -} - -Command* EchoCommand::clone() const { - return new EchoCommand(d_output); -} - -std::string EchoCommand::getCommandName() const throw() { - return "echo"; -} - -/* class AssertCommand */ - -AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() : - d_expr(e), d_inUnsatCore(inUnsatCore) { -} - -Expr AssertCommand::getExpr() const throw() { - return d_expr; -} - -void AssertCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->assertFormula(d_expr, d_inUnsatCore); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); -} - -Command* AssertCommand::clone() const { - return new AssertCommand(d_expr, d_inUnsatCore); -} - -std::string AssertCommand::getCommandName() const throw() { - return "assert"; -} - -/* class PushCommand */ - -void PushCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->push(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new PushCommand(); -} - -Command* PushCommand::clone() const { - return new PushCommand(); -} - -std::string PushCommand::getCommandName() const throw() { - return "push"; -} - -/* class PopCommand */ - -void PopCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->pop(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new PopCommand(); -} - -Command* PopCommand::clone() const { - return new PopCommand(); -} - -std::string PopCommand::getCommandName() const throw() { - return "pop"; -} - -/* class CheckSatCommand */ - -CheckSatCommand::CheckSatCommand() throw() : - d_expr() { -} - -CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() : - d_expr(expr), d_inUnsatCore(inUnsatCore) { -} - -Expr CheckSatCommand::getExpr() const throw() { - return d_expr; -} - -void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->checkSat(d_expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Result CheckSatCommand::getResult() const throw() { - return d_result; -} - -void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); - c->d_result = d_result; - return c; -} - -Command* CheckSatCommand::clone() const { - CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore); - c->d_result = d_result; - return c; -} - -std::string CheckSatCommand::getCommandName() const throw() { - return "check-sat"; -} - -/* class QueryCommand */ - -QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() : - d_expr(e), d_inUnsatCore(inUnsatCore) { -} - -Expr QueryCommand::getExpr() const throw() { - return d_expr; -} - -void QueryCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->query(d_expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Result QueryCommand::getResult() const throw() { - return d_result; -} - -void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); - c->d_result = d_result; - return c; -} - -Command* QueryCommand::clone() const { - QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore); - c->d_result = d_result; - return c; -} - -std::string QueryCommand::getCommandName() const throw() { - return "query"; -} - -/* class ResetCommand */ - -void ResetCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->reset(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new ResetCommand(); -} - -Command* ResetCommand::clone() const { - return new ResetCommand(); -} - -std::string ResetCommand::getCommandName() const throw() { - return "reset"; -} - -/* class ResetAssertionsCommand */ - -void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->resetAssertions(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new ResetAssertionsCommand(); -} - -Command* ResetAssertionsCommand::clone() const { - return new ResetAssertionsCommand(); -} - -std::string ResetAssertionsCommand::getCommandName() const throw() { - return "reset-assertions"; -} - -/* class QuitCommand */ - -void QuitCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("benchmark") << *this; - d_commandStatus = CommandSuccess::instance(); -} - -Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new QuitCommand(); -} - -Command* QuitCommand::clone() const { - return new QuitCommand(); -} - -std::string QuitCommand::getCommandName() const throw() { - return "exit"; -} - -/* class CommentCommand */ - -CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { -} - -std::string CommentCommand::getComment() const throw() { - return d_comment; -} - -void CommentCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("benchmark") << *this; - d_commandStatus = CommandSuccess::instance(); -} - -Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new CommentCommand(d_comment); -} - -Command* CommentCommand::clone() const { - return new CommentCommand(d_comment); -} - -std::string CommentCommand::getCommandName() const throw() { - return "comment"; -} - -/* class CommandSequence */ - -CommandSequence::CommandSequence() throw() : - d_index(0) { -} - -CommandSequence::~CommandSequence() throw() { - for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { - delete d_commandSequence[i]; - } -} - -void CommandSequence::addCommand(Command* cmd) throw() { - d_commandSequence.push_back(cmd); -} - -void CommandSequence::clear() throw() { - d_commandSequence.clear(); -} - -void CommandSequence::invoke(SmtEngine* smtEngine) throw() { - for(; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine); - if(! d_commandSequence[d_index]->ok()) { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - for(; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine, out); - if(! d_commandSequence[d_index]->ok()) { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CommandSequence* seq = new CommandSequence(); - for(iterator i = begin(); i != end(); ++i) { - Command* cmd_to_export = *i; - Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); - seq->addCommand(cmd); - Debug("export") << "[export] so far converted: " << seq << endl; - } - seq->d_index = d_index; - return seq; -} - -Command* CommandSequence::clone() const { - CommandSequence* seq = new CommandSequence(); - for(const_iterator i = begin(); i != end(); ++i) { - seq->addCommand((*i)->clone()); - } - seq->d_index = d_index; - return seq; -} - -CommandSequence::const_iterator CommandSequence::begin() const throw() { - return d_commandSequence.begin(); -} - -CommandSequence::const_iterator CommandSequence::end() const throw() { - return d_commandSequence.end(); -} - -CommandSequence::iterator CommandSequence::begin() throw() { - return d_commandSequence.begin(); -} - -CommandSequence::iterator CommandSequence::end() throw() { - return d_commandSequence.end(); -} - -std::string CommandSequence::getCommandName() const throw() { - return "sequence"; -} - -/* class DeclarationSequenceCommand */ - -/* class DeclarationDefinitionCommand */ - -DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() : - d_symbol(id) { -} - -std::string DeclarationDefinitionCommand::getSymbol() const throw() { - return d_symbol; -} - -/* class DeclareFunctionCommand */ - -DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_type(t), - d_printInModel(true), - d_printInModelSetByUser(false){ -} - -Expr DeclareFunctionCommand::getFunction() const throw() { - return d_func; -} - -Type DeclareFunctionCommand::getType() const throw() { - return d_type; -} - -bool DeclareFunctionCommand::getPrintInModel() const throw() { - return d_printInModel; -} - -bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { - return d_printInModelSetByUser; -} - -void DeclareFunctionCommand::setPrintInModel( bool p ) { - d_printInModel = p; - d_printInModelSetByUser = true; -} - -void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) { - DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; - return dfc; -} - -Command* DeclareFunctionCommand::clone() const { - DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; - return dfc; -} - -std::string DeclareFunctionCommand::getCommandName() const throw() { - return "declare-fun"; -} - -/* class DeclareTypeCommand */ - -DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : - DeclarationDefinitionCommand(id), - d_arity(arity), - d_type(t) { -} - -size_t DeclareTypeCommand::getArity() const throw() { - return d_arity; -} - -Type DeclareTypeCommand::getType() const throw() { - return d_type; -} - -void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) { - return new DeclareTypeCommand(d_symbol, d_arity, - d_type.exportTo(exprManager, variableMap)); -} - -Command* DeclareTypeCommand::clone() const { - return new DeclareTypeCommand(d_symbol, d_arity, d_type); -} - -std::string DeclareTypeCommand::getCommandName() const throw() { - return "declare-sort"; -} - -/* class DefineTypeCommand */ - -DefineTypeCommand::DefineTypeCommand(const std::string& id, - Type t) throw() : - DeclarationDefinitionCommand(id), - d_params(), - d_type(t) { -} - -DefineTypeCommand::DefineTypeCommand(const std::string& id, - const std::vector<Type>& params, - Type t) throw() : - DeclarationDefinitionCommand(id), - d_params(params), - d_type(t) { -} - -const std::vector<Type>& DefineTypeCommand::getParameters() const throw() { - return d_params; -} - -Type DefineTypeCommand::getType() const throw() { - return d_type; -} - -void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - vector<Type> params; - transform(d_params.begin(), d_params.end(), back_inserter(params), - ExportTransformer(exprManager, variableMap)); - Type type = d_type.exportTo(exprManager, variableMap); - return new DefineTypeCommand(d_symbol, params, type); -} - -Command* DefineTypeCommand::clone() const { - return new DefineTypeCommand(d_symbol, d_params, d_type); -} - -std::string DefineTypeCommand::getCommandName() const throw() { - return "define-sort"; -} - -/* class DefineFunctionCommand */ - -DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - Expr formula) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_formals(), - d_formula(formula) { -} - -DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - const std::vector<Expr>& formals, - Expr formula) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_formals(formals), - d_formula(formula) { -} - -Expr DefineFunctionCommand::getFunction() const throw() { - return d_func; -} - -const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() { - return d_formals; -} - -Expr DefineFunctionCommand::getFormula() const throw() { - return d_formula; -} - -void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - if(!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula); - } - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); - vector<Expr> formals; - transform(d_formals.begin(), d_formals.end(), back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineFunctionCommand(d_symbol, func, formals, formula); -} - -Command* DefineFunctionCommand::clone() const { - return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); -} - -std::string DefineFunctionCommand::getCommandName() const throw() { - return "define-fun"; -} - -/* class DefineNamedFunctionCommand */ - -DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, - Expr func, - const std::vector<Expr>& formals, - Expr formula) throw() : - DefineFunctionCommand(id, func, formals, formula) { -} - -void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - this->DefineFunctionCommand::invoke(smtEngine); - if(!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); - } - d_commandStatus = CommandSuccess::instance(); -} - -Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Expr func = d_func.exportTo(exprManager, variableMap); - vector<Expr> formals; - transform(d_formals.begin(), d_formals.end(), back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); -} - -Command* DefineNamedFunctionCommand::clone() const { - return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); -} - -/* class SetUserAttribute */ - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : - d_attr( attr ), d_expr( expr ){ -} - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, - std::vector<Expr>& values ) throw() : - d_attr( attr ), d_expr( expr ){ - d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() ); -} - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, - const std::string& value ) throw() : - d_attr( attr ), d_expr( expr ), d_str_value( value ){ -} - -void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){ - try { - if(!d_expr.isNull()) { - smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value ); - } - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ - Expr expr = d_expr.exportTo(exprManager, variableMap); - SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value ); - c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); - return c; -} - -Command* SetUserAttributeCommand::clone() const{ - SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value ); - c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); - return c; -} - -std::string SetUserAttributeCommand::getCommandName() const throw() { - return "set-user-attribute"; -} - -/* class SimplifyCommand */ - -SimplifyCommand::SimplifyCommand(Expr term) throw() : - d_term(term) { -} - -Expr SimplifyCommand::getTerm() const throw() { - return d_term; -} - -void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->simplify(d_term); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Expr SimplifyCommand::getResult() const throw() { - return d_result; -} - -void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* SimplifyCommand::clone() const { - SimplifyCommand* c = new SimplifyCommand(d_term); - c->d_result = d_result; - return c; -} - -std::string SimplifyCommand::getCommandName() const throw() { - return "simplify"; -} - -/* class ExpandDefinitionsCommand */ - -ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() : - d_term(term) { -} - -Expr ExpandDefinitionsCommand::getTerm() const throw() { - return d_term; -} - -void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() { - d_result = smtEngine->expandDefinitions(d_term); - d_commandStatus = CommandSuccess::instance(); -} - -Expr ExpandDefinitionsCommand::getResult() const throw() { - return d_result; -} - -void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* ExpandDefinitionsCommand::clone() const { - ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); - c->d_result = d_result; - return c; -} - -std::string ExpandDefinitionsCommand::getCommandName() const throw() { - return "expand-definitions"; -} - -/* class GetValueCommand */ - -GetValueCommand::GetValueCommand(Expr term) throw() : - d_terms() { - d_terms.push_back(term); -} - -GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() : - d_terms(terms) { - PrettyCheckArgument(terms.size() >= 1, terms, - "cannot get-value of an empty set of terms"); -} - -const std::vector<Expr>& GetValueCommand::getTerms() const throw() { - return d_terms; -} - -void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { - try { - vector<Expr> result; - ExprManager* em = smtEngine->getExprManager(); - NodeManager* nm = NodeManager::fromExprManager(em); - for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { - Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); - smt::SmtScope scope(smtEngine); - Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); - Node value = Node::fromExpr(smtEngine->getValue(*i)); - if(value.getType().isInteger() && request.getType() == nm->realType()) { - // Need to wrap in special marker so that output printers know this - // is an integer-looking constant that really should be output as - // a rational. Necessary for SMT-LIB standards compliance, but ugly. - value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, - nm->mkConst(AscriptionType(em->realType())), value); - } - result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); - } - d_result = em->mkExpr(kind::SEXPR, result); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Expr GetValueCommand::getResult() const throw() { - return d_result; -} - -void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - expr::ExprDag::Scope scope(out, false); - out << d_result << endl; - } -} - -Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - vector<Expr> exportedTerms; - for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { - exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); - } - GetValueCommand* c = new GetValueCommand(exportedTerms); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* GetValueCommand::clone() const { - GetValueCommand* c = new GetValueCommand(d_terms); - c->d_result = d_result; - return c; -} - -std::string GetValueCommand::getCommandName() const throw() { - return "get-value"; -} - -/* class GetAssignmentCommand */ - -GetAssignmentCommand::GetAssignmentCommand() throw() { -} - -void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getAssignment(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -SExpr GetAssignmentCommand::getResult() const throw() { - return d_result; -} - -void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssignmentCommand* c = new GetAssignmentCommand(); - c->d_result = d_result; - return c; -} - -Command* GetAssignmentCommand::clone() const { - GetAssignmentCommand* c = new GetAssignmentCommand(); - c->d_result = d_result; - return c; -} - -std::string GetAssignmentCommand::getCommandName() const throw() { - return "get-assignment"; -} - -/* class GetModelCommand */ - -GetModelCommand::GetModelCommand() throw() { -} - -void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getModel(); - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -/* Model is private to the library -- for now -Model* GetModelCommand::getResult() const throw() { - return d_result; -} -*/ - -void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << *d_result; - } -} - -Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetModelCommand* c = new GetModelCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetModelCommand::clone() const { - GetModelCommand* c = new GetModelCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetModelCommand::getCommandName() const throw() { - return "get-model"; -} - -/* class GetProofCommand */ - -GetProofCommand::GetProofCommand() throw() { -} - -void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_result = smtEngine->getProof(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Proof* GetProofCommand::getResult() const throw() { - return d_result; -} - -void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - smt::SmtScope scope(d_smtEngine); - d_result->toStream(out); - } -} - -Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetProofCommand::clone() const { - GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetProofCommand::getCommandName() const throw() { - return "get-proof"; -} - -/* class GetInstantiationsCommand */ - -GetInstantiationsCommand::GetInstantiationsCommand() throw() { -} - -void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -//Instantiations* GetInstantiationsCommand::getResult() const throw() { -// return d_result; -//} - -void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_smtEngine->printInstantiations(out); - } -} - -Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetInstantiationsCommand* c = new GetInstantiationsCommand(); - //c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetInstantiationsCommand::clone() const { - GetInstantiationsCommand* c = new GetInstantiationsCommand(); - //c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetInstantiationsCommand::getCommandName() const throw() { - return "get-instantiations"; -} - -/* class GetSynthSolutionCommand */ - -GetSynthSolutionCommand::GetSynthSolutionCommand() throw() { -} - -void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_smtEngine->printSynthSolution(out); - } -} - -Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetSynthSolutionCommand::clone() const { - GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetSynthSolutionCommand::getCommandName() const throw() { - return "get-instantiations"; -} - -/* class GetUnsatCoreCommand */ - -GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { -} - -GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) { -} - -void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getUnsatCore(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_result.toStream(out, d_names); - } -} - -const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { - // of course, this will be empty if the command hasn't been invoked yet - return d_result; -} - -Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); - c->d_result = d_result; - return c; -} - -Command* GetUnsatCoreCommand::clone() const { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); - c->d_result = d_result; - return c; -} - -std::string GetUnsatCoreCommand::getCommandName() const throw() { - return "get-unsat-core"; -} - -/* class GetAssertionsCommand */ - -GetAssertionsCommand::GetAssertionsCommand() throw() { -} - -void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - stringstream ss; - const vector<Expr> v = smtEngine->getAssertions(); - ss << "(\n"; - copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); - ss << ")\n"; - d_result = ss.str(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetAssertionsCommand::getResult() const throw() { - return d_result; -} - -void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result; - } -} - -Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssertionsCommand* c = new GetAssertionsCommand(); - c->d_result = d_result; - return c; -} - -Command* GetAssertionsCommand::clone() const { - GetAssertionsCommand* c = new GetAssertionsCommand(); - c->d_result = d_result; - return c; -} - -std::string GetAssertionsCommand::getCommandName() const throw() { - return "get-assertions"; -} - -/* class SetBenchmarkStatusCommand */ - -SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : - d_status(status) { -} - -BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { - return d_status; -} - -void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { - try { - stringstream ss; - ss << d_status; - SExpr status = SExpr(ss.str()); - smtEngine->setInfo("status", status); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetBenchmarkStatusCommand(d_status); -} - -Command* SetBenchmarkStatusCommand::clone() const { - return new SetBenchmarkStatusCommand(d_status); -} - -std::string SetBenchmarkStatusCommand::getCommandName() const throw() { - return "set-info"; -} - -/* class SetBenchmarkLogicCommand */ - -SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : - d_logic(logic) { -} - -std::string SetBenchmarkLogicCommand::getLogic() const throw() { - return d_logic; -} - -void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setLogic(d_logic); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetBenchmarkLogicCommand(d_logic); -} - -Command* SetBenchmarkLogicCommand::clone() const { - return new SetBenchmarkLogicCommand(d_logic); -} - -std::string SetBenchmarkLogicCommand::getCommandName() const throw() { - return "set-logic"; -} - -/* class SetInfoCommand */ - -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : - d_flag(flag), - d_sexpr(sexpr) { -} - -std::string SetInfoCommand::getFlag() const throw() { - return d_flag; -} - -SExpr SetInfoCommand::getSExpr() const throw() { - return d_sexpr; -} - -void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setInfo(d_flag, d_sexpr); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - // As per SMT-LIB spec, silently accept unknown set-info keys - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetInfoCommand(d_flag, d_sexpr); -} - -Command* SetInfoCommand::clone() const { - return new SetInfoCommand(d_flag, d_sexpr); -} - -std::string SetInfoCommand::getCommandName() const throw() { - return "set-info"; -} - -/* class GetInfoCommand */ - -GetInfoCommand::GetInfoCommand(std::string flag) throw() : - d_flag(flag) { -} - -std::string GetInfoCommand::getFlag() const throw() { - return d_flag; -} - -void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { - try { - vector<SExpr> v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.push_back(smtEngine->getInfo(d_flag)); - stringstream ss; - if(d_flag == "all-options" || d_flag == "all-statistics") { - ss << PrettySExprs(true); - } - ss << SExpr(v); - d_result = ss.str(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetInfoCommand::getResult() const throw() { - return d_result; -} - -void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else if(d_result != "") { - out << d_result << endl; - } -} - -Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetInfoCommand* c = new GetInfoCommand(d_flag); - c->d_result = d_result; - return c; -} - -Command* GetInfoCommand::clone() const { - GetInfoCommand* c = new GetInfoCommand(d_flag); - c->d_result = d_result; - return c; -} - -std::string GetInfoCommand::getCommandName() const throw() { - return "get-info"; -} - -/* class SetOptionCommand */ - -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : - d_flag(flag), - d_sexpr(sexpr) { -} - -std::string SetOptionCommand::getFlag() const throw() { - return d_flag; -} - -SExpr SetOptionCommand::getSExpr() const throw() { - return d_sexpr; -} - -void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setOption(d_flag, d_sexpr); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetOptionCommand(d_flag, d_sexpr); -} - -Command* SetOptionCommand::clone() const { - return new SetOptionCommand(d_flag, d_sexpr); -} - -std::string SetOptionCommand::getCommandName() const throw() { - return "set-option"; -} - -/* class GetOptionCommand */ - -GetOptionCommand::GetOptionCommand(std::string flag) throw() : - d_flag(flag) { -} - -std::string GetOptionCommand::getFlag() const throw() { - return d_flag; -} - -void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - SExpr res = smtEngine->getOption(d_flag); - d_result = res.toString(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetOptionCommand::getResult() const throw() { - return d_result; -} - -void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else if(d_result != "") { - out << d_result << endl; - } -} - -Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetOptionCommand* c = new GetOptionCommand(d_flag); - c->d_result = d_result; - return c; -} - -Command* GetOptionCommand::clone() const { - GetOptionCommand* c = new GetOptionCommand(d_flag); - c->d_result = d_result; - return c; -} - -std::string GetOptionCommand::getCommandName() const throw() { - return "get-option"; -} - -/* class DatatypeDeclarationCommand */ - -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : - d_datatypes() { - d_datatypes.push_back(datatype); -} - -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() : - d_datatypes(datatypes) { -} - -const std::vector<DatatypeType>& -DatatypeDeclarationCommand::getDatatypes() const throw() { - return d_datatypes; -} - -void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - throw ExportUnsupportedException - ("export of DatatypeDeclarationCommand unsupported"); -} - -Command* DatatypeDeclarationCommand::clone() const { - return new DatatypeDeclarationCommand(d_datatypes); -} - -std::string DatatypeDeclarationCommand::getCommandName() const throw() { - return "declare-datatypes"; -} - -/* class RewriteRuleCommand */ - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - Expr head, Expr body, - const Triggers& triggers) throw() : - d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) { -} - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - Expr head, Expr body) throw() : - d_vars(vars), d_head(head), d_body(body) { -} - -const std::vector<Expr>& RewriteRuleCommand::getVars() const throw() { - return d_vars; -} - -const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() { - return d_guards; -} - -Expr RewriteRuleCommand::getHead() const throw() { - return d_head; -} - -Expr RewriteRuleCommand::getBody() const throw() { - return d_body; -} - -const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() { - return d_triggers; -} - -void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { - try { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if(d_guards.size() == 0) guards = em->mkConst<bool>(true); - else if(d_guards.size() == 1) guards = d_guards[0]; - else guards = em->mkExpr(kind::AND,d_guards); - /** build expression */ - Expr expr; - if( d_triggers.empty() ){ - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body); - } else { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for(Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); i != end; ++i){ - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - /** Convert variables */ - VExpr vars; vars.reserve(d_vars.size()); - for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); - i == end; ++i){ - vars.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert guards */ - VExpr guards; guards.reserve(d_guards.size()); - for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); - i == end; ++i){ - guards.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert triggers */ - Triggers triggers; triggers.resize(d_triggers.size()); - for(size_t i = 0, end = d_triggers.size(); - i < end; ++i){ - triggers[i].reserve(d_triggers[i].size()); - for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); - j == jend; ++i){ - triggers[i].push_back(j->exportTo(exprManager, variableMap)); - }; - }; - /** Convert head and body */ - Expr head = d_head.exportTo(exprManager, variableMap); - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new RewriteRuleCommand(vars, guards, head, body, triggers); -} - -Command* RewriteRuleCommand::clone() const { - return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); -} - -std::string RewriteRuleCommand::getCommandName() const throw() { - return "rewrite-rule"; -} - -/* class PropagateRuleCommand */ - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body, - const Triggers& triggers, - bool deduction) throw() : - d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) { -} - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& heads, - Expr body, - bool deduction) throw() : - d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) { -} - -const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() { - return d_vars; -} - -const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() { - return d_guards; -} - -const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() { - return d_heads; -} - -Expr PropagateRuleCommand::getBody() const throw() { - return d_body; -} - -const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() { - return d_triggers; -} - -bool PropagateRuleCommand::isDeduction() const throw() { - return d_deduction; -} - -void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { - try { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if(d_guards.size() == 0) guards = em->mkConst<bool>(true); - else if(d_guards.size() == 1) guards = d_guards[0]; - else guards = em->mkExpr(kind::AND,d_guards); - /** build heads list */ - Expr heads; - if(d_heads.size() == 1) heads = d_heads[0]; - else heads = em->mkExpr(kind::AND,d_heads); - /** build expression */ - Expr expr; - if( d_triggers.empty() ){ - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body); - } else { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for(Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); i != end; ++i){ - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - /** Convert variables */ - VExpr vars; vars.reserve(d_vars.size()); - for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); - i == end; ++i){ - vars.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert guards */ - VExpr guards; guards.reserve(d_guards.size()); - for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); - i == end; ++i){ - guards.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert heads */ - VExpr heads; heads.reserve(d_heads.size()); - for(VExpr::iterator i = d_heads.begin(), end = d_heads.end(); - i == end; ++i){ - heads.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert triggers */ - Triggers triggers; triggers.resize(d_triggers.size()); - for(size_t i = 0, end = d_triggers.size(); - i < end; ++i){ - triggers[i].reserve(d_triggers[i].size()); - for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); - j == jend; ++i){ - triggers[i].push_back(j->exportTo(exprManager, variableMap)); - }; - }; - /** Convert head and body */ - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new PropagateRuleCommand(vars, guards, heads, body, triggers); -} - -Command* PropagateRuleCommand::clone() const { - return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers); -} - -std::string PropagateRuleCommand::getCommandName() const throw() { - return "propagate-rule"; -} - -/* output stream insertion operator for benchmark statuses */ -std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) throw() { - switch(status) { - - case SMT_SATISFIABLE: - return out << "sat"; - - case SMT_UNSATISFIABLE: - return out << "unsat"; - - case SMT_UNKNOWN: - return out << "unknown"; - - default: - return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; - } -} - -}/* CVC4 namespace */ diff --git a/src/smt_util/command.h b/src/smt_util/command.h deleted file mode 100644 index 248e69b0e..000000000 --- a/src/smt_util/command.h +++ /dev/null @@ -1,905 +0,0 @@ -/********************* */ -/*! \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_util/command.i b/src/smt_util/command.i deleted file mode 100644 index e4744c4f4..000000000 --- a/src/smt_util/command.i +++ /dev/null @@ -1,77 +0,0 @@ -%{ -#include "smt_util/command.h" - -#ifdef SWIGJAVA - -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ -%} - -%ignore CVC4::operator<<(std::ostream&, const Command&) throw(); -%ignore CVC4::operator<<(std::ostream&, const Command*) throw(); -%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw(); -%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw(); -%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); -%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw(); - -%ignore CVC4::GetProofCommand; -%ignore CVC4::CommandPrintSuccess::Scope; - -#ifdef SWIGJAVA - -// Instead of CommandSequence::begin() and end(), create an -// iterator() method on the Java side that returns a Java-style -// Iterator. -%ignore CVC4::CommandSequence::begin(); -%ignore CVC4::CommandSequence::end(); -%ignore CVC4::CommandSequence::begin() const; -%ignore CVC4::CommandSequence::end() const; -%extend CVC4::CommandSequence { - CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() { - return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self); - } -} - -// CommandSequence is "iterable" on the Java side -%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>"; -// add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public edu.nyu.acsys.CVC4.Command next() { - if(hasNext()) { - return getNext(); - } else { - throw new java.util.NoSuchElementException(); - } - } -" -// getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private"; - -// map the types appropriately -%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject"; -%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; } - -#endif /* SWIGJAVA */ - -%include "smt_util/command.h" - -#ifdef SWIGJAVA - -%include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" - -%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>; - -#endif /* SWIGJAVA */ diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp deleted file mode 100644 index 66cb6e3d1..000000000 --- a/src/smt_util/dump.cpp +++ /dev/null @@ -1,221 +0,0 @@ -/********************* */ -/*! \file dump.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Dump utility classes and functions - ** - ** Dump utility classes and functions. - **/ -#include "smt_util/dump.h" - -#include "base/output.h" - -namespace CVC4 { - -DumpC DumpChannel CVC4_PUBLIC; - -std::ostream& DumpC::setStream(std::ostream* os) { - ::CVC4::DumpOutChannel.setStream(os); - return *os; -} -std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); } -std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); } - - -void DumpC::setDumpFromString(const std::string& optarg) { -#ifdef CVC4_DUMPING - char* optargPtr = strdup(optarg.c_str()); - char* tokstr = optargPtr; - char* toksave; - while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) { - tokstr = NULL; - if(!strcmp(optargPtr, "benchmark")) { - } else if(!strcmp(optargPtr, "declarations")) { - } else if(!strcmp(optargPtr, "assertions")) { - Dump.on("assertions:post-everything"); - } else if(!strncmp(optargPtr, "assertions:", 11)) { - const char* p = optargPtr + 11; - if(!strncmp(p, "pre-", 4)) { - p += 4; - } else if(!strncmp(p, "post-", 5)) { - p += 5; - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - if(!strcmp(p, "everything")) { - } else if(!strcmp(p, "definition-expansion")) { - } else if(!strcmp(p, "boolean-terms")) { - } else if(!strcmp(p, "constrain-subtypes")) { - } else if(!strcmp(p, "substitution")) { - } else if(!strcmp(p, "strings-pp")) { - } else if(!strcmp(p, "skolem-quant")) { - } else if(!strcmp(p, "simplify")) { - } else if(!strcmp(p, "static-learning")) { - } else if(!strcmp(p, "ite-removal")) { - } else if(!strcmp(p, "repeat-simplify")) { - } else if(!strcmp(p, "rewrite-apply-to-const")) { - } else if(!strcmp(p, "theory-preprocessing")) { - } else if(!strcmp(p, "nonclausal")) { - } else if(!strcmp(p, "theorypp")) { - } else if(!strcmp(p, "itesimp")) { - } else if(!strcmp(p, "unconstrained")) { - } else if(!strcmp(p, "repeatsimp")) { - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - Dump.on("assertions"); - } else if(!strcmp(optargPtr, "skolems")) { - } else if(!strcmp(optargPtr, "clauses")) { - } else if(!strcmp(optargPtr, "t-conflicts") || - !strcmp(optargPtr, "t-lemmas") || - !strcmp(optargPtr, "t-explanations") || - !strcmp(optargPtr, "bv-rewrites") || - !strcmp(optargPtr, "theory::fullcheck")) { - // These are "non-state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is dumped, it will interfere with the validity - // of these generated queries. - if(Dump.isOn("state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("no-permit-state"); - } - } else if(!strcmp(optargPtr, "state") || - !strcmp(optargPtr, "missed-t-conflicts") || - !strcmp(optargPtr, "t-propagations") || - !strcmp(optargPtr, "missed-t-propagations")) { - // These are "state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is not dumped, it will interfere with the - // validity of these generated queries. - if(Dump.isOn("no-permit-state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "non-state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("state"); - } - } else if(!strcmp(optargPtr, "help")) { - puts(s_dumpHelp.c_str()); - exit(1); - } else if(!strcmp(optargPtr, "bv-abstraction")) { - Dump.on("bv-abstraction"); - } else if(!strcmp(optargPtr, "bv-algebraic")) { - Dump.on("bv-algebraic"); - } else { - throw OptionException(std::string("unknown option for --dump: `") + - optargPtr + "'. Try --dump help."); - } - - Dump.on(optargPtr); - Dump.on("benchmark"); - if(strcmp(optargPtr, "benchmark")) { - Dump.on("declarations"); - if(strcmp(optargPtr, "declarations")) { - Dump.on("skolems"); - } - } - } - free(optargPtr); -#else /* CVC4_DUMPING */ - throw OptionException("The dumping feature was disabled in this build of CVC4."); -#endif /* CVC4_DUMPING */ -} - - -const std::string DumpC::s_dumpHelp = "\ -Dump modes currently supported by the --dump option:\n\ -\n\ -benchmark\n\ -+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ - does not include any declarations or assertions. Implied by all following\n\ - modes.\n\ -\n\ -declarations\n\ -+ Dump user declarations. Implied by all following modes.\n\ -\n\ -skolems\n\ -+ Dump internally-created skolem variable declarations. These can\n\ - arise from preprocessing simplifications, existential elimination,\n\ - and a number of other things. Implied by all following modes.\n\ -\n\ -assertions\n\ -+ Output the assertions after preprocessing and before clausification.\n\ - Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ - where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ - simplify static-learning ite-removal repeat-simplify\n\ - rewrite-apply-to-const theory-preprocessing.\n\ - PASS can also be the special value \"everything\", in which case the\n\ - assertions are printed before any preprocessing (with\n\ - \"assertions:pre-everything\") or after all preprocessing completes\n\ - (with \"assertions:post-everything\").\n\ -\n\ -clauses\n\ -+ Do all the preprocessing outlined above, and dump the CNF-converted\n\ - output\n\ -\n\ -state\n\ -+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ - Implied by all \"stateful\" modes below and conflicts with all\n\ - non-stateful modes below.\n\ -\n\ -t-conflicts [non-stateful]\n\ -+ Output correctness queries for all theory conflicts\n\ -\n\ -missed-t-conflicts [stateful]\n\ -+ Output completeness queries for theory conflicts\n\ -\n\ -t-propagations [stateful]\n\ -+ Output correctness queries for all theory propagations\n\ -\n\ -missed-t-propagations [stateful]\n\ -+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ -\n\ -t-lemmas [non-stateful]\n\ -+ Output correctness queries for all theory lemmas\n\ -\n\ -t-explanations [non-stateful]\n\ -+ Output correctness queries for all theory explanations\n\ -\n\ -bv-rewrites [non-stateful]\n\ -+ Output correctness queries for all bitvector rewrites\n\ -\n\ -bv-abstraction [non-stateful]\n\ -+ Output correctness queries for all bv abstraction \n\ -\n\ -bv-algebraic [non-stateful]\n\ -+ Output correctness queries for bv algebraic solver. \n\ -\n\ -theory::fullcheck [non-stateful]\n \ -+ Output completeness queries for all full-check effort-level theory checks\n\ -\n\ -Dump modes can be combined with multiple uses of --dump. Generally you want\n\ -one from the assertions category (either assertions or clauses), and\n\ -perhaps one or more stateful or non-stateful modes for checking correctness\n\ -and completeness of decision procedure implementations. Stateful modes dump\n\ -the contextual assertions made by the core solver (all decisions and\n\ -propagations as assertions; that affects the validity of the resulting\n\ -correctness and completeness queries, so of course stateful and non-stateful\n\ -modes cannot be mixed in the same run.\n\ -\n\ -The --output-language option controls the language used for dumping, and\n\ -this allows you to connect CVC4 to another solver implementation via a UNIX\n\ -pipe to perform on-line checking. The --dump-to option can be used to dump\n\ -to a file.\n\ -"; - -}/* CVC4 namespace */ diff --git a/src/smt_util/dump.h b/src/smt_util/dump.h deleted file mode 100644 index 19f9118e3..000000000 --- a/src/smt_util/dump.h +++ /dev/null @@ -1,123 +0,0 @@ -/********************* */ -/*! \file dump.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Dump utility classes and functions - ** - ** Dump utility classes and functions. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__DUMP_H -#define __CVC4__DUMP_H - -#include "base/output.h" -#include "smt_util/command.h" - -namespace CVC4 { - -class CVC4_PUBLIC CVC4dumpstream { - -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - std::ostream* d_os; -#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ - -#ifdef CVC4_PORTFOLIO - CommandSequence* d_commands; -#endif /* CVC4_PORTFOLIO */ - -public: - CVC4dumpstream() throw() -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(NULL), d_commands(NULL) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(NULL) -#elif defined(CVC4_PORTFOLIO) - : d_commands(NULL) -#endif /* CVC4_PORTFOLIO */ - { } - - CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw() -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(&os), d_commands(&commands) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(&os) -#elif defined(CVC4_PORTFOLIO) - : d_commands(&commands) -#endif /* CVC4_PORTFOLIO */ - { } - - CVC4dumpstream& operator<<(const Command& c) { -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - if(d_os != NULL) { - (*d_os) << c << std::endl; - } -#endif -#if defined(CVC4_PORTFOLIO) - if(d_commands != NULL) { - d_commands->addCommand(c.clone()); - } -#endif - return *this; - } -};/* class CVC4dumpstream */ - -/** The dump class */ -class CVC4_PUBLIC DumpC { - std::set<std::string> d_tags; - CommandSequence d_commands; - - static const std::string s_dumpHelp; - -public: - CVC4dumpstream operator()(const char* tag) { - if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); - } else { - return CVC4dumpstream(); - } - } - - CVC4dumpstream operator()(std::string tag) { - if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); - } else { - return CVC4dumpstream(); - } - } - - void clear() { d_commands.clear(); } - const CommandSequence& getCommands() const { return d_commands; } - - bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } - bool on (std::string tag) { d_tags.insert(tag); return true; } - bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } - bool off(std::string tag) { d_tags.erase (tag); return false; } - bool off() { d_tags.clear(); return false; } - - bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } - bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } - - std::ostream& setStream(std::ostream* os); - std::ostream& getStream(); - std::ostream* getStreamPointer(); - - void setDumpFromString(const std::string& optarg); -};/* class DumpC */ - -/** The dump singleton */ -extern DumpC DumpChannel CVC4_PUBLIC; - -#define Dump ::CVC4::DumpChannel - -}/* CVC4 namespace */ - -#endif /* __CVC4__DUMP_H */ diff --git a/src/smt_util/ite_removal.cpp b/src/smt_util/ite_removal.cpp deleted file mode 100644 index 0d1c7b61e..000000000 --- a/src/smt_util/ite_removal.cpp +++ /dev/null @@ -1,192 +0,0 @@ -/********************* */ -/*! \file ite_removal.cpp - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Tim King, Morgan Deters - ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Removal of term ITEs - ** - ** Removal of term ITEs. - **/ -#include "smt_util/ite_removal.h" - -#include <vector> - -#include "proof/proof_manager.h" -#include "smt_util/command.h" -#include "theory/ite_utilities.h" - -using namespace CVC4; -using namespace std; - -namespace CVC4 { - -RemoveITE::RemoveITE(context::UserContext* u) - : d_iteCache(u) -{ - d_containsVisitor = new theory::ContainsTermITEVisitor(); -} - -RemoveITE::~RemoveITE(){ - delete d_containsVisitor; -} - -void RemoveITE::garbageCollect(){ - d_containsVisitor->garbageCollect(); -} - -theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() { - return d_containsVisitor; -} - -size_t RemoveITE::collectedCacheSizes() const{ - return d_containsVisitor->cache_size() + d_iteCache.size(); -} - -void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) -{ - size_t n = output.size(); - for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { - // Do this in two steps to avoid Node problems(?) - // Appears related to bug 512, splitting this into two lines - // fixes the bug on clang on Mac OS - Node itesRemoved = run(output[i], output, iteSkolemMap, false); - // In some calling contexts, not necessary to report dependence information. - if(reportDeps && options::unsatCores()) { - // new assertions have a dependence on the node - PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) - while(n < output.size()) { - PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) - ++n; - } - } - output[i] = itesRemoved; - } -} - -bool RemoveITE::containsTermITE(TNode e) const { - return d_containsVisitor->containsTermITE(e); -} - -Node RemoveITE::run(TNode node, std::vector<Node>& output, - IteSkolemMap& iteSkolemMap, bool inQuant) { - // Current node - Debug("ite") << "removeITEs(" << node << ")" << endl; - - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ - return Node(node); - } - - // The result may be cached already - std::pair<Node, bool> cacheKey(node, inQuant); - NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(cacheKey); - if(i != d_iteCache.end()) { - Node cached = (*i).second; - Debug("ite") << "removeITEs: in-cache: " << cached << endl; - return cached.isNull() ? Node(node) : cached; - } - - // Remember that we're inside a quantifier - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - inQuant = true; - } - - // If an ITE replace it - if(node.getKind() == kind::ITE) { - TypeNode nodeType = node.getType(); - if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { - Node skolem; - // Make the skolem to represent the ITE - skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); - - // The new assertion - Node newAssertion = - nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), - skolem.eqNode(node[2])); - Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; - - // Attach the skolem - d_iteCache.insert(cacheKey, skolem); - - // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, inQuant); - - iteSkolemMap[skolem] = output.size(); - output.push_back(newAssertion); - - // The representation is now the skolem - return skolem; - } - } - - // If not an ITE, go deep - vector<Node> newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Remove the ITEs from the children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap, inQuant); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - // If changes, we rewrite - if(somethingChanged) { - Node cached = nodeManager->mkNode(node.getKind(), newChildren); - d_iteCache.insert(cacheKey, cached); - return cached; - } else { - d_iteCache.insert(cacheKey, Node::null()); - return node; - } -} - -Node RemoveITE::replace(TNode node, bool inQuant) const { - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ - return Node(node); - } - - // Check the cache - NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant)); - if(i != d_iteCache.end()) { - Node cached = (*i).second; - return cached.isNull() ? Node(node) : cached; - } - - // Remember that we're inside a quantifier - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - inQuant = true; - } - - vector<Node> newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Replace in children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = replace(*it, inQuant); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - // If changes, we rewrite - if(somethingChanged) { - return nodeManager->mkNode(node.getKind(), newChildren); - } else { - return node; - } -} - -}/* CVC4 namespace */ diff --git a/src/smt_util/ite_removal.h b/src/smt_util/ite_removal.h deleted file mode 100644 index 0cc0ea5d0..000000000 --- a/src/smt_util/ite_removal.h +++ /dev/null @@ -1,93 +0,0 @@ -/********************* */ -/*! \file ite_removal.h - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters - ** Minor contributors (to current version): Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Removal of term ITEs - ** - ** Removal of term ITEs. - **/ - -#include "cvc4_private.h" - -#pragma once - -#include <vector> - -#include "context/cdinsert_hashmap.h" -#include "context/context.h" -#include "expr/node.h" -#include "smt_util/dump.h" -#include "util/bool.h" -#include "util/hash.h" - -namespace CVC4 { - -namespace theory { - class ContainsTermITEVisitor; -}/* CVC4::theory namespace */ - -typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; - -class RemoveITE { - typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache; - ITECache d_iteCache; - - -public: - - RemoveITE(context::UserContext* u); - ~RemoveITE(); - - /** - * Removes the ITE nodes by introducing skolem variables. All - * additional assertions are pushed into assertions. iteSkolemMap - * contains a map from introduced skolem variables to the index in - * assertions containing the new Boolean ite created in conjunction - * with that skolem variable. - * - * With reportDeps true, report reasoning dependences to the proof - * manager (for unsat cores). - */ - void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); - - /** - * Removes the ITE from the node by introducing skolem - * variables. All additional assertions are pushed into - * assertions. iteSkolemMap contains a map from introduced skolem - * variables to the index in assertions containing the new Boolean - * ite created in conjunction with that skolem variable. - */ - Node run(TNode node, std::vector<Node>& additionalAssertions, - IteSkolemMap& iteSkolemMap, bool inQuant); - - /** - * Substitute under node using pre-existing cache. Do not remove - * any ITEs not seen during previous runs. - */ - Node replace(TNode node, bool inQuant = false) const; - - /** Returns true if e contains a term ite. */ - bool containsTermITE(TNode e) const; - - /** Returns the collected size of the caches. */ - size_t collectedCacheSizes() const; - - /** Garbage collects non-context dependent data-structures. */ - void garbageCollect(); - - /** Return the RemoveITE's containsVisitor. */ - theory::ContainsTermITEVisitor* getContainsVisitor(); - -private: - theory::ContainsTermITEVisitor* d_containsVisitor; - -};/* class RemoveTTE */ - -}/* CVC4 namespace */ diff --git a/src/smt_util/model.cpp b/src/smt_util/model.cpp deleted file mode 100644 index ddac7e263..000000000 --- a/src/smt_util/model.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/********************* */ -/*! \file model.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief implementation of Model class - **/ - -#include "smt_util/model.h" - -#include <vector> - -#include "expr/expr_iomanip.h" -#include "options/base_options.h" -#include "printer/printer.h" -#include "smt/command_list.h" -#include "smt/smt_engine_scope.h" -#include "smt_util/command.h" - -using namespace std; - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, const Model& m) { - smt::SmtScope smts(&m.d_smt); - expr::ExprDag::Scope scope(out, false); - Printer::getPrinter(options::outputLanguage())->toStream(out, m); - return out; -} - -Model::Model() : - d_smt(*smt::currentSmtEngine()) { -} - -size_t Model::getNumCommands() const { - return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); -} - -const Command* Model::getCommand(size_t i) const { - Assert(i < getNumCommands()); - // index the global commands first, then the locals - if(i < d_smt.d_modelGlobalCommands.size()) { - return d_smt.d_modelGlobalCommands[i]; - } else { - return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; - } -} - -}/* CVC4 namespace */ diff --git a/src/smt_util/model.h b/src/smt_util/model.h deleted file mode 100644 index 33a9312a6..000000000 --- a/src/smt_util/model.h +++ /dev/null @@ -1,78 +0,0 @@ -/********************* */ -/*! \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 */ |