smtlib-rs
smtlib-rs copied to clipboard
Support retrieving values from get-model (i.e. extracting values from `Term`s)
Take the following example program:
use miette::IntoDiagnostic;
use smtlib::{backend::Z3Binary, Real, Solver, Sort};
fn main() -> miette::Result<()> {
miette::set_panic_hook();
let mut solver = Solver::new(Z3Binary::new("z3").into_diagnostic()?)?;
let x = Real::from_name("x");
let y = Real::from_name("y");
let z = Real::from_name("z");
solver.assert(x.lt(0))?;
solver.assert(z.lt(0))?;
solver.assert(y.gt(1))?;
solver.assert((x * x - y * z * (-10))._eq(y))?;
let m = solver.check_sat_with_model()?.expect_sat()?;
eprintln!("{}", m);
eprintln!("x = {:?}", m.eval(x).unwrap());
eprintln!("y = {:?}", m.eval(y).unwrap());
eprintln!("z = {:?}", m.eval(z).unwrap());
Ok(())
}
In this case, say I would like to get the values of x, y, and z as f64
. Z3 will return the values in terms of define-fun
, so this would require some ability to interpret the AST in Rust, most likely?
{ z: (- (/ 1.0 4.0)), x: (- 2.0), y: (/ 8.0 7.0) }
That is, I would want z = -0.25
, x = -2
, y = 1.14285714286
or some similar approximation, with the understanding that Real
and f64
are not exactly equivalent.
Maybe this is already possible?