Skolem Identifiers

enum class cvc5::SkolemId
The kind of a cvc5 skolem. A skolem is a (family of) internal functions or constants that are introduced by cvc5. These symbols are treated as uninterpreted internally. We track their definition for the purposes of formal bookkeeping for the user of features like proofs, lemma exporting, simplification and so on.
A skolem has an identifier and a set of “skolem indices”. The skolem indices are not children of the skolem function, but rather should be seen as the way of distinguishing skolems from the same family.
For example, the family of “array diff” skolems
ARRAY_DEQ_DIFF
witness the disequality between two arrays, which are its skolem indices.Say that skolem k witnesses the disequality between two arrays A and B of type
(Array Int Int)
. Then, k is a term whose skolem identifier isARRAY_DEQ_DIFF
, skolem indices are A and B, and whose type isInt
.Note the type of k is not
(> (Array Int Int) (Array Int Int) Int)
. Intuitively, this is due to the fact that cvc5 does not reason about array diff skolem as a function symbol. Furthermore, the array diff skolem that witnesses the disequality of arrays C and D is a separate skolem function k2 from this family, also of typeInt
, where internally k2 has no relation to k apart from having the same skolem identifier.In contrast, cvc5 reasons about divisionbyzero using a single skolem function whose identifier is
DIV_BY_ZERO
. This means its skolem indices are empty and the skolem has a functional type(> Real Real)
.Values:

enumerator INTERNAL
The identifier of the skolem is not exported. These skolems should not appear in any userlevel API calls.

enumerator PURIFY
The purification skolem for a term. This is a variable that is semantically equivalent to the indexed term t.
Number of skolem indices:
1
1:
The term t that this skolem purifies.
Sort: The sort of t.

enumerator GROUND_TERM
An arbitrary ground term of a given sort.
Number of skolem indices:
1
1:
A term that represents the sort of the term.
Sort: The sort given by the index.

enumerator ARRAY_DEQ_DIFF
The array diff skolem, which is the witness k for the inference
(=> (not (= A B)) (not (= (select A k) (select B k))))
.Number of skolem indices:
2
1:
The first array of sort(Array T1 T2)
.2:
The second array of sort(Array T1 T2)
.
Sort:
T1

enumerator BV_EMPTY
The empty bitvector.
Number of skolem indices:
0
Type:
(_ BitVec 0)

enumerator DIV_BY_ZERO
The function for division by zero. This is semantically equivalent to the SMTLIB term
(lambda ((x Real)) (/ x 0.0))
.Number of skolem indices:
0
Sort:
(> Real Real)

enumerator INT_DIV_BY_ZERO
The function for integer division by zero. This is semantically equivalent to the SMTLIB term
(lambda ((x Int)) (div x 0))
.Number of skolem indices:
0
Sort:
(> Int Int)

enumerator MOD_BY_ZERO
The function for integer modulus by zero. This is semantically equivalent to the SMTLIB term
(lambda ((x Int)) (mod x 0))
.Number of skolem indices:
0
Sort:
(> Int Int)

enumerator TRANSCENDENTAL_PURIFY
A function introduced to eliminate extended trancendental functions. Transcendental functions like sqrt, arccos, arcsin, etc. are replaced during processing with uninterpreted functions that are unique to each function.
Number of skolem indices:
1
1:
A lambda corresponding to the function, e.g.(lambda ((x Real)) (sqrt x))
.
Sort:
(> Real Real)

enumerator TRANSCENDENTAL_PURIFY_ARG
Argument used to purify trancendental function app
(f x)
. For(sin x)
, this is a variable that is assumed to be in phase withx
that is betweenpi
andpi
.Number of skolem indices:
1
1:
The application of a trancendental function.
Sort:
Real

enumerator SHARED_SELECTOR
A shared datatype selector, see Reynolds et. al. “Datatypes with Shared
Selectors”, IJCAR 2018. Represents a selector that can extract fields of multiple constructors.
Number of skolem indices:
3
1:
A term that represents the datatype we are extracting from.2:
A term that represents the sort of field we are extracting.3:
An integer n such that this shared selector returns the n^th subfield term of the given sort.
Sort: A selector sort whose domain is given by first index, and whose codomain is the given by the second index.

enumerator QUANTIFIERS_SKOLEMIZE
The n^th skolem for quantified formula Q.
Number of skolem indices:
2
1:
The quantified formula Q.2:
The variable in the binder of Q to skolemize.
Sort: The type of the second index.

enumerator STRINGS_NUM_OCCUR
An integer corresponding to the number of times a string occurs in another string. This is used to reason about str.replace_all.
Number of skolem indices:
2
1:
The first string.2:
The second string.
Sort:
Int

enumerator STRINGS_OCCUR_INDEX
A function k such that for x = 0…n, (k x) is the end index of the x^th occurrence of a string b in string a, where n is the number of occurrences of b in a, and
(= (k 0) 0)
. This is used to reason about str.replace_all.Number of skolem indices:
2
1:
The first string.2:
The second string.
Sort:
(> Int Int)

enumerator STRINGS_NUM_OCCUR_RE
Analogous to STRINGS_NUM_OCCUR, but for regular expressions. An integer corresponding to the number of times a regular expression can be matched in a string. This is used to reason about str.replace_all_re.
Number of skolem indices:
2
1:
The string to match.2:
The regular expression to find.
Sort:
Int

enumerator STRINGS_OCCUR_INDEX_RE
Analogous to STRINGS_OCCUR_INDEX, but for regular expressions. A function k such that for x = 0…n, (k x) is the end index of the x^th occurrence of a regular expression R in string a, where n is the number of occurrences of R in a, and
(= (k 0) 0)
. This is used to reason about str.replace_all_re.Number of skolem indices:
2
1:
The string to match.2:
The regular expression to find.
Sort:
(> Int Int)

enumerator STRINGS_OCCUR_LEN_RE
A function k where for x = 0…n,
(k x)
is the length of the x^th occurrence of R in a (excluding matches of empty strings) where R is a regular expression, n is the number of occurrences of R in a, and(= (k 0) 0)
.Number of skolem indices:
2
1:
The string to match.2:
The regular expression to find.
Sort:
(> Int Int)

enumerator STRINGS_DEQ_DIFF
Difference index for string disequalities, such that k is the witness for the inference
(=> (not (= a b)) (not (= (substr a k 1) (substr b k 1))))
where note thatk
may be out of bounds for at most of a,b.Number of skolem indices:
2
1:
The first string.2:
The second string.
Sort:
Int

enumerator STRINGS_REPLACE_ALL_RESULT
A function used to define intermediate results of str.replace_all and str.replace_re_all applications. This denotes a function that denotes the result of processing the string or sequence after processing the n^th occurrence of string or match of the regular expression in the given replace_all term.
Number of skolem indices:
1
1:
The application of replace_all or replace_all_re.
Sort:
(> Int S)
where S is eitherString
or(Seq T)
for someT
.

enumerator STRINGS_ITOS_RESULT
A function used to define intermediate results of str.from_int applications. This is a function k denoting the result of processing the first n digits of the argument.
Number of skolem indices:
1
1:
The argument to str.from_int.
Sort:
(> Int Int)

enumerator STRINGS_STOI_RESULT
A function used to define intermediate results of str.from_int applications. This is a function k of type
(> Int String)
denoting the result of processing the first n characters of the argument.Number of skolem indices:
1
1:
The argument to str.to_int.
Sort:
(> Int String)

enumerator STRINGS_STOI_NON_DIGIT
A position containing a nondigit in a string, used when
(str.to_int a)
is equal to 1. This is an integer that returns a position for which the argument string is not a digit if one exists, or is unconstrained otherwise.Number of skolem indices:
1
1:
The argument to str.to_int.
Sort:
Int

enumerator RE_FIRST_MATCH_PRE
The next three skolems are used to decompose the match of a regular expression in string.
For string a and regular expression R, this skolem is the prefix of string a before the first, shortest match of R in a. Formally, if
(str.in_re a (re.++ (re.* re.allchar) R (re.* re.allchar)))
, then there exists strings k_pre, k_match, k_post such that:(= a (str.++ k_pre k_match k_post))
and(= (len k_pre) (indexof_re a R 0))
and(forall ((l Int)) (=> (< 0 l (len k_match)) (not (str.in_re (substr k_match 0 l) R))))
and(str.in_re k_match R)
This skolem is k_pre, and the proceeding two skolems are k_match and k_post.Number of skolem indices:
2
1:
The string.2:
The regular expression to match.
Sort:
String

enumerator RE_FIRST_MATCH
For string a and regular expression R, this skolem is the string that the first, shortest match of R was matched to in a.
Number of skolem indices:
2
1:
The string.2:
The regular expression to match.
Sort:
String

enumerator RE_FIRST_MATCH_POST
For string a and regular expression
R
, this skolem is the remainder of a after the first, shortest match ofR
in a.Number of skolem indices:
2
1:
The string.2:
The regular expression to match.
Sort:
String

enumerator RE_UNFOLD_POS_COMPONENT
Regular expression unfold component: if
(str.in_re a R)
, where R is(re.++ R0 ... Rn)
, then theRE_UNFOLD_POS_COMPONENT
for indices (a,R,i) is a string ki such that(= a (str.++ k0 ... kn))
and(str.in_re k0 R0)
for i = 0, …, n.Number of skolem indices:
3
1:
The string.2:
The regular expression.3:
The index of the skolem.
Sort:
String

enumerator BAGS_CARD_COMBINE
An uninterpreted function for bag.card operator: To compute
(bag.card A)
, we need a function that counts multiplicities of distinct elements. We call this function combine of type Int > Int where: combine(0) = 0. combine(i) = m(elements(i), A) + combine(i1) for 1 <= i <= n. elements: a skolem function for (bag.fold f t A). SeeBAGS_DISTINCT_ELEMENTS
. n: is the number of distinct elements in A.Number of skolem indices:
1
1:
the bag argument A.
Sort:
(> Int Int)

enumerator BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT
An uninterpreted function for the union of distinct elements in a bag (Bag T). To compute operators like bag.card, we need a function for distinct elements in A of type (> Int T) (see
BAGS_DISTINCT_ELEMENTS
). We also need to restrict the range [1, n] to only elements in the bag as follows: unionDisjoint(0) = bag.empty. unionDisjoint(i) = disjoint union of {<elements(i), m(elements(i), A)>} and unionDisjoint(i1). unionDisjoint(n) = A.Number of skolem indices:
1
1:
the bag argument A of type (Bag T).
Sort:
(> Int (Bag T))

enumerator BAGS_FOLD_CARD
An uninterpreted function for bag.fold operator: To compute
(bag.fold f t A)
, we need to guess the cardinality n of bag A using a skolem function withBAGS_FOLD_CARD
id.Number of skolem indices:
1
1:
the bag argument A.
Sort:
Int

enumerator BAGS_FOLD_COMBINE
An uninterpreted function for bag.fold operator: To compute
(bag.fold f t A)
, we need a function that accumulates intermidiate values. We call this function combine of type Int > T2 where: combine(0) = t combine(i) = f(elements(i), combine(i  1)) for 1 <= i <= n. elements: a skolem function for (bag.fold f t A) seeBAGS_FOLD_ELEMENTS
. n: is the cardinality of A. T2: is the type of initial value t.Number of skolem indices:
3
1:
the function f of type(> T1 T2)
.2:
the initial value t of typeT2
.3:
the bag argument A of type(Bag T1)
.
Sort:
(> Int T2)

enumerator BAGS_FOLD_ELEMENTS
An uninterpreted function for bag.fold operator: To compute
(bag.fold f t A)
, we need a function for elements of A. We call this function elements of type(> Int T1)
where T1 is the type of elements of A. If the cardinality of A is n, then A is the disjoint union of {elements(i)} for 1 <= i <= n. SeeBAGS_FOLD_UNION_DISJOINT
.Number of skolem indices:
1
1:
a bag argument A of type(Bag T1)
Sort:
(> Int T1)

enumerator BAGS_FOLD_UNION_DISJOINT
An uninterpreted function for bag.fold operator: To compute
(bag.fold f t A)
, we need a function for elements of A which is given by elements defined inBAGS_FOLD_ELEMENTS
. We also need unionDisjoint:(> Int (Bag T1))
to compute the disjoint union such that: unionDisjoint(0) = bag.empty. unionDisjoint(i) = disjoint union of {elements(i)} and unionDisjoint (i1). unionDisjoint(n) = A.Number of skolem indices:
1
1:
the bag argument A of type(Bag T1)
.
Sort:
(> Int (Bag T1))

enumerator BAGS_CHOOSE
An interpreted function
uf
for bag.choose operator:(bag.choose A)
is replaced by(uf A)
along with the inference that(>= (bag.count (uf A) A) 1)
whenA
is nonempty. whereT
is the type of elements of A.Number of skolem indices:
1
1:
the bag to chose from, of type (Bag T).
Sort:
(> (Bag T) T)

enumerator BAGS_DISTINCT_ELEMENTS
An uninterpreted function for distinct elements of a bag A, which returns the n^th distinct element of the bag. See
BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT
.Number of skolem indices:
1
1:
the bag argument A of type(Bag T)
.
Sort:
(> Int T)

enumerator BAGS_DISTINCT_ELEMENTS_SIZE
A skolem variable for the size of the distinct elements of a bag A.
Number of skolem indices:
1
1:
the bag argument A.
Sort:
Int

enumerator BAGS_MAP_PREIMAGE_INJECTIVE
A skolem for the preimage of an element y in
(bag.map f A)
such that(= (f x) y)
where f:(> E T)
is an injective function.Number of skolem indices:
3
1:
the function f of type(> E T)
.2:
the bag argument A of(Bag E)
.3:
the element argument y typeT
.
Sort:
E

enumerator BAGS_MAP_INDEX
A skolem variable for the index that is unique per terms
(bag.map f A)
, y, e where: f:(> E T)
, A:(Bag E)
, y:T
, e:E
Number of skolem indices:
5
1:
a map term of the form(bag.map f A)
.2:
a skolem function with idBAGS_DISTINCT_ELEMENTS
.3:
a skolem function with idBAGS_DISTINCT_ELEMENTS_SIZE
.4:
an element y of typeT
representing the mapped value.5:
an element x of typeE
.
Sort:
Int

enumerator BAGS_MAP_SUM
An uninterpreted function for bag.map operator: If bag A is {uf(1), …, uf(n)} (see
BAGS_DISTINCT_ELEMENTS
}, then the multiplicity of an element y in a bag(bag.map f A)
is sum(n), where sum:(> Int Int)
is a skolem function such that: sum(0) = 0 sum(i) = sum (i1) + (bag.count (uf i) A)Number of skolem indices:
3
1:
the function f of type(> E T)
.2:
the bag argument A of(Bag E)
.3:
the element argument e typeE
.
Sort:
(> Int Int)

enumerator BAGS_DEQ_DIFF
The bag diff skolem, which is the witness k for the inference
(=> (not (= A B)) (not (= (bag.count k A) (bag.count k B))))
.Number of skolem indices:
2
1:
The first bag of type(Bag T)
.2:
The second bag of type(Bag T)
.
Sort:
T

enumerator TABLES_GROUP_PART
Given a group term
((_ table.group n1 ... nk) A)
of type(Bag (Table T))
, this skolem maps elements of A to their parts in the resulting partition.Number of skolem indices:
1
1:
a group term of the form((_ table.group n1 ... nk) A)
.
Sort:
(> T (Table T))

enumerator TABLES_GROUP_PART_ELEMENT
Given a group term
((_ table.group n1 ... nk) A)
of type(Bag (Table T))
and a part B of type(Table T)
, this function returns a skolem element that is a member of B if B is not empty.Number of skolem indices:
2
1:
a group term of the form((_ table.group n1 ... nk) A)
.2:
a table B of type(Table T)
.
Sort:
T

enumerator RELATIONS_GROUP_PART
Given a group term
((_ rel.group n1 ... nk) A)
of type(Set (Relation T))
this skolem maps elements of A to their parts in the resulting partition.Number of skolem indices:
1
1:
a relation of the form((_ rel.group n1 ... nk) A)
.
Sort:
(> T (Relation T))

enumerator RELATIONS_GROUP_PART_ELEMENT
Given a group term ((_ rel.group n1 … nk) A) of type (Set (Relation T)) and a part B of type (Relation T), this function returns a skolem element that is a member of B if B is not empty.
Number of skolem indices:
2
1:
a group term of the form((_ rel.group n1 ... nk) A)
.2:
a relation B of type(Relation T)
.
Sort:
T

enumerator SETS_CHOOSE
An interpreted function for set.choose operator, where
(set.choose A)
is expanded to(uf A)
along with the inference(set.member (uf A) A))
whenA
is nonempty, where uf:(> (Set E) E)
is this skolem function, and E is the type of elements ofA
.Number of skolem indices:
1
1:
a ground value for the type(Set E)
.
Sort:
(> (Set E) E)

enumerator SETS_DEQ_DIFF
The set diff skolem, which is the witness k for the inference
(=> (not (= A B)) (not (= (set.member k A) (set.member k B))))
.Number of skolem indices:
2
1:
The first set of type(Set E)
.2:
The second set of type(Set E)
.
Sort:
E

enumerator SETS_FOLD_CARD
An uninterpreted function for set.fold operator: To compute
(set.fold f t A)
, we need to guess the cardinality n of set A using a skolem function with SETS_FOLD_CARD id.Number of skolem indices:
1
1:
the set argument A.
Sort:
Int

enumerator SETS_FOLD_COMBINE
An uninterpreted function for set.fold operator: To compute
(set.fold f t A)
, we need a function that accumulates intermidiate values. We call this function combine of type Int > T2 where: combine(0) = t combine(i) = f(elements(i), combine(i  1)) for 1 <= i <= n elements: a skolem function for (set.fold f t A) see SETS_FOLD_ELEMENTS n: is the cardinality of A T2: is the type of initial value tNumber of skolem indices:
3
1:
the function f of type(> T1 T2)
.2:
the initial value t of typeT2
.3:
the set argument A of type(Set T1)
.
Sort:
(> Int T2)

enumerator SETS_FOLD_ELEMENTS
An uninterpreted function for set.fold operator: To compute
(set.fold f t A)
, we need a function for elements of A. We call this function elements of type(> Int T)
where T is the type of elements of A. If the cardinality of A is n, then A is the union of {elements(i)} for 1 <= i <= n. See SETS_FOLD_UNION_DISJOINT.Number of skolem indices:
1
1:
a set argument A of type(Set T)
.
Sort:
(> Int T)

enumerator SETS_FOLD_UNION
An uninterpreted function for set.fold operator: To compute
(set.fold f t A)
, we need a function for elements of A which is given by elements defined in SETS_FOLD_ELEMENTS. We also need unionFn:(> Int (Set E))
to compute the union such that: unionFn(0) = set.empty unionFn(i) = union of {elements(i)} and unionFn (i1) unionFn(n) = ANumber of skolem indices:
1
1:
a set argument A of type(Set E)
.
Sort:
(> Int (Set E))

enumerator SETS_MAP_DOWN_ELEMENT
A skolem variable that is unique per terms
(set.map f A)
, y which is an element in(set.map f A)
. The skolem is constrained to be an element in A, and it is mapped to y by f.Number of skolem indices:
2
1:
a map term of the form(set.map f A)
where A of type(Set E)
2:
the element argument y.
Sort:
E

enumerator FP_MIN_ZERO
A skolem function that is unique per floatingpoint sort, introduced for the undefined zero case of
fp.min
.Number of skolem indices:
1
1:
The floatingpoint sortFP
of the fp.min operator.
Sort:
(> FP FP (_ BitVec 1))

enumerator FP_MAX_ZERO
A skolem function that is unique per floatingpoint sort, introduced for the undefined zero case of
fp.max
.Number of skolem indices:
1
1:
The floatingpoint sortFP
of the fp.max operator.
Sort:
(> FP FP (_ BitVec 1))

enumerator FP_TO_UBV
A skolem function introduced for the undefined outoufbounds case of
fp.to_ubv
that is unique per floatingpoint sort and sort of the arguments to the operator.Number of skolem indices:
2
1:
The floatingpoint sortFP
of operand of fp.to_ubv.2:
The bitvector sortBV
to convert to.
Sort:
(> RoundingMode FP BV)

enumerator FP_TO_SBV
A skolem function introduced for the undefined outoufbounds case of
fp.to_sbv
that is unique per floatingpoint sort and sort of the arguments to the operator.Number of skolem indices:
2
1:
The floatingpoint sortFP
of operand of fp.to_sbv.2:
The bitvector sortBV
to convert to.
Sort:
(> RoundingMode FP BV)

enumerator FP_TO_REAL
A skolem function introduced for the undefined of
fp.to_real
that is unique per floatingpoint sort.Number of skolem indices:
1
1:
The floatingpoint sortFP
of the operand of fp.to_real.
Sort:
(> FP Real)

enumerator NONE
Indicates this is not a skolem.

enumerator INTERNAL