Module solve 

Algebraic solver and bounded model checker for Trident constraint systems.

Takes the ConstraintSystem from sym.rs and checks it using:

1. Schwartz-Zippel testing: Evaluate polynomial constraints at random field points. If a polynomial identity holds at k random points over F_p, the probability it’s false is ≤ d/p where d is the degree. For our degrees (< 2^16) and Goldilocks p (≈ 2^64), this is negligibly small.

2. Bounded model checking: Enumerate concrete variable assignments and check all constraints. For programs with few free variables (< 20), we can check a large sample. For programs with many variables, we use random sampling with the Schwartz-Zippel guarantee.

3. Counterexample generation: When a constraint fails, report the concrete variable assignment that violates it.

4. Redundant assertion detection: Identify constraints that hold for all tested inputs (candidate tautologies) — these can be eliminated to reduce proving cost.

Structs

BmcConfig

Configuration for bounded model checking.

Counterexample

A concrete counterexample showing a constraint violation.

SolverConfig

Configuration for the solver.

SolverResult

Result of solving/checking a constraint system.

VerificationReport

Full verification result combining static analysis, random testing, and BMC.

Enums

Verdict

Functions

bounded_check

Run bounded model checking: test constraints against systematic value choices.

format_constraint

Format a constraint for human-readable display.

format_sym_value

Format a symbolic value for display (abbreviated).

solve

Solve a constraint system using random evaluation (Schwartz-Zippel) and bounded model checking.

verify

Run full verification: static + random + BMC.