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: ordeal decides under a conflict budget (check_with_limit) so an adversarial query degrades to a clean conservative Unknown instead of hanging. Override with SYNTH_ORDEAL_MAX_CONFLICTS (0 = unbounded).

Structs

OrdealSolver

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

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: