From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Oct 2020 13:33:32 +0000 (-0500)
Subject: Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enabled. ... 
X-Git-Tag: cvc5-1.0.0~2724
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e93c443a0bfb1a66909e8467b24da399be3d01ac;p=cvc5.git

Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enabled. (#5248)

This ensures that arrays is not the owner of uninterpreted sorts if uf-ho or finite-model-find are enabled. In these cases, the UF solver implements special techniques (cardinality, ho reasoning) that should take priority.

Fixes #5233.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d9123e7f4..4402beba2 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -623,7 +623,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // If in arrays, set the UF handler to arrays
-  if (logic.isTheoryEnabled(THEORY_ARRAYS)
+  if (logic.isTheoryEnabled(THEORY_ARRAYS) && !options::ufHo()
+      && !options::finiteModelFind()
       && (!logic.isQuantified()
           || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1eca91a5a..3a6c60fb0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -559,6 +559,7 @@ set(regress_0_tests
   regress0/ho/hoa0008.smt2
   regress0/ho/issue4477.smt2
   regress0/ho/issue4990-care-graph.smt2
+  regress0/ho/issue5233-part1-usort-owner.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/match-middle.smt2
diff --git a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
new file mode 100644
index 000000000..e97b914a2
--- /dev/null
+++ b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: sat
+(set-logic QF_AUFBVLIA)
+(set-option :uf-ho true)
+(declare-fun a (Int) Int)
+(declare-fun b (Int) Int)
+(assert (distinct a b))
+(check-sat)