Repository navigation

Bound the FiveTuple rescaling by the encoded depth, in SMT and MILP (#65) - #88

Merged

ondrik merged 5 commits into

fix/65-rescaling-bound

Oct 26, 2026

Merged

Bound the FiveTuple rescaling by the encoded depth, in SMT and MILP (#65)#88
ondrik merged 5 commits into
masterfrom
fix/65-rescaling-bound

Commits on Oct 26, 2026
- fix: bound the FiveTuple rescaling by the depth, not by the input's max_k
  
  ondrik
  and
  claude
  committed
  8cde44b
- fix: reject a non-integral FiveTuple k in vector pairs
  
  ondrik
  and
  claude
  committed
  6e5e6ce
- fix: integral_k check before synthesis even begins -- crashed pysmt before
  
  jkhav
  authored and
  ondrik
  committed
  eede8f6
- fix: bound the MILP FiveTuple rescaling by the encoded depth (#65)
  
  jkhav
  authored and
  ondrik
  committed
  79bfe6b
- fix: declare the target's rescaled vector at every depth
  
  ondrik
  and
  claude
  committed
  594b542