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/quantifiers/instantiate.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/quantifiers/instantiate.h')
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index b3c056506..b56938fd1 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -117,7 +117,7 @@ class Instantiate : public QuantifiersUtil /** identify */ std::string identify() const override { return "Instantiate"; } /** check incomplete */ - bool checkComplete() override; + bool checkComplete(IncompleteId& incId) override; //--------------------------------------rewrite objects /** add instantiation rewriter */ |