Module Wax_wasm.Cond_solverSource

BDD-based reasoning over conditional-annotation conditions, used for path-sensitive validation.

Conditions (@if <cond> ...) are translated into boolean formulas (BDDs) over condition variables. Boolean variables, version comparisons and string equalities are modeled precisely (using the vendored Theo library); conditions that cannot be modeled are reported as diagnostics.

Sourcetype t

A boolean formula over condition variables.

Sourceval true_ : t
Sourceval false_ : t
Sourceval and_ : t -> t -> t
Sourceval or_ : t -> t -> t
Sourceval not_ : t -> t
Sourceval is_satisfiable : t -> bool

Whether the formula has a satisfying assignment (theory-aware: e.g. contradictory version bounds are unsatisfiable).

Sourceval logical_implies : t -> t -> bool

logical_implies a b is true when a entails b.

Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourcetype env

Per-module solver state: variable interning, kind tracking and ill-formed diagnostic deduplication. Use a fresh env per module so nothing leaks between modules processed in the same process.

Sourceval create : unit -> env

Create a fresh, empty solver state.

Sourceval of_cond : env -> Wax_utils.Diagnostic.context -> location:Ast.location -> Ast.cond -> t

of_cond env ctx ~location c translates condition c into a formula, interning its variables in env. A diagnostic is reported (once per source location) for conditions that cannot be modeled; such conditions become a fresh unconstrained variable so that exploration can proceed. location is the enclosing conditional, used when a sub-condition carries no location of its own.

Sourceval explain : env -> ?style:[ `Wat | `Wax ] -> t -> string option

explain env ?style f returns a minimal human-readable assumption that makes f satisfiable (via shortest_sat), e.g. "$oxcaml and not $debug", naming variables from env. style selects the surface syntax for rendering variables, versions and operators (`Wat, the default, uses $-prefixed names, dotted versions and <>; `Wax uses bare names, version tuples and !=). Returns None when f is a tautology (always reachable) or unsatisfiable.