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.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 65d4396a9edc217524b998062209e4dea7e7daea..2805d87939f052d72fea80fffb3febd882c50442 100644 (file)
--- 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 a9a9a29c33685522fcdad0e81109a53225a86d60..56a68ca4080caefe7543dcdf45c6aa120a8ba1b4 100644 (file)
--- 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 <typename T>
-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 804077186ab9303cb1f06931166406174795ee30..543fbd158a0917a661e12ce0d5e6939d4670b549 100644 (file)
--- 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 5a01e44f8f704ed973cb52e20396e64759b8576a..dabcaba8649126001a505af8d36f96eb09860276 100644 (file)
--- 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 (file)
index 0000000..7a8113d
--- /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)