diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-20 19:59:42 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-20 20:01:28 -0400 |
| commit | 9df2b70bac396301ac9c0586f60414033ba7f128 (patch) | |
| tree | b7aa4e23385888f3562cae6a7b64509429fe6e0c /src/theory/uf/kinds | |
| parent | 33324a13308886291d802d69a23993226d557d1a (diff) | |
UF kinds documentation
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index e99c3366c..ccdac32ab 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -11,14 +11,14 @@ properties stable-infinite parametric properties check propagate ppStaticLearn presolve getNextDecisionRequest rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" -parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" +parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function" typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule -operator CARDINALITY_CONSTRAINT 2 "cardinality constraint" +operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S" typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule -operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint" +operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature" typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule endtheory |