From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 10 Mar 2022 20:41:26 +0000 (-0600)
Subject: Fix theoryOf call in get equality status (#8279)
X-Git-Tag: cvc5-1.0.0~285
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=84cb773e072548dffd24b570a01cb8aefc7112ac;p=cvc5.git

Fix theoryOf call in get equality status (#8279)

Should depend on uninterpreted sort owner.

Fixes cvc5/cvc5-projects#476.
---

diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
index 1399bac18..ee0fa5d5a 100644
--- a/src/theory/shared_solver_distributed.cpp
+++ b/src/theory/shared_solver_distributed.cpp
@@ -59,8 +59,10 @@ EqualityStatus SharedSolverDistributed::getEqualityStatus(TNode a, TNode b)
       return EQUALITY_FALSE_AND_PROPAGATED;
     }
   }
-  // otherwise, ask the theory
-  return d_te.theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
+  // otherwise, ask the theory, which may depend on the uninterpreted sort owner
+  TheoryId tid =
+      Theory::theoryOf(a.getType(), d_env.getUninterpretedSortOwner());
+  return d_te.theoryOf(tid)->getEqualityStatus(a, b);
 }
 
 TrustNode SharedSolverDistributed::explain(TNode literal, TheoryId id)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 30311558d..48c602a62 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2016,6 +2016,7 @@ set(regress_1_tests
   regress1/non-fatal-errors.smt2
   regress1/proj-issue175.smt2
   regress1/proj-issue406-diff-unsat-core.smt2
+  regress1/proj-issue476-theoryOf-no-uf.smt2
   regress1/proof00.smt2
   regress1/proofs/issue6625-unsat-core-proofs.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
diff --git a/test/regress/regress1/proj-issue476-theoryOf-no-uf.smt2 b/test/regress/regress1/proj-issue476-theoryOf-no-uf.smt2
new file mode 100644
index 000000000..2bb9d0bd9
--- /dev/null
+++ b/test/regress/regress1/proj-issue476-theoryOf-no-uf.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic QF_ADTNIA)
+(set-info :status sat)
+(declare-sort u 0)
+(declare-sort u1 0)
+(declare-datatypes ((d 3)) ((par (p _p p5) ((c (s u1)) (_c (_s p) (e p) (se u))))))
+(declare-const x u)
+(declare-const _x (d Int Int Int))
+(declare-const x4 (d u1 Int u))
+(declare-const x6 (d u Int u1))
+(assert (and (> (_s ((_ update se) _x x)) 0) (match ((_ update s) x6 (s x4)) (((_c _x64 _x65 _x66) (> (_s ((_ update se) _x x)) 0)) (_x67 true)))))
+(check-sat)