diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-12 16:55:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-12 21:55:44 +0000 |
| commit | 76f495646c0e3a95f2474c5d746bc61ece18f89f (patch) | |
| tree | 5390007f4be229dfb18e641f34b9d9df6a9dea92 /src/theory/theory_model_builder.h | |
| parent | af398235ef9f3a909991fddbb71d43434d6cf3a1 (diff) | |
Fix computation of whether a type is finite (#6312)
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.
Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
Diffstat (limited to 'src/theory/theory_model_builder.h')
| -rw-r--r-- | src/theory/theory_model_builder.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 5652dc7ab..2ed8e2be6 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -299,9 +299,14 @@ class TheoryEngineModelBuilder bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m); //------------------------------------end for codatatypes + /** + * Is the given type constrained to be finite? This depends on whether + * finite model finding is enabled. + */ + bool isFiniteType(TypeNode tn) const; //---------------------------------for debugging finite model finding /** does type tn involve an uninterpreted sort? */ - bool involvesUSort(TypeNode tn); + bool involvesUSort(TypeNode tn) const; /** is v an excluded value based on uninterpreted sorts? * This gives an assertion failure in the case that v contains * an uninterpreted constant whose index is out of the bounds |