Module z3_synth 

Sprint 4A: Z3 Synthesis Constraint Builder

Converts a kernel spec type (Term) into a synthesis constraint. When tactics can’t construct a proof term directly, we ask Z3 to find one.

For a spec like Pi(a:Bit). Pi(b:Bit). Bit, this extracts:

• Inputs: [(a, Bit), (b, Bit)]
• Output: Bit
• Constraint: the function must map all 2^n inputs to valid outputs

Structs

SynthesisConstraintConfig

Configuration for synthesis constraint building.

Enums

SynthesisConstraint

Result of building a synthesis constraint.

Functions

build_synthesis_constraint

Convert a kernel Pi-typed specification into a synthesis constraint.

extract_io_from_spec

Extract input/output signal types from a kernel spec type.