Struct OrdealSolver 

pub struct OrdealSolver { /* private fields */ }

The default engine: pure-Rust ordeal under a per-query wall-clock deadline (with a conflict budget as the disabled-deadline fallback).

Implementations

impl OrdealSolver

pub fn new() -> Self

New solver bounded by SYNTH_ORDEAL_DEADLINE_MS (default [DEFAULT_DEADLINE_MS]; 0 = deadline off), falling back to the SYNTH_ORDEAL_MAX_CONFLICTS conflict budget (default [DEFAULT_MAX_CONFLICTS]; 0 = unbounded) when the deadline is off.

pub fn with_deadline_ms(deadline_ms: u64) -> Self

New solver with an explicit wall-clock budget in ms (0 = deadline off). Env-independent, so tests can pin a budget without racing the process-global environment.

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.