✨ refine SafeDivision interface, add tests

lsrcz · Feb 20, 2023 · 48cc7d3 · 48cc7d3
1 parent 84a2266
commit 48cc7d3
Show file tree

Hide file tree

Showing 27 changed files with 1,863 additions and 875 deletions.
diff --git a/grisette.cabal b/grisette.cabal
@@ -60,9 +60,9 @@ library
       Grisette.Core.Data.Class.ExtractSymbolics
       Grisette.Core.Data.Class.Function
       Grisette.Core.Data.Class.GenSym
-      Grisette.Core.Data.Class.Integer
       Grisette.Core.Data.Class.Mergeable
       Grisette.Core.Data.Class.ModelOps
+      Grisette.Core.Data.Class.SafeArith
       Grisette.Core.Data.Class.SimpleMergeable
       Grisette.Core.Data.Class.Solvable
       Grisette.Core.Data.Class.Solver
@@ -93,7 +93,7 @@ library
       Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
       Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
       Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
-      Grisette.IR.SymPrim.Data.Prim.PartialEval.Integer
+      Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
       Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
       Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
       Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
@@ -192,7 +192,7 @@ test-suite spec
       Grisette.IR.SymPrim.Data.Prim.BitsTests
       Grisette.IR.SymPrim.Data.Prim.BoolTests
       Grisette.IR.SymPrim.Data.Prim.BVTests
-      Grisette.IR.SymPrim.Data.Prim.IntegerTests
+      Grisette.IR.SymPrim.Data.Prim.IntegralTests
       Grisette.IR.SymPrim.Data.Prim.ModelTests
       Grisette.IR.SymPrim.Data.Prim.NumTests
       Grisette.IR.SymPrim.Data.Prim.TabularFunTests

diff --git a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
@@ -313,14 +313,38 @@ lowerSinglePrimImpl' config t@(GeneralFunApplyTerm _ (f :: Term (b --> a)) (arg
       addResult @integerBitWidth t g
       return g
     _ -> translateBinaryError "generalApply" (R.typeRep @(b --> a)) (R.typeRep @b) (R.typeRep @a)
-lowerSinglePrimImpl' config t@(DivIntegerTerm _ arg1 arg2) =
+lowerSinglePrimImpl' config t@(DivIntegralTerm _ arg1 arg2) =
   case (config, R.typeRep @a) of
-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm' config t arg1 arg2 SBV.sDiv
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sDiv
     _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
-lowerSinglePrimImpl' config t@(ModIntegerTerm _ arg1 arg2) =
+lowerSinglePrimImpl' config t@(ModIntegralTerm _ arg1 arg2) =
   case (config, R.typeRep @a) of
-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm' config t arg1 arg2 SBV.sMod
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sMod
     _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl' config t@(QuotIntegralTerm _ arg1 arg2) =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sQuot
+    _ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl' config t@(RemIntegralTerm _ arg1 arg2) =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sRem
+    _ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl' config t@(DivBoundedIntegralTerm _ arg1 arg2) =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sDiv
+    _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl' config t@(ModBoundedIntegralTerm _ arg1 arg2) =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sMod
+    _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl' config t@(QuotBoundedIntegralTerm _ arg1 arg2) =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sQuot
+    _ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl' config t@(RemBoundedIntegralTerm _ arg1 arg2) =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm' config t arg1 arg2 SBV.sRem
+    _ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
 lowerSinglePrimImpl' _ _ = undefined
 
 buildUTFun11 ::
@@ -699,14 +723,38 @@ lowerSinglePrimImpl config t@(GeneralFunApplyTerm _ (f :: Term (b --> a)) (arg :
       let g = l1 l2
       return (addBiMapIntermediate (SomeTerm t) (toDyn g) m2, g)
     _ -> translateBinaryError "generalApply" (R.typeRep @(b --> a)) (R.typeRep @b) (R.typeRep @a)
-lowerSinglePrimImpl config t@(DivIntegerTerm _ arg1 arg2) m =
+lowerSinglePrimImpl config t@(DivIntegralTerm _ arg1 arg2) m =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m
+    _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl config t@(ModIntegralTerm _ arg1 arg2) m =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m
+    _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl config t@(QuotIntegralTerm _ arg1 arg2) m =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sQuot m
+    _ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl config t@(RemIntegralTerm _ arg1 arg2) m =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sRem m
+    _ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl config t@(DivBoundedIntegralTerm _ arg1 arg2) m =
   case (config, R.typeRep @a) of
-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m
     _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
-lowerSinglePrimImpl config t@(ModIntegerTerm _ arg1 arg2) m =
+lowerSinglePrimImpl config t@(ModBoundedIntegralTerm _ arg1 arg2) m =
   case (config, R.typeRep @a) of
-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m
     _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl config t@(QuotBoundedIntegralTerm _ arg1 arg2) m =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sQuot m
+    _ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
+lowerSinglePrimImpl config t@(RemBoundedIntegralTerm _ arg1 arg2) m =
+  case (config, R.typeRep @a) of
+    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sRem m
+    _ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
 lowerSinglePrimImpl _ _ _ = error "Should never happen"
 
 bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r
@@ -1117,6 +1165,34 @@ pattern ResolvedNumType ::
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedNumType <- (resolveNumTypeView -> Just DictNumType)
 
+type SDivisibleTypeConstraint integerBitWidth s s' =
+  ( SimpleTypeConstraint integerBitWidth s s',
+    SBV.SDivisible (SBV.SBV s'),
+    Integral s
+  )
+
+data DictSDivisibleType integerBitWidth s where
+  DictSDivisibleType ::
+    forall integerBitWidth s s'.
+    (SDivisibleTypeConstraint integerBitWidth s s') =>
+    DictSDivisibleType integerBitWidth s
+
+resolveSDivisibleTypeView :: TypeResolver DictSDivisibleType
+resolveSDivisibleTypeView (ResolvedConfig {}, s) = case s of
+  IntegerType -> Just DictSDivisibleType
+  SignedBVType _ -> Just DictSDivisibleType
+  UnsignedBVType _ -> Just DictSDivisibleType
+  _ -> Nothing
+resolveSDivisibleTypeView _ = error "Should never happen, make compiler happy"
+
+pattern ResolvedSDivisibleType ::
+  forall integerBitWidth s.
+  (SupportedPrim s) =>
+  forall s'.
+  SDivisibleTypeConstraint integerBitWidth s s' =>
+  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
+pattern ResolvedSDivisibleType <- (resolveSDivisibleTypeView -> Just DictSDivisibleType)
+
 type NumOrdTypeConstraint integerBitWidth s s' =
   ( NumTypeConstraint integerBitWidth s s',
     SBV.OrdSymbolic (SBV.SBV s'),

diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
@@ -910,7 +910,7 @@ module Grisette.Core
     -- >>> let x = "x" :: SymInteger
     -- >>> let y = "y" :: SymInteger
     -- >>> assert = symAssertWith Assert
-    -- >>> sdiv = safeDiv Arith
+    -- >>> sdiv = safeDiv' (const Arith)
     -- >>> :{
     --   -- equivalent concrete program:
     --   -- let x = x `div` y
@@ -1026,10 +1026,10 @@ import Grisette.Core.Data.Class.Evaluate
 import Grisette.Core.Data.Class.ExtractSymbolics
 import Grisette.Core.Data.Class.Function
 import Grisette.Core.Data.Class.GenSym
-import Grisette.Core.Data.Class.Integer
 import Grisette.Core.Data.Class.Mergeable
 import Grisette.Core.Data.Class.ModelOps
 import Grisette.Core.Data.Class.SOrd
+import Grisette.Core.Data.Class.SafeArith
 import Grisette.Core.Data.Class.SimpleMergeable
 import Grisette.Core.Data.Class.Solvable
 import Grisette.Core.Data.Class.Solver