From 0ec00cc244d20fd34e501db0b9d26aacc3a18405 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 15 Jan 2025 10:38:05 -0600 Subject: [PATCH] Fix --- src/smt/expand_definitions.cpp | 9 ++++++--- src/theory/datatypes/datatypes_rewriter.cpp | 2 ++ test/regress/cli/CMakeLists.txt | 1 + .../regress0/datatypes/proj-issue754-check-model.smt2 | 5 +++++ 4 files changed, 14 insertions(+), 3 deletions(-) create mode 100644 test/regress/cli/regress0/datatypes/proj-issue754-check-model.smt2 diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index d3e824915ae..37bbc189d95 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -79,13 +79,16 @@ 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 index aa3cba4b47c..49a3aac4e10 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -1096,7 +1096,9 @@ 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 index b0e0df062f4..1a19381df3d 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -734,6 +734,7 @@ set(regress_0_tests regress0/datatypes/proj-issue172.smt2 regress0/datatypes/proj-issue474-app-cons-value.smt2 regress0/datatypes/proj-issue578-clash-pf.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 new file mode 100644 index 00000000000..10909d05229 --- /dev/null +++ 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))))