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
240 stars 33 forks source link

Internal variables and lambdas don't work together #654

Closed LeventErkok closed 1 year ago

LeventErkok commented 1 year ago 
Prelude Data.SBV Data.SBV.Either> sat $ \(Exists x) -> isLeft x .&& fromLeft (x  :: SEither Bool Integer)
*** Exception:
*** Data.SBV: Impossible happened; saw inputs in lambda mode.
***
***   Inps    : [NamedSymVar l1_s3 "__internal_sbv_l1_s3"]
***   Trackers: []

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1880:39 in sbv-10.1-0a4a9dcf:Data.SBV.Core.Symbolic

This is because fromLeft/fromRight create an extra variable. (Need to dig back into why we do this, it escapes me now).

LeventErkok commented 1 year ago

Note that this isn't really about Exists.. But it's really about fromLeft, which introduces such variables. We'll have similar problems whenever we create an internal variable.

For instance, with tuples we don't have any such problem:

Prelude Data.SBV Data.SBV.Tuple> sat $ skolemize $ \(Exists @"x" x) -> (x :: STuple Bool Integer)^._1
Satisfiable. Model:
  x = (True,0) :: (Bool, Integer)