diff options
53 files changed, 593 insertions, 501 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3b0794a8f..e6cb97894 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -216,6 +216,8 @@ libcvc4_add_sources( 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 diff --git a/src/main/command_executor.h b/src/main/command_executor.h index de21db74d..1c10aa09f 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -21,12 +21,13 @@ #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; } diff --git a/src/main/main.cpp b/src/main/main.cpp index 9cf168392..7b72ae249 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -32,7 +32,6 @@ #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" diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index bf5e8824a..54165feb7 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -33,7 +33,6 @@ #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; diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp index 4d409a0b4..7caa35dd6 100644 --- a/src/parser/cvc/cvc.cpp +++ b/src/parser/cvc/cvc.cpp @@ -15,6 +15,7 @@ **/ #include "parser/cvc/cvc.h" +#include "smt/command.h" namespace CVC4 { namespace parser { diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index 7c226168f..3930a02f5 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -21,7 +21,6 @@ #include "api/cvc4cpp.h" #include "parser/parser.h" -#include "smt/command.h" namespace CVC4 { diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 13903eaf5..8d5057151 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -23,7 +23,6 @@ #include "expr/type.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "smt/command.h" using namespace std; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 2e725f9bf..ebf3811c4 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -28,12 +28,12 @@ #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 { diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index cb4d3fd9e..ab6a4c5eb 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -24,6 +24,7 @@ #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 diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 3d5419be9..40dd85f63 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -28,11 +28,12 @@ #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; } diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 965edcd2f..cd2a51c45 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -18,6 +18,7 @@ #include "smt/dump.h" #include "smt/smt_statistics_registry.h" +#include "printer/printer.h" namespace CVC4 { namespace preprocessing { @@ -39,8 +40,13 @@ void PreprocessingPass::dumpAssertions(const char* key, 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); } } } diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index f776d07db..e179b7ffd 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -166,23 +166,28 @@ void AstPrinter::toStream(std::ostream& out, 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 { @@ -194,6 +199,7 @@ void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const { out << "CheckSat(" << n << ')'; } + out << std::endl; } void AstPrinter::toStreamCmdCheckSatAssuming( @@ -201,22 +207,28 @@ 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 @@ -228,7 +240,7 @@ void AstPrinter::toStreamCmdDeclarationSequence( { out << *i << endl; } - out << "]"; + out << "]" << std::endl; } void AstPrinter::toStreamCmdCommandSequence( @@ -241,14 +253,14 @@ 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, @@ -263,7 +275,7 @@ 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, @@ -271,7 +283,8 @@ 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, @@ -287,7 +300,7 @@ void AstPrinter::toStreamCmdDefineType(std::ostream& out, ostream_iterator<TypeNode>(out, ", ")); out << params.back(); } - out << "]," << t << ')'; + out << "]," << t << ')' << std::endl; } void AstPrinter::toStreamCmdDefineNamedFunction( @@ -304,7 +317,7 @@ 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, @@ -312,70 +325,70 @@ 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( @@ -386,13 +399,13 @@ 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> diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 02afa715d..46b509388 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1203,12 +1203,18 @@ void CvcPrinter::toStream(std::ostream& out, 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 { @@ -1228,6 +1234,7 @@ void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const { out << " POP;"; } + out << std::endl; } void CvcPrinter::toStreamCmdCheckSatAssuming( @@ -1251,6 +1258,7 @@ void CvcPrinter::toStreamCmdCheckSatAssuming( { out << " POP;"; } + out << std::endl; } void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const @@ -1271,18 +1279,22 @@ 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( @@ -1292,7 +1304,7 @@ void CvcPrinter::toStreamCmdCommandSequence( i != sequence.cend(); ++i) { - out << *i << endl; + out << *i; } } @@ -1314,13 +1326,14 @@ void CvcPrinter::toStreamCmdDeclarationSequence( 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, @@ -1353,7 +1366,7 @@ void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out, } out << "): "; } - out << formula << ';'; + out << formula << ';' << std::endl; } void CvcPrinter::toStreamCmdDeclareType(std::ostream& out, @@ -1370,7 +1383,7 @@ void CvcPrinter::toStreamCmdDeclareType(std::ostream& out, } else { - out << id << " : TYPE;"; + out << id << " : TYPE;" << std::endl; } } @@ -1387,7 +1400,7 @@ void CvcPrinter::toStreamCmdDefineType(std::ostream& out, } else { - out << id << " : TYPE = " << t << ';'; + out << id << " : TYPE = " << t << ';' << std::endl; } } @@ -1403,7 +1416,7 @@ void CvcPrinter::toStreamCmdDefineNamedFunction( void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const { - out << "TRANSFORM " << n << ';'; + out << "TRANSFORM " << n << ';' << std::endl; } void CvcPrinter::toStreamCmdGetValue(std::ostream& out, @@ -1414,44 +1427,44 @@ 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, @@ -1462,13 +1475,13 @@ 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, @@ -1477,13 +1490,13 @@ 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( @@ -1552,25 +1565,26 @@ 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> diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2cc6c8973..7ef02c576 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1451,15 +1451,18 @@ void Smt2Printer::toStream(std::ostream& out, 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 { @@ -1477,6 +1480,7 @@ void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const { out << "(check-sat)"; } + out << std::endl; } void Smt2Printer::toStreamCmdCheckSatAssuming( @@ -1484,7 +1488,7 @@ 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 @@ -1508,34 +1512,25 @@ 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; } } @@ -1563,7 +1558,7 @@ void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out, type = type.getRangeType(); } - out << ") " << type << ')'; + out << ") " << type << ')' << std::endl; } void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out, @@ -1590,7 +1585,7 @@ void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out, } } } - out << ") " << range << ' ' << formula << ')'; + out << ") " << range << ' ' << formula << ')' << std::endl; } void Smt2Printer::toStreamCmdDefineFunctionRec( @@ -1659,7 +1654,7 @@ void Smt2Printer::toStreamCmdDefineFunctionRec( { out << ")"; } - out << ")"; + out << ")" << std::endl; } static void toStreamRational(std::ostream& out, @@ -1704,7 +1699,8 @@ void Smt2Printer::toStreamCmdDeclareType(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, @@ -1719,7 +1715,7 @@ 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( @@ -1738,7 +1734,7 @@ 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, @@ -1746,49 +1742,49 @@ 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, @@ -1797,13 +1793,13 @@ 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, @@ -1812,13 +1808,13 @@ 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 @@ -1951,7 +1947,7 @@ void Smt2Printer::toStreamCmdDatatypeDeclaration( } out << ")"; } - out << ")" << endl; + out << ")" << std::endl; } void Smt2Printer::toStreamCmdComment(std::ostream& out, @@ -1964,12 +1960,13 @@ 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, @@ -1983,7 +1980,7 @@ 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; } /* @@ -2084,31 +2081,31 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out, { 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, @@ -2125,7 +2122,7 @@ void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, { toStreamSygusGrammar(out, sygusType); } - out << ')'; + out << ')' << std::endl; } /* diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index e54d976c9..03d614433 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -20,7 +20,6 @@ #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 { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index c46cd5136..203ed34e9 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -31,7 +31,9 @@ #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" @@ -42,10 +44,14 @@ using namespace CVC4::kind; 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), @@ -54,32 +60,41 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, 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); } } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index aec4257f2..f538a60a1 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -34,6 +34,8 @@ namespace CVC4 { +class OutputManager; + namespace prop { class PropEngine; @@ -56,6 +58,9 @@ class CnfStream { /** 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; @@ -166,12 +171,17 @@ class CnfStream { * @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 = ""); /** @@ -256,6 +266,8 @@ class TseitinCnfStream : public CnfStream { * @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 @@ -263,6 +275,7 @@ class TseitinCnfStream : public CnfStream { TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, + OutputManager* outMgr, ResourceManager* rm, bool fullLitToNodeMap = false, std::string name = ""); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 311224a03..e769ba6cc 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -669,9 +669,6 @@ void Solver::cancelUntil(int level) { // 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]); diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index a5f3664e8..0630df1b7 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -572,10 +572,6 @@ inline void Solver::newDecisionLevel() 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(); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e71e681e5..4b114aa2c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -34,7 +34,6 @@ #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" @@ -70,7 +69,8 @@ public: PropEngine::PropEngine(TheoryEngine* te, Context* satContext, UserContext* userContext, - ResourceManager* rm) + ResourceManager* rm, + OutputManager& outMgr) : d_inCheckSat(false), d_theoryEngine(te), d_context(satContext), @@ -79,7 +79,8 @@ PropEngine::PropEngine(TheoryEngine* te, d_registrar(NULL), d_cnfStream(NULL), d_interrupted(false), - d_resourceManager(rm) + d_resourceManager(rm), + d_outMgr(outMgr) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -91,7 +92,7 @@ PropEngine::PropEngine(TheoryEngine* te, 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); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 1df862568..75f628d9a 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -36,6 +36,7 @@ namespace CVC4 { class ResourceManager; class DecisionEngine; +class OutputManager; class TheoryEngine; namespace theory { @@ -62,7 +63,8 @@ class PropEngine PropEngine(TheoryEngine*, context::Context* satContext, context::UserContext* userContext, - ResourceManager* rm); + ResourceManager* rm, + OutputManager& outMgr); /** * Destructor. @@ -255,6 +257,8 @@ class PropEngine /** Pointer to resource manager for associated SmtEngine */ ResourceManager* d_resourceManager; + /** Reference to the output manager of the smt engine */ + OutputManager& d_outMgr; }; } // namespace prop diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 8165c5d8a..a89c8799f 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -22,7 +22,6 @@ #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" @@ -150,11 +149,5 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { return d_decisionEngine->getPolarity(var); } -void TheoryProxy::dumpStatePop() { - if(Dump.isOn("state")) { - Dump("state") << PopCommand(); - } -} - }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 7fd735bf2..688bd4e1c 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -88,9 +88,6 @@ class TheoryProxy SatValue getDecisionPolarity(SatVariable var); - /** Shorthand for Dump("state") << PopCommand() */ - void dumpStatePop(); - private: /** The prop engine we are using. */ PropEngine* d_propEngine; 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" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 408f4c682..3dc19d39b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -23,7 +23,6 @@ #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" diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index a9ec7aa53..d7899f010 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -15,12 +15,14 @@ #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; @@ -691,15 +693,6 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign } 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; @@ -742,16 +735,6 @@ Node AbstractionModule::simplifyConflict(TNode 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; } @@ -836,15 +819,6 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le 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(); - } } } } diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 6417740fd..48aa0fbd6 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -20,6 +20,7 @@ #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" @@ -71,6 +72,7 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), d_bitblastingRegistrar.get(), d_nullContext.get(), + nullptr, rm, false, "EagerBitblaster")); diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 1813784d7..93c91719b 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -21,6 +21,7 @@ #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" @@ -82,6 +83,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), + nullptr, rm, false, "LazyBitblaster")); @@ -573,8 +575,11 @@ void TLazyBitblaster::clearSolver() { 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() diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index e900566f9..52f68c6ef 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -19,6 +19,10 @@ #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" @@ -321,16 +325,6 @@ bool AlgebraicSolver::check(Theory::Effort e) 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; @@ -344,16 +338,6 @@ bool AlgebraicSolver::check(Theory::Effort e) 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; @@ -536,17 +520,6 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { 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; } diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 0dbb51753..549843421 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -22,7 +22,10 @@ #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" @@ -449,9 +452,13 @@ public: 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; diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index f5c13b183..0e1c5f6ce 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -26,6 +26,9 @@ #include "theory/quantifiers/quant_util.h" namespace CVC4 { + +class DTypeConstructor; + namespace theory { namespace quantifiers { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index b89015b00..bd9697084 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -17,6 +17,7 @@ #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" diff --git a/src/theory/theory.h b/src/theory/theory.h index 77652f874..da651d259 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -32,8 +32,6 @@ #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" @@ -911,10 +909,6 @@ inline theory::Assertion Theory::get() { 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; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7ff073cf3..b5167ffe4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -31,6 +31,8 @@ #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" @@ -211,17 +213,18 @@ TheoryEngine::TheoryEngine(context::Context* context, 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), @@ -231,8 +234,6 @@ TheoryEngine::TheoryEngine(context::Context* context, 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), @@ -285,11 +286,8 @@ TheoryEngine::~TheoryEngine() { 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) { @@ -400,26 +398,28 @@ void TheoryEngine::printAssertions(const char* tag) { 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 @@ -428,17 +428,17 @@ void TheoryEngine::dumpAssertions(const char* tag) { 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); } } } @@ -516,12 +516,6 @@ void TheoryEngine::check(Theory::Effort effort) { // 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 @@ -622,25 +616,6 @@ void TheoryEngine::propagate(Theory::Effort effort) // 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() @@ -1134,14 +1109,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { // 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]; @@ -1484,8 +1451,10 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, 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); @@ -1621,8 +1590,10 @@ void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) 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 diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 550a4f496..a6258b7d6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -33,7 +33,6 @@ #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" @@ -139,6 +138,9 @@ class TheoryEngine { */ 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; @@ -182,19 +184,6 @@ class TheoryEngine { 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. */ theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; @@ -330,7 +319,8 @@ class TheoryEngine { context::UserContext* userContext, ResourceManager* rm, RemoveTermFormulas& iteRemover, - const LogicInfo& logic); + const LogicInfo& logic, + OutputManager& outMgr); /** Destroys a theory engine */ ~TheoryEngine(); diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index ed00a3b8f..04e852408 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -28,7 +28,6 @@ #include "options/language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt/command.h" using namespace CVC4; using namespace CVC4::parser; diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 33fc15674..7fa429054 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -146,8 +146,11 @@ class CnfStreamWhite : public CxxTest::TestSuite { 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 |