diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-20 20:00:22 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 18:11:56 -0400 |
commit | 1a41e26473ff12108eb6700da3d386ffa9e731bd (patch) | |
tree | 0bd5e31740d2c3a7c89a0a7e663b734b98982e79 /src/theory/builtin | |
parent | 75ec455661ecc88a8b9f77f7b913c227b7f3e728 (diff) |
Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, and arith.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 51 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 5 |
2 files changed, 30 insertions, 26 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index d140d1990..508106106 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -246,19 +246,18 @@ typechecker "theory/builtin/theory_builtin_type_rules.h" properties stable-infinite -# Rewriter responisble for all the terms of the theory +# Rewriter responsible for all the terms of the theory rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" sort BUILTIN_OPERATOR_TYPE \ Cardinality::INTEGERS \ not-well-founded \ - "Built in type for built in operators" + "the type for built-in operators" variable SORT_TAG "sort tag" -parameterized SORT_TYPE SORT_TAG 0: "sort type" +parameterized SORT_TYPE SORT_TAG 0: "specifies types of user-declared 'uninterpreted' sorts" # This is really "unknown" cardinality, but maybe this will be good -# enough (for now) ? Once we support quantifiers, maybe reconsider -# this.. +# enough (for now) ? cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" well-founded SORT_TYPE \ "::CVC4::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \ @@ -268,7 +267,7 @@ constant UNINTERPRETED_CONSTANT \ ::CVC4::UninterpretedConstant \ ::CVC4::UninterpretedConstantHashFunction \ "util/uninterpreted_constant.h" \ - "The kind of expressions representing uninterpreted constants" + "the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::UninterpretedConstant class (used in models)" typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule enumerator SORT_TYPE \ ::CVC4::theory::builtin::UninterpretedSortEnumerator \ @@ -278,7 +277,7 @@ constant ABSTRACT_VALUE \ ::CVC4::AbstractValue \ ::CVC4::AbstractValueHashFunction \ "util/abstract_value.h" \ - "The kind of expressions representing abstract values (other than uninterpreted sort constants)" + "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC4::AbstractValue class (used in models)" typerule ABSTRACT_VALUE ::CVC4::theory::builtin::AbstractValueTypeRule # A kind representing "inlined" operators defined with OPERATOR @@ -289,39 +288,41 @@ constant BUILTIN \ ::CVC4::Kind \ ::CVC4::kind::KindHashFunction \ "expr/kind.h" \ - "The kind of expressions representing built-in operators" + "the kind of expressions representing built-in operators" -variable FUNCTION "function" -parameterized APPLY FUNCTION 0: "defined function application" +variable FUNCTION "a defined function" +parameterized APPLY FUNCTION 0: "application of a defined function" -operator EQUAL 2 "equality" -operator DISTINCT 2: "disequality" -variable VARIABLE "variable" -variable BOUND_VARIABLE "bound variable" -variable SKOLEM "skolem var" -operator SEXPR 0: "a symbolic expression" +operator EQUAL 2 "equality (two parameters only, sorts must match)" +operator DISTINCT 2: "disequality (N-ary, sorts must match)" +variable VARIABLE "a variable (not permitted in bindings)" +variable BOUND_VARIABLE "a bound variable (permitted in bindings and the associated lambda and quantifier bodies only)" +variable SKOLEM "a Skolem variable (internal only)" +operator SEXPR 0: "a symbolic expression (any arity)" -operator LAMBDA 2 "lambda" -operator MU 2 "mu" +operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body" -parameterized CHAIN CHAIN_OP 2: "chained operator" +## for co-datatypes, not yet supported +# operator MU 2 "mu" + +parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator" constant CHAIN_OP \ ::CVC4::Chain \ ::CVC4::ChainHashFunction \ "util/chain.h" \ - "the chained operator" + "the chained operator; payload is an instance of the CVC4::Chain class" constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ ::CVC4::TypeConstantHashFunction \ "expr/kind.h" \ - "basic types" -operator FUNCTION_TYPE 2: "function type" + "a representation for basic types" +operator FUNCTION_TYPE 2: "a function type" cardinality FUNCTION_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" well-founded FUNCTION_TYPE false -operator SEXPR_TYPE 0: "symbolic expression type" +operator SEXPR_TYPE 0: "the type of a symbolic expression" cardinality SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" @@ -335,7 +336,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule -typerule MU ::CVC4::theory::builtin::MuTypeRule +#typerule MU ::CVC4::theory::builtin::MuTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule @@ -343,7 +344,7 @@ constant SUBTYPE_TYPE \ ::CVC4::Predicate \ ::CVC4::PredicateHashFunction \ "util/predicate.h" \ - "predicate subtype" + "predicate subtype; payload is an instance of the CVC4::Predicate class" cardinality SUBTYPE_TYPE \ "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 3c8953e15..aba194d95 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -164,6 +164,8 @@ public: } };/* class LambdaTypeRule */ +/* For co-datatypes, not yet supported-- +** class MuTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -180,7 +182,8 @@ public: TypeNode rangeType = n[1].getType(check); return nodeManager->mkFunctionType(argTypes, rangeType); } -};/* class MuTypeRule */ +}; +**/ class ChainTypeRule { public: |