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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/theory_inference_manager.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index ff6f0ebc7..81f5c45e6 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -464,5 +464,7 @@ void TheoryInferenceManager::safePoint(ResourceManager::Resource r) d_out.safePoint(r); } +void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); } + } // namespace theory } // namespace CVC4 |