Enum SkolemId 

#[repr(u32)]
pub enum SkolemId {
    Internal = 0,
    Purify = 1,
    GroundTerm = 2,
    ArrayDeqDiff = 3,
    BvEmpty = 4,
    DivByZero = 5,
    IntDivByZero = 6,
    ModByZero = 7,
    TranscendentalPurify = 8,
    TranscendentalPurifyArg = 9,
    TranscendentalSinePhaseShift = 10,
    ArithVtsDelta = 11,
    ArithVtsDeltaFree = 12,
    ArithVtsInfinity = 13,
    ArithVtsInfinityFree = 14,
    SharedSelector = 15,
    HoDeqDiff = 16,
    QuantifiersSkolemize = 17,
    WitnessStringLength = 18,
    WitnessInvCondition = 19,
    StringsNumOccur = 20,
    StringsOccurIndex = 21,
    StringsNumOccurRe = 22,
    StringsOccurIndexRe = 23,
    StringsDeqDiff = 24,
    StringsReplaceAllResult = 25,
    StringsItosResult = 26,
    StringsStoiResult = 27,
    StringsStoiNonDigit = 28,
    ReUnfoldPosComponent = 29,
    BagsCardCombine = 30,
    BagsDistinctElementsUnionDisjoint = 31,
    BagsFoldCard = 32,
    BagsFoldCombine = 33,
    BagsFoldElements = 34,
    BagsFoldUnionDisjoint = 35,
    BagsChoose = 36,
    BagsDistinctElements = 37,
    BagsDistinctElementsSize = 38,
    BagsMapPreimageInjective = 39,
    BagsMapIndex = 40,
    BagsMapSum = 41,
    BagsDeqDiff = 42,
    TablesGroupPart = 43,
    TablesGroupPartElement = 44,
    RelationsGroupPart = 45,
    RelationsGroupPartElement = 46,
    SetsChoose = 47,
    SetsDeqDiff = 48,
    SetsFoldCard = 49,
    SetsFoldCombine = 50,
    SetsFoldElements = 51,
    SetsFoldUnion = 52,
    SetsMapDownElement = 53,
    FpMinZero = 54,
    FpMaxZero = 55,
    FpToUbv = 56,
    FpToSbv = 57,
    FpToReal = 58,
    BvToIntUf = 59,
    None = 60,
    Last = 61,
}

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 is ARRAY_DEQ_DIFF, skolem indices are A and B, and whose type is Int.

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 type Int, where internally k2 has no relation to k apart from having the same skolem identifier.

In contrast, cvc5 reasons about division-by-zero 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).

\internal

Variants

Internal = 0

Purify = 1

GroundTerm = 2

ArrayDeqDiff = 3

BvEmpty = 4

DivByZero = 5

IntDivByZero = 6

ModByZero = 7

TranscendentalPurify = 8

TranscendentalPurifyArg = 9

TranscendentalSinePhaseShift = 10

ArithVtsDelta = 11

ArithVtsDeltaFree = 12

ArithVtsInfinity = 13

ArithVtsInfinityFree = 14

SharedSelector = 15

HoDeqDiff = 16

QuantifiersSkolemize = 17

WitnessStringLength = 18

WitnessInvCondition = 19

StringsNumOccur = 20

StringsOccurIndex = 21

StringsNumOccurRe = 22

StringsOccurIndexRe = 23

StringsDeqDiff = 24

StringsReplaceAllResult = 25

StringsItosResult = 26

StringsStoiResult = 27

StringsStoiNonDigit = 28

ReUnfoldPosComponent = 29

BagsCardCombine = 30

BagsDistinctElementsUnionDisjoint = 31

BagsFoldCard = 32

BagsFoldCombine = 33

BagsFoldElements = 34

BagsFoldUnionDisjoint = 35

BagsChoose = 36

BagsDistinctElements = 37

BagsDistinctElementsSize = 38

BagsMapPreimageInjective = 39

BagsMapIndex = 40

BagsMapSum = 41

BagsDeqDiff = 42

TablesGroupPart = 43

TablesGroupPartElement = 44

RelationsGroupPart = 45

RelationsGroupPartElement = 46

SetsChoose = 47

SetsDeqDiff = 48

SetsFoldCard = 49

SetsFoldCombine = 50

SetsFoldElements = 51

SetsFoldUnion = 52

SetsMapDownElement = 53

FpMinZero = 54

FpMaxZero = 55

FpToUbv = 56

FpToSbv = 57

FpToReal = 58

BvToIntUf = 59

None = 60

Last = 61

Trait Implementations

impl Clone for SkolemId

fn clone(&self) -> SkolemId

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SkolemId

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for SkolemId

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for SkolemId

fn eq(&self, other: &SkolemId) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for SkolemId

impl Eq for SkolemId

impl StructuralPartialEq for SkolemId