Fix theory mismatch in expand definitions (cvc5#11532)

Fixes a bug in our `--check-models` functionality where the wrong theory could be asked to expand a term. Fixes cvc5/cvc5-projects#754. Fixes cvc5/cvc5-projects#758. Fixes cvc5/cvc5-projects#759.
HanielB · Jan 21, 2025 · 02ed0ef · 02ed0ef
1 parent d5fddea
commit 02ed0ef
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 3 deletions.
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
@@ -79,13 +79,17 @@ Node ExpandDefs::expandDefinitions(TNode n,
         result.push(ret.isNull() ? n : ret);
         continue;
       }
-      theory::TheoryId tid = d_env.theoryOf(node);
+      // ensure rewritten
+      Node nr = rewrite(n);
+      // now get the appropriate theory
+      theory::TheoryId tid = d_env.theoryOf(nr);
       theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid);
 
       Assert(tr != NULL);
-      // ensure rewritten
-      Node nr = rewrite(n);
+      Trace("expand") << "Expand definition on " << nr << " (from " << n << ")"
+                      << std::endl;
       Node nre = tr->expandDefinition(nr);
+      Trace("expand") << "...returns " << nre << std::endl;
       node = nre.isNull() ? nr : nre;
       // the partial functions can fall through, in which case we still
       // consider their children

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -1096,7 +1096,10 @@ Node DatatypesRewriter::expandDefinition(Node n)
   {
     case Kind::APPLY_SELECTOR:
     {
+      Trace("dt-expand") << "expand selector, share sel = "
+                         << d_opts.datatypes.dtSharedSelectors << std::endl;
       ret = expandApplySelector(n, d_opts.datatypes.dtSharedSelectors);
+      Trace("dt-expand") << "...returns " << ret << std::endl;
     }
     break;
     case Kind::APPLY_UPDATER:

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -735,6 +735,7 @@ set(regress_0_tests
   regress0/datatypes/proj-issue474-app-cons-value.smt2
   regress0/datatypes/proj-issue578-clash-pf.smt2
   regress0/datatypes/proj-issue752-ipc.smt2
+  regress0/datatypes/proj-issue754-check-model.smt2
   regress0/datatypes/rec1.cvc.smt2
   regress0/datatypes/rec2.cvc.smt2
   regress0/datatypes/rec4.cvc.smt2

diff --git a/test/regress/cli/regress0/datatypes/proj-issue754-check-model.smt2 b/test/regress/cli/regress0/datatypes/proj-issue754-check-model.smt2
@@ -0,0 +1,5 @@
+; EXPECT: sat
+(set-logic QF_BVDT)
+(declare-datatypes ((d 0)) (((c) (_c (s Bool)))))
+(declare-const x d)
+(check-sat-assuming ((ite (s c) (s x) (s x))))