Add output -o pre-asserts (#8270)

Analogous to -o post-asserts.

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 7c41e90b8bb72727ecd351342c721fe18e447adb..cd04406c1fd8bf052619e318e7b7611fa2f2e38a 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -200,9 +200,14 @@ name   = "Base"
   example-file = "regress0/printer/print_subs.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."
+  help = "print a benchmark corresponding to the assertions of the input problem after preprocessing"
+  description = "With ``-o post-asserts``, cvc5 prints a benchmark corresponding to the assertions of the input problem after preprocessing."
   example-file = "regress0/printer/post-asserts-output.smt2"
+[[option.mode.PRE_ASSERTS]]
+  name = "pre-asserts"
+  help = "print a benchmark corresponding to the assertions of the input problem before preprocessing"
+  description = "With ``-o pre-asserts``, cvc5 prints a benchmark corresponding to the assertions of the input problem before preprocessing."
+  example-file = "regress0/printer/pre-asserts-output.smt2"
 
 # Stores then enabled output tags.
 [[option]]

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 22a6bde98ba9c3be31b129081ce8e1301e268630..e6185dffc4e5dd2f42c8dd21c6ffbda28164e51f 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -98,6 +98,13 @@ bool ProcessAssertions::apply(Assertions& as)
   // Dump the assertions
   dumpAssertions("assertions::pre-everything", as);
   Trace("assertions::pre-everything") << std::endl;
+  if (isOutputOn(OutputTag::PRE_ASSERTS))
+  {
+    std::ostream& outPA = d_env.output(OutputTag::PRE_ASSERTS);
+    outPA << ";; pre-asserts start" << std::endl;
+    dumpAssertionsToStream(outPA, as);
+    outPA << ";; pre-asserts end" << std::endl;
+  }
 
   Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
   Trace("smt") << "ProcessAssertions::processAssertions()" << endl;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0ca6b0775bc998ea6268aef39f13e92ffb963146..fdbe1ed55c5f2bfff9938c64cb3f02bc0032e5cb 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -928,6 +928,7 @@ set(regress_0_tests
   regress0/printer/learned-lit-output.smt2
   regress0/printer/let_shadowing.smt2
   regress0/printer/post-asserts-output.smt2
+  regress0/printer/pre-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/pre-asserts-output.smt2 b/test/regress/regress0/printer/pre-asserts-output.smt2
new file mode 100644 (file)
index 0000000..209c5ba
--- /dev/null
+++ b/test/regress/regress0/printer/pre-asserts-output.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -o pre-asserts
+; SCRUBBER: grep -E '\(assert'
+; EXPECT: (assert (= x x))
+(set-logic ALL)
+(declare-fun x () Int)
+(assert (= x x))
+(check-sat)