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/printer | |
| 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/printer')
0 files changed, 0 insertions, 0 deletions