rustproof-libsmt 0.1.0

Rust bindings for z3 as utilized by RustProof.
Documentation 
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
117
118
119
120
121
122

//! Defines basic operations defined under FixedSizeBitVectors theory in SMTLIB2.

use std::fmt;

use backends::backend::SMTNode;

#[macro_export]
macro_rules! bv_const {
    ($solver: ident, $i: expr, $n: expr) => { $solver.new_const(bitvec::OpCodes::Const($i, $n)) }
}

#[derive(Clone, Debug)]
pub enum OpCodes {
    Concat,
    Extract(u64, u64),
    BvNot,
    BvAnd,
    BvOr,
    BvNeg,
    BvAdd,
    BvMul,
    BvSMulDoesNotOverflow,
    BvSMulDoesNotUnderflow,
    BvUMulDoesNotOverflow,
    BvUDiv,
    BvURem,
    BvShl,
    BvLShr,
    BvULt,
    BvNand,
    BvNor,
    BvXor,
    BvXnor,
    BvComp,
    BvSub,
    BvSDiv,
    BvSRem,
    BvSMod,
    BvAShr,
    // parameterized functions
    Repeat(u64),
    ZeroExtend(u64),
    SignExtend(u64),
    RotateLeft(u64),
    RotateRight(u64),
    // logical functions
    BvULe,
    BvUGt,
    BvUGe,
    BvSLt,
    BvSLe,
    BvSGt,
    BvSGe,
    Const(u64, usize),
    FreeVar(String),
}

impl fmt::Display for OpCodes {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        let s = match *self {
            OpCodes::Concat => "concat".to_owned(),
            OpCodes::Extract(i, j) => format!("(_ extract {} {})", i, j),
            OpCodes::BvNot => "bvnot".to_owned(),
            OpCodes::BvAnd => "bvand".to_owned(),
            OpCodes::BvOr => "bvor".to_owned(),
            OpCodes::BvNeg => "bvneg".to_owned(),
            OpCodes::BvAdd => "bvadd".to_owned(),
            OpCodes::BvMul => "bvmul".to_owned(),
            OpCodes::BvSMulDoesNotOverflow => "bvsmul_noovfl".to_owned(),
            OpCodes::BvSMulDoesNotUnderflow => "bvsmul_noudfl".to_owned(),
            OpCodes::BvUMulDoesNotOverflow => "bvumul_noovfl".to_owned(),
            OpCodes::BvUDiv => "bvudiv".to_owned(),
            OpCodes::BvURem => "bvurem".to_owned(),
            OpCodes::BvShl => "bvshl".to_owned(),
            OpCodes::BvLShr => "bvlshr".to_owned(),
            OpCodes::BvULt => "bvult".to_owned(),
            OpCodes::BvNand => "bvnand".to_owned(),
            OpCodes::BvNor => "bvnor".to_owned(),
            OpCodes::BvXor => "bvxor".to_owned(),
            OpCodes::BvXnor => "bvxnor".to_owned(),
            OpCodes::BvComp => "bvcomp".to_owned(),
            OpCodes::BvSub => "bvsub".to_owned(),
            OpCodes::BvSDiv => "bvsdiv".to_owned(),
            OpCodes::BvSRem => "bvsrem".to_owned(),
            OpCodes::BvSMod => "bvsmod".to_owned(),
            OpCodes::BvAShr => "bvashr".to_owned(),
            OpCodes::Repeat(i) => format!("(_ repeat {})", i),
            OpCodes::ZeroExtend(i) => format!("(_ zero_extend {})", i),
            OpCodes::SignExtend(i) => format!("(_ sign_extend {})", i),
            OpCodes::RotateLeft(i) => format!("(_ rotate_left {})", i),
            OpCodes::RotateRight(i) => format!("(_ rotate_right {})", i),
            OpCodes::BvULe => "bvule".to_owned(),
            OpCodes::BvUGt => "bvugt".to_owned(),
            OpCodes::BvUGe => "bvuge".to_owned(),
            OpCodes::BvSLt => "bvslt".to_owned(),
            OpCodes::BvSLe => "bvsle".to_owned(),
            OpCodes::BvSGt => "bvsgt".to_owned(),
            OpCodes::BvSGe => "bvsge".to_owned(),
            OpCodes::Const(val, n) => format!("(_ bv{} {})", val, n),
            OpCodes::FreeVar(ref name) => format!("{}", name),
        };
        write!(f, "{}", s)
    }
}

impl_smt_node!(OpCodes, define vars [OpCodes::FreeVar(_)], define consts [OpCodes::Const(_, _)]);

#[derive(Clone, Debug)]
pub enum Sorts {
    BitVector(usize),
    Bool,
}

impl fmt::Display for Sorts {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        let s = match *self {
            Sorts::BitVector(ref n) => format!("(_ BitVec {})", n),
            Sorts::Bool => format!("{}", "bool"),
        };
        write!(f, "{}", s)
    }
}