From 9df2b70bac396301ac9c0586f60414033ba7f128 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 20 Jun 2014 19:59:42 -0400 Subject: [PATCH] UF kinds documentation --- src/theory/uf/kinds | 6 +++--- 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().getNumerator().sgn()!=1 ){ + throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be positive"); + } } return nodeManager->booleanType(); } -- 2.30.2