diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/arith/kinds | 31 | ||||
| -rw-r--r-- | src/theory/arrays/kinds | 8 | ||||
| -rw-r--r-- | src/theory/booleans/kinds | 14 | ||||
| -rw-r--r-- | src/theory/builtin/kinds | 51 | ||||
| -rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 5 | ||||
| -rw-r--r-- | src/theory/strings/kinds | 9 |
6 files changed, 61 insertions, 57 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index a8a4047ca..45470180b 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -12,39 +12,38 @@ properties check propagate ppStaticLearn presolve notifyRestart rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" - -operator PLUS 2: "arithmetic addition" -operator MULT 2: "arithmetic multiplication" +operator PLUS 2: "arithmetic addition (N-ary)" +operator MULT 2: "arithmetic multiplication (N-ary)" operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" -operator DIVISION 2 "real division (user symbol)" +operator DIVISION 2 "real division, division by 0 undefined (user symbol)" operator DIVISION_TOTAL 2 "real division with interpreted division by 0 (internal symbol)" -operator INTS_DIVISION 2 "ints division (user symbol)" -operator INTS_DIVISION_TOTAL 2 "ints division with interpreted division by 0 (internal symbol)" -operator INTS_MODULUS 2 "ints modulus (user symbol)" -operator INTS_MODULUS_TOTAL 2 "ints modulus with interpreted division by 0 (internal symbol)" +operator INTS_DIVISION 2 "integer division, division by 0 undefined (user symbol)" +operator INTS_DIVISION_TOTAL 2 "integer division with interpreted division by 0 (internal symbol)" +operator INTS_MODULUS 2 "integer modulus, division by 0 undefined (user symbol)" +operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (internal symbol)" operator ABS 1 "absolute value" -parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate" +parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term" operator POW 2 "arithmetic power" constant DIVISIBLE_OP \ ::CVC4::Divisible \ ::CVC4::DivisibleHashFunction \ "util/divisible.h" \ - "operator for the divisibility-by-k predicate" + "operator for the divisibility-by-k predicate; payload is an instance of the CVC4::Divisible class" sort REAL_TYPE \ Cardinality::REALS \ well-founded \ "NodeManager::currentNM()->mkConst(Rational(0))" \ "expr/node_manager.h" \ - "Real type" + "real type" sort INTEGER_TYPE \ Cardinality::INTEGERS \ well-founded \ "NodeManager::currentNM()->mkConst(Rational(0))" \ "expr/node_manager.h" \ - "Integer type" + "integer type" constant SUBRANGE_TYPE \ ::CVC4::SubrangeBounds \ @@ -63,7 +62,7 @@ constant CONST_RATIONAL \ ::CVC4::Rational \ ::CVC4::RationalHashFunction \ "util/rational.h" \ - "a multiple-precision rational constant" + "a multiple-precision rational constant; payload is an instance of the CVC4::Rational class" enumerator REAL_TYPE \ "::CVC4::theory::arith::RationalEnumerator" \ @@ -80,9 +79,9 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" -operator IS_INTEGER 1 "term is integer" -operator TO_INTEGER 1 "cast term to integer" -operator TO_REAL 1 "cast term to real" +operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" +operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)" +operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)" typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index a731d3677..0bc973de9 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -26,20 +26,20 @@ enumerator ARRAY_TYPE \ "theory/arrays/type_enumerator.h" # select a i is a[i] -operator SELECT 2 "array select" +operator SELECT 2 "array select; first parameter is an array term, second is the selection index" # store a i e is a[i] <= e -operator STORE 3 "array store" +operator STORE 3 "array store; first parameter is an array term, second is the store index, third is the term to store at the index" # storeall t e is \all i in indexType(t) <= e constant STORE_ALL \ ::CVC4::ArrayStoreAll \ ::CVC4::ArrayStoreAllHashFunction \ "util/array_store_all.h" \ - "array store-all" + "array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)" # used internally by array theory -operator ARR_TABLE_FUN 4 "array table function (internal symbol)" +operator ARR_TABLE_FUN 4 "array table function (internal-only symbol)" typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 4d748ca59..ad45e3cbb 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -22,19 +22,19 @@ constant CONST_BOOLEAN \ bool \ ::CVC4::BoolHashFunction \ "util/bool.h" \ - "truth and falsity" + "truth and falsity; payload is a (C++) bool" enumerator BOOLEAN_TYPE \ "::CVC4::theory::booleans::BooleanEnumerator" \ "theory/booleans/type_enumerator.h" operator NOT 1 "logical not" -operator AND 2: "logical and" -operator IFF 2 "logical equivalence" -operator IMPLIES 2 "logical implication" -operator OR 2: "logical or" -operator XOR 2 "exclusive or" -operator ITE 3 "if-then-else" +operator AND 2: "logical and (N-ary)" +operator IFF 2 "logical equivalence (exactly two parameters)" +operator IMPLIES 2 "logical implication (exactly two parameters)" +operator OR 2: "logical or (N-ary)" +operator XOR 2 "exclusive or (exactly two parameters)" +operator ITE 3 "if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) condition, second is 'then', third is 'else' and these two parameters must have same base sort" typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule 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: diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 48e9957d4..3134fcab0 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -1,4 +1,7 @@ -# kinds [for strings theory] +# kinds -*- sh -*- +# +# For documentation on this file format, please refer to +# src/theory/builtin/kinds. # theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" @@ -9,8 +12,7 @@ rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_s typechecker "theory/strings/theory_strings_type_rules.h" - -operator STRING_CONCAT 2: "string concat" +operator STRING_CONCAT 2: "string concat (N-ary)" operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" operator STRING_SUBSTR 3 "string substr (user symbol)" @@ -97,7 +99,6 @@ typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule - typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule |