diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 380e0896e..5172c1554 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -202,7 +202,14 @@ public: /** mark relevant quantified formula, this will indicate it should be checked before the others */ void markRelevant( Node q ); /** has added lemma */ - bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } + bool hasAddedLemma() const; + /** theory engine needs check + * + * This is true if the theory engine has more constraints to process. When + * it is false, we are tentatively going to terminate solving with + * sat/unknown. For details, see TheoryEngine::needCheck. + */ + bool theoryEngineNeedsCheck() const; /** is in conflict */ bool inConflict() { return d_conflict; } /** set conflict */ |