diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-03 16:27:56 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-03 16:27:56 +0200 |
| commit | 58733b382a4a956c051d06e7318afa1deed612da (patch) | |
| tree | e41944879de5e7f1a06b1994731c9957d65acd3d /src/preprocessing/passes/bv_gauss.h | |
| parent | 337f8b791943e9b6b9a234f4f5422cf173342dd9 (diff) | |
Basic integration of arith::InferenceManager (#4999)
This PR adds a first basic integration of the arith::InferenceManager into the arithmetic theory and the nonlinear extension in particular.
While the lemma collection mechanism (in the nonlinear extension) remains unchanged, the lemmas are ultimately not directly pushed to the output channel but instead added to the inference manager. Additionally, we no longer use the cache within the nonlinear extension but instead rely on the inference manager.
This PR is based on #4960.
Diffstat (limited to 'src/preprocessing/passes/bv_gauss.h')
0 files changed, 0 insertions, 0 deletions