Struct OrdealSolver 

pub struct OrdealSolver { /* private fields */ }

The default engine: pure-Rust ordeal with a conflict budget.

Implementations

impl OrdealSolver

pub fn new() -> Self

New solver with the budget from SYNTH_ORDEAL_MAX_CONFLICTS (default [DEFAULT_MAX_CONFLICTS]; 0 = unbounded).

Trait Implementations

impl BvSolver for OrdealSolver

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

Engine name (diagnostics).

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

Add cond to the asserted conjunction.

fn check(&mut self) -> CheckOutcome

Decide satisfiability of the asserted conjunction.

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.

impl Default for OrdealSolver

fn default() -> Self

Returns the “default value” for a type.