Add type to uninterpreted constant values (#8891)

Before
```smt2
(define-fun x () UInt (as @a_0 UInt))
(define-fun y () Atom (as @a_0 Atom))
```
After

```smt2
(define-fun x () UInt (as @UInt_0 UInt))
(define-fun y () Atom (as @Atom_0 Atom))
```

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6cf212d22e503586dc0e1d4c9b861c642d3189a9..f05825324e5455438aebc75a9b174861f5bf08a4 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -325,9 +325,9 @@ void Smt2Printer::toStream(std::ostream& out,
 
     case kind::UNINTERPRETED_SORT_VALUE:
     {
-      const UninterpretedSortValue& av = n.getConst<UninterpretedSortValue>();
+      const UninterpretedSortValue& v = n.getConst<UninterpretedSortValue>();
       std::stringstream ss;
-      ss << "(as " << av << " " << n.getType() << ")";
+      ss << "(as " << v << " " << n.getType() << ")";
       out << ss.str();
       break;
     }

diff --git a/src/util/uninterpreted_sort_value.cpp b/src/util/uninterpreted_sort_value.cpp
index 0e02d98c1c359b611a923697fc59a3e6669ebdd7..1ba2ebd232ebce7098ffff08bd6d3e0530effdc6 100644 (file)
--- a/src/util/uninterpreted_sort_value.cpp
+++ b/src/util/uninterpreted_sort_value.cpp
@@ -28,7 +28,7 @@ namespace cvc5::internal {
 
 std::ostream& operator<<(std::ostream& out, const UninterpretedSortValue& val)
 {
-  return out << "@a" << val.getIndex();
+  return out << "@" << val.getType() << "_" << val.getIndex();
 }
 
 UninterpretedSortValue::UninterpretedSortValue(const TypeNode& type,

diff --git a/test/regress/cli/regress0/models-print-2.smt2 b/test/regress/cli/regress0/models-print-2.smt2
index 2f4e94f83a3871dec2b923c43ffc59d3c1602bcb..03f666ee7275ee871db21bef3fe609c322fb85c8 100644 (file)
--- a/test/regress/cli/regress0/models-print-2.smt2
+++ b/test/regress/cli/regress0/models-print-2.smt2
@@ -1,9 +1,9 @@
-; the purpose of this test is to verify that there is a `as` term in the output.
-; the scrubber searches for "(as @a" patterns.
+; the purpose of this test is to verify that name of the uninterpreted sort appears in the constant output.
+; For example, if the sort is Sort0, then scrubber searches for "(as @Sort0_" patterns.
 
-; SCRUBBER: grep -o "(as @a"
-; EXPECT: (as @a
-; EXPECT: (as @a
+; SCRUBBER: grep -o "(as @Sort0_"
+; EXPECT: (as @Sort0_
+; EXPECT: (as @Sort0_
 (set-logic QF_UF)
 (set-option :produce-models true)
 (declare-sort Sort0 0)

diff --git a/test/regress/cli/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/cli/regress0/parser/issue6908-get-value-uc.smt2
index 722d4308efa334ecba1a49700860740a6e135eac..b241867e0410dd50e6a54a23c3d412125ba913f6 100644 (file)
--- a/test/regress/cli/regress0/parser/issue6908-get-value-uc.smt2
+++ b/test/regress/cli/regress0/parser/issue6908-get-value-uc.smt2
@@ -1,11 +1,11 @@
 ; DISABLE-TESTER: dump
 ; COMMAND-LINE: --produce-models
 ; EXPECT: sat
-; EXPECT: (((f (as @a0 Foo)) 3))
+; EXPECT: (((f (as @Foo_0 Foo)) 3))
 (set-logic ALL)
 (set-option :produce-models true)
 (declare-sort Foo 0)
 (declare-fun f (Foo) Int)
 (assert (exists ((x Foo)) (= (f x) 3)))
 (check-sat)
-(get-value ((f @a0)))
+(get-value ((f @Foo_0)))