From e951bcab2f4d2c19557b8af8eb8f925ffe718ee8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 19:09:54 -0600 Subject: [PATCH] Document type rules (#8248) Fixes cvc5/cvc5-projects#272. Fixes cvc5/cvc5-projects#270. Fixes cvc5/cvc5-projects#269. Fixes cvc5/cvc5-projects#268. Also makes a few minor internal fixes to type rules. --- .../datatypes/theory_datatypes_type_rules.h | 81 +++++++++++++++++++ .../theory_quantifiers_type_rules.h | 32 ++++++++ src/theory/sep/theory_sep_type_rules.h | 26 ++++++ src/theory/uf/theory_uf_type_rules.cpp | 11 +-- src/theory/uf/theory_uf_type_rules.h | 39 +++++++-- 5 files changed, 173 insertions(+), 16 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 3b1276221..5ad325c6a 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -25,25 +25,56 @@ namespace cvc5 { namespace theory { namespace datatypes { +/** + * A constructor is associated with a type (-> T1 ... Tn T). The type rule + * for constructors ensures that the arguments are T1 ... Tn and returns T. + * If the constructor is for a parametric datatype, the above is generalized + * so that the arguments of type S1 ... Sn are specializations of T1 ... Tn + * for type substitution sigma, and returns T * sigma. + */ struct DatatypeConstructorTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); + /** + * A constructor term is constant if it is an AST built from constructor + * terms only. This check is computed recursively on n. + */ static bool computeIsConst(NodeManager* nodeManager, TNode n); }; +/** + * A selector is associated with a type (-> T1 T2). The type rule + * for selectors ensures that the argument is T1 and returns T2. + * This rule is generalized for parametric datatypes. + */ struct DatatypeSelectorTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * A tester is associated with a type (-> T1 Bool). The type rule + * for testers ensures that the argument is T1 and returns Bool. + * This rule is generalized for parametric datatypes. + */ struct DatatypeTesterTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * An updater is associated with a selector of type (-> T1 T2). The type + * rule for updaters expects arguments of type T1 and T2 and returns T1. + * This rule is generalized for parametric datatypes. + */ struct DatatypeUpdateTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * APPLY_TYPE_ASCRIPTION is a dummy kind to specialize the type of a datatype + * constructor, e.g., (as nil (List Int)). The type rule returns the ascribed + * type. + */ struct DatatypeAscriptionTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); @@ -54,46 +85,96 @@ struct ConstructorProperties static Cardinality computeCardinality(TypeNode type); }; +/** + * The datatype size function expects any datatype and returns the integer type. + */ class DtSizeTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * The datatype bound predicate expects any datatype, a constant integer, and + * returns the Boolean type. + */ class DtBoundTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * The type rule for sygus evaluation functions. DT_SYGUS_EVAL expects + * (1) a term of SyGuS datatype type T, whose SyGuS variable list is (x1 ... + * xn), (2) terms t1 ... tn whose types are the same as x1 ... xn. The returned + * type is the builtin type associated with T. + */ class DtSygusEvalTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * The type rule for match. Recall that a match term: + * (match l (((cons h t) h) (nil 0))) + * is represented by the AST + * (MATCH l + * (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h) + * (MATCH_CASE nil 0)) + * + * The type rule for match performs several well-formedness checks, including: + * - The head is a datatype T, + * - The remaining children are either MATCH_BIND_CASE or MATCH_CASE, + * - The patterns for the cases are over the same datatype as the head term, + * - The return types for the cases are comparable, + * - The patterns specified by the children are exhaustive for T. + * + * The type rule returns the (least common subtype) of the return types of the + * cases. + */ class MatchTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * The type rule for match case ensures the first child is a datatype term, + * and returns the type of the second argument. + */ class MatchCaseTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * The type rule for match bind case ensures the first child is a bound variable + * list and the second child is a datatype. Returns the type of the third + * argument. + */ class MatchBindCaseTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Tuple project is indexed by a list of indices (n_1, ..., n_m). It ensures + * that the argument is a tuple whose arity k is greater that each n_i for + * i = 1, ..., m. If the argument is of type (Tuple T_1 ... T_k), then the + * returned type is (Tuple T_{n_1} ... T_{n_m}). + */ class TupleProjectTypeRule { public: static TypeNode computeType(NodeManager* nm, TNode n, bool check); }; +/** + * A codatatype bound variable is used for constructing values for codatatypes. + * It stores an index and a type. The type rule returns that type. + */ class CodatatypeBoundVariableTypeRule { public: diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 80d7b0e03..a957159e4 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -25,26 +25,58 @@ namespace cvc5 { namespace theory { namespace quantifiers { +/** + * Type rule used for FORALL and EXISTS. Ensures the first argument is a + * bound variable list, the second argument has Boolean Type, and the third + * argument (if it exists) is an instantiation pattern list. Returns the + * Boolean type. + * + * Furthermore ensures that certain annotations (e.g., for INST_POOL) are well + * formed. In particular, instantiation pool annotations specify how to + * instantiate this quantified formula. These must specify n sets, where n + * is the number of variables of this quantified formula. + */ struct QuantifierTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for bound variable lists. Ensures its children are bound variables, + * and returns the bound variable list type. + */ struct QuantifierBoundVarListTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for instantiation patterns. This checks for a common mistake + * of using terms instead of term lists in pattern annotations, and returns + * the instantiation pattern type. + */ struct QuantifierInstPatternTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * A quantifier annotation, which returns the instantiation pattern type. + * + * Furthermore ensures well-formedness of instantiation attributes with more + * that one child, which must have a keyword specified as a constant string as + * the first child (the remaining children can be arbitrary). + */ struct QuantifierAnnotationTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for instantiation pattern lists. Ensures its children are either + * instantiation patterns, instantiation attributes, or other allowed + * annotations. Returns the instantiation pattern list type. + */ struct QuantifierInstPatternListTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index f437ba2d7..961c2e582 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -25,32 +25,58 @@ namespace cvc5 { namespace theory { namespace sep { +/** + * Separation empty heap constraint is a nullary predicate. Its type rule + * returns the Boolean type. + */ class SepEmpTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Separation points-to is a predicate over any two types that specify the + * heap, which is not checked by the type system. Its type rule + * returns the Boolean type. + */ struct SepPtoTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Separation star is an n-ary Boolean connective. Its type rule ensures all + * arguments are Boolean. Returns the Boolean type. + */ struct SepStarTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Separation star is a binary Boolean connective. Its type rule ensures all + * arguments are Boolean and returns the Boolean type. + */ struct SepWandTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Separation label annotates formulas with sets that specify the heap. It + * ensures its first argument is a Boolean, its second argument is a set and + * returns the Boolean type. + */ struct SepLabelTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Separation nil is a nullary constructor. Its type is specified via an + * attribute upon construction and is return in this rule. + */ struct SepNilTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index 2c0dcd763..e46560a71 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -84,7 +84,7 @@ TypeNode CardinalityConstraintOpTypeRule::computeType(NodeManager* nodeManager, n, "cardinality constraint must be positive"); } } - return nodeManager->booleanType(); + return nodeManager->builtinOperatorType(); } TypeNode CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager, @@ -107,7 +107,7 @@ TypeNode CombinedCardinalityConstraintOpTypeRule::computeType( n, "combined cardinality constraint must be positive"); } } - return nodeManager->booleanType(); + return nodeManager->builtinOperatorType(); } TypeNode CombinedCardinalityConstraintTypeRule::computeType( @@ -116,13 +116,6 @@ TypeNode CombinedCardinalityConstraintTypeRule::computeType( return nodeManager->booleanType(); } -TypeNode PartialTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - return n.getOperator().getType().getRangeType(); -} - TypeNode HoApplyTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 6f0374ae6..3ff0f63c6 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -25,43 +25,63 @@ namespace cvc5 { namespace theory { namespace uf { +/** + * Type rule for applications of uninterpreted functions, which are associated + * to types (-> T1 ... Tn T). This ensures the arguments of n have type + * T1 ... Tn and returns T. + */ class UfTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * A cardinality constraint specified by its operator, returns the Boolean type. + */ class CardinalityConstraintTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * The type rule for cardinality constraint operators, which is indexed by a + * type and an integer. Ensures that type is an uninterpreted sort and the + * integer is positive, and returns the builtin type. + */ class CardinalityConstraintOpTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * A combined cardinality constraint specified by its operator, returns the + * Boolean type. + */ class CombinedCardinalityConstraintTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * The type rule for combined cardinality constraint operators, which is indexed + * by an integer. Ensures that the integer is positive, and returns the builtin + * type. + */ class CombinedCardinalityConstraintOpTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class PartialTypeRule -{ - public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - -// class with the typing rule for HO_APPLY terms +/** + * Type rule for HO_APPLY terms. Ensures the first argument is a function type + * (-> T1 ... Tn T), the second argument is T1, and returns (-> T2 ... Tn T) if + * n > 1 or T otherwise. + */ class HoApplyTypeRule { public: @@ -69,6 +89,11 @@ class HoApplyTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for lambas. Ensures the first argument is a bound varible list + * (x1 ... xn). Returns the function type (-> T1 ... Tn T) where T1...Tn are + * the types of x1..xn and T is the type of the second argument. + */ class LambdaTypeRule { public: -- 2.30.2