diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-16 11:57:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-16 11:57:59 -0500 |
| commit | 0534ea1bbee9a3a7049580449ab25025a4f92a9a (patch) | |
| tree | 1f514b1fc098baed3353728e0ce285899ed62565 /src/parser/antlr_input.cpp | |
| parent | 5557985d7320668b2625f1559f907488e2a85590 (diff) | |
Add buffered inference manager to TheorySep (#5038)
This makes TheorySep use a standard buffered inference manager. Notice the behavior in TheorySep::doPending was simplified to assert both facts and lemmas. Previously, this was doing something strange: if there were any lemmas, then both facts and lemmas would be processed as lemmas, otherwise the facts would be processed as facts. Notice that TheorySep currently does not use facts by default. This design can be addressed in the future.
Note this PR eliminates the need for a custom explain method in TheorySep.
Diffstat (limited to 'src/parser/antlr_input.cpp')
0 files changed, 0 insertions, 0 deletions