summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/printer/smt2/smt2_printer.cpp7
-rw-r--r--src/printer/smt2/smt2_printer.h1
-rw-r--r--test/regress/regress0/decision/quant-ex1.disable_miniscope.smt21
-rw-r--r--test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect3
-rw-r--r--test/regress/regress0/quantifiers/array-unsat-simp3.smt21
-rw-r--r--test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect3
-rw-r--r--test/regress/regress0/quantifiers/bug291.smt21
-rw-r--r--test/regress/regress0/quantifiers/bug291.smt2.expect3
-rw-r--r--test/regress/regress0/quantifiers/ex1.smt21
-rw-r--r--test/regress/regress0/quantifiers/ex1.smt2.expect3
-rw-r--r--test/regress/regress0/quantifiers/ex7.smt21
-rw-r--r--test/regress/regress0/quantifiers/ex7.smt2.expect3
-rw-r--r--test/regress/regress0/tptp_parser5.p2
-rw-r--r--test/regress/regress0/tptp_parser6.p2
-rw-r--r--test/regress/regress0/tptp_parser7.p2
-rw-r--r--test/regress/regress0/tptp_parser8.p2
-rw-r--r--test/regress/regress0/tptp_parser9.p2
17 files changed, 28 insertions, 10 deletions
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
%--------------------------------------------------------------------------
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback