diff options
| -rw-r--r-- | src/theory/datatypes/datatypes_rewriter.cpp | 78 | ||||
| -rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 11 | ||||
| -rw-r--r-- | src/theory/quantifiers/ematching/candidate_generator.cpp | 4 |
3 files changed, 54 insertions, 39 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index e0e2f7ac8..e41bef015 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -824,6 +824,45 @@ Node DatatypesRewriter::replaceDebruijn(Node n, return n; } +Node DatatypesRewriter::expandApplySelector(Node n) +{ + Assert(n.getKind() == APPLY_SELECTOR); + Node selector = n.getOperator(); + // APPLY_SELECTOR always applies to an external selector, cindexOf is + // legal here + size_t cindex = utils::cindexOf(selector); + const DType& dt = utils::datatypeOf(selector); + const DTypeConstructor& c = dt[cindex]; + Node selector_use; + TypeNode ndt = n[0].getType(); + if (options::dtSharedSelectors()) + { + size_t selectorIndex = utils::indexOf(selector); + Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl; + Assert(selectorIndex < c.getNumArgs()); + selector_use = c.getSelectorInternal(ndt, selectorIndex); + } + else + { + selector_use = selector; + } + NodeManager* nm = NodeManager::currentNM(); + Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]); + if (options::dtRewriteErrorSel()) + { + return sel; + } + Node tester = c.getTester(); + Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]); + SkolemManager* sm = nm->getSkolemManager(); + TypeNode tnw = nm->mkFunctionType(ndt, n.getType()); + Node f = sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector); + Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]); + Node ret = nm->mkNode(kind::ITE, tst, sel, sk); + Trace("dt-expand") << "Expand def : " << n << " to " << ret << std::endl; + return ret; +} + TrustNode DatatypesRewriter::expandDefinition(Node n) { NodeManager* nm = NodeManager::currentNM(); @@ -833,44 +872,7 @@ TrustNode DatatypesRewriter::expandDefinition(Node n) { case kind::APPLY_SELECTOR: { - Node selector = n.getOperator(); - // APPLY_SELECTOR always applies to an external selector, cindexOf is - // legal here - size_t cindex = utils::cindexOf(selector); - const DType& dt = utils::datatypeOf(selector); - const DTypeConstructor& c = dt[cindex]; - Node selector_use; - TypeNode ndt = n[0].getType(); - if (options::dtSharedSelectors()) - { - size_t selectorIndex = utils::indexOf(selector); - Trace("dt-expand") << "...selector index = " << selectorIndex - << std::endl; - Assert(selectorIndex < c.getNumArgs()); - selector_use = c.getSelectorInternal(ndt, selectorIndex); - } - else - { - selector_use = selector; - } - Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]); - if (options::dtRewriteErrorSel()) - { - ret = sel; - } - else - { - Node tester = c.getTester(); - Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]); - SkolemManager* sm = nm->getSkolemManager(); - TypeNode tnw = nm->mkFunctionType(ndt, n.getType()); - Node f = - sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector); - Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]); - ret = nm->mkNode(kind::ITE, tst, sel, sk); - Trace("dt-expand") << "Expand def : " << n << " to " << ret - << std::endl; - } + ret = expandApplySelector(n); } break; case APPLY_UPDATER: diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 89e1901fa..7ba3c9758 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -48,6 +48,17 @@ class DatatypesRewriter : public TheoryRewriter * on all top-level codatatype subterms of n. */ static Node normalizeConstant(Node n); + /** + * Expand an APPLY_SELECTOR term n, return its expanded form. If n is + * (APPLY_SELECTOR selC x) + * its expanded form is + * (ITE (APPLY_TESTER is-C x) + * (APPLY_SELECTOR_TOTAL selC' x) + * (f x)) + * where f is a skolem function with id SELECTOR_WRONG, and selC' is the + * internal selector function for selC (possibly a shared selector). + */ + static Node expandApplySelector(Node n); /** expand defintions */ TrustNode expandDefinition(Node n) override; diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 5295302c4..0fd5c21d5 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -14,11 +14,13 @@ */ #include "theory/quantifiers/ematching/candidate_generator.h" + #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" @@ -292,7 +294,7 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs, // NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when // expand definitions is eliminated, however, this also requires avoiding // term formula removal. - Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat); + Node mpatExp = datatypes::DatatypesRewriter::expandApplySelector(mpat); Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl; if (mpatExp.getKind() == ITE) { |