diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-05 08:03:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-05 13:03:33 +0000 |
| commit | dbf823ab9c0fa1ed3b5ab6e165625c3d3993d65f (patch) | |
| tree | b848b3f0d44b2643a250c27c83a4f0014f9741ab /src/theory/theory_engine.h | |
| parent | 698d244a00618a0399bce9e15eddef52f68b8c94 (diff) | |
Make buffered inference manager more robust to backtracking (#6833)
This makes TheoryEngine notify all theories when a theory sends a conflict. This means that buffered inference managers always clear their buffers when any theory sends a conflict.
This is required for making theories robust to conflicts that may arise when using the central equality engine, where a different theory may raise a conflict during another theory's check.
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f293a2cc8..cfcdcce13 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -193,6 +193,9 @@ class TheoryEngine { */ void conflict(TrustNode conflict, theory::TheoryId theoryId); + /** set in conflict */ + void markInConflict(); + /** * Debugging flag to ensure that shutdown() is called before the * destructor. |