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 \
::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" \
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
"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
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
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%)" \
::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 \
::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
::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"
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
::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"
}
};/* class LambdaTypeRule */
+/* For co-datatypes, not yet supported--
+**
class MuTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
TypeNode rangeType = n[1].getType(check);
return nodeManager->mkFunctionType(argTypes, rangeType);
}
-};/* class MuTypeRule */
+};
+**/
class ChainTypeRule {
public:
-# 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"
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)"
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
projects / cvc5.git / commitdiff