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/smt | |
| 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/smt')
| -rw-r--r-- | src/smt/expand_definitions.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index c5080db81..d331e8e78 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -255,9 +255,10 @@ TrustNode ExpandDefs::expandDefinitions( // do not do any theory stuff if expandOnly is true theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node); + theory::TheoryRewriter* tr = t->getTheoryRewriter(); Assert(t != NULL); - TrustNode trn = t->expandDefinition(n); + TrustNode trn = tr->expandDefinition(n); if (!trn.isNull()) { node = trn.getNode(); |