From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 10 Mar 2022 18:28:54 +0000 (-0600)
Subject: Add output -o pre-asserts (#8270)
X-Git-Tag: cvc5-1.0.0~288
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b94fc449bd07c355cf95c0f6ff9281f880019ad3;p=cvc5.git

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 7c41e90b8..cd04406c1 100644
--- 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 22a6bde98..e6185dffc 100644
--- 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 0ca6b0775..fdbe1ed55 100644
--- 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
index 000000000..209c5ba97
--- /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)