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
|
use super::{Solver, FloatHandle};
use std::collections::HashMap;
pub struct Z3Solver {
ctx: z3::Context,
}
pub struct Handles<'a> {
float: HashMap<u32, z3::ast::Real<'a>>,
float_max_id: u32,
}
impl<'a> Handles<'a> {
pub fn new() -> Self {
Self {
float: HashMap::new(),
float_max_id: 0,
}
}
}
impl Z3Solver {
pub fn new<'a>() -> (Self, Handles<'a>) {
let config = z3::Config::new();
(
Self {
ctx: z3::Context::new(&config),
},
Handles::new(),
)
}
}
impl Solver for Z3Solver {
fn new_float<'a>(&'a mut self, handles: &mut Handles<'a>) -> FloatHandle {
let id = handles.float_max_id;
let float = z3::ast::Real::new_const(&self.ctx, id);
handles.float_max_id += 1;
handles.float.insert(id, float);
FloatHandle(id)
}
}
|
