Model declarations printing options (#5432)

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 is step 2. It allows the user to choose the model printing style in case of uninterpreted elements: either using datatypes, or using declare-sorts and declare-funs or just using declare-funs.

The default option, which is closest to the standard, is just using declare-funs. In step 3, these will be replaced by abstract values using as.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 54d81eba6caf15330523a6cd9d21535ebadc0143..55ba43ce9bb568bf00fef7eeb89f33d4697e4ce0 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -412,13 +412,24 @@ header = "options/smt_options.h"
   help       = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard"
 
 [[option]]
-  name       = "modelUninterpDtEnum"
-  category   = "regular"
-  long       = "model-u-dt-enum"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "in models, output uninterpreted sorts as datatype enumerations"
+  name       = "modelUninterpPrint"
+  smt_name   = "model-uninterp-print"
+  category   = "regular"
+  long       = "model-u-print=MODE"
+  type       = "ModelUninterpPrintMode"
+  default    = "DeclFun"
+  read_only  = true
+  help       = "determines how to print uninterpreted elements in models"
+  help_mode  = "uninterpreted elements in models printing  modes."
+[[option.mode.DtEnum]]
+  name = "dtenum"
+  help = "print uninterpreted elements as datatype enumerations, where the sort is the datatype"
+[[option.mode.DeclSortAndFun]]
+  name = "decl-sort-and-fun"
+  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"
 
 [[option]]
   name       = "modelWitnessValue"

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 236c87b91876a2d648c1ccf16261ebc2a0a83ee9..8b252d0eaea384f5db9597a09276bd9833a4cd3f 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1076,8 +1076,8 @@ void DeclareTypeNodeCommandToStream(std::ostream& out,
   TypeNode type_node = command.getType();
   const std::vector<Node>* type_reps =
       model.getRepSet()->getTypeRepsOrNull(type_node);
-  if (options::modelUninterpDtEnum() && type_node.isSort()
-      && type_reps != nullptr)
+  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
+      && type_node.isSort() && type_reps != nullptr)
   {
     out << "DATATYPE" << std::endl;
     out << "  " << command.getSymbol() << " = ";
@@ -1147,7 +1147,8 @@ void DeclareFunctionNodeCommandToStream(
   // We get the value from the theory model directly, which notice
   // does not have to go through the standard SmtEngine::getValue interface.
   Node val = model.getValue(n);
-  if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE)
+  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
+      && val.getKind() == kind::STORE)
   {
     TypeNode type_node = val[1].getType();
     if (tn.isSort())

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index feef7321756116131b75e7ebb839a1accfe3ecc4..d44842633a7b1603e12ead742ea240ebc2e6ef98 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1365,7 +1365,8 @@ void Smt2Printer::toStream(std::ostream& out,
     else
     {
       std::vector<Node> elements = theory_model->getDomainElements(tn);
-      if (options::modelUninterpDtEnum())
+      if (options::modelUninterpPrint()
+          == options::ModelUninterpPrintMode::DtEnum)
       {
         if (isVariant_2_6(d_variant))
         {
@@ -1385,7 +1386,11 @@ void Smt2Printer::toStream(std::ostream& out,
       {
         // print the cardinality
         out << "; cardinality of " << tn << " is " << elements.size() << endl;
-        out << (*dtc) << endl;
+        if (options::modelUninterpPrint()
+            == options::ModelUninterpPrintMode::DeclSortAndFun)
+        {
+          out << (*dtc) << endl;
+        }
         // print the representatives
         for (const Node& trn : elements)
         {
@@ -1432,7 +1437,9 @@ void Smt2Printer::toStream(std::ostream& out,
     }
     else
     {
-      if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE)
+      if (options::modelUninterpPrint()
+              == options::ModelUninterpPrintMode::DtEnum
+          && val.getKind() == kind::STORE)
       {
         TypeNode tn = val[1].getType();
         const std::vector<Node>* type_refs =