diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-08 09:15:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-08 14:15:31 +0000 |
| commit | cd8fd2e4909513b4253ce8f9aa272eb87ae6bf83 (patch) | |
| tree | 713ef362a026a676363894277219a54658a9e05e /src/theory/theory_engine.h | |
| parent | 889daf13112f71b6f5dd98444af99ec7656195be (diff) | |
Add identifiers for sources of incompleteness (#6311)
This PR classifies all internal kinds of incompleteness as identifiers.
It makes it so TheoryEngine records an identifier when its incomplete flag is set.
The next step will be to possibly communicate this value to the user.
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 8960b324d..cc3de2e50 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -199,13 +199,14 @@ class TheoryEngine { * context level or below). */ context::CDO<bool> d_incomplete; + /** The theory and identifier that (most recently) set incomplete */ + context::CDO<theory::TheoryId> d_incompleteTheory; + context::CDO<theory::IncompleteId> d_incompleteId; /** * Called by the theories to notify that the current branch is incomplete. */ - void setIncomplete(theory::TheoryId theory) { - d_incomplete = true; - } + void setIncomplete(theory::TheoryId theory, theory::IncompleteId id); /** * Mapping of propagations from recievers to senders. |