From 8994bc9fd49a255286f8a6bac6c14407e8add41f Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 3 Dec 2020 12:18:10 -0800
Subject: Models as (#5581)

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

delete the model keyword (done in #5415 )
avoid printing extra declarations by default (done in #5432 )
wrap UF values with as expressions.
This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.
---
 src/options/smt_options.toml                  |  8 ++++++--
 src/printer/smt2/smt2_printer.cpp             | 13 ++++++++++---
 test/regress/CMakeLists.txt                   |  2 ++
 test/regress/regress0/models-print-1.smt2     | 10 ++++++++++
 test/regress/regress0/models-print-2.smt2     | 11 +++++++++++
 test/regress/regress0/printer/empty_sort.smt2 |  1 +
 6 files changed, 40 insertions(+), 5 deletions(-)
 create mode 100644 test/regress/regress0/models-print-1.smt2
 create mode 100644 test/regress/regress0/models-print-2.smt2

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 405abfc4f..08d53855c 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -417,7 +417,7 @@ header = "options/smt_options.h"
   category   = "regular"
   long       = "model-u-print=MODE"
   type       = "ModelUninterpPrintMode"
-  default    = "DeclFun"
+  default    = "None"
   read_only  = true
   help       = "determines how to print uninterpreted elements in models"
   help_mode  = "uninterpreted elements in models printing  modes."
@@ -429,7 +429,11 @@ header = "options/smt_options.h"
   help = "print uninterpreted elements declare-fun, and also include a declare-sort for the sort"
 [[option.mode.DeclFun]]
   name = "decl-fun"
-  help = "(default) print uninterpreted elements declare-fun, but don't include a declare-sort for the sort"
+  help = "print uninterpreted elements declare-fun, but don't include a declare-sort for the sort"
+[[option.mode.None]]
+  name = "none"
+  help = "(default) do not print declarations of uninterpreted elements in models."
+
 
 [[option]]
   name       = "modelWitnessValue"
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6f03553ae..376913ebd 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -309,8 +309,8 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::UNINTERPRETED_CONSTANT: {
       const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
       std::stringstream ss;
-      ss << '@' << uc;
-      out << CVC4::quoteSymbol(ss.str());
+      ss << "(as @" << uc << " " << n.getType() << ")";
+      out << ss.str();
       break;
     }
 
@@ -1403,7 +1403,14 @@ void Smt2Printer::toStreamModelSort(std::ostream& out,
   {
     if (trn.isVar())
     {
-      out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")" << endl;
+      if (options::modelUninterpPrint()
+              == options::ModelUninterpPrintMode::DeclSortAndFun
+          || options::modelUninterpPrint()
+                 == options::ModelUninterpPrintMode::DeclFun)
+      {
+        out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")"
+            << endl;
+      }
     }
     else
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5ab1cd6c2..4145c0e27 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -613,6 +613,8 @@ set(regress_0_tests
   regress0/logops.04.cvc
   regress0/logops.05.cvc
   regress0/model-core.smt2
+  regress0/models-print-1.smt2
+  regress0/models-print-2.smt2
   regress0/named-expr-use.smt2
   regress0/nl/coeff-sat.smt2
   regress0/nl/ext-rew-aggr-test.smt2
diff --git a/test/regress/regress0/models-print-1.smt2 b/test/regress/regress0/models-print-1.smt2
new file mode 100644
index 000000000..974c1f774
--- /dev/null
+++ b/test/regress/regress0/models-print-1.smt2
@@ -0,0 +1,10 @@
+; the purpose of this test is to verify that there are no redundant `declare-fun`s
+
+; EXIT: 0  
+; SCRUBBER: grep declare-fun
+(set-logic QF_UF)
+(set-option :produce-models true)
+(declare-sort Sort0 0)
+(declare-fun f1 (Sort0) Bool)
+(check-sat)
+(get-model)
diff --git a/test/regress/regress0/models-print-2.smt2 b/test/regress/regress0/models-print-2.smt2
new file mode 100644
index 000000000..1e176d5c2
--- /dev/null
+++ b/test/regress/regress0/models-print-2.smt2
@@ -0,0 +1,11 @@
+; the purpose of this test is to verify that there is a `as` term in the output.
+; the scrubber excludes all lines without "(as @", and replaces this pattern by "AS".
+
+; SCRUBBER: sed -e 's/.*(as @.*/AS/; /sat/d; /cardinality/d; /^($/d; /^)$/d'
+; EXPECT: AS
+(set-logic QF_UF)
+(set-option :produce-models true)
+(declare-sort Sort0 0)
+(declare-fun f1 () Sort0)
+(check-sat)
+(get-model)
diff --git a/test/regress/regress0/printer/empty_sort.smt2 b/test/regress/regress0/printer/empty_sort.smt2
index efe68e920..eb963e443 100644
--- a/test/regress/regress0/printer/empty_sort.smt2
+++ b/test/regress/regress0/printer/empty_sort.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --model-u-print=decl-fun
 ; EXPECT: (declare-fun gt () us_image)
 ; EXPECT: (declare-fun gt () ||)
 ; SCRUBBER: sed -e '/declare-fun/!d; s/declare-fun [^[:space:]]*/declare-fun gt/g'
-- 
cgit v1.2.3