1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
//! Constraint solving for `randomize()` (LRM 1800-2023 Clause 18).
//!
//! Design: `docs/superpowers/plans/2026-10-03-constraints.md`. Pure Rust, no
//! sv-lang dependency except the AST builder (behind the `frontend` feature),
//! so `vj-runtime` (which depends on this crate with `default-features =
//! false`) reaches the solver through `sv_rt_obj`'s `Randomize` op.
//!
//! Layering, each module depending only on the ones above it:
//!
//! - [`ir`]: the word-level constraint IR (2-state bit-vector expressions and
//! boolean constraints) plus a direct evaluator used as the semantic oracle
//! for everything below. Deliberately NOT a reuse of codegen's 4-state
//! expression lowering (plan section 1.2).
//! - `build` (feature `frontend`): the sv-lang `Constraint`/`Expression` to
//! IR builder (`build::Builder`).
//! - [`bdd`]: bit-blasting of the IR into reduced ordered BDDs
//! (`biodivine-lib-bdd`), with an explicit node budget.
//! - [`rng`]: the thin draw wrapper over an object's own PRNG seed; the solver
//! never seeds, it only draws (plan section 1.6).
//! - [`order`]: the `solve ... before` partial order (18.5.9) reduced to the
//! ordered variable groups the solver samples in.
//! - [`randc`]: the per-variable `randc` cyclic-permutation state machine
//! (18.4.2); knows nothing about BDDs.
//! - [`sat`]: the fallback for problems whose BDD exceeds its node budget: the
//! same gadgets (`blast`) emitted as a CNF and searched with `splr`;
//! approximately uniform sampling.
//! - [`solve`]: the orchestrator: exact model counting and uniform sampling in
//! the caller-supplied solve order (or ordered groups, `randc` first,
//! weighted selector variables for `dist`); [`solve::Engine`] picks the BDD
//! solver, or [`sat`] when the BDD does not fit.
//! - [`dist`]: `dist` constraints (18.5.3): the selector-variable encoding and
//! the per-value weights evaluated at each `randomize()`.
//! - [`guard`]: the 18.5.12 constraint-guard evaluator (Task C8): the
//! TRUE/FALSE/RANDOM/ERROR value of an implication or `if` predicate
//! (Figure 18-3) and the resolve pass that picks the arms before solving.
//! - [`real_domain`]: constraints on `real`/`shortreal` random variables
//! (Task C9): interval sets on the float grid, `dist` over real ranges, and
//! staged solving of coupled guards; a separate namespace solved after the
//! integral variables.
//! - [`array`]: dynamic arrays, queues and associative arrays as constraint
//! operands (Task C11/C12/C14): the two-phase size-then-elements solve and
//! the `foreach`/reduction expansion that turns array-level IR nodes into
//! the scalar conjuncts [`bdd`] understands.
//! - [`func`]: functions called from constraints (Task C13, 18.5.11): the
//! small statement IR a function body is translated to, its interpreter, and
//! the folding of calls whose arguments are known into constants.
//! - [`func_order`]: the implicit priority a function's random arguments get
//! (18.5.11), as the stage each variable is solved in.
//! - [`priority`]: soft constraints (Task C15, 18.5.13): discard flags,
//! priorities, `disable soft`, the relaxation loop and the contained-object
//! priority order.
//! - [`joint`]: global constraints (Task C17, 18.5.8): the objects randomized
//! together with one that holds `rand` object members, and the merge of
//! their programs into one.
//! - [`walk`]: the object traversals behind `pre_randomize()` /
//! `post_randomize()` (Task C18, 18.6.2): which objects a `randomize()` call
//! runs the hooks of, and in what order.
//! - [`registry`]: per-class-template constraint programs and the
//! `randomize()` entry point the runtime's `Randomize` object op calls.
pub