SMT-LIBv2 compliance regarding outputting "unknown".

Thanks to Peter Collingbourne for the report, and the patch!

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8356f9e49edf45a8159b271a884351d3b5dd54bb..e41fd9c65513316f9aac5d14bf8d5ea126164471 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -590,6 +590,13 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type )
   }
 }
 
+void Smt2Printer::toStream(std::ostream& out, const Result& r) const throw() {
+  if (r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
+    out << "unknown";
+  } else {
+    Printer::toStream(out, r);
+  }
+}
 
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "(assert " << c->getExpr() << ")";

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 30c0ce647180b6d9f3110f5cecb447b5b2638f37..4754790959689eac64a718f7e1f68e9c5d24bf96 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -37,6 +37,7 @@ public:
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   //for models
   void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw();
+  void toStream(std::ostream& out, const Result& r) const throw();
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */

diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
index a8f4ff2b99a11e4361a646a654f7ad4ec0abb3f6..20230a6fa79ca11d641d1d16b02a066aeac7f497 100644 (file)
--- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
@@ -9,4 +9,5 @@
 (declare-fun p () Bool)
 (assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)

diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
index 9d5c95cdd0139bd9953ef2dfe04b6f97012b70aa..e2cc320e124bd553c4fe602749701569cc8a6926 100644 (file)
--- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
@@ -1,3 +1,4 @@
 % COMMAND-LINE: --decision=justification --disable-miniscope-quant-fv --disable-miniscope-quant
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0

diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2 b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
index 40e07ada77769d1df2adc553c1cf799582e5ccad..a16c9395d8a45a35b1c89b359b92313a00aa1a93 100644 (file)
--- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
+++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
@@ -18,4 +18,5 @@
 (assert (not (= i1 i2)))
 (assert (not (= (store_uf (store_uf a1 i1 e1) i2 e2) (store_uf (store_uf a1 i2 e2) i1 e1))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)

diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
index df24647ad33b5ad3e656844d110b54ef741bd887..2aefdcfc306d34a68148f7178aaaabf9080855cc 100644 (file)
--- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
+++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0

diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2
index dbc2305995240f1434de6ee5fdca10f351f76b8f..b39e415a827beb117cf901f7a3a45cd256804eee 100644 (file)
--- a/test/regress/regress0/quantifiers/bug291.smt2
+++ b/test/regress/regress0/quantifiers/bug291.smt2
@@ -10,4 +10,5 @@
 (declare-fun store2 (Int) Int)
 (assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A)) (select2 ?A)))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)

diff --git a/test/regress/regress0/quantifiers/bug291.smt2.expect b/test/regress/regress0/quantifiers/bug291.smt2.expect
index df24647ad33b5ad3e656844d110b54ef741bd887..2aefdcfc306d34a68148f7178aaaabf9080855cc 100644 (file)
--- a/test/regress/regress0/quantifiers/bug291.smt2.expect
+++ b/test/regress/regress0/quantifiers/bug291.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0

diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2
index a8f4ff2b99a11e4361a646a654f7ad4ec0abb3f6..20230a6fa79ca11d641d1d16b02a066aeac7f497 100644 (file)
--- a/test/regress/regress0/quantifiers/ex1.smt2
+++ b/test/regress/regress0/quantifiers/ex1.smt2
@@ -9,4 +9,5 @@
 (declare-fun p () Bool)
 (assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)

diff --git a/test/regress/regress0/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect
index df24647ad33b5ad3e656844d110b54ef741bd887..2aefdcfc306d34a68148f7178aaaabf9080855cc 100644 (file)
--- a/test/regress/regress0/quantifiers/ex1.smt2.expect
+++ b/test/regress/regress0/quantifiers/ex1.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0

diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2
index 0cac5ff54ae815601fd02ac2b287ee632bd75ffe..11a83fdc471f638d2665355c6bd64f0ec33609dc 100644 (file)
--- a/test/regress/regress0/quantifiers/ex7.smt2
+++ b/test/regress/regress0/quantifiers/ex7.smt2
@@ -9,4 +9,5 @@
 (declare-fun f (U) U)
 (assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b)))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)

diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect
index df24647ad33b5ad3e656844d110b54ef741bd887..2aefdcfc306d34a68148f7178aaaabf9080855cc 100644 (file)
--- a/test/regress/regress0/quantifiers/ex7.smt2.expect
+++ b/test/regress/regress0/quantifiers/ex7.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0

diff --git a/test/regress/regress0/tptp_parser5.p b/test/regress/regress0/tptp_parser5.p
index faacfdccc305bef4763ddad04c819c15f5fadd53..23ddf3e604663390ba644b6862b4df37d6b04f6a 100644 (file)
--- a/test/regress/regress0/tptp_parser5.p
+++ b/test/regress/regress0/tptp_parser5.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------

diff --git a/test/regress/regress0/tptp_parser6.p b/test/regress/regress0/tptp_parser6.p
index 0684a6a3d4e79560b1eec83df8aa288baaef1696..799bc4c6dd8969bd2463cc45f3cf70e3170c73e6 100644 (file)
--- a/test/regress/regress0/tptp_parser6.p
+++ b/test/regress/regress0/tptp_parser6.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------

diff --git a/test/regress/regress0/tptp_parser7.p b/test/regress/regress0/tptp_parser7.p
index ec90157e78f49bcbda333d115d42a3bd6d159abe..f87c3484ce0eac67cd59d0de0c287c5ca06ace65 100644 (file)
--- a/test/regress/regress0/tptp_parser7.p
+++ b/test/regress/regress0/tptp_parser7.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------

diff --git a/test/regress/regress0/tptp_parser8.p b/test/regress/regress0/tptp_parser8.p
index 3bfd8efb629d564ad539586bc56f0b9604f88d29..4bb2694ea38ab16e557346c5d161a1e973ff4a47 100644 (file)
--- a/test/regress/regress0/tptp_parser8.p
+++ b/test/regress/regress0/tptp_parser8.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------

diff --git a/test/regress/regress0/tptp_parser9.p b/test/regress/regress0/tptp_parser9.p
index dab8065b5968fc9405ff36178cbbe10f4a680556..bcbb8859864260d4f3a8f061de8f5478ed702695 100644 (file)
--- a/test/regress/regress0/tptp_parser9.p
+++ b/test/regress/regress0/tptp_parser9.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------