From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 25 Jan 2022 19:50:50 +0000 (-0600)
Subject: Add output -o post-asserts (#7987)
X-Git-Tag: cvc5-1.0.0~504
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8e57b9025bcfffb1e3ecc9d7d6e7b36b62a15aa;p=cvc5.git

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 6a34978f5..6b7eaefb9 100644
--- 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 90fd5847d..01d616305 100644
--- 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 81ea9f475..4195e001e 100644
--- 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 d2148bdfd..f521e77ed 100644
--- 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
index 000000000..d8fa3fc88
--- /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)