Module solver 

The thin solver trait behind which the SMT engines sit (#553).

Queries are built once as solver-agnostic terms (crate::term) and discharged through BvSolver:

• OrdealSolver — the default engine: ordeal, the pure-Rust, certificate-checked QF_BV solver (every Unsat carries an LRAT proof the trusted ordeal-lrat checker validated before it is reported). No C++ toolchain, no z3-sys build.
• Z3Solver (feature z3-solver) — the former engine, retained as the differential oracle.
• DifferentialSolver — used when both backends are compiled in and SYNTH_SOLVER_DIFF=1: every query runs through both engines. A verdict disagreement (Sat vs Unsat) is a hard error (panic — one of the solvers is wrong, and nothing downstream may proceed on either answer). An ordeal Unknown falls through to Z3’s verdict (logged, not fatal — Unknown is the conservative non-answer, not a verdict).

Budget: every query runs under a wall-clock deadline (Solver::check_with_deadline, ordeal ≥0.15) so an adversarial query degrades to a clean conservative Unknown instead of hanging. See [DEFAULT_DEADLINE_MS] for the budget, the env overrides and the documented limitation.

Structs

OrdealSolver

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

Enums

CheckOutcome

Outcome of a one-shot check of the asserted conjunction.

Traits

BvSolver

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).

Functions

new_solver

Construct the configured solver: