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)
    }
}