Add buffered inference manager to TheorySep (#5038)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Sep 2020 16:57:59 +0000 (11:57 -0500)
committerGitHub <noreply@github.com>
Wed, 16 Sep 2020 16:57:59 +0000 (11:57 -0500)
commit0534ea1bbee9a3a7049580449ab25025a4f92a9a
tree1f514b1fc098baed3353728e0ce285899ed62565
parent5557985d7320668b2625f1559f907488e2a85590
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.
src/theory/sep/theory_sep.cpp
src/theory/sep/theory_sep.h