From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 20 Jun 2014 23:59:42 +0000 (-0400)
Subject: UF kinds documentation
X-Git-Tag: cvc5-1.0.0~6727^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9df2b70bac396301ac9c0586f60414033ba7f128;p=cvc5.git

UF kinds documentation
---

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();
   }