diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 16 | ||||
-rw-r--r-- | src/smt/dump.cpp | 100 | ||||
-rw-r--r-- | src/smt/dump.h | 22 | ||||
-rw-r--r-- | src/smt/dump_manager.cpp | 12 | ||||
-rw-r--r-- | src/smt/dump_manager.h | 4 | ||||
-rw-r--r-- | src/smt/listeners.cpp | 12 | ||||
-rw-r--r-- | src/smt/listeners.h | 5 | ||||
-rw-r--r-- | src/smt/output_manager.cpp | 35 | ||||
-rw-r--r-- | src/smt/output_manager.h | 57 | ||||
-rw-r--r-- | src/smt/preprocessor.cpp | 6 | ||||
-rw-r--r-- | src/smt/process_assertions.cpp | 5 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 188 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 15 | ||||
-rw-r--r-- | src/smt/smt_solver.cpp | 17 | ||||
-rw-r--r-- | src/smt/sygus_solver.cpp | 15 | ||||
-rw-r--r-- | src/smt/sygus_solver.h | 10 | ||||
-rw-r--r-- | src/smt/term_formula_removal.h | 1 |
17 files changed, 322 insertions, 198 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 64ef60906..38c799fca 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -106,20 +106,6 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) } // !!! Temporary until commands are migrated to the new API !!! -std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs) -{ - std::vector<Node> nodes; - nodes.reserve(exprs.size()); - - for (Expr e : exprs) - { - nodes.push_back(Node::fromExpr(e)); - } - - return nodes; -} - -// !!! Temporary until commands are migrated to the new API !!! std::vector<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types) { std::vector<TypeNode> typeNodes; @@ -2977,7 +2963,7 @@ void SetBenchmarkStatusCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Result::Sat status; + Result::Sat status = Result::SAT_UNKNOWN; switch (d_status) { case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break; diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index d8d486e12..28cf8a34f 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -19,9 +19,29 @@ #include "base/output.h" #include "lib/strtok_r.h" #include "preprocessing/preprocessing_pass_registry.h" +#include "smt/command.h" +#include "smt/node_command.h" namespace CVC4 { +CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) +{ + if (d_os != nullptr) + { + (*d_os) << c; + } + return *this; +} + +CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) +{ + if (d_os != nullptr) + { + (*d_os) << nc; + } + return *this; +} + DumpC DumpChannel CVC4_PUBLIC; std::ostream& DumpC::setStream(std::ostream* os) { @@ -100,42 +120,6 @@ void DumpC::setDumpFromString(const std::string& optarg) { || !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")) { @@ -152,14 +136,6 @@ void DumpC::setDumpFromString(const std::string& optarg) { puts(ss.str().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: `") @@ -222,49 +198,25 @@ 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\ +t-conflicts\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\ +t-lemmas\n\ + Output correctness queries for all theory lemmas\n\ \n\ -t-explanations [non-stateful]\n\ +t-explanations\n\ + Output correctness queries for all theory explanations\n\ \n\ -bv-rewrites [non-stateful]\n\ +bv-rewrites\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\ +theory::fullcheck\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\ raw-benchmark or, alternatively, one from the assertions category (either\n\ -assertions or clauses), and perhaps one or more stateful or non-stateful modes\n\ +assertions or clauses), and perhaps one or more other modes\n\ for checking correctness and completeness of decision procedure implementations.\n\ -Stateful modes dump the contextual assertions made by the core solver (all\n\ -decisions and propagations as assertions); this affects the validity of the\n\ -resulting correctness and completeness queries, so of course stateful and\n\ -non-stateful 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\ diff --git a/src/smt/dump.h b/src/smt/dump.h index 4c0efeb6e..ec13a9ae9 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -20,11 +20,12 @@ #define CVC4__DUMP_H #include "base/output.h" -#include "smt/command.h" -#include "smt/node_command.h" namespace CVC4 { +class Command; +class NodeCommand; + #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) class CVC4_PUBLIC CVC4dumpstream @@ -33,27 +34,14 @@ class CVC4_PUBLIC CVC4dumpstream CVC4dumpstream() : d_os(nullptr) {} CVC4dumpstream(std::ostream& os) : d_os(&os) {} - CVC4dumpstream& operator<<(const Command& c) { - if (d_os != nullptr) - { - (*d_os) << c << std::endl; - } - return *this; - } + CVC4dumpstream& operator<<(const Command& c); /** A convenience function for dumping internal commands. * * Since Commands are now part of the public API, internal code should use * NodeCommands and this function (instead of the one above) to dump them. */ - CVC4dumpstream& operator<<(const NodeCommand& nc) - { - if (d_os != nullptr) - { - (*d_os) << nc << std::endl; - } - return *this; - } + CVC4dumpstream& operator<<(const NodeCommand& nc); private: std::ostream* d_os; diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 033be405f..849339106 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -17,6 +17,7 @@ #include "expr/expr_manager.h" #include "options/smt_options.h" #include "smt/dump.h" +#include "smt/node_command.h" namespace CVC4 { namespace smt { @@ -98,11 +99,11 @@ void DumpManager::setPrintFuncInModel(Node f, bool p) Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; for (std::unique_ptr<NodeCommand>& c : d_modelGlobalCommands) { - DeclareFunctionCommand* dfc = - dynamic_cast<DeclareFunctionCommand*>(c.get()); + DeclareFunctionNodeCommand* dfc = + dynamic_cast<DeclareFunctionNodeCommand*>(c.get()); if (dfc != NULL) { - Node df = Node::fromExpr(dfc->getFunction()); + Node df = dfc->getFunction(); if (df == f) { dfc->setPrintInModel(p); @@ -111,10 +112,11 @@ void DumpManager::setPrintFuncInModel(Node f, bool p) } for (NodeCommand* c : d_modelCommands) { - DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c); + DeclareFunctionNodeCommand* dfc = + dynamic_cast<DeclareFunctionNodeCommand*>(c); if (dfc != NULL) { - Node df = Node::fromExpr(dfc->getFunction()); + Node df = dfc->getFunction(); if (df == f) { dfc->setPrintInModel(p); diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 2ce0570e4..5954817bd 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -22,9 +22,11 @@ #include "context/cdlist.h" #include "expr/node.h" -#include "smt/node_command.h" namespace CVC4 { + +class NodeCommand; + namespace smt { /** diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 52ddcf156..fdf32fa41 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -18,9 +18,10 @@ #include "expr/expr.h" #include "expr/node_manager_attributes.h" #include "options/smt_options.h" -#include "smt/node_command.h" +#include "printer/printer.h" #include "smt/dump.h" #include "smt/dump_manager.h" +#include "smt/node_command.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -36,7 +37,11 @@ void ResourceOutListener::notify() d_smt.interrupt(); } -SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm) : d_dm(dm) {} +SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm, + OutputManager& outMgr) + : d_dm(dm), d_outMgr(outMgr) +{ +} void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags) { @@ -92,7 +97,8 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, DeclareFunctionNodeCommand c(id, n, n.getType()); if (Dump.isOn("skolems") && comment != "") { - Dump("skolems") << CommentCommand(id + " is " + comment); + d_outMgr.getPrinter().toStreamCmdComment(d_outMgr.getDumpOut(), + id + " is " + comment); } if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { diff --git a/src/smt/listeners.h b/src/smt/listeners.h index 77d6d257f..0efbed096 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -24,6 +24,7 @@ namespace CVC4 { +class OutputManager; class SmtEngine; namespace smt { @@ -49,7 +50,7 @@ class DumpManager; class SmtNodeManagerListener : public NodeManagerListener { public: - SmtNodeManagerListener(DumpManager& dm); + SmtNodeManagerListener(DumpManager& dm, OutputManager& outMgr); /** Notify when new sort is created */ void nmNotifyNewSort(TypeNode tn, uint32_t flags) override; /** Notify when new sort constructor is created */ @@ -69,6 +70,8 @@ class SmtNodeManagerListener : public NodeManagerListener private: /** Reference to the dump manager of smt engine */ DumpManager& d_dm; + /** Reference to the output manager of the smt engine */ + OutputManager& d_outMgr; }; } // namespace smt diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp new file mode 100644 index 000000000..a801b7527 --- /dev/null +++ b/src/smt/output_manager.cpp @@ -0,0 +1,35 @@ +/********************* */ +/*! \file output_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of OutputManager functions. + ** + ** Implementation of OutputManager functions. + **/ + +#include "smt/output_manager.h" + +#include "smt/smt_engine.h" + +namespace CVC4 { + +OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {} + +const Printer& OutputManager::getPrinter() const +{ + return *d_smt->getPrinter(); +} + +std::ostream& OutputManager::getDumpOut() const +{ + return *d_smt->getOptions().getOut(); +} + +} // namespace CVC4 diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h new file mode 100644 index 000000000..5ffd6b964 --- /dev/null +++ b/src/smt/output_manager.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file output_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The output manager for the SmtEngine. + ** + ** The output manager provides helper functions for printing commands + ** internally. + **/ + +#ifndef CVC4__SMT__OUTPUT_MANAGER_H +#define CVC4__SMT__OUTPUT_MANAGER_H + +#include <ostream> + +namespace CVC4 { + +class Printer; +class SmtEngine; + +/** This utility class provides helper functions for printing commands + * internally */ +class OutputManager +{ + public: + /** Constructor + * + * @param smt SMT engine to manage output for + */ + explicit OutputManager(SmtEngine* smt); + + /** Get the current printer based on the current options + * + * @return the current printer + */ + const Printer& getPrinter() const; + + /** Get the output stream that --dump=X should print to + * + * @return the output stream + */ + std::ostream& getDumpOut() const; + + private: + SmtEngine* d_smt; +}; + +} // namespace CVC4 + +#endif // CVC4__SMT__OUTPUT_MANAGER_H diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index ea5ef2bad..c376c99ba 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -15,9 +15,10 @@ #include "smt/preprocessor.h" #include "options/smt_options.h" +#include "printer/printer.h" #include "smt/abstract_values.h" #include "smt/assertions.h" -#include "smt/command.h" +#include "smt/dump.h" #include "smt/smt_engine.h" using namespace CVC4::theory; @@ -128,7 +129,8 @@ Node Preprocessor::simplify(const Node& node, bool removeItes) Trace("smt") << "SMT simplify(" << node << ")" << endl; if (Dump.isOn("benchmark")) { - Dump("benchmark") << SimplifyCommand(node.toExpr()); + d_smt.getOutputManager().getPrinter().toStreamCmdSimplify( + d_smt.getOutputManager().getDumpOut(), node); } Node nas = d_absValues.substituteAbstractValues(node); if (options::typeChecking()) diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 33d092def..944f35593 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -27,7 +27,9 @@ #include "options/uf_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_registry.h" +#include "printer/printer.h" #include "smt/defined_function.h" +#include "smt/dump.h" #include "smt/smt_engine.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" @@ -562,7 +564,8 @@ void ProcessAssertions::dumpAssertions(const char* key, for (unsigned i = 0; i < assertionList.size(); ++i) { TNode n = assertionList[i]; - Dump("assertions") << AssertCommand(Expr(n.toExpr())); + d_smt.getOutputManager().getPrinter().toStreamCmdAssert( + d_smt.getOutputManager().getDumpOut(), n); } } } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d271ca05d..d520d664c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -71,7 +71,7 @@ #include "smt/abduction_solver.h" #include "smt/abstract_values.h" #include "smt/assertions.h" -#include "smt/command.h" +#include "smt/node_command.h" #include "smt/defined_function.h" #include "smt/dump_manager.h" #include "smt/expr_names.h" @@ -114,9 +114,19 @@ using namespace CVC4::theory; namespace CVC4 { -namespace smt { +// !!! Temporary until commands are migrated to the new API !!! +std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs) +{ + std::vector<Node> nodes; + nodes.reserve(exprs.size()); -}/* namespace CVC4::smt */ + for (Expr e : exprs) + { + nodes.push_back(Node::fromExpr(e)); + } + + return nodes; +} SmtEngine::SmtEngine(ExprManager* em, Options* optr) : d_state(new SmtEngineState(*this)), @@ -127,7 +137,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_exprNames(new ExprNames(getUserContext())), d_dumpm(new DumpManager(getUserContext())), d_routListener(new ResourceOutListener(*this)), - d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())), + d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)), d_smtSolver(nullptr), d_proofManager(nullptr), d_pfManager(nullptr), @@ -143,6 +153,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_isInternalSubsolver(false), d_statisticsRegistry(nullptr), d_stats(nullptr), + d_outMgr(this), d_resourceManager(nullptr), d_optm(nullptr), d_pp(nullptr), @@ -183,7 +194,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_smtSolver.reset( new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats)); // make the SyGuS solver - d_sygusSolver.reset(new SygusSolver(*d_smtSolver, *d_pp, getUserContext())); + d_sygusSolver.reset( + new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr)); // make the quantifier elimination solver d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver)); @@ -285,12 +297,13 @@ void SmtEngine::finishInit() { LogicInfo everything; everything.lock(); - Dump("benchmark") << CommentCommand( + getOutputManager().getPrinter().toStreamCmdComment( + getOutputManager().getDumpOut(), "CVC4 always dumps the most general, all-supported logic (below), as " "some internals might require the use of a logic more general than " - "the input.") - << SetBenchmarkLogicCommand( - everything.getLogicString()); + "the input."); + getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic( + getOutputManager().getDumpOut(), everything.getLogicString()); } // initialize the dump manager @@ -404,8 +417,8 @@ void SmtEngine::setLogic(const std::string& s) // dump out a set-logic command if (Dump.isOn("raw-benchmark")) { - Dump("raw-benchmark") - << SetBenchmarkLogicCommand(d_logic.getLogicString()); + getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic( + getOutputManager().getDumpOut(), d_logic.getLogicString()); } } catch (IllegalArgumentException& e) @@ -459,12 +472,14 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) if(Dump.isOn("benchmark")) { if(key == "status") { string s = value.getValue(); - BenchmarkStatus status = - (s == "sat") ? SMT_SATISFIABLE : - ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN); - Dump("benchmark") << SetBenchmarkStatusCommand(status); + Result::Sat status = + (s == "sat") ? Result::SAT + : ((s == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN); + getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus( + getOutputManager().getDumpOut(), status); } else { - Dump("benchmark") << SetInfoCommand(key, value); + getOutputManager().getPrinter().toStreamCmdSetInfo( + getOutputManager().getDumpOut(), key, value); } } @@ -774,16 +789,15 @@ void SmtEngine::defineFunctionsRec( if (Dump.isOn("raw-benchmark")) { - std::vector<api::Term> tFuncs = api::exprVectorToTerms(d_solver, funcs); - std::vector<std::vector<api::Term>> tFormals; + std::vector<Node> nFuncs = exprVectorToNodes(funcs); + std::vector<std::vector<Node>> nFormals; for (const std::vector<Expr>& formal : formals) { - tFormals.emplace_back(api::exprVectorToTerms(d_solver, formal)); + nFormals.emplace_back(exprVectorToNodes(formal)); } - std::vector<api::Term> tFormulas = - api::exprVectorToTerms(d_solver, formulas); - Dump("raw-benchmark") << DefineFunctionRecCommand( - d_solver, tFuncs, tFormals, tFormulas, global); + std::vector<Node> nFormulas = exprVectorToNodes(formulas); + getOutputManager().getPrinter().toStreamCmdDefineFunctionRec( + getOutputManager().getDumpOut(), nFuncs, nFormals, nFormulas); } ExprManager* em = getExprManager(); @@ -930,7 +944,11 @@ void SmtEngine::notifyPostSolvePost() Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { - Dump("benchmark") << CheckSatCommand(assumption); + if (Dump.isOn("benchmark")) + { + getOutputManager().getPrinter().toStreamCmdCheckSat( + getOutputManager().getDumpOut(), assumption); + } std::vector<Node> assump; if (!assumption.isNull()) { @@ -941,13 +959,18 @@ Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) { - if (assumptions.empty()) - { - Dump("benchmark") << CheckSatCommand(); - } - else + if (Dump.isOn("benchmark")) { - Dump("benchmark") << CheckSatAssumingCommand(assumptions); + if (assumptions.empty()) + { + getOutputManager().getPrinter().toStreamCmdCheckSat( + getOutputManager().getDumpOut()); + } + else + { + getOutputManager().getPrinter().toStreamCmdCheckSatAssuming( + getOutputManager().getDumpOut(), exprVectorToNodes(assumptions)); + } } std::vector<Node> assumps; for (const Expr& e : assumptions) @@ -959,7 +982,11 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore) { - Dump("benchmark") << QueryCommand(node, inUnsatCore); + if (Dump.isOn("benchmark")) + { + getOutputManager().getPrinter().toStreamCmdQuery( + getOutputManager().getDumpOut(), node.getNode()); + } return checkSatInternal(node.isNull() ? std::vector<Node>() : std::vector<Node>{Node::fromExpr(node)}, @@ -1045,7 +1072,8 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void) finishInit(); if (Dump.isOn("benchmark")) { - Dump("benchmark") << GetUnsatAssumptionsCommand(); + getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions( + getOutputManager().getDumpOut()); } UnsatCore core = getUnsatCoreInternal(); std::vector<Node> res; @@ -1069,7 +1097,8 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl; if (Dump.isOn("raw-benchmark")) { - Dump("raw-benchmark") << AssertCommand(formula.toExpr()); + getOutputManager().getPrinter().toStreamCmdAssert( + getOutputManager().getDumpOut(), formula); } // Substitute out any abstract values in ex @@ -1090,8 +1119,11 @@ void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type) SmtScope smts(this); finishInit(); d_sygusSolver->declareSygusVar(id, var, type); - Dump("raw-benchmark") << DeclareSygusVarCommand( - id, var.toExpr(), type.toType()); + if (Dump.isOn("raw-benchmark")) + { + getOutputManager().getPrinter().toStreamCmdDeclareVar( + getOutputManager().getDumpOut(), var, type); + } // don't need to set that the conjecture is stale } @@ -1112,22 +1144,14 @@ void SmtEngine::declareSynthFun(const std::string& id, if (Dump.isOn("raw-benchmark")) { - std::stringstream ss; - - Printer::getPrinter(options::outputLanguage()) - ->toStreamCmdSynthFun(ss, - id, - vars, - func.getType().isFunction() - ? func.getType().getRangeType() - : func.getType(), - isInv, - sygusType); - - // must print it on the standard output channel since it is not possible - // to print anything except for commands with Dump. - std::ostream& out = *d_options.getOut(); - out << ss.str() << std::endl; + getOutputManager().getPrinter().toStreamCmdSynthFun( + getOutputManager().getDumpOut(), + id, + vars, + func.getType().isFunction() ? func.getType().getRangeType() + : func.getType(), + isInv, + sygusType); } } @@ -1136,7 +1160,11 @@ void SmtEngine::assertSygusConstraint(Node constraint) SmtScope smts(this); finishInit(); d_sygusSolver->assertSygusConstraint(constraint); - Dump("raw-benchmark") << SygusConstraintCommand(constraint.toExpr()); + if (Dump.isOn("raw-benchmark")) + { + getOutputManager().getPrinter().toStreamCmdConstraint( + getOutputManager().getDumpOut(), constraint); + } } void SmtEngine::assertSygusInvConstraint(Node inv, @@ -1147,8 +1175,11 @@ void SmtEngine::assertSygusInvConstraint(Node inv, SmtScope smts(this); finishInit(); d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); - Dump("raw-benchmark") << SygusInvConstraintCommand( - inv.toExpr(), pre.toExpr(), trans.toExpr(), post.toExpr()); + if (Dump.isOn("raw-benchmark")) + { + getOutputManager().getPrinter().toStreamCmdInvConstraint( + getOutputManager().getDumpOut(), inv, pre, trans, post); + } } Result SmtEngine::checkSynth() @@ -1192,7 +1223,7 @@ Node SmtEngine::getValue(const Node& ex) const Trace("smt") << "SMT getValue(" << ex << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetValueCommand(ex.toExpr()); + d_outMgr.getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex}); } TypeNode expectedType = ex.getType(); @@ -1290,7 +1321,8 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment() SmtScope smts(this); finishInit(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetAssignmentCommand(); + getOutputManager().getPrinter().toStreamCmdGetAssignment( + getOutputManager().getDumpOut()); } if(!options::produceAssignments()) { const char* msg = @@ -1351,7 +1383,8 @@ Model* SmtEngine::getModel() { finishInit(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetModelCommand(); + getOutputManager().getPrinter().toStreamCmdGetModel( + getOutputManager().getDumpOut()); } TheoryModel* m = getAvailableModel("get model"); @@ -1384,7 +1417,8 @@ Result SmtEngine::blockModel() if (Dump.isOn("benchmark")) { - Dump("benchmark") << BlockModelCommand(); + getOutputManager().getPrinter().toStreamCmdBlockModel( + getOutputManager().getDumpOut()); } TheoryModel* m = getAvailableModel("block model"); @@ -1415,7 +1449,8 @@ Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs) "block model values must be called on non-empty set of terms"); if (Dump.isOn("benchmark")) { - Dump("benchmark") << BlockModelValuesCommand(exprs); + getOutputManager().getPrinter().toStreamCmdBlockModelValues( + getOutputManager().getDumpOut(), exprVectorToNodes(exprs)); } TheoryModel* m = getAvailableModel("block model values"); @@ -1573,7 +1608,8 @@ void SmtEngine::checkModel(bool hardFailure) { SubstitutionMap substitutions(&fakeContext, /* substituteUnderQuantifiers = */ false); for(size_t k = 0; k < m->getNumCommands(); ++k) { - const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k)); + const DeclareFunctionNodeCommand* c = + dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k)); Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl; if(c == NULL) { // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ... @@ -1584,7 +1620,7 @@ void SmtEngine::checkModel(bool hardFailure) { // We'll first do some checks, then add to our substitution map // the mapping: function symbol |-> value - Expr func = c->getFunction(); + Expr func = c->getFunction().toExpr(); Node val = m->getValue(func); Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl; @@ -1767,7 +1803,8 @@ UnsatCore SmtEngine::getUnsatCore() { SmtScope smts(this); finishInit(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetUnsatCoreCommand(); + getOutputManager().getPrinter().toStreamCmdGetUnsatCore( + getOutputManager().getDumpOut()); } return getUnsatCoreInternal(); } @@ -1896,7 +1933,8 @@ std::vector<Expr> SmtEngine::getAssertions() finishInit(); d_state->doPendingPops(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetAssertionsCommand(); + getOutputManager().getPrinter().toStreamCmdGetAssertions( + getOutputManager().getDumpOut()); } Trace("smt") << "SMT getAssertions()" << endl; if(!options::produceAssertions()) { @@ -1923,7 +1961,8 @@ void SmtEngine::push() Trace("smt") << "SMT push()" << endl; d_smtSolver->processAssertions(*d_asserts); if(Dump.isOn("benchmark")) { - Dump("benchmark") << PushCommand(); + getOutputManager().getPrinter().toStreamCmdPush( + getOutputManager().getDumpOut()); } d_state->userPush(); } @@ -1933,7 +1972,8 @@ void SmtEngine::pop() { finishInit(); Trace("smt") << "SMT pop()" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << PopCommand(); + getOutputManager().getPrinter().toStreamCmdPop( + getOutputManager().getDumpOut()); } d_state->userPop(); @@ -1954,7 +1994,8 @@ void SmtEngine::reset() ExprManager *em = d_exprManager; Trace("smt") << "SMT reset()" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << ResetCommand(); + getOutputManager().getPrinter().toStreamCmdReset( + getOutputManager().getDumpOut()); } std::string filename = d_state->getFilename(); Options opts; @@ -1983,7 +2024,8 @@ void SmtEngine::resetAssertions() Trace("smt") << "SMT resetAssertions()" << endl; if (Dump.isOn("benchmark")) { - Dump("benchmark") << ResetAssertionsCommand(); + getOutputManager().getPrinter().toStreamCmdResetAssertions( + getOutputManager().getDumpOut()); } d_state->notifyResetAssertions(); @@ -2073,7 +2115,8 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetOptionCommand(key, value); + getOutputManager().getPrinter().toStreamCmdSetOption( + getOutputManager().getDumpOut(), key, value); } if(key == "command-verbosity") { @@ -2126,7 +2169,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const } if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetOptionCommand(key); + d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key); } if(key == "command-verbosity") { @@ -2181,4 +2224,11 @@ ResourceManager* SmtEngine::getResourceManager() DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); } +const Printer* SmtEngine::getPrinter() const +{ + return Printer::getPrinter(d_options[options::outputLanguage]); +} + +OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index eec17a5f8..d855e3181 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -31,6 +31,7 @@ #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" +#include "smt/output_manager.h" #include "smt/smt_mode.h" #include "theory/logic_info.h" #include "util/hash.h" @@ -63,6 +64,8 @@ class Model; class LogicRequest; class StatisticsRegistry; +class Printer; + /* -------------------------------------------------------------------------- */ namespace api { @@ -130,6 +133,8 @@ namespace theory { class Rewriter; }/* CVC4::theory namespace */ +std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs); + // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass // SmtEngine and override check()? @@ -862,6 +867,12 @@ class CVC4_PUBLIC SmtEngine /** Permit access to the underlying dump manager. */ smt::DumpManager* getDumpManager(); + /** Get the printer used by this SMT engine */ + const Printer* getPrinter() const; + + /** Get the output manager for this SMT engine */ + OutputManager& getOutputManager(); + /** Get a pointer to the Rewriter owned by this SmtEngine. */ theory::Rewriter* getRewriter() { return d_rewriter.get(); } @@ -1139,6 +1150,10 @@ class CVC4_PUBLIC SmtEngine /** The options object */ Options d_options; + + /** the output manager for commands */ + mutable OutputManager d_outMgr; + /** * Manager for limiting time and abstract resource usage. */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c64689be6..922831106 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -51,7 +51,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) d_smt.getUserContext(), d_rm, d_pp.getTermFormulaRemover(), - logicInfo)); + logicInfo, + d_smt.getOutputManager())); // Add the theories for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; @@ -65,8 +66,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + d_propEngine.reset(new PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager())); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -82,8 +86,11 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + d_propEngine.reset(new PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager())); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 0fc63d198..979eaec6d 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -17,6 +17,8 @@ #include "expr/dtype.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "printer/printer.h" +#include "smt/dump.h" #include "smt/preprocessor.h" #include "smt/smt_solver.h" #include "theory/smt_engine_subsolver.h" @@ -30,8 +32,12 @@ namespace smt { SygusSolver::SygusSolver(SmtSolver& sms, Preprocessor& pp, - context::UserContext* u) - : d_smtSolver(sms), d_pp(pp), d_sygusConjectureStale(u, true) + context::UserContext* u, + OutputManager& outMgr) + : d_smtSolver(sms), + d_pp(pp), + d_sygusConjectureStale(u, true), + d_outMgr(outMgr) { } @@ -205,7 +211,10 @@ Result SygusSolver::checkSynth(Assertions& as) te->setUserAttribute("sygus", sygusVar, {}, ""); Trace("smt") << "Check synthesis conjecture: " << body << std::endl; - Dump("raw-benchmark") << CheckSynthCommand(); + if (Dump.isOn("raw-benchmark")) + { + d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut()); + } d_sygusConjectureStale = false; diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 621bea9f3..deb253142 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -24,6 +24,9 @@ #include "util/result.h" namespace CVC4 { + +class OutputManager; + namespace smt { class Preprocessor; @@ -41,7 +44,10 @@ class SmtSolver; class SygusSolver { public: - SygusSolver(SmtSolver& sms, Preprocessor& pp, context::UserContext* u); + SygusSolver(SmtSolver& sms, + Preprocessor& pp, + context::UserContext* u, + OutputManager& outMgr); ~SygusSolver(); /** @@ -174,6 +180,8 @@ class SygusSolver * Whether we need to reconstruct the sygus conjecture. */ context::CDO<bool> d_sygusConjectureStale; + /** Reference to the output manager of the smt engine */ + OutputManager& d_outMgr; }; } // namespace smt diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 85f0c30d7..00bf74360 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -27,7 +27,6 @@ #include "expr/node.h" #include "expr/term_context_stack.h" #include "expr/term_conversion_proof_generator.h" -#include "smt/dump.h" #include "theory/eager_proof_generator.h" #include "theory/trust_node.h" #include "util/bool.h" |