Contact initiation with CVC4 fails

[finnteegen]

Hello again,

when I try to use CVC4 as a solver via runSMTWith cvc4 I get the following error message on the console.

*** Exception:
*** Data.SBV: Failed to initiate contact with the solver!
***
***   Sent    : (set-option :print-success true)
***   Expected: success
***   Received: (set-option :print-success true)
***
*** Try running in debug mode for further information.

It seems to be as if the input command is printed and parsed again instead of the actual result output. Executing cvc4 manually with a subset of options used by SBV (namely executing echo '(set-option :print-success true)' | cvc4 --lang smt --interactive --no-interactive-prompt) indicates that CVC4 indeed outputs the input (which is falsely parsed) before printing the result.

Cheers, Finn

[LeventErkok]

I can't replicate this:

import Data.SBV
import Data.SBV.Control

t :: IO ()
t = runSMTWith cvc4{verbose=True} $ do
        x <- sBool "x"

        query $ do cs <- checkSat
                   case cs of
                     Sat -> do xv <- getValue x
                               io $ print xv
                     _   -> error $ "solver said: " ++ show cs

I get:

*Main> t
** Calling: cvc4 --lang smt --incremental --interactive --no-interactive-prompt --model-witness-value
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; external query, using all logics.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Bool) ; tracks user variable "x"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- preQuantifier assignments ---
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] ; --- formula ---
[GOOD] ; --- postQuantifier assignments ---
[GOOD] ; --- delayedEqualities ---
[GOOD] ; -- finalAssert ---
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 false))
False
*** Solver   : CVC4
*** Exit code: ExitSuccess
*** Std-out  :

It could be that you've a different version of cvc4:

$ cvc4 --version
This is CVC4 version 1.8
compiled with GCC version Apple LLVM 12.0.0 (clang-1200.0.32.29)
on May 13 2021 16:23:34

See if you can upgrade your CVC4 to something newer. (Or if you have a newer version than the above, let me know and I'll upgrade mine.)

Note that cvc4 is being replaced by cvc5; so you might want to switch to that instead. (SBV supports CVC5 too: https://cvc5.github.io)

[finnteegen]

That is interesting, because I use version 1.8 as well.

$ cvc4 --version
This is CVC4 version 1.8
compiled with GCC version 11.1.1 20210623 (Red Hat 11.1.1-6)
on Jul 21 2021 00:00:00

With your test program I get the exact same error message.

[LeventErkok]

When I run:

$ echo '(set-option :print-success true)' | cvc4 --lang smt --interactive --no-interactive-prompt
success

So, if you're seeing some other behavior; that'd trip SBV up.

I'm not sure why you'd see something else, perhaps you've multiple versions of cvc4 installed? Or maybe some funky terminal settings? But doesn't look like this have much to do with SBV at this point.

[finnteegen]

My console output when running the command is the following.

$ echo '(set-option :print-success true)' | cvc4 --lang smt --interactive --no-interactive-prompt
(set-option :print-success true)
success

My colleague has the exact same output and therefore the same problem. However, we are both running Linux instead of Mac OS (although different distributions). Don't know if this could have anything to do with it.

[LeventErkok]

Yes, that first line of output is definitely the culprit here. I just tried on a Linux box:

$ echo '(set-option :print-success true)' | cvc4 --lang smt --interactive --no-interactive-prompt
success

(The above is with CVC 1.6 but I doubt this behavior would depend on the CVC version.)

So, it seems something really bizarre with your installation there. Check if the cvc4 executable is a redirection to some other binary/wrapper perhaps? If not, and given that cvc5 is replacing cvc4, I recommend downloading and using cvc5 instead (https://cvc5.github.io).

Again, I don't see anything SBV can do here, as I can't replicate the issue neither on Mac nor on Linux.

[finnteegen]

Based on your remark that you tried version 1.6, I quickly tried version 1.6, 1.7, and 1.8 and it turned out that the behavior has indeed changed with version 1.8 (though I do not know why). With version 1.6 and 1.7 I get the behavior you describe (and which seems to be expected within SBV), while version 1.8 behaves differently.

Perhaps, SBV could take CVC4's version into account and adjust its communication? Nonetheless, I will consider using CVC5 as you mentioned and, for now, use version 1.7 of CVC4.

[LeventErkok]

Given this is a Linux only thing with only on some versions, I think this should be addressed by CVC folks. Clearly it's a bug somewhere down the pipe that impacts only some variants, and it'd be a fool's errand for SBV to track each version and behave differently. (There'd be way too many behaviors to handle if we go down this path.) You can of course report it to CVC4 people; but most likely they'll tell you to use CVC5 as well.

I'm closing this ticket as there's nothing for SBV to do here. Feel free to reopen if you upgrade to CVC5 and find similar issues.