pub fn build_synthesis_constraint(
spec_type: &Term,
config: &SynthesisConstraintConfig,
) -> SynthesisConstraintExpand description
Convert a kernel Pi-typed specification into a synthesis constraint.
Given a spec like Pi(a:Bit). Pi(b:Bit). Bit,
this determines whether the spec can be synthesized by:
- Extracting input/output types
- Checking all types are hardware types (Bit, BVec, Unit)
- Returning Satisfiable if the spec is well-formed