Struct Z3 

pub struct Z3 {
    pub queries: usize,
    pub z3_calls: usize,
    /* private fields */
}

A cached Z3 pipe, using either the command line or a JavaScript callback.

Fields

queries: usize

Obligations submitted.

z3_calls: usize

Obligations passed to z3.

Implementations

impl Z3

pub fn new_cli(cache_dir: Option<PathBuf>) -> Option<Self>

Expect the z3 command to be available in the environment. Optionally provide a filesystem cache for model output.

pub fn new_wasm(callback: Function) -> Self

Pass a javascript callback string->string for smt2 input.

pub fn entails_lia( &mut self, facts: &[Constraint], goal: &Constraint, nonneg: &[Var], names: &[&str], ) -> Verdict

Try to prove a goal given facts by linearizing the whole system.