blob: 71d5fce4ad5b9b09bbf78236be64880d8c8dfe32 (
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_SETS \
::cvc5::theory::sets::TheorySets \
"theory/sets/theory_sets.h"
typechecker "theory/sets/theory_sets_type_rules.h"
rewriter ::cvc5::theory::sets::TheorySetsRewriter \
"theory/sets/theory_sets_rewriter.h"
properties parametric
properties check presolve
# constants
constant SET_EMPTY\
class \
EmptySet \
::cvc5::EmptySetHashFunction \
"expr/emptyset.h" \
"the empty set constant; payload is an instance of the cvc5::EmptySet class"
# the type
operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
cardinality SET_TYPE \
"::cvc5::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
"theory/sets/theory_sets_type_rules.h"
well-founded SET_TYPE \
"::cvc5::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
"::cvc5::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
"theory/sets/theory_sets_type_rules.h"
enumerator SET_TYPE \
"::cvc5::theory::sets::SetEnumerator" \
"theory/sets/theory_sets_type_enumerator.h"
# operators
operator SET_UNION 2 "set union"
operator SET_INTER 2 "set intersection"
operator SET_MINUS 2 "set subtraction"
operator SET_SUBSET 2 "subset predicate; first parameter a subset of second"
operator SET_MEMBER 2 "set membership predicate; first parameter a member of second"
constant SET_SINGLETON_OP \
class \
SetSingletonOp \
::cvc5::SetSingletonOpHashFunction \
"theory/sets/singleton_op.h" \
"operator for singletons; payload is an instance of the cvc5::SingletonOp class"
parameterized SET_SINGLETON SET_SINGLETON_OP 1 \
"constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
operator SET_INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
operator SET_CARD 1 "set cardinality operator"
operator SET_COMPLEMENT 1 "set complement (with respect to finite universe)"
nullaryoperator SET_UNIVERSE "(finite) universe set, all set variables must be interpreted as subsets of it."
# A set comprehension is specified by:
# (1) a bound variable list x1 ... xn,
# (2) a predicate P[x1...xn], and
# (3) a term t[x1...xn].
# A comprehension C with the above form has members given by the following
# semantics:
# forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C)
# where y ranges over the element type of the (set) type of the comprehension.
# Notice that since all sets must be interpreted as finite, this means that
# cvc5 will not be able to construct a model for any set comprehension such
# that there are infinitely many y that satisfy the left hand side of the
# equivalence above. The same limitation occurs more generally when combining
# finite sets with quantified formulas.
operator SET_COMPREHENSION 3 "set comprehension specified by a bound variable list, a predicate, and a term."
# The operator choose returns an element from a given set.
# If set A = {x}, then the term (choose A) is equivalent to the term x.
# If the set is empty, then (choose A) is an arbitrary value.
# If the set has cardinality > 1, then (choose A) will deterministically return an element in A.
operator SET_CHOOSE 1 "return an element in the set given as a parameter"
# The operator is_singleton returns whether the given set is a singleton
operator SET_IS_SINGLETON 1 "return whether the given set is a singleton"
operator RELATION_JOIN 2 "relation join"
operator RELATION_PRODUCT 2 "relation cartesian product"
operator RELATION_TRANSPOSE 1 "relation transpose"
operator RELATION_TCLOSURE 1 "relation transitive closure"
operator RELATION_JOIN_IMAGE 2 "relation join image"
operator RELATION_IDEN 1 "relation identity"
typerule SET_UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SET_INTER ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SET_MINUS ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SET_SUBSET ::cvc5::theory::sets::SubsetTypeRule
typerule SET_MEMBER ::cvc5::theory::sets::MemberTypeRule
typerule SET_SINGLETON_OP "SimpleTypeRule<RBuiltinOperator>"
typerule SET_SINGLETON ::cvc5::theory::sets::SingletonTypeRule
typerule SET_EMPTY ::cvc5::theory::sets::EmptySetTypeRule
typerule SET_INSERT ::cvc5::theory::sets::InsertTypeRule
typerule SET_CARD ::cvc5::theory::sets::CardTypeRule
typerule SET_COMPLEMENT ::cvc5::theory::sets::ComplementTypeRule
typerule SET_UNIVERSE ::cvc5::theory::sets::UniverseSetTypeRule
typerule SET_COMPREHENSION ::cvc5::theory::sets::ComprehensionTypeRule
typerule SET_CHOOSE ::cvc5::theory::sets::ChooseTypeRule
typerule SET_IS_SINGLETON ::cvc5::theory::sets::IsSingletonTypeRule
typerule RELATION_JOIN ::cvc5::theory::sets::RelBinaryOperatorTypeRule
typerule RELATION_PRODUCT ::cvc5::theory::sets::RelBinaryOperatorTypeRule
typerule RELATION_TRANSPOSE ::cvc5::theory::sets::RelTransposeTypeRule
typerule RELATION_TCLOSURE ::cvc5::theory::sets::RelTransClosureTypeRule
typerule RELATION_JOIN_IMAGE ::cvc5::theory::sets::JoinImageTypeRule
typerule RELATION_IDEN ::cvc5::theory::sets::RelIdenTypeRule
construle SET_UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
construle SET_SINGLETON ::cvc5::theory::sets::SingletonTypeRule
endtheory
|
