From 12ff8418d65db0ddbf53035100652d9f645d71fc Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 21 Jun 2022 20:56:01 -0500 Subject: [PATCH] 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)) ``` --- src/printer/smt2/smt2_printer.cpp | 4 ++-- src/util/uninterpreted_sort_value.cpp | 2 +- test/regress/cli/regress0/models-print-2.smt2 | 10 +++++----- .../cli/regress0/parser/issue6908-get-value-uc.smt2 | 4 ++-- 4 files changed, 10 insertions(+), 10 deletions(-) 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(); + const UninterpretedSortValue& v = n.getConst(); 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))) -- 2.30.2