From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 16 Dec 2021 21:07:55 +0000 (-0600)
Subject: Fix get-model when sort constructors are present (#7828)
X-Git-Tag: cvc5-1.0.0~651
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c21537af09a451e57cb6251ebba2c20c69cf612;p=cvc5.git

Fix get-model when sort constructors are present (#7828)

Fixes a spurious error on kind benchmarks.

Note that we don't properly handle instantiated sort constructors currently, which I believe need to be handled as declared sorts when calling getModel.
---

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 7cd475cbb..1321c558e 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1231,8 +1231,12 @@ size_t DeclareSortCommand::getArity() const { return d_arity; }
 api::Sort DeclareSortCommand::getSort() const { return d_sort; }
 void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
-  // mark that it will be printed in the model
-  sm->addModelDeclarationSort(d_sort);
+  // mark that it will be printed in the model, if it is an uninterpreted
+  // sort (arity 0)
+  if (d_arity == 0)
+  {
+    sm->addModelDeclarationSort(d_sort);
+  }
   d_commandStatus = CommandSuccess::instance();
 }
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4addbd8d1..4d8a7a65f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -806,6 +806,7 @@ set(regress_0_tests
   regress0/parser/define_sort.smt2
   regress0/parser/force_logic_set_logic.smt2
   regress0/parser/force_logic_success.smt2
+  regress0/parser/get-model-sort-constructor.smt2
   regress0/parser/issue5163.smt2
   regress0/parser/issue6908-get-value-uc.smt2
   regress0/parser/issue7274.smt2
diff --git a/test/regress/regress0/parser/get-model-sort-constructor.smt2 b/test/regress/regress0/parser/get-model-sort-constructor.smt2
new file mode 100644
index 000000000..4f40e3448
--- /dev/null
+++ b/test/regress/regress0/parser/get-model-sort-constructor.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: )
+(set-option :produce-models true)
+(set-logic QF_UFLIRA)
+(declare-sort FArray 2)
+(check-sat)
+(get-model)