dv-solve

Domain-agnostic CLP(FD) constraint solver. No Zuspec runtime dependency.

Install

pip install dv-solve

For Zuspec-powered benchmarks and tests:

pip install dv-solve[zuspec]

Quick start

from dv_solve.builder import SolveProblemBuilder
from dv_solve.ctx import SolveCtx, SOLVE_OK

b = SolveProblemBuilder()
x = b.add_variable("x", 0, 255, signed=False, bits=8)
b.add_constraint(b.gt(b.var(x), b.constant(100, 8)))
prob_bytes, _ = b.finalize()

ctx = SolveCtx(prob_bytes)
ctx.compile()
assert ctx.solve() == SOLVE_OK
print("x =", ctx.get_value(x))

Module map

Zuspec integration

Install zuspec-solver to wire this solver into zuspec-dataclasses randomization via the zuspec.solver.backend entry point.

Building the C library

cmake -S . -B build
cmake --build build

The shared library (libdv_solve.so) is installed alongside the Python package. The C source prefix (zsp_) will be renamed to dvs_ in a future release.