Support building with sbv-10.*

`sbv-10.*` brings in two changes to the SBV internals that affects SAW:

1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two
   separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions.
   We use the `generateSMTBenchmarkSat` variant in `SAWScript.Prover.Exporter`.
2. `sbv-10.0` changes the `Maybe [String]` argument to `svUninterpreted` (which
   we use in `saw-core-sbv`'s `Verifier.SAW.Simulator.SBV`) to a `UICodeKind`
   argument, where `UINone` is now what used to be denoted with `Nothing`.

We now use the appropriate CPP to make SAW compile before and after these
changes. See also GaloisInc/cryptol#1513, which was in similar territory.

saw-core-sbv/saw-core-sbv.cabal

@@ -20,7 +20,7 @@ library
     lens,
     mtl,
     saw-core,
-    sbv >= 9.1 && < 9.3,
+    sbv >= 9.1 && < 10.3,
     text,
     transformers,
     vector

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -37,6 +37,9 @@ module Verifier.SAW.Simulator.SBV
   ) where
 
 import Data.SBV.Dynamic
+#if MIN_VERSION_sbv(10,0,0)
+import Data.SBV.Internals (UICodeKind(..))
+#endif
 
 import Verifier.SAW.Simulator.SBV.SWord
 
@@ -667,7 +670,14 @@ parseUninterpreted cws nm ty =
     _ -> fail $ "could not create uninterpreted type for " ++ show ty
 
 mkUninterpreted :: Kind -> [SVal] -> String -> SVal
-mkUninterpreted k args nm = svUninterpreted k nm' Nothing args
+mkUninterpreted k args nm =
+  svUninterpreted k nm'
+#if MIN_VERSION_sbv(10,0,0)
+                  UINone
+#else
+                  Nothing
+#endif
+                  args
   where nm' = "|" ++ nm ++ "|" -- enclose name to allow primes and other non-alphanum chars
 
 sbvSATQuery :: SharedContext -> Map Ident SPrim -> SATQuery -> IO ([Labeler], [ExtCns Term], Symbolic SBool)

saw-script.cabal

@@ -84,7 +84,7 @@ library
     , saw-core-coq
     , saw-core-sbv
     , saw-core-what4
-    , sbv >= 9.1 && < 9.3
+    , sbv >= 9.1 && < 10.3
     , serialise
     , split
     , temporary

src/SAWScript/Prover/Exporter.hs

@@ -1,3 +1,4 @@
+{-# Language CPP #-}
 {-# Language GADTs #-}
 {-# Language ImplicitParams #-}
 {-# Language NamedFieldPuns #-}
@@ -299,8 +300,12 @@ write_smtlib2_w4 f (TypedTerm schema t) = do
 writeSMTLib2 :: FilePath -> SATQuery -> TopLevel ()
 writeSMTLib2 f satq = getSharedContext >>= \sc -> io $
   do (_, _, l) <- SBV.sbvSATQuery sc mempty satq
+#if MIN_VERSION_sbv(10,0,0)
+     txt <- SBV.generateSMTBenchmarkSat l
+#else
      let isSat = True -- l is encoded as an existential formula
      txt <- SBV.generateSMTBenchmark isSat l
+#endif
      writeFile f txt
 
 -- | Write a SAT query an SMT-Lib version 2 file.