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.
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);
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:
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);
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);
n, "cardinality constraint must be positive");
}
}
- return nodeManager->booleanType();
+ return nodeManager->builtinOperatorType();
}
TypeNode CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager,
n, "combined cardinality constraint must be positive");
}
}
- return nodeManager->booleanType();
+ return nodeManager->builtinOperatorType();
}
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)
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:
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:
projects / cvc5.git / commitdiff