Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191)

Printing the original benchmark is simple, as it is exactly the commands we execute.

This removes the previous code from SmtEngine, which is currently broken.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 98e93ca5a14bbe91b4e875e84caa1334e751e03d..ad0d24143293c779623b63b6b25185e1b1368aff 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -197,6 +197,12 @@ bool solverInvoke(api::Solver* solver,
                   Command* cmd,
                   std::ostream& out)
 {
+  // print output for -o raw-benchmark
+  if (solver->isOutputOn("raw-benchmark"))
+  {
+    std::ostream& ss = solver->getOutput("raw-benchmark");
+    cmd->toStream(ss);
+  }
   cmd->invoke(solver, sm, out);
   // ignore the error if the command-verbosity is 0 for this command
   std::string commandName =

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index e3035e0d63d95fe2b13e67477dea99fbfcd75457..89032ba50fbf9ece9f4f9538563cbac2d2056ccf 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -233,6 +233,9 @@ name   = "Base"
 [[option.mode.TRIGGER]]
   name = "trigger"
   help = "print selected triggers for quantified formulas"
+[[option.mode.RAW_BENCHMARK]]
+  name = "raw-benchmark"
+  help = "print the benchmark back on the output verbatim as it is processed"
 
 # Stores then enabled output tags.
 [[option]]

diff --git a/src/smt/command.h b/src/smt/command.h
index 7d2d9cfc4be9230cc285a74929cec0d2725af0e0..b374a48c965ec20adfa8e006fc17522b3558d5ee 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -219,7 +219,6 @@ class CVC5_EXPORT Command
 
   virtual void toStream(std::ostream& out,
                         int toDepth = -1,
-
                         size_t dag = 1,
                         Language language = Language::LANG_AUTO) const = 0;
 

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 630a91288fc140ed90d5ab6debcf01b417a66f5c..d74668433e62fd59db7c0e307fd4addfb841c5c5 100644 (file)
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -78,10 +78,7 @@ void DumpC::setDumpFromString(const std::string& optarg) {
     while ((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL)
     {
       tokstr = NULL;
-      if (!strcmp(optargPtr, "raw-benchmark"))
-      {
-      }
-      else if (!strcmp(optargPtr, "benchmark"))
+      if (!strcmp(optargPtr, "benchmark"))
       {
       }
       else if (!strcmp(optargPtr, "declarations"))
@@ -163,11 +160,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
       if (strcmp(optargPtr, "benchmark"))
       {
         Dump.on("declarations");
-        if (strcmp(optargPtr, "declarations")
-            && strcmp(optargPtr, "raw-benchmark"))
-        {
-          Dump.on("skolems");
-        }
       }
     }
   }
@@ -190,10 +182,6 @@ benchmark\n\
 declarations\n\
 + Dump user declarations.  Implied by all following modes.\n\
 \n\
-raw-benchmark\n\
-+ Dump all user-commands as they are received (including assertions) without\n\
-  any preprocessing and without any internally-created commands.\n\
-\n\
 skolems\n\
 + Dump internally-created skolem variable declarations.  These can\n\
   arise from preprocessing simplifications, existential elimination,\n\
@@ -228,10 +216,9 @@ theory::fullcheck\n\
 + Output completeness queries for all full-check effort-level theory checks\n\
 \n\
 Dump modes can be combined by concatenating the above values with \",\" in\n\
-between them.  Generally you want raw-benchmark or, alternatively, one from\n\
-the assertions category (either assertions or clauses), and perhaps one or more\n\
-other modes for checking correctness and completeness of decision procedure\n\
-implementations.\n\
+between them.  Generally you want one from the assertions category (either\n\
+assertions or clauses), and perhaps one or more other modes for checking\n\
+correctness and completeness of decision procedure implementations.\n\
 \n\
 The --output-language option controls the language used for dumping, and\n\
 this allows you to connect cvc5 to another solver implementation via a UNIX\n\

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cd8bd1d7b25e0b55fbffe0ed245982424bdee263..279761b43d8b8cd9325182483104dc77a9ae3f97 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -231,7 +231,7 @@ void SmtEngine::finishInit()
 
   // dump out a set-logic command only when raw-benchmark is disabled to avoid
   // dumping the command twice.
-  if (Dump.isOn("benchmark") && !Dump.isOn("raw-benchmark"))
+  if (Dump.isOn("benchmark"))
   {
       LogicInfo everything;
       everything.lock();
@@ -338,12 +338,6 @@ void SmtEngine::setLogic(const std::string& s)
   try
   {
     setLogic(LogicInfo(s));
-    // dump out a set-logic command
-    if (Dump.isOn("raw-benchmark"))
-    {
-      getPrinter().toStreamCmdSetBenchmarkLogic(
-          d_env->getDumpOut(), getLogicInfo().getLogicString());
-    }
   }
   catch (IllegalArgumentException& e)
   {
@@ -643,12 +637,6 @@ void SmtEngine::defineFunctionsRec(
     debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
   }
 
-  if (Dump.isOn("raw-benchmark"))
-  {
-    getPrinter().toStreamCmdDefineFunctionRec(
-        d_env->getDumpOut(), funcs, formals, formulas);
-  }
-
   NodeManager* nm = getNodeManager();
   for (unsigned i = 0, size = funcs.size(); i < size; i++)
   {
@@ -679,9 +667,9 @@ void SmtEngine::defineFunctionsRec(
       Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]);
       lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr);
     }
-    // assert the quantified formula
-    //   notice we don't call assertFormula directly, since this would
-    //   duplicate the output on raw-benchmark.
+    // Assert the quantified formula. Notice we don't call assertFormula
+    // directly, since we should call a private member method since we have
+    // already ensuring this SmtEngine is initialized above.
     // add define recursive definition to the assertions
     d_asserts->addDefineFunDefinition(lem, global);
   }
@@ -968,11 +956,6 @@ Result SmtEngine::assertFormula(const Node& formula)
 
   Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
 
-  if (Dump.isOn("raw-benchmark"))
-  {
-    getPrinter().toStreamCmdAssert(d_env->getDumpOut(), formula);
-  }
-
   // Substitute out any abstract values in ex
   Node n = d_absValues->substituteAbstractValues(formula);
 
@@ -990,11 +973,6 @@ void SmtEngine::declareSygusVar(Node var)
 {
   SmtScope smts(this);
   d_sygusSolver->declareSygusVar(var);
-  if (Dump.isOn("raw-benchmark"))
-  {
-    getPrinter().toStreamCmdDeclareVar(d_env->getDumpOut(), var, var.getType());
-  }
-  // don't need to set that the conjecture is stale
 }
 
 void SmtEngine::declareSynthFun(Node func,
@@ -1006,16 +984,6 @@ void SmtEngine::declareSynthFun(Node func,
   finishInit();
   d_state->doPendingPops();
   d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars);
-
-  // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot
-  // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we
-  // must print the command using the Node-level utility method for now.
-
-  if (Dump.isOn("raw-benchmark"))
-  {
-    getPrinter().toStreamCmdSynthFun(
-        d_env->getDumpOut(), func, vars, isInv, sygusType);
-  }
 }
 void SmtEngine::declareSynthFun(Node func,
                                 bool isInv,
@@ -1031,10 +999,6 @@ void SmtEngine::assertSygusConstraint(Node constraint)
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusConstraint(constraint);
-  if (Dump.isOn("raw-benchmark"))
-  {
-    getPrinter().toStreamCmdConstraint(d_env->getDumpOut(), constraint);
-  }
 }
 
 void SmtEngine::assertSygusInvConstraint(Node inv,
@@ -1045,11 +1009,6 @@ void SmtEngine::assertSygusInvConstraint(Node inv,
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
-  if (Dump.isOn("raw-benchmark"))
-  {
-    getPrinter().toStreamCmdInvConstraint(
-        d_env->getDumpOut(), inv, pre, trans, post);
-  }
 }
 
 Result SmtEngine::checkSynth()
@@ -1200,12 +1159,7 @@ std::string SmtEngine::getModel(const std::vector<TypeNode>& declaredSorts,
   // completely accessible by the user. This is currently not rigorously
   // enforced. An alternative design would be to have this method implemented
   // at the API level, but this makes exceptions in the text interface less
-  // intuitive and makes it impossible to implement raw-benchmark at the
-  // SmtEngine level.
-  if (Dump.isOn("raw-benchmark"))
-  {
-    getPrinter().toStreamCmdGetModel(d_env->getDumpOut());
-  }
+  // intuitive.
   TheoryModel* tm = getAvailableModel("get model");
   // use the smt::Model model utility for printing
   const Options& opts = d_env->getOptions();

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 240f96af741654cce7a3931b5ff1ac54344f16c3..32a0ee22033f82c5ffe8a421bb2b4fa482c07582 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -25,8 +25,6 @@
 #include "options/option_exception.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/datatypes/sygus_datatype_utils.h"
@@ -211,10 +209,6 @@ Result SygusSolver::checkSynth(Assertions& as)
     Trace("smt") << "...constructed forall " << body << std::endl;
 
     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
-    if (Dump.isOn("raw-benchmark"))
-    {
-      d_env.getPrinter().toStreamCmdCheckSynth(d_env.getDumpOut());
-    }
 
     d_sygusConjectureStale = false;
 

diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc
index e28fc630503252b4f88daf27e03f8fdfd5aab4cf..8a193b71ae9ded3f4309264f631aba54156d4970 100644 (file)
--- a/test/regress/regress0/datatypes/datatype-dump.cvc
+++ b/test/regress/regress0/datatypes/datatype-dump.cvc
@@ -1,7 +1,7 @@
 % This regression is the same as datatype.cvc but tests the
 % dumping infrastructure.
 %
-% COMMAND-LINE: --dump raw-benchmark
+% COMMAND-LINE: -o raw-benchmark
 %
 % EXPECT: OPTION "incremental" false;
 % EXPECT: OPTION "logic" "ALL";

diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2
index 02eb3376aeef671aaed6180e4304e746be98ac86..fbea9d1428d8671537099c73268add4201d3c7b7 100644 (file)
--- a/test/regress/regress0/printer/let_shadowing.smt2
+++ b/test/regress/regress0/printer/let_shadowing.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: dumping
-; COMMAND-LINE: --dump raw-benchmark --preprocess-only
+; COMMAND-LINE: -o raw-benchmark --preprocess-only
 ; SCRUBBER: grep assert
 ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0))))
 ; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0))))))

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 0f9bcda1a40b2054a93675352c04c49d649548b0..4c9ea3fcb733897b7cd447ca0b4adf260d608c93 100755 (executable)
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -141,7 +141,7 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary,
     exit_status = None
     if dump:
         dump_args = [
-            '--preprocess-only', '--dump', 'raw-benchmark',
+            '--preprocess-only', '-o', 'raw-benchmark',
             '--output-lang=smt2', '-qq'
         ]
         dump_output, _, _ = run_process(

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 75cd970607432c3566cbbe55bef719593f39a4dd..1f6f7801e5ec330ea9adc488916eb83fcc943c20 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1375,8 +1375,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
     EXPECT_EQ("NONE", modeInfo.defaultValue);
     EXPECT_EQ("OutputTag::NONE", modeInfo.currentValue);
-    std::vector<std::string> modes{"INST", "NONE", "SYGUS", "TRIGGER"};
-    EXPECT_EQ(modes, modeInfo.modes);
+    EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "NONE")
+                != modeInfo.modes.end());
   }
 }