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 | |
| parent | 33324a13308886291d802d69a23993226d557d1a (diff) | |
UF kinds documentation
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/uf/kinds | 6 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 9 |
2 files changed, 12 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 diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 128b8ceda..4f64da37e 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -61,6 +61,9 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { if( check ) { + // don't care what it is, but it should be well-typed + n[0].getType(check); + TypeNode valType = n[1].getType(check); if( valType != nodeManager->integerType() ) { throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be integer"); @@ -85,6 +88,12 @@ public: if( valType != nodeManager->integerType() ) { throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be integer"); } + if( n[0].getKind()!=kind::CONST_RATIONAL ){ + throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be a constant"); + } + if( n[0].getConst<Rational>().getNumerator().sgn()!=1 ){ + throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be positive"); + } } return nodeManager->booleanType(); } |