🔀 Merge pull request #66 from lsrcz/fix-sbv-10+

Fix compatibility with sbv 10+
lsrcz · May 8, 2023 · f7697ac · f7697ac
2 parents cafaa89 + 7504613
commit f7697ac
Show file tree

Hide file tree

Showing 4 changed files with 28 additions and 8 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -20,8 +20,8 @@ jobs:
         - { build: stack, arg: "", ismain: true, experimental: false, ghc: "902", cachekey: "stack" }
         - { build: stack, arg: "--stack-yaml stack-lts-20.9.yaml", ismain: false, experimental: false, ghc: "925", cachekey: "stack-20.9" }
         - { build: stack, arg: "--stack-yaml stack-nightly.yaml", ismain: false, experimental: false, ghc: "944", cachekey: "stack-nightly" }
-        - { build: cabal, arg: "", ismain: false, experimental: false, ghc: "8107", cachekey: "cabal-8107" }
-        - { build: cabal, arg: "", ismain: false, experimental: false, ghc: "902", cachekey: "cabal-902" }
+        - { build: cabal, arg: "--constraint=sbv<10", ismain: false, experimental: false, ghc: "8107", cachekey: "cabal-8107" }
+        - { build: cabal, arg: "--constraint=sbv<10", ismain: false, experimental: false, ghc: "902", cachekey: "cabal-902" }
         - { build: cabal, arg: "", ismain: false, experimental: false, ghc: "925", cachekey: "cabal-925" }
         - { build: cabal, arg: "", ismain: false, experimental: false, ghc: "944", cachekey: "cabal-944" }
 
@@ -81,7 +81,7 @@ jobs:
             ;;
           cabal)
             nix develop --allow-dirty --no-warn-dirty -c cabal update
-            nix develop --allow-dirty --no-warn-dirty -c cabal run spec -- --xml=test-report.xml
+            nix develop --allow-dirty --no-warn-dirty -c cabal run spec $ARGS -- --xml=test-report.xml
             ;;
         esac
         set +ex

diff --git a/grisette.cabal b/grisette.cabal
@@ -131,7 +131,7 @@ library
     , mtl >=2.2.2 && <2.3
     , once >=0.2 && <0.5
     , parallel
-    , sbv >=8.11 && <9.1
+    , sbv >=8.11 && <10.2
     , template-haskell >=2.16 && <2.20
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.6
@@ -167,7 +167,7 @@ test-suite doctest
     , mtl >=2.2.2 && <2.3
     , once >=0.2 && <0.5
     , parallel
-    , sbv >=8.11 && <9.1
+    , sbv >=8.11 && <10.2
     , template-haskell >=2.16 && <2.20
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.6
@@ -216,7 +216,7 @@ test-suite spec
     , mtl >=2.2.2 && <2.3
     , once >=0.2 && <0.5
     , parallel
-    , sbv >=8.11 && <9.1
+    , sbv >=8.11 && <10.2
     , tasty >=1.1.0.3 && <1.5
     , tasty-hunit ==0.10.*
     , tasty-quickcheck >=0.10.1 && <0.11

diff --git a/package.yaml b/package.yaml
@@ -39,7 +39,7 @@ dependencies:
 - array >= 0.5.4 && < 0.6
 - vector >= 0.12.1 && < 0.14
 - once >= 0.2 && < 0.5
-- sbv >= 8.11 && < 9.1
+- sbv >= 8.11 && < 10.2
 - parallel
 
 flags: {

diff --git a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -827,8 +828,27 @@ bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r
 bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of
   Refl -> r1
 
+#if MIN_VERSION_sbv(10,0,0)
+preprocessUIFuncs ::
+  [(String, (SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
+  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
+preprocessUIFuncs =
+  traverse
+    (\case
+      (a, (b, Right c)) -> Just (a, (b, c))
+      _ -> Nothing)
+#else
+preprocessUIFuncs ::
+  [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
+  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
+preprocessUIFuncs = Just
+#endif
+
 parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model
-parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs
+parseModel _ (SBVI.SMTModel _ _ assoc orguifuncs) mp =
+  case preprocessUIFuncs orguifuncs of
+    Just uifuncs -> foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs
+    _ -> error "SBV Failed to parse model"
   where
     goassoc :: (String, SBVI.CV) -> PM.Model -> PM.Model
     goassoc (name, cv) m = case findStringToSymbol name mp of