Models standard (#5415)

This PR relates to #4987 .
Our plan is to:

delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR does step 1, and fixes regressions accordingly.

diff --git a/NEWS b/NEWS
index 682b9ce757ba18d564a738480e5fd4245c2ea56d..d915ef44fa010782482da4a431bc7e9f5d16e79c 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -34,6 +34,9 @@ Changes:
   now restrict bvxnor to only allow two operands in order to avoid confusion
   about the semantics, since the behavior of n-ary operands to bvxnor is now
   undefined in SMT-LIB.
+* SMT-LIB output for `get-model` command now conforms with the standard,
+  and does *not* begin with the keyword `model`. The output
+  is the same as before, only with this word removed from the beginning.
 
 
 Changes since 1.7

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 032d265112664b314273b7736edbde854c2f97d2..feef7321756116131b75e7ebb839a1accfe3ecc4 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1330,7 +1330,7 @@ void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
     out << "; " << ln << std::endl;
   }
   //print the model
-  out << "(model" << endl;
+  out << "(" << endl;
   // don't need to print approximations since they are built into choice
   // functions in the values of variables.
   this->Printer::toStream(out, m);

diff --git a/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2
index 165de0dbae2f243a80562f042fb8476116045271..2b706478fbba918c0af51f1e2fe38daa09412a37 100644 (file)
--- a/test/regress/regress0/datatypes/dt-param-2.6-print.smt2
+++ b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: (model
+; EXPECT: (
 ; EXPECT: (declare-datatypes ((Pair 2)) ((par (X Y)((mkPair (first X) (second Y))))))
 ; EXPECT: (define-fun x () (Pair Int Real) ((as mkPair (Pair Int Real)) 2 (/ 3 2)))
 ; EXPECT: )

diff --git a/test/regress/regress0/parser/strings20.smt2 b/test/regress/regress0/parser/strings20.smt2
index 6e9ea4434fab5d0930a1b45712bbc3e6d633c8f3..3682e06e640c6a173393a733e1f43888da3c24c1 100644 (file)
--- a/test/regress/regress0/parser/strings20.smt2
+++ b/test/regress/regress0/parser/strings20.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: (model
+; EXPECT: (
 ; EXPECT: (define-fun s () String "\"")
 ; EXPECT: )
 

diff --git a/test/regress/regress0/parser/strings25.smt2 b/test/regress/regress0/parser/strings25.smt2
index 90602e67dbf1d5bf0661165c251635f214b9d36f..f8cc084e67fcd648ba17245ce0d7aeaa608dd96a 100644 (file)
--- a/test/regress/regress0/parser/strings25.smt2
+++ b/test/regress/regress0/parser/strings25.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: (model
+; EXPECT: (
 ; EXPECT: (define-fun s () String """")
 ; EXPECT: )
 

diff --git a/test/regress/regress0/simple-dump-model.smt2 b/test/regress/regress0/simple-dump-model.smt2
index 6849b63a88838344fc3bf3b2924cc6e7ec372666..20b82690f780598337e913bd55bd0ac5417a4733 100644 (file)
--- a/test/regress/regress0/simple-dump-model.smt2
+++ b/test/regress/regress0/simple-dump-model.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --dump-models
 ; EXPECT: sat
-; EXPECT: (model
+; EXPECT: (
 ; EXPECT: (define-fun x () Int 1)
 ; EXPECT: (define-fun y () Int 1)
 ; EXPECT: )

diff --git a/test/regress/regress0/smt2output.smt2 b/test/regress/regress0/smt2output.smt2
index dbaad265f3bcb16dbc67ca0a0fc127c61f357e00..7f7e3dbf2d65c5d6803e2e5c31f0b852121261e1 100644 (file)
--- a/test/regress/regress0/smt2output.smt2
+++ b/test/regress/regress0/smt2output.smt2
@@ -8,7 +8,7 @@
 (check-sat)
 ; EXPECT: sat
 (get-model)
-; EXPECT: (model
+; EXPECT: (
 ; EXPECT: (define-fun toto () Bool true)
 ; EXPECT: (define-fun |to to| () Bool true)
 ; EXPECT: )