Code

Implement any-length BitVectors#335

Code

Draft

shingarov wants to merge 8 commits intopure-z3shingarov/MachineArithmetic:pure-z3from any-bvshingarov/MachineArithmetic:any-bvCopy head branch name to clipboard

+421-9

Commits

Commits on Sep 5, 2024

• [cosmetic] Groom instantiation of TAll

  shingarov

  committed
  4657e42

• Introduce class PAnyBV

  Show description for 91bd949
  shingarov

  committed
  91bd949

• Add RType>>#==>

  Show description for 413fce2
  shingarov

  committed
  413fce2

• Add convenience ΛBase>>bUnknown

  shingarov

  committed
  215ec13

• Introduce UndefinedElement

  shingarov

  committed
  1b77bec

• Add some temporary Sprite tests to assist in understanding AnyBVs

  shingarov

  committed
  9c4477b

• Add "bv?" to Sprite grammar (instantiating PAnyBV)

  shingarov

  committed
  9a6e374

• Silly attempt to unify BV lengths via BvSubstitution

  shingarov

  committed
  8d09e56