From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Wed, 22 Jun 2022 01:56:01 +0000 (-0500)
Subject: Add type to uninterpreted constant values (#8891)
X-Git-Tag: cvc5-1.0.1~45
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12ff8418d65db0ddbf53035100652d9f645d71fc;p=cvc5.git

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 6cf212d22..f05825324 100644
--- 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 0e02d98c1..1ba2ebd23 100644
--- 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 2f4e94f83..03f666ee7 100644
--- 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 722d4308e..b241867e0 100644
--- 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)))