From: Andres Noetzli Date: Thu, 23 Jun 2022 19:25:29 +0000 (-0700) Subject: Move non-stream options out of `printer_options.toml` (#8909) X-Git-Tag: cvc5-1.0.1~35 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=288ad5358ef79097f35a656def614c664006d6b9;p=cvc5.git Move non-stream options out of `printer_options.toml` (#8909) After #8827, we automatically generate code for the options listed in printer_options.toml, which allows those options to be set on input/output streams. Some of the options that are currently in printer_options.toml are not a good fit for that and this commit moves them out of the file. This is in preparation of making that stream options public (or at public in the parser), because some commands require setting stream options. --- diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 697202ba1..f541b5fe3 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -174,3 +174,11 @@ name = "Driver" type = "uint64_t" default = "1" help = "Number of parallel jobs the portfolio engine can run" + +[[option]] + name = "printSuccess" + category = "common" + long = "print-success" + type = "bool" + default = "false" + help = "print the \"success\" output required of SMT-LIBv2" diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index 7eb0652ba..0a473100c 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -30,53 +30,6 @@ name = "Printing" minimum = "0" help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)" -[[option]] - name = "printInstMode" - category = "common" - long = "print-inst=MODE" - type = "PrintInstMode" - default = "LIST" - help = "print format for printing instantiations" - help_mode = "Print format for printing instantiations." -[[option.mode.LIST]] - name = "list" - help = "Print the list of instantiations per quantified formula, when non-empty." -[[option.mode.NUM]] - name = "num" - help = "Print the total number of instantiations per quantified formula, when non-zero." - -[[option]] - name = "printInstFull" - category = "regular" - long = "print-inst-full" - type = "bool" - default = "true" - help = "print instantiations for formulas that do not have given identifiers" - -[[option]] - name = "printDotAsDAG" - category = "expert" - long = "proof-dot-dag" - type = "bool" - default = "false" - help = "Indicates if the dot proof will be printed as a DAG or as a tree" - -[[option]] - name = "printDotClusters" - category = "regular" - long = "print-dot-clusters" - type = "bool" - default = "false" - help = "Whether the proof node clusters (e.g. SAT, CNF, INPUT) will be printed when using the dot format or not." - -[[option]] - name = "printUnsatCoresFull" - category = "regular" - long = "print-unsat-cores-full" - type = "bool" - default = "false" - help = "when printing unsat cores, include unlabeled assertions" - [[option]] name = "flattenHOChains" category = "expert" @@ -103,24 +56,6 @@ name = "Printing" name = "none" help = "(default) do not print declarations of uninterpreted elements in models." -[[option]] - name = "sygusOut" - category = "regular" - long = "sygus-out=MODE" - type = "SygusSolutionOutMode" - default = "STANDARD" - help = "output mode for sygus" - help_mode = "Modes for sygus solution output." -[[option.mode.STATUS]] - name = "status" - help = "Print only status for check-synth calls." -[[option.mode.STATUS_AND_DEF]] - name = "status-and-def" - help = "Print status followed by definition corresponding to solution." -[[option.mode.STANDARD]] - name = "sygus-standard" - help = "Print based on SyGuS standard." - [[option]] name = "bvPrintConstsAsIndexedSymbols" category = "regular" @@ -128,11 +63,3 @@ name = "Printing" type = "bool" default = "false" help = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x" - -[[option]] - name = "printSuccess" - category = "common" - long = "print-success" - type = "bool" - default = "false" - help = "print the \"success\" output required of SMT-LIBv2" diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index 5d49bfc5f..bb8cbd300 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -115,3 +115,19 @@ name = "Proof" type = "bool" default = "false" help = "Add pivots to Alethe resolution steps" + +[[option]] + name = "printDotAsDAG" + category = "expert" + long = "proof-dot-dag" + type = "bool" + default = "false" + help = "Indicates if the dot proof will be printed as a DAG or as a tree" + +[[option]] + name = "printDotClusters" + category = "regular" + long = "print-dot-clusters" + type = "bool" + default = "false" + help = "Whether the proof node clusters (e.g. SAT, CNF, INPUT) will be printed when using the dot format or not." diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8ee7eebf6..b5147d1b7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -448,6 +448,29 @@ name = "Quantifiers" default = "2" help = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen" +[[option]] + name = "printInstMode" + category = "common" + long = "print-inst=MODE" + type = "PrintInstMode" + default = "LIST" + help = "print format for printing instantiations" + help_mode = "Print format for printing instantiations." +[[option.mode.LIST]] + name = "list" + help = "Print the list of instantiations per quantified formula, when non-empty." +[[option.mode.NUM]] + name = "num" + help = "Print the total number of instantiations per quantified formula, when non-zero." + +[[option]] + name = "printInstFull" + category = "regular" + long = "print-inst-full" + type = "bool" + default = "true" + help = "print instantiations for formulas that do not have given identifiers" + [[option]] name = "instMaxLevel" category = "expert" @@ -833,6 +856,24 @@ name = "Quantifiers" default = "false" help = "support SyGuS commands" +[[option]] + name = "sygusOut" + category = "regular" + long = "sygus-out=MODE" + type = "SygusSolutionOutMode" + default = "STANDARD" + help = "output mode for sygus" + help_mode = "Modes for sygus solution output." +[[option.mode.STATUS]] + name = "status" + help = "Print only status for check-synth calls." +[[option.mode.STATUS_AND_DEF]] + name = "status-and-def" + help = "Print status followed by definition corresponding to solution." +[[option.mode.STANDARD]] + name = "sygus-standard" + help = "Print based on SyGuS standard." + [[option]] name = "cegqiSingleInvMode" category = "regular" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 6e47b6b8f..a309b5005 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -175,6 +175,14 @@ name = "SMT Layer" default = "false" help = "if an unsat core is produced, it is reduced to a minimal unsat core" +[[option]] + name = "printUnsatCoresFull" + category = "regular" + long = "print-unsat-cores-full" + type = "bool" + default = "false" + help = "when printing unsat cores, include unlabeled assertions" + [[option]] name = "checkUnsatCores" category = "regular" diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index b89a4a9b6..f91bf5d0d 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -424,10 +424,7 @@ static bool tryToStream(std::ostream& out, const cvc5::Command* c) static void toStream(std::ostream& out, const cvc5::CommandSuccess* s) { - if (options::ioutils::getPrintSuccess(out)) - { - out << "OK" << endl; - } + out << "OK" << endl; } static void toStream(std::ostream& out, const cvc5::CommandInterrupted* s) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2f0df00a8..c495f5618 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2120,10 +2120,7 @@ static void toStream(std::ostream& out, const cvc5::CommandSuccess* s, Variant v) { - if (options::ioutils::getPrintSuccess(out)) - { - out << "success" << endl; - } + out << "success" << endl; } static void toStream(std::ostream& out, diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index dec582579..2c6f15702 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -30,8 +30,10 @@ namespace cvc5::internal { namespace proof { -DotPrinter::DotPrinter() - : d_lbind(options::dagThresh() ? options::dagThresh() + 1 : 0), d_ruleID(0) +DotPrinter::DotPrinter(Env& env) + : EnvObj(env), + d_lbind(options::dagThresh() ? options::dagThresh() + 1 : 0), + d_ruleID(0) { const std::string acronyms[5] = {"SAT", "CNF", "TL", "PP", "IN"}; const std::string colors[5] = {"purple", "yellow", "green", "brown", "blue"}; @@ -205,7 +207,7 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn) ancestorHashs, ProofNodeClusterType::NOT_DEFINED); - if (options::ioutils::getPrintDotClusters(out)) + if (options().proof.printDotClusters) { // Print the sub-graphs for (unsigned i = 0; i < 5; i++) @@ -228,7 +230,7 @@ uint64_t DotPrinter::printInternal( uint64_t currentRuleID = d_ruleID; // Print DAG option enabled - if (options::ioutils::getPrintDotAsDAG(out)) + if (options().proof.printDotAsDAG) { ProofNodeHashFunction hasher; size_t currentHash = hasher(pn); @@ -273,7 +275,7 @@ uint64_t DotPrinter::printInternal( } ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED; - if (options::ioutils::getPrintDotClusters(out)) + if (options().proof.printDotClusters) { // Define the type of this node proofNodeType = defineProofNodeType(pn, parentType); @@ -303,7 +305,7 @@ uint64_t DotPrinter::printInternal( ancestorHashs, proofNodeType); out << "\t" << childId << " -> " << currentRuleID << ";\n"; - if (options::ioutils::getPrintDotAsDAG(out)) + if (options().proof.printDotAsDAG) { ancestorHashs.pop_back(); } @@ -321,7 +323,7 @@ uint64_t DotPrinter::printInternal( ancestorHashs, proofNodeType); out << "\t" << childId << " -> " << currentRuleID << ";\n"; - if (options::ioutils::getPrintDotAsDAG(out)) + if (options().proof.printDotAsDAG) { ancestorHashs.pop_back(); } @@ -329,7 +331,7 @@ uint64_t DotPrinter::printInternal( } // If it's a scope, then remove from the stack - if (isSCOPE(r) && options::ioutils::getPrintDotClusters(out)) + if (isSCOPE(r) && options().proof.printDotClusters) { d_scopesArgs.pop_back(); } diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index ac9606c90..59869453a 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -23,6 +23,7 @@ #include "printer/let_binding.h" #include "proof/proof_node.h" +#include "smt/env_obj.h" namespace cvc5::internal { namespace proof { @@ -68,10 +69,10 @@ enum class ProofNodeClusterType : uint8_t NOT_DEFINED }; -class DotPrinter +class DotPrinter : protected EnvObj { public: - DotPrinter(); + DotPrinter(Env& env); ~DotPrinter(); /** diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 9420b0251..b2d7ccb8f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -168,7 +168,7 @@ void Command::invoke(cvc5::Solver* solver, SymbolManager* sm, std::ostream& out) } else if (!isMuted()) { - printResult(out); + printResult(solver, out); } } @@ -184,9 +184,11 @@ void CommandStatus::toStream(std::ostream& out) const Printer::getPrinter(out)->toStream(out, this); } -void Command::printResult(std::ostream& out) const +void Command::printResult(cvc5::Solver* solver, std::ostream& out) const { - if (d_commandStatus != nullptr) + if (!ok() + || (d_commandStatus != nullptr + && solver->getOption("print-success") == "true")) { out << *d_commandStatus; } @@ -271,7 +273,7 @@ void EchoCommand::invoke(cvc5::Solver* solver, Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~" << std::endl; d_commandStatus = CommandSuccess::instance(); - printResult(out); + printResult(solver, out); } std::string EchoCommand::getCommandName() const { return "echo"; } @@ -383,7 +385,7 @@ void CheckSatCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) cvc5::Result CheckSatCommand::getResult() const { return d_result; } -void CheckSatCommand::printResult(std::ostream& out) const +void CheckSatCommand::printResult(cvc5::Solver* solver, std::ostream& out) const { out << d_result << endl; } @@ -436,7 +438,8 @@ cvc5::Result CheckSatAssumingCommand::getResult() const return d_result; } -void CheckSatAssumingCommand::printResult(std::ostream& out) const +void CheckSatAssumingCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << d_result << endl; } @@ -704,7 +707,8 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } cvc5::SynthResult CheckSynthCommand::getResult() const { return d_result; } -void CheckSynthCommand::printResult(std::ostream& out) const +void CheckSynthCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << d_solution.str(); } @@ -1272,7 +1276,7 @@ void SimplifyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } cvc5::Term SimplifyCommand::getResult() const { return d_result; } -void SimplifyCommand::printResult(std::ostream& out) const +void SimplifyCommand::printResult(cvc5::Solver* solver, std::ostream& out) const { out << d_result << endl; } @@ -1330,7 +1334,7 @@ void GetValueCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } cvc5::Term GetValueCommand::getResult() const { return d_result; } -void GetValueCommand::printResult(std::ostream& out) const +void GetValueCommand::printResult(cvc5::Solver* solver, std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); @@ -1388,7 +1392,8 @@ void GetAssignmentCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } cvc5::Term GetAssignmentCommand::getResult() const { return d_result; } -void GetAssignmentCommand::printResult(std::ostream& out) const +void GetAssignmentCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << d_result << endl; } @@ -1427,7 +1432,10 @@ void GetModelCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetModelCommand::printResult(std::ostream& out) const { out << d_result; } +void GetModelCommand::printResult(cvc5::Solver* solver, std::ostream& out) const +{ + out << d_result; +} std::string GetModelCommand::getCommandName() const { return "get-model"; } @@ -1534,7 +1542,10 @@ void GetProofCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetProofCommand::printResult(std::ostream& out) const { out << d_result; } +void GetProofCommand::printResult(cvc5::Solver* solver, std::ostream& out) const +{ + out << d_result; +} std::string GetProofCommand::getCommandName() const { return "get-proof"; } @@ -1570,7 +1581,8 @@ void GetInstantiationsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetInstantiationsCommand::printResult(std::ostream& out) const +void GetInstantiationsCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << d_solver->getInstantiations(); } @@ -1633,7 +1645,8 @@ void GetInterpolantCommand::invoke(Solver* solver, SymbolManager* sm) } } -void GetInterpolantCommand::printResult(std::ostream& out) const +void GetInterpolantCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); @@ -1682,7 +1695,8 @@ void GetInterpolantNextCommand::invoke(Solver* solver, SymbolManager* sm) } } -void GetInterpolantNextCommand::printResult(std::ostream& out) const +void GetInterpolantNextCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); @@ -1755,7 +1769,8 @@ void GetAbductCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetAbductCommand::printResult(std::ostream& out) const +void GetAbductCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); @@ -1801,7 +1816,8 @@ void GetAbductNextCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetAbductNextCommand::printResult(std::ostream& out) const +void GetAbductNextCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); @@ -1867,7 +1883,8 @@ cvc5::Term GetQuantifierEliminationCommand::getResult() const { return d_result; } -void GetQuantifierEliminationCommand::printResult(std::ostream& out) const +void GetQuantifierEliminationCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << d_result << endl; } @@ -1911,7 +1928,8 @@ std::vector GetUnsatAssumptionsCommand::getResult() const return d_result; } -void GetUnsatAssumptionsCommand::printResult(std::ostream& out) const +void GetUnsatAssumptionsCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { container_to_stream(out, d_result, "(", ")\n", " "); } @@ -1951,7 +1969,8 @@ void GetUnsatCoreCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetUnsatCoreCommand::printResult(std::ostream& out) const +void GetUnsatCoreCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { if (d_solver->getOption("print-unsat-cores-full") == "true") { @@ -2009,7 +2028,8 @@ void GetDifficultyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetDifficultyCommand::printResult(std::ostream& out) const +void GetDifficultyCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << "(" << std::endl; for (const std::pair& d : d_result) @@ -2069,7 +2089,8 @@ void GetLearnedLiteralsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetLearnedLiteralsCommand::printResult(std::ostream& out) const +void GetLearnedLiteralsCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << "(" << std::endl; for (const cvc5::Term& lit : d_result) @@ -2119,7 +2140,8 @@ void GetAssertionsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } std::string GetAssertionsCommand::getResult() const { return d_result; } -void GetAssertionsCommand::printResult(std::ostream& out) const +void GetAssertionsCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { out << d_result; } @@ -2239,7 +2261,7 @@ void GetInfoCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } std::string GetInfoCommand::getResult() const { return d_result; } -void GetInfoCommand::printResult(std::ostream& out) const +void GetInfoCommand::printResult(cvc5::Solver* solver, std::ostream& out) const { if (d_result != "") { @@ -2318,7 +2340,8 @@ void GetOptionCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } std::string GetOptionCommand::getResult() const { return d_result; } -void GetOptionCommand::printResult(std::ostream& out) const +void GetOptionCommand::printResult(cvc5::Solver* solver, + std::ostream& out) const { if (d_result != "") { diff --git a/src/smt/command.h b/src/smt/command.h index 65adafce6..ba6e30f1b 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -213,7 +213,7 @@ class CVC5_EXPORT Command * Print the result of running the command. This method is only called if the * command ran successfully. */ - virtual void printResult(std::ostream& out) const; + virtual void printResult(cvc5::Solver* solver, std::ostream& out) const; // These methods rely on Command being a friend of classes in the API. // Subclasses of command should use these methods for conversions, @@ -515,7 +515,7 @@ class CVC5_EXPORT CheckSatCommand : public Command CheckSatCommand(); cvc5::Result getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -537,7 +537,7 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command const std::vector& getTerms() const; cvc5::Result getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -698,7 +698,7 @@ class CVC5_EXPORT CheckSynthCommand : public Command /** returns the result of the check-synth call */ cvc5::SynthResult getResult() const; /** prints the result of the check-synth-call */ - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; /** invokes this command * * This invocation makes the SMT engine build a synthesis conjecture based on @@ -737,7 +737,7 @@ class CVC5_EXPORT SimplifyCommand : public Command cvc5::Term getTerm() const; cvc5::Term getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class SimplifyCommand */ @@ -755,7 +755,7 @@ class CVC5_EXPORT GetValueCommand : public Command const std::vector& getTerms() const; cvc5::Term getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class GetValueCommand */ @@ -770,7 +770,7 @@ class CVC5_EXPORT GetAssignmentCommand : public Command cvc5::Term getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class GetAssignmentCommand */ @@ -780,7 +780,7 @@ class CVC5_EXPORT GetModelCommand : public Command public: GetModelCommand(); void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -827,7 +827,7 @@ class CVC5_EXPORT GetProofCommand : public Command void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -844,7 +844,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command static bool isEnabled(cvc5::Solver* solver, const cvc5::Result& res); void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -879,7 +879,7 @@ class CVC5_EXPORT GetInterpolantCommand : public Command cvc5::Term getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -906,7 +906,7 @@ class CVC5_EXPORT GetInterpolantNextCommand : public Command cvc5::Term getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -946,7 +946,7 @@ class CVC5_EXPORT GetAbductCommand : public Command cvc5::Term getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -972,7 +972,7 @@ class CVC5_EXPORT GetAbductNextCommand : public Command cvc5::Term getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -998,7 +998,7 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : public Command bool getDoFull() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; cvc5::Term getResult() const; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -1010,7 +1010,7 @@ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command GetUnsatAssumptionsCommand(); void invoke(cvc5::Solver* solver, SymbolManager* sm) override; std::vector getResult() const; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -1025,7 +1025,7 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command const std::vector& getUnsatCore() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -1046,7 +1046,7 @@ class CVC5_EXPORT GetDifficultyCommand : public Command const std::map& getDifficultyMap() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -1065,7 +1065,7 @@ class CVC5_EXPORT GetLearnedLiteralsCommand : public Command const std::vector& getLearnedLiterals() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -1085,7 +1085,7 @@ class CVC5_EXPORT GetAssertionsCommand : public Command void invoke(cvc5::Solver* solver, SymbolManager* sm) override; std::string getResult() const; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class GetAssertionsCommand */ @@ -1134,7 +1134,7 @@ class CVC5_EXPORT GetInfoCommand : public Command std::string getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class GetInfoCommand */ @@ -1169,7 +1169,7 @@ class CVC5_EXPORT GetOptionCommand : public Command std::string getResult() const; void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out) const override; + void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class GetOptionCommand */ diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 19336df5a..4099df771 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -178,7 +178,7 @@ void PfManager::printProof(std::ostream& out, // according to the proof format, post process and print the proof node if (options().proof.proofFormatMode == options::ProofFormatMode::DOT) { - proof::DotPrinter dotPrinter; + proof::DotPrinter dotPrinter(d_env); dotPrinter.print(out, fp.get()); } else if (options().proof.proofFormatMode == options::ProofFormatMode::ALETHE) diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index ed5fb7a43..4b0876abb 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -31,6 +31,7 @@ #include "options/options_public.h" #include "options/parser_options.h" #include "options/printer_options.h" +#include "options/quantifiers_options.h" #include "options/proof_options.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -1575,9 +1576,9 @@ void SolverEngine::printInstantiations(std::ostream& out) // First, extract and print the skolemizations bool printed = false; - bool reqNames = !d_env->getOptions().printer.printInstFull; + bool reqNames = !d_env->getOptions().quantifiers.printInstFull; // only print when in list mode - if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST) + if (d_env->getOptions().quantifiers.printInstMode == options::PrintInstMode::LIST) { std::map> sks; qe->getSkolemTermVectors(sks); @@ -1635,7 +1636,7 @@ void SolverEngine::printInstantiations(std::ostream& out) continue; } // must have a name - if (d_env->getOptions().printer.printInstMode + if (d_env->getOptions().quantifiers.printInstMode == options::PrintInstMode::NUM) { out << "(num-instantiations " << name << " " << i.second.d_inst.size() @@ -1645,7 +1646,7 @@ void SolverEngine::printInstantiations(std::ostream& out) { // take the name i.second.d_quant = name; - Assert(d_env->getOptions().printer.printInstMode + Assert(d_env->getOptions().quantifiers.printInstMode == options::PrintInstMode::LIST); out << i.second; } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 1d9ef1dfe..d7beb12c8 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -17,7 +17,6 @@ #include "expr/node_algorithm.h" #include "options/base_options.h" -#include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "proof/lazy_proof.h" @@ -712,7 +711,7 @@ void Instantiate::notifyEndRound() } if (isOutputOn(OutputTag::INST)) { - bool req = !options().printer.printInstFull; + bool req = !options().quantifiers.printInstFull; for (std::pair& i : d_instDebugTemp) { Node name;