blob: e4b946105eaa1efc70df97f828d4f26aee87a474 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_UF ::cvc5::theory::uf::TheoryUF "theory/uf/theory_uf.h"
typechecker "theory/uf/theory_uf_type_rules.h"
properties stable-infinite parametric
properties check ppStaticLearn presolve
rewriter ::cvc5::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function"
typerule APPLY_UF ::cvc5::theory::uf::UfTypeRule
variable BOOLEAN_TERM_VARIABLE "Boolean term variable"
operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S"
typerule CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CardinalityConstraintTypeRule
operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature"
typerule COMBINED_CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CombinedCardinalityConstraintTypeRule
parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application"
typerule PARTIAL_APPLY_UF ::cvc5::theory::uf::PartialTypeRule
operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
typerule CARDINALITY_VALUE ::cvc5::theory::uf::CardinalityValueTypeRule
operator HO_APPLY 2 "higher-order (partial) function application"
typerule HO_APPLY ::cvc5::theory::uf::HoApplyTypeRule
endtheory
|
