From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 12 Nov 2020 22:00:14 +0000 (-0800)
Subject: Models standard (#5415)
X-Git-Tag: cvc5-1.0.0~2605
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3db60fa3fba4787cc33a61c1a357c43ba1cc9d6d;p=cvc5.git

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 682b9ce75..d915ef44f 100644
--- 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 032d26511..feef73217 100644
--- 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 165de0dba..2b706478f 100644
--- 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 6e9ea4434..3682e06e6 100644
--- 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 90602e67d..f8cc084e6 100644
--- 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 6849b63a8..20b82690f 100644
--- 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 dbaad265f..7f7e3dbf2 100644
--- 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: )