From 94e3d283a58684118e06f9a698606e58574fa26f Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 13 Aug 2018 18:03:54 -0700 Subject: [PATCH] Fix get-unsat-assumptions output (#2301) Fixes #2298. The `get-unsat-assumptions` command was printing the result with square brackets and commas instead of parentheses and spaces between the assumptions. --- src/smt/command.cpp | 3 ++- src/util/utility.h | 12 ++++++++---- test/regress/Makefile.tests | 3 ++- .../regress0/push-pop/bug821-check_sat_assuming.smt2 | 4 ++-- .../regress0/smtlib/get-unsat-assumptions.smt2 | 12 ++++++++++++ 5 files changed, 26 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/smtlib/get-unsat-assumptions.smt2 diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 65d4396a9..2805d8793 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -35,6 +35,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "util/sexpr.h" +#include "util/utility.h" using namespace std; @@ -1873,7 +1874,7 @@ void GetUnsatAssumptionsCommand::printResult(std::ostream& out, } else { - out << d_result << endl; + container_to_stream(out, d_result, "(", ")\n", " "); } } diff --git a/src/util/utility.h b/src/util/utility.h index a9a9a29c3..56a68ca40 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -69,16 +69,20 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre } template -void container_to_stream(std::ostream& out, const T& container) +void container_to_stream(std::ostream& out, + const T& container, + const char* prefix = "[", + const char* postfix = "]", + const char* sep = ", ") { - out << "["; + out << prefix; bool is_first = true; for (const auto& item : container) { - out << (!is_first ? ", " : "") << item; + out << (!is_first ? sep : "") << item; is_first = false; } - out << "]"; + out << postfix; } }/* CVC4 namespace */ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 804077186..543fbd158 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -239,9 +239,9 @@ REG0_TESTS = \ regress0/bv/core/slice-18.smt \ regress0/bv/core/slice-19.smt \ regress0/bv/core/slice-20.smt \ - regress0/bv/eager-inc-cryptominisat.smt2 \ regress0/bv/divtest_2_5.smt2 \ regress0/bv/divtest_2_6.smt2 \ + regress0/bv/eager-inc-cryptominisat.smt2 \ regress0/bv/fuzz01.smt \ regress0/bv/fuzz02.delta01.smt \ regress0/bv/fuzz02.smt \ @@ -786,6 +786,7 @@ REG0_TESTS = \ regress0/simplification_bug2.smt \ regress0/smallcnf.cvc \ regress0/smt2output.smt2 \ + regress0/smtlib/get-unsat-assumptions.smt2 \ regress0/strings/bug001.smt2 \ regress0/strings/bug002.smt2 \ regress0/strings/bug612.smt2 \ diff --git a/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 index 5a01e44f8..dabcaba86 100644 --- a/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 +++ b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 @@ -7,8 +7,8 @@ (check-sat-assuming (_substvar_4_ false)) ; EXPECT: unsat (get-unsat-assumptions) -; EXPECT: [false] +; EXPECT: (false) (check-sat-assuming ((= _substvar_4_ _substvar_4_) (distinct _substvar_4_ _substvar_4_))) ; EXPECT: unsat (get-unsat-assumptions) -; EXPECT: [(distinct _substvar_4_ _substvar_4_)] +; EXPECT: ((distinct _substvar_4_ _substvar_4_)) diff --git a/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 new file mode 100644 index 000000000..7a8113d8f --- /dev/null +++ b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 @@ -0,0 +1,12 @@ +; EXPECT: unsat +; EXPECT: (x x) +; SCRUBBER: sed -e 's/a[1-2]/x/g' +(set-option :produce-unsat-assumptions true) +(set-logic QF_LIA) +(declare-const a1 Bool) +(declare-const a2 Bool) +(declare-const x Int) +(assert (= a1 (= x 5))) +(assert (= a2 (not (= x 5)))) +(check-sat-assuming (a1 a2)) +(get-unsat-assumptions) -- 2.30.2