z3-solver/src/solving/mod.rs


1
2
3
4
5
6
7
8
9

pub mod z3;

#[derive(Debug, Eq, PartialEq, Ord, PartialOrd, Hash, Clone, Copy)]
pub struct FloatHandle(u32);

pub trait Solver {
    // TODO: make handles generic?
    fn new_float<'a>(&'a mut self, handles: &mut z3::Handles<'a>) -> FloatHandle;
}