Enum Constant and Description |
---|
ARITH_VTS_DELTA
Used to reason about virtual term substitution.
|
ARITH_VTS_DELTA_FREE
Used to reason about virtual term substitution.
|
ARITH_VTS_INFINITY
Used to reason about virtual term substitution.
|
ARITH_VTS_INFINITY_FREE
Used to reason about virtual term substitution.
|
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)))) . |
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. |
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) when A is non-empty. |
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)))) . |
BAGS_DISTINCT_ELEMENTS
An uninterpreted function for distinct elements of a bag A, which returns
the n^th distinct element of the bag.
|
BAGS_DISTINCT_ELEMENTS_SIZE
A skolem variable for the size of the distinct elements of a bag A.
|
BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT
An uninterpreted function for the union of distinct elements
in a bag (Bag T).
|
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 with BAGS_FOLD_CARD id. |
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. |
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. |
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 in
BAGS_FOLD_ELEMENTS . |
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) . |
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. |
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 (i-1) + (bag.count (uf i) A)
Number of skolem indices: 3
1: the function f of type (-> E T) . |
BV_EMPTY
The empty bitvector.
|
BV_TO_INT_UF
A skolem function introduced by the int-blaster.
|
DIV_BY_ZERO
The function for division by zero.
|
FP_MAX_ZERO
A skolem function that is unique per floating-point sort, introduced for
the undefined zero case of
fp.max . |
FP_MIN_ZERO
A skolem function that is unique per floating-point sort, introduced for
the undefined zero case of
fp.min . |
FP_TO_REAL
A skolem function introduced for the undefined of
fp.to_real that is
unique per floating-point sort. |
FP_TO_SBV
A skolem function introduced for the undefined out-ouf-bounds case of
fp.to_sbv that is unique per floating-point sort and sort of the
arguments to the operator. |
FP_TO_UBV
A skolem function introduced for the undefined out-ouf-bounds case of
fp.to_ubv that is unique per floating-point sort and sort of the
arguments to the operator. |
GROUND_TERM
An arbitrary ground term of a given sort.
|
HO_DEQ_DIFF
The higher-roder diff skolem, which is the witness k for the inference
{@code (=> (not (= A B)) (not (= (A k1 ...
|
INT_DIV_BY_ZERO
The function for integer division by zero.
|
INTERNAL
The identifier of the skolem is not exported.
|
MOD_BY_ZERO
The function for integer modulus by zero.
|
NONE
Indicates this is not a skolem.
|
PURIFY
The purification skolem for a term.
|
QUANTIFIERS_SKOLEMIZE
The n^th skolem for the negation of universally quantified formula Q.
|
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.
|
RE_FIRST_MATCH_POST
For string a and regular expression
R , this skolem is the remainder
of a after the first, shortest match of R in a. |
RE_FIRST_MATCH_PRE
The next three skolems are used to decompose the match of a regular
expression in string.
|
RE_UNFOLD_POS_COMPONENT
Regular expression unfold component: if
(str.in_re a R) , where R is
{@code (re.++ R0 ... |
RELATIONS_GROUP_PART
Given a group term {@code ((_ rel.group n1 ...
|
RELATIONS_GROUP_PART_ELEMENT
Given a group term ((_ rel.group n1 ...
|
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)) when A is non-empty,
where uf: (-> (Set E) E) is this skolem function, and E is the type of
elements of A . |
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)))) . |
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. |
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. |
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. |
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. |
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) . |
SHARED_SELECTOR
A shared datatype selector, see Reynolds et.
|
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 that `k` may be out of bounds for at most of a,b. |
STRINGS_ITOS_RESULT
A function used to define intermediate results of str.from_int
applications.
|
STRINGS_NUM_OCCUR
An integer corresponding to the number of times a string occurs in another
string.
|
STRINGS_NUM_OCCUR_RE
Analogous to STRINGS_NUM_OCCUR, but for regular expressions.
|
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) . |
STRINGS_OCCUR_INDEX_RE
Analogous to STRINGS_OCCUR_INDEX, but for regular expressions.
|
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) . |
STRINGS_REPLACE_ALL_RESULT
A function used to define intermediate results of str.replace_all and
str.replace_re_all applications.
|
STRINGS_STOI_NON_DIGIT
A position containing a non-digit in a string, used when
(str.to_int a)
is equal to -1. |
STRINGS_STOI_RESULT
A function used to define intermediate results of str.from_int
applications.
|
TABLES_GROUP_PART
Given a group term {@code ((_ table.group n1 ...
|
TABLES_GROUP_PART_ELEMENT
Given a group term {@code ((_ table.group n1 ...
|
TRANSCENDENTAL_PURIFY
A function introduced to eliminate extended trancendental functions.
|
TRANSCENDENTAL_PURIFY_ARG
Argument used to purify trancendental function app
(f x) . |
TRANSCENDENTAL_SINE_PHASE_SHIFT
Argument used to reason about the phase shift of arguments to sine.
|
WITNESS_INV_CONDITION
A witness for an invertibility condition.
|
WITNESS_STRING_LENGTH
A witness for a string or sequence of a given length.
|
Modifier and Type | Method and Description |
---|---|
static SkolemId |
fromInt(int value) |
int |
getValue() |
static SkolemId |
valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static SkolemId[] |
values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
public static final SkolemId INTERNAL
public static final SkolemId PURIFY
1
1:
The term t that this skolem purifies.
public static final SkolemId GROUND_TERM
1
1:
A term that represents the sort of the term.
public static final SkolemId ARRAY_DEQ_DIFF
(=> (not (= A B)) (not (= (select A k) (select B k))))
.
2
1:
The first array of sort (Array T1 T2)
.
2:
The second array of sort (Array T1 T2)
.
T1
public static final SkolemId BV_EMPTY
0
(_ BitVec 0)
public static final SkolemId DIV_BY_ZERO
(lambda ((x Real)) (/ x 0.0))
.
0
(-> Real Real)
public static final SkolemId INT_DIV_BY_ZERO
(lambda ((x Int)) (div x 0))
.
0
(-> Int Int)
public static final SkolemId MOD_BY_ZERO
(lambda ((x Int)) (mod x 0))
.
0
(-> Int Int)
public static final SkolemId TRANSCENDENTAL_PURIFY
1
1:
A lambda corresponding to the function, e.g.,
(-> Real Real)
public static final SkolemId TRANSCENDENTAL_PURIFY_ARG
(f x)
.
For (sin x)
, this is a variable that is assumed to be in phase with
x
that is between -pi
and pi
.
1
1:
The application of a trancendental function.
Real
public static final SkolemId TRANSCENDENTAL_SINE_PHASE_SHIFT
1
1:
The argument to sine.
Real
public static final SkolemId ARITH_VTS_DELTA
0
Real
public static final SkolemId ARITH_VTS_DELTA_FREE
0
Real
public static final SkolemId ARITH_VTS_INFINITY
0
1:
A term that represents an arithmetic sort (Int or Real).
public static final SkolemId ARITH_VTS_INFINITY_FREE
0
1:
A term that represents an arithmetic sort (Int or Real).
public static final SkolemId SHARED_SELECTOR
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.
public static final SkolemId HO_DEQ_DIFF
(=> (not (= A B)) (not (= (A k1 ... kn) (B k1 ... kn))))
.
2
1:
The first function of sort (-> T1 ... Tn T)
.
2:
The second function of sort (-> T1 ... Tn T)
.
3:
The argument index i.
Ti
public static final SkolemId QUANTIFIERS_SKOLEMIZE
2
1:
The quantified formula Q.
2:
The index of the variable in the binder of Q to skolemize.
public static final SkolemId WITNESS_STRING_LENGTH
3
1:
A term that represents the sort of the term.
2:
The assumed length of this term, expected to be a non-negative integer.
3:
A numeral identifier.
public static final SkolemId WITNESS_INV_CONDITION
1
1:
A formula of the form (exists x. (x <op> s) <rel> t)
or (exists x. x <rel> t)
, where s and t are ground
(bitvector) terms.
public static final SkolemId STRINGS_NUM_OCCUR
2
1:
The first string.
2:
The second string.
Int
public static final SkolemId STRINGS_OCCUR_INDEX
(= (k 0) 0)
. This is used to
reason about str.replace_all.
2
1:
The first string.
2:
The second string.
(-> Int Int)
public static final SkolemId STRINGS_NUM_OCCUR_RE
2
1:
The string to match.
2:
The regular expression to find.
Int
public static final SkolemId STRINGS_OCCUR_INDEX_RE
(= (k 0) 0)
. This is used
to reason about str.replace_all_re.
2
1:
The string to match.
2:
The regular expression to find.
(-> Int Int)
public static final SkolemId STRINGS_OCCUR_LEN_RE
(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)
.
2
1:
The string to match.
2:
The regular expression to find.
(-> Int Int)
public static final SkolemId STRINGS_DEQ_DIFF
(=> (not (= a b)) (not (= (substr a k 1) (substr b k 1))))
where note that `k` may be out of bounds for at most of a,b.
2
1:
The first string.
2:
The second string.
Int
public static final SkolemId STRINGS_REPLACE_ALL_RESULT
1
1:
The application of replace_all or replace_all_re.
(-> Int S)
where S is either String
or (Seq T)
for
T
.public static final SkolemId STRINGS_ITOS_RESULT
1
1:
The argument to str.from_int.
(-> Int Int)
public static final SkolemId STRINGS_STOI_RESULT
(-> Int String)
denoting the
result of processing the first n characters of the argument.
1
1:
The argument to str.to_int.
(-> Int String)
public static final SkolemId STRINGS_STOI_NON_DIGIT
(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.
1
1:
The argument to str.to_int.
Int
public static final SkolemId RE_FIRST_MATCH_PRE
(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.
2
1:
The string.
2:
The regular expression to match.
String
public static final SkolemId RE_FIRST_MATCH
2
1:
The string.
2:
The regular expression to match.
String
public static final SkolemId RE_FIRST_MATCH_POST
R
, this skolem is the remainder
of a after the first, shortest match of R
in a.
2
1:
The string.
2:
The regular expression to match.
String
public static final SkolemId RE_UNFOLD_POS_COMPONENT
(str.in_re a R)
, where R is
(re.++ R0 ... Rn)
, then the RE_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.
3
1:
The string.
2:
The regular expression.
3:
The index of the skolem.
String
public static final SkolemId BAGS_CARD_COMBINE
(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(i-1) for 1 <= i <= n.
elements: a skolem function for (bag.fold f t A).
See BAGS_DISTINCT_ELEMENTS
.
n: is the number of distinct elements in A.
1
1:
the bag argument A.
(-> Int Int)
public static final SkolemId BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT
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(i-1).
unionDisjoint(n) = A.
1
1:
the bag argument A of type (Bag T).
(-> Int (Bag T))
public static final SkolemId BAGS_FOLD_CARD
(bag.fold f t A)
, we need to guess the cardinality n of
bag A using a skolem function with BAGS_FOLD_CARD
id.
1
1:
the bag argument A.
Int
public static final SkolemId BAGS_FOLD_COMBINE
(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)
see BAGS_FOLD_ELEMENTS
.
n: is the cardinality of A.
T2: is the type of initial value t.
3
1:
the function f of type (-> T1 T2)
.
2:
the initial value t of type T2
.
3:
the bag argument A of type (Bag T1)
.
(-> Int T2)
public static final SkolemId BAGS_FOLD_ELEMENTS
(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.
See BAGS_FOLD_UNION_DISJOINT
.
1
1:
a bag argument A of type (Bag T1)
(-> Int T1)
public static final SkolemId BAGS_FOLD_UNION_DISJOINT
(bag.fold f t A)
, we need a function for
elements of A which is given by elements defined in
BAGS_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 (i-1).
unionDisjoint(n) = A.
1
1:
the bag argument A of type (Bag T1)
.
(-> Int (Bag T1))
public static final SkolemId BAGS_CHOOSE
uf
for bag.choose operator:
(bag.choose A)
is replaced by (uf A)
along with the inference
that (>= (bag.count (uf A) A) 1)
when A
is non-empty.
where T
is the type of elements of A.
1
1:
the bag to chose from, of type (Bag T).
(-> (Bag T) T)
public static final SkolemId BAGS_DISTINCT_ELEMENTS
BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT
.
1
1:
the bag argument A of type (Bag T)
.
(-> Int T)
public static final SkolemId BAGS_DISTINCT_ELEMENTS_SIZE
1
1:
the bag argument A.
Int
public static final SkolemId BAGS_MAP_PREIMAGE_INJECTIVE
(bag.map f A)
such that
(= (f x) y)
where f: (-> E T)
is an injective function.
3
1:
the function f of type (-> E T)
.
2:
the bag argument A of (Bag E)
.
3:
the element argument y type T
.
E
public static final SkolemId BAGS_MAP_INDEX
(bag.map f A)
, y, e where:
f: (-> E T)
,
A: (Bag E)
,
y: T
,
e: E
5
1:
a map term of the form (bag.map f A)
.
2:
a skolem function with id BAGS_DISTINCT_ELEMENTS
.
3:
a skolem function with id BAGS_DISTINCT_ELEMENTS_SIZE
.
4:
an element y of type T
representing the mapped value.
5:
an element x of type E
.
Int
public static final SkolemId BAGS_MAP_SUM
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 (i-1) + (bag.count (uf i) A)
3
1:
the function f of type (-> E T)
.
2:
the bag argument A of (Bag E)
.
3:
the element argument e type E
.
(-> Int Int)
public static final SkolemId BAGS_DEQ_DIFF
(=> (not (= A B)) (not (= (bag.count k A) (bag.count k B))))
.
2
1:
The first bag of type (Bag T)
.
2:
The second bag of type (Bag T)
.
T
public static final SkolemId TABLES_GROUP_PART
((_ table.group n1 ... nk) A)
of type
(Bag (Table T))
, this skolem maps elements of A to their parts in the
resulting partition.
1
1:
a group term of the form ((_ table.group n1 ... nk) A)
.
(-> T (Table T))
public static final SkolemId TABLES_GROUP_PART_ELEMENT
((_ 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.
2
1:
a group term of the form ((_ table.group n1 ... nk) A)
.
2:
a table B of type (Table T)
.
T
public static final SkolemId RELATIONS_GROUP_PART
((_ rel.group n1 ... nk) A)
of type
(Set (Relation T))
this skolem maps elements of A to their parts in the
resulting partition.
1
1:
a relation of the form ((_ rel.group n1 ... nk) A)
.
(-> T (Relation T))
public static final SkolemId RELATIONS_GROUP_PART_ELEMENT
2
1:
a group term of the form ((_ rel.group n1 ... nk) A)
.
2:
a relation B of type (Relation T)
.
T
public static final SkolemId SETS_CHOOSE
(set.choose A)
is expanded to (uf A)
along with the inference
(set.member (uf A) A))
when A
is non-empty,
where uf: (-> (Set E) E)
is this skolem function, and E is the type of
elements of A
.
1
1:
a ground value for the type (Set E)
.
(-> (Set E) E)
public static final SkolemId SETS_DEQ_DIFF
(=> (not (= A B)) (not (= (set.member k A) (set.member k B))))
.
2
1:
The first set of type (Set E)
.
2:
The second set of type (Set E)
.
E
public static final SkolemId SETS_FOLD_CARD
(set.fold f t A)
, we need to guess the cardinality n of
set A using a skolem function with SETS_FOLD_CARD id.
1
1:
the set argument A.
Int
public static final SkolemId SETS_FOLD_COMBINE
(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 t
3
1:
the function f of type (-> T1 T2)
.
2:
the initial value t of type T2
.
3:
the set argument A of type (Set T1)
.
(-> Int T2)
public static final SkolemId SETS_FOLD_ELEMENTS
(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.
1
1:
a set argument A of type (Set T)
.
(-> Int T)
public static final SkolemId SETS_FOLD_UNION
(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 (i-1)
unionFn(n) = A
1
1:
a set argument A of type (Set E)
.
(-> Int (Set E))
public static final SkolemId SETS_MAP_DOWN_ELEMENT
(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.
2
1:
a map term of the form (set.map f A)
where A of type (Set E)
2:
the element argument y.
E
public static final SkolemId FP_MIN_ZERO
fp.min
.
1
1:
The floating-point sort FP
of the fp.min operator.
(-> FP FP (_ BitVec 1))
public static final SkolemId FP_MAX_ZERO
fp.max
.
1
1:
The floating-point sort FP
of the fp.max operator.
(-> FP FP (_ BitVec 1))
public static final SkolemId FP_TO_UBV
fp.to_ubv
that is unique per floating-point sort and sort of the
arguments to the operator.
2
1:
The floating-point sort FP
of operand of fp.to_ubv.
2:
The bit-vector sort BV
to convert to.
(-> RoundingMode FP BV)
public static final SkolemId FP_TO_SBV
fp.to_sbv
that is unique per floating-point sort and sort of the
arguments to the operator.
2
1:
The floating-point sort FP
of operand of fp.to_sbv.
2:
The bit-vector sort BV
to convert to.
(-> RoundingMode FP BV)
public static final SkolemId FP_TO_REAL
fp.to_real
that is
unique per floating-point sort.
1
1:
The floating-point sort FP
of the operand of fp.to_real.
(-> FP Real)
public static final SkolemId BV_TO_INT_UF
1
1:
the original function f, with BV sorts.
public static final SkolemId NONE
public static SkolemId[] values()
for (SkolemId c : SkolemId.values()) System.out.println(c);
public static SkolemId valueOf(java.lang.String name)
name
- the name of the enum constant to be returned.java.lang.IllegalArgumentException
- if this enum type has no constant with the specified namejava.lang.NullPointerException
- if the argument is nullpublic static SkolemId fromInt(int value) throws CVC5ApiException
CVC5ApiException
public int getValue()