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_engine.cpp | |
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_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0bcf1d19c..21c82e9eb 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -205,6 +205,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_qim.reset(); bool setIncomplete = false; + IncompleteId setIncompleteId = IncompleteId::QUANTIFIERS; Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; if( needsCheck ){ @@ -354,7 +355,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //sources of incompleteness for (QuantifiersUtil*& util : d_util) { - if (!util->checkComplete()) + if (!util->checkComplete(setIncompleteId)) { Trace("quant-engine-debug") << "Set incomplete because utility " << util->identify().c_str() @@ -372,7 +373,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //check if we should set the incomplete flag for (QuantifiersModule*& mdl : d_modules) { - if (!mdl->checkComplete()) + if (!mdl->checkComplete(setIncompleteId)) { Trace("quant-engine-debug") << "Set incomplete because module " @@ -447,7 +448,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ { if( setIncomplete ){ Trace("quant-engine") << "Set incomplete flag." << std::endl; - d_qim.setIncomplete(); + d_qim.setIncomplete(setIncompleteId); } //output debug stats d_qim.getInstantiate()->debugPrintModel(); |