Fix for get-value with empty uninterpreted sort domain (#8547)

Alternative for https://github.com/cvc5/cvc5/pull/8546.

We were mistakenly using `mkGroundTerm` instead of `mkGroundValue` to make the domain of an uninterpreted sort non-empty.

This ensures that get-value calls do not throw a spurious exception when there is a declared uninterpreted sort and there are no terms of that sort.

As a result, this also required fixing a few further issues regarding how uninterpreted sort constants are printed in models, and fixing the expected results on 2 more regressions.

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 5e82012dddaa3fbc1dd5925035b083fab3847d51..5bd4c1c9c0e17440b549b3cdc859c3b9b9047c9f 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -731,9 +731,19 @@ void Parser::pushGetValueScope()
   for (const cvc5::Sort& s : declareSorts)
   {
     std::vector<cvc5::Term> elements = d_solver->getModelDomainElements(s);
+    Trace("parser") << "elements for " << s << ":" << std::endl;
     for (const cvc5::Term& e : elements)
     {
-      defineVar(e.getUninterpretedSortValue(), e);
+      Trace("parser") << "  " << e.getKind() << " " << e << std::endl;
+      if (e.getKind() == Kind::UNINTERPRETED_SORT_VALUE)
+      {
+        defineVar(e.getUninterpretedSortValue(), e);
+      }
+      else
+      {
+        Assert(false)
+            << "model domain element is not an uninterpreted sort value: " << e;
+      }
     }
   }
 }

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2aab3d9806cdf1eb755bee7b7f4dcb8b6dc96961..f8f3af1b54822a70cd5563f9c1c28e4676a7bebf 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1403,15 +1403,27 @@ void Smt2Printer::toStreamModelSort(std::ostream& out,
   // print the representatives
   for (const Node& trn : elements)
   {
-    if (trn.isVar())
+    if (options::modelUninterpPrint()
+            == options::ModelUninterpPrintMode::DeclSortAndFun
+        || options::modelUninterpPrint()
+               == options::ModelUninterpPrintMode::DeclFun)
     {
-      if (options::modelUninterpPrint()
-              == options::ModelUninterpPrintMode::DeclSortAndFun
-          || options::modelUninterpPrint()
-                 == options::ModelUninterpPrintMode::DeclFun)
+      out << "(declare-fun ";
+      if (trn.getKind() == kind::UNINTERPRETED_SORT_VALUE)
       {
-        out << "(declare-fun " << trn << " () " << tn << ")" << endl;
+        // prints as raw symbol
+        const UninterpretedSortValue& av =
+            trn.getConst<UninterpretedSortValue>();
+        out << av;
       }
+      else
+      {
+        Assert(false)
+            << "model domain element is not an uninterpreted sort value: "
+            << trn;
+        out << trn;
+      }
+      out << " () " << tn << ")" << endl;
     }
     else
     {

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index c6962d171ac860caf50c841343bd327fd5c3fbe0..87c9ce21c16f3bc8aed062fbcf83fe9d997d7d86 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -118,8 +118,10 @@ std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const
   {
     // This is called when t is a sort that does not occur in this model.
     // Sorts are always interpreted as non-empty, thus we add a single element.
+    // We use mkGroundValue here, since domain elements must all be
+    // of UNINTERPRETED_SORT_VALUE kind.
     NodeManager* nm = NodeManager::currentNM();
-    elements.push_back(nm->mkGroundTerm(tn));
+    elements.push_back(nm->mkGroundValue(tn));
     return elements;
   }
   return *type_refs;

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index d6be8cafd15288a011ea41e38012bf365704a857..e40ee670e9f450c6aac436db8ed71a0c2745ecf4 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -490,6 +490,7 @@ set(regress_0_tests
   regress0/cvc3.userdoc.04.cvc.smt2
   regress0/cvc3.userdoc.05.cvc.smt2
   regress0/cvc3.userdoc.06.cvc.smt2
+  regress0/cvc5-printing.cpp-sample.smt2
   regress0/datatypes/4482-unc-simp-one.smt2
   regress0/datatypes/boolean-equality.cvc.smt2
   regress0/datatypes/boolean-terms-datatype.cvc.smt2

diff --git a/test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2 b/test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2
new file mode 100644 (file)
index 0000000..da362a2
--- /dev/null
+++ b/test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/((x.*//g'
+; EXPECT: unsat
+; EXPECT: sat
+(set-option :bv-print-consts-as-indexed-symbols true)
+(set-logic QF_AUFBV)
+(set-option :produce-models true)
+(set-option :incremental true)
+(set-option :produce-unsat-assumptions true)
+(declare-sort S 0)
+(declare-fun x () (_ BitVec 32))
+(declare-fun y () (_ BitVec 32))
+(declare-fun arr () (Array (_ BitVec 32) (_ BitVec 32)))
+(declare-fun f ((_ BitVec 32) ) S)
+(declare-fun s () S)
+(declare-fun ind1 () Bool)
+(push 1)
+(assert ind1)
+(assert (= ind1 (= (f x) s)))
+(assert (= (f x) s))
+(assert (not (=> (= x y) (= (select arr x) (select arr y)))))
+(check-sat-assuming (ind1 ))
+(pop 1)
+(check-sat)
+(get-value (x))

diff --git a/test/regress/cli/regress0/models-print-2.smt2 b/test/regress/cli/regress0/models-print-2.smt2
index 1e176d5c25d2d98cb151899a4a6ad797e7fc4568..286bbc13b5c6dcd29ae34b9c60b36c845d66363f 100644 (file)
--- a/test/regress/cli/regress0/models-print-2.smt2
+++ b/test/regress/cli/regress0/models-print-2.smt2
@@ -1,7 +1,8 @@
 ; 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'
+; SCRUBBER: sed -e 's/.*(as @.*/AS/; /sat/d; /cardinality/d; /rep/d; /^($/d; /^)$/d'
+; EXPECT: AS
 ; EXPECT: AS
 (set-logic QF_UF)
 (set-option :produce-models true)

diff --git a/test/regress/cli/regress0/printer/empty_sort.smt2 b/test/regress/cli/regress0/printer/empty_sort.smt2
index eb963e4435a00d2cd5cf78c7a3fdd8eaabf4047f..5c4ec7a9e1883bab6f7dd71892075aa9d31bc92a 100644 (file)
--- a/test/regress/cli/regress0/printer/empty_sort.smt2
+++ b/test/regress/cli/regress0/printer/empty_sort.smt2
@@ -1,7 +1,7 @@
 ; 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'
+; EXPECT: (declare-fun a () us_image)
+; EXPECT: (declare-fun a () ||)
+; SCRUBBER: sed -e '/declare-fun/!d; s/declare-fun [^[:space:]]*/declare-fun a/g'
 (set-option :produce-models true)
 (set-logic QF_UF)
 (declare-sort us_image 0)