switch to Z3 for typechecking and proving

Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in
the 2.3 branch we will only have to change the default setting for the
typechecker.

README.md

@@ -37,17 +37,17 @@ On Mac OS X, Cryptol is also available via
 [Homebrew](http://brew.sh/). Simply run `brew update && brew install
 cryptol` to get the latest stable version.
 
-## Getting CVC4
+## Getting Z3
 
-Cryptol currently depends on the
-[CVC4 SMT solver](http://cvc4.cs.nyu.edu/) to solve constraints during
-type checking, and as the default solver for the `:sat` and `:prove`
-commands. You can download CVC4 binaries for a variety of platforms
-from their [download page](http://cvc4.cs.nyu.edu/downloads/). Note
-that if you install Cryptol using Homebrew, CVC4 will be installed
-automatically.
+Cryptol currently uses Microsoft Research's
+[Z3 SMT solver](https://github.com/Z3Prover/z3) by default to solve
+constraints during type checking, and as the default solver for the
+`:sat` and `:prove` commands. You can download Z3 binaries for a
+variety of platforms from their
+[releases page](https://github.com/Z3Prover/z3/releases). Note that if you
+install Cryptol using Homebrew, Z3 will be installed automatically.
 
-After installation, make sure that `cvc4` (or `cvc4.exe` on Windows)
+After installation, make sure that `z3` (or `z3.exe` on Windows)
 is on your PATH.
 
 # Building Cryptol From Source
@@ -64,9 +64,9 @@ Windows. We regularly build and test it in the following environments:
 
 ## Prerequisites
 
-Cryptol is developed using GHC 7.8.4 and cabal-install 1.22. The
-easiest way to get the correct versions is to follow the instructions
-on the
+Cryptol is developed using GHC 7.10.2 and cabal-install 1.22, though
+it is still tested with the previous major version of GHC. The easiest
+way to get the correct versions is to follow the instructions on the
 [haskell.org downloads page](https://www.haskell.org/downloads).
 
 Some supporting non-Haskell libraries are required to build
@@ -76,7 +76,7 @@ you may need to install the following:
 - [The GNU Multiple Precision Arithmetic Library (GMP)](https://gmplib.org/)
 - [ncurses](https://www.gnu.org/software/ncurses/)
 
-You'll also need [CVC4](#getting-cvc4) installed when running Cryptol.
+You'll also need [Z3](#getting-z3) installed when running Cryptol.
 
 ## Building Cryptol
 

docs/ProgrammingCryptol/highAssurance/HighAssurance.tex

@@ -349,13 +349,13 @@ user the proof is complete.\indQED\indProve
 \nb{Cryptol uses off-the-shelf SAT\glosSAT and SMT\glosSMT solvers to
   perform these formal
   proofs~\cite{erkok-matthews-cryptolEqChecking-09}.  By default,
-  Cryptol will use the CVC4 SMT solver~\cite{cvc4WWW} under the hood,
+  Cryptol will use Microsoft Research's Z3 SMT solver under the hood,
   but it can be configured to use other SAT/SMT solvers as well, such
-  as SRI's Yices~\cite{YicesWWW}\indYices, or Microsoft Research's
-  Z3~\cite{Z3WWW}\footnote{To do this, first install the package(s)
+  as SRI's Yices~\cite{YicesWWW}\indYices, or CVC4
+  ~\cite{cvc4WWW}\footnote{To do this, first install the package(s)
     from the URLs provided in the bibliography. Once a prover has been
     installed you can activate it with, for example, {\tt :set
-      prover=z3}.}. Note that the {\tt :prove} command is a
+      prover=cvc4}.}. Note that the {\tt :prove} command is a
   push-button tool: once the proof starts there is no user
   involvement. Of course, the external tool used may not be able to
   complete all the proofs in a feasible amount of time, naturally.

docs/ProgrammingCryptol/installation/Install.tex

@@ -261,7 +261,7 @@ aliases you have defined, along with their types.
      \texttt{base}            & \texttt{10}    & numeric base for printing words  \\
      \texttt{debug}           & \texttt{off}   & whether to print verbose debugging information \\
      \texttt{infLength}       & \texttt{5}     & number of elements to show from an infinite sequence \\
-     \texttt{prover}          & \texttt{cvc4}  & which SMT solver to use for \texttt{:prove}  \\
+     \texttt{prover}          & \texttt{z3}    & which SMT solver to use for \texttt{:prove}  \\
      \texttt{tests}           & \texttt{100}   & number of tests to run for \texttt{:check} \\
      \texttt{warnDefaulting}  & \texttt{on}    & \todo[inline]{talk to Iavor} \\
     \hline

src/Cryptol/REPL/Monad.hs

@@ -527,7 +527,7 @@ userOptions  = mkOptionMap
     "The number of random tests to try."
   , simpleOpt "satNum" (EnvString "1") checkSatNum
     "The maximum number of :sat solutions to display (\"all\" for no limit)."
-  , simpleOpt "prover" (EnvString "cvc4") checkProver $
+  , simpleOpt "prover" (EnvString "z3") checkProver $
     "The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
   , simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing)
     "Choose if we should display warnings when defaulting."
@@ -603,25 +603,25 @@ whenDebug m = do
 smokeTest :: REPL [Smoke]
 smokeTest = catMaybes <$> sequence tests
   where
-    tests = [ cvc4exists ]
+    tests = [ z3exists ]
 
 type SmokeTest = REPL (Maybe Smoke)
 
 data Smoke
-  = CVC4NotFound
+  = Z3NotFound
   deriving (Show, Eq)
 
 instance PP Smoke where
   ppPrec _ smoke =
     case smoke of
-      CVC4NotFound -> text . intercalate " " $ [
-          "[error] cvc4 is required to run Cryptol, but was not found in the"
-        , "system path. See the Cryptol README for more on how to install cvc4."
+      Z3NotFound -> text . intercalate " " $ [
+          "[error] z3 is required to run Cryptol, but was not found in the"
+        , "system path. See the Cryptol README for more on how to install z3."
         ]
 
-cvc4exists :: SmokeTest
-cvc4exists = do
-  mPath <- io $ findExecutable "cvc4"
+z3exists :: SmokeTest
+z3exists = do
+  mPath <- io $ findExecutable "z3"
   case mPath of
-    Nothing -> return (Just CVC4NotFound)
+    Nothing -> return (Just Z3NotFound)
     Just _  -> return Nothing

src/Cryptol/TypeCheck/Solver/Smtlib.hs

@@ -45,7 +45,7 @@ simpDelayed _qvars ordAsmp origAsmps goals =
   asmps = mapMaybe toPred (ordFactsToProps ordAsmp ++ origAsmps)
 
   tryGoal g = case toPred (goal g) of
-                Just q -> do res <- cvc4 (toScript vs asmps q)
+                Just q -> do res <- z3 (toScript vs asmps q)
                              return (g, res == Unsat)
                               -- i.e., solved for Nats, anyway
                 Nothing -> return (g, False)
@@ -124,35 +124,35 @@ toScript vs pes q =
 data SMTResult = Sat | Unsat | Unknown
                   deriving (Eq,Show)
 
--- | First look for @cvc4@ in the path, but failing that, assume that it's 
+-- | First look for @z3@ in the path, but failing that, assume that it's 
 -- installed side-by-side with Cryptol.
-findCvc4 :: IO FilePath
-findCvc4 = do
-  mfp <- findExecutable "cvc4"
+findZ3 :: IO FilePath
+findZ3 = do
+  mfp <- findExecutable "z3"
   case mfp of
     Just fp -> return fp
     Nothing -> do
      bindir <- takeDirectory `fmap` getExecutablePath
-     return (bindir </> "cvc4")
+     return (bindir </> "z3")
 
-cvc4 :: SMT.Script -> IO SMTResult
-cvc4 script =
+z3 :: SMT.Script -> IO SMTResult
+z3 script =
   X.handle (\(_::X.IOException) -> return Unknown) $
   do let txt = show (SMT.pp script)
-     cvc4path <- findCvc4
-     (ex,out,err) <- readProcessWithExitCode cvc4path ["--lang=smtlib2","--rewrite-divk","-"] txt
+     z3path <- findZ3
+     (ex,out,err) <- readProcessWithExitCode z3path ["-smt2","-in"] txt
      case ex of
        ExitFailure 10  -> return Sat
        ExitFailure 20  -> return Unsat
-       ExitFailure 127 -> return Unknown -- cvc4 program not found
+       ExitFailure 127 -> return Unknown -- z3 program not found
        ExitSuccess
          | out == "sat\n"     -> return Sat
          | out == "unsat\n"   -> return Unsat
-         | out == "unknwon\n" -> return Unknown
+         | out == "unknown\n" -> return Unknown
 
        -- XXX: We should not print to STDOUT here.
        -- Report to a separate logger.
-       x -> do putStrLn "Called to CVC4 failed!!!"
+       x -> do putStrLn "Called to Z3 failed!!!"
                putStrLn ("Exit code: " ++ show x)
                putStrLn "Script"
                putStrLn txt

tests/issues/issue066.icry.stdout

@@ -4,9 +4,9 @@ it : {result : Bit, arg1 : [4]}
 
 Run-time error: no counterexample available
 True
-f 0x0 = False
+f 0xc = False
 it : {result : Bit, arg1 : [4]}
-{result = False, arg1 = 0x0}
+{result = False, arg1 = 0xc}
 False
 f 0x3 = True
 it : {result : Bit, arg1 : [4]}
@@ -16,9 +16,9 @@ Unsatisfiable
 it : {result : Bit, arg1 : [4]}
 
 Run-time error: no satisfying assignment available
-g {x = 0x00000000, y = 0x00000001} = False
+g {x = 0xffffffff, y = 0x00000000} = False
 it : {result : Bit, arg1 : {x : [32], y : [32]}}
-{result = False, arg1 = {x = 0x00000000, y = 0x00000001}}
+{result = False, arg1 = {x = 0xffffffff, y = 0x00000000}}
 g {x = 0x00000000, y = 0x00000000} = True
 it : {result : Bit, arg1 : {x : [32], y : [32]}}
 {result = True, arg1 = {x = 0x00000000, y = 0x00000000}}

tests/issues/issue072.icry.stdout

@@ -1,30 +1,30 @@
 Loading module Cryptol
-(\x -> x > 0x4) 0x5 = True
-it : {result : Bit, arg1 : [4]}
-{result = True, arg1 = 0x5}
-(\x -> x > 0x4) 0x5 = True
 (\x -> x > 0x4) 0x6 = True
-(\x -> x > 0x4) 0x7 = True
+it : {result : Bit, arg1 : [4]}
+{result = True, arg1 = 0x6}
+(\x -> x > 0x4) 0x6 = True
 (\x -> x > 0x4) 0x8 = True
+(\x -> x > 0x4) 0x5 = True
+(\x -> x > 0x4) 0x7 = True
+(\x -> x > 0x4) 0xd = True
+(\x -> x > 0x4) 0xc = True
 (\x -> x > 0x4) 0x9 = True
 (\x -> x > 0x4) 0xa = True
-(\x -> x > 0x4) 0xb = True
-(\x -> x > 0x4) 0xc = True
-(\x -> x > 0x4) 0xd = True
 (\x -> x > 0x4) 0xe = True
 (\x -> x > 0x4) 0xf = True
+(\x -> x > 0x4) 0xb = True
 it : [11]{result : Bit, arg1 : [4]}
-[{result = True, arg1 = 0x5}, {result = True, arg1 = 0x6},
- {result = True, arg1 = 0x7}, {result = True, arg1 = 0x8},
+[{result = True, arg1 = 0x6}, {result = True, arg1 = 0x8},
+ {result = True, arg1 = 0x5}, {result = True, arg1 = 0x7},
+ {result = True, arg1 = 0xd}, {result = True, arg1 = 0xc},
  {result = True, arg1 = 0x9}, {result = True, arg1 = 0xa},
- {result = True, arg1 = 0xb}, {result = True, arg1 = 0xc},
- {result = True, arg1 = 0xd}, {result = True, arg1 = 0xe},
- {result = True, arg1 = 0xf}]
+ {result = True, arg1 = 0xe}, {result = True, arg1 = 0xf},
+ {result = True, arg1 = 0xb}]
 must be an integer > 0 or "all"
 must be an integer > 0 or "all"
-(\x -> x > 0x4) 0x5 = True
 (\x -> x > 0x4) 0x6 = True
-(\x -> x > 0x4) 0x7 = True
+(\x -> x > 0x4) 0x8 = True
+(\x -> x > 0x4) 0x5 = True
 it : [3]{result : Bit, arg1 : [4]}
-[{result = True, arg1 = 0x5}, {result = True, arg1 = 0x6},
- {result = True, arg1 = 0x7}]
+[{result = True, arg1 = 0x6}, {result = True, arg1 = 0x8},
+ {result = True, arg1 = 0x5}]

tests/issues/issue093.icry.stdout

@@ -27,4 +27,4 @@ Coverage: 0.00% (100 of 2^^64 values)
 :sat t1
 	t1 0x00000000 = True
 :sat t2
-	t2 0x00000000 0x00000000 = True
+	t2 0xfffffffe 0xffffffff = True

tests/issues/issue289.icry.stdout

@@ -2,5 +2,5 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 Q.E.D.
-av1 0xc00001c9 0xbfffffd5 = False
+av1 0xfdffffe0 0x7fffffe0 = False
 Q.E.D.

tests/regression/r03.icry.stdout

@@ -1,5 +1,5 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module r03
-(nQueens : Solution 5) [0x4, 0x2, 0x0, 0x3, 0x1] = True
+(nQueens : Solution 5) [0x3, 0x1, 0x4, 0x2, 0x0] = True
 (nQueensProve : Solution 4) [0x2, 0x0, 0x3, 0x1] = False