Add output -o post-asserts (#7987)

This is equivalent to -t assertions::post-everything.

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 6a34978f57b1797ae7534466a41867437d01154a..6b7eaefb9b464df5e6e599e8243a422f8c49cd6e 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -198,6 +198,11 @@ name   = "Base"
   help = "print top-level substitutions learned during preprocessing"
   description = "With ``-o subs``, cvc5 prints top-level substitutions learned during preprocessing."
   example-file = "regress0/printer/subs-output.smt2"
+[[option.mode.POST_ASSERTS]]
+  name = "post-asserts"
+  help = "print assertions corresponding to the input problem after preprocessing"
+  description = "With ``-o post-asserts``, cvc5 prints assertions corresponding to the input problem after preprocessing."
+  example-file = "regress0/printer/post-asserts-output.smt2"
 
 # Stores then enabled output tags.
 [[option]]

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 90fd5847d5257e7322c96fe59158c35aa82e417e..01d6163054fba0c705bb07cfd45f582a45d956c4 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -339,6 +339,13 @@ bool ProcessAssertions::apply(Assertions& as)
   Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
   dumpAssertions("assertions::post-everything", as);
   Trace("assertions::post-everything") << std::endl;
+  if (isOutputOn(OutputTag::POST_ASSERTS))
+  {
+    std::ostream& outPA = d_env.output(OutputTag::POST_ASSERTS);
+    outPA << ";; post-asserts start" << std::endl;
+    dumpAssertionsToStream(outPA, as);
+    outPA << ";; post-asserts end" << std::endl;
+  }
 
   return noConflict;
 }
@@ -441,6 +448,15 @@ void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as)
   {
     return;
   }
+  std::stringstream ss;
+  dumpAssertionsToStream(ss, as);
+  Trace(key) << ";;; " << key << " start" << std::endl;
+  Trace(key) << ss.str();
+  Trace(key) << ";;; " << key << " end " << std::endl;
+}
+
+void ProcessAssertions::dumpAssertionsToStream(std::ostream& os, Assertions& as)
+{
   // Cannot print unless produce assertions is enabled. Otherwise, the printing
   // is misleading, since it does not capture what symbols were provided
   // as definitions.
@@ -478,11 +494,7 @@ void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as)
   {
     assertions.push_back(ap[i]);
   }
-  std::stringstream ss;
-  pb.printBenchmark(ss, logicInfo().getLogicString(), defs, assertions);
-  Trace(key) << ";;; " << key << " start" << std::endl;
-  Trace(key) << ss.str();
-  Trace(key) << ";;; " << key << " end " << std::endl;
+  pb.printBenchmark(os, logicInfo().getLogicString(), defs, assertions);
 }
 
 PreprocessingPassResult ProcessAssertions::applyPass(const std::string& pname,

diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 81ea9f4757f7f10e9b6577300d69c21de42a6c4e..4195e001eca8736d67b74c9bfd25af5caf010366 100644 (file)
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -111,6 +111,10 @@ class ProcessAssertions : protected EnvObj
    * assertions:`key` if it is enabled.
    */
   void dumpAssertions(const std::string& key, Assertions& as);
+  /**
+   * Dump assertions to stream os using the print benchmark utility.
+   */
+  void dumpAssertionsToStream(std::ostream& os, Assertions& as);
   /** apply pass */
   preprocessing::PreprocessingPassResult applyPass(const std::string& pass,
                                                    Assertions& as);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d2148bdfd956dd5e9c205652b7bd2117002887b8..f521e77eda65794758b56d178e471f876a914fdf 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -880,6 +880,7 @@ set(regress_0_tests
   regress0/printer/empty_symbol_name.smt2
   regress0/printer/learned-lit-output.smt2
   regress0/printer/let_shadowing.smt2
+  regress0/printer/post-asserts-output.smt2
   regress0/printer/print_subs.smt2
   regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc.smt2

diff --git a/test/regress/regress0/printer/post-asserts-output.smt2 b/test/regress/regress0/printer/post-asserts-output.smt2
new file mode 100644 (file)
index 0000000..d8fa3fc
--- /dev/null
+++ b/test/regress/regress0/printer/post-asserts-output.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -o post-asserts --produce-assertions
+; SCRUBBER: grep -E '\(assert'
+; EXPECT: (assert true)
+; EXPECT: (assert true)
+(set-logic ALL)
+(declare-fun x () Int)
+(assert (= x x))
+(check-sat)