Solvers and diagnostics¶

Randomized transaction classes produce a backend-neutral constraint problem. The backend decides how to find a satisfying assignment, but it does not change the transaction API, seed source, or field access.

Choose a backend¶

Backend	Dependency	Best fit	Failure knowledge
`AdaptiveConstraintBackend`	None; optional fallback chosen by the application	Default policy: sample common constraints and invoke a configured solver only after genuine search exhaustion	Preserves the result and diagnostics from the engine that ran
`RandomSearchBackend`	None	Ranges, membership, distributions, and constraints with reasonable acceptance	Proves empty direct domains; otherwise distinguishes search exhaustion
`Z3RandomBackend`	Z3 for translation units that include it	Tightly coupled arithmetic or models whose legal assignments are sparse	Proves unsatisfiability and reports named hard constraints from an unsat core

The dependency-free adaptive policy is the default. It uses deterministic sampling with a 4096-candidate budget. Without a configured fallback, exhaustion remains an actionable SearchExhausted result. Z3 is optional: use it only in applications that need sparse solving or proof-quality diagnostics.

Default deterministic search¶

Packet packet;
test.randomize(packet); // AdaptiveConstraintBackend sampling fast path

The backend folds simple bounds and inside() sets into candidate domains, applies active distributions within those domains, prefers satisfiable soft constraints, and tests the remaining expressions. The default search budget is 4096 candidates.

Standalone code can choose another budget:

RandomSearchBackend search{16384};
Random random{0x1234};

const RandomizeResult result = packet.randomize(random, search);

A SearchExhausted result does not mean the model is impossible. Its message lists named constraints and rejection counts and suggests Z3RandomBackend when deterministic sampling could not find a solution.

Adaptive Z3 fallback¶

Configure one policy object when most models are inexpensive but a few need a solver:

#include "cpptb/z3_random_backend.hpp"

Z3RandomBackend z3_only{0};
AdaptiveConstraintBackend constraints{z3_only};

Task<void> packet_sequence(Dut dut, TestContext& test) {
    test.set_random_backend(constraints);

    Packet packet;
    test.randomize(packet); // samples first, falls back only on exhaustion
    co_await drive_packet(dut, packet);
}

Construct the fallback Z3 backend with 0 because the adaptive policy already performed the sampling pass. Both backend objects must outlive every test.randomize() call that uses them.

Applications that deliberately use the process-wide default policy can install the same fallback once:

Z3RandomBackend z3_only{0};
default_adaptive_constraint_backend().set_fallback(z3_only);

Keep z3_only alive for the complete test run. Explicit per-test policy is usually easier to isolate and reason about.

Optional direct Z3 backend¶

Only code that selects Z3 needs its header and linker dependency:

#include "cpptb/z3_random_backend.hpp"

Task<void> coupled_sequence(Dut dut, TestContext& test) {
    Z3RandomBackend z3;
    test.set_random_backend(z3);

    CoupledTransaction item;
    test.randomize(item);
    co_await drive_transaction(dut, item);
}

With the installed CMake package, enable the optional adapter when building cpptb and link its explicit target:

cmake -S . -B build -DCPPTB_WITH_Z3=ON

target_link_libraries(my_testbench PRIVATE cpptb::z3)

For a non-CMake build, add the compiler and linker flags reported by:

pkg-config --cflags --libs z3

Z3RandomBackend first runs a small deterministic fast search, then invokes Z3 when needed. Construct it with 0 to force every solve through Z3:

Z3RandomBackend z3_only{0};
test.set_random_backend(z3_only);

Satisfying Z3 models are selected using the same test random stream. The same seed replays; different seeds can select different valid assignments. Membership, distribution support, soft preference, and independent RandC cycles retain their user-visible semantics across both backends.

The backend object must outlive every test.randomize() call that uses it. TestContext stores a reference, not an owning copy.

Z3 caches the translated persistent model for each Randomized object. Repeated solves, including randomize_with() calls, reuse it; changing a constraint or distribution mode invalidates that object’s cached model. cache_builds(), cache_hits(), and clear_cache() are available for focused diagnostics and tests.

Result metadata¶

Structured test result schema 5 records:

{
  "constraint_backend": "adaptive",
  "constraint_backend_version": "4.13.3.0",
  "random_sampling_solves": 999,
  "random_solver_solves": 1
}

The version is supplied by the configured fallback when present. The solve counters report the engine that actually produced each result, making replay and performance reports distinguish an inexpensive sampling run from solver fallback.

Failure statuses¶

Status	Meaning	Typical response
`Solved`	A complete assignment was produced	Use the fields
`Unsatisfiable`	The backend proved the active hard model has no solution	Fix conflicting constraints or modes
`SearchExhausted`	Sampling used its candidate budget without finding a solution	Inspect rejection counts, increase attempts, or use Z3
`CycleExhausted`	Internal signal that one or more `RandC` domains completed	The owning `Randomized` object resets only those cycles and retries automatically
`BackendError`	Invalid model, incompatible policies, malformed backend result, or misuse	Follow the actionable message

test.randomize() converts any externally visible failure into a fatal test requirement at the call site. Call item.randomize(random, backend) directly when code needs to branch on status.

Write useful constraint names¶

Names are part of the diagnostic surface:

constraint("DMA length is a whole beat", length % beat_bytes == 0);
constraint("atomic requests stay in one cache line",
           opcode != Opcode::Atomic || length <= cache_line_bytes);

Prefer a stable statement of intent over an expression transcription. Search diagnostics report which named constraints rejected candidates; Z3 unsat cores report the named hard constraints needed for the contradiction. Nested object labels are qualified automatically, such as header.default route.

Common errors¶

Message shape	Cause
`minimum exceeds maximum`	A field, `range()`, or `randint()` was constructed with reversed bounds
`multiple active distributions`	More than one enabled `dist()` policy targets the same field
`distribution ... has no legal values`	Hard constraints removed the complete weighted support
`nested randomized object ... must be randomized through its owning object`	A child was solved independently of its root
`search exhausted ... rejected N`	Legal assignments were too sparse for the configured search budget
`returned the wrong assignment size`	A custom backend violated the `ConstraintBackend` contract

Backend extension point¶

A custom backend implements one small interface:

class ConstraintBackend {
  public:
    virtual std::string_view name() const noexcept = 0;
    virtual std::string_view version() const noexcept { return {}; }
    virtual RandomizeResult solve(const ConstraintProblem& problem,
                                  Random& random) = 0;
};

The problem carries typed field descriptors, named hard and soft constraints, active distributions, and current RandC exclusions. A backend must return one raw assignment per variable and use the supplied Random for replayable model selection. Backend-specific types should not leak into transaction classes.