diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-09 19:19:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-09 19:19:41 -0500 |
| commit | abc5af448a464615018c020c9ec6bb1e8dd4d48c (patch) | |
| tree | 009b0d971e8ffd4ad39e649cc6d7a6346ee98b2d /src/theory/theory_inference_manager.h | |
| parent | 3d181b9b308a24a4cec9bf949f457bc77515c1bc (diff) | |
Use state and inference manager in UF CardinalityExtension (#5036)
Previously, the cardinality extension of UF maintained its own (SAT-context-dependent) conflict flag, made custom calls to output channel, and maintained its own cache of lemmas. This standardizes the CardinalityExtension so that it uses state and inference manager of UF, which means that UF and the cardinality extension are fully syncronized concerning whether we are in a conflicting state at all times (d_state.isInConflict). It further cleans up some of the interfaces in CardinalityExtension. This required adding a forwarding method for setIncomplete in inference manager.
Diffstat (limited to 'src/theory/theory_inference_manager.h')
| -rw-r--r-- | src/theory/theory_inference_manager.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 496a7f0f1..e63d55366 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -341,6 +341,11 @@ class TheoryInferenceManager * Forward to OutputChannel::safePoint() to spend resources. */ void safePoint(ResourceManager::Resource r); + /** + * Notification from a theory that it realizes it is incomplete at + * this context level. + */ + void setIncomplete(); protected: /** |