diff options
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index a1fcac1df..d7f542038 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,15 +6,22 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" -properties stable-infinite check propagate staticLearning presolve +properties stable-infinite +properties check propagate staticLearning presolve notifyRestart rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" -sort KIND_TYPE "Uninterpreted Sort" +# Justified because we can have an unbounded-but-finite number of +# sorts. Assuming we have |Z| is probably ok for now.. +sort KIND_TYPE Cardinality::INTEGERS "Uninterpreted Sort" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" variable SORT_TAG "sort tag" parameterized SORT_TYPE SORT_TAG 0: "sort type" +# This is really "unknown" cardinality, but maybe this will be good +# enough (for now) ? Once we support quantifiers, maybe reconsider +# this.. +cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" -endtheory
\ No newline at end of file +endtheory |