Skip to main content

BvSolver

synth_verify::solver

Trait BvSolver 

Source 
pub trait BvSolver {
    // Required methods
    fn name(&self) -> &'static str;
    fn assert(&mut self, cond: &Bool);
    fn check(&mut self) -> CheckOutcome;
    fn value(&self, var: &BV) -> Option<u128>;
}
Expand description

The thin solver interface: assert boolean terms, check once, read the model back on Sat. One instance = one query (no incremental solving — synth’s translation-validation fragment is one-shot by design).

Required Methods§

Source

fn name(&self) -> &'static str

Engine name (diagnostics).

Source

fn assert(&mut self, cond: &Bool)

Add cond to the asserted conjunction.

Source

fn check(&mut self) -> CheckOutcome

Decide satisfiability of the asserted conjunction.

Source

fn value(&self, var: &BV) -> Option<u128>

After CheckOutcome::Sat: the model value of a free variable (with model completion — unconstrained variables read as 0, matching z3’s eval(_, true)). None if there is no model or var is not a free variable.

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§