Fix for get-value with empty uninterpreted sort domain (#8547)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 4 Apr 2022 10:31:27 +0000 (05:31 -0500)
committerGitHub <noreply@github.com>
Mon, 4 Apr 2022 10:31:27 +0000 (03:31 -0700)
commit7841167c829fe524b350f7c1b05647e13aac59be
tree860ceaef2bdced59fe7a007534978cbe667a5a06
parent145f31d5d0df0019d2a3e6f09776b55bc5d5bffe
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.
src/parser/parser.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/theory_model.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2 [new file with mode: 0644]
test/regress/cli/regress0/models-print-2.smt2
test/regress/cli/regress0/printer/empty_sort.smt2