CVC4 from Macports in OS X does not work with SAW/SBV

[robby-phd]

In OS X, SAW complains that it cannot find CVC4 executable if CVC4 is installed using Macports. A quick inspection indicates that it seems SBV cannot find CVC4 in /opt/local/bin, although it's installed there by Macports. Oddly, it works if one installs CVC4 pre-compiled binary downloaded from the CVC4 website (which interestingly, is created using Macports).

[brianhuffman]

Do you get a similar error with the Cryptol REPL if you use :set prover=cvc4?

[robby-phd]

Yup.

Main> :set prover=cvc4
Warning: cvc4 installation not found
Main> :prove correctSpeck32_64
*** An error occurred.
*** Failed to start the external solver: fd:54: hGetLine: end of file
*** Make sure you can start "/opt/local/bin/cvc4"
*** from the command line without issues.

[brianhuffman]

The relevant SBV code is at
https://github.com/LeventErkok/sbv/blob/master/Data/SBV/SMT/SMT.hs#L396 and
https://github.com/LeventErkok/sbv/blob/master/Data/SBV/SMT/SMT.hs#L495 .

It doesn't look like SBV is doing anything weird; it's possible the library functions for finding and running the executable are at fault. The relevant library functions are

• findExecutable from module System.Directory in package directory
• runInteractiveProcess from module System.Process in package process

Perhaps you could try running findExecutable "cvc4" from ghci on your system and see what you get?

[robby-phd]

findExecutable found the CVC4 executable at /opt/local/bin. Also, runInteractiveProcess seems to work using the following program (note: I'm not that familiar with Haskell):

import System.Process
import Control.Concurrent
import System.IO

main = do
  putStrLn "Running cvc4 ..."
  (inp, out, err, pid) <- runInteractiveProcess "cvc4" [] Nothing Nothing
  forkIO (hPutStrLn inp "EXIT;" >> hClose inp)
  forkIO (putStrLn =<< hGetContents out)
  forkIO (putStrLn =<< hGetContents err)
  threadDelay 1000000
  return ()

[robby-phd]

I tried the following SMT2 query. CVC4 works using runInteractiveProcess (but still does not work in Cryptol/SAW/SBV):

import System.Process
import Control.Concurrent
import System.IO

main = do
  putStrLn "Running cvc4 ..."
  (inp, out, err, pid) <- runInteractiveProcess "cvc4" ["--language", "smt2"] Nothing Nothing
  forkIO (hPutStrLn inp "(set-logic AUFLIA) \
                        \(declare-const l_n Int) \
                        \(declare-const l_r_0 Int) \
                        \(declare-const l_r Int) \
                        \(declare-const l_r_1 Int) \
                        \(assert (not (=> (and (> l_n (- 128)) (or (and (> l_n 0) (and (= l_r_0 0) (= l_r l_n))) (and (not (> l_n 0)) (and (= l_r_1 0) (= l_r (- l_n)))))) (>= l_r 0)))) \
                        \(check-sat)" >> hClose inp)
  forkIO (putStrLn =<< hGetContents out)
  forkIO (putStrLn =<< hGetContents err)
  threadDelay 1000000
  return ()

[atomb]

I think this is ultimately a problem with the MacPorts version of CVC4. The version I've compiled from source seems to work fine with the latest Cryptol, SAW, and SBV. In my experience, the MacPorts version of CVC4 has frequently crashed, while from-source builds from the latest GitHub code seem pretty stable. Feel free to re-open with more information if you still see this happening.

[linesthatinterlace]

I am having a similar issues with the Linux version of CVC4 (within WSL2, but that shouldn't make a difference). Cryptol and SAW cannot find CVC4, but findExecutable finds it, the above program runs (with a small modification, but not relevant I think...)

Is CVC4 still supported?