This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
smt/node_command.h
smt/options_manager.cpp
smt/options_manager.h
+ smt/output_manager.cpp
+ smt/output_manager.h
smt/quant_elim_solver.cpp
smt/quant_elim_solver.h
smt/preprocessor.cpp
#include "api/cvc4cpp.h"
#include "expr/expr_manager.h"
#include "options/options.h"
-#include "smt/command.h"
#include "smt/smt_engine.h"
#include "util/statistics_registry.h"
namespace CVC4 {
+class Command;
+
namespace api {
class Solver;
}
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/parser_exception.h"
-#include "smt/command.h"
#include "smt/smt_engine.h"
#include "util/result.h"
#include "util/statistics.h"
#include "parser/smt2/smt2_input.h"
#include "parser/smt2/sygus_input.h"
#include "parser/tptp/tptp_input.h"
-#include "smt/command.h"
using namespace std;
using namespace CVC4;
**/
#include "parser/cvc/cvc.h"
+#include "smt/command.h"
namespace CVC4 {
namespace parser {
#include "api/cvc4cpp.h"
#include "parser/parser.h"
-#include "smt/command.h"
namespace CVC4 {
#include "expr/type.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
-#include "smt/command.h"
using namespace std;
#include "api/cvc4cpp.h"
#include "parser/parse_op.h"
#include "parser/parser.h"
-#include "smt/command.h"
#include "theory/logic_info.h"
#include "util/abstract_value.h"
namespace CVC4 {
+class Command;
class SExpr;
namespace api {
#include "expr/type.h"
#include "options/options.h"
#include "parser/parser.h"
+#include "smt/command.h"
// ANTLR defines these, which is really bad!
#undef true
#include "api/cvc4cpp.h"
#include "parser/parse_op.h"
#include "parser/parser.h"
-#include "smt/command.h"
#include "util/hash.h"
namespace CVC4 {
+class Command;
+
namespace api {
class Solver;
}
#include "smt/dump.h"
#include "smt/smt_statistics_registry.h"
+#include "printer/printer.h"
namespace CVC4 {
namespace preprocessing {
if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
{
// Push the simplified assertions to the dump output stream
- for (const auto& n : assertionList) {
- Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+ OutputManager& outMgr = d_preprocContext->getSmt()->getOutputManager();
+ const Printer& printer = outMgr.getPrinter();
+ std::ostream& out = outMgr.getDumpOut();
+
+ for (const auto& n : assertionList)
+ {
+ printer.toStreamCmdAssert(out, n);
}
}
}
void AstPrinter::toStreamCmdEmpty(std::ostream& out,
const std::string& name) const
{
- out << "EmptyCommand(" << name << ')';
+ out << "EmptyCommand(" << name << ')' << std::endl;
}
void AstPrinter::toStreamCmdEcho(std::ostream& out,
const std::string& output) const
{
- out << "EchoCommand(" << output << ')';
+ out << "EchoCommand(" << output << ')' << std::endl;
}
void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "Assert(" << n << ')';
+ out << "Assert(" << n << ')' << std::endl;
}
-void AstPrinter::toStreamCmdPush(std::ostream& out) const { out << "Push()"; }
+void AstPrinter::toStreamCmdPush(std::ostream& out) const
+{
+ out << "Push()" << std::endl;
+}
-void AstPrinter::toStreamCmdPop(std::ostream& out) const { out << "Pop()"; }
+void AstPrinter::toStreamCmdPop(std::ostream& out) const {
+ out << "Pop()" << std::endl;
+}
void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
{
out << "CheckSat(" << n << ')';
}
+ out << std::endl;
}
void AstPrinter::toStreamCmdCheckSatAssuming(
{
out << "CheckSatAssuming( << ";
copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
- out << ">> )";
+ out << ">> )" << std::endl;
}
void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
{
- out << "Query(" << n << ')';
+ out << "Query(" << n << ')' << std::endl;
}
-void AstPrinter::toStreamCmdReset(std::ostream& out) const { out << "Reset()"; }
+void AstPrinter::toStreamCmdReset(std::ostream& out) const
+{
+ out << "Reset()" << std::endl;
+}
void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
{
- out << "ResetAssertions()";
+ out << "ResetAssertions()" << std::endl;
}
-void AstPrinter::toStreamCmdQuit(std::ostream& out) const { out << "Quit()"; }
+void AstPrinter::toStreamCmdQuit(std::ostream& out) const
+{
+ out << "Quit()" << std::endl;
+}
void AstPrinter::toStreamCmdDeclarationSequence(
std::ostream& out, const std::vector<Command*>& sequence) const
{
out << *i << endl;
}
- out << "]";
+ out << "]" << std::endl;
}
void AstPrinter::toStreamCmdCommandSequence(
{
out << *i << endl;
}
- out << "]";
+ out << "]" << std::endl;
}
void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
const std::string& id,
TypeNode type) const
{
- out << "Declare(" << id << "," << type << ')';
+ out << "Declare(" << id << "," << type << ')' << std::endl;
}
void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
out << formals.back();
}
- out << "], << " << formula << " >> )";
+ out << "], << " << formula << " >> )" << std::endl;
}
void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
size_t arity,
TypeNode type) const
{
- out << "DeclareType(" << id << "," << arity << "," << type << ')';
+ out << "DeclareType(" << id << "," << arity << "," << type << ')'
+ << std::endl;
}
void AstPrinter::toStreamCmdDefineType(std::ostream& out,
ostream_iterator<TypeNode>(out, ", "));
out << params.back();
}
- out << "]," << t << ')';
+ out << "]," << t << ')' << std::endl;
}
void AstPrinter::toStreamCmdDefineNamedFunction(
void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "Simplify( << " << n << " >> )";
+ out << "Simplify( << " << n << " >> )" << std::endl;
}
void AstPrinter::toStreamCmdGetValue(std::ostream& out,
{
out << "GetValue( << ";
copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
- out << ">> )";
+ out << ">> )" << std::endl;
}
void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
{
- out << "GetModel()";
+ out << "GetModel()" << std::endl;
}
void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
{
- out << "GetAssignment()";
+ out << "GetAssignment()" << std::endl;
}
void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
{
- out << "GetAssertions()";
+ out << "GetAssertions()" << std::endl;
}
void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
{
- out << "GetProof()";
+ out << "GetProof()" << std::endl;
}
void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
{
- out << "GetUnsatCore()";
+ out << "GetUnsatCore()" << std::endl;
}
void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
Result::Sat status) const
{
- out << "SetBenchmarkStatus(" << status << ')';
+ out << "SetBenchmarkStatus(" << status << ')' << std::endl;
}
void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
const std::string& logic) const
{
- out << "SetBenchmarkLogic(" << logic << ')';
+ out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
}
void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
const std::string& flag,
SExpr sexpr) const
{
- out << "SetInfo(" << flag << ", " << sexpr << ')';
+ out << "SetInfo(" << flag << ", " << sexpr << ')' << std::endl;
}
void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
const std::string& flag) const
{
- out << "GetInfo(" << flag << ')';
+ out << "GetInfo(" << flag << ')' << std::endl;
}
void AstPrinter::toStreamCmdSetOption(std::ostream& out,
const std::string& flag,
SExpr sexpr) const
{
- out << "SetOption(" << flag << ", " << sexpr << ')';
+ out << "SetOption(" << flag << ", " << sexpr << ')' << std::endl;
}
void AstPrinter::toStreamCmdGetOption(std::ostream& out,
const std::string& flag) const
{
- out << "GetOption(" << flag << ')';
+ out << "GetOption(" << flag << ')' << std::endl;
}
void AstPrinter::toStreamCmdDatatypeDeclaration(
{
out << t << ";" << endl;
}
- out << "])";
+ out << "])" << std::endl;
}
void AstPrinter::toStreamCmdComment(std::ostream& out,
const std::string& comment) const
{
- out << "CommentCommand([" << comment << "])";
+ out << "CommentCommand([" << comment << "])" << std::endl;
}
template <class T>
void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "ASSERT " << n << ';';
+ out << "ASSERT " << n << ';' << std::endl;
}
-void CvcPrinter::toStreamCmdPush(std::ostream& out) const { out << "PUSH;"; }
+void CvcPrinter::toStreamCmdPush(std::ostream& out) const
+{
+ out << "PUSH;" << std::endl;
+}
-void CvcPrinter::toStreamCmdPop(std::ostream& out) const { out << "POP;"; }
+void CvcPrinter::toStreamCmdPop(std::ostream& out) const
+{
+ out << "POP;" << std::endl;
+}
void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
{
out << " POP;";
}
+ out << std::endl;
}
void CvcPrinter::toStreamCmdCheckSatAssuming(
{
out << " POP;";
}
+ out << std::endl;
}
void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
{
out << " POP;";
}
+ out << std::endl;
}
-void CvcPrinter::toStreamCmdReset(std::ostream& out) const { out << "RESET;"; }
+void CvcPrinter::toStreamCmdReset(std::ostream& out) const
+{
+ out << "RESET;" << std::endl;
+}
void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const
{
- out << "RESET ASSERTIONS;";
+ out << "RESET ASSERTIONS;" << std::endl;
}
void CvcPrinter::toStreamCmdQuit(std::ostream& out) const
{
- // out << "EXIT;";
+ // out << "EXIT;" << std::endl;
}
void CvcPrinter::toStreamCmdCommandSequence(
i != sequence.cend();
++i)
{
- out << *i << endl;
+ out << *i;
}
}
break;
}
}
+ out << std::endl;
}
void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out,
const std::string& id,
TypeNode type) const
{
- out << id << " : " << type << ';';
+ out << id << " : " << type << ';' << std::endl;
}
void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out,
}
out << "): ";
}
- out << formula << ';';
+ out << formula << ';' << std::endl;
}
void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
}
else
{
- out << id << " : TYPE;";
+ out << id << " : TYPE;" << std::endl;
}
}
}
else
{
- out << id << " : TYPE = " << t << ';';
+ out << id << " : TYPE = " << t << ';' << std::endl;
}
}
void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "TRANSFORM " << n << ';';
+ out << "TRANSFORM " << n << ';' << std::endl;
}
void CvcPrinter::toStreamCmdGetValue(std::ostream& out,
copy(nodes.begin(),
nodes.end() - 1,
ostream_iterator<Node>(out, ";\nGET_VALUE "));
- out << nodes.back() << ';';
+ out << nodes.back() << ';' << std::endl;
}
void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const
{
- out << "COUNTERMODEL;";
+ out << "COUNTERMODEL;" << std::endl;
}
void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const
{
- out << "% (get-assignment)";
+ out << "% (get-assignment)" << std::endl;
}
void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const
{
- out << "WHERE;";
+ out << "WHERE;" << std::endl;
}
void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const
{
- out << "DUMP_PROOF;";
+ out << "DUMP_PROOF;" << std::endl;
}
void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
{
- out << "DUMP_UNSAT_CORE;";
+ out << "DUMP_UNSAT_CORE;" << std::endl;
}
void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
Result::Sat status) const
{
- out << "% (set-info :status " << status << ')';
+ out << "% (set-info :status " << status << ')' << std::endl;
}
void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
const std::string& logic) const
{
- out << "OPTION \"logic\" \"" << logic << "\";";
+ out << "OPTION \"logic\" \"" << logic << "\";" << std::endl;
}
void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
OutputLanguage language =
d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
SExpr::toStream(out, sexpr, language);
- out << ')';
+ out << ')' << std::endl;
}
void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
const std::string& flag) const
{
- out << "% (get-info " << flag << ')';
+ out << "% (get-info " << flag << ')' << std::endl;
}
void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
{
out << "OPTION \"" << flag << "\" ";
SExpr::toStream(out, sexpr, language::output::LANG_CVC4);
- out << ';';
+ out << ';' << std::endl;
}
void CvcPrinter::toStreamCmdGetOption(std::ostream& out,
const std::string& flag) const
{
- out << "% (get-option " << flag << ')';
+ out << "% (get-option " << flag << ')' << std::endl;
}
void CvcPrinter::toStreamCmdDatatypeDeclaration(
}
firstDatatype = false;
}
- out << endl << "END;";
+ out << endl << "END;" << std::endl;
}
}
void CvcPrinter::toStreamCmdComment(std::ostream& out,
const std::string& comment) const
{
- out << "% " << comment;
+ out << "% " << comment << std::endl;
}
void CvcPrinter::toStreamCmdEmpty(std::ostream& out,
const std::string& name) const
{
+ out << std::endl;
}
void CvcPrinter::toStreamCmdEcho(std::ostream& out,
const std::string& output) const
{
- out << "ECHO \"" << output << "\";";
+ out << "ECHO \"" << output << "\";" << std::endl;
}
template <class T>
void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "(assert " << n << ')';
+ out << "(assert " << n << ')' << std::endl;
}
void Smt2Printer::toStreamCmdPush(std::ostream& out) const
{
- out << "(push 1)";
+ out << "(push 1)" << std::endl;
}
-void Smt2Printer::toStreamCmdPop(std::ostream& out) const { out << "(pop 1)"; }
+void Smt2Printer::toStreamCmdPop(std::ostream& out) const
+{
+ out << "(pop 1)" << std::endl;
+}
void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
{
out << "(check-sat)";
}
+ out << std::endl;
}
void Smt2Printer::toStreamCmdCheckSatAssuming(
{
out << "(check-sat-assuming ( ";
copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
- out << "))";
+ out << "))" << std::endl;
}
void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
void Smt2Printer::toStreamCmdReset(std::ostream& out) const
{
- out << "(reset)";
+ out << "(reset)" << std::endl;
}
void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
{
- out << "(reset-assertions)";
+ out << "(reset-assertions)" << std::endl;
}
-void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; }
+void Smt2Printer::toStreamCmdQuit(std::ostream& out) const
+{
+ out << "(exit)" << std::endl;
+}
void Smt2Printer::toStreamCmdCommandSequence(
std::ostream& out, const std::vector<Command*>& sequence) const
{
- CommandSequence::const_iterator i = sequence.cbegin();
- if (i != sequence.cend())
+ for (Command* i : sequence)
{
- for (;;)
- {
- out << *i;
- if (++i != sequence.cend())
- {
- out << endl;
- }
- else
- {
- break;
- }
- }
+ out << *i;
}
}
type = type.getRangeType();
}
- out << ") " << type << ')';
+ out << ") " << type << ')' << std::endl;
}
void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
}
}
}
- out << ") " << range << ' ' << formula << ')';
+ out << ") " << range << ' ' << formula << ')' << std::endl;
}
void Smt2Printer::toStreamCmdDefineFunctionRec(
{
out << ")";
}
- out << ")";
+ out << ")" << std::endl;
}
static void toStreamRational(std::ostream& out,
size_t arity,
TypeNode type) const
{
- out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")";
+ out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")"
+ << std::endl;
}
void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
out << params.back();
}
- out << ") " << t << ")";
+ out << ") " << t << ")" << std::endl;
}
void Smt2Printer::toStreamCmdDefineNamedFunction(
void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "(simplify " << n << ')';
+ out << "(simplify " << n << ')' << std::endl;
}
void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
{
out << "(get-value ( ";
copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
- out << "))";
+ out << "))" << std::endl;
}
void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
{
- out << "(get-model)";
+ out << "(get-model)" << std::endl;
}
void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
{
- out << "(get-assignment)";
+ out << "(get-assignment)" << std::endl;
}
void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
{
- out << "(get-assertions)";
+ out << "(get-assertions)" << std::endl;
}
void Smt2Printer::toStreamCmdGetProof(std::ostream& out) const
{
- out << "(get-proof)";
+ out << "(get-proof)" << std::endl;
}
void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
{
- out << "(get-unsat-assumptions)";
+ out << "(get-unsat-assumptions)" << std::endl;
}
void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
{
- out << "(get-unsat-core)";
+ out << "(get-unsat-core)" << std::endl;
}
void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
Result::Sat status) const
{
- out << "(set-info :status " << status << ')';
+ out << "(set-info :status " << status << ')' << std::endl;
}
void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
const std::string& logic) const
{
- out << "(set-logic " << logic << ')';
+ out << "(set-logic " << logic << ')' << std::endl;
}
void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
{
out << "(set-info :" << flag << ' ';
SExpr::toStream(out, sexpr, variantToLanguage(d_variant));
- out << ')';
+ out << ')' << std::endl;
}
void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
const std::string& flag) const
{
- out << "(get-info :" << flag << ')';
+ out << "(get-info :" << flag << ')' << std::endl;
}
void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
{
out << "(set-option :" << flag << ' ';
SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5);
- out << ')';
+ out << ')' << std::endl;
}
void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
const std::string& flag) const
{
- out << "(get-option :" << flag << ')';
+ out << "(get-option :" << flag << ')' << std::endl;
}
void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
}
out << ")";
}
- out << ")" << endl;
+ out << ")" << std::endl;
}
void Smt2Printer::toStreamCmdComment(std::ostream& out,
s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
- out << "(set-info :notes \"" << s << "\")";
+ out << "(set-info :notes \"" << s << "\")" << std::endl;
}
void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
const std::string& name) const
{
+ out << std::endl;
}
void Smt2Printer::toStreamCmdEcho(std::ostream& out,
s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
- out << "(echo \"" << s << "\")";
+ out << "(echo \"" << s << "\")" << std::endl;
}
/*
{
toStreamSygusGrammar(out, sygusType);
}
- out << ')';
+ out << ')' << std::endl;
}
void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
Node var,
TypeNode type) const
{
- out << "(declare-var " << var << ' ' << type << ')';
+ out << "(declare-var " << var << ' ' << type << ')' << std::endl;
}
void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
{
- out << "(constraint " << n << ')';
+ out << "(constraint " << n << ')' << std::endl;
}
void Smt2Printer::toStreamCmdInvConstraint(
std::ostream& out, Node inv, Node pre, Node trans, Node post) const
{
out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
- << ')';
+ << ')' << std::endl;
}
void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
{
- out << "(check-synth)";
+ out << "(check-synth)" << std::endl;
}
void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
{
toStreamSygusGrammar(out, sygusType);
}
- out << ')';
+ out << ')' << std::endl;
}
/*
#include "expr/expr_iomanip.h"
#include "options/base_options.h"
#include "printer/printer.h"
-#include "smt/command.h"
#include "smt/smt_engine_scope.h"
namespace CVC4 {
#include "prop/minisat/minisat.h"
#include "prop/prop_engine.h"
#include "prop/theory_proxy.h"
-#include "smt/command.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "printer/printer.h"
#include "smt/smt_engine_scope.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
namespace CVC4 {
namespace prop {
-CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
- context::Context* context, bool fullLitToNodeMap,
+CnfStream::CnfStream(SatSolver* satSolver,
+ Registrar* registrar,
+ context::Context* context,
+ OutputManager* outMgr,
+ bool fullLitToNodeMap,
std::string name)
: d_satSolver(satSolver),
+ d_outMgr(outMgr),
d_booleanVariables(context),
d_nodeToLiteralMap(context),
d_literalToNodeMap(context),
d_registrar(registrar),
d_name(name),
d_cnfProof(NULL),
- d_removable(false) {
+ d_removable(false)
+{
}
TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver,
Registrar* registrar,
context::Context* context,
+ OutputManager* outMgr,
ResourceManager* rm,
bool fullLitToNodeMap,
std::string name)
- : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name),
+ : CnfStream(satSolver, registrar, context, outMgr, fullLitToNodeMap, name),
d_resourceManager(rm)
{}
void CnfStream::assertClause(TNode node, SatClause& c) {
Debug("cnf") << "Inserting into stream " << c << " node = " << node << endl;
- if(Dump.isOn("clauses")) {
- if(c.size() == 1) {
- Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
- } else {
+ if (Dump.isOn("clauses") && d_outMgr != nullptr)
+ {
+ const Printer& printer = d_outMgr->getPrinter();
+ std::ostream& out = d_outMgr->getDumpOut();
+ if (c.size() == 1)
+ {
+ printer.toStreamCmdAssert(out, getNode(c[0]));
+ }
+ else
+ {
Assert(c.size() > 1);
NodeBuilder<> b(kind::OR);
- for(unsigned i = 0; i < c.size(); ++i) {
+ for (unsigned i = 0; i < c.size(); ++i)
+ {
b << getNode(c[i]);
}
Node n = b;
- Dump("clauses") << AssertCommand(Expr(n.toExpr()));
+ printer.toStreamCmdAssert(out, n);
}
}
namespace CVC4 {
+class OutputManager;
+
namespace prop {
class PropEngine;
/** The SAT solver we will be using */
SatSolver* d_satSolver;
+ /** Reference to the output manager of the smt engine */
+ OutputManager* d_outMgr;
+
/** Boolean variables that we translated */
context::CDList<TNode> d_booleanVariables;
* @param satSolver the sat solver to use.
* @param registrar the entity that takes care of preregistration of Nodes.
* @param context the context that the CNF should respect.
+ * @param outMgr Reference to the output manager of the smt engine. Assertions
+ * will not be dumped if outMgr == nullptr.
* @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
* @param name string identifier to distinguish between different instances
* even for non-theory literals.
*/
- CnfStream(SatSolver* satSolver, Registrar* registrar,
- context::Context* context, bool fullLitToNodeMap = false,
+ CnfStream(SatSolver* satSolver,
+ Registrar* registrar,
+ context::Context* context,
+ OutputManager* outMgr = nullptr,
+ bool fullLitToNodeMap = false,
std::string name = "");
/**
* @param satSolver the sat solver to use
* @param registrar the entity that takes care of pre-registration of Nodes
* @param context the context that the CNF should respect.
+ * @param outMgr reference to the output manager of the smt engine. Assertions
+ * will not be dumped if outMgr == nullptr.
* @param rm the resource manager of the CNF stream
* @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
* even for non-theory literals
TseitinCnfStream(SatSolver* satSolver,
Registrar* registrar,
context::Context* context,
+ OutputManager* outMgr,
ResourceManager* rm,
bool fullLitToNodeMap = false,
std::string name = "");
// Pop the SMT context
for (int l = trail_lim.size() - level; l > 0; --l) {
d_context->pop();
- if(Dump.isOn("state")) {
- d_proxy->dumpStatePop();
- }
}
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
trail_lim.push(trail.size());
flipped.push(false);
d_context->push();
- if (Dump.isOn("state"))
- {
- Dump("state") << CVC4::PushCommand();
- }
}
inline int Solver::decisionLevel () const { return trail_lim.size(); }
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
#include "prop/theory_proxy.h"
-#include "smt/command.h"
#include "smt/smt_statistics_registry.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
PropEngine::PropEngine(TheoryEngine* te,
Context* satContext,
UserContext* userContext,
- ResourceManager* rm)
+ ResourceManager* rm,
+ OutputManager& outMgr)
: d_inCheckSat(false),
d_theoryEngine(te),
d_context(satContext),
d_registrar(NULL),
d_cnfStream(NULL),
d_interrupted(false),
- d_resourceManager(rm)
+ d_resourceManager(rm),
+ d_outMgr(outMgr)
{
Debug("prop") << "Constructing the PropEngine" << endl;
d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::TseitinCnfStream(
- d_satSolver, d_registrar, userContext, rm, true);
+ d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
d_theoryProxy = new TheoryProxy(
this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
class ResourceManager;
class DecisionEngine;
+class OutputManager;
class TheoryEngine;
namespace theory {
PropEngine(TheoryEngine*,
context::Context* satContext,
context::UserContext* userContext,
- ResourceManager* rm);
+ ResourceManager* rm,
+ OutputManager& outMgr);
/**
* Destructor.
/** Pointer to resource manager for associated SmtEngine */
ResourceManager* d_resourceManager;
+ /** Reference to the output manager of the smt engine */
+ OutputManager& d_outMgr;
};
} // namespace prop
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "proof/cnf_proof.h"
-#include "smt/command.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
return d_decisionEngine->getPolarity(var);
}
-void TheoryProxy::dumpStatePop() {
- if(Dump.isOn("state")) {
- Dump("state") << PopCommand();
- }
-}
-
}/* CVC4::prop namespace */
}/* CVC4 namespace */
SatValue getDecisionPolarity(SatVariable var);
- /** Shorthand for Dump("state") << PopCommand() */
- void dumpStatePop();
-
private:
/** The prop engine we are using. */
PropEngine* d_propEngine;
}
}
-// !!! 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)
{
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;
#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) {
|| !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(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: `")
+ 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\
#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
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;
#include "expr/expr_manager.h"
#include "options/smt_options.h"
#include "smt/dump.h"
+#include "smt/node_command.h"
namespace CVC4 {
namespace smt {
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);
}
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);
#include "context/cdlist.h"
#include "expr/node.h"
-#include "smt/node_command.h"
namespace CVC4 {
+
+class NodeCommand;
+
namespace smt {
/**
#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"
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)
{
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)
{
namespace CVC4 {
+class OutputManager;
class SmtEngine;
namespace smt {
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 */
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
#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;
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())
#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"
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);
}
}
}
#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"
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)),
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),
d_isInternalSubsolver(false),
d_statisticsRegistry(nullptr),
d_stats(nullptr),
+ d_outMgr(this),
d_resourceManager(nullptr),
d_optm(nullptr),
d_pp(nullptr),
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));
{
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
// 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)
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);
}
}
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();
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())
{
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)
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)},
finishInit();
if (Dump.isOn("benchmark"))
{
- Dump("benchmark") << GetUnsatAssumptionsCommand();
+ getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions(
+ getOutputManager().getDumpOut());
}
UnsatCore core = getUnsatCoreInternal();
std::vector<Node> res;
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
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
}
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);
}
}
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,
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()
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();
SmtScope smts(this);
finishInit();
if(Dump.isOn("benchmark")) {
- Dump("benchmark") << GetAssignmentCommand();
+ getOutputManager().getPrinter().toStreamCmdGetAssignment(
+ getOutputManager().getDumpOut());
}
if(!options::produceAssignments()) {
const char* msg =
finishInit();
if(Dump.isOn("benchmark")) {
- Dump("benchmark") << GetModelCommand();
+ getOutputManager().getPrinter().toStreamCmdGetModel(
+ getOutputManager().getDumpOut());
}
TheoryModel* m = getAvailableModel("get model");
if (Dump.isOn("benchmark"))
{
- Dump("benchmark") << BlockModelCommand();
+ getOutputManager().getPrinter().toStreamCmdBlockModel(
+ getOutputManager().getDumpOut());
}
TheoryModel* m = getAvailableModel("block model");
"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");
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, ...
// 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;
SmtScope smts(this);
finishInit();
if(Dump.isOn("benchmark")) {
- Dump("benchmark") << GetUnsatCoreCommand();
+ getOutputManager().getPrinter().toStreamCmdGetUnsatCore(
+ getOutputManager().getDumpOut());
}
return getUnsatCoreInternal();
}
finishInit();
d_state->doPendingPops();
if(Dump.isOn("benchmark")) {
- Dump("benchmark") << GetAssertionsCommand();
+ getOutputManager().getPrinter().toStreamCmdGetAssertions(
+ getOutputManager().getDumpOut());
}
Trace("smt") << "SMT getAssertions()" << endl;
if(!options::produceAssertions()) {
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();
}
finishInit();
Trace("smt") << "SMT pop()" << endl;
if(Dump.isOn("benchmark")) {
- Dump("benchmark") << PopCommand();
+ getOutputManager().getPrinter().toStreamCmdPop(
+ getOutputManager().getDumpOut());
}
d_state->userPop();
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;
Trace("smt") << "SMT resetAssertions()" << endl;
if (Dump.isOn("benchmark"))
{
- Dump("benchmark") << ResetAssertionsCommand();
+ getOutputManager().getPrinter().toStreamCmdResetAssertions(
+ getOutputManager().getDumpOut());
}
d_state->notifyResetAssertions();
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") {
}
if(Dump.isOn("benchmark")) {
- Dump("benchmark") << GetOptionCommand(key);
+ d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
}
if(key == "command-verbosity") {
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 */
#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"
class LogicRequest;
class StatisticsRegistry;
+class Printer;
+
/* -------------------------------------------------------------------------- */
namespace api {
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()?
/** 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(); }
/** The options object */
Options d_options;
+
+ /** the output manager for commands */
+ mutable OutputManager d_outMgr;
+
/**
* Manager for limiting time and abstract resource usage.
*/
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;
* 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());
* 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
#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"
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)
{
}
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;
#include "util/result.h"
namespace CVC4 {
+
+class OutputManager;
+
namespace smt {
class Preprocessor;
class SygusSolver
{
public:
- SygusSolver(SmtSolver& sms, Preprocessor& pp, context::UserContext* u);
+ SygusSolver(SmtSolver& sms,
+ Preprocessor& pp,
+ context::UserContext* u,
+ OutputManager& outMgr);
~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
#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"
#include "expr/node_algorithm.h"
#include "options/arrays_options.h"
#include "options/smt_options.h"
-#include "smt/command.h"
#include "smt/logic_exception.h"
#include "smt/smt_statistics_registry.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/bv/abstraction.h"
#include "options/bv_options.h"
+#include "printer/printer.h"
#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
-
using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::bv;
}
Node AbstractionModule::simplifyConflict(TNode conflict) {
- if (Dump.isOn("bv-abstraction")) {
- NodeNodeMap seen;
- Node c = reverseAbstraction(conflict, seen);
- Dump("bv-abstraction") << PushCommand();
- Dump("bv-abstraction") << AssertCommand(c.toExpr());
- Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
- }
-
Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
if (conflict.getKind() != kind::AND)
return conflict;
Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
Debug("bv-abstraction") << " => " << new_conflict <<"\n";
- if (Dump.isOn("bv-abstraction")) {
-
- NodeNodeMap seen;
- Node nc = reverseAbstraction(new_conflict, seen);
- Dump("bv-abstraction") << PushCommand();
- Dump("bv-abstraction") << AssertCommand(nc.toExpr());
- Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
- }
-
return new_conflict;
}
lemmas.push_back(lemma);
Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
storeLemma(lemma);
-
- if (Dump.isOn("bv-abstraction")) {
- NodeNodeMap seen;
- Node l = reverseAbstraction(lemma, seen);
- Dump("bv-abstraction") << PushCommand();
- Dump("bv-abstraction") << AssertCommand(l.toExpr());
- Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
- }
}
}
}
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv.h"
d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
d_bitblastingRegistrar.get(),
d_nullContext.get(),
+ nullptr,
rm,
false,
"EagerBitblaster"));
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/bv_solver_lazy.h"
d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
d_nullRegistrar.get(),
d_nullContext.get(),
+ nullptr,
rm,
false,
"LazyBitblaster"));
d_satSolver.reset(
prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
ResourceManager* rm = smt::currentResourceManager();
- d_cnfStream.reset(new prop::TseitinCnfStream(
- d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm));
+ d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
+ d_nullRegistrar.get(),
+ d_nullContext.get(),
+ nullptr,
+ rm));
d_satSolverNotify.reset(
d_emptyNotify
? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
#include "expr/node_algorithm.h"
#include "options/bv_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "smt_util/boolean_simplification.h"
#include "theory/bv/bv_quick_check.h"
TNode fact = worklist[r].node;
unsigned id = worklist[r].id;
- if (Dump.isOn("bv-algebraic")) {
- Node expl = d_explanations[id];
- Node query = utils::mkNot(nm->mkNode(kind::IMPLIES, expl, fact));
- Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
- Dump("bv-algebraic") << PushCommand();
- Dump("bv-algebraic") << AssertCommand(query.toExpr());
- Dump("bv-algebraic") << CheckSatCommand();
- Dump("bv-algebraic") << PopCommand();
- }
-
if (fact.isConst() &&
fact.getConst<bool>() == true) {
continue;
d_isComplete.set(true);
Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
- if (Dump.isOn("bv-algebraic")) {
- Dump("bv-algebraic")
- << EchoCommand("BVSolverLazy::AlgebraicSolver::conflict");
- Dump("bv-algebraic") << PushCommand();
- Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
- Dump("bv-algebraic") << CheckSatCommand();
- Dump("bv-algebraic") << PopCommand();
- }
-
-
++(d_statistics.d_numSimplifiesToFalse);
++(d_numSolved);
return false;
Node new_right = nm->mkNode(kind::BITVECTOR_XOR, right, inverse);
bool changed = subst.addSubstitution(var, new_right, reason);
- if (Dump.isOn("bv-algebraic")) {
- Node query = utils::mkNot(nm->mkNode(
- kind::EQUAL, fact, nm->mkNode(kind::EQUAL, var, new_right)));
- Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
- Dump("bv-algebraic") << PushCommand();
- Dump("bv-algebraic") << AssertCommand(query.toExpr());
- Dump("bv-algebraic") << CheckSatCommand();
- Dump("bv-algebraic") << PopCommand();
- }
-
-
return changed;
}
#include <sstream>
#include "context/context.h"
-#include "smt/command.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
#include "util/statistics_registry.h"
Node condition = node.eqNode(result).notNode();
- Dump("bv-rewrites")
- << CommentCommand(os.str())
- << CheckSatCommand(condition.toExpr());
+ const Printer& printer =
+ smt::currentSmtEngine()->getOutputManager().getPrinter();
+ std::ostream& out =
+ smt::currentSmtEngine()->getOutputManager().getDumpOut();
+
+ printer.toStreamCmdComment(out, os.str());
+ printer.toStreamCmdCheckSat(out, condition);
}
}
Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
#include "theory/quantifiers/quant_util.h"
namespace CVC4 {
+
+class DTypeConstructor;
+
namespace theory {
namespace quantifiers {
#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
+#include "smt/command.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/first_order_model.h"
#include "expr/node.h"
#include "options/options.h"
#include "options/theory_options.h"
-#include "smt/command.h"
-#include "smt/dump.h"
#include "smt/logic_request.h"
#include "theory/assertion.h"
#include "theory/care_graph.h"
Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
- if(Dump.isOn("state")) {
- Dump("state") << AssertCommand(fact.d_assertion.toExpr());
- }
-
return fact;
}
#include "options/quantifiers_options.h"
#include "options/theory_options.h"
#include "preprocessing/assertion_pipeline.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
#include "smt/logic_exception.h"
#include "smt/term_formula_removal.h"
#include "theory/arith/arith_ite_utils.h"
context::UserContext* userContext,
ResourceManager* rm,
RemoveTermFormulas& iteRemover,
- const LogicInfo& logicInfo)
+ const LogicInfo& logicInfo,
+ OutputManager& outMgr)
: d_propEngine(nullptr),
d_context(context),
d_userContext(userContext),
d_logicInfo(logicInfo),
+ d_outMgr(outMgr),
d_pnm(nullptr),
d_lazyProof(
- d_pnm != nullptr
- ? new LazyCDProof(
- d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
- : nullptr),
+ d_pnm != nullptr ? new LazyCDProof(
+ d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
+ : nullptr),
d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
d_sharedTerms(this, context),
d_tc(nullptr),
d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms),
d_eager_model_building(false),
- d_possiblePropagations(context),
- d_hasPropagated(context),
d_inConflict(context, false),
d_inSatMode(false),
d_hasShutDown(false),
void TheoryEngine::interrupt() { d_interrupted = true; }
void TheoryEngine::preRegister(TNode preprocessed) {
-
- Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl;
- if(Dump.isOn("missed-t-propagations")) {
- d_possiblePropagations.push_back(preprocessed);
- }
+ Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
+ << std::endl;
d_preregisterQueue.push(preprocessed);
if (!d_inPreregister) {
void TheoryEngine::dumpAssertions(const char* tag) {
if (Dump.isOn(tag)) {
- Dump(tag) << CommentCommand("Starting completeness check");
+ const Printer& printer = d_outMgr.getPrinter();
+ std::ostream& out = d_outMgr.getDumpOut();
+ printer.toStreamCmdComment(out, "Starting completeness check");
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
Theory* theory = d_theoryTable[theoryId];
if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
- Dump(tag) << CommentCommand("Completeness check");
- Dump(tag) << PushCommand();
+ printer.toStreamCmdComment(out, "Completeness check");
+ printer.toStreamCmdPush(out);
// Dump the shared terms
if (d_logicInfo.isSharingEnabled()) {
- Dump(tag) << CommentCommand("Shared terms");
+ printer.toStreamCmdComment(out, "Shared terms");
context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
for (unsigned i = 0; it != it_end; ++ it, ++i) {
stringstream ss;
ss << (*it);
- Dump(tag) << CommentCommand(ss.str());
+ printer.toStreamCmdComment(out, ss.str());
}
}
// Dump the assertions
- Dump(tag) << CommentCommand("Assertions");
+ printer.toStreamCmdComment(out, "Assertions");
context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
for (; it != it_end; ++ it) {
// Get the assertion
if ((*it).d_isPreregistered)
{
- Dump(tag) << CommentCommand("Preregistered");
+ printer.toStreamCmdComment(out, "Preregistered");
}
else
{
- Dump(tag) << CommentCommand("Shared assertion");
+ printer.toStreamCmdComment(out, "Shared assertion");
}
- Dump(tag) << AssertCommand(assertionNode.toExpr());
+ printer.toStreamCmdAssert(out, assertionNode);
}
- Dump(tag) << CheckSatCommand();
+ printer.toStreamCmdCheckSat(out);
- Dump(tag) << PopCommand();
+ printer.toStreamCmdPop(out);
}
}
}
// Do the checking
CVC4_FOR_EACH_THEORY;
- if(Dump.isOn("missed-t-conflicts")) {
- Dump("missed-t-conflicts")
- << CommentCommand("Completeness check for T-conflicts; expect sat")
- << CheckSatCommand();
- }
-
Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
// We are still satisfiable, propagate as much as possible
// Propagate for each theory using the statement above
CVC4_FOR_EACH_THEORY;
-
- if(Dump.isOn("missed-t-propagations")) {
- for(unsigned i = 0; i < d_possiblePropagations.size(); ++i) {
- Node atom = d_possiblePropagations[i];
- bool value;
- if(d_propEngine->hasValue(atom, value)) {
- continue;
- }
- // Doesn't have a value, check it (and the negation)
- if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
- Dump("missed-t-propagations")
- << CommentCommand("Completeness check for T-propagations; expect invalid")
- << EchoCommand(atom.toString())
- << QueryCommand(atom.toExpr())
- << EchoCommand(atom.notNode().toString())
- << QueryCommand(atom.notNode().toExpr());
- }
- }
- }
}
Node TheoryEngine::getNextDecisionRequest()
// spendResource();
- if(Dump.isOn("t-propagations")) {
- Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
- << QueryCommand(literal.toExpr());
- }
- if(Dump.isOn("missed-t-propagations")) {
- d_hasPropagated.insert(literal);
- }
-
// Get the atom
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
if(Dump.isOn("t-lemmas")) {
// we dump the negation of the lemma, to show validity of the lemma
Node n = lemma.negate();
- Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
- << CheckSatCommand(n.toExpr());
+ const Printer& printer = d_outMgr.getPrinter();
+ std::ostream& out = d_outMgr.getDumpOut();
+ printer.toStreamCmdComment(out, "theory lemma: expect valid");
+ printer.toStreamCmdCheckSat(out, n);
}
bool removable = isLemmaPropertyRemovable(p);
bool preprocess = isLemmaPropertyPreprocess(p);
d_inConflict = true;
if(Dump.isOn("t-conflicts")) {
- Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
- << CheckSatCommand(conflict.toExpr());
+ const Printer& printer = d_outMgr.getPrinter();
+ std::ostream& out = d_outMgr.getDumpOut();
+ printer.toStreamCmdComment(out, "theory conflict: expect unsat");
+ printer.toStreamCmdCheckSat(out, conflict);
}
// In the multiple-theories case, we need to reconstruct the conflict
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "prop/prop_engine.h"
-#include "smt/command.h"
#include "theory/atom_requests.h"
#include "theory/engine_output_channel.h"
#include "theory/interrupted.h"
*/
const LogicInfo& d_logicInfo;
+ /** Reference to the output manager of the smt engine */
+ OutputManager& d_outMgr;
+
//--------------------------------- new proofs
/** Proof node manager used by this theory engine, if proofs are enabled */
ProofNodeManager* d_pnm;
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
- /**
- * Used for "missed-t-propagations" dumping mode only. A set of all
- * theory-propagable literals.
- */
- context::CDList<TNode> d_possiblePropagations;
-
- /**
- * Used for "missed-t-propagations" dumping mode only. A
- * context-dependent set of those theory-propagable literals that
- * have been propagated.
- */
- context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
-
/**
* Output channels for individual theories.
*/
context::UserContext* userContext,
ResourceManager* rm,
RemoveTermFormulas& iteRemover,
- const LogicInfo& logic);
+ const LogicInfo& logic,
+ OutputManager& outMgr);
/** Destroys a theory engine */
~TheoryEngine();
#include "options/language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "smt/command.h"
using namespace CVC4;
using namespace CVC4::parser;
d_cnfContext = new context::Context();
d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
ResourceManager* rm = d_smt->getResourceManager();
- d_cnfStream = new CVC4::prop::TseitinCnfStream(
- d_satSolver, d_cnfRegistrar, d_cnfContext, rm);
+ d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver,
+ d_cnfRegistrar,
+ d_cnfContext,
+ &d_smt->getOutputManager(),
+ rm);
}
void tearDown() override
projects / cvc5.git / commitdiff