rz3 0.1.2

Deterministic, exact-rational SMT solver in pure Rust (DPLL(T)/CDCL) with a complete linear-arithmetic core. Zero C dependencies, WASM-deployable, reproducible run-to-run.
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226

pub mod fp;

impl Expr {
    pub fn get_type(&self) -> Type {
        match self {
            Expr::Bool(_) | Expr::And(_) | Expr::Or(_) | Expr::Not(_) | Expr::Implies(_, _) |
            Expr::Eq(_, _) | Expr::Lt(_, _) | Expr::Le(_, _) | Expr::Gt(_, _) | Expr::Ge(_, _) |
            Expr::StrContains(_, _) | Expr::BvUle(_, _) | Expr::BvUlt(_, _) | 
            Expr::BvSle(_, _) | Expr::BvSlt(_, _) | Expr::ForAll(_, _) | Expr::Exists(_, _) => Type::Bool,
            
            Expr::Int(_) | Expr::Add(_) | Expr::Sub(_) | Expr::Mul(_) | Expr::Div(_, _) |
            Expr::StrLen(_) => Type::Int,
            
            Expr::Real(_, _) => Type::Real,
            
            Expr::Var(_, ty) => ty.clone(),
            
            Expr::BvConst(_, w) => Type::BitVec(*w),
            Expr::BvAdd(a, _) | Expr::BvSub(a, _) | Expr::BvMul(a, _) |
            Expr::BvAnd(a, _) | Expr::BvOr(a, _) | Expr::BvXor(a, _) |
            Expr::BvNot(a) | Expr::BvShl(a, _) | Expr::BvLshr(a, _) |
            Expr::BvAshr(a, _) => a.get_type(),
            Expr::BvExtract(h, l, _) => Type::BitVec(h - l + 1),
            Expr::BvConcat(a, b) => {
                if let (Type::BitVec(wa), Type::BitVec(wb)) = (a.get_type(), b.get_type()) {
                    Type::BitVec(wa + wb)
                } else {
                    Type::Unknown
                }
            }
            
            Expr::Select(a, _) => {
                if let Type::Array(_, ety) = a.get_type() {
                    *ety
                } else {
                    Type::Unknown
                }
            }
            Expr::Store(a, _, _) => a.get_type(),
            
            Expr::StrConst(_) | Expr::StrConcat(_) => Type::String,
            
            Expr::App(name, args) if name == "fp" => match args.as_slice() {
                [Expr::BvConst(_, 1), Expr::BvConst(_, ebits), Expr::BvConst(_, sig_bits)] => {
                    Type::Float(fp::FloatSort {
                        exponent_bits: *ebits as u16,
                        significand_bits: (*sig_bits + 1) as u16,
                    })
                }
                _ => Type::Unknown,
            },
            Expr::App(name, args) if name.starts_with("fp.") => match name.as_str() {
                "fp.add" | "fp.sub" | "fp.mul" | "fp.div" | "fp.sqrt" | "fp.neg" | "fp.abs" => {
                    args.iter()
                        .find_map(|arg| match arg.get_type() {
                            Type::Float(sort) => Some(Type::Float(sort)),
                            _ => None,
                        })
                        .unwrap_or(Type::Unknown)
                }
                "fp.isNaN" | "fp.isInfinite" | "fp.isZero" => Type::Bool,
                _ => Type::Unknown,
            },
            Expr::App(_, _) => Type::Unknown,
            Expr::Ite(_, t, _) => t.get_type(),
        }
    }

    pub fn substitute(&self, vars: &BTreeMap<String, Expr>) -> Expr {
        match self {
            Expr::Var(name, _) => {
                if let Some(replacement) = vars.get(name) {
                    replacement.clone()
                } else {
                    self.clone()
                }
            }
            Expr::And(args) => Expr::And(args.iter().map(|a| a.substitute(vars)).collect()),
            Expr::Or(args) => Expr::Or(args.iter().map(|a| a.substitute(vars)).collect()),
            Expr::Not(inner) => Expr::Not(Box::new(inner.substitute(vars))),
            Expr::Implies(a, b) => Expr::Implies(Box::new(a.substitute(vars)), Box::new(b.substitute(vars))),
            Expr::Eq(a, b) => Expr::Eq(Box::new(a.substitute(vars)), Box::new(b.substitute(vars))),
            Expr::Add(args) => Expr::Add(args.iter().map(|a| a.substitute(vars)).collect()),
            Expr::App(name, args) => Expr::App(name.clone(), args.iter().map(|a| a.substitute(vars)).collect()),
            Expr::Select(a, i) => Expr::Select(Box::new(a.substitute(vars)), Box::new(i.substitute(vars))),
            Expr::Store(a, i, v) => Expr::Store(Box::new(a.substitute(vars)), Box::new(i.substitute(vars)), Box::new(v.substitute(vars))),
            _ => self.clone(),
        }
    }

    pub fn contains_var(&self, name: &str) -> bool {
        match self {
            Expr::Var(n, _) => n == name,
            Expr::And(args) | Expr::Or(args) | Expr::Add(args) | Expr::Mul(args) => args.iter().any(|a| a.contains_var(name)),
            Expr::Not(inner) | Expr::BvNot(inner) | Expr::StrLen(inner) => inner.contains_var(name),
            Expr::Implies(a, b) | Expr::Eq(a, b) | Expr::Lt(a, b) | Expr::Le(a, b) | Expr::Gt(a, b) | Expr::Ge(a, b) | 
            Expr::Div(a, b) | Expr::BvAdd(a, b) | Expr::BvSub(a, b) | Expr::BvMul(a, b) | 
            Expr::BvAnd(a, b) | Expr::BvOr(a, b) | Expr::BvXor(a, b) | Expr::BvShl(a, b) | Expr::BvLshr(a, b) | Expr::BvAshr(a, b) | 
            Expr::BvUle(a, b) | Expr::BvUlt(a, b) | Expr::BvSle(a, b) | Expr::BvSlt(a, b) | Expr::BvConcat(a, b) | 
            Expr::Select(a, b) | Expr::StrContains(a, b) => a.contains_var(name) || b.contains_var(name),
            Expr::Ite(c, t, e) | Expr::Store(c, t, e) => c.contains_var(name) || t.contains_var(name) || e.contains_var(name),
            Expr::App(_, args) => args.iter().any(|a| a.contains_var(name)),
            _ => false,
        }
    }
}

use std::collections::BTreeMap;
use std::fmt;

use num_bigint::BigInt;
use serde::{Serialize, Deserialize};

#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, PartialOrd, Ord)]
pub enum Expr {
    Bool(bool),
    Int(i64),
    Real(i64, u32), // Integer part and decimal scale
    Var(String, Type),
    And(Vec<Expr>),
    Or(Vec<Expr>),
    Not(Box<Expr>),
    Implies(Box<Expr>, Box<Expr>),
    Ite(Box<Expr>, Box<Expr>, Box<Expr>), // If-Then-Else
    Eq(Box<Expr>, Box<Expr>),
    Lt(Box<Expr>, Box<Expr>), // Less than
    Le(Box<Expr>, Box<Expr>), // Lower or equal
    Gt(Box<Expr>, Box<Expr>), // Greater than
    Ge(Box<Expr>, Box<Expr>), // Greater or equal
    Add(Vec<Expr>),
    Sub(Vec<Expr>),
    Mul(Vec<Expr>),
    Div(Box<Expr>, Box<Expr>),
    App(String, Vec<Expr>), // Function application
    // Bit-vectors
    BvConst(u64, usize), // Value and width
    BvAdd(Box<Expr>, Box<Expr>),
    BvSub(Box<Expr>, Box<Expr>),
    BvMul(Box<Expr>, Box<Expr>),
    BvAnd(Box<Expr>, Box<Expr>),
    BvOr(Box<Expr>, Box<Expr>),
    BvXor(Box<Expr>, Box<Expr>),
    BvNot(Box<Expr>),
    BvShl(Box<Expr>, Box<Expr>),
    BvLshr(Box<Expr>, Box<Expr>),
    BvAshr(Box<Expr>, Box<Expr>),
    BvUle(Box<Expr>, Box<Expr>),
    BvUlt(Box<Expr>, Box<Expr>),
    BvSle(Box<Expr>, Box<Expr>),
    BvSlt(Box<Expr>, Box<Expr>),
    BvExtract(usize, usize, Box<Expr>), // high, low, expr
    BvConcat(Box<Expr>, Box<Expr>),
    // Arrays
    Select(Box<Expr>, Box<Expr>),        // Array, Index
    Store(Box<Expr>, Box<Expr>, Box<Expr>), // Array, Index, Value
    // Quantifiers
    ForAll(Vec<(String, Type)>, Box<Expr>), // Bound variables and body
    Exists(Vec<(String, Type)>, Box<Expr>),
    // Strings
    StrConst(String),
    StrConcat(Vec<Expr>),
    StrLen(Box<Expr>),
    StrContains(Box<Expr>, Box<Expr>),
}

#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, PartialOrd, Ord)]
pub enum Type {
    Unknown,
    Bool,
    Int,
    Real,
    Float(fp::FloatSort),
    BitVec(usize),
    String,
    Array(Box<Type>, Box<Type>), // Index Type, Element Type
    Fn(Vec<Type>, Box<Type>), // Function type
}

#[derive(Debug, Clone)]
pub enum ModelValue {
    Bool(bool),
    Int(BigInt),
    Real(num_rational::BigRational),
    BitVec(u64, usize),
    /// Valor de modelo de punto flotante IEEE-754 exacto (contrato compartido con theory::fp).
    Float(fp::FloatValue),
}

impl fmt::Display for Expr {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Expr::Bool(b) => write!(f, "{}", b),
            Expr::Int(i) => write!(f, "{}", i),
            Expr::Real(i, s) => write!(f, "{}.{}", i, s),
            Expr::Var(s, _) => write!(f, "{}", s),
            Expr::And(v) => write!(f, "(and {:?})", v),
            Expr::Or(v) => write!(f, "(or {:?})", v),
            Expr::Not(e) => write!(f, "(not {})", e),
            Expr::Implies(a, b) => write!(f, "(=> {} {})", a, b),
            Expr::Ite(c, t, e) => write!(f, "(ite {} {} {})", c, t, e),
            Expr::Eq(a, b) => write!(f, "(= {} {})", a, b),
            Expr::Lt(a, b) => write!(f, "(< {} {})", a, b),
            Expr::Le(a, b) => write!(f, "(<= {} {})", a, b),
            Expr::Gt(a, b) => write!(f, "(> {} {})", a, b),
            Expr::Ge(a, b) => write!(f, "(>= {} {})", a, b),
            Expr::Add(v) => write!(f, "(+ {:?})", v),
            Expr::Sub(v) => write!(f, "(- {:?})", v),
            Expr::Mul(v) => write!(f, "(* {:?})", v),
            Expr::Div(a, b) => write!(f, "(/ {} {})", a, b),
            Expr::App(s, args) => write!(f, "({} {:?})", s, args),
            Expr::BvConst(v, w) => write!(f, "(_ bv{} {})", v, w),
            Expr::BvAdd(a, b) => write!(f, "(bvadd {} {})", a, b),
            Expr::BvAnd(a, b) => write!(f, "(bvand {} {})", a, b),
            Expr::BvExtract(h, l, e) => write!(f, "((_ extract {} {}) {})", h, l, e),
            Expr::Select(a, i) => write!(f, "(select {} {})", a, i),
            Expr::Store(a, i, v) => write!(f, "(store {} {} {})", a, i, v),
            Expr::ForAll(vars, body) => write!(f, "(forall {:?} {})", vars, body),
            Expr::Exists(vars, body) => write!(f, "(exists {:?} {})", vars, body),
            Expr::StrConst(s) => write!(f, "\"{}\"", s),
            Expr::StrConcat(v) => write!(f, "(str.++ {:?})", v),
            Expr::StrLen(s) => write!(f, "(str.len {})", s),
            Expr::StrContains(a, b) => write!(f, "(str.contains {} {})", a, b),
            _ => write!(f, "{:?}", self),
        }
    }
}