From b94fc449bd07c355cf95c0f6ff9281f880019ad3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Mar 2022 12:28:54 -0600 Subject: [PATCH] Add output -o pre-asserts (#8270) Analogous to -o post-asserts. --- src/options/base_options.toml | 9 +++++++-- src/smt/process_assertions.cpp | 7 +++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/printer/pre-asserts-output.smt2 | 7 +++++++ 4 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/printer/pre-asserts-output.smt2 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) -- 2.30.2