blob: 68941489f4bf8c7ae2c7ff70f9a081cc81468fdc (
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
|
# 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 check propagate #presolve postsolve
# Theory content goes here.
# constants...
constant EMPTYSET \
::CVC4::EmptySet \
::CVC4::EmptySetHashFunction \
"util/emptyset.h" \
"empty set"
# types...
operator SET_TYPE 1 "set type" # the type
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"
operator MEMBER 2 "set membership"
operator SET_SINGLETON 1 "singleton set"
typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
typerule MEMBER ::CVC4::theory::sets::SetMemberTypeRule
typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule
construle UNION ::CVC4::theory::sets::SetConstTypeRule
endtheory
|
