diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-24 19:08:41 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-24 19:08:41 -0600 |
| commit | 3ab0db55341e7e752411bb003fb203fcd9ec9120 (patch) | |
| tree | df79841a5e8244ea159ccc4a5e32c9e9d5fee2dc /src/theory/quantifiers/quant_util.h | |
| parent | bb095659fb12e3733a73f1be31769ff5b5eb6055 (diff) | |
(Refactor) Instantiate utility (#1387)
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index f958605b1..b1bba1842 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -167,14 +167,19 @@ public: /* reset * Called at the beginning of an instantiation round * Returns false if the reset failed. When reset fails, the utility should have - * added a lemma - * via a call to qe->addLemma. TODO: improve this contract #1163 + * added a lemma via a call to qe->addLemma. TODO: improve this contract #1163 */ virtual bool reset( Theory::Effort e ) = 0; /* Called for new quantifiers */ virtual void registerQuantifier(Node q) = 0; /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; + /** Check complete? + * + * Returns false if the utility's reasoning was globally incomplete + * (e.g. "sat" must be replaced with "incomplete"). + */ + virtual bool checkComplete() { return true; } }; /** Arithmetic utilities regarding monomial sums. |