diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-21 21:42:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-22 02:42:08 +0000 |
| commit | 89620a0d73e7134437a39d742e91de11a08a4962 (patch) | |
| tree | 46b37970a7d3f74317f8e255b6aefa9cfae127b1 /src/theory/sets | |
| parent | 90cde45ee963b994054f96f97111684cce808d82 (diff) | |
Move expand definition from Theory to TheoryRewriter (#6408)
This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.
The next step will be to add Rewriter::expandDefinition.
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/theory_sets.cpp | 6 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets.h | 2 |
2 files changed, 0 insertions, 8 deletions
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index fdb744d67..8406bd14a 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -131,12 +131,6 @@ void TheorySets::preRegisterTerm(TNode node) d_internal->preRegisterTerm(node); } -TrustNode TheorySets::expandDefinition(Node n) -{ - // we currently do not expand any set operators - return TrustNode::null(); -} - TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems) { Kind nk = n.getKind(); diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index bb8741e35..e99d25d36 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -78,8 +78,6 @@ class TheorySets : public Theory Node getModelValue(TNode) override; std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; - /** Expand partial operators (choose) from n. */ - TrustNode expandDefinition(Node n) override; /** * If the sets-ext option is not set and we have an extended operator, * we throw an exception. Additionally, we expand operators like choose |