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/uf | |
| 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/uf')
| -rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 2 | ||||
| -rw-r--r-- | src/theory/uf/ho_extension.cpp | 2 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index eb6145f9c..6ba459452 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1432,7 +1432,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ // cardinality constraint from user input, set incomplete Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl; - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::UF_CARD_MODE); } } Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index ee3753e92..78171349d 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -227,7 +227,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) // are present if (hasFunctions) { - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED); } return 0; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9cb37a26d..e23bc0c45 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -177,7 +177,7 @@ bool TheoryUF::preNotifyFact( else { // support for cardinality constraints is not enabled, set incomplete - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED); } } // don't need to assert cardinality constraints if not producing models |