z3 0.20.0

High-level rust bindings for the Z3 SMT solver from Microsoft Research
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

use crate::Context;
use crate::ast::Ast;
use z3_sys::Z3_translate;

pub mod synchronization;

/// Represents types that depend on a [`Context`] and can be translated to another [`Context`].
///
/// # Safety
///
/// Implementations of this trait must ensure that the `translate` method
/// translates _all_ contained z3 data into the new `Context`
pub unsafe trait Translate {
    fn translate(&self, dest: &Context) -> Self;
}

unsafe impl<T: Translate> Translate for Vec<T> {
    fn translate(&self, dest: &Context) -> Self {
        self.iter().map(|t| t.translate(dest)).collect()
    }
}

unsafe impl<T: Ast> Translate for T {
    fn translate(&self, dest: &Context) -> Self {
        unsafe {
            Self::wrap(dest, {
                Z3_translate(self.get_ctx().z3_ctx.0, self.get_z3_ast(), dest.z3_ctx.0).unwrap()
            })
        }
    }
}