search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
242 stars 34 forks source link

Better parsing for bitwuzla output #723

Closed LeventErkok closed 2 months ago

LeventErkok commented 2 months ago 
satWith bitwuzla  $ ((uninterpret "f") :: SWord 8 -> SWord 8 -> SWord 8) 1 2 .== ((uninterpret "f") :: SWord 8 -> SWord 8 -> SWord 8) 2 3
Satisfiable. Model:
  f :: Word8 -> Word8 -> Word8
  f x = lambda (@bzla.var_11 (_ BitVec 8)) (ite (x == 2 && @bzla.var_11 == 3) 0 (ite (x == 1 && @bzla.var_11 == 2) 0 0))

surely we can do better here..

LeventErkok commented 2 months ago

New output is:

  f :: Word8 -> Word8 -> Word8
  f 2 3 = 0
  f 1 2 = 0
  f _ _ = 0