diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-27 21:24:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-27 21:24:16 -0500 |
commit | a0a969d7d65a778f2230ee920339541fdf380234 (patch) | |
tree | 2e8a3436a36a487f97b3bc75e473a68259fb145b /INSTALL.md | |
parent | 31f2135ad14b12e2ee9a24f5ca0da06cf5ed7b92 (diff) |
Add the buffered inference manager (#4954)
This class implements a highly common pattern of buffering facts and lemmas to send on the output channel. It is planned that the inference managers of strings, sets, datatypes, (non-linear) arithmetic, sep, quantifiers will inherit from this class.
This PR adds basic calls to add lemmas on the output channel from InferenceManager.
It introduces a Lemma virtual class which arith::nl::NlLemma and strings::InferInfo will inherit from.
This is required to begin refactoring a flexible configurable strategy for non-linear arithmetic, and will make it easier to further develop towards a configurable approach for theory combination.
Diffstat (limited to 'INSTALL.md')
0 files changed, 0 insertions, 0 deletions