blob: 3fb73749dee3e5df6d1b08957935865223da3e07 (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_SETS \
::CVC4::theory::sets::TheorySets \
"theory/sets/theory_sets.h"
typechecker "theory/sets/theory_sets_type_rules.h"
rewriter ::CVC4::theory::sets::TheorySetsRewriter \
"theory/sets/theory_sets_rewriter.h"
properties parametric
properties check propagate presolve
# constants
constant EMPTYSET \
::CVC4::EmptySet \
::CVC4::EmptySetHashFunction \
"expr/emptyset.h" \
"the empty set constant; payload is an instance of the CVC4::EmptySet class"
# the type
operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
cardinality SET_TYPE \
"::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
"theory/sets/theory_sets_type_rules.h"
well-founded SET_TYPE \
"::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
"::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
"theory/sets/theory_sets_type_rules.h"
enumerator SET_TYPE \
"::CVC4::theory::sets::SetEnumerator" \
"theory/sets/theory_sets_type_enumerator.h"
# operators
operator UNION 2 "set union"
operator INTERSECTION 2 "set intersection"
operator SETMINUS 2 "set subtraction"
operator SUBSET 2 "subset predicate; first parameter a subset of second"
operator MEMBER 2 "set membership predicate; first parameter a member of second"
operator SINGLETON 1 "the set of the single element given as a parameter"
operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
operator CARD 1 "set cardinality operator"
operator JOIN 2 "set join"
operator PRODUCT 2 "set cartesian product"
operator TRANSPOSE 1 "set transpose"
operator TCLOSURE 1 "set transitive closure"
typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SUBSET ::CVC4::theory::sets::SubsetTypeRule
typerule MEMBER ::CVC4::theory::sets::MemberTypeRule
typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
typerule INSERT ::CVC4::theory::sets::InsertTypeRule
typerule CARD ::CVC4::theory::sets::CardTypeRule
typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule
typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule
construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule
construle INSERT ::CVC4::theory::sets::InsertTypeRule
construle CARD ::CVC4::theory::sets::CardTypeRule
construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule
construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule
endtheory
|
