grisette 0.7.0.0 → 0.8.0.0

raw patch · 159 files changed

+17139/−7456 lines, 159 filesdep +libBFdep +th-lift-instancesdep −GlobPVP ok

version bump matches the API change (PVP)

Dependencies added: libBF, th-lift-instances

Dependencies removed: Glob

API changes (from Hackage documentation)

Files

• CHANGELOG.md +72/−1
• README.md +19/−5
• doctest/Main.hs +28/−3
• grisette.cabal +50/−15
• src/Grisette/Backend.hs +4/−7
• src/Grisette/Core.hs +92/−45
• src/Grisette/Experimental.hs +8/−0
• src/Grisette/Experimental/GenSymConstrained.hs +5/−3
• src/Grisette/Experimental/MonadParallelUnion.hs +0/−1
• src/Grisette/Experimental/Qualified/ParallelUnionDo.hs +2/−0
• src/Grisette/Internal/Backend/QuantifiedStack.hs +86/−0
• src/Grisette/Internal/Backend/Solving.hs +392/−348
• src/Grisette/Internal/Backend/SymBiMap.hs +72/−13
• src/Grisette/Internal/Core/Control/Monad/CBMCExcept.hs +10/−9
• src/Grisette/Internal/Core/Control/Monad/Union.hs +7/−8
• src/Grisette/Internal/Core/Data/Class/BitCast.hs +49/−1
• src/Grisette/Internal/Core/Data/Class/BitVector.hs +0/−5
• src/Grisette/Internal/Core/Data/Class/CEGISSolver.hs +5/−9
• src/Grisette/Internal/Core/Data/Class/Error.hs +2/−4
• src/Grisette/Internal/Core/Data/Class/EvalSym.hs +31/−10
• src/Grisette/Internal/Core/Data/Class/ExtractSym.hs +195/−110
• src/Grisette/Internal/Core/Data/Class/Function.hs +0/−7
• src/Grisette/Internal/Core/Data/Class/GenSym.hs +9/−6
• src/Grisette/Internal/Core/Data/Class/IEEEFP.hs +85/−249
• src/Grisette/Internal/Core/Data/Class/ITEOp.hs +7/−5
• src/Grisette/Internal/Core/Data/Class/LogicalOp.hs +16/−5
• src/Grisette/Internal/Core/Data/Class/Mergeable.hs +150/−132
• src/Grisette/Internal/Core/Data/Class/ModelOps.hs +19/−19
• src/Grisette/Internal/Core/Data/Class/PPrint.hs +92/−26
• src/Grisette/Internal/Core/Data/Class/SafeBitCast.hs +141/−0
• src/Grisette/Internal/Core/Data/Class/SafeDiv.hs +475/−0
• src/Grisette/Internal/Core/Data/Class/SafeDivision.hs +0/−290
• src/Grisette/Internal/Core/Data/Class/SafeFdiv.hs +153/−0
• src/Grisette/Internal/Core/Data/Class/SafeFromFP.hs +265/−0
• src/Grisette/Internal/Core/Data/Class/SafeLogBase.hs +86/−0
• src/Grisette/Internal/Core/Data/Class/SimpleMergeable.hs +2/−0
• src/Grisette/Internal/Core/Data/Class/Solvable.hs +0/−2
• src/Grisette/Internal/Core/Data/Class/Solver.hs +4/−4
• src/Grisette/Internal/Core/Data/Class/SubstSym.hs +39/−27
• src/Grisette/Internal/Core/Data/Class/SymEq.hs +73/−12
• src/Grisette/Internal/Core/Data/Class/SymFiniteBits.hs +206/−0
• src/Grisette/Internal/Core/Data/Class/SymFromIntegral.hs +110/−0
• src/Grisette/Internal/Core/Data/Class/SymIEEEFP.hs +125/−0
• src/Grisette/Internal/Core/Data/Class/SymOrd.hs +12/−7
• src/Grisette/Internal/Core/Data/Class/ToCon.hs +9/−4
• src/Grisette/Internal/Core/Data/Class/ToSym.hs +82/−24
• src/Grisette/Internal/Core/Data/Symbol.hs +12/−1
• src/Grisette/Internal/SymPrim/AlgReal.hs +182/−0
• src/Grisette/Internal/SymPrim/AllSyms.hs +5/−3
• src/Grisette/Internal/SymPrim/BV.hs +17/−13
• src/Grisette/Internal/SymPrim/FP.hs +621/−34
• src/Grisette/Internal/SymPrim/FunInstanceGen.hs +253/−0
• src/Grisette/Internal/SymPrim/GeneralFun.hs +301/−461
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/BVPEval.hs +77/−75
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalBitCastTerm.hs +135/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalBitwiseTerm.hs +2/−2
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalDivModIntegralTerm.hs +11/−13
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalFP.hs +92/−8
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalFloatingTerm.hs +34/−5
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalFractionalTerm.hs +46/−3
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalFromIntegralTerm.hs +176/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalIEEEFPConvertibleTerm.hs +298/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalNumTerm.hs +42/−35
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalOrdTerm.hs +26/−22
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalRotateTerm.hs +12/−10
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalShiftTerm.hs +6/−4
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/SupportedPrim.hs +204/−108
• src/Grisette/Internal/SymPrim/Prim/Internal/IsZero.hs +0/−44
• src/Grisette/Internal/SymPrim/Prim/Internal/PartialEval.hs +12/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs +3125/−2706
• src/Grisette/Internal/SymPrim/Prim/Internal/Unfold.hs +14/−9
• src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs +8/−0
• src/Grisette/Internal/SymPrim/Prim/Model.hs +131/−471
• src/Grisette/Internal/SymPrim/Prim/SomeTerm.hs +7/−1
• src/Grisette/Internal/SymPrim/Prim/Term.hs +4/−0
• src/Grisette/Internal/SymPrim/Prim/TermUtils.hs +228/−145
• src/Grisette/Internal/SymPrim/Quantifier.hs +199/−0
• src/Grisette/Internal/SymPrim/SomeBV.hs +603/−168
• src/Grisette/Internal/SymPrim/SymAlgReal.hs +136/−0
• src/Grisette/Internal/SymPrim/SymBV.hs +28/−8
• src/Grisette/Internal/SymPrim/SymBool.hs +5/−4
• src/Grisette/Internal/SymPrim/SymFP.hs +301/−8
• src/Grisette/Internal/SymPrim/SymGeneralFun.hs +7/−8
• src/Grisette/Internal/SymPrim/SymInteger.hs +2/−2
• src/Grisette/Internal/SymPrim/SymTabularFun.hs +2/−3
• src/Grisette/Internal/SymPrim/TabularFun.hs +54/−361
• src/Grisette/Internal/TH/DeriveBuiltin.hs +16/−7
• src/Grisette/Internal/TH/DerivePredefined.hs +83/−23
• src/Grisette/Internal/TH/UnifiedConstructor.hs +35/−18
• src/Grisette/Internal/TH/Util.hs +1/−1
• src/Grisette/Internal/Utils/Parameterized.hs +16/−16
• src/Grisette/SymPrim.hs +76/−20
• src/Grisette/Unified.hs +93/−3
• src/Grisette/Unified/Internal/BVBVConversion.hs +161/−0
• src/Grisette/Unified/Internal/BVFPConversion.hs +231/−0
• src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs +203/−0
• src/Grisette/Unified/Internal/Class/UnifiedFromIntegral.hs +226/−0
• src/Grisette/Unified/Internal/Class/UnifiedITEOp.hs +11/−1
• src/Grisette/Unified/Internal/Class/UnifiedSafeBitCast.hs +128/−0
• src/Grisette/Unified/Internal/Class/UnifiedSafeDiv.hs +265/−0
• src/Grisette/Unified/Internal/Class/UnifiedSafeDivision.hs +0/−264
• src/Grisette/Unified/Internal/Class/UnifiedSafeFdiv.hs +83/−0
• src/Grisette/Unified/Internal/Class/UnifiedSafeFromFP.hs +213/−0
• src/Grisette/Unified/Internal/Class/UnifiedSafeLinearArith.hs +11/−10
• src/Grisette/Unified/Internal/Class/UnifiedSafeSymRotate.hs +12/−13
• src/Grisette/Unified/Internal/Class/UnifiedSafeSymShift.hs +12/−13
• src/Grisette/Unified/Internal/Class/UnifiedSimpleMergeable.hs +13/−0
• src/Grisette/Unified/Internal/Class/UnifiedSymEq.hs +31/−1
• src/Grisette/Unified/Internal/Class/UnifiedSymOrd.hs +10/−1
• src/Grisette/Unified/Internal/EvalMode.hs +11/−3
• src/Grisette/Unified/Internal/FPFPConversion.hs +127/−0
• src/Grisette/Unified/Internal/UnifiedAlgReal.hs +76/−0
• src/Grisette/Unified/Internal/UnifiedBV.hs +63/−35
• src/Grisette/Unified/Internal/UnifiedData.hs +34/−11
• src/Grisette/Unified/Internal/UnifiedFP.hs +191/−0
• src/Grisette/Unified/Internal/UnifiedInteger.hs +4/−2
• test/Grisette/Backend/CEGISTests.hs +2/−2
• test/Grisette/Backend/LoweringTests.hs +446/−136
• test/Grisette/Backend/TermRewritingGen.hs +277/−67
• test/Grisette/Backend/TermRewritingTests.hs +537/−37
• test/Grisette/Core/Control/Monad/UnionTests.hs +8/−6
• test/Grisette/Core/Data/Class/BitCastTests.hs +93/−0
• test/Grisette/Core/Data/Class/EvalSymTests.hs +1/−0
• test/Grisette/Core/Data/Class/ExtractSymTests.hs +1/−0
• test/Grisette/Core/Data/Class/PPrintTests.hs +103/−19
• test/Grisette/Core/Data/Class/SafeDivTests.hs +400/−0
• test/Grisette/Core/Data/Class/SafeDivisionTests.hs +0/−278
• test/Grisette/Core/Data/Class/SafeLinearArithTests.hs +7/−8
• test/Grisette/Core/Data/Class/SafeSymRotateTests.hs +5/−19
• test/Grisette/Core/Data/Class/SafeSymShiftTests.hs +5/−20
• test/Grisette/Core/Data/Class/SymFiniteBitsTests.hs +162/−0
• test/Grisette/Core/Data/Class/SymOrdTests.hs +1/−1
• test/Grisette/Core/Data/Class/SymRotateTests.hs +0/−6
• test/Grisette/Core/Data/Class/SymShiftTests.hs +1/−7
• test/Grisette/Core/Data/Class/TestValues.hs +5/−2
• test/Grisette/Core/Data/Class/ToSymTests.hs +3/−1
• test/Grisette/Core/TH/DerivationTest.hs +12/−1
• test/Grisette/Lib/Control/Monad/Trans/State/Common.hs +4/−4
• test/Grisette/Lib/Control/MonadTests.hs +1/−1
• test/Grisette/Lib/Data/ListTests.hs +11/−12
• test/Grisette/SymPrim/AlgRealTests.hs +105/−0
• test/Grisette/SymPrim/BVTests.hs +12/−13
• test/Grisette/SymPrim/FPTests.hs +893/−24
• test/Grisette/SymPrim/GeneralFunTests.hs +54/−0
• test/Grisette/SymPrim/Prim/BVTests.hs +27/−25
• test/Grisette/SymPrim/Prim/BitsTests.hs +2/−6
• test/Grisette/SymPrim/Prim/IntegralTests.hs +4/−4
• test/Grisette/SymPrim/Prim/ModelTests.hs +52/−39
• test/Grisette/SymPrim/Prim/TabularFunTests.hs +11/−9
• test/Grisette/SymPrim/QuantifierTests.hs +77/−0
• test/Grisette/SymPrim/SomeBVTests.hs +275/−33
• test/Grisette/SymPrim/SymGeneralFunTests.hs +37/−0
• test/Grisette/SymPrim/SymPrimTests.hs +132/−27
• test/Grisette/SymPrim/TabularFunTests.hs +6/−6
• test/Grisette/TestUtil/SymbolicAssertion.hs +6/−7
• test/Grisette/Unified/EvalModeTest.hs +155/−22
• test/Grisette/Unified/UnifiedClassesTest.hs +3/−2
• test/Grisette/Unified/UnifiedConstructorTest.hs +44/−15
• test/Main.hs +16/−4

@@ -6,6 +6,76 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.8.0.0] - 2024-08-13++### Added+- Added pretty printer for models.+  ([#225](https://github.com/lsrcz/grisette/pull/225))+- Added support for algebraic reals (`AlgReal` and `SymAlgReal`).+  ([#228](https://github.com/lsrcz/grisette/pull/228),+   [#229](https://github.com/lsrcz/grisette/pull/229))+- Added support for quantifiers.+  ([#230](https://github.com/lsrcz/grisette/pull/230))+- Added `SafeFdiv`, `SafeLogBase`, `DivOr`, `FdivOr`, and `LogBaseOr`.+  ([#228](https://github.com/lsrcz/grisette/pull/228),+   [#231](https://github.com/lsrcz/grisette/pull/231))+- Added bitcast from and to `Bool`, `IntN`, `WordN`, `FP` and their symbolic+  counterparts when appropriate.+  ([#232](https://github.com/lsrcz/grisette/pull/232))+- Add `SymFromIntegral`. ([#233](https://github.com/lsrcz/grisette/pull/233))+- Add operations for concrete floating point numbers. Add IEEE754-2019+  `fpMinimum`, `fpMinimumNumber`, `fpMaximum`, and `fpMaximumNumber` operations.+  ([#235](https://github.com/lsrcz/grisette/pull/235))+- Add conversion from and to floating points.+  ([#236](https://github.com/lsrcz/grisette/pull/236))+- Add `SymFiniteBits`. ([#237](https://github.com/lsrcz/grisette/pull/237))+- Add unified instances for all provided operations, including `FP` and+  `AlgReal`.+  ([#239](https://github.com/lsrcz/grisette/pull/239),+   [#240](https://github.com/lsrcz/grisette/pull/240),+   [#243](https://github.com/lsrcz/grisette/pull/243))+- Allow the use of number literals for `SomeBV`.+  ([#245](https://github.com/lsrcz/grisette/pull/245))+- Add `symDistinct`.+  ([#246](https://github.com/lsrcz/grisette/pull/246),+   [#247](https://github.com/lsrcz/grisette/pull/247))++### Fixed+- Fixed model parsing for floating points.+  ([#227](https://github.com/lsrcz/grisette/pull/227))+- Allowed `mkUnifiedConstructor` to be used with types without modes or args.+  ([#242](https://github.com/lsrcz/grisette/pull/242))++### Changed+- [Breaking] Changed the operand order for `liftPFormatPrec2` and+  `liftPFormatList2`.+  ([#225](https://github.com/lsrcz/grisette/pull/225))+- [Breaking] Changed the term representation with a compile-time tag for its+  kind (`AnyKind` for all symbols and `ConstantKind` for symbols other than+  uninterpreted functions). This also affects the 'ExtractSym'. A new+  `extractSymMaybe` will regard this tag if not all symbols can be casted to+  that tag. `extractSym` will always succeed, returning a set with `AnyKind`.+  ([#230](https://github.com/lsrcz/grisette/pull/230))+- [Breaking] `SafeDivision` renamed to `SafeDiv`.+  ([#231](https://github.com/lsrcz/grisette/pull/231))+- Refined the template-haskell-based derivation mechanism.+  ([#238](https://github.com/lsrcz/grisette/pull/238))+- [Breaking] `GetData` is made injective by giving `Identity` wrapped type for+  concrete evaluation instead of the type itself.+  ([#242](https://github.com/lsrcz/grisette/pull/242))+- Changed pprint for `Identity` to not to print the constructor.+  ([#242](https://github.com/lsrcz/grisette/pull/242))+- Make `ToSym` requires the target type to be `Mergeable`. This enable us to+  merge the results for converting from `Union a` to `Union b` again.+  ([#244](https://github.com/lsrcz/grisette/pull/244))++### Removed+- Removed `fpMin` and `fpMax`, which is removed in IEEE754-2019.+  ([#235](https://github.com/lsrcz/grisette/pull/235))+- Dropped support for post-evaluation approximation.+  ([#241](https://github.com/lsrcz/grisette/pull/241))+  + ## [0.7.0.0] - 2024-07-02  ### Added@@ -379,7 +449,8 @@  - Initial release for Grisette. -[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.7.0.0...HEAD+[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.8.0.0...HEAD+[0.8.0.0]: https://github.com/lsrcz/grisette/compare/v0.7.0.0...v0.8.0.0 [0.7.0.0]: https://github.com/lsrcz/grisette/compare/v0.6.0.0...v0.7.0.0 [0.6.0.0]: https://github.com/lsrcz/grisette/compare/v0.5.0.1...v0.6.0.0 [0.5.0.1]: https://github.com/lsrcz/grisette/compare/v0.5.0.0...v0.5.0.1

@@ -49,7 +49,7 @@ ```cabal library   ...-  build-depends: grisette >= 0.7 < 0.8+  build-depends: grisette >= 0.8 < 0.9 ```  #### Quick start template with `stack new`@@ -276,6 +276,23 @@  ## Note +Grisette is fully compatible with GHC 9.6+, and works in most cases with GHC+8.10+.++### CLC proposal #10+As the type classes provided by Grisette implements+[CLC proposal #10](https://github.com/haskell/core-libraries-committee/issues/10),+which requires `base-4.18.0.0` to work reliably, Grisette is fully compatible+with GHC 9.6.+You may experience instance resolution failure when using older GHCs in the+client code (Grisette itself is buildable against GHC 8.10+ with some tricks).++### Quantifiers++Grisette currently supports universal and existential quantifiers $\forall$ and+$\exists$, but only when building with sbv >= 10.1. This also means that you+need to use GHC >= 9.2.+ ### Floating-points  Grisette currently supports boolean, uninterpreted functions, bitvector,@@ -290,11 +307,8 @@ interface](https://hackage.haskell.org/package/grisette/docs/Grisette-Unified.html) to symbolic and concrete evaluations. GHC 9.0 or earlier, without the [QuickLook](https://dl.acm.org/doi/10.1145/3408971) type inference algorithm for-impredicative types, may fail to resolve some constraints . You may need to+impredicative types, may fail to resolve some constraints. You may need to provide additional constraints in your code to help the compiler.--If you don't use the unified interface, Grisette should work fine with GHC 8.10-or later.  ## Citing Grisette 

@@ -1,9 +1,34 @@ module Main (main) where -import System.FilePath.Glob (glob) import Test.DocTest (doctest)  main :: IO () main = do-  core <- glob "src/**/*.hs"-  doctest core+  doctest+    [ "-isrc",+      "--fast",+      "-XBinaryLiterals",+      "-XDataKinds",+      "-XDeriveAnyClass",+      "-XDeriveGeneric",+      "-XDeriveLift",+      "-XDerivingStrategies",+      "-XDerivingVia",+      "-XFlexibleContexts",+      "-XFlexibleInstances",+      "-XFunctionalDependencies",+      "-XLambdaCase",+      "-XMonoLocalBinds",+      "-XMultiParamTypeClasses",+      "-XOverloadedStrings",+      "-XScopedTypeVariables",+      "-XStandaloneDeriving",+      "-XTemplateHaskell",+      "-XTypeApplications",+      "-XTypeOperators",+      "-XUndecidableInstances",+      "-Wno-unrecognised-warning-flags",+      "-Wno-x-partial",+      "-Wno-deriving-defaults",+      "src"+    ]

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.36.0.+-- This file has been generated from package.yaml by hpack version 0.36.1. -- -- see: https://github.com/sol/hpack  name:           grisette-version:        0.7.0.0+version:        0.8.0.0 synopsis:       Symbolic evaluation as a library description:    Grisette is a reusable symbolic evaluation library for Haskell. By                 translating programs into constraints, Grisette can help the development of@@ -37,7 +37,7 @@   , GHC == 9.0.2   , GHC == 9.2.8   , GHC == 9.4.8-  , GHC == 9.6.5+  , GHC == 9.6.6   , GHC == 9.8.2   , GHC == 9.10.1 extra-source-files:@@ -62,6 +62,7 @@       Grisette.Experimental.GenSymConstrained       Grisette.Experimental.MonadParallelUnion       Grisette.Experimental.Qualified.ParallelUnionDo+      Grisette.Internal.Backend.QuantifiedStack       Grisette.Internal.Backend.Solving       Grisette.Internal.Backend.SymBiMap       Grisette.Internal.Core.Control.Exception@@ -83,8 +84,12 @@       Grisette.Internal.Core.Data.Class.ModelOps       Grisette.Internal.Core.Data.Class.PlainUnion       Grisette.Internal.Core.Data.Class.PPrint-      Grisette.Internal.Core.Data.Class.SafeDivision+      Grisette.Internal.Core.Data.Class.SafeBitCast+      Grisette.Internal.Core.Data.Class.SafeDiv+      Grisette.Internal.Core.Data.Class.SafeFdiv+      Grisette.Internal.Core.Data.Class.SafeFromFP       Grisette.Internal.Core.Data.Class.SafeLinearArith+      Grisette.Internal.Core.Data.Class.SafeLogBase       Grisette.Internal.Core.Data.Class.SafeSymRotate       Grisette.Internal.Core.Data.Class.SafeSymShift       Grisette.Internal.Core.Data.Class.SignConversion@@ -93,6 +98,9 @@       Grisette.Internal.Core.Data.Class.Solver       Grisette.Internal.Core.Data.Class.SubstSym       Grisette.Internal.Core.Data.Class.SymEq+      Grisette.Internal.Core.Data.Class.SymFiniteBits+      Grisette.Internal.Core.Data.Class.SymFromIntegral+      Grisette.Internal.Core.Data.Class.SymIEEEFP       Grisette.Internal.Core.Data.Class.SymOrd       Grisette.Internal.Core.Data.Class.SymRotate       Grisette.Internal.Core.Data.Class.SymShift@@ -102,25 +110,29 @@       Grisette.Internal.Core.Data.MemoUtils       Grisette.Internal.Core.Data.Symbol       Grisette.Internal.Core.Data.UnionBase+      Grisette.Internal.SymPrim.AlgReal       Grisette.Internal.SymPrim.AllSyms       Grisette.Internal.SymPrim.BV       Grisette.Internal.SymPrim.FP+      Grisette.Internal.SymPrim.FunInstanceGen       Grisette.Internal.SymPrim.GeneralFun       Grisette.Internal.SymPrim.IntBitwidth       Grisette.Internal.SymPrim.ModelRep       Grisette.Internal.SymPrim.Prim.Internal.Caches       Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim-      Grisette.Internal.SymPrim.Prim.Internal.IsZero       Grisette.Internal.SymPrim.Prim.Internal.PartialEval       Grisette.Internal.SymPrim.Prim.Internal.Term       Grisette.Internal.SymPrim.Prim.Internal.Unfold@@ -130,7 +142,9 @@       Grisette.Internal.SymPrim.Prim.SomeTerm       Grisette.Internal.SymPrim.Prim.Term       Grisette.Internal.SymPrim.Prim.TermUtils+      Grisette.Internal.SymPrim.Quantifier       Grisette.Internal.SymPrim.SomeBV+      Grisette.Internal.SymPrim.SymAlgReal       Grisette.Internal.SymPrim.SymBool       Grisette.Internal.SymPrim.SymBV       Grisette.Internal.SymPrim.SymFP@@ -175,8 +189,15 @@       Grisette.Unified       Grisette.Unified.Internal.BaseConstraint       Grisette.Unified.Internal.BaseMonad+      Grisette.Unified.Internal.BVBVConversion+      Grisette.Unified.Internal.BVFPConversion+      Grisette.Unified.Internal.Class.UnifiedFiniteBits+      Grisette.Unified.Internal.Class.UnifiedFromIntegral       Grisette.Unified.Internal.Class.UnifiedITEOp-      Grisette.Unified.Internal.Class.UnifiedSafeDivision+      Grisette.Unified.Internal.Class.UnifiedSafeBitCast+      Grisette.Unified.Internal.Class.UnifiedSafeDiv+      Grisette.Unified.Internal.Class.UnifiedSafeFdiv+      Grisette.Unified.Internal.Class.UnifiedSafeFromFP       Grisette.Unified.Internal.Class.UnifiedSafeLinearArith       Grisette.Unified.Internal.Class.UnifiedSafeSymRotate       Grisette.Unified.Internal.Class.UnifiedSafeSymShift@@ -185,11 +206,14 @@       Grisette.Unified.Internal.Class.UnifiedSymOrd       Grisette.Unified.Internal.EvalMode       Grisette.Unified.Internal.EvalModeTag+      Grisette.Unified.Internal.FPFPConversion       Grisette.Unified.Internal.MonadWithMode+      Grisette.Unified.Internal.UnifiedAlgReal       Grisette.Unified.Internal.UnifiedBool       Grisette.Unified.Internal.UnifiedBV       Grisette.Unified.Internal.UnifiedConstraint       Grisette.Unified.Internal.UnifiedData+      Grisette.Unified.Internal.UnifiedFP       Grisette.Unified.Internal.UnifiedInteger       Grisette.Unified.Internal.Util       Grisette.Unified.Lib.Control.Applicative@@ -201,7 +225,7 @@       Paths_grisette   hs-source-dirs:       src-  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns+  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags   build-depends:       QuickCheck >=2.14 && <2.16     , array >=0.5.4 && <0.6@@ -211,9 +235,10 @@     , containers >=0.4 && <0.8     , deepseq >=1.4.4 && <1.6     , generic-deriving >=1.14.1 && <1.15-    , hashable >=1.2.3 && <1.5+    , hashable >=1.2.3 && <1.6     , hashtables >=1.2.3.4 && <1.4     , intern >=0.9.2 && <0.10+    , libBF >=0.6.3 && <0.7     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3@@ -224,6 +249,7 @@     , text >=1.2.4.1 && <2.2     , th-abstraction >=0.4 && <0.8     , th-compat >=0.1.2 && <0.2+    , th-lift-instances >=0.1.16 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3   default-language: Haskell2010@@ -239,10 +265,9 @@       Paths_grisette   hs-source-dirs:       doctest-  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N+  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags -threaded -rtsopts -with-rtsopts=-N   build-depends:-      Glob-    , QuickCheck >=2.14 && <2.16+      QuickCheck >=2.14 && <2.16     , array >=0.5.4 && <0.6     , async >=2.2.2 && <2.3     , base >=4.14 && <5@@ -252,9 +277,10 @@     , doctest >=0.18.2 && <0.23     , generic-deriving >=1.14.1 && <1.15     , grisette-    , hashable >=1.2.3 && <1.5+    , hashable >=1.2.3 && <1.6     , hashtables >=1.2.3.4 && <1.4     , intern >=0.9.2 && <0.10+    , libBF >=0.6.3 && <0.7     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3@@ -265,6 +291,7 @@     , text >=1.2.4.1 && <2.2     , th-abstraction >=0.4 && <0.8     , th-compat >=0.1.2 && <0.2+    , th-lift-instances >=0.1.16 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3   default-language: Haskell2010@@ -283,6 +310,7 @@       Grisette.Backend.TermRewritingTests       Grisette.Core.Control.ExceptionTests       Grisette.Core.Control.Monad.UnionTests+      Grisette.Core.Data.Class.BitCastTests       Grisette.Core.Data.Class.BoolTests       Grisette.Core.Data.Class.EvalSymTests       Grisette.Core.Data.Class.ExtractSymTests@@ -290,13 +318,14 @@       Grisette.Core.Data.Class.MergeableTests       Grisette.Core.Data.Class.PlainUnionTests       Grisette.Core.Data.Class.PPrintTests-      Grisette.Core.Data.Class.SafeDivisionTests+      Grisette.Core.Data.Class.SafeDivTests       Grisette.Core.Data.Class.SafeLinearArithTests       Grisette.Core.Data.Class.SafeSymRotateTests       Grisette.Core.Data.Class.SafeSymShiftTests       Grisette.Core.Data.Class.SimpleMergeableTests       Grisette.Core.Data.Class.SubstSymTests       Grisette.Core.Data.Class.SymEqTests+      Grisette.Core.Data.Class.SymFiniteBitsTests       Grisette.Core.Data.Class.SymOrdTests       Grisette.Core.Data.Class.SymRotateTests       Grisette.Core.Data.Class.SymShiftTests@@ -319,8 +348,10 @@       Grisette.Lib.Data.FunctorTests       Grisette.Lib.Data.ListTests       Grisette.Lib.Data.TraversableTests+      Grisette.SymPrim.AlgRealTests       Grisette.SymPrim.BVTests       Grisette.SymPrim.FPTests+      Grisette.SymPrim.GeneralFunTests       Grisette.SymPrim.Prim.BitsTests       Grisette.SymPrim.Prim.BoolTests       Grisette.SymPrim.Prim.BVTests@@ -328,7 +359,9 @@       Grisette.SymPrim.Prim.ModelTests       Grisette.SymPrim.Prim.NumTests       Grisette.SymPrim.Prim.TabularFunTests+      Grisette.SymPrim.QuantifierTests       Grisette.SymPrim.SomeBVTests+      Grisette.SymPrim.SymGeneralFunTests       Grisette.SymPrim.SymPrimTests       Grisette.SymPrim.TabularFunTests       Grisette.TestUtil.NoMerge@@ -340,7 +373,7 @@       Paths_grisette   hs-source-dirs:       test-  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N+  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags -threaded -rtsopts -with-rtsopts=-N -Wredundant-constraints   build-depends:       HUnit ==1.6.*     , QuickCheck >=2.14 && <2.16@@ -352,9 +385,10 @@     , deepseq >=1.4.4 && <1.6     , generic-deriving >=1.14.1 && <1.15     , grisette-    , hashable >=1.2.3 && <1.5+    , hashable >=1.2.3 && <1.6     , hashtables >=1.2.3.4 && <1.4     , intern >=0.9.2 && <0.10+    , libBF >=0.6.3 && <0.7     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3@@ -368,6 +402,7 @@     , text >=1.2.4.1 && <2.2     , th-abstraction >=0.4 && <0.8     , th-compat >=0.1.2 && <0.2+    , th-lift-instances >=0.1.16 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3   default-language: Haskell2010

@@ -23,27 +23,25 @@     abc,      -- * Changing the extra configurations-    ApproximationConfig (..),     ExtraConfig (..),-    precise,-    approximate,     withTimeout,     clearTimeout,      -- * SBV backend solver configuration     SBV.SMTConfig (..),+    SBV.Logic (..),+    SBVC.SMTOption (..),     SBV.Timing (..),     SBV.SMTSolver (..),   ) where  import qualified Data.SBV as SBV+import qualified Data.SBV.Control as SBVC import Grisette.Internal.Backend.Solving-  ( ApproximationConfig (..),-    ExtraConfig (..),+  ( ExtraConfig (..),     GrisetteSMTConfig (..),     abc,-    approximate,     bitwuzla,     boolector,     clearTimeout,@@ -51,7 +49,6 @@     cvc5,     dReal,     mathSAT,-    precise,     withTimeout,     yices,     z3,

@@ -41,7 +41,7 @@     -- Additional tools for building symbolic evaluation based applications are     -- also provided:     ---    -- * Pretty printing (e.g., 'Format')+    -- * Pretty printing (e.g., 'PPrint')     -- * Symbolic generation, or generating fresh symbolic values (e.g.,     --   'GenSym')     -- * Error handling (e.g., 'symAssert')@@ -204,7 +204,6 @@     -- result is then merged into a single formula, and further operation on it     -- won't have to split into multiple paths:     ---    -- >>> :set -Wno-unrecognised-warning-flags -Wno-x-partial     -- >>> x = mrgIf "a1" (return ["b"]) (mrgIf "a2" (return ["c", "d"]) (return ["f"])) :: Union [SymBool]     -- >>> :{     -- do@@ -239,6 +238,8 @@     -- * @'Grisette.SymPrim.SymFP' eb sb@ (@'Grisette.SymPrim.FP' eb sb@,     --   symbolic IEEE-754 floating point numbers with @eb@ exponent bits and     --   @sb@ significand bits)+    -- * 'Grisette.SymPrim.SymAlgReal' ('Grisette.SymPrim.AlgReal'), symbolic+    --   algebraic real numbers.     -- * @'Grisette.SymPrim.SymBool' t'Grisette.SymPrim.=~>' 'Grisette.SymPrim.SymBool'@     --   (@'Bool' t'Grisette.SymPrim.=->' 'Bool'@, symbolic functions,     --   uninterpreted or represented as a table for the input-outputs@@ -262,7 +263,6 @@     --     -- __Examples:__     ---    -- >>> import Grisette     -- >>> con True :: SymBool -- a concrete value     -- true     -- >>> true :: SymBool -- via the LogicalOp instance@@ -275,7 +275,6 @@     -- With the @OverloadedStrings@ GHC extension enabled, symbolic constants     -- can also be constructed from strings.     ---    -- >>> :set -XOverloadedStrings     -- >>> "a" :: SymBool     -- a     --@@ -309,6 +308,8 @@     uniqueIdentifier,     simple,     indexed,+    symbolIdentifier,+    modifyIdentifier,      -- ** Creation and extraction of solvable values     Solvable (..),@@ -329,6 +330,9 @@     SymEq2 (..),     symEq2, +    -- ** Supplemental operation for 'Eq'+    distinct,+     -- ** Symbolic comparison     SymOrd (..),     SymOrd1 (..),@@ -350,11 +354,24 @@     SymRotate (..),     SafeSymRotate (..),     SignConversion (..),-    BitCast (..),      -- ** Safe operation for Numbers-    SafeDivision (..),+    DivOr (..),+    divOrZero,+    modOrDividend,+    quotOrZero,+    remOrDividend,+    divModOrZeroDividend,+    quotRemOrZeroDividend,+    SafeDiv (..),     SafeLinearArith (..),+    FdivOr (..),+    fdivOrZero,+    recipOrZero,+    SafeFdiv (..),+    LogBaseOr (..),+    logBaseOrZero,+    SafeLogBase (..),      -- ** Functions     Function (..),@@ -374,10 +391,12 @@     fpIsSubnormal,     fpIsPoint,     SymIEEEFPTraits (..),-    IEEEConstants (..),+    IEEEFPConstants (..),     IEEEFPRoundingMode (..),     IEEEFPOp (..),     IEEEFPRoundingOp (..),+    IEEEFPConvertible (..),+    IEEEFPToAlgReal (..),      -- ** Conversion between Concrete and Symbolic values     ToCon (..),@@ -391,6 +410,15 @@     ToSym2 (..),     toSym2, +    -- ** Conversion between different symbolic types+    BitCast (..),+    BitCastCanonical (..),+    BitCastOr (..),+    BitCastOrCanonical,+    bitCastOrCanonical,+    SafeBitCast (..),+    SymFromIntegral (..),+     -- * Unsolvable types and merging      -- | There are types that be directly represented as SMT formulas and@@ -921,7 +949,6 @@     -- We can generate many symbolic values at once with the 'Fresh' monad.     -- The symbolic constants are ensured to be unique:     ---    -- >>> :set -XScopedTypeVariables     -- >>> :{     --   flip runFresh "x" $ do     --     a :: SymBool <- simpleFresh ()@@ -1008,9 +1035,7 @@     -- You can define your own error types, and reason about them with the     -- solver APIs.     ---    -- >>> :set -XDerivingVia -XDeriveGeneric -XDerivingStrategies -XLambdaCase     -- >>> import GHC.Generics-    -- >>> import Grisette.Backend     -- >>> :{     --   data Error = Error1 | Error2 | Error3     --     deriving (Show, Generic)@@ -1140,7 +1165,6 @@     --     -- We can first define the error type used in the program.     ---    -- >>> :set -XLambdaCase -XDeriveGeneric -XDerivingStrategies -XDerivingVia     -- >>> import Control.Monad.Except     -- >>> import Grisette.Lib.Control.Monad.Trans.Except     -- >>> import Control.Exception@@ -1257,8 +1281,10 @@     ExtractSym (..),     ExtractSym1 (..),     extractSym1,+    extractSymMaybe1,     ExtractSym2 (..),     extractSym2,+    extractSymMaybe2,      -- ** Evaluation with a model @@ -1345,8 +1371,8 @@     -- *** 'ExtractSym'     ExtractSymArgs (..),     GExtractSym (..),-    genericExtractSym,-    genericLiftExtractSym,+    genericExtractSymMaybe,+    genericLiftExtractSymMaybe,      -- *** 'SubstSym'     SubstSymArgs (..),@@ -1365,6 +1391,12 @@   ) where +#if MIN_VERSION_prettyprinter(1,7,0)+import Prettyprinter+#else+import Data.Text.Prettyprint.Doc as Prettyprinter+#endif+ import Generics.Deriving (Default (..), Default1 (..)) import Grisette.Internal.Core.Control.Exception   ( AssertionError (..),@@ -1388,7 +1420,13 @@     unionSize,     unionUnaryOp,   )-import Grisette.Internal.Core.Data.Class.BitCast (BitCast (..))+import Grisette.Internal.Core.Data.Class.BitCast+  ( BitCast (..),+    BitCastCanonical (..),+    BitCastOr (..),+    BitCastOrCanonical,+    bitCastOrCanonical,+  ) import Grisette.Internal.Core.Data.Class.BitVector   ( BV (..),     SizedBV (..),@@ -1462,8 +1500,10 @@     GExtractSym (..),     extractSym1,     extractSym2,-    genericExtractSym,-    genericLiftExtractSym,+    extractSymMaybe1,+    extractSymMaybe2,+    genericExtractSymMaybe,+    genericLiftExtractSymMaybe,   ) import Grisette.Internal.Core.Data.Class.Function (Apply (..), Function (..)) import Grisette.Internal.Core.Data.Class.GenSym@@ -1496,11 +1536,12 @@     runFreshT,   ) import Grisette.Internal.Core.Data.Class.IEEEFP-  ( IEEEConstants (..),+  ( IEEEFPConstants (..),+    IEEEFPConvertible (..),     IEEEFPOp (..),     IEEEFPRoundingMode (..),     IEEEFPRoundingOp (..),-    SymIEEEFPTraits (..),+    IEEEFPToAlgReal (..),     fpIsInfinite,     fpIsNaN,     fpIsNegative,@@ -1582,8 +1623,29 @@     pattern If,     pattern Single,   )-import Grisette.Internal.Core.Data.Class.SafeDivision (SafeDivision (..))+import Grisette.Internal.Core.Data.Class.SafeBitCast (SafeBitCast (..))+import Grisette.Internal.Core.Data.Class.SafeDiv+  ( DivOr (..),+    SafeDiv (..),+    divModOrZeroDividend,+    divOrZero,+    modOrDividend,+    quotOrZero,+    quotRemOrZeroDividend,+    remOrDividend,+  )+import Grisette.Internal.Core.Data.Class.SafeFdiv+  ( FdivOr (..),+    SafeFdiv (..),+    fdivOrZero,+    recipOrZero,+  ) import Grisette.Internal.Core.Data.Class.SafeLinearArith (SafeLinearArith (..))+import Grisette.Internal.Core.Data.Class.SafeLogBase+  ( LogBaseOr (..),+    SafeLogBase (..),+    logBaseOrZero,+  ) import Grisette.Internal.Core.Data.Class.SafeSymRotate (SafeSymRotate (..)) import Grisette.Internal.Core.Data.Class.SafeSymShift (SafeSymShift (..)) import Grisette.Internal.Core.Data.Class.SignConversion (SignConversion (..))@@ -1643,11 +1705,18 @@     SymEq1 (..),     SymEq2 (..),     SymEqArgs (..),+    distinct,     genericLiftSymEq,     genericSymEq,     symEq1,     symEq2,   )+import Grisette.Internal.Core.Data.Class.SymFromIntegral+  ( SymFromIntegral (..),+  )+import Grisette.Internal.Core.Data.Class.SymIEEEFP+  ( SymIEEEFPTraits (..),+  ) import Grisette.Internal.Core.Data.Class.SymOrd   ( GSymOrd (..),     SymOrd (..),@@ -1706,40 +1775,18 @@     Symbol (..),     identifier,     indexed,+    modifyIdentifier,     simple,+    symbolIdentifier,     uniqueIdentifier,     withInfo,     withLoc,   )-#if MIN_VERSION_prettyprinter(1,7,0)-import Prettyprinter-#else-import Data.Text.Prettyprint.Doc as Prettyprinter-#endif+import Instances.TH.Lift ()  -- $setup+-- >>> import Grisette -- >>> import Grisette.Core -- >>> import Grisette.Lib.Base -- >>> import Grisette.SymPrim -- >>> import Grisette.TH--- >>> :set -XDataKinds--- >>> :set -XBinaryLiterals--- >>> :set -XFlexibleContexts--- >>> :set -XFlexibleInstances--- >>> :set -XFunctionalDependencies--- >>> :set -XOverloadedStrings--- >>> :set -XTemplateHaskell--- >>> :set -XScopedTypeVariables--- >>> :set -XDerivingVia--- >>> :set -XStandaloneDeriving--- >>> :set -XTypeApplications--- >>> :set -XFlexibleInstances--- >>> :set -XMultiParamTypeClasses--- >>> :set -XFlexibleContexts--- >>> :set -XDeriveLift--- >>> :set -XUndecidableInstances--- >>> :set -XDeriveAnyClass--- >>> :set -XMonoLocalBinds--- >>> :set -XDerivingStrategies--- >>> :set -XDerivingVia--- >>> :set -XDeriveGeneric

@@ -1,6 +1,14 @@ -- Disable this warning because we are re-exporting things. {-# OPTIONS_GHC -Wno-missing-import-lists #-} +-- |+-- Module      :   Grisette.Experimental+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only module Grisette.Experimental   ( -- * Experimental features 

@@ -77,8 +77,6 @@ -- >>> import Grisette.Core -- >>> import Grisette.Experimental -- >>> import Grisette.SymPrim--- >>> :set -XOverloadedStrings--- >>> :set -XTypeApplications  -- | Class of types in which symbolic values can be generated with some -- specification.@@ -108,6 +106,8 @@     m (Union a)   freshConstrained e spec = mrgSingle <$> simpleFreshConstrained e spec +-- | Generates a symbolic value with the given specification, also place the+-- necessary constraints. genSymConstrained :: forall spec a e. (GenSymConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union (Union a) genSymConstrained e spec = tryMerge . runFreshT (freshConstrained e spec) @@ -129,6 +129,8 @@     spec ->     m a +-- | Generates a symbolic value with the given specification, also place the+-- necessary constraints. genSymSimpleConstrained :: forall spec a e. (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union a genSymSimpleConstrained e spec = tryMerge . runFreshT (simpleFreshConstrained e spec) @@ -857,7 +859,7 @@ -- your own types. -- -- This 'simpleFreshConstrained' implementation is for the types that does not need any specification.--- It will generate product types by generating each fields with '()' as specification.+-- It will generate product types by generating each fields with () as specification. -- It will not work on sum types. -- -- __Note:__ __Never__ use on recursive types.

@@ -37,7 +37,6 @@ -- With the @QualifiedDo@ extension and the "Grisette.Qualified.ParallelUnionDo" -- module, one can execute the paths in parallel and merge the results with: ----- > :set -XQualifiedDo -XOverloadedStrings -- > import Grisette -- > import qualified Grisette.Qualified.ParallelUnionDo as P -- > P.do

@@ -15,8 +15,10 @@ import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable) import Prelude (const, ($)) +-- | Parallel '(>>=)' operation. (>>=) :: (MonadParallelUnion m, Mergeable b, NFData b) => m a -> (a -> m b) -> m b (>>=) = parBindUnion +-- | Parallel '(>>)' operation. (>>) :: (MonadParallelUnion m, Mergeable b, NFData b) => m a -> m b -> m b (>>) a b = parBindUnion a $ const b

@@ -0,0 +1,86 @@+{-# LANGUAGE DataKinds #-}++-- |+-- Module      :   Grisette.Internal.Backend.QuantifiedStack+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.Backend.QuantifiedStack+  ( QuantifiedSymbols (..),+    QuantifiedStack,+    addQuantified,+    lookupQuantified,+    emptyQuantifiedSymbols,+    addQuantifiedSymbol,+    isQuantifiedSymbol,+    emptyQuantifiedStack,+  )+where++import Data.Dynamic (Dynamic)+import qualified Data.HashMap.Lazy as M+import qualified Data.HashSet as S+import GHC.Stack (HasCallStack)+import Grisette.Internal.SymPrim.Prim.Internal.Term+  ( IsSymbolKind,+    SomeTypedConstantSymbol,+    SomeTypedSymbol,+    SupportedPrim (castTypedSymbol),+    TypedConstantSymbol,+    TypedSymbol,+    castSomeTypedSymbol,+    someTypedSymbol,+  )++-- | A set of quantified symbols.+newtype QuantifiedSymbols = QuantifiedSymbols+  { _symbols :: S.HashSet SomeTypedConstantSymbol+  }+  deriving (Show)++-- | An empty set of quantified symbols.+emptyQuantifiedSymbols :: QuantifiedSymbols+emptyQuantifiedSymbols = QuantifiedSymbols S.empty++-- | Add a quantified symbol to the set.+addQuantifiedSymbol ::+  TypedConstantSymbol a -> QuantifiedSymbols -> QuantifiedSymbols+addQuantifiedSymbol s (QuantifiedSymbols t) =+  QuantifiedSymbols (S.insert (someTypedSymbol s) t)++-- | Check if a symbol is quantified.+isQuantifiedSymbol ::+  (SupportedPrim a, IsSymbolKind knd) =>+  TypedSymbol knd a ->+  QuantifiedSymbols ->+  Bool+isQuantifiedSymbol s (QuantifiedSymbols t) =+  case castTypedSymbol s of+    Just s' -> S.member (someTypedSymbol s') t+    _ -> False++-- | A stack of quantified symbols.+newtype QuantifiedStack = QuantifiedStack+  {_stack :: M.HashMap SomeTypedConstantSymbol Dynamic}++-- | An empty stack of quantified symbols.+emptyQuantifiedStack :: QuantifiedStack+emptyQuantifiedStack = QuantifiedStack M.empty++-- | Add a quantified symbol to the stack.+addQuantified ::+  TypedConstantSymbol a -> Dynamic -> QuantifiedStack -> QuantifiedStack+addQuantified s d (QuantifiedStack t) =+  QuantifiedStack (M.insert (someTypedSymbol s) d t)++-- | Look up a quantified symbol in the stack.+lookupQuantified ::+  (HasCallStack, IsSymbolKind knd) =>+  SomeTypedSymbol knd ->+  QuantifiedStack ->+  Maybe Dynamic+lookupQuantified s (QuantifiedStack t) =+  (`M.lookup` t) =<< castSomeTypedSymbol s

@@ -34,10 +34,7 @@     abc,      -- * Changing the extra configurations-    ApproximationConfig (..),     ExtraConfig (..),-    precise,-    approximate,     withTimeout,     clearTimeout, @@ -69,15 +66,21 @@   ) import Control.Concurrent.STM.TChan (TChan, newTChan, readTChan, writeTChan) import Control.Exception (handle, throwTo)+import Control.Monad (when) import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.RWS (RWST (runRWST)) import Control.Monad.Reader   ( MonadReader (ask),     MonadTrans (lift),     ReaderT (runReaderT),+    ask,+    local,   ) import Control.Monad.STM (STM)-import Control.Monad.State (MonadState (get, put), StateT, evalStateT)+import Control.Monad.State (MonadState (get, put), StateT, evalStateT, modify)+import Control.Monad.Writer (tell) import Data.Dynamic (fromDyn, toDyn)+import Data.List.NonEmpty (NonEmpty) import Data.Proxy (Proxy (Proxy)) import qualified Data.SBV as SBV import qualified Data.SBV.Control as SBVC@@ -87,11 +90,21 @@ import qualified Data.SBV.Trans.Control as SBVTC import GHC.IO.Exception (ExitCode (ExitSuccess)) import GHC.Stack (HasCallStack)-import GHC.TypeNats (KnownNat, Nat)+import Grisette.Internal.Backend.QuantifiedStack+  ( QuantifiedStack,+    QuantifiedSymbols,+    addQuantified,+    addQuantifiedSymbol,+    emptyQuantifiedStack,+    emptyQuantifiedSymbols,+    isQuantifiedSymbol,+    lookupQuantified,+  ) import Grisette.Internal.Backend.SymBiMap   ( SymBiMap,     addBiMap,     addBiMapIntermediate,+    attachNextQuantifiedSymbolInfo,     emptySymBiMap,     findStringToSymbol,     lookupTerm,@@ -125,6 +138,7 @@       ),     SolvingFailure (SolvingError, Terminated, Unk, Unsat),   )+import Grisette.Internal.SymPrim.GeneralFun (substTerm) import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP   ( sbvFPBinaryTerm,     sbvFPFMATerm,@@ -133,11 +147,11 @@     sbvFPTraitTerm,     sbvFPUnaryTerm,   )-import Grisette.Internal.SymPrim.Prim.Internal.IsZero (KnownIsZero) import Grisette.Internal.SymPrim.Prim.Internal.Term   ( PEvalApplyTerm (sbvApplyTerm),-    PEvalBVSignConversionTerm (sbvToSigned, sbvToUnsigned),     PEvalBVTerm (sbvBVConcatTerm, sbvBVExtendTerm, sbvBVSelectTerm),+    PEvalBitCastOrTerm (sbvBitCastOr),+    PEvalBitCastTerm (sbvBitCast),     PEvalBitwiseTerm       ( sbvAndBitsTerm,         sbvComplementBitsTerm,@@ -150,8 +164,10 @@         sbvQuotIntegralTerm,         sbvRemIntegralTerm       ),-    PEvalFloatingTerm (sbvSqrtTerm),+    PEvalFloatingTerm (sbvFloatingUnaryTerm, sbvPowerTerm),     PEvalFractionalTerm (sbvFdivTerm, sbvRecipTerm),+    PEvalFromIntegralTerm (sbvFromIntegralTerm),+    PEvalIEEEFPConvertibleTerm (sbvFromFPOrTerm, sbvToFPTerm),     PEvalNumTerm       ( sbvAbsNumTerm,         sbvAddNumTerm,@@ -165,9 +181,13 @@     SBVFreshMonad,     SBVRep (SBVType),     SomeTypedSymbol (SomeTypedSymbol),+    SupportedNonFuncPrim (withNonFuncPrim),     SupportedPrim       ( conSBVTerm,+        funcDummyConstraint,+        isFuncType,         parseSMTModelResult,+        sbvDistinct,         sbvEq,         sbvIte,         symSBVName,@@ -183,10 +203,15 @@         BVConcatTerm,         BVExtendTerm,         BVSelectTerm,+        BinaryTerm,+        BitCastOrTerm,+        BitCastTerm,         ComplementBitsTerm,         ConTerm,+        DistinctTerm,         DivIntegralTerm,         EqTerm,+        ExistsTerm,         FPBinaryTerm,         FPFMATerm,         FPRoundingBinaryTerm,@@ -194,6 +219,10 @@         FPTraitTerm,         FPUnaryTerm,         FdivTerm,+        FloatingUnaryTerm,+        ForallTerm,+        FromFPOrTerm,+        FromIntegralTerm,         ITETerm,         LeOrdTerm,         LtOrdTerm,@@ -203,6 +232,7 @@         NotTerm,         OrBitsTerm,         OrTerm,+        PowerTerm,         QuotIntegralTerm,         RecipTerm,         RemIntegralTerm,@@ -211,14 +241,17 @@         ShiftLeftTerm,         ShiftRightTerm,         SignumNumTerm,-        SqrtTerm,         SymTerm,-        ToSignedTerm,-        ToUnsignedTerm,+        TernaryTerm,+        ToFPTerm,+        UnaryTerm,         XorBitsTerm       ),+    TypedConstantSymbol,+    TypedSymbol (TypedSymbol),     introSupportedPrimConstraint,     someTypedSymbol,+    symTerm,     withSymbolSupported,   ) import Grisette.Internal.SymPrim.Prim.Model as PM@@ -233,36 +266,11 @@ -- >>> import Grisette.Backend -- >>> import Data.Proxy --- | Configures how to approximate unbounded values.------ For example, if we use @'Approx' ('Data.Proxy' :: 'Data.Proxy' 4)@ to--- approximate the following unbounded integer:------ > (+ a 9)------ We will get------ > (bvadd a #x9)------ Here the value 9 will be approximated to a 4-bit bit vector, and the--- operation @bvadd@ will be used instead of @+@.------ Note that this approximation may not be sound, and usually you should not use--- this feature. See 'approximate' for more details.-data ApproximationConfig (n :: Nat) where-  NoApprox :: ApproximationConfig 0-  Approx ::-    (KnownNat n, SBV.BVIsNonZero n, KnownIsZero n) =>-    p n ->-    ApproximationConfig n- -- | Grisette specific extra configurations for the SBV backend.-data ExtraConfig (i :: Nat) = ExtraConfig-  { -- | Timeout in milliseconds for each solver call. CEGIS may call the+newtype ExtraConfig = ExtraConfig+  { -- | Timeout in microseconds for each solver call. CEGIS may call the     -- solver multiple times and each call has its own timeout.-    timeout :: Maybe Int,-    -- | Configures how to approximate unbounded integer values.-    integerApprox :: ApproximationConfig i+    timeout :: Maybe Int   }  -- | Solver configuration for the Grisette SBV backend.@@ -271,144 +279,60 @@ -- some extra configurations. -- -- You should start with the predefined configurations.-data GrisetteSMTConfig (i :: Nat) = GrisetteSMTConfig+data GrisetteSMTConfig = GrisetteSMTConfig   { sbvConfig :: SBV.SMTConfig,-    extraConfig :: ExtraConfig i+    extraConfig :: ExtraConfig   } -preciseExtraConfig :: ExtraConfig 0-preciseExtraConfig =-  ExtraConfig-    { timeout = Nothing,-      integerApprox = NoApprox-    }+preciseExtraConfig :: ExtraConfig+preciseExtraConfig = ExtraConfig {timeout = Nothing}  -- | Solver configuration for Boolector. <https://boolector.github.io/>-boolector :: GrisetteSMTConfig 0+boolector :: GrisetteSMTConfig boolector = GrisetteSMTConfig SBV.boolector preciseExtraConfig  -- | Solver configuration for Bitwuzla. <https://bitwuzla.github.io/>-bitwuzla :: GrisetteSMTConfig 0+bitwuzla :: GrisetteSMTConfig bitwuzla = GrisetteSMTConfig SBV.bitwuzla preciseExtraConfig  -- | Solver configuration for CVC4. <https://cvc4.github.io/>-cvc4 :: GrisetteSMTConfig 0+cvc4 :: GrisetteSMTConfig cvc4 = GrisetteSMTConfig SBV.cvc4 preciseExtraConfig  -- | Solver configuration for CVC5. <https://cvc5.github.io/>-cvc5 :: GrisetteSMTConfig 0+cvc5 :: GrisetteSMTConfig cvc5 = GrisetteSMTConfig SBV.cvc5 preciseExtraConfig  -- | Solver configuration for Yices. <https://yices.csl.sri.com/>-yices :: GrisetteSMTConfig 0+yices :: GrisetteSMTConfig yices = GrisetteSMTConfig SBV.yices preciseExtraConfig  -- | Solver configuration for DReal. <http://dreal.github.io/>-dReal :: GrisetteSMTConfig 0+dReal :: GrisetteSMTConfig dReal = GrisetteSMTConfig SBV.dReal preciseExtraConfig  -- | Solver configuration for Z3. <https://github.com/Z3Prover/z3/>-z3 :: GrisetteSMTConfig 0+z3 :: GrisetteSMTConfig z3 = GrisetteSMTConfig SBV.z3 preciseExtraConfig  -- | Solver configuration for MathSAT. <http://mathsat.fbk.eu/>-mathSAT :: GrisetteSMTConfig 0+mathSAT :: GrisetteSMTConfig mathSAT = GrisetteSMTConfig SBV.mathSAT preciseExtraConfig  -- | Solver configuration for ABC. <http://www.eecs.berkeley.edu/~alanmi/abc/>-abc :: GrisetteSMTConfig 0+abc :: GrisetteSMTConfig abc = GrisetteSMTConfig SBV.abc preciseExtraConfig --- | Set to perform precise reasoning with the solver configuration.-precise :: GrisetteSMTConfig n -> GrisetteSMTConfig 0-precise config =-  config {extraConfig = (extraConfig config) {integerApprox = NoApprox}}---- | Set to perform approximate reasoning with the solver configuration.------ __Note:__ This isn't the preferred way to control the reasoning precision.--- A better way is to write your symbolic evaluation code in a generic way, and--- control the evaluation with the types.------ >>> f :: (Num a) => a -> a -> a; f x y = x + y--- >>> solve z3 $ f "a" 5 .== (2 :: SymInteger)--- Right (Model {a -> -3 :: Integer})--- >>> solve z3 $ f "a" 5 .== (2 :: SymWordN 4)--- Right (Model {a -> 0xd :: WordN 4})------ __Description:__------ Integers can be unbounded (mathematical integer) or bounded (machine--- integer/bit vector). The two types of integers have their own use cases,--- and should be used to model different systems.--- However, the solvers are known to have bad performance on some unbounded--- integer operations, for example, when reason about non-linear integer--- algebraic (e.g., multiplication or division),--- the solver may not be able to get a result in a reasonable time.--- In contrast, reasoning about bounded integers is usually more efficient.------ To bridge the performance gap between the two types of integers, Grisette--- allows to model the system with unbounded integers, and evaluate them with--- infinite precision during the symbolic evaluation, but when solving the--- queries, they are translated to bit vectors for better performance.------ For example, the Grisette term @5 * "a" :: 'Grisette.SymPrim.SymInteger'@--- should be translated to the following SMT with the unbounded reasoning--- configuration (the term is @t1@):------ > (declare-fun a () Int)           ; declare symbolic constant a--- > (define-fun c1 () Int 5)         ; define the concrete value 5--- > (define-fun t1 () Int (* c1 a))  ; define the term------ While with reasoning precision 4, it would be translated to the following--- SMT (the term is @t1@):------ > ; declare symbolic constant a, the type is a bit vector with bit width 4--- > (declare-fun a () (_ BitVec 4))--- > ; define the concrete value 1, translated to the bit vector #x1--- > (define-fun c1 () (_ BitVec 4) #x5)--- > ; define the term, using bit vector addition rather than integer addition--- > (define-fun t1 () (_ BitVec 4) (bvmul c1 a))------ This bounded translation can usually be solved faster than the unbounded--- one, and should work well when no overflow is possible, in which case the--- performance can be improved with almost no cost.------ We must note that the bounded translation is an approximation and is--- __/not sound/__. As the approximation happens only during the final--- translation, the symbolic evaluation may aggressively optimize the term based--- on the properties of mathematical integer arithmetic. This may cause the--- solver yield results that is incorrect under both unbounded or bounded--- semantics.------ The following is an example that is correct under bounded semantics, while is--- incorrect under the unbounded semantics:------ >>> :set -XTypeApplications -XOverloadedStrings -XDataKinds--- >>> let a = "a" :: SymInteger--- >>> solve z3 $ a .> 7 .&& a .< 9--- Right (Model {a -> 8 :: Integer})--- >>> solve (approximate (Proxy @4) z3) $ a .> 7 .&& a .< 9--- Left Unsat------ This may be avoided by setting an large enough reasoning precision to prevent--- overflows.-approximate ::-  forall p m n.-  (KnownNat n, SBV.BVIsNonZero n, KnownIsZero n) =>-  p n ->-  GrisetteSMTConfig m ->-  GrisetteSMTConfig n-approximate p config =-  config {extraConfig = (extraConfig config) {integerApprox = Approx p}}- -- | Set the timeout for the solver configuration.-withTimeout :: Int -> GrisetteSMTConfig i -> GrisetteSMTConfig i+--+-- The timeout is in microseconds (1e-6 seconds). The timeout is applied to each+-- individual solver query.+withTimeout :: Int -> GrisetteSMTConfig -> GrisetteSMTConfig withTimeout t config =   config {extraConfig = (extraConfig config) {timeout = Just t}}  -- | Clear the timeout for the solver configuration.-clearTimeout :: GrisetteSMTConfig i -> GrisetteSMTConfig i+clearTimeout :: GrisetteSMTConfig -> GrisetteSMTConfig clearTimeout config =   config {extraConfig = (extraConfig config) {timeout = Nothing}} @@ -420,27 +344,27 @@  -- | Apply the timeout to the configuration. applyTimeout ::-  (MonadIO m, SBVTC.MonadQuery m) => GrisetteSMTConfig i -> m a -> m a+  (MonadIO m, SBVTC.MonadQuery m) => GrisetteSMTConfig -> m a -> m a applyTimeout config q = case timeout (extraConfig config) of   Nothing -> q   Just t -> SBVTC.timeout t q  -- | Incremental solver monad transformer with the SBV backend.-type SBVIncrementalT n m =-  ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (SBVTC.QueryT m))+type SBVIncrementalT m =+  ReaderT GrisetteSMTConfig (StateT SymBiMap (SBVTC.QueryT m))  -- | Incremental solver monad with the SBV backend.-type SBVIncremental n = SBVIncrementalT n IO+type SBVIncremental = SBVIncrementalT IO  -- | Run the incremental solver monad with a given configuration.-runSBVIncremental :: GrisetteSMTConfig n -> SBVIncremental n a -> IO a+runSBVIncremental :: GrisetteSMTConfig -> SBVIncremental a -> IO a runSBVIncremental = runSBVIncrementalT  -- | Run the incremental solver monad transformer with a given configuration. runSBVIncrementalT ::   (SBVTC.ExtractIO m) =>-  GrisetteSMTConfig n ->-  SBVIncrementalT n m a ->+  GrisetteSMTConfig ->+  SBVIncrementalT m a ->   m a runSBVIncrementalT config sbvIncrementalT =   SBVT.runSMTWith (sbvConfig config) $@@ -449,12 +373,14 @@         flip evalStateT emptySymBiMap $           runReaderT sbvIncrementalT config -instance (MonadIO m) => MonadicSolver (SBVIncrementalT n m) where+instance (MonadIO m) => MonadicSolver (SBVIncrementalT m) where   monadicSolverAssert (SymBool formula) = do     symBiMap <- get     config <- ask-    (newSymBiMap, lowered) <- lowerSinglePrimCached config formula symBiMap-    lift $ lift $ SBV.constrain lowered+    (newSymBiMap, lowered, dummyConstraint) <-+      lowerSinglePrimCached config formula symBiMap+    lift $ lift $ SBV.constrain dummyConstraint+    lift $ lift $ SBV.constrain (lowered emptyQuantifiedStack)     put newSymBiMap   monadicSolverCheckSat = do     checkSatResult <- SBVTC.checkSat@@ -487,7 +413,7 @@   _ <- tryTakeTMVar status   putTMVar status SBVSolverTerminated -instance ConfigurableSolver (GrisetteSMTConfig n) SBVSolverHandle where+instance ConfigurableSolver GrisetteSMTConfig SBVSolverHandle where   newSolver config = do     sbvSolverHandleInChan <- atomically newTChan     sbvSolverHandleOutChan <- atomically newTChan@@ -500,7 +426,8 @@                 writeTChan sbvSolverHandleOutChan (Left (SolvingError e))       handle handler $ runSBVIncremental config $ do         let loop = do-              nextFormula <- liftIO $ atomically $ readTChan sbvSolverHandleInChan+              nextFormula <-+                liftIO $ atomically $ readTChan sbvSolverHandleInChan               case nextFormula of                 SolverPush n -> monadicSolverPush n >> loop                 SolverPop n -> monadicSolverPop n >> loop@@ -554,223 +481,341 @@     throwTo (asyncThreadId thread) ExitSuccess     wait thread -configIntroKnownIsZero :: GrisetteSMTConfig n -> ((KnownIsZero n) => r) -> r-configIntroKnownIsZero (GrisetteSMTConfig _ (ExtraConfig _ (Approx _))) r = r-configIntroKnownIsZero (GrisetteSMTConfig _ (ExtraConfig _ NoApprox)) r = r+newtype TermAll = TermAll SBV.SBool +instance Semigroup TermAll where+  TermAll a <> TermAll b = TermAll (a SBV..&& b)++instance Monoid TermAll where+  mempty = TermAll SBV.sTrue+ -- | Lower a single primitive term to SBV. With an explicitly provided -- 'SymBiMap' cache. lowerSinglePrimCached ::-  forall integerBitWidth a m.+  forall a m.   (HasCallStack, SBVFreshMonad m) =>-  GrisetteSMTConfig integerBitWidth ->+  GrisetteSMTConfig ->   Term a ->   SymBiMap ->-  m (SymBiMap, SBVType integerBitWidth a)-lowerSinglePrimCached config t m =-  introSupportedPrimConstraint t $-    configIntroKnownIsZero config $-      case lookupTerm (SomeTerm t) m of-        Just x ->-          return-            ( m,-              withPrim @a (Proxy @integerBitWidth) $ fromDyn x undefined-            )-        Nothing -> lowerSinglePrimImpl config t m+  m (SymBiMap, QuantifiedStack -> SBVType a, SBV.SBool)+lowerSinglePrimCached config t m = do+  -- (_, newm, dummy) <- declareAllUFuncsImpl config t HS.empty m+  (r, finalm, TermAll dummy) <-+    runRWST (lowerSinglePrimCached' config t) emptyQuantifiedSymbols m+  return (finalm, r, dummy)  -- | Lower a single primitive term to SBV. lowerSinglePrim ::-  forall integerBitWidth a m.+  forall a m.   (HasCallStack, SBVFreshMonad m) =>-  GrisetteSMTConfig integerBitWidth ->+  GrisetteSMTConfig ->   Term a ->-  m (SymBiMap, SBVType integerBitWidth a)-lowerSinglePrim config t = lowerSinglePrimCached config t emptySymBiMap+  m (SymBiMap, QuantifiedStack -> SBVType a, SBV.SBool)+lowerSinglePrim config t =+  lowerSinglePrimCached config t emptySymBiMap +lowerSinglePrimCached' ::+  forall a m.+  (HasCallStack, SBVFreshMonad m) =>+  GrisetteSMTConfig ->+  Term a ->+  RWST+    QuantifiedSymbols+    TermAll+    SymBiMap+    m+    (QuantifiedStack -> SBVType a)+lowerSinglePrimCached' config t = do+  m <- get+  introSupportedPrimConstraint t $+    case lookupTerm (SomeTerm t) m of+      Just x ->+        return+          ( \qst ->+              withPrim @a $+                fromDyn (x qst) undefined+          )+      Nothing -> do+        lowerSinglePrimImpl config t+ lowerSinglePrimImpl ::-  forall integerBitWidth a m.-  (HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>-  GrisetteSMTConfig integerBitWidth ->+  forall a m.+  (HasCallStack, SBVFreshMonad m) =>+  GrisetteSMTConfig ->   Term a ->-  SymBiMap ->-  m (SymBiMap, SBVType integerBitWidth a)-lowerSinglePrimImpl config (ConTerm _ v) m =-  return (m, conSBVTerm config v)-lowerSinglePrimImpl config t@(SymTerm _ ts) m =-  withPrim @a config $ do-    let name = symSBVName ts (sizeBiMap m)-    g <- symSBVTerm @a config name-    return (addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts) m, g)-lowerSinglePrimImpl config t m =+  RWST+    QuantifiedSymbols+    TermAll+    SymBiMap+    m+    (QuantifiedStack -> SBVType a)+lowerSinglePrimImpl _ (ConTerm _ v) =+  return $ const $ conSBVTerm v+lowerSinglePrimImpl _ t@(SymTerm _ ts) = do+  qs <- ask+  if isQuantifiedSymbol ts qs+    then withPrim @a $ do+      let retDyn qst =+            case lookupQuantified (someTypedSymbol ts) qst of+              Just v -> v+              Nothing -> error "BUG: Symbol not found in the quantified stack"+      modify $ \m -> addBiMapIntermediate (SomeTerm t) retDyn m+      return $+        \x ->+          fromDyn+            (retDyn x)+            (error "BUG: Symbol not found in the quantified stack")+    else withPrim @a $ do+      m <- get+      let name = symSBVName ts (sizeBiMap m)+      g <- symSBVTerm @a name+      when (isFuncType @a) $ tell $ TermAll $ funcDummyConstraint @a g+      put $ addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts) m+      return $ const g+#if MIN_VERSION_sbv(10,1,0)+lowerSinglePrimImpl config t@(ForallTerm _ (ts :: TypedConstantSymbol t1) v) =+  withNonFuncPrim @t1 $ do+    do+      m <- get+      let (newm, sb@(TypedSymbol sbs)) = attachNextQuantifiedSymbolInfo m ts+      put newm+      let substedTerm = substTerm ts (symTerm sbs) v+      r <-+        local (addQuantifiedSymbol sb) $+          lowerSinglePrimCached'+            config+            substedTerm+      let ret qst = SBV.quantifiedBool $+            \(SBV.Forall (a :: SBVType t1)) ->+              r $ addQuantified sb (toDyn a) qst+      modify $ addBiMapIntermediate (SomeTerm t) (toDyn . ret)+      return ret+lowerSinglePrimImpl config t@(ExistsTerm _ (ts :: TypedConstantSymbol t1) v) =+  withNonFuncPrim @t1 $ do+    do+      m <- get+      let (newm, sb@(TypedSymbol sbs)) = attachNextQuantifiedSymbolInfo m ts+      put newm+      let substedTerm = substTerm ts (symTerm sbs) v+      r <-+        local (addQuantifiedSymbol sb) $+          lowerSinglePrimCached'+            config+            substedTerm+      let ret qst = SBV.quantifiedBool $+            \(SBV.Exists (a :: SBVType t1)) ->+              r $ addQuantified sb (toDyn a) qst+      modify $ addBiMapIntermediate (SomeTerm t) (toDyn . ret)+      return ret+#else+lowerSinglePrimImpl _ ForallTerm {} =+  error "Quantifiers are only available when you build with SBV 10.1.0 or later"+lowerSinglePrimImpl _ ExistsTerm {} =+  error "Quantifiers are only available when you build with SBV 10.1.0 or later"+#endif+lowerSinglePrimImpl config t =   introSupportedPrimConstraint t $-    withPrim @a config $ do-      (m, r) <- lowerSinglePrimIntermediate config t m-      return (addBiMapIntermediate (SomeTerm t) (toDyn r) m, r)+    withPrim @a $ do+      r <- lowerSinglePrimIntermediate config t+      modify $ addBiMapIntermediate (SomeTerm t) (toDyn . r)+      return r  lowerSinglePrimIntermediate ::-  forall integerBitWidth a m.-  (HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>-  GrisetteSMTConfig integerBitWidth ->+  forall a m.+  (HasCallStack, SBVFreshMonad m) =>+  GrisetteSMTConfig ->   Term a ->-  SymBiMap ->-  m (SymBiMap, SBVType integerBitWidth a)-lowerSinglePrimIntermediate config (NotTerm _ a) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  return (m1, SBV.sNot a')-lowerSinglePrimIntermediate config (OrTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, a' SBV..|| b')-lowerSinglePrimIntermediate config (AndTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, a' SBV..&& b')-lowerSinglePrimIntermediate config (EqTerm _ (a :: Term v) b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvEq @v config a' b')-lowerSinglePrimIntermediate config (ITETerm _ c a b) m = do-  (m1, c') <- lowerSinglePrimCached config c m-  (m2, a') <- lowerSinglePrimCached config a m1-  (m3, b') <- lowerSinglePrimCached config b m2-  return (m3, sbvIte @a config c' a' b')-lowerSinglePrimIntermediate config (AddNumTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvAddNumTerm @a config a' b')-lowerSinglePrimIntermediate config (NegNumTerm _ a) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  return (m1, sbvNegNumTerm @a config a')-lowerSinglePrimIntermediate config (MulNumTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvMulNumTerm @a config a' b')-lowerSinglePrimIntermediate config (AbsNumTerm _ a) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  return (m1, sbvAbsNumTerm @a config a')-lowerSinglePrimIntermediate config (SignumNumTerm _ a) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  return (m1, sbvSignumNumTerm @a config a')-lowerSinglePrimIntermediate config (LtOrdTerm _ (a :: Term v) b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvLtOrdTerm @v config a' b')-lowerSinglePrimIntermediate config (LeOrdTerm _ (a :: Term v) b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvLeOrdTerm @v config a' b')-lowerSinglePrimIntermediate config (AndBitsTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvAndBitsTerm @a config a' b')-lowerSinglePrimIntermediate config (OrBitsTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvOrBitsTerm @a config a' b')-lowerSinglePrimIntermediate config (XorBitsTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvXorBitsTerm @a config a' b')-lowerSinglePrimIntermediate config (ComplementBitsTerm _ a) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  return (m1, sbvComplementBitsTerm @a config a')-lowerSinglePrimIntermediate config (ShiftLeftTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvShiftLeftTerm @a config a' b')-lowerSinglePrimIntermediate config (ShiftRightTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvShiftRightTerm @a config a' b')-lowerSinglePrimIntermediate config (RotateLeftTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvRotateLeftTerm @a config a' b')-lowerSinglePrimIntermediate config (RotateRightTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvRotateRightTerm @a config a' b')-lowerSinglePrimIntermediate config (ApplyTerm _ (f :: Term f) a) m = do-  (m1, l1) <- lowerSinglePrimCached config f m-  (m2, l2) <- lowerSinglePrimCached config a m1-  return (m2, sbvApplyTerm @f config l1 l2)-lowerSinglePrimIntermediate config (ToSignedTerm _ (a :: Term (u n))) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  return (m1, sbvToSigned (Proxy @u) (Proxy @n) config a')-lowerSinglePrimIntermediate config (ToUnsignedTerm _ (a :: Term (s n))) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  return (m1, sbvToUnsigned (Proxy @s) (Proxy @n) config a')+  RWST+    QuantifiedSymbols+    TermAll+    SymBiMap+    m+    (QuantifiedStack -> SBVType a)+lowerSinglePrimIntermediate config (NotTerm _ a) = do+  a' <- lowerSinglePrimCached' config a+  return $ SBV.sNot . a'+lowerSinglePrimIntermediate config (OrTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> a' qst SBV..|| b' qst+lowerSinglePrimIntermediate config (AndTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> a' qst SBV..&& b' qst+lowerSinglePrimIntermediate config (EqTerm _ (a :: Term v) b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvEq @v (a' qst) (b' qst)+lowerSinglePrimIntermediate config (DistinctTerm _ (args :: NonEmpty (Term t))) = do+  args' <- traverse (lowerSinglePrimCached' config) args+  return $ \qst -> sbvDistinct @t (fmap ($ qst) args')+lowerSinglePrimIntermediate config (ITETerm _ c a b) = do+  c' <- lowerSinglePrimCached' config c+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvIte @a (c' qst) (a' qst) (b' qst)+lowerSinglePrimIntermediate config (AddNumTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvAddNumTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (NegNumTerm _ a) = do+  a' <- lowerSinglePrimCached' config a+  return $ sbvNegNumTerm @a . a'+lowerSinglePrimIntermediate config (MulNumTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvMulNumTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (AbsNumTerm _ a) = do+  a' <- lowerSinglePrimCached' config a+  return $ sbvAbsNumTerm @a . a'+lowerSinglePrimIntermediate config (SignumNumTerm _ a) = do+  a' <- lowerSinglePrimCached' config a+  return $ sbvSignumNumTerm @a . a'+lowerSinglePrimIntermediate config (LtOrdTerm _ (a :: Term v) b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvLtOrdTerm @v (a' qst) (b' qst)+lowerSinglePrimIntermediate config (LeOrdTerm _ (a :: Term v) b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvLeOrdTerm @v (a' qst) (b' qst)+lowerSinglePrimIntermediate config (AndBitsTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvAndBitsTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (OrBitsTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvOrBitsTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (XorBitsTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvXorBitsTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (ComplementBitsTerm _ a) = do+  a' <- lowerSinglePrimCached' config a+  return $ sbvComplementBitsTerm @a . a'+lowerSinglePrimIntermediate config (ShiftLeftTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvShiftLeftTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (ShiftRightTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvShiftRightTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (RotateLeftTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvRotateLeftTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (RotateRightTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvRotateRightTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (ApplyTerm _ (f :: Term f) a) = do+  l1 <- lowerSinglePrimCached' config f+  l2 <- lowerSinglePrimCached' config a+  return $ \qst -> sbvApplyTerm @f (l1 qst) (l2 qst)+lowerSinglePrimIntermediate config (BitCastTerm _ (a :: Term x)) = do+  a' <- lowerSinglePrimCached' config a+  return $ sbvBitCast @x @a . a' lowerSinglePrimIntermediate   config-  (BVConcatTerm _ (a :: Term (bv l)) (b :: Term (bv r)))-  m = do-    (m1, a') <- lowerSinglePrimCached config a m-    (m2, b') <- lowerSinglePrimCached config b m1-    return (m2, sbvBVConcatTerm @bv config (Proxy @l) (Proxy @r) a' b')+  (BitCastOrTerm _ (d :: Term a) (a :: Term x)) = do+    d' <- lowerSinglePrimCached' config d+    a' <- lowerSinglePrimCached' config a+    return $ \qst -> sbvBitCastOr @x @a (d' qst) (a' qst) lowerSinglePrimIntermediate   config-  (BVExtendTerm _ signed (pr :: p r) (a :: Term (bv l)))-  m = do-    (m1, a') <- lowerSinglePrimCached config a m-    return (m1, sbvBVExtendTerm @bv config (Proxy @l) pr signed a')+  (BVConcatTerm _ (a :: Term (bv l)) (b :: Term (bv r))) =+    do+      a' <- lowerSinglePrimCached' config a+      b' <- lowerSinglePrimCached' config b+      return $ \qst -> sbvBVConcatTerm @bv (Proxy @l) (Proxy @r) (a' qst) (b' qst) lowerSinglePrimIntermediate   config-  (BVSelectTerm _ (pix :: p ix) (pw :: q w) (a :: Term (bv n)))-  m = do-    (m1, a') <- lowerSinglePrimCached config a m-    return (m1, sbvBVSelectTerm @bv config pix pw (Proxy @n) a')-lowerSinglePrimIntermediate config (DivIntegralTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvDivIntegralTerm @a config a' b')-lowerSinglePrimIntermediate config (ModIntegralTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvModIntegralTerm @a config a' b')-lowerSinglePrimIntermediate config (QuotIntegralTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvQuotIntegralTerm @a config a' b')-lowerSinglePrimIntermediate config (RemIntegralTerm _ a b) m = do-  (m1, a') <- lowerSinglePrimCached config a m-  (m2, b') <- lowerSinglePrimCached config b m1-  return (m2, sbvRemIntegralTerm @a config a' b')-lowerSinglePrimIntermediate config (FPTraitTerm _ trait a) m = do-  (m, a') <- lowerSinglePrimCached config a m-  return (m, sbvFPTraitTerm trait a')-lowerSinglePrimIntermediate config (FdivTerm _ a b) m = do-  (m, a) <- lowerSinglePrimCached config a m-  (m, b) <- lowerSinglePrimCached config b m-  return (m, sbvFdivTerm @a config a b)-lowerSinglePrimIntermediate config (RecipTerm _ a) m = do-  (m, a) <- lowerSinglePrimCached config a m-  return (m, sbvRecipTerm @a config a)-lowerSinglePrimIntermediate config (SqrtTerm _ a) m = do-  (m, a) <- lowerSinglePrimCached config a m-  return (m, sbvSqrtTerm @a config a)-lowerSinglePrimIntermediate config (FPUnaryTerm _ op a) m = do-  (m, a) <- lowerSinglePrimCached config a m-  return (m, sbvFPUnaryTerm op a)-lowerSinglePrimIntermediate config (FPBinaryTerm _ op a b) m = do-  (m, a) <- lowerSinglePrimCached config a m-  (m, b) <- lowerSinglePrimCached config b m-  return (m, sbvFPBinaryTerm op a b)-lowerSinglePrimIntermediate config (FPRoundingUnaryTerm _ op round a) m = do-  (m, round) <- lowerSinglePrimCached config round m-  (m, a) <- lowerSinglePrimCached config a m-  return (m, sbvFPRoundingUnaryTerm op round a)-lowerSinglePrimIntermediate config (FPRoundingBinaryTerm _ op round a b) m = do-  (m, round) <- lowerSinglePrimCached config round m-  (m, a) <- lowerSinglePrimCached config a m-  (m, b) <- lowerSinglePrimCached config b m-  return (m, sbvFPRoundingBinaryTerm op round a b)-lowerSinglePrimIntermediate config (FPFMATerm _ round a b c) m = do-  (m, round) <- lowerSinglePrimCached config round m-  (m, a) <- lowerSinglePrimCached config a m-  (m, b) <- lowerSinglePrimCached config b m-  (m, c) <- lowerSinglePrimCached config c m-  return (m, sbvFPFMATerm round a b c)-lowerSinglePrimIntermediate _ _ _ = undefined+  (BVExtendTerm _ signed (pr :: p r) (a :: Term (bv l))) =+    do+      a' <- lowerSinglePrimCached' config a+      return $ sbvBVExtendTerm @bv (Proxy @l) pr signed . a'+lowerSinglePrimIntermediate+  config+  (BVSelectTerm _ (pix :: p ix) (pw :: q w) (a :: Term (bv n))) =+    do+      a' <- lowerSinglePrimCached' config a+      return $ sbvBVSelectTerm @bv pix pw (Proxy @n) . a'+lowerSinglePrimIntermediate config (DivIntegralTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvDivIntegralTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (ModIntegralTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvModIntegralTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (QuotIntegralTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvQuotIntegralTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (RemIntegralTerm _ a b) = do+  a' <- lowerSinglePrimCached' config a+  b' <- lowerSinglePrimCached' config b+  return $ \qst -> sbvRemIntegralTerm @a (a' qst) (b' qst)+lowerSinglePrimIntermediate config (FPTraitTerm _ trait a) = do+  a' <- lowerSinglePrimCached' config a+  return $ sbvFPTraitTerm trait . a'+lowerSinglePrimIntermediate config (FdivTerm _ a b) = do+  a <- lowerSinglePrimCached' config a+  b <- lowerSinglePrimCached' config b+  return $ \qst -> sbvFdivTerm @a (a qst) (b qst)+lowerSinglePrimIntermediate config (RecipTerm _ a) = do+  a <- lowerSinglePrimCached' config a+  return $ sbvRecipTerm @a . a+lowerSinglePrimIntermediate config (FloatingUnaryTerm _ op a) = do+  a <- lowerSinglePrimCached' config a+  return $ sbvFloatingUnaryTerm @a op . a+lowerSinglePrimIntermediate config (PowerTerm _ a b) = do+  a <- lowerSinglePrimCached' config a+  b <- lowerSinglePrimCached' config b+  return $ \qst -> sbvPowerTerm @a (a qst) (b qst)+lowerSinglePrimIntermediate config (FPUnaryTerm _ op a) = do+  a <- lowerSinglePrimCached' config a+  return $ sbvFPUnaryTerm op . a+lowerSinglePrimIntermediate config (FPBinaryTerm _ op a b) = do+  a <- lowerSinglePrimCached' config a+  b <- lowerSinglePrimCached' config b+  return $ \qst -> sbvFPBinaryTerm op (a qst) (b qst)+lowerSinglePrimIntermediate config (FPRoundingUnaryTerm _ op round a) = do+  round <- lowerSinglePrimCached' config round+  a <- lowerSinglePrimCached' config a+  return $ \qst -> sbvFPRoundingUnaryTerm op (round qst) (a qst)+lowerSinglePrimIntermediate config (FPRoundingBinaryTerm _ op round a b) = do+  round <- lowerSinglePrimCached' config round+  a <- lowerSinglePrimCached' config a+  b <- lowerSinglePrimCached' config b+  return $ \qst -> sbvFPRoundingBinaryTerm op (round qst) (a qst) (b qst)+lowerSinglePrimIntermediate config (FPFMATerm _ round a b c) = do+  round <- lowerSinglePrimCached' config round+  a <- lowerSinglePrimCached' config a+  b <- lowerSinglePrimCached' config b+  c <- lowerSinglePrimCached' config c+  return $ \qst -> sbvFPFMATerm (round qst) (a qst) (b qst) (c qst)+lowerSinglePrimIntermediate config (FromIntegralTerm _ (b :: Term b)) = do+  b <- lowerSinglePrimCached' config b+  return $ sbvFromIntegralTerm @b @a . b+lowerSinglePrimIntermediate config (FromFPOrTerm _ d mode arg) = do+  d <- lowerSinglePrimCached' config d+  mode <- lowerSinglePrimCached' config mode+  arg <- lowerSinglePrimCached' config arg+  return $ \qst -> sbvFromFPOrTerm @a (d qst) (mode qst) (arg qst)+lowerSinglePrimIntermediate config (ToFPTerm _ mode (arg :: Term b) _ _) = do+  mode <- lowerSinglePrimCached' config mode+  arg <- lowerSinglePrimCached' config arg+  return $ \qst -> sbvToFPTerm @b (mode qst) (arg qst)+lowerSinglePrimIntermediate _ ConTerm {} = error "Should not happen"+lowerSinglePrimIntermediate _ SymTerm {} = error "Should not happen"+lowerSinglePrimIntermediate _ ForallTerm {} = error "Should not happen"+lowerSinglePrimIntermediate _ ExistsTerm {} = error "Should not happen"+lowerSinglePrimIntermediate _ UnaryTerm {} = error "Not implemented"+lowerSinglePrimIntermediate _ BinaryTerm {} = error "Not implemented"+lowerSinglePrimIntermediate _ TernaryTerm {} = error "Not implemented"  #if MIN_VERSION_sbv(10,3,0) preprocessUIFuncs ::@@ -799,8 +844,7 @@  -- | Parse an SBV model to a Grisette model. parseModel ::-  forall integerBitWidth.-  GrisetteSMTConfig integerBitWidth ->+  GrisetteSMTConfig ->   SBVI.SMTModel ->   SymBiMap ->   PM.Model@@ -809,7 +853,7 @@     Just funcs -> foldr goSingle emptyModel $ funcs ++ assocFuncs     _ -> error "SBV Failed to parse model"   where-    assocFuncs = (\(s, v) -> (s, ([([], v)], v))) <$> assoc+    assocFuncs = (\(s, v) -> (s, ([], v))) <$> assoc     goSingle :: (String, ([([SBVD.CV], SBVD.CV)], SBVD.CV)) -> PM.Model -> PM.Model     goSingle (name, cv) m = case findStringToSymbol name mp of       Just (SomeTypedSymbol (_ :: p r) s) ->

@@ -1,8 +1,12 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveLift #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables #-}  -- | -- Module      :   Grisette.Internal.Backend.SymBiMap--- Copyright   :   (c) Sirui Lu 2021-2023+-- Copyright   :   (c) Sirui Lu 2021-2024 -- License     :   BSD-3-Clause (see the LICENSE file) -- -- Maintainer  :   siruilu@cs.washington.edu@@ -16,47 +20,102 @@     addBiMapIntermediate,     findStringToSymbol,     lookupTerm,+    QuantifiedSymbolInfo (..),+    attachNextQuantifiedSymbolInfo,   ) where +import Control.DeepSeq (NFData) import Data.Dynamic (Dynamic) import qualified Data.HashMap.Strict as M+import Data.Hashable (Hashable)+import GHC.Generics (Generic) import GHC.Stack (HasCallStack)+import Grisette.Internal.Backend.QuantifiedStack (QuantifiedStack)+import Grisette.Internal.Core.Data.Symbol+  ( Symbol (IndexedSymbol, SimpleSymbol),+    withInfo,+  ) import Grisette.Internal.SymPrim.Prim.SomeTerm   ( SomeTerm,   ) import Grisette.Internal.SymPrim.Prim.Term-  ( SomeTypedSymbol,+  ( IsSymbolKind,+    SomeTypedAnySymbol,+    SomeTypedSymbol,+    TypedConstantSymbol,+    TypedSymbol (TypedSymbol),+    castSomeTypedSymbol,   )+import Language.Haskell.TH.Syntax (Lift)  -- | A bidirectional map between symbolic Grisette terms and sbv terms. data SymBiMap = SymBiMap-  { biMapToSBV :: M.HashMap SomeTerm Dynamic,-    biMapFromSBV :: M.HashMap String SomeTypedSymbol+  { biMapToSBV :: M.HashMap SomeTerm (QuantifiedStack -> Dynamic),+    biMapFromSBV :: M.HashMap String SomeTypedAnySymbol,+    quantifiedSymbolNum :: Int   }-  deriving (Show) +-- | Information about a quantified symbol.+newtype QuantifiedSymbolInfo = QuantifiedSymbolInfo Int+  deriving (Generic, Ord, Eq, Show, Hashable, Lift, NFData)++nextQuantifiedSymbolInfo :: SymBiMap -> (SymBiMap, QuantifiedSymbolInfo)+nextQuantifiedSymbolInfo (SymBiMap t f num) =+  (SymBiMap t f (num + 1), QuantifiedSymbolInfo num)++attachQuantifiedSymbolInfo ::+  QuantifiedSymbolInfo -> TypedConstantSymbol a -> TypedConstantSymbol a+attachQuantifiedSymbolInfo+  info+  (TypedSymbol (SimpleSymbol ident)) =+    TypedSymbol $ SimpleSymbol $ withInfo ident info+attachQuantifiedSymbolInfo+  info+  (TypedSymbol (IndexedSymbol ident idx)) =+    TypedSymbol $ IndexedSymbol (withInfo ident info) idx++-- | Attach the next quantified symbol info to a symbol.+attachNextQuantifiedSymbolInfo ::+  SymBiMap -> TypedConstantSymbol a -> (SymBiMap, TypedConstantSymbol a)+attachNextQuantifiedSymbolInfo m s =+  let (m', info) = nextQuantifiedSymbolInfo m+   in (m', attachQuantifiedSymbolInfo info s)+ -- | An empty bidirectional map. emptySymBiMap :: SymBiMap-emptySymBiMap = SymBiMap M.empty M.empty+emptySymBiMap = SymBiMap M.empty M.empty 0  -- | The size of the bidirectional map. sizeBiMap :: SymBiMap -> Int sizeBiMap = M.size . biMapToSBV  -- | Add a new entry to the bidirectional map.-addBiMap :: (HasCallStack) => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap-addBiMap s d n sb (SymBiMap t f) = SymBiMap (M.insert s d t) (M.insert n sb f)+addBiMap ::+  (HasCallStack) =>+  SomeTerm ->+  Dynamic ->+  String ->+  SomeTypedSymbol knd ->+  SymBiMap ->+  SymBiMap+addBiMap s d n sb (SymBiMap t f num) =+  case castSomeTypedSymbol sb of+    Just sb' -> SymBiMap (M.insert s (const d) t) (M.insert n sb' f) num+    _ -> error "Casting to AnySymbol, should not fail"  -- | Add a new entry to the bidirectional map for intermediate values.-addBiMapIntermediate :: (HasCallStack) => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap-addBiMapIntermediate s d (SymBiMap t f) = SymBiMap (M.insert s d t) f+addBiMapIntermediate ::+  (HasCallStack) => SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap+addBiMapIntermediate s d (SymBiMap t f num) = SymBiMap (M.insert s d t) f num  -- | Find a symbolic Grisette term from a string.-findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol-findStringToSymbol s (SymBiMap _ f) = M.lookup s f+findStringToSymbol :: (IsSymbolKind knd) => String -> SymBiMap -> Maybe (SomeTypedSymbol knd)+findStringToSymbol s (SymBiMap _ f _) = do+  r <- M.lookup s f+  castSomeTypedSymbol r  -- | Look up an sbv value with a symbolic Grisette term in the bidirectional -- map.-lookupTerm :: (HasCallStack) => SomeTerm -> SymBiMap -> Maybe Dynamic+lookupTerm :: (HasCallStack) => SomeTerm -> SymBiMap -> Maybe (QuantifiedStack -> Dynamic) lookupTerm t m = M.lookup t (biMapToSBV m)

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-} {-# LANGUAGE DerivingStrategies #-}@@ -67,7 +68,7 @@ import Grisette.Internal.Core.Control.Monad.Union (Union) import Grisette.Internal.Core.Data.Class.EvalSym (EvalSym (evalSym)) import Grisette.Internal.Core.Data.Class.ExtractSym-  ( ExtractSym (extractSym),+  ( ExtractSym (extractSymMaybe),   ) import Grisette.Internal.Core.Data.Class.GenSym   ( GenSym (fresh),@@ -91,8 +92,8 @@ import Grisette.Internal.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept)) import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==))) import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd (symCompare, (.<), (.<=), (.>), (.>=)))-import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon))-import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym))+import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon), ToCon1)+import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym), ToSym1) import Grisette.Internal.Core.Data.Class.TryMerge   ( TryMerge (tryMergeWithStrategy),     tryMerge,@@ -197,15 +198,15 @@ cbmcEither :: forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c cbmcEither l r v = either l r (unsafeCoerce v) --- | Wrap an 'Either' value in 'CBMCExceptT'+-- | Wrap an 'Either' value in t'CBMCExceptT' cbmcExcept :: (Monad m) => Either e a -> CBMCExceptT e m a cbmcExcept m = CBMCExceptT (return $ CBMCEither m) --- | Map the error and values in a 'CBMCExceptT'+-- | Map the error and values in a t'CBMCExceptT' mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b mapCBMCExceptT f m = CBMCExceptT $ (unsafeCoerce . f . unsafeCoerce) (runCBMCExceptT m) --- | Map the error in a 'CBMCExceptT'+-- | Map the error in a t'CBMCExceptT' withCBMCExceptT :: (Functor m) => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a withCBMCExceptT f = mapCBMCExceptT $ fmap $ either (Left . f) Right @@ -366,7 +367,7 @@   (ExtractSym (m (CBMCEither e a))) =>   ExtractSym (CBMCExceptT e m a)   where-  extractSym (CBMCExceptT v) = extractSym v+  extractSymMaybe (CBMCExceptT v) = extractSymMaybe v  instance   (Mergeable1 m, Mergeable e, Mergeable a) =>@@ -455,7 +456,7 @@   symCompare (CBMCExceptT l) (CBMCExceptT r) = symCompare l r  instance-  (ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b))) =>+  (ToCon1 m1 m2, ToCon e1 e2, ToCon a b) =>   ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)   where   toCon (CBMCExceptT v) = CBMCExceptT <$> toCon v@@ -467,7 +468,7 @@   toCon (CBMCExceptT v) = toCon v  instance-  (ToSym (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b))) =>+  (ToSym e1 e2, ToSym a b, ToSym1 m1 m2) =>   ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)   where   toSym (CBMCExceptT v) = CBMCExceptT $ toSym v

@@ -58,9 +58,9 @@     evalSym1,   ) import Grisette.Internal.Core.Data.Class.ExtractSym-  ( ExtractSym (extractSym),-    ExtractSym1 (liftExtractSym),-    extractSym1,+  ( ExtractSym (extractSymMaybe),+    ExtractSym1 (liftExtractSymMaybe),+    extractSymMaybe1,   ) import Grisette.Internal.Core.Data.Class.Function (Function ((#))) import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))@@ -154,7 +154,6 @@ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.SymPrim--- >>> :set -XScopedTypeVariables  -- | 'Union' is the 'UnionBase' container (hidden) enhanced with -- 'MergingStrategy'@@ -469,7 +468,7 @@   toSym = toSym1  instance ToSym1 Union Union where-  liftToSym = fmap+  liftToSym f = tryMerge . fmap f  instance ToSym (Union Bool) SymBool where   toSym = simpleMerge . fmap con@@ -545,13 +544,13 @@       unionIf = maybe mrgIfPropagatedStrategy mrgIfWithStrategy strategy  instance (ExtractSym a) => ExtractSym (Union a) where-  extractSym = extractSym1+  extractSymMaybe = extractSymMaybe1  instance ExtractSym1 Union where-  liftExtractSym e v = go $ unionBase v+  liftExtractSymMaybe e v = go $ unionBase v     where       go (UnionSingle x) = e x-      go (UnionIf _ _ cond t f) = extractSym cond <> go t <> go f+      go (UnionIf _ _ cond t f) = extractSymMaybe cond <> go t <> go f  instance (Hashable a) => Hashable (Union a) where   s `hashWithSalt` (UAny u) = s `hashWithSalt` (0 :: Int) `hashWithSalt` u

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -13,7 +14,14 @@ -- Maintainer  :   siruilu@cs.washington.edu -- Stability   :   Experimental -- Portability :   GHC only-module Grisette.Internal.Core.Data.Class.BitCast (BitCast (..)) where+module Grisette.Internal.Core.Data.Class.BitCast+  ( BitCast (..),+    BitCastCanonical (..),+    BitCastOr (..),+    bitCastOrCanonical,+    BitCastOrCanonical,+  )+where  import Control.Monad.ST (ST, runST) import Data.Array.ST (MArray (newArray), STUArray, readArray)@@ -22,6 +30,22 @@ import Data.Word (Word32, Word64)  -- | Type class for bit-casting between types.+--+-- __Special Considerations for Floating-Point Types:__+--+-- Typically, bit-casting a value from type @a@ to type @b@ and then back to+-- type @a@ should result in the original value. However, this is not always+-- true for floating-point values. In SMT-LIB2, there is only one NaN value with+-- multiple bit representations.+--+-- Given this, we do not provide 'BitCast' for the t'Grisette.SymPrim.FP' type,+-- instead, we use the 'bitCastOrCanonical' function to use a canonical+-- representation for the NaN values.+--+-- If your application requires distinguishing between different NaN values,+-- it is recommended to define your own floating-point type using bit-vectors.+-- This allows you to check for NaN values and perform operations by bitcasting+-- back to the provided floating-point types when they are not NaN values. class BitCast from to where   bitCast :: from -> to @@ -54,3 +78,27 @@   ST s b bitcastWithMArray x =   newArray (0 :: Int, 0) x >>= castSTUArray >>= flip readArray 0++-- | The canonical value when the bitcast cannot be precisely performed.+--+-- For example, with SMT-LIB2, there is only one NaN for floating point numbers,+-- with multiple bit representations. Our underlying t'Grisette.SymPrim.FP' type+-- also follows this convention. This means that we cannot precisely bitcast a+-- t'Grisette.SymPrim.FP' to other types. So instead, we bitcast the NaN value+-- to a canonical representation, defined with this type class.+class BitCastCanonical from to where+  bitCastCanonicalValue :: proxy from -> to++-- | Bitcasting a value. If the value cannot be precisely bitcast, use the+-- default value.+class BitCastOr from to where+  bitCastOr :: to -> from -> to++-- | Constraint for bitcasting a value and when the value cannot be precisely+-- bitcast, use the canonical value.+type BitCastOrCanonical a b = (BitCastCanonical a b, BitCastOr a b)++-- | Bitcasting a value and when the value cannot be precisely bitcast, use the+-- canonical value.+bitCastOrCanonical :: (BitCastOrCanonical from to) => from -> to+bitCastOrCanonical x = bitCastOr (bitCastCanonicalValue [x]) x

@@ -43,11 +43,6 @@ -- >>> import Grisette.Core -- >>> import Grisette.SymPrim -- >>> import Grisette.Utils--- >>> :set -XDataKinds--- >>> :set -XBinaryLiterals--- >>> :set -XFlexibleContexts--- >>> :set -XFlexibleInstances--- >>> :set -XFunctionalDependencies  -- | Bit vector operations. Including concatenation ('bvConcat'), -- extension ('bvZext', 'bvSext', 'bvExt'), and selection

@@ -332,7 +332,7 @@   handle ->   -- | Initial symbolic inputs. The solver will try to find a   -- program that works on all the inputs representable by these inputs (see-  -- 'CEGISCondition').+  -- t'CEGISCondition').   [input] ->   -- | The condition for the solver to solve. All the   -- symbolic constants that are not in the inputs will@@ -393,7 +393,7 @@   handle ->   -- | Initial symbolic inputs. The solver will try to find a   -- program that works on all the inputs representable by it (see-  -- 'CEGISCondition').+  -- t'CEGISCondition').   inputs ->   -- | The condition for the solver to solve. All the   -- symbolic constants that are not in the inputs will@@ -751,7 +751,7 @@  -- | -- CEGIS with multiple (possibly symbolic) inputs. Solves the following formula--- (see 'CEGISCondition' for details).+-- (see t'CEGISCondition' for details). -- -- \[ --   \forall P. (\exists I\in\mathrm{inputs}. \mathrm{pre}(P, I)) \wedge (\forall I\in\mathrm{inputs}. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I))@@ -769,7 +769,7 @@   config ->   -- | Initial symbolic inputs. The solver will try to find a   -- program that works on all the inputs representable by these inputs (see-  -- 'CEGISCondition').+  -- t'CEGISCondition').   [input] ->   -- | The condition for the solver to solve. All the   -- symbolic constants that are not in the inputs will@@ -795,7 +795,6 @@ -- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make -- the solution unique. ----- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger] -- >>> cegis z3 x (\x -> cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2)) -- (...,CEGISSuccess (Model {c -> -1 :: Integer}))@@ -809,7 +808,7 @@   config ->   -- | Initial symbolic inputs. The solver will try to find a   -- program that works on all the inputs representable by it (see-  -- 'CEGISCondition').+  -- t'CEGISCondition').   inputs ->   -- | The condition for the solver to solve. All the   -- symbolic constants that are not in the inputs will@@ -917,7 +916,6 @@ -- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make -- the solution unique. ----- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger] -- >>> import Control.Monad.Except -- >>> :{@@ -993,7 +991,6 @@ -- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make -- the solution unique. ----- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger] -- >>> import Control.Monad.Except -- >>> :{@@ -1031,7 +1028,6 @@ -- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make -- the solution unique. ----- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger] -- >>> cegisForAll z3 x $ cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2) -- (...,CEGISSuccess (Model {c -> -1 :: Integer}))

@@ -42,8 +42,6 @@ -- >>> import Grisette.SymPrim -- >>> import Grisette.Lib.Control.Monad -- >>> import Control.Monad.Except--- >>> :set -XOverloadedStrings--- >>> :set -XFlexibleContexts  -- | This class indicates that the error type @to@ can always represent the -- error type @from@.@@ -152,7 +150,7 @@ -- The symbolic execution will continue on the then-branch, where the condition is true. -- For the else branch, where the condition is false, the execution will be terminated. ----- The resulting monadic environment should be compatible with the 'AssertionError'+-- The resulting monadic environment should be compatible with the t'AssertionError' -- error type. See 'TransformError' type class for details. -- -- __/Examples/__:@@ -182,7 +180,7 @@ -- >>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError Union Integer -- ExceptT {If (! a) (Left AssertionError) (Right 1)} ----- 'AssertionError' is compatible with 'VerificationConditions':+-- t'AssertionError' is compatible with 'VerificationConditions': -- -- >>> symAssert (ssym "a") :: ExceptT VerificationConditions Union () -- ExceptT {If (! a) (Left AssertionViolation) (Right ())}

@@ -55,6 +55,7 @@ import Data.Functor.Const (Const) import Data.Functor.Product (Product) import Data.Functor.Sum (Sum)+import qualified Data.HashSet as HS import Data.Int (Int16, Int32, Int64, Int8) import Data.Kind (Type) import Data.Maybe (fromJust)@@ -91,11 +92,18 @@     toCon1,     toCon2,   )+import Grisette.Internal.SymPrim.AlgReal (AlgReal) import Grisette.Internal.SymPrim.BV (IntN, WordN)-import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)-import Grisette.Internal.SymPrim.GeneralFun (type (-->))-import Grisette.Internal.SymPrim.Prim.Model (Model, evaluateTerm)-import Grisette.Internal.SymPrim.Prim.Term (LinkedRep, SupportedPrim)+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)+import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))+import Grisette.Internal.SymPrim.Prim.Model (Model, evalTerm)+import Grisette.Internal.SymPrim.Prim.Term+  ( LinkedRep,+    SupportedPrim,+    SymRep (SymType),+    someTypedSymbol,+  )+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal)) import Grisette.Internal.SymPrim.SymBV   ( SymIntN (SymIntN),     SymWordN (SymWordN),@@ -108,7 +116,7 @@ import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))-import Grisette.Internal.SymPrim.TabularFun (type (=->))+import Grisette.Internal.SymPrim.TabularFun (type (=->) (TabularFun)) import Grisette.Internal.TH.DeriveBuiltin (deriveBuiltins) import Grisette.Internal.TH.DeriveInstanceProvider   ( Strategy (ViaDefault, ViaDefault1),@@ -119,7 +127,6 @@ -- >>> import Grisette.Core -- >>> import Grisette.SymPrim -- >>> import Data.Proxy--- >>> :set -XTypeApplications  -- | Evaluating symbolic values with some model. This would substitute the -- symbols (symbolic constants) with the values in the model.@@ -348,6 +355,7 @@ CONCRETE_EVALUATESYM(Ordering) CONCRETE_EVALUATESYM_BV(IntN) CONCRETE_EVALUATESYM_BV(WordN)+CONCRETE_EVALUATESYM(AlgReal) #endif  instance (ValidFP eb fb) => EvalSym (FP eb fb) where@@ -357,23 +365,24 @@ #define EVALUATE_SYM_SIMPLE(symtype) \ instance EvalSym symtype where \   evalSym fillDefault model (symtype t) = \-    symtype $ evaluateTerm fillDefault model t+    symtype $ evalTerm fillDefault model HS.empty t  #define EVALUATE_SYM_BV(symtype) \ instance (KnownNat n, 1 <= n) => EvalSym (symtype n) where \   evalSym fillDefault model (symtype t) = \-    symtype $ evaluateTerm fillDefault model t+    symtype $ evalTerm fillDefault model HS.empty t  #define EVALUATE_SYM_FUN(cop, op, cons) \ instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \   EvalSym (op sa sb) where \   evalSym fillDefault model (cons t) = \-    cons $ evaluateTerm fillDefault model t+    cons $ evalTerm fillDefault model HS.empty t  #if 1 EVALUATE_SYM_SIMPLE(SymBool) EVALUATE_SYM_SIMPLE(SymInteger) EVALUATE_SYM_SIMPLE(SymFPRoundingMode)+EVALUATE_SYM_SIMPLE(SymAlgReal) EVALUATE_SYM_BV(SymIntN) EVALUATE_SYM_BV(SymWordN) EVALUATE_SYM_FUN((=->), (=~>), SymTabularFun)@@ -382,7 +391,7 @@  instance (ValidFP eb sb) => EvalSym (SymFP eb sb) where   evalSym fillDefault model (SymFP t) =-    SymFP $ evaluateTerm fillDefault model t+    SymFP $ evalTerm fillDefault model HS.empty t  -- Instances deriveBuiltins@@ -408,6 +417,7 @@     ''(,,,,,,,,,,,,,,),     ''AssertionError,     ''VerificationConditions,+    ''NotRepresentableFPError,     ''Identity,     ''Monoid.Dual,     ''Monoid.Sum,@@ -629,3 +639,14 @@       g fillDefault model d     )   {-# INLINE liftEvalSym2 #-}++instance (EvalSym a, EvalSym b) => EvalSym (a =-> b) where+  evalSym fillDefault model (TabularFun s t) =+    TabularFun+      (evalSym fillDefault model s)+      (evalSym fillDefault model t)++instance (EvalSym (SymType b)) => EvalSym (a --> b) where+  evalSym fillDefault model (GeneralFun s t) =+    GeneralFun s $+      evalTerm fillDefault model (HS.singleton $ someTypedSymbol s) t

@@ -4,11 +4,14 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}@@ -25,15 +28,17 @@   ( -- * Extracting symbolic constant set from a value     ExtractSym (..),     ExtractSym1 (..),+    extractSymMaybe1,     extractSym1,     ExtractSym2 (..),+    extractSymMaybe2,     extractSym2,      -- * Generic 'ExtractSym'     ExtractSymArgs (..),     GExtractSym (..),-    genericExtractSym,-    genericLiftExtractSym,+    genericExtractSymMaybe,+    genericLiftExtractSymMaybe,   ) where @@ -50,12 +55,15 @@ import Data.Functor.Const (Const) import Data.Functor.Product (Product) import Data.Functor.Sum (Sum)+import qualified Data.HashSet as HS import Data.Int (Int16, Int32, Int64, Int8) import Data.Kind (Type)+import Data.Maybe (fromJust) import Data.Monoid (Alt, Ap) import qualified Data.Monoid as Monoid import Data.Ord (Down) import qualified Data.Text as T+import Data.Typeable (type (:~~:) (HRefl)) import Data.Word (Word16, Word32, Word64, Word8) import GHC.TypeNats (KnownNat, type (<=)) import Generics.Deriving@@ -73,18 +81,28 @@     type (:+:) (L1, R1),     type (:.:) (Comp1),   )-import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Internal.Core.Control.Exception+  ( AssertionError,+    VerificationConditions,+  )+import Grisette.Internal.SymPrim.AlgReal (AlgReal) import Grisette.Internal.SymPrim.BV (IntN, WordN)-import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)-import Grisette.Internal.SymPrim.GeneralFun (type (-->))+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)+import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun)) import Grisette.Internal.SymPrim.Prim.Model-  ( SymbolSet (SymbolSet),+  ( AnySymbolSet,+    SymbolSet (SymbolSet),   ) import Grisette.Internal.SymPrim.Prim.Term-  ( LinkedRep,+  ( IsSymbolKind (decideSymbolKind),+    LinkedRep,     SupportedPrim,+    SymRep (SymType),+    SymbolKind,+    someTypedSymbol,   ) import Grisette.Internal.SymPrim.Prim.TermUtils (extractTerm)+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal)) import Grisette.Internal.SymPrim.SymBV   ( SymIntN (SymIntN),     SymWordN (SymWordN),@@ -97,7 +115,7 @@ import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))-import Grisette.Internal.SymPrim.TabularFun (type (=->))+import Grisette.Internal.SymPrim.TabularFun (type (=->) (TabularFun)) import Grisette.Internal.TH.DeriveBuiltin (deriveBuiltins) import Grisette.Internal.TH.DeriveInstanceProvider   ( Strategy (ViaDefault, ViaDefault1),@@ -114,10 +132,10 @@ -- | Extracts all the symbols (symbolic constants) that are transitively -- contained in the given value. ----- >>> extractSym ("a" :: SymBool) :: SymbolSet+-- >>> extractSym ("a" :: SymBool) -- SymbolSet {a :: Bool} ----- >>> extractSym (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: Union [SymBool]) :: SymbolSet+-- >>> extractSym (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: Union [SymBool]) -- SymbolSet {a :: Bool, b :: Bool, c :: Bool, d :: Bool} -- -- __Note 1:__ This type class can be derived for algebraic data types.@@ -125,145 +143,178 @@ -- -- > data X = ... deriving Generic deriving ExtractSym via (Default X) class ExtractSym a where-  extractSym :: a -> SymbolSet+  extractSym :: a -> AnySymbolSet+  extractSym = fromJust . extractSymMaybe+  {-# INLINE extractSym #-}+  extractSymMaybe :: (IsSymbolKind knd) => a -> Maybe (SymbolSet knd)  -- | Lifting of 'ExtractSym' to unary type constructors. class   (forall a. (ExtractSym a) => ExtractSym (f a)) =>   ExtractSym1 f   where-  -- | Lifts the 'extractSym' function to unary type constructors.-  liftExtractSym :: (a -> SymbolSet) -> f a -> SymbolSet+  -- | Lifts the 'extractSymMaybe' function to unary type constructors.+  liftExtractSymMaybe ::+    (IsSymbolKind knd) =>+    (a -> Maybe (SymbolSet knd)) ->+    f a ->+    Maybe (SymbolSet knd)  -- | Lift the standard 'extractSym' to unary type constructors.-extractSym1 :: (ExtractSym1 f, ExtractSym a) => f a -> SymbolSet-extractSym1 = liftExtractSym extractSym+extractSym1 ::+  (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>+  f a ->+  SymbolSet knd+extractSym1 = fromJust . liftExtractSymMaybe extractSymMaybe {-# INLINE extractSym1 #-} +-- | Lift the standard 'extractSymMaybe' to unary type constructors.+extractSymMaybe1 ::+  (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>+  f a ->+  Maybe (SymbolSet knd)+extractSymMaybe1 = liftExtractSymMaybe extractSymMaybe+{-# INLINE extractSymMaybe1 #-}+ -- | Lifting of 'ExtractSym' to binary type constructors. class   (forall a. (ExtractSym a) => ExtractSym1 (f a)) =>   ExtractSym2 f   where-  -- | Lifts the 'extractSym' function to binary type constructors.-  liftExtractSym2 ::-    (a -> SymbolSet) -> (b -> SymbolSet) -> f a b -> SymbolSet+  -- | Lifts the 'extractSymMaybe' function to binary type constructors.+  liftExtractSymMaybe2 ::+    (IsSymbolKind knd) =>+    (a -> Maybe (SymbolSet knd)) ->+    (b -> Maybe (SymbolSet knd)) ->+    f a b ->+    Maybe (SymbolSet knd)  -- | Lift the standard 'extractSym' to binary type constructors. extractSym2 ::-  (ExtractSym2 f, ExtractSym a, ExtractSym b) =>+  (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>   f a b ->-  SymbolSet-extractSym2 = liftExtractSym2 extractSym extractSym-{-# INLINE extractSym2 #-}+  SymbolSet knd+extractSym2 = fromJust . liftExtractSymMaybe2 extractSymMaybe extractSymMaybe +-- | Lift the standard 'extractSymMaybe' to binary type constructors.+extractSymMaybe2 ::+  (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>+  f a b ->+  Maybe (SymbolSet knd)+extractSymMaybe2 = liftExtractSymMaybe2 extractSymMaybe extractSymMaybe+{-# INLINE extractSymMaybe2 #-}+ -- Derivations  -- | The arguments to the generic 'extractSym' function.-data family ExtractSymArgs arity a :: Type+data family ExtractSymArgs arity (knd :: SymbolKind) a :: Type -data instance ExtractSymArgs Arity0 _ = ExtractSymArgs0+data instance ExtractSymArgs Arity0 _ _ = ExtractSymArgs0 -newtype instance ExtractSymArgs Arity1 a-  = ExtractSymArgs1 (a -> SymbolSet)+newtype instance ExtractSymArgs Arity1 knd a+  = ExtractSymArgs1 (a -> Maybe (SymbolSet knd))  -- | The class of types that can generically extract the symbols. class GExtractSym arity f where-  gextractSym :: ExtractSymArgs arity a -> f a -> SymbolSet+  gextractSymMaybe ::+    (IsSymbolKind knd) =>+    ExtractSymArgs arity knd a ->+    f a ->+    Maybe (SymbolSet knd)  instance GExtractSym arity V1 where-  gextractSym _ _ = mempty-  {-# INLINE gextractSym #-}+  gextractSymMaybe _ _ = Just mempty+  {-# INLINE gextractSymMaybe #-}  instance GExtractSym arity U1 where-  gextractSym _ _ = mempty-  {-# INLINE gextractSym #-}+  gextractSymMaybe _ _ = Just mempty+  {-# INLINE gextractSymMaybe #-}  instance (GExtractSym arity a) => GExtractSym arity (M1 i c a) where-  gextractSym args (M1 x) = gextractSym args x-  {-# INLINE gextractSym #-}+  gextractSymMaybe args (M1 x) = gextractSymMaybe args x+  {-# INLINE gextractSymMaybe #-}  instance (ExtractSym a) => GExtractSym arity (K1 i a) where-  gextractSym _ (K1 x) = extractSym x-  {-# INLINE gextractSym #-}+  gextractSymMaybe _ (K1 x) = extractSymMaybe x+  {-# INLINE gextractSymMaybe #-}  instance   (GExtractSym arity a, GExtractSym arity b) =>   GExtractSym arity (a :+: b)   where-  gextractSym args (L1 x) = gextractSym args x-  gextractSym args (R1 x) = gextractSym args x-  {-# INLINE gextractSym #-}+  gextractSymMaybe args (L1 x) = gextractSymMaybe args x+  gextractSymMaybe args (R1 x) = gextractSymMaybe args x+  {-# INLINE gextractSymMaybe #-}  instance   (GExtractSym arity a, GExtractSym arity b) =>   GExtractSym arity (a :*: b)   where-  gextractSym args (x :*: y) =-    gextractSym args x <> gextractSym args y-  {-# INLINE gextractSym #-}+  gextractSymMaybe args (x :*: y) =+    gextractSymMaybe args x <> gextractSymMaybe args y+  {-# INLINE gextractSymMaybe #-}  instance GExtractSym Arity1 Par1 where-  gextractSym (ExtractSymArgs1 f) (Par1 x) = f x-  {-# INLINE gextractSym #-}+  gextractSymMaybe (ExtractSymArgs1 f) (Par1 x) = f x+  {-# INLINE gextractSymMaybe #-}  instance (ExtractSym1 a) => GExtractSym Arity1 (Rec1 a) where-  gextractSym (ExtractSymArgs1 f) (Rec1 x) =-    liftExtractSym f x-  {-# INLINE gextractSym #-}+  gextractSymMaybe (ExtractSymArgs1 f) (Rec1 x) =+    liftExtractSymMaybe f x+  {-# INLINE gextractSymMaybe #-}  instance   (ExtractSym1 f, GExtractSym Arity1 g) =>   GExtractSym Arity1 (f :.: g)   where-  gextractSym targs (Comp1 x) =-    liftExtractSym (gextractSym targs) x-  {-# INLINE gextractSym #-}+  gextractSymMaybe targs (Comp1 x) =+    liftExtractSymMaybe (gextractSymMaybe targs) x+  {-# INLINE gextractSymMaybe #-}  -- | Generic 'extractSym' function.-genericExtractSym ::-  (Generic a, GExtractSym Arity0 (Rep a)) =>+genericExtractSymMaybe ::+  (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) =>   a ->-  SymbolSet-genericExtractSym = gextractSym ExtractSymArgs0 . from+  Maybe (SymbolSet knd)+genericExtractSymMaybe = gextractSymMaybe ExtractSymArgs0 . from --- | Generic 'liftExtractSym' function.-genericLiftExtractSym ::-  (Generic1 f, GExtractSym Arity1 (Rep1 f)) =>-  (a -> SymbolSet) ->+-- | Generic 'liftExtractSymMaybe' function.+genericLiftExtractSymMaybe ::+  (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) =>+  (a -> Maybe (SymbolSet knd)) ->   f a ->-  SymbolSet-genericLiftExtractSym f =-  gextractSym (ExtractSymArgs1 f) . from1+  Maybe (SymbolSet knd)+genericLiftExtractSymMaybe f =+  gextractSymMaybe (ExtractSymArgs1 f) . from1  instance   (Generic a, GExtractSym Arity0 (Rep a)) =>   ExtractSym (Default a)   where-  extractSym = genericExtractSym . unDefault-  {-# INLINE extractSym #-}+  extractSymMaybe = genericExtractSymMaybe . unDefault+  {-# INLINE extractSymMaybe #-}  instance   (Generic1 f, GExtractSym Arity1 (Rep1 f), ExtractSym a) =>   ExtractSym (Default1 f a)   where-  extractSym = extractSym1-  {-# INLINE extractSym #-}+  extractSymMaybe = extractSymMaybe1+  {-# INLINE extractSymMaybe #-}  instance   (Generic1 f, GExtractSym Arity1 (Rep1 f)) =>   ExtractSym1 (Default1 f)   where-  liftExtractSym f = genericLiftExtractSym f . unDefault1-  {-# INLINE liftExtractSym #-}+  liftExtractSymMaybe f = genericLiftExtractSymMaybe f . unDefault1+  {-# INLINE liftExtractSymMaybe #-}  #define CONCRETE_EXTRACT_SYMBOLICS(type) \ instance ExtractSym type where \-  extractSym _ = mempty+  extractSymMaybe _ = return mempty  #define CONCRETE_EXTRACT_SYMBOLICS_BV(type) \ instance (KnownNat n, 1 <= n) => ExtractSym (type n) where \-  extractSym _ = mempty+  extractSymMaybe _ = return mempty  #if 1 CONCRETE_EXTRACT_SYMBOLICS(Bool)@@ -289,28 +340,45 @@ CONCRETE_EXTRACT_SYMBOLICS(Ordering) CONCRETE_EXTRACT_SYMBOLICS_BV(WordN) CONCRETE_EXTRACT_SYMBOLICS_BV(IntN)+CONCRETE_EXTRACT_SYMBOLICS(AlgReal) #endif  instance (ValidFP eb sb) => ExtractSym (FP eb sb) where-  extractSym _ = mempty+  extractSymMaybe _ = return mempty  #define EXTRACT_SYMBOLICS_SIMPLE(symtype) \ instance ExtractSym symtype where \-  extractSym (symtype t) = SymbolSet $ extractTerm t+  extractSymMaybe :: \+    forall knd. (IsSymbolKind knd) => symtype -> Maybe (SymbolSet knd); \+  extractSymMaybe (symtype t) = \+    case decideSymbolKind @knd of\+      Left HRefl -> SymbolSet <$> extractTerm HS.empty t; \+      Right HRefl -> SymbolSet <$> extractTerm HS.empty t  #define EXTRACT_SYMBOLICS_BV(symtype) \ instance (KnownNat n, 1 <= n) => ExtractSym (symtype n) where \-  extractSym (symtype t) = SymbolSet $ extractTerm t+  extractSymMaybe :: \+    forall knd. (IsSymbolKind knd) => symtype n -> Maybe (SymbolSet knd); \+  extractSymMaybe (symtype t) = \+    case decideSymbolKind @knd of\+      Left HRefl -> SymbolSet <$> extractTerm HS.empty t; \+      Right HRefl -> SymbolSet <$> extractTerm HS.empty t  #define EXTRACT_SYMBOLICS_FUN(cop, op, cons) \ instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \   ExtractSym (op sa sb) where \-  extractSym (cons t) = SymbolSet $ extractTerm t+  extractSymMaybe :: \+    forall knd. (IsSymbolKind knd) => op sa sb -> Maybe (SymbolSet knd); \+  extractSymMaybe (cons t) = \+    case decideSymbolKind @knd of \+      Left HRefl -> Nothing; \+      Right HRefl -> SymbolSet <$> extractTerm HS.empty t  #if 1 EXTRACT_SYMBOLICS_SIMPLE(SymBool) EXTRACT_SYMBOLICS_SIMPLE(SymInteger) EXTRACT_SYMBOLICS_SIMPLE(SymFPRoundingMode)+EXTRACT_SYMBOLICS_SIMPLE(SymAlgReal) EXTRACT_SYMBOLICS_BV(SymIntN) EXTRACT_SYMBOLICS_BV(SymWordN) EXTRACT_SYMBOLICS_FUN((=->), (=~>), SymTabularFun)@@ -318,7 +386,12 @@ #endif  instance (ValidFP eb fb) => ExtractSym (SymFP eb fb) where-  extractSym (SymFP t) = SymbolSet $ extractTerm t+  extractSymMaybe ::+    forall knd. (IsSymbolKind knd) => SymFP eb fb -> Maybe (SymbolSet knd)+  extractSymMaybe (SymFP t) =+    case decideSymbolKind @knd of+      Left HRefl -> SymbolSet <$> extractTerm HS.empty t+      Right HRefl -> SymbolSet <$> extractTerm HS.empty t  -- Instances deriveBuiltins@@ -344,6 +417,7 @@     ''(,,,,,,,,,,,,,,),     ''AssertionError,     ''VerificationConditions,+    ''NotRepresentableFPError,     ''Identity,     ''Monoid.Dual,     ''Monoid.Sum,@@ -387,75 +461,75 @@   (ExtractSym1 m, ExtractSym e, ExtractSym a) =>   ExtractSym (ExceptT e m a)   where-  extractSym = extractSym1-  {-# INLINE extractSym #-}+  extractSymMaybe = extractSymMaybe1+  {-# INLINE extractSymMaybe #-}  instance   (ExtractSym1 m, ExtractSym e) =>   ExtractSym1 (ExceptT e m)   where-  liftExtractSym f (ExceptT v) =-    liftExtractSym (liftExtractSym f) v-  {-# INLINE liftExtractSym #-}+  liftExtractSymMaybe f (ExceptT v) =+    liftExtractSymMaybe (liftExtractSymMaybe f) v+  {-# INLINE liftExtractSymMaybe #-}  -- MaybeT instance   (ExtractSym1 m, ExtractSym a) =>   ExtractSym (MaybeT m a)   where-  extractSym = extractSym1-  {-# INLINE extractSym #-}+  extractSymMaybe = extractSymMaybe1+  {-# INLINE extractSymMaybe #-}  instance   (ExtractSym1 m) =>   ExtractSym1 (MaybeT m)   where-  liftExtractSym f (MaybeT v) =-    liftExtractSym (liftExtractSym f) v-  {-# INLINE liftExtractSym #-}+  liftExtractSymMaybe f (MaybeT v) =+    liftExtractSymMaybe (liftExtractSymMaybe f) v+  {-# INLINE liftExtractSymMaybe #-}  -- WriterT instance   (ExtractSym1 m, ExtractSym w, ExtractSym a) =>   ExtractSym (WriterLazy.WriterT w m a)   where-  extractSym = extractSym1-  {-# INLINE extractSym #-}+  extractSymMaybe = extractSymMaybe1+  {-# INLINE extractSymMaybe #-}  instance   (ExtractSym1 m, ExtractSym w) =>   ExtractSym1 (WriterLazy.WriterT w m)   where-  liftExtractSym f (WriterLazy.WriterT v) =-    liftExtractSym (liftExtractSym2 f extractSym) v-  {-# INLINE liftExtractSym #-}+  liftExtractSymMaybe f (WriterLazy.WriterT v) =+    liftExtractSymMaybe (liftExtractSymMaybe2 f extractSymMaybe) v+  {-# INLINE liftExtractSymMaybe #-}  instance   (ExtractSym1 m, ExtractSym w, ExtractSym a) =>   ExtractSym (WriterStrict.WriterT w m a)   where-  extractSym = extractSym1-  {-# INLINE extractSym #-}+  extractSymMaybe = extractSymMaybe1+  {-# INLINE extractSymMaybe #-}  instance   (ExtractSym1 m, ExtractSym w) =>   ExtractSym1 (WriterStrict.WriterT w m)   where-  liftExtractSym f (WriterStrict.WriterT v) =-    liftExtractSym (liftExtractSym2 f extractSym) v-  {-# INLINE liftExtractSym #-}+  liftExtractSymMaybe f (WriterStrict.WriterT v) =+    liftExtractSymMaybe (liftExtractSymMaybe2 f extractSymMaybe) v+  {-# INLINE liftExtractSymMaybe #-}  -- IdentityT instance   (ExtractSym1 m, ExtractSym a) =>   ExtractSym (IdentityT m a)   where-  extractSym = extractSym1-  {-# INLINE extractSym #-}+  extractSymMaybe = extractSymMaybe1+  {-# INLINE extractSymMaybe #-}  instance (ExtractSym1 m) => ExtractSym1 (IdentityT m) where-  liftExtractSym f (IdentityT v) = liftExtractSym f v-  {-# INLINE liftExtractSym #-}+  liftExtractSymMaybe f (IdentityT v) = liftExtractSymMaybe f v+  {-# INLINE liftExtractSymMaybe #-}  -- Product deriving via@@ -492,9 +566,9 @@   (ExtractSym1 f, ExtractSym1 g) =>   ExtractSym1 (Compose f g)   where-  liftExtractSym f (Compose l) =-    liftExtractSym (liftExtractSym f) l-  {-# INLINE liftExtractSym #-}+  liftExtractSymMaybe f (Compose l) =+    liftExtractSymMaybe (liftExtractSymMaybe f) l+  {-# INLINE liftExtractSymMaybe #-}  -- Const deriving via@@ -573,22 +647,33 @@  -- ExtractSym2 instance ExtractSym2 Either where-  liftExtractSym2 f _ (Left x) = f x-  liftExtractSym2 _ g (Right y) = g y-  {-# INLINE liftExtractSym2 #-}+  liftExtractSymMaybe2 f _ (Left x) = f x+  liftExtractSymMaybe2 _ g (Right y) = g y+  {-# INLINE liftExtractSymMaybe2 #-}  instance ExtractSym2 (,) where-  liftExtractSym2 f g (x, y) = f x <> g y-  {-# INLINE liftExtractSym2 #-}+  liftExtractSymMaybe2 f g (x, y) = f x <> g y+  {-# INLINE liftExtractSymMaybe2 #-}  instance (ExtractSym a) => ExtractSym2 ((,,) a) where-  liftExtractSym2 f g (x, y, z) = extractSym x <> f y <> g z-  {-# INLINE liftExtractSym2 #-}+  liftExtractSymMaybe2 f g (x, y, z) = extractSymMaybe x <> f y <> g z+  {-# INLINE liftExtractSymMaybe2 #-}  instance   (ExtractSym a, ExtractSym b) =>   ExtractSym2 ((,,,) a b)   where-  liftExtractSym2 f g (x, y, z, w) =-    extractSym x <> extractSym y <> f z <> g w-  {-# INLINE liftExtractSym2 #-}+  liftExtractSymMaybe2 f g (x, y, z, w) =+    extractSymMaybe x <> extractSymMaybe y <> f z <> g w+  {-# INLINE liftExtractSymMaybe2 #-}++instance (ExtractSym a, ExtractSym b) => ExtractSym (a =-> b) where+  extractSymMaybe (TabularFun s t) =+    extractSymMaybe s <> extractSymMaybe t++instance (ExtractSym (SymType b)) => ExtractSym (a --> b) where+  extractSymMaybe :: forall knd. (IsSymbolKind knd) => (a --> b) -> Maybe (SymbolSet knd)+  extractSymMaybe (GeneralFun t f) =+    case decideSymbolKind @knd of+      Left HRefl -> Nothing+      Right HRefl -> SymbolSet <$> extractTerm (HS.singleton $ someTypedSymbol t) f

@@ -21,13 +21,6 @@ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.SymPrim--- >>> :set -XDataKinds--- >>> :set -XBinaryLiterals--- >>> :set -XFlexibleContexts--- >>> :set -XFlexibleInstances--- >>> :set -XFunctionalDependencies--- >>> :set -XOverloadedStrings--- >>> :set -XTypeOperators  -- | Abstraction for function-like types. class Function f arg ret | f -> arg ret where

@@ -140,6 +140,7 @@   ( LinkedRep,     SupportedPrim,   )+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal) import Grisette.Internal.SymPrim.SymBV   ( SymIntN,     SymWordN,@@ -154,8 +155,6 @@ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.SymPrim--- >>> :set -XOverloadedStrings--- >>> :set -XTypeApplications  -- | Index type used for 'GenSym'. --@@ -175,7 +174,7 @@ -- | Monad class for fresh symbolic value generation. -- -- The monad should be a reader monad for the 'Identifier' and a state monad for--- the 'FreshIndex'.+-- the t'FreshIndex'. class (Monad m) => MonadFresh m where   -- | Get the current index for fresh variable generation.   getFreshIndex :: m FreshIndex@@ -389,7 +388,7 @@   localIdentifier f (RWSStrict.RWST m) =     RWSStrict.RWST $ \r s -> localIdentifier f (m r s) --- | 'FreshT' specialized with Identity.+-- | t'FreshT' specialized with Identity. type Fresh = FreshT Identity  -- | Run the symbolic generation with the given identifier and 0 as the initial@@ -413,7 +412,7 @@ -- This ensures that we can generate those types with complex merging rules. -- -- The uniqueness of symbolic constants is managed with the a monadic context.--- 'Fresh' and 'FreshT' can be useful.+-- 'Fresh' and t'FreshT' can be useful. class (Mergeable a) => GenSym spec a where   -- | Generate a symbolic value given some specification. Within a single   -- `MonadFresh` context, calls to `fresh` would generate unique symbolic@@ -474,7 +473,7 @@ -- The result will __/not/__ be wrapped in a union-like monad. -- -- The uniqueness of symbolic constants is managed with the a monadic context.--- 'Fresh' and 'FreshT' can be useful.+-- 'Fresh' and t'FreshT' can be useful. class GenSymSimple spec a where   -- | Generate a symbolic value given some specification. The uniqueness is ensured.   --@@ -1699,6 +1698,10 @@ GENSYM_SIMPLE_SIMPLE(SymFPRoundingMode) GENSYM_UNIT_SIMPLE(SymFPRoundingMode) GENSYM_UNIT_SIMPLE_SIMPLE(SymFPRoundingMode)+GENSYM_SIMPLE(SymAlgReal)+GENSYM_SIMPLE_SIMPLE(SymAlgReal)+GENSYM_UNIT_SIMPLE(SymAlgReal)+GENSYM_UNIT_SIMPLE_SIMPLE(SymAlgReal)  GENSYM_BV(SymIntN) GENSYM_SIMPLE_BV(SymIntN)

@@ -1,7 +1,7 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-}  -- |@@ -25,48 +25,15 @@     fpIsNormal,     fpIsSubnormal,     fpIsPoint,-    SymIEEEFPTraits (..),-    IEEEConstants (..),+    IEEEFPConstants (..),     IEEEFPRoundingMode (..),     IEEEFPOp (..),     IEEEFPRoundingOp (..),+    IEEEFPConvertible (..),+    IEEEFPToAlgReal (..),   ) where -import Data.SBV (infinity, nan)-import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))-import Grisette.Internal.SymPrim.FP (FP (FP), FPRoundingMode (RNA, RNE, RTN, RTP, RTZ), ValidFP)-import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP-  ( pevalFPBinaryTerm,-    pevalFPFMATerm,-    pevalFPRoundingBinaryTerm,-    pevalFPRoundingUnaryTerm,-    pevalFPTraitTerm,-    pevalFPUnaryTerm,-  )-import Grisette.Internal.SymPrim.Prim.Internal.Term-  ( FPBinaryOp (FPMax, FPMin, FPRem),-    FPRoundingBinaryOp (FPAdd, FPDiv, FPMul, FPSub),-    FPRoundingUnaryOp (FPRoundToIntegral, FPSqrt),-    FPTrait-      ( FPIsInfinite,-        FPIsNaN,-        FPIsNegative,-        FPIsNegativeInfinite,-        FPIsNegativeZero,-        FPIsNormal,-        FPIsPoint,-        FPIsPositive,-        FPIsPositiveInfinite,-        FPIsPositiveZero,-        FPIsSubnormal,-        FPIsZero-      ),-    FPUnaryOp (FPAbs, FPNeg),-  )-import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))-import Grisette.Internal.SymPrim.SymFP (SymFP (SymFP), SymFPRoundingMode (SymFPRoundingMode))- -- | Check if a floating-point number is not-a-number. fpIsNaN :: (RealFloat a) => a -> Bool fpIsNaN = isNaN@@ -101,7 +68,7 @@ -- | Check if a floating-point number is negative. -- -0, -inf are considered negative. nan, +0, +inf are not negative. fpIsNegative :: (RealFloat a) => a -> Bool-fpIsNegative = isNegativeZero+fpIsNegative x = not (fpIsNaN x) && (x < 0 || isNegativeZero x) {-# INLINE fpIsNegative #-}  -- | Check if a floating-point number is infinite.@@ -135,127 +102,8 @@ fpIsPoint x = not (fpIsInfinite x) && not (fpIsNaN x) {-# INLINE fpIsPoint #-} --- | A class for symbolic traits of IEEE floating-point numbers.-class SymIEEEFPTraits a where-  -- | Check if a symbolic floating-point number is not-a-number.-  symFpIsNaN :: a -> SymBool--  -- | Check if a symbolic floating-point number is positive.-  -- +0, +inf are considered positive. nan, -0, -inf are not positive.-  symFpIsPositive :: a -> SymBool--  -- | Check if a symbolic floating-point number is negative.-  -- -0, -inf are considered negative. nan, +0, +inf are not negative.-  symFpIsNegative :: a -> SymBool--  -- | Check if a symbolic floating-point number is positive infinite.-  symFpIsPositiveInfinite :: a -> SymBool--  -- | Check if a symbolic floating-point number is negative infinite.-  symFpIsNegativeInfinite :: a -> SymBool--  -- | Check if a symbolic floating-point number is infinite.-  symFpIsInfinite :: a -> SymBool--  -- | Check if a symbolic floating-point number is positive zero.-  symFpIsPositiveZero :: a -> SymBool--  -- | Check if a symbolic floating-point number is negative zero.-  symFpIsNegativeZero :: a -> SymBool--  -- | Check if a symbolic floating-point number is zero.-  symFpIsZero :: a -> SymBool--  -- | Check if a symbolic floating-point number is normal, i.e., not 0, not-  -- inf, not nan, and not denormalized.-  symFpIsNormal :: a -> SymBool--  -- | Check if a symbolic floating-point number is subnormal, i.e.,-  -- denormalized. 0, inf, or nan are not subnormal.-  symFpIsSubnormal :: a -> SymBool--  -- | Check if a symbolic floating-point number is a point, i.e., not inf, not-  -- nan.-  symFpIsPoint :: a -> SymBool--newtype ConcreteFloat f = ConcreteFloat f--instance (RealFloat f) => SymIEEEFPTraits (ConcreteFloat f) where-  symFpIsNaN (ConcreteFloat x) = con $ fpIsNaN x-  {-# INLINE symFpIsNaN #-}--  symFpIsPositive (ConcreteFloat x) = con $ fpIsPositive x-  {-# INLINE symFpIsPositive #-}--  symFpIsNegative (ConcreteFloat x) = con $ fpIsNegative x-  {-# INLINE symFpIsNegative #-}--  symFpIsInfinite (ConcreteFloat x) = con $ fpIsInfinite x-  {-# INLINE symFpIsInfinite #-}--  symFpIsPositiveInfinite (ConcreteFloat x) = con $ fpIsPositiveInfinite x-  {-# INLINE symFpIsPositiveInfinite #-}--  symFpIsNegativeInfinite (ConcreteFloat x) = con $ fpIsNegativeInfinite x-  {-# INLINE symFpIsNegativeInfinite #-}--  symFpIsPositiveZero (ConcreteFloat x) = con $ fpIsPositiveZero x-  {-# INLINE symFpIsPositiveZero #-}--  symFpIsNegativeZero (ConcreteFloat x) = con $ fpIsNegativeZero x-  {-# INLINE symFpIsNegativeZero #-}--  symFpIsZero (ConcreteFloat x) = con $ fpIsZero x-  {-# INLINE symFpIsZero #-}--  symFpIsNormal (ConcreteFloat x) = con $ fpIsNormal x-  {-# INLINE symFpIsNormal #-}--  symFpIsSubnormal (ConcreteFloat x) = con $ fpIsSubnormal x-  {-# INLINE symFpIsSubnormal #-}--  symFpIsPoint (ConcreteFloat x) = con $ fpIsPoint x-  {-# INLINE symFpIsPoint #-}--deriving via (ConcreteFloat Float) instance SymIEEEFPTraits Float--deriving via (ConcreteFloat Double) instance SymIEEEFPTraits Double--deriving via-  (ConcreteFloat (FP eb sb))-  instance-    (ValidFP eb sb) => SymIEEEFPTraits (FP eb sb)--instance (ValidFP eb sb) => SymIEEEFPTraits (SymFP eb sb) where-  symFpIsNaN (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNaN x-  {-# INLINE symFpIsNaN #-}-  symFpIsPositive (SymFP x) = SymBool $ pevalFPTraitTerm FPIsPositive x-  {-# INLINE symFpIsPositive #-}-  symFpIsNegative (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNegative x-  {-# INLINE symFpIsNegative #-}-  symFpIsInfinite (SymFP x) = SymBool $ pevalFPTraitTerm FPIsInfinite x-  {-# INLINE symFpIsInfinite #-}-  symFpIsPositiveInfinite (SymFP x) =-    SymBool $ pevalFPTraitTerm FPIsPositiveInfinite x-  {-# INLINE symFpIsPositiveInfinite #-}-  symFpIsNegativeInfinite (SymFP x) =-    SymBool $ pevalFPTraitTerm FPIsNegativeInfinite x-  {-# INLINE symFpIsNegativeInfinite #-}-  symFpIsPositiveZero (SymFP x) = SymBool $ pevalFPTraitTerm FPIsPositiveZero x-  {-# INLINE symFpIsPositiveZero #-}-  symFpIsNegativeZero (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNegativeZero x-  {-# INLINE symFpIsNegativeZero #-}-  symFpIsZero (SymFP x) = SymBool $ pevalFPTraitTerm FPIsZero x-  {-# INLINE symFpIsZero #-}-  symFpIsNormal (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNormal x-  {-# INLINE symFpIsNormal #-}-  symFpIsSubnormal (SymFP x) = SymBool $ pevalFPTraitTerm FPIsSubnormal x-  {-# INLINE symFpIsSubnormal #-}-  symFpIsPoint (SymFP x) = SymBool $ pevalFPTraitTerm FPIsPoint x-  {-# INLINE symFpIsPoint #-}- -- | Constants for IEEE floating-point numbers.-class IEEEConstants a where+class IEEEFPConstants a where   -- | Positive infinity.   fpPositiveInfinite :: a @@ -271,50 +119,53 @@   -- | Positive zero.   fpPositiveZero :: a -instance (ValidFP eb sb) => IEEEConstants (FP eb sb) where-  fpPositiveInfinite = FP infinity-  {-# INLINE fpPositiveInfinite #-}-  fpNegativeInfinite = FP $ -infinity-  {-# INLINE fpNegativeInfinite #-}-  fpNaN = FP nan-  {-# INLINE fpNaN #-}-  fpNegativeZero = FP $ -0-  {-# INLINE fpNegativeZero #-}-  fpPositiveZero = FP 0-  {-# INLINE fpPositiveZero #-}+  -- | Smallest positive normalized number.+  fpMinNormalized :: a -instance (ValidFP eb sb) => IEEEConstants (SymFP eb sb) where-  fpPositiveInfinite = con fpPositiveInfinite-  {-# INLINE fpPositiveInfinite #-}-  fpNegativeInfinite = con fpNegativeInfinite-  {-# INLINE fpNegativeInfinite #-}-  fpNaN = con fpNaN-  {-# INLINE fpNaN #-}-  fpNegativeZero = con fpNegativeZero-  {-# INLINE fpNegativeZero #-}-  fpPositiveZero = con fpPositiveZero-  {-# INLINE fpPositiveZero #-}+  -- | Smallest positive subnormal number.+  fpMinSubnormal :: a +  -- | Largest positive normalized number.+  fpMaxNormalized :: a++  -- | Largest positive subnormal number.+  fpMaxSubnormal :: a+ -- | Operations on IEEE floating-point numbers, without rounding mode. class IEEEFPOp a where-  symFpAbs :: a -> a-  symFpNeg :: a -> a-  symFpRem :: a -> a -> a-  symFpMin :: a -> a -> a-  symFpMax :: a -> a -> a+  -- | IEEE754-2019 abs operation.+  fpAbs :: a -> a -instance (ValidFP eb sb) => IEEEFPOp (SymFP eb sb) where-  symFpAbs (SymFP l) = SymFP $ pevalFPUnaryTerm FPAbs l-  {-# INLINE symFpAbs #-}-  symFpNeg (SymFP l) = SymFP $ pevalFPUnaryTerm FPNeg l-  {-# INLINE symFpNeg #-}-  symFpRem (SymFP l) (SymFP r) = SymFP $ pevalFPBinaryTerm FPRem l r-  {-# INLINE symFpRem #-}-  symFpMin (SymFP l) (SymFP r) = SymFP $ pevalFPBinaryTerm FPMin l r-  {-# INLINE symFpMin #-}-  symFpMax (SymFP l) (SymFP r) = SymFP $ pevalFPBinaryTerm FPMax l r-  {-# INLINE symFpMax #-}+  -- | IEEE754-2019 negate operation.+  fpNeg :: a -> a +  -- | IEEE754-2019 remainder operation.+  fpRem :: a -> a -> a++  -- | IEEE754-2019 minimum operation.+  --+  -- * The comparison for zeros follows -0 < 0+  -- * Returns NaN if one operand is NaN.+  fpMinimum :: a -> a -> a++  -- | IEEE754-2019 minimumNumber operation.+  --+  -- * The comparison for zeros follows -0 < 0+  -- * Returns the other operand if one operand is NaN.+  fpMinimumNumber :: a -> a -> a++  -- | IEEE754-2019 maximum operation.+  --+  -- * The comparison for zeros follows -0 < 0+  -- * Returns NaN if one operand is NaN.+  fpMaximum :: a -> a -> a++  -- | IEEE754-2019 maximumNumber operation.+  --+  -- * The comparison for zeros follows -0 < 0+  -- * Returns the other operand if one operand is NaN.+  fpMaximumNumber :: a -> a -> a+ -- | Rounding modes for floating-point operations. class IEEEFPRoundingMode mode where   -- | Round to nearest, ties to even.@@ -332,59 +183,44 @@   -- | Round towards zero.   rtz :: mode -instance IEEEFPRoundingMode FPRoundingMode where-  rne = RNE-  {-# INLINE rne #-}-  rna = RNA-  {-# INLINE rna #-}-  rtp = RTP-  {-# INLINE rtp #-}-  rtn = RTN-  {-# INLINE rtn #-}-  rtz = RTZ-  {-# INLINE rtz #-}--instance IEEEFPRoundingMode SymFPRoundingMode where-  rne = con RNE-  {-# INLINE rne #-}-  rna = con RNA-  {-# INLINE rna #-}-  rtp = con RTP-  {-# INLINE rtp #-}-  rtn = con RTN-  {-# INLINE rtn #-}-  rtz = con RTZ-  {-# INLINE rtz #-}- -- | Operations on IEEE floating-point numbers, with rounding mode. class (IEEEFPRoundingMode mode) => IEEEFPRoundingOp a mode | a -> mode where-  symFpAdd :: mode -> a -> a -> a-  symFpSub :: mode -> a -> a -> a-  symFpMul :: mode -> a -> a -> a-  symFpDiv :: mode -> a -> a -> a-  symFpFMA :: mode -> a -> a -> a -> a-  symFpSqrt :: mode -> a -> a-  symFpRoundToIntegral :: mode -> a -> a+  fpAdd :: mode -> a -> a -> a+  fpSub :: mode -> a -> a -> a+  fpMul :: mode -> a -> a -> a+  fpDiv :: mode -> a -> a -> a+  fpFMA :: mode -> a -> a -> a -> a+  fpSqrt :: mode -> a -> a+  fpRoundToIntegral :: mode -> a -> a -instance (ValidFP eb sb) => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode where-  symFpAdd (SymFPRoundingMode mode) (SymFP l) (SymFP r) =-    SymFP $ pevalFPRoundingBinaryTerm FPAdd mode l r-  {-# INLINE symFpAdd #-}-  symFpSub (SymFPRoundingMode mode) (SymFP l) (SymFP r) =-    SymFP $ pevalFPRoundingBinaryTerm FPSub mode l r-  {-# INLINE symFpSub #-}-  symFpMul (SymFPRoundingMode mode) (SymFP l) (SymFP r) =-    SymFP $ pevalFPRoundingBinaryTerm FPMul mode l r-  {-# INLINE symFpMul #-}-  symFpDiv (SymFPRoundingMode mode) (SymFP l) (SymFP r) =-    SymFP $ pevalFPRoundingBinaryTerm FPDiv mode l r-  {-# INLINE symFpDiv #-}-  symFpFMA (SymFPRoundingMode mode) (SymFP l) (SymFP m) (SymFP r) =-    SymFP $ pevalFPFMATerm mode l m r-  {-# INLINE symFpFMA #-}-  symFpSqrt (SymFPRoundingMode mode) (SymFP v) =-    SymFP $ pevalFPRoundingUnaryTerm FPSqrt mode v-  {-# INLINE symFpSqrt #-}-  symFpRoundToIntegral (SymFPRoundingMode mode) (SymFP v) =-    SymFP $ pevalFPRoundingUnaryTerm FPRoundToIntegral mode v-  {-# INLINE symFpRoundToIntegral #-}+-- | Conversion from and to FPs.+class IEEEFPConvertible a fp mode | fp -> mode where+  fromFPOr ::+    -- | Default value when converting non-representable FPs. For example, when+    -- converting to non-FP types, the NaN and infinities are not representable.+    -- Additionally, when converting to bit-vectors, out-of-bound FPs are not+    -- representable.+    --+    -- Note that out-of-bound means that the /value after conversion/ is out of+    -- bound, not the /value before conversion/, meaning that converting from+    -- 3.5 to 2-bit unsigned bit-vector is out-of-bound when rounding to+    -- positive, but not when rounding to negative.+    a ->+    -- | Rounding mode. Ignored when converting to 'Grisette.AlgReal' because+    -- every representable FP value is converted to an exact 'Grisette.AlgReal'.+    mode ->+    -- | FP value.+    fp ->+    a+  toFP :: mode -> a -> fp++-- | Converting FP to real numbers.+class+  (IEEEFPConvertible a fp mode, IEEEFPRoundingMode mode) =>+  IEEEFPToAlgReal a fp mode+    | fp -> mode+  where+  -- | Similar to 'fromFPOr' for 'Grisette.AlgReal', but dropped the ignored+  -- rounding mode.+  fpToAlgReal :: a -> fp -> a+  fpToAlgReal d = fromFPOr d rna

@@ -18,6 +18,7 @@   ) where +import Control.Monad.Identity (Identity (Identity)) import GHC.TypeNats (KnownNat, type (<=)) import Grisette.Internal.SymPrim.FP (ValidFP) import Grisette.Internal.SymPrim.GeneralFun (type (-->))@@ -25,6 +26,7 @@   ( LinkedRep,     SupportedPrim (pevalITETerm),   )+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal)) import Grisette.Internal.SymPrim.SymBV   ( SymIntN (SymIntN),     SymWordN (SymWordN),@@ -42,11 +44,6 @@ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.SymPrim--- >>> :set -XDataKinds--- >>> :set -XBinaryLiterals--- >>> :set -XFlexibleContexts--- >>> :set -XFlexibleInstances--- >>> :set -XFunctionalDependencies  -- | ITE operator for solvable (see "Grisette.Core#g:solvable")s, including -- symbolic boolean, integer, etc.@@ -80,6 +77,7 @@ ITEOP_SIMPLE(SymBool) ITEOP_SIMPLE(SymInteger) ITEOP_SIMPLE(SymFPRoundingMode)+ITEOP_SIMPLE(SymAlgReal) ITEOP_BV(SymIntN) ITEOP_BV(SymWordN) ITEOP_FUN((=->), (=~>), SymTabularFun)@@ -88,4 +86,8 @@  instance (ValidFP eb sb) => ITEOp (SymFP eb sb) where   symIte (SymBool c) (SymFP t) (SymFP f) = SymFP $ pevalITETerm c t f+  {-# INLINE symIte #-}++instance (ITEOp v) => ITEOp (Identity v) where+  symIte c (Identity t) (Identity f) = Identity $ symIte c t f   {-# INLINE symIte #-}

@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ -- | -- Module      :   Grisette.Internal.Core.Data.Class.LogicalOp -- Copyright   :   (c) Sirui Lu 2021-2024@@ -11,6 +13,11 @@   ) where +#if !MIN_VERSION_base(4,18,0)+import Control.Applicative (liftA2)+#endif++import Control.Monad.Identity (Identity) import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con)) import Grisette.Internal.SymPrim.Prim.Term   ( pevalAndTerm,@@ -24,11 +31,6 @@ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.SymPrim--- >>> :set -XDataKinds--- >>> :set -XBinaryLiterals--- >>> :set -XFlexibleContexts--- >>> :set -XFlexibleInstances--- >>> :set -XFunctionalDependencies  -- | Symbolic logical operators for symbolic booleans. --@@ -125,3 +127,12 @@   symNot (SymBool v) = SymBool $ pevalNotTerm v   (SymBool l) `symXor` (SymBool r) = SymBool $ pevalXorTerm l r   (SymBool l) `symImplies` (SymBool r) = SymBool $ pevalImplyTerm l r++instance (LogicalOp a) => LogicalOp (Identity a) where+  true = pure true+  false = pure false+  (.||) = liftA2 (.||)+  (.&&) = liftA2 (.&&)+  symNot = fmap symNot+  symXor = liftA2 symXor+  symImplies = liftA2 symImplies

@@ -1,3 +1,4 @@+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-}@@ -52,6 +53,7 @@     buildStrategyList,     resolveStrategy,     resolveStrategy',+    resolveMergeable1,   ) where @@ -124,16 +126,17 @@   ( AssertionError,     VerificationConditions,   )-import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))+import Grisette.Internal.Core.Data.Class.BitCast (bitCastOrCanonical) import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))+import Grisette.Internal.SymPrim.AlgReal (AlgReal, AlgRealPoly, RealPoint) import Grisette.Internal.SymPrim.BV-  ( BitwidthMismatch,-    IntN,+  ( IntN,     WordN,   ) import Grisette.Internal.SymPrim.FP   ( FP,     FPRoundingMode,+    NotRepresentableFPError,     ValidFP,     withValidFPProofs,   )@@ -142,6 +145,7 @@   ( LinkedRep,     SupportedPrim,   )+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal) import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN) import Grisette.Internal.SymPrim.SymBool (SymBool) import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)@@ -285,6 +289,15 @@ rootStrategy1 = liftRootStrategy rootStrategy {-# INLINE rootStrategy1 #-} +-- | Workaround as GHC prior to 9.6 doesn't support quantified constraints+-- reliably.+--+-- Similar to https://github.com/haskell/core-libraries-committee/issues/10,+-- which is only available with 9.6 or higher.+resolveMergeable1 ::+  forall f a r. (Mergeable1 f, Mergeable a) => ((Mergeable (f a)) => r) -> r+resolveMergeable1 v = v+ -- | Lifting of the 'Mergeable' class to binary type constructors. class   (forall a. (Mergeable a) => Mergeable1 (u a)) =>@@ -572,6 +585,7 @@ CONCRETE_ORD_MERGEABLE(Word64) CONCRETE_ORD_MERGEABLE(Float) CONCRETE_ORD_MERGEABLE(Double)+CONCRETE_ORD_MERGEABLE(Rational) CONCRETE_ORD_MERGEABLE(B.ByteString) CONCRETE_ORD_MERGEABLE(T.Text) CONCRETE_ORD_MERGEABLE(FPRoundingMode)@@ -587,7 +601,7 @@     let sub = SimpleStrategy $ \_ t _ -> t      in withValidFPProofs @eb @sb           $ SortedStrategy-            (\fp -> (bitCast fp :: WordN (eb + sb)))+            (\fp -> (bitCastOrCanonical fp :: WordN (eb + sb)))           $ const sub  #define MERGEABLE_SIMPLE(symtype) \@@ -607,6 +621,7 @@ MERGEABLE_SIMPLE(SymBool) MERGEABLE_SIMPLE(SymInteger) MERGEABLE_SIMPLE(SymFPRoundingMode)+MERGEABLE_SIMPLE(SymAlgReal) MERGEABLE_BV(SymIntN) MERGEABLE_BV(SymWordN) MERGEABLE_FUN((=->), (=~>))@@ -635,71 +650,6 @@     _ -> NoStrategy   {-# INLINE liftRootStrategy2 #-} --- Instances-deriveBuiltins-  (ViaDefault ''Mergeable)-  [''Mergeable]-  [ ''Maybe,-    ''Either,-    ''(),-    -- The following three are implemented by hand because they need to be-    -- consistent with Mergeable2 instances.-    -- ''(,),-    -- ''(,,),-    -- ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''AssertionError,-    ''VerificationConditions,-    ''BitwidthMismatch,-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]--deriveBuiltins-  (ViaDefault1 ''Mergeable1)-  [''Mergeable, ''Mergeable1]-  [ ''Maybe,-    ''Either,-    -- The following three are implemented by hand because they need to be-    -- consistent with Mergeable2 instances.-    -- ''(,),-    -- ''(,,),-    -- ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]- -- List  -- | Helper type for building efficient merge strategy for list-like containers.@@ -780,6 +730,137 @@               else NoStrategy   {-# INLINE liftRootStrategy #-} +-- (,)+instance (Mergeable a, Mergeable b) => Mergeable (a, b) where+  rootStrategy = rootStrategy1+  {-# INLINE rootStrategy #-}++instance (Mergeable a) => Mergeable1 ((,) a) where+  liftRootStrategy = liftRootStrategy2 rootStrategy+  {-# INLINE liftRootStrategy #-}++instance Mergeable2 (,) where+  liftRootStrategy2 = product2Strategy (,) id+  {-# INLINE liftRootStrategy2 #-}++-- (,,)+instance (Mergeable a, Mergeable b, Mergeable c) => Mergeable ((,,) a b c) where+  rootStrategy = rootStrategy1+  {-# INLINE rootStrategy #-}++instance (Mergeable a, Mergeable b) => Mergeable1 ((,,) a b) where+  liftRootStrategy = liftRootStrategy2 rootStrategy+  {-# INLINE liftRootStrategy #-}++instance (Mergeable a) => Mergeable2 ((,,) a) where+  liftRootStrategy2 = liftRootStrategy3 rootStrategy+  {-# INLINE liftRootStrategy2 #-}++instance Mergeable3 (,,) where+  liftRootStrategy3 m1 m2 m3 =+    product2Strategy+      (\a (b, c) -> (a, b, c))+      (\(a, b, c) -> (a, (b, c)))+      m1+      (liftRootStrategy2 m2 m3)+  {-# INLINE liftRootStrategy3 #-}++-- (,,,)+instance+  (Mergeable a, Mergeable b, Mergeable c, Mergeable d) =>+  Mergeable ((,,,) a b c d)+  where+  rootStrategy = rootStrategy1+  {-# INLINE rootStrategy #-}++instance+  (Mergeable a, Mergeable b, Mergeable c) =>+  Mergeable1 ((,,,) a b c)+  where+  liftRootStrategy = liftRootStrategy2 rootStrategy+  {-# INLINE liftRootStrategy #-}++instance (Mergeable a, Mergeable b) => Mergeable2 ((,,,) a b) where+  liftRootStrategy2 = liftRootStrategy3 rootStrategy+  {-# INLINE liftRootStrategy2 #-}++instance (Mergeable a) => Mergeable3 ((,,,) a) where+  liftRootStrategy3 m1 m2 m3 =+    product2Strategy+      (\(a, b) (c, d) -> (a, b, c, d))+      (\(a, b, c, d) -> ((a, b), (c, d)))+      (liftRootStrategy m1)+      (liftRootStrategy2 m2 m3)+  {-# INLINE liftRootStrategy3 #-}++-- Instances+deriveBuiltins+  (ViaDefault ''Mergeable)+  [''Mergeable]+  [ ''Maybe,+    ''Either,+    ''AlgRealPoly,+    ''RealPoint,+    ''AlgReal,+    ''(),+    -- The following three are implemented by hand because they need to be+    -- consistent with Mergeable2 instances.+    -- ''(,),+    -- ''(,,),+    -- ''(,,,),+    ''(,,,,),+    ''(,,,,,),+    ''(,,,,,,),+    ''(,,,,,,,),+    ''(,,,,,,,,),+    ''(,,,,,,,,,),+    ''(,,,,,,,,,,),+    ''(,,,,,,,,,,,),+    ''(,,,,,,,,,,,,),+    ''(,,,,,,,,,,,,,),+    ''(,,,,,,,,,,,,,,),+    ''AssertionError,+    ''VerificationConditions,+    ''NotRepresentableFPError,+    ''Identity,+    ''Monoid.Dual,+    ''Monoid.Sum,+    ''Monoid.Product,+    ''Monoid.First,+    ''Monoid.Last,+    ''Down+  ]++deriveBuiltins+  (ViaDefault1 ''Mergeable1)+  [''Mergeable, ''Mergeable1]+  [ ''Maybe,+    ''Either,+    -- The following three are implemented by hand because they need to be+    -- consistent with Mergeable2 instances.+    -- ''(,),+    -- ''(,,),+    -- ''(,,,),+    ''(,,,,),+    ''(,,,,,),+    ''(,,,,,,),+    ''(,,,,,,,),+    ''(,,,,,,,,),+    ''(,,,,,,,,,),+    ''(,,,,,,,,,,),+    ''(,,,,,,,,,,,),+    ''(,,,,,,,,,,,,),+    ''(,,,,,,,,,,,,,),+    ''(,,,,,,,,,,,,,,),+    ''Identity,+    ''Monoid.Dual,+    ''Monoid.Sum,+    ''Monoid.Product,+    ''Monoid.First,+    ''Monoid.Last,+    ''Down+  ]+ -- MaybeT instance (Mergeable1 m, Mergeable a) => Mergeable (MaybeT m a) where   rootStrategy = rootStrategy1@@ -1098,66 +1179,3 @@           True -> wrapStrategy m2 Right (\case (Right v) -> v; _ -> undefined)       )   {-# INLINE liftRootStrategy2 #-}---- (,)-instance (Mergeable a, Mergeable b) => Mergeable (a, b) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable a) => Mergeable1 ((,) a) where-  liftRootStrategy = liftRootStrategy2 rootStrategy-  {-# INLINE liftRootStrategy #-}--instance Mergeable2 (,) where-  liftRootStrategy2 = product2Strategy (,) id-  {-# INLINE liftRootStrategy2 #-}---- (,,)-instance (Mergeable a, Mergeable b, Mergeable c) => Mergeable ((,,) a b c) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable a, Mergeable b) => Mergeable1 ((,,) a b) where-  liftRootStrategy = liftRootStrategy2 rootStrategy-  {-# INLINE liftRootStrategy #-}--instance (Mergeable a) => Mergeable2 ((,,) a) where-  liftRootStrategy2 = liftRootStrategy3 rootStrategy-  {-# INLINE liftRootStrategy2 #-}--instance Mergeable3 (,,) where-  liftRootStrategy3 m1 m2 m3 =-    product2Strategy-      (\a (b, c) -> (a, b, c))-      (\(a, b, c) -> (a, (b, c)))-      m1-      (liftRootStrategy2 m2 m3)-  {-# INLINE liftRootStrategy3 #-}---- (,,,)-instance-  (Mergeable a, Mergeable b, Mergeable c, Mergeable d) =>-  Mergeable ((,,,) a b c d)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance-  (Mergeable a, Mergeable b, Mergeable c) =>-  Mergeable1 ((,,,) a b c)-  where-  liftRootStrategy = liftRootStrategy2 rootStrategy-  {-# INLINE liftRootStrategy #-}--instance (Mergeable a, Mergeable b) => Mergeable2 ((,,,) a b) where-  liftRootStrategy2 = liftRootStrategy3 rootStrategy-  {-# INLINE liftRootStrategy2 #-}--instance (Mergeable a) => Mergeable3 ((,,,) a) where-  liftRootStrategy3 m1 m2 m3 =-    product2Strategy-      (\(a, b) (c, d) -> (a, b, c, d))-      (\(a, b, c, d) -> ((a, b), (c, d)))-      (liftRootStrategy m1)-      (liftRootStrategy2 m2 m3)-  {-# INLINE liftRootStrategy3 #-}

@@ -31,22 +31,22 @@ -- -- Note that symbolic constants with different types are considered different. ----- >>> let aBool = "a" :: TypedSymbol Bool--- >>> let bBool = "b" :: TypedSymbol Bool--- >>> let cBool = "c" :: TypedSymbol Bool--- >>> let aInteger = "a" :: TypedSymbol Integer--- >>> emptySet :: SymbolSet+-- >>> let aBool = "a" :: TypedAnySymbol Bool+-- >>> let bBool = "b" :: TypedAnySymbol Bool+-- >>> let cBool = "c" :: TypedAnySymbol Bool+-- >>> let aInteger = "a" :: TypedAnySymbol Integer+-- >>> emptySet :: AnySymbolSet -- SymbolSet {}--- >>> containsSymbol aBool (buildSymbolSet aBool :: SymbolSet)+-- >>> containsSymbol aBool (buildSymbolSet aBool :: AnySymbolSet) -- True--- >>> containsSymbol bBool (buildSymbolSet aBool :: SymbolSet)+-- >>> containsSymbol bBool (buildSymbolSet aBool :: AnySymbolSet) -- False--- >>> insertSymbol aBool (buildSymbolSet aBool :: SymbolSet)+-- >>> insertSymbol aBool (buildSymbolSet aBool :: AnySymbolSet) -- SymbolSet {a :: Bool}--- >>> insertSymbol aInteger (buildSymbolSet aBool :: SymbolSet)+-- >>> insertSymbol aInteger (buildSymbolSet aBool :: AnySymbolSet) -- SymbolSet {a :: Bool, a :: Integer}--- >>> let abSet = buildSymbolSet (aBool, bBool) :: SymbolSet--- >>> let acSet = buildSymbolSet (aBool, cBool) :: SymbolSet+-- >>> let abSet = buildSymbolSet (aBool, bBool) :: AnySymbolSet+-- >>> let acSet = buildSymbolSet (aBool, cBool) :: AnySymbolSet -- >>> intersectionSet abSet acSet -- SymbolSet {a :: Bool} -- >>> unionSet abSet acSet@@ -82,7 +82,7 @@ -- | A type class for building a symbolic constant set manually from a symbolic -- constant set representation ----- >>> buildSymbolSet ("a" :: TypedSymbol Bool, "b" :: TypedSymbol Bool) :: SymbolSet+-- >>> buildSymbolSet ("a" :: TypedAnySymbol Bool, "b" :: TypedAnySymbol Bool) :: AnySymbolSet -- SymbolSet {a :: Bool, b :: Bool} class   (SymbolSetOps symbolSet typedSymbol) =>@@ -95,10 +95,10 @@ -- -- Note that symbolic constants with different types are considered different. ----- >>> let aBool = "a" :: TypedSymbol Bool--- >>> let bBool = "b" :: TypedSymbol Bool--- >>> let cBool = "c" :: TypedSymbol Bool--- >>> let aInteger = "a" :: TypedSymbol Integer+-- >>> let aBool = "a" :: TypedAnySymbol Bool+-- >>> let bBool = "b" :: TypedAnySymbol Bool+-- >>> let cBool = "c" :: TypedAnySymbol Bool+-- >>> let aInteger = "a" :: TypedAnySymbol Integer -- >>> emptyModel :: Model -- Model {} -- >>> valueOf aBool (buildModel (aBool ::= True) :: Model)@@ -108,7 +108,7 @@ -- >>> insertValue bBool False (buildModel (aBool ::= True) :: Model) -- Model {a -> True :: Bool, b -> False :: Bool} -- >>> let abModel = buildModel (aBool ::= True, bBool ::= False) :: Model--- >>> let acSet = buildSymbolSet (aBool, cBool) :: SymbolSet+-- >>> let acSet = buildSymbolSet (aBool, cBool) :: AnySymbolSet -- >>> exceptFor acSet abModel -- Model {b -> False :: Bool} -- >>> restrictTo acSet abModel@@ -163,8 +163,8 @@ class ModelRep rep model | rep -> model where   -- | Build a model   ---  -- >>> let aBool = "a" :: TypedSymbol Bool-  -- >>> let bBool = "b" :: TypedSymbol Bool+  -- >>> let aBool = "a" :: TypedAnySymbol Bool+  -- >>> let bBool = "b" :: TypedAnySymbol Bool   -- >>> buildModel (aBool ::= True, bBool ::= False) :: Model   -- Model {a -> True :: Bool, b -> False :: Bool}   buildModel :: rep -> model

@@ -126,13 +126,24 @@   ( AssertionError,     VerificationConditions,   )+import Grisette.Internal.Core.Data.Symbol (Identifier, Symbol)+import Grisette.Internal.SymPrim.AlgReal (AlgReal) import Grisette.Internal.SymPrim.BV (IntN, WordN)-import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)+import Grisette.Internal.SymPrim.Prim.Internal.Term ()+import Grisette.Internal.SymPrim.Prim.Model+  ( Model (Model),+    SymbolSet (SymbolSet),+  )+import Grisette.Internal.SymPrim.Prim.ModelValue (ModelValue) import Grisette.Internal.SymPrim.Prim.Term   ( LinkedRep,+    SomeTypedSymbol (SomeTypedSymbol),     SupportedPrim,+    TypedSymbol (unTypedSymbol),     prettyPrintTerm,   )+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal)) import Grisette.Internal.SymPrim.SymBV   ( SymIntN (SymIntN),     SymWordN (SymWordN),@@ -174,14 +185,18 @@    {-# MINIMAL pformat | pformatPrec #-} -prettyPrintList :: [Doc ann] -> Doc ann-prettyPrintList l-  | null l = "[]"-  | length l == 1 = align $ group $ vcat ["[" <> flatAlt " " "" <> head l, "]"]+pformatListLike :: Doc ann -> Doc ann -> [Doc ann] -> Doc ann+pformatListLike ldelim rdelim l+  | null l = ldelim <> rdelim+  | length l == 1 =+      align $ group $ vcat [ldelim <> flatAlt " " "" <> head l, rdelim]   | otherwise =-      groupedEnclose "[" "]" . align . vcat $+      groupedEnclose ldelim rdelim . align . vcat $         ((\v -> v <> flatAlt "," ", ") <$> init l) ++ [last l] +prettyPrintList :: [Doc ann] -> Doc ann+prettyPrintList = pformatListLike "[" "]"+ prettyPrintTuple :: [Doc ann] -> Doc ann prettyPrintTuple l   | length l >= 2 =@@ -198,7 +213,7 @@  -- | Convenience function to layout and render a 'Doc' to 'T.Text'. ----- You can control the layout with 'LayoutOptions'.+-- You can control the layout with t'LayoutOptions'. docToTextWith :: LayoutOptions -> Doc ann -> T.Text docToTextWith options = renderStrict . layoutPretty options @@ -218,7 +233,7 @@  -- | Convenience function to format a value to 'T.Text'. ----- You can control the layout with 'LayoutOptions'.+-- You can control the layout with t'LayoutOptions'. pformatTextWith :: (PPrint a) => LayoutOptions -> a -> T.Text pformatTextWith options = docToTextWith options . pformat @@ -275,8 +290,8 @@   -- | Lift two pretty-printers to a binary type constructor.   liftPFormatPrec2 ::     (Int -> a -> Doc ann) ->-    (Int -> b -> Doc ann) ->     ([a] -> Doc ann) ->+    (Int -> b -> Doc ann) ->     ([b] -> Doc ann) ->     Int ->     f a b ->@@ -285,8 +300,8 @@   -- | Lift two pretty-printers to list of values with binary type constructors.   liftPFormatList2 ::     (Int -> a -> Doc ann) ->-    (Int -> b -> Doc ann) ->     ([a] -> Doc ann) ->+    (Int -> b -> Doc ann) ->     ([b] -> Doc ann) ->     [f a b] ->     Doc ann@@ -296,13 +311,13 @@ -- | Lift the standard pretty-printer ('pformatPrec', 'pformatList') to binary -- type constructors. pformatPrec2 :: (PPrint2 f, PPrint a, PPrint b) => Int -> f a b -> Doc ann-pformatPrec2 = liftPFormatPrec2 pformatPrec pformatPrec pformatList pformatList+pformatPrec2 = liftPFormatPrec2 pformatPrec pformatList pformatPrec pformatList {-# INLINE pformatPrec2 #-}  -- | Lift the standard pretty-printer ('pformatPrec', 'pformatList') to list of -- values with binary type constructors. pformatList2 :: (PPrint2 f, PPrint a, PPrint b) => [f a b] -> Doc ann-pformatList2 = liftPFormatList2 pformatPrec pformatPrec pformatList pformatList+pformatList2 = liftPFormatList2 pformatPrec pformatList pformatPrec pformatList {-# INLINE pformatList2 #-}  -- | The arguments to the generic 'PPrint' class.@@ -546,6 +561,7 @@ FORMAT_SIMPLE(Monoid.All) FORMAT_SIMPLE(Monoid.Any) FORMAT_SIMPLE(Ordering)+FORMAT_SIMPLE(AlgReal) #endif  instance PPrint B.ByteString where@@ -581,6 +597,7 @@ FORMAT_SYM_SIMPLE(SymBool) FORMAT_SYM_SIMPLE(SymInteger) FORMAT_SYM_SIMPLE(SymFPRoundingMode)+FORMAT_SYM_SIMPLE(SymAlgReal) FORMAT_SYM_BV(SymIntN) FORMAT_SYM_BV(SymWordN) FORMAT_SYM_FUN(=~>, SymTabularFun)@@ -613,6 +630,7 @@     ''(,,,,,,,,,,,,,,),     ''AssertionError,     ''VerificationConditions,+    ''NotRepresentableFPError,     ''Monoid.Dual,     ''Monoid.Sum,     ''Monoid.Product,@@ -653,8 +671,7 @@   pformatPrec = pformatPrec1  instance PPrint1 Identity where-  liftPFormatPrec f _ n (Identity a) =-    pformatWithConstructor n "Identity" [f 11 a]+  liftPFormatPrec f _ n (Identity a) = f n a  -- MaybeT instance@@ -706,8 +723,8 @@       n       "WriterT"       [ liftPFormatPrec-          (liftPFormatPrec2 f pformatPrec l pformatList)-          (liftPFormatList2 f pformatPrec l pformatList)+          (liftPFormatPrec2 f l pformatPrec pformatList)+          (liftPFormatList2 f l pformatPrec pformatList)           11           a       ]@@ -727,8 +744,8 @@       n       "WriterT"       [ liftPFormatPrec-          (liftPFormatPrec2 f pformatPrec l pformatList)-          (liftPFormatList2 f pformatPrec l pformatList)+          (liftPFormatPrec2 f l pformatPrec pformatList)+          (liftPFormatList2 f l pformatPrec pformatList)           11           a       ]@@ -834,25 +851,74 @@ instance PPrint2 Either where   liftPFormatPrec2 fe _ _ _ n (Left e) =     pformatWithConstructor n "Left" [fe 11 e]-  liftPFormatPrec2 _ fa _ _ n (Right a) =+  liftPFormatPrec2 _ _ fa _ n (Right a) =     pformatWithConstructor n "Right" [fa 11 a]  instance PPrint2 (,) where-  liftPFormatPrec2 fa fb _ _ _ (a, b) =+  liftPFormatPrec2 fa _ fb _ _ (a, b) =     prettyPrintTuple [fa 0 a, fb 0 b]  instance (PPrint a) => PPrint2 ((,,) a) where-  liftPFormatPrec2 fb fc _ _ _ (a, b, c) =+  liftPFormatPrec2 fb _ fc _ _ (a, b, c) =     prettyPrintTuple [pformat a, fb 0 b, fc 0 c]  instance (PPrint a, PPrint b) => PPrint2 ((,,,) a b) where-  liftPFormatPrec2 fc fd _ _ _ (a, b, c, d) =+  liftPFormatPrec2 fc _ fd _ _ (a, b, c, d) =     prettyPrintTuple [pformat a, pformat b, fc 0 c, fd 0 d]  instance (PPrint a) => PPrint (HS.HashSet a) where-  pformatPrec n s =-    pformatWithConstructor n "fromList" [pformatPrec 11 $ HS.toList s]+  pformatPrec = pformatPrec1 +instance PPrint1 HS.HashSet where+  liftPFormatPrec p l n s =+    pformatWithConstructor n "HashSet" [liftPFormatPrec p l 11 $ HS.toList s]+ instance (PPrint k, PPrint v) => PPrint (HM.HashMap k v) where-  pformatPrec n s =-    pformatWithConstructor n "fromList" [pformatPrec 11 $ HM.toList s]+  pformatPrec = pformatPrec1++instance (PPrint k) => PPrint1 (HM.HashMap k) where+  liftPFormatPrec = liftPFormatPrec2 pformatPrec pformatList++instance PPrint2 HM.HashMap where+  liftPFormatPrec2 pk lk pv lv n s =+    pformatWithConstructor+      n+      "HashMap"+      [ liftPFormatPrec+          (liftPFormatPrec2 pk lk pv lv)+          (liftPFormatList2 pk lk pv lv)+          11+          $ HM.toList s+      ]++instance PPrint Identifier where+  pformat = viaShow++instance PPrint Symbol where+  pformat = viaShow++instance PPrint (TypedSymbol knd t) where+  pformat = viaShow++instance PPrint (SomeTypedSymbol knd) where+  pformat = viaShow++instance PPrint ModelValue where+  pformat = viaShow++instance PPrint Model where+  pformatPrec n (Model m) =+    pformatWithConstructor n "Model" [bodyFormatted]+    where+      pformatSymbolWithoutType :: SomeTypedSymbol knd -> Doc ann+      pformatSymbolWithoutType (SomeTypedSymbol _ s) = pformat $ unTypedSymbol s+      pformatPair :: (SomeTypedSymbol knd, ModelValue) -> Doc ann+      pformatPair (s, v) = pformatSymbolWithoutType s <> " -> " <> pformat v+      bodyFormatted = pformatListLike "{" "}" $ pformatPair <$> HM.toList m++instance PPrint (SymbolSet knd) where+  pformatPrec n (SymbolSet s) =+    pformatWithConstructor+      n+      "SymbolSet"+      [pformatListLike "{" "}" $ pformat <$> HS.toList s]

@@ -0,0 +1,141 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module      :   Grisette.Internal.Core.Data.Class.SafeBitCast+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.Core.Data.Class.SafeBitCast+  ( SafeBitCast (..),+  )+where++import Control.Monad.Error.Class (MonadError (throwError))+import Data.Int (Int16, Int32, Int64)+import Data.SBV (Word32)+import Data.Word (Word16, Word64)+import GHC.TypeLits (KnownNat, type (+), type (<=))+import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)+import Grisette.Internal.Core.Data.Class.BitCast+  ( BitCast (bitCast),+    BitCastOr,+    bitCastOrCanonical,+  )+import Grisette.Internal.Core.Data.Class.IEEEFP (fpIsNaN)+import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Internal.Core.Data.Class.SimpleMergeable (mrgIf)+import Grisette.Internal.Core.Data.Class.SymIEEEFP+  ( SymIEEEFPTraits (symFpIsNaN),+  )+import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge, tryMerge)+import Grisette.Internal.SymPrim.BV (IntN, WordN, WordN16, WordN32, WordN64)+import Grisette.Internal.SymPrim.FP+  ( FP,+    FP16,+    FP32,+    FP64,+    NotRepresentableFPError (NaNError),+    ValidFP,+  )+import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)+import Grisette.Internal.SymPrim.SymFP (SymFP)++-- | Bitcasting a value. If the value cannot be precisely bitcast, throw an+-- error.+class+  (MonadError e m, TryMerge m, Mergeable b, BitCastOr a b) =>+  SafeBitCast e a b m+  where+  safeBitCast :: a -> m b++instance+  ( ValidFP eb sb,+    r ~ (eb + sb),+    KnownNat r,+    1 <= r,+    TryMerge m,+    MonadError NotRepresentableFPError m+  ) =>+  SafeBitCast NotRepresentableFPError (FP eb sb) (WordN r) m+  where+  safeBitCast a+    | fpIsNaN a = tryMerge $ throwError NaNError+    | otherwise = tryMerge $ return $ bitCastOrCanonical a++instance+  ( ValidFP eb sb,+    r ~ (eb + sb),+    KnownNat r,+    1 <= r,+    TryMerge m,+    MonadError NotRepresentableFPError m+  ) =>+  SafeBitCast NotRepresentableFPError (FP eb sb) (IntN r) m+  where+  safeBitCast a+    | fpIsNaN a = tryMerge $ throwError NaNError+    | otherwise = tryMerge $ return $ bitCastOrCanonical a++#define SAFE_BIT_CAST_VIA_INTERMEDIATE(from, to, intermediate) \+instance \+  (MonadError NotRepresentableFPError m, TryMerge m) => \+  SafeBitCast NotRepresentableFPError from to m \+  where \+  safeBitCast a = do \+    r :: intermediate <- safeBitCast a; \+    tryMerge $ return $ bitCast r++#if 1+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP64, Word64, WordN64)+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP64, Int64, WordN64)+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP64, Double, WordN64)+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP32, Word32, WordN32)+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP32, Int32, WordN32)+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP32, Float, WordN32)+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP16, Word16, WordN16)+SAFE_BIT_CAST_VIA_INTERMEDIATE(FP16, Int16, WordN16)+#endif++instance+  ( ValidFP eb sb,+    r ~ (eb + sb),+    KnownNat r,+    1 <= r,+    MonadUnion m,+    MonadError NotRepresentableFPError m+  ) =>+  SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN r) m+  where+  safeBitCast a =+    mrgIf+      (symFpIsNaN a)+      (throwError NaNError)+      (return $ bitCastOrCanonical a)++instance+  ( ValidFP eb sb,+    r ~ (eb + sb),+    KnownNat r,+    1 <= r,+    MonadUnion m,+    MonadError NotRepresentableFPError m+  ) =>+  SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN r) m+  where+  safeBitCast a =+    mrgIf+      (symFpIsNaN a)+      (throwError NaNError)+      (return $ bitCastOrCanonical a)

@@ -0,0 +1,475 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module      :   Grisette.Internal.Core.Data.Class.SafeDiv+-- Copyright   :   (c) Sirui Lu 2021-2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.Core.Data.Class.SafeDiv+  ( ArithException (..),+    SafeDiv (..),+    DivOr (..),+    divOrZero,+    modOrDividend,+    quotOrZero,+    remOrDividend,+    divModOrZeroDividend,+    quotRemOrZeroDividend,+  )+where++import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))+import Control.Monad.Except (MonadError (throwError))+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, type (<=))+import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)+import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))+import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp ((.&&)))+import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Internal.Core.Data.Class.SimpleMergeable+  ( mrgIf,+  )+import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))+import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))+import Grisette.Internal.Core.Data.Class.TryMerge+  ( TryMerge,+    mrgSingle,+    tryMerge,+  )+import Grisette.Internal.SymPrim.BV+  ( IntN,+    WordN,+  )+import Grisette.Internal.SymPrim.Prim.Term+  ( PEvalDivModIntegralTerm+      ( pevalDivIntegralTerm,+        pevalModIntegralTerm,+        pevalQuotIntegralTerm,+        pevalRemIntegralTerm+      ),+  )+import Grisette.Internal.SymPrim.SymBV+  ( SymIntN (SymIntN),+    SymWordN (SymWordN),+  )+import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))+import Grisette.Lib.Data.Functor (mrgFmap)++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.SymPrim+-- >>> import Control.Monad.Except+-- >>> import Control.Exception++-- | Safe division handling with default values returned on exception.+class DivOr a where+  -- | Safe 'div' with default value returned on exception.+  --+  -- >>> divOr "d" "a" "b" :: SymInteger+  -- (ite (= b 0) d (div a b))+  divOr :: a -> a -> a -> a++  -- | Safe 'mod' with default value returned on exception.+  --+  -- >>> modOr "d" "a" "b" :: SymInteger+  -- (ite (= b 0) d (mod a b))+  modOr :: a -> a -> a -> a++  -- | Safe 'divMod' with default value returned on exception.+  --+  -- >>> divModOr ("d", "m") "a" "b" :: (SymInteger, SymInteger)+  -- ((ite (= b 0) d (div a b)),(ite (= b 0) m (mod a b)))+  divModOr :: (a, a) -> a -> a -> (a, a)++  -- | Safe 'quot' with default value returned on exception.+  quotOr :: a -> a -> a -> a++  -- | Safe 'rem' with default value returned on exception.+  remOr :: a -> a -> a -> a++  -- | Safe 'quotRem' with default value returned on exception.+  quotRemOr :: (a, a) -> a -> a -> (a, a)++-- | Safe 'div' with 0 returned on exception.+divOrZero :: (DivOr a, Num a) => a -> a -> a+divOrZero l = divOr (l - l) l+{-# INLINE divOrZero #-}++-- | Safe 'mod' with dividend returned on exception.+modOrDividend :: (DivOr a, Num a) => a -> a -> a+modOrDividend l = modOr l l+{-# INLINE modOrDividend #-}++-- | Safe 'quot' with 0 returned on exception.+quotOrZero :: (DivOr a, Num a) => a -> a -> a+quotOrZero l = quotOr (l - l) l+{-# INLINE quotOrZero #-}++-- | Safe 'rem' with dividend returned on exception.+remOrDividend :: (DivOr a, Num a) => a -> a -> a+remOrDividend l = remOr l l+{-# INLINE remOrDividend #-}++-- | Safe 'divMod' with 0 returned on exception.+divModOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a)+divModOrZeroDividend l = divModOr (l - l, l) l+{-# INLINE divModOrZeroDividend #-}++-- | Safe 'quotRem' with 0 returned on exception.+quotRemOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a)+quotRemOrZeroDividend l = quotRemOr (l - l, l) l+{-# INLINE quotRemOrZeroDividend #-}++-- | Safe division with monadic error handling in multi-path+-- execution. These procedures throw an exception when the+-- divisor is zero. The result should be able to handle errors with+-- `MonadError`.+class (MonadError e m, TryMerge m, Mergeable a, DivOr a) => SafeDiv e a m where+  -- | Safe 'div' with monadic error handling in multi-path execution.+  --+  -- >>> safeDiv "a" "b" :: ExceptT ArithException Union SymInteger+  -- ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}+  safeDiv :: a -> a -> m a+  safeDiv l r = mrgFmap fst $ safeDivMod l r+  {-# INLINE safeDiv #-}++  -- | Safe 'mod' with monadic error handling in multi-path execution.+  --+  -- >>> safeMod "a" "b" :: ExceptT ArithException Union SymInteger+  -- ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}+  safeMod :: a -> a -> m a+  safeMod l r = mrgFmap snd $ safeDivMod l r+  {-# INLINE safeMod #-}++  -- | Safe 'divMod' with monadic error handling in multi-path execution.+  --+  -- >>> safeDivMod "a" "b" :: ExceptT ArithException Union (SymInteger, SymInteger)+  -- ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}+  safeDivMod :: a -> a -> m (a, a)+  safeDivMod l r = do+    d <- safeDiv l r+    m <- safeMod l r+    mrgSingle (d, m)+  {-# INLINE safeDivMod #-}++  -- | Safe 'quot' with monadic error handling in multi-path execution.+  safeQuot :: a -> a -> m a+  safeQuot l r = mrgFmap fst $ safeQuotRem l r+  {-# INLINE safeQuot #-}++  -- | Safe 'rem' with monadic error handling in multi-path execution.+  safeRem :: a -> a -> m a+  safeRem l r = mrgFmap snd $ safeQuotRem l r+  {-# INLINE safeRem #-}++  -- | Safe 'quotRem' with monadic error handling in multi-path execution.+  safeQuotRem :: a -> a -> m (a, a)+  safeQuotRem l r = do+    q <- safeQuot l r+    m <- safeRem l r+    mrgSingle (q, m)+  {-# INLINE safeQuotRem #-}++  {-# MINIMAL+    ((safeDiv, safeMod) | safeDivMod),+    ((safeQuot, safeRem) | safeQuotRem)+    #-}++concreteDivOrHelper ::+  (Integral a) =>+  (a -> a -> r) ->+  r ->+  a ->+  a ->+  r+concreteDivOrHelper f d l r+  | r == 0 = d+  | otherwise = f l r++concreteSafeDivHelper ::+  (MonadError ArithException m, TryMerge m, Integral a, Mergeable r) =>+  (a -> a -> r) ->+  a ->+  a ->+  m r+concreteSafeDivHelper f l r+  | r == 0 = tryMerge $ throwError DivideByZero+  | otherwise = mrgSingle $ f l r++concreteSignedBoundedDivOrHelper ::+  ( Integral a,+    Bounded a,+    Mergeable r+  ) =>+  (a -> a -> r) ->+  r ->+  a ->+  a ->+  r+concreteSignedBoundedDivOrHelper f d l r+  | r == 0 = d+  | l == minBound && r == -1 = d+  | otherwise = f l r++concreteSignedBoundedSafeDivHelper ::+  ( MonadError ArithException m,+    TryMerge m,+    Integral a,+    Bounded a,+    Mergeable r+  ) =>+  (a -> a -> r) ->+  a ->+  a ->+  m r+concreteSignedBoundedSafeDivHelper f l r+  | r == 0 = tryMerge $ throwError DivideByZero+  | l == minBound && r == -1 = tryMerge $ throwError Overflow+  | otherwise = mrgSingle $ f l r++#define QUOTE() '+#define QID(a) a+#define QRIGHT(a) QID(a)'++#define QRIGHTT(a) QID(a)' t'+#define QRIGHTU(a) QID(a)' _'++#define DIVISION_OR_CONCRETE(type) \+instance DivOr type where \+  divOr = concreteDivOrHelper div; \+  modOr = concreteDivOrHelper mod; \+  divModOr = concreteDivOrHelper divMod; \+  quotOr = concreteDivOrHelper quot; \+  remOr = concreteDivOrHelper rem; \+  quotRemOr = concreteDivOrHelper quotRem++#define SAFE_DIVISION_CONCRETE(type) \+instance (MonadError ArithException m, TryMerge m) => \+  SafeDiv ArithException type m where \+  safeDiv = concreteSafeDivHelper div; \+  safeMod = concreteSafeDivHelper mod; \+  safeDivMod = concreteSafeDivHelper divMod; \+  safeQuot = concreteSafeDivHelper quot; \+  safeRem = concreteSafeDivHelper rem; \+  safeQuotRem = concreteSafeDivHelper quotRem++#define DIVISION_OR_CONCRETE_SIGNED_BOUNDED(type) \+instance DivOr type where \+  divOr = concreteSignedBoundedDivOrHelper div; \+  modOr = concreteDivOrHelper mod; \+  divModOr = concreteSignedBoundedDivOrHelper divMod; \+  quotOr = concreteSignedBoundedDivOrHelper quot; \+  remOr = concreteDivOrHelper rem; \+  quotRemOr = concreteSignedBoundedDivOrHelper quotRem++#define SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(type) \+instance (MonadError ArithException m, TryMerge m) => \+  SafeDiv ArithException type m where \+  safeDiv = concreteSignedBoundedSafeDivHelper div; \+  safeMod = concreteSafeDivHelper mod; \+  safeDivMod = concreteSignedBoundedSafeDivHelper divMod; \+  safeQuot = concreteSignedBoundedSafeDivHelper quot; \+  safeRem = concreteSafeDivHelper rem; \+  safeQuotRem = concreteSignedBoundedSafeDivHelper quotRem++#if 1+DIVISION_OR_CONCRETE(Integer)+SAFE_DIVISION_CONCRETE(Integer)+DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int8)+SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int8)+DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int16)+SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int16)+DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int32)+SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int32)+DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int64)+SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int64)+DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int)+SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int)+DIVISION_OR_CONCRETE(Word8)+SAFE_DIVISION_CONCRETE(Word8)+DIVISION_OR_CONCRETE(Word16)+SAFE_DIVISION_CONCRETE(Word16)+DIVISION_OR_CONCRETE(Word32)+SAFE_DIVISION_CONCRETE(Word32)+DIVISION_OR_CONCRETE(Word64)+SAFE_DIVISION_CONCRETE(Word64)+DIVISION_OR_CONCRETE(Word)+SAFE_DIVISION_CONCRETE(Word)+++#endif++instance (KnownNat n, 1 <= n) => DivOr (IntN n) where+  divOr = concreteSignedBoundedDivOrHelper div+  modOr = concreteDivOrHelper mod+  divModOr = concreteSignedBoundedDivOrHelper divMod+  quotOr = concreteSignedBoundedDivOrHelper quot+  remOr = concreteDivOrHelper rem+  quotRemOr = concreteSignedBoundedDivOrHelper quotRem++instance+  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>+  SafeDiv ArithException (IntN n) m+  where+  safeDiv = concreteSignedBoundedSafeDivHelper div+  safeMod = concreteSafeDivHelper mod+  safeDivMod = concreteSignedBoundedSafeDivHelper divMod+  safeQuot = concreteSignedBoundedSafeDivHelper quot+  safeRem = concreteSafeDivHelper rem+  safeQuotRem = concreteSignedBoundedSafeDivHelper quotRem++instance (KnownNat n, 1 <= n) => DivOr (WordN n) where+  divOr = concreteDivOrHelper div+  modOr = concreteDivOrHelper mod+  divModOr = concreteDivOrHelper divMod+  quotOr = concreteDivOrHelper quot+  remOr = concreteDivOrHelper rem+  quotRemOr = concreteDivOrHelper quotRem++instance+  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>+  SafeDiv ArithException (WordN n) m+  where+  safeDiv = concreteSafeDivHelper div+  safeMod = concreteSafeDivHelper mod+  safeDivMod = concreteSafeDivHelper divMod+  safeQuot = concreteSafeDivHelper quot+  safeRem = concreteSafeDivHelper rem+  safeQuotRem = concreteSafeDivHelper quotRem++#define DIVISION_OR_SYMBOLIC_FUNC(name, type, op) \+name d (type l) rs@(type r) = \+  symIte (rs .== con 0) d (type $ op l r)++#define DIVISION_OR_SYMBOLIC_FUNC2(name, type, op1, op2) \+name (dd, dm) (type l) rs@(type r) = \+  (symIte (rs .== con 0) dd (type $ op1 l r), \+   symIte (rs .== con 0) dm (type $ op2 l r))++#define SAFE_DIVISION_SYMBOLIC_FUNC(name, type, op) \+name (type l) rs@(type r) = \+  mrgIf \+    (rs .== con 0) \+    (throwError DivideByZero) \+    (mrgSingle $ type $ op l r); \++#define SAFE_DIVISION_SYMBOLIC_FUNC2(name, type, op1, op2) \+name (type l) rs@(type r) = \+  mrgIf \+    (rs .== con 0) \+    (throwError DivideByZero) \+    (mrgSingle (type $ op1 l r, type $ op2 l r)); \++#if 1+instance DivOr SymInteger where+  DIVISION_OR_SYMBOLIC_FUNC(divOr, SymInteger, pevalDivIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(modOr, SymInteger, pevalModIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(quotOr, SymInteger, pevalQuotIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(remOr, SymInteger, pevalRemIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC2(divModOr, SymInteger, pevalDivIntegralTerm, pevalModIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC2(quotRemOr, SymInteger, pevalQuotIntegralTerm, pevalRemIntegralTerm)+instance+  (MonadUnion m, MonadError ArithException m) =>+  SafeDiv ArithException SymInteger m where+  SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, SymInteger, pevalDivIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymInteger, pevalModIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, SymInteger, pevalQuotIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymInteger, pevalRemIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, SymInteger, pevalDivIntegralTerm, pevalModIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, SymInteger, pevalQuotIntegralTerm, pevalRemIntegralTerm)+#endif++#define DIVISION_OR_SYMBOLIC_FUNC_BOUNDED_SIGNED(name, type, op) \+name d ls@(type l) rs@(type r) = \+  symIte \+    (rs .== con 0) \+    d \+    (symIte (rs .== con (-1) .&& ls .== con minBound) \+      d \+      (type $ op l r)) \++#define DIVISION_OR_SYMBOLIC_FUNC2_BOUNDED_SIGNED(name, type, op1, op2) \+name (dd, dr) ls@(type l) rs@(type r) = \+  (symIte \+    (rs .== con 0) \+    dd \+    (symIte (rs .== con (-1) .&& ls .== con minBound) \+      dd \+      (type $ op1 l r)), \+  symIte \+    (rs .== con 0) \+    dr \+    (symIte (rs .== con (-1) .&& ls .== con minBound) \+      dr \+      (type $ op2 l r))) \++#define SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(name, type, op) \+name ls@(type l) rs@(type r) = \+  mrgIf \+    (rs .== con 0) \+    (throwError DivideByZero) \+    (mrgIf (rs .== con (-1) .&& ls .== con minBound) \+      (throwError Overflow) \+      (mrgSingle $ type $ op l r)); \++#define SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(name, type, op1, op2) \+name ls@(type l) rs@(type r) = \+  mrgIf \+    (rs .== con 0) \+    (throwError DivideByZero) \+    (mrgIf (rs .== con (-1) .&& ls .== con minBound) \+      (throwError Overflow) \+      (mrgSingle (type $ op1 l r, type $ op2 l r))); \++#if 1+instance (KnownNat n, 1 <= n) => DivOr (SymIntN n) where+  DIVISION_OR_SYMBOLIC_FUNC_BOUNDED_SIGNED(divOr, SymIntN, pevalDivIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(modOr, SymIntN, pevalModIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC_BOUNDED_SIGNED(quotOr, SymIntN, pevalQuotIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(remOr, SymIntN, pevalRemIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC2_BOUNDED_SIGNED(divModOr, SymIntN, pevalDivIntegralTerm, pevalModIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC2_BOUNDED_SIGNED(quotRemOr, SymIntN, pevalQuotIntegralTerm, pevalRemIntegralTerm)+instance+  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>+  SafeDiv ArithException (SymIntN n) m where+  SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeDiv, SymIntN, pevalDivIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymIntN, pevalModIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeQuot, SymIntN, pevalQuotIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymIntN, pevalRemIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeDivMod, SymIntN, pevalDivIntegralTerm, pevalModIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeQuotRem, SymIntN, pevalQuotIntegralTerm, pevalRemIntegralTerm)+#endif++#if 1+instance (KnownNat n, 1 <= n) => DivOr (SymWordN n) where+  DIVISION_OR_SYMBOLIC_FUNC(divOr, SymWordN, pevalDivIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(modOr, SymWordN, pevalModIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(quotOr, SymWordN, pevalQuotIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC(remOr, SymWordN, pevalRemIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC2(divModOr, SymWordN, pevalDivIntegralTerm, pevalModIntegralTerm)+  DIVISION_OR_SYMBOLIC_FUNC2(quotRemOr, SymWordN, pevalQuotIntegralTerm, pevalRemIntegralTerm)+instance+  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>+  SafeDiv ArithException (SymWordN n) m where+  SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, SymWordN, pevalDivIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymWordN, pevalModIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, SymWordN, pevalQuotIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymWordN, pevalRemIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, SymWordN, pevalDivIntegralTerm, pevalModIntegralTerm)+  SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, SymWordN, pevalQuotIntegralTerm, pevalRemIntegralTerm)+#endif

@@ -1,290 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DerivingVia #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}---- |--- Module      :   Grisette.Internal.Core.Data.Class.SafeDivision--- Copyright   :   (c) Sirui Lu 2021-2024--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Internal.Core.Data.Class.SafeDivision-  ( ArithException (..),-    SafeDivision (..),-  )-where--import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))-import Control.Monad.Except (MonadError (throwError))-import Data.Int (Int16, Int32, Int64, Int8)-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, type (<=))-import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)-import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp ((.&&)))-import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)-import Grisette.Internal.Core.Data.Class.SimpleMergeable-  ( mrgIf,-  )-import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))-import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))-import Grisette.Internal.Core.Data.Class.TryMerge-  ( TryMerge,-    mrgSingle,-    tryMerge,-  )-import Grisette.Internal.SymPrim.BV-  ( IntN,-    WordN,-  )-import Grisette.Internal.SymPrim.Prim.Term-  ( PEvalDivModIntegralTerm-      ( pevalDivIntegralTerm,-        pevalModIntegralTerm,-        pevalQuotIntegralTerm,-        pevalRemIntegralTerm-      ),-  )-import Grisette.Internal.SymPrim.SymBV-  ( SymIntN (SymIntN),-    SymWordN (SymWordN),-  )-import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))-import Grisette.Lib.Data.Functor (mrgFmap)---- $setup--- >>> import Grisette.Core--- >>> import Grisette.SymPrim--- >>> import Control.Monad.Except--- >>> import Control.Exception---- | Safe division with monadic error handling in multi-path--- execution. These procedures throw an exception when the--- divisor is zero. The result should be able to handle errors with--- `MonadError`.-class (MonadError e m, TryMerge m, Mergeable a) => SafeDivision e a m where-  -- | Safe signed 'div' with monadic error handling in multi-path execution.-  ---  -- >>> safeDiv (ssym "a") (ssym "b") :: ExceptT ArithException Union SymInteger-  -- ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}-  safeDiv :: a -> a -> m a-  safeDiv l r = mrgFmap fst $ safeDivMod l r-  {-# INLINE safeDiv #-}--  -- | Safe signed 'mod' with monadic error handling in multi-path execution.-  ---  -- >>> safeMod (ssym "a") (ssym "b") :: ExceptT ArithException Union SymInteger-  -- ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}-  safeMod :: a -> a -> m a-  safeMod l r = mrgFmap snd $ safeDivMod l r-  {-# INLINE safeMod #-}--  -- | Safe signed 'divMod' with monadic error handling in multi-path execution.-  ---  -- >>> safeDivMod (ssym "a") (ssym "b") :: ExceptT ArithException Union (SymInteger, SymInteger)-  -- ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}-  safeDivMod :: a -> a -> m (a, a)-  safeDivMod l r = do-    d <- safeDiv l r-    m <- safeMod l r-    mrgSingle (d, m)-  {-# INLINE safeDivMod #-}--  -- | Safe signed 'quot' with monadic error handling in multi-path execution.-  safeQuot :: a -> a -> m a-  safeQuot l r = mrgFmap fst $ safeQuotRem l r-  {-# INLINE safeQuot #-}--  -- | Safe signed 'rem' with monadic error handling in multi-path execution.-  safeRem :: a -> a -> m a-  safeRem l r = mrgFmap snd $ safeQuotRem l r-  {-# INLINE safeRem #-}--  -- | Safe signed 'quotRem' with monadic error handling in multi-path execution.-  safeQuotRem :: a -> a -> m (a, a)-  safeQuotRem l r = do-    q <- safeQuot l r-    m <- safeRem l r-    mrgSingle (q, m)-  {-# INLINE safeQuotRem #-}--  {-# MINIMAL-    ((safeDiv, safeMod) | safeDivMod),-    ((safeQuot, safeRem) | safeQuotRem)-    #-}--concreteSafeDivisionHelper ::-  (MonadError ArithException m, TryMerge m, Integral a, Mergeable r) =>-  (a -> a -> r) ->-  a ->-  a ->-  m r-concreteSafeDivisionHelper f l r-  | r == 0 = tryMerge $ throwError DivideByZero-  | otherwise = mrgSingle $ f l r--concreteSignedBoundedSafeDivisionHelper ::-  ( MonadError ArithException m,-    TryMerge m,-    Integral a,-    Bounded a,-    Mergeable r-  ) =>-  (a -> a -> r) ->-  a ->-  a ->-  m r-concreteSignedBoundedSafeDivisionHelper f l r-  | r == 0 = tryMerge $ throwError DivideByZero-  | l == minBound && r == -1 = tryMerge $ throwError Overflow-  | otherwise = mrgSingle $ f l r--#define QUOTE() '-#define QID(a) a-#define QRIGHT(a) QID(a)'--#define QRIGHTT(a) QID(a)' t'-#define QRIGHTU(a) QID(a)' _'--#define SAFE_DIVISION_CONCRETE(type) \-instance (MonadError ArithException m, TryMerge m) => \-  SafeDivision ArithException type m where \-  safeDiv = concreteSafeDivisionHelper div; \-  safeMod = concreteSafeDivisionHelper mod; \-  safeDivMod = concreteSafeDivisionHelper divMod; \-  safeQuot = concreteSafeDivisionHelper quot; \-  safeRem = concreteSafeDivisionHelper rem; \-  safeQuotRem = concreteSafeDivisionHelper quotRem--#define SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(type) \-instance (MonadError ArithException m, TryMerge m) => \-  SafeDivision ArithException type m where \-  safeDiv = concreteSignedBoundedSafeDivisionHelper div; \-  safeMod = concreteSafeDivisionHelper mod; \-  safeDivMod = concreteSignedBoundedSafeDivisionHelper divMod; \-  safeQuot = concreteSignedBoundedSafeDivisionHelper quot; \-  safeRem = concreteSafeDivisionHelper rem; \-  safeQuotRem = concreteSignedBoundedSafeDivisionHelper quotRem--#define SAFE_DIVISION_CONCRETE_BV(type) \-instance \-  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => \-  SafeDivision ArithException (type n) m where \-  safeDiv = concreteSafeDivisionHelper div; \-  safeMod = concreteSafeDivisionHelper mod; \-  safeDivMod = concreteSafeDivisionHelper divMod; \-  safeQuot = concreteSafeDivisionHelper quot; \-  safeRem = concreteSafeDivisionHelper rem; \-  safeQuotRem = concreteSafeDivisionHelper quotRem--#if 1-SAFE_DIVISION_CONCRETE(Integer)-SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int8)-SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int16)-SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int32)-SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int64)-SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int)-SAFE_DIVISION_CONCRETE(Word8)-SAFE_DIVISION_CONCRETE(Word16)-SAFE_DIVISION_CONCRETE(Word32)-SAFE_DIVISION_CONCRETE(Word64)-SAFE_DIVISION_CONCRETE(Word)--instance-  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>-  SafeDivision ArithException (IntN n) m where-  safeDiv = concreteSignedBoundedSafeDivisionHelper div-  safeMod = concreteSafeDivisionHelper mod-  safeDivMod = concreteSignedBoundedSafeDivisionHelper divMod-  safeQuot = concreteSignedBoundedSafeDivisionHelper quot-  safeRem = concreteSafeDivisionHelper rem-  safeQuotRem = concreteSignedBoundedSafeDivisionHelper quotRem--instance-  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>-  SafeDivision ArithException (WordN n) m where-  safeDiv = concreteSafeDivisionHelper div-  safeMod = concreteSafeDivisionHelper mod-  safeDivMod = concreteSafeDivisionHelper divMod-  safeQuot = concreteSafeDivisionHelper quot-  safeRem = concreteSafeDivisionHelper rem-  safeQuotRem = concreteSafeDivisionHelper quotRem-#endif--#define SAFE_DIVISION_SYMBOLIC_FUNC(name, type, op) \-name (type l) rs@(type r) = \-  mrgIf \-    (rs .== con 0) \-    (throwError DivideByZero) \-    (mrgSingle $ type $ op l r); \--#define SAFE_DIVISION_SYMBOLIC_FUNC2(name, type, op1, op2) \-name (type l) rs@(type r) = \-  mrgIf \-    (rs .== con 0) \-    (throwError DivideByZero) \-    (mrgSingle (type $ op1 l r, type $ op2 l r)); \--#if 1-instance-  (MonadUnion m, MonadError ArithException m) =>-  SafeDivision ArithException SymInteger m where-  SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, SymInteger, pevalDivIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymInteger, pevalModIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, SymInteger, pevalQuotIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymInteger, pevalRemIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, SymInteger, pevalDivIntegralTerm, pevalModIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, SymInteger, pevalQuotIntegralTerm, pevalRemIntegralTerm)-#endif--#define SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(name, type, op) \-name ls@(type l) rs@(type r) = \-  mrgIf \-    (rs .== con 0) \-    (throwError DivideByZero) \-    (mrgIf (rs .== con (-1) .&& ls .== con minBound) \-      (throwError Overflow) \-      (mrgSingle $ type $ op l r)); \--#define SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(name, type, op1, op2) \-name ls@(type l) rs@(type r) = \-  mrgIf \-    (rs .== con 0) \-    (throwError DivideByZero) \-    (mrgIf (rs .== con (-1) .&& ls .== con minBound) \-      (throwError Overflow) \-      (mrgSingle (type $ op1 l r, type $ op2 l r))); \--#if 1-instance-  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>-  SafeDivision ArithException (SymIntN n) m where-  SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeDiv, SymIntN, pevalDivIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymIntN, pevalModIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeQuot, SymIntN, pevalQuotIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymIntN, pevalRemIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeDivMod, SymIntN, pevalDivIntegralTerm, pevalModIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeQuotRem, SymIntN, pevalQuotIntegralTerm, pevalRemIntegralTerm)-#endif--#if 1-instance-  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>-  SafeDivision ArithException (SymWordN n) m where-  SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, SymWordN, pevalDivIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymWordN, pevalModIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, SymWordN, pevalQuotIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymWordN, pevalRemIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, SymWordN, pevalDivIntegralTerm, pevalModIntegralTerm)-  SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, SymWordN, pevalQuotIntegralTerm, pevalRemIntegralTerm)-#endif

@@ -0,0 +1,153 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module      :   Grisette.Internal.Core.Data.Class.SafeFdiv+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.Core.Data.Class.SafeFdiv+  ( SafeFdiv (..),+    FdivOr (..),+    fdivOrZero,+    recipOrZero,+  )+where++import Control.Exception (ArithException (RatioZeroDenominator), throw)+import Control.Monad.Error.Class (MonadError (throwError))+import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)+import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))+import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Internal.Core.Data.Class.SimpleMergeable (mrgIf)+import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))+import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))+import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge, tryMerge)+import Grisette.Internal.SymPrim.AlgReal+  ( AlgReal (AlgExactRational),+    UnsupportedAlgRealOperation (UnsupportedAlgRealOperation),+  )+import Grisette.Internal.SymPrim.Prim.Internal.Term+  ( PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),+  )+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.SymPrim+-- >>> import Control.Monad.Except+-- >>> import Control.Exception++-- | Safe fractional with default values returned on exception.+class FdivOr a where+  -- | Safe '/' with default values returned on exception.+  --+  -- >>> fdivOr "d" "a" "b" :: SymAlgReal+  -- (ite (= b 0.0) d (fdiv a b))+  fdivOr :: a -> a -> a -> a++  -- | Safe 'recip' with default values returned on exception.+  --+  -- >>> recipOr "d" "a" :: SymAlgReal+  -- (ite (= a 0.0) d (recip a))+  recipOr :: a -> a -> a++-- | Safe '/' with 0 returned on exception.+fdivOrZero :: (FdivOr a, Num a) => a -> a -> a+fdivOrZero l = fdivOr (l - l) l++-- | Safe 'recip' with 0 returned on exception.+recipOrZero :: (FdivOr a, Num a) => a -> a+recipOrZero v = recipOr (v - v) v++-- | Safe fractional division with monadic error handling in multi-path+-- execution. These procedures throw an exception when the denominator is zero.+-- The result should be able to handle errors with `MonadError`.+class (MonadError e m, TryMerge m, Mergeable a) => SafeFdiv e a m where+  -- | Safe fractional division with monadic error handling in multi-path+  -- execution.+  --+  -- >>> safeFdiv "a" "b" :: ExceptT ArithException Union SymAlgReal+  -- ExceptT {If (= b 0.0) (Left Ratio has zero denominator) (Right (fdiv a b))}+  safeFdiv :: a -> a -> m a++  -- | Safe fractional reciprocal with monadic error handling in multi-path+  -- execution.+  --+  -- >>> safeRecip "a" :: ExceptT ArithException Union SymAlgReal+  -- ExceptT {If (= a 0.0) (Left Ratio has zero denominator) (Right (recip a))}+  safeRecip :: a -> m a+  default safeRecip :: (Fractional a) => a -> m a+  safeRecip = safeFdiv (fromRational 1)+  {-# INLINE safeRecip #-}++  {-# MINIMAL safeFdiv #-}++instance FdivOr AlgReal where+  fdivOr d (AlgExactRational l) (AlgExactRational r)+    | r /= 0 = AlgExactRational (l / r)+    | otherwise = d+  fdivOr d l r =+    -- Throw the error because the user should never construct an AlgReal+    -- other than AlgExactRational.+    throw $+      UnsupportedAlgRealOperation "fdivOr" $+        show d <> " and " <> show l <> " and " <> show r+  {-# INLINE fdivOr #-}+  recipOr d (AlgExactRational l)+    | l /= 0 = AlgExactRational (recip l)+    | otherwise = d+  recipOr d l =+    throw $ UnsupportedAlgRealOperation "recipOr" $ show d <> " and " <> show l+  {-# INLINE recipOr #-}++instance+  ( MonadError ArithException m,+    TryMerge m+  ) =>+  SafeFdiv ArithException AlgReal m+  where+  safeFdiv (AlgExactRational l) (AlgExactRational r)+    | r /= 0 =+        pure $ AlgExactRational (l / r)+    | otherwise = tryMerge $ throwError RatioZeroDenominator+  safeFdiv l r =+    -- Throw the error because the user should never construct an AlgReal+    -- other than AlgExactRational.+    throw $+      UnsupportedAlgRealOperation "safeFdiv" $+        show l <> " and " <> show r+  {-# INLINE safeFdiv #-}+  safeRecip (AlgExactRational l)+    | l /= 0 =+        pure $ AlgExactRational (recip l)+    | otherwise = tryMerge $ throwError RatioZeroDenominator+  safeRecip l =+    throw $ UnsupportedAlgRealOperation "safeRecip" $ show l++instance FdivOr SymAlgReal where+  fdivOr d (SymAlgReal lt) r@(SymAlgReal rt) =+    symIte (r .== con 0) d (SymAlgReal $ pevalFdivTerm lt rt)+  recipOr d l@(SymAlgReal lt) =+    symIte (l .== con 0) d (SymAlgReal $ pevalRecipTerm lt)++instance+  (MonadError ArithException m, MonadUnion m) =>+  SafeFdiv ArithException SymAlgReal m+  where+  safeFdiv (SymAlgReal lt) r@(SymAlgReal rt) =+    mrgIf+      (r .== con 0)+      (throwError RatioZeroDenominator)+      (pure $ SymAlgReal $ pevalFdivTerm lt rt)+  safeRecip l@(SymAlgReal lt) =+    mrgIf+      (l .== con 0)+      (throwError RatioZeroDenominator)+      (pure $ SymAlgReal $ pevalRecipTerm lt)