use smtlib::{backend::z3_binary::Z3Binary, Int, SatResultWithModel, Solver, prelude::*};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    // Initialize the solver with the Z3 backend. The "z3" string refers the
    // to location of the already installed `z3` binary. In this case, the
    // binary is in the path.
    let mut solver = Solver::new(Z3Binary::new("z3")?)?;

    // Declare two new variables
    let x = Int::new_const("x");
    let y = Int::new_const("y");

    // Assert some constraints. This tells the solver that these expressions
    // must be true, so any solution will satisfy these.
    solver.assert(x._eq(y + 25))?;
    solver.assert(x._eq(204))?;
    // The constraints are thus:
    // - x == y + 25
    // - x == 204
    // Note that we use `a._eq(b)` rather than `a == b`, since we want to
    // express the mathematical relation of `a` and `b`, while `a == b` checks
    // that the two **expressions** are structurally the same.

    // Check for validity
    match solver.check_sat_with_model()? {
        SatResultWithModel::Sat(model) => {
            // Since it is valid, we can extract the possible values of the
            // variables using a model
            println!("x = {}", model.eval(x).unwrap());
            println!("y = {}", model.eval(y).unwrap());
        }
        SatResultWithModel::Unsat => println!("No valid solutions found!"),
        SatResultWithModel::Unknown => println!("Satisfaction remains unknown..."),
    }

    Ok(())
}