From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 18 Sep 2012 14:50:45 +0000 (+0000)
Subject: SMT-LIBv2 compliance regarding outputting "unknown".
X-Git-Tag: cvc5-1.0.0~7802
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=283822d8dc26004cd5b15a5b8e198d4f3068ebd0;p=cvc5.git

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 8356f9e49..e41fd9c65 100644
--- 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 30c0ce647..475479095 100644
--- 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 a8f4ff2b9..20230a6fa 100644
--- 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 9d5c95cdd..e2cc320e1 100644
--- 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 40e07ada7..a16c9395d 100644
--- 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 df24647ad..2aefdcfc3 100644
--- 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 dbc230599..b39e415a8 100644
--- 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 df24647ad..2aefdcfc3 100644
--- 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 a8f4ff2b9..20230a6fa 100644
--- 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 df24647ad..2aefdcfc3 100644
--- 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 0cac5ff54..11a83fdc4 100644
--- 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 df24647ad..2aefdcfc3 100644
--- 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 faacfdccc..23ddf3e60 100644
--- 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 0684a6a3d..799bc4c6d 100644
--- 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 ec90157e7..f87c3484c 100644
--- 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 3bfd8efb6..4bb2694ea 100644
--- 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 dab8065b5..bcbb88598 100644
--- 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
 
 %--------------------------------------------------------------------------