opened
gramseyer
username_0
Hello,

I get the following error when running yices 2.5.4 (QF_NRA logic, no options) from sbv.
 *** Data.SBV: Unexpected response from the solver.
 ***    Context : getModel
 ***    Sent    : (get-value (s0))
 ***    Expected: a value binding for kind: SReal
 ***    Received: ((s0 1))

The value (1) is correct, and is indeed what yices returns when I translate the problem into smtlib and run it directly.  The solver also works correctly when I adjust my problems slightly (a translation in a 2d geometry problem) so that none of the resulting variables is an integer.
Yices AlgReal Parse Error
issue
created
LeventErkok
username_1
Hi @username_0, thanks for the report.

I think this is fixed in the head about two weeks ago with this commit: https://github.com/username_1/sbv/commit/067090798916bb7f53e916990e21ea021d6b2645

Any chance you can build from github and give it a shot?
comment
created
gramseyer
username_0
Thanks for the quick response.  I just built from source, but unfortunately I still get the error.

This shouldn't change yices output, but for what its worth, my queries are all in QF_NRA and thus are routing to the separate mcsat solver in yices.
comment
created
LeventErkok
username_1
Interesting. Would it be possible for you to give me some SBV code that replicates the issue? The shorter the better, but don't worry about making it minimal.
comment
created
gramseyer
username_0
Here's something close to minimal that reproduces the error.

I need to disable incremental solving because the yices nonlinear solver does not support incremental solving.

basic :: IO ()
basic = runSMTWith (disableIncrementalConfig yices) basic'
basic' :: Symbolic ()
basic' = do
    x <- sReal "x"
    constrain $ x .== (fromInteger 0)
    setLogic QF_NRA -- QF_LRA also gives the error
    result <- query $ do
        cs <- getSMTResult
       return ()
    return ()

disableIncremental :: SMTSolver -> SMTSolver
disableIncremental solver = solver { options = const []}

disableIncrementalConfig :: SMTConfig -> SMTConfig
disableIncrementalConfig config = config { solver = disableIncremental (solver config) }
comment
created
LeventErkok
username_1
Thanks! I just pushed a fix, can you give it a try?
comment
closed
gramseyer
username_0
issue
created
gramseyer
username_0
That fixed it!  Thanks!
comment
created
LeventErkok
username_1
Great.. A new hackage release will come out sometime this weekend. Please feel free to report other issues if you come across anything else.
comment
created
LeventErkok
username_1
@username_0 Just a comment on changing the options to Yices. This is a pain, and actually the easiest way to do so is to use the environment variable `SBV_YICES_OPTIONS`.

Programmatically, something like this would achieve the same effect:

```
import System.Posix.Env

basic :: IO ()
basic = do setEnv "SBV_YICES_OPTIONS" "" True
           runSMTWith yices basic'
```

But it's a lot easier to use from the shell, as you can simply set it to empty string and run ghci/your-program directly with that setting easily.

Note that `setEnv` from `System.Environment` deletes the env-var if you set something to an empty-string; so you really need to use the one from `System.Posix.Env`.
comment
created
LeventErkok
username_1
@username_0 SBV 7.4 is now out on hackage, which contains this fix.
comment