Variables remain undeclared when defined using specialized `sInt8,...` functions

[MrChico]

I noticed an oddity when trying out functions like sInt8, sList... from Data.SBV.Trans They seem to leave variables undeclared to the solver. freshVar works well however...

This fails:

import Data.SBV hiding (sInt8)
import Data.SBV.Control
import Data.SBV.Trans (sInt8)
trySIntQuery :: IO ()
trySIntQuery = runSMT $ query $ do
  d <- sInt8 "d"
  constrain $ d .== 0

with the error message:

*** Exception:
*** Data.SBV: Unexpected response from the solver, context: define-fun:
***
***    Sent      : (define-fun s2 () Bool (= s0 s1))
***    Expected  : success
***    Received  : (error "line 8 column 26: unknown constant s0")
***
***    Executable: /nix/store/c3mv21z0r2xkx7cyb8vcr14c1i98ikbi-z3-4.8.7/bin/z3
***    Options   : -nw -in -smt2

whereas this succeeds:

import Data.SBV hiding (sInt8)
import Data.SBV.Control
import Data.SBV.Trans (sInt8)
trySIntQuery :: IO ()
trySIntQuery = runSMT $ query $ do
  d <- freshVar "d" :: Query (SInt8)
  constrain $ d .== 0

am I using this function wrong or is this a bug?

[LeventErkok]

yeah, the idea is that you should only use sIntN/sWordN in the symbolic mode, and once you start the query mode always use freshVar.

But I do agree that this behavior is rather unexpected. I'll take a look. It should either be supported, or we should get a decent error message.

[LeventErkok]

@MrChico

Looking at this more, it's rather unfortunate that we have this separation of how we create variables in regular symbolic mode and in the query mode. But the reasons are rather historical and the code is hard to untangle now with little benefit.

I checked in some changes though, to improve the error message. You now get the following error for the program you posted:

*Main> trySIntQuery
*** Exception:
*** Data.SBV: Unsupported interactive/query mode feature.
***  Adding a new input variable in query mode: "d"
***
***  Hint: Use freshVar/freshVar_ for introducing new inputs in query mode.

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1029:24 in sbv-8.7.5-a974440a:Data.SBV.Core.Symbolic

I hope that's much more explanatory and helpful.

I'm closing this ticket; but please feel free to re-open it, and please continue to report any other oddities you find. Thanks!

[MrChico]

Sounds much clearer, nice!