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

// Copyright (c) Facebook, Inc. and its affiliates.
//
// This source code is licensed under the MIT license found in the
// LICENSE file in the root directory of this source tree.

pub enum Sorts {
    // Core theory
    Bool,

    // Arithmetic
    Int,
    Real,

    // Arrays
    Array,

    // Bitvectors
    BitVec(u32),
}

pub enum Fn<'a> {
    // Core theory
    False,
    True,
    Not,
    Implies,
    And,
    Or,
    Xor,
    Eq,
    Neq, // abbreviation for Not o Eq
    Ite,
    Distinct,

    // Arithmetic
    Uminus,
    Minus,
    Plus,
    Times,
    Divide,
    Div,
    Mod,
    Abs,
    LE,
    LT,
    GE,
    GT,
    ToReal,
    ToInt,
    IsInt,

    // Arrays
    Select,
    Store,

    // Records
    RecordSelect(&'a str),
    RecordUpdate(&'a str),

    // Bitvectors
    Concat,
    Extract(u32, u32),
    Bvnot,
    Bvand,
    Bvor,
    Bvneg,
    Bvadd,
    Bvmul,
    Bvudiv,
    Bvurem,
    Bvshl,
    Bvlshr,
    Bvult,
    Bvnand,
    Bvnor,
    Bvxor,
    Bvxnor,
    Bvcomp,
    Bvsub,
    Bvsdiv,
    Bvsrem,
    Bvsmod,
    Bvashr,
    Repeat(u32),
    ZeroExtend(u32),
    SignExtend(u32),
    RotateLeft(u32),
    RotateRight(u32),
    Bvule,
    Bvugt,
    Bvuge,
    Bvslt,
    Bvsle,
    Bvsgt,
    Bvsge,
}