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 697202ba123d41e37f95450ccc4936fe25d3d43d..f541b5fe3045e1b450f02069c850ff7246870de3 100644 (file)
--- 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 7eb0652ba5bff5eaf0f3951a2f51cca5a7e5192c..0a473100c6f79cf4bded6fe2291a8c0723a04d0a 100644 (file)
--- 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 5d49bfc5f0fe65efdbb5cb0e7983945a30a2e6cb..bb8cbd300b6f654ac890415ce49a222fa3b009dd 100644 (file)
--- 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 8ee7eebf63d15ac8efa6da0a7c5a794181731860..b5147d1b7090bda2f9178f41f1fdcea846f3d771 100644 (file)
--- 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 6e47b6b8fd75cfb40dcd0f2966202d35b738cb52..a309b50051f6b26f77d67329dd96534e8c44d891 100644 (file)
--- 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 b89a4a9b655ba0447fc15c42ff4d833762bab038..f91bf5d0dc2dd21ccaccba37958b9fa91632078e 100644 (file)
--- 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 2f0df00a876b093e2f3589c938685357c177da06..c495f56187b436fd0ed9c495605b792fe531e879 100644 (file)
--- 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 dec582579070ce4d2a146339a7d67e2d880f9dd3..2c6f15702798ff693debc06f6375eaf12bd2b71d 100644 (file)
--- 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 ac9606c90b2e62a1c53be5c1ce9b2e4281bca6a6..59869453af7292b09d286077e858955fed774a12 100644 (file)
--- 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 9420b0251808715ea59b5626fe369f9aeb123ca8..b2d7ccb8f22056a68c238b2266dad5a1aa247a80 100644 (file)
--- 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<cvc5::Term> 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<const cvc5::Term, cvc5::Term>& 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 65adafce6cc0591d0188f98a380f79abfedd0b6a..ba6e30f1b1436c614888fe4d29a785204965dc98 100644 (file)
--- 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<cvc5::Term>& 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<cvc5::Term>& 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<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;
 
@@ -1025,7 +1025,7 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command
   const std::vector<cvc5::Term>& 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<cvc5::Term, cvc5::Term>& 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<cvc5::Term>& 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 19336df5aa385d0646112620264565ccaa4620f5..4099df7715f3b57ad3ae5b0dd7cb17a7edcbc505 100644 (file)
--- 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 ed5fb7a43c746d7e1585bcf10e696260d6838e10..4b0876abb0e04b073ec0076703cc1e4903b0e097 100644 (file)
--- 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<Node, std::vector<Node>> 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 1d9ef1dfe49c9bb515fe484da8c0129804be8776..d7beb12c80e3c791168f1c10c930b60ac02ac4f8 100644 (file)
--- 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<const Node, uint32_t>& i : d_instDebugTemp)
     {
       Node name;