UF kinds documentation

diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index e99c3366cd9bd6a15a9fffc8d0b3a646313b03dc..ccdac32abf0dfef5ed3e7354937891f25c5a8918 100644 (file)
--- 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 128b8ceda343d316c01a23e9773613983ba3aa02..4f64da37e04e1a83bc93b43d65ba92a23c83f56c 100644 (file)
--- 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();
   }