From 84cb773e072548dffd24b570a01cb8aefc7112ac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Mar 2022 14:41:26 -0600 Subject: [PATCH] Fix theoryOf call in get equality status (#8279) Should depend on uninterpreted sort owner. Fixes cvc5/cvc5-projects#476. --- src/theory/shared_solver_distributed.cpp | 6 ++++-- test/regress/CMakeLists.txt | 1 + .../regress1/proj-issue476-theoryOf-no-uf.smt2 | 13 +++++++++++++ 3 files changed, 18 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/proj-issue476-theoryOf-no-uf.smt2 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) -- 2.30.2