diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-24 11:42:08 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-24 11:42:08 -0600 |
| commit | 1d49bcb407777cf177620dac4d8e4df82f5e1122 (patch) | |
| tree | 00ea9256957d8547519b7164d10344d7313e56c8 /src/theory/theory_engine.cpp | |
| parent | 109e7e43efdeb557ff17880da83da438db35eb3e (diff) | |
Add interface for getting preprocessed term (#5798)
Several places, e.g. in quantifiers, requiring knowing what the theory-preprocessed form of a node is.
This is required for an improvement to our E-matching algorithm, which requires knowing what the preprocessed form of ground subterms of triggers are.
Note that I'm not 100% happy with adding a new interface to Valuation, but at the moment I don't see a better way of doing this. On the positive side, this interface will make a few other things (e.g. the return value of OutputChannel::lemma) obsolete.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5206ed7ae..27ae0018e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1174,6 +1174,11 @@ Node TheoryEngine::ensureLiteral(TNode n) { return d_propEngine->ensureLiteral(rewritten); } +Node TheoryEngine::getPreprocessedTerm(TNode n) +{ + Node rewritten = Rewriter::rewrite(n); + return d_propEngine->getPreprocessedTerm(rewritten); +} void TheoryEngine::printInstantiations( std::ostream& out ) { if( d_quantEngine ){ |