summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/command.cpp16
-rw-r--r--src/smt/dump.cpp100
-rw-r--r--src/smt/dump.h22
-rw-r--r--src/smt/dump_manager.cpp12
-rw-r--r--src/smt/dump_manager.h4
-rw-r--r--src/smt/listeners.cpp12
-rw-r--r--src/smt/listeners.h5
-rw-r--r--src/smt/output_manager.cpp35
-rw-r--r--src/smt/output_manager.h57
-rw-r--r--src/smt/preprocessor.cpp6
-rw-r--r--src/smt/process_assertions.cpp5
-rw-r--r--src/smt/smt_engine.cpp188
-rw-r--r--src/smt/smt_engine.h15
-rw-r--r--src/smt/smt_solver.cpp17
-rw-r--r--src/smt/sygus_solver.cpp15
-rw-r--r--src/smt/sygus_solver.h10
-rw-r--r--src/smt/term_formula_removal.h1
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback