Add TheoryInference base class (#4990)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 1 Sep 2020 20:50:58 +0000 (15:50 -0500)
committerGitHub <noreply@github.com>
Tue, 1 Sep 2020 20:50:58 +0000 (15:50 -0500)
commit2add221570239ded0e9865be22d1cb1b4e7ef0b1
treeb096f3a369c0497ae78ccc7f7c685e9e0218f8c1
parent56b6eabba4202b8fb848c97b04e12f622eba411f
Add TheoryInference base class (#4990)

This introduces a TheoryInference base class, which is a generalization and cleaner version of the former Lemma object. This changes the name of Lemma -> SimpleTheoryLemma, and makes the callback responsible for calling the inference manager.

This PR also updates the datatypes inference manager to use the new style. This required adding some additional interfaces to TheoryInferenceManager.
src/CMakeLists.txt
src/theory/datatypes/inference_manager.cpp
src/theory/datatypes/inference_manager.h
src/theory/inference_manager_buffered.cpp
src/theory/inference_manager_buffered.h
src/theory/theory_inference.cpp [new file with mode: 0644]
src/theory/theory_inference.h [new file with mode: 0644]
src/theory/theory_inference_manager.cpp
src/theory/theory_inference_manager.h