grisette 0.5.0.1 → 0.6.0.0

raw patch · 52 files changed

+5103/−1289 lines, 52 filesdep ~sbvdep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: sbv, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +39/−2
• README.md +9/−1
• grisette.cabal +22/−13
• src/Grisette/Backend.hs +2/−0
• src/Grisette/Core.hs +45/−3
• src/Grisette/Internal/Backend/Solving.hs +85/−12
• src/Grisette/Internal/Core/Data/Class/BitCast.hs +47/−0
• src/Grisette/Internal/Core/Data/Class/CEGISSolver.hs +670/−160
• src/Grisette/Internal/Core/Data/Class/EvaluateSym.hs +13/−0
• src/Grisette/Internal/Core/Data/Class/ExtractSymbolics.hs +15/−0
• src/Grisette/Internal/Core/Data/Class/GPretty.hs +46/−51
• src/Grisette/Internal/Core/Data/Class/GenSym.hs +34/−0
• src/Grisette/Internal/Core/Data/Class/IEEEFP.hs +338/−0
• src/Grisette/Internal/Core/Data/Class/ITEOp.hs +10/−0
• src/Grisette/Internal/Core/Data/Class/Mergeable.hs +24/−1
• src/Grisette/Internal/Core/Data/Class/PlainUnion.hs +17/−1
• src/Grisette/Internal/Core/Data/Class/SEq.hs +25/−3
• src/Grisette/Internal/Core/Data/Class/SOrd.hs +16/−0
• src/Grisette/Internal/Core/Data/Class/SimpleMergeable.hs +10/−1
• src/Grisette/Internal/Core/Data/Class/Solver.hs +155/−34
• src/Grisette/Internal/Core/Data/Class/SubstituteSym.hs +15/−0
• src/Grisette/Internal/Core/Data/Class/ToCon.hs +26/−1
• src/Grisette/Internal/Core/Data/Class/ToSym.hs +25/−0
• src/Grisette/Internal/Core/Data/Symbol.hs +23/−2
• src/Grisette/Internal/SymPrim/BV.hs +91/−0
• src/Grisette/Internal/SymPrim/FP.hs +268/−0
• src/Grisette/Internal/SymPrim/GeneralFun.hs +20/−1
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalFP.hs +218/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalFloatingTerm.hs +25/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalFractionalTerm.hs +26/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalNumTerm.hs +11/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalOrdTerm.hs +63/−3
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/SupportedPrim.hs +100/−3
• src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs +397/−1
• src/Grisette/Internal/SymPrim/Prim/Internal/Unfold.hs +34/−1
• src/Grisette/Internal/SymPrim/Prim/Model.hs +33/−0
• src/Grisette/Internal/SymPrim/Prim/Term.hs +4/−0
• src/Grisette/Internal/SymPrim/Prim/TermUtils.hs +41/−0
• src/Grisette/Internal/SymPrim/SomeBV.hs +38/−4
• src/Grisette/Internal/SymPrim/SymFP.hs +169/−0
• test/Grisette/Backend/CEGISTests.hs +72/−3
• test/Grisette/Backend/LoweringTests.hs +71/−67
• test/Grisette/Backend/TermRewritingGen.hs +282/−1
• test/Grisette/Backend/TermRewritingTests.hs +132/−2
• test/Grisette/Core/Data/BVTests.hs +0/−523
• test/Grisette/Core/Data/Class/GPrettyTests.hs +38/−2
• test/Grisette/Core/Data/Class/PlainUnionTests.hs +13/−5
• test/Grisette/Core/Data/SomeBVTests.hs +0/−382
• test/Grisette/SymPrim/BVTests.hs +523/−0
• test/Grisette/SymPrim/FPTests.hs +289/−0
• test/Grisette/SymPrim/SomeBVTests.hs +426/−0
• test/Main.hs +8/−6

@@ -6,8 +6,44 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [Unreleased]+## [0.6.0.0] +### Added++- Added solving procedures with solver handles.+  ([#198](https://github.com/lsrcz/grisette/pull/198))+- Added `overestimateUnionValues`.+  ([#203](https://github.com/lsrcz/grisette/pull/203))+- Added pretty printing for hashset and hashmaps.+  ([#205](https://github.com/lsrcz/grisette/pull/205))+- Added support for refinement of solutions in CEGIS algorithm.+  ([#206](https://github.com/lsrcz/grisette/pull/206))+- Added generation of globally unique identifier with `uniqueIdentifier`.+  ([#206](https://github.com/lsrcz/grisette/pull/206))+- Added support for arbitrary precision floating point theory.+  ([#207](https://github.com/lsrcz/grisette/pull/207))++### Fixed++- `withSolver` now forcifully terminate the solver when exiting the scope.+  ([#199](https://github.com/lsrcz/grisette/pull/199))+- Fixed pretty printing for monad transformers.+  ([#205](https://github.com/lsrcz/grisette/pull/205))++### Changed++- [Breaking] Equality test for `SomeBV` with different bit widths will now+  return false rather than crash.+  ([#200](https://github.com/lsrcz/grisette/pull/200))+- [Breaking] More intuitive CEGIS interface.+  ([#201](https://github.com/lsrcz/grisette/pull/201))+- [Breaking] Changed the low-level solver interface.+  ([#206](https://github.com/lsrcz/grisette/pull/206))+- [Breaking] Changed the CEGIS interface.+  ([#206](https://github.com/lsrcz/grisette/pull/206))+- Bumped the minimum supported sbv version to 8.17.+  ([#207](https://github.com/lsrcz/grisette/pull/207))+ ## [0.5.0.1] -- 2024-04-18  ### Fixed@@ -283,7 +319,8 @@  - Initial release for Grisette. -[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.5.0.1...HEAD+[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.6.0.0...HEAD+[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 [0.5.0.0]: https://github.com/lsrcz/grisette/compare/v0.4.1.0...v0.5.0.0 [0.4.1.0]: https://github.com/lsrcz/grisette/compare/v0.4.0.0...v0.4.1.0

@@ -49,7 +49,7 @@ ```cabal library   ...-  build-depends: grisette >= 0.5.0.1 < 0.6+  build-depends: grisette >= 0.6 < 0.7 ```  #### Quick start template with `stack new`@@ -260,6 +260,14 @@  The Grisette library is distributed under the terms of the BSD3 license. The [LICENSE](LICENSE) file contains the full license text.++## Note++Grisette currently supports boolean, uninterpreted functions, bitvector,+integer, and floating point theories. However, if you want to use the floating+point theory, please make sure that you have the latest libBF (>=0.6.8) and sbv +installed (>=10.10.6). We've detected and fixed several bugs that would prevent+a sound reasoning for floating points.  ## Citing Grisette 

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           grisette-version:        0.5.0.1+version:        0.6.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@@ -29,8 +29,9 @@   , GHC == 9.0.2   , GHC == 9.2.8   , GHC == 9.4.8-  , GHC == 9.6.4+  , GHC == 9.6.5   , GHC == 9.8.2+  , GHC == 9.10.1 extra-source-files:     CHANGELOG.md     README.md@@ -59,6 +60,7 @@       Grisette.Internal.Core.Control.Monad.CBMCExcept       Grisette.Internal.Core.Control.Monad.Union       Grisette.Internal.Core.Control.Monad.UnionM+      Grisette.Internal.Core.Data.Class.BitCast       Grisette.Internal.Core.Data.Class.BitVector       Grisette.Internal.Core.Data.Class.CEGISSolver       Grisette.Internal.Core.Data.Class.Error@@ -67,6 +69,7 @@       Grisette.Internal.Core.Data.Class.Function       Grisette.Internal.Core.Data.Class.GenSym       Grisette.Internal.Core.Data.Class.GPretty+      Grisette.Internal.Core.Data.Class.IEEEFP       Grisette.Internal.Core.Data.Class.ITEOp       Grisette.Internal.Core.Data.Class.LogicalOp       Grisette.Internal.Core.Data.Class.Mergeable@@ -94,6 +97,7 @@       Grisette.Internal.Core.TH.MergeConstructor       Grisette.Internal.SymPrim.AllSyms       Grisette.Internal.SymPrim.BV+      Grisette.Internal.SymPrim.FP       Grisette.Internal.SymPrim.GeneralFun       Grisette.Internal.SymPrim.IntBitwidth       Grisette.Internal.SymPrim.ModelRep@@ -101,6 +105,9 @@       Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval       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.PEvalNumTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm       Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm@@ -119,6 +126,7 @@       Grisette.Internal.SymPrim.SomeBV       Grisette.Internal.SymPrim.SymBool       Grisette.Internal.SymPrim.SymBV+      Grisette.Internal.SymPrim.SymFP       Grisette.Internal.SymPrim.SymGeneralFun       Grisette.Internal.SymPrim.SymInteger       Grisette.Internal.SymPrim.SymTabularFun@@ -153,7 +161,7 @@       src   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns   build-depends:-      QuickCheck ==2.14.*+      QuickCheck >=2.14 && <2.16     , array >=0.5.4 && <0.6     , async >=2.2.2 && <2.3     , base >=4.14 && <5@@ -167,9 +175,9 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <11+    , sbv >=8.17 && <11     , stm ==2.5.*-    , template-haskell >=2.16 && <2.22+    , template-haskell >=2.16 && <2.23     , text >=1.2.4.1 && <2.2     , th-compat >=0.1.2 && <0.2     , transformers >=0.5.6 && <0.7@@ -190,7 +198,7 @@   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   build-depends:       Glob-    , QuickCheck ==2.14.*+    , QuickCheck >=2.14 && <2.16     , array >=0.5.4 && <0.6     , async >=2.2.2 && <2.3     , base >=4.14 && <5@@ -206,9 +214,9 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <11+    , sbv >=8.17 && <11     , stm ==2.5.*-    , template-haskell >=2.16 && <2.22+    , template-haskell >=2.16 && <2.23     , text >=1.2.4.1 && <2.2     , th-compat >=0.1.2 && <0.2     , transformers >=0.5.6 && <0.7@@ -230,7 +238,6 @@       Grisette.Core.Control.ExceptionTests       Grisette.Core.Control.Monad.UnionMTests       Grisette.Core.Control.Monad.UnionTests-      Grisette.Core.Data.BVTests       Grisette.Core.Data.Class.BoolTests       Grisette.Core.Data.Class.EvaluateSymTests       Grisette.Core.Data.Class.ExtractSymbolicsTests@@ -252,7 +259,6 @@       Grisette.Core.Data.Class.ToConTests       Grisette.Core.Data.Class.ToSymTests       Grisette.Core.Data.Class.TryMergeTests-      Grisette.Core.Data.SomeBVTests       Grisette.Lib.Control.ApplicativeTest       Grisette.Lib.Control.Monad.ExceptTests       Grisette.Lib.Control.Monad.State.ClassTests@@ -266,6 +272,8 @@       Grisette.Lib.Data.FunctorTests       Grisette.Lib.Data.ListTests       Grisette.Lib.Data.TraversableTests+      Grisette.SymPrim.BVTests+      Grisette.SymPrim.FPTests       Grisette.SymPrim.Prim.BitsTests       Grisette.SymPrim.Prim.BoolTests       Grisette.SymPrim.Prim.BVTests@@ -273,6 +281,7 @@       Grisette.SymPrim.Prim.ModelTests       Grisette.SymPrim.Prim.NumTests       Grisette.SymPrim.Prim.TabularFunTests+      Grisette.SymPrim.SomeBVTests       Grisette.SymPrim.SymPrimTests       Grisette.SymPrim.TabularFunTests       Grisette.TestUtil.NoMerge@@ -284,7 +293,7 @@   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   build-depends:       HUnit ==1.6.*-    , QuickCheck ==2.14.*+    , QuickCheck >=2.14 && <2.16     , array >=0.5.4 && <0.6     , async >=2.2.2 && <2.3     , base >=4.14 && <5@@ -299,9 +308,9 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <11+    , sbv >=8.17 && <11     , stm ==2.5.*-    , template-haskell >=2.16 && <2.22+    , template-haskell >=2.16 && <2.23     , test-framework >=0.8.2 && <0.9     , test-framework-hunit >=0.3.0.2 && <0.4     , test-framework-quickcheck2 >=0.3.0.5 && <0.4

@@ -24,7 +24,9 @@     -- * SBV backend solver configuration     SBV.SMTConfig (..),     SBV.boolector,+    SBV.bitwuzla,     SBV.cvc4,+    SBV.cvc5,     SBV.yices,     SBV.dReal,     SBV.z3,

@@ -177,6 +177,7 @@     identifier,     withInfo,     withLoc,+    uniqueIdentifier,     slocsym,     ilocsym,     simple,@@ -962,27 +963,47 @@     -- ** Solver interfaces     SolvingFailure (..),     MonadicSolver (..),+    monadicSolverSolve,     SolverCommand (..),     ConfigurableSolver (..),     Solver (..),+    solverSolve,     withSolver,     solve,+    solverSolveMulti,     solveMulti,      -- ** Union with exceptions     UnionWithExcept (..),+    solverSolveExcept,     solveExcept,+    solverSolveMultiExcept,     solveMultiExcept,      -- ** Generic Counter-example Guided Inductive Synthesis (CEGIS) interface-    SynthesisConstraintFun,     VerifierResult (..),-    StatefulVerifierFun,+    SynthesisConstraintFun,+    VerifierFun,     CEGISResult (..),+    solverGenericCEGIS,+    solverGenericCEGISWithRefinement,     genericCEGIS,+    genericCEGISWithRefinement,      -- ** CEGIS interfaces with pre/post conditions     CEGISCondition (..),+    solverCegisMultiInputs,+    solverCegis,+    solverCegisExcept,+    solverCegisExceptStdVC,+    solverCegisExceptVC,+    solverCegisExceptMultiInputs,+    solverCegisExceptStdVCMultiInputs,+    solverCegisExceptVCMultiInputs,+    solverCegisForAll,+    solverCegisForAllExcept,+    solverCegisForAllExceptStdVC,+    solverCegisForAllExceptVC,     cegisPostCond,     cegisPrePost,     cegisMultiInputs,@@ -1073,8 +1094,8 @@ import Grisette.Internal.Core.Data.Class.CEGISSolver   ( CEGISCondition (..),     CEGISResult (..),-    StatefulVerifierFun,     SynthesisConstraintFun,+    VerifierFun,     VerifierResult (..),     cegis,     cegisExcept,@@ -1091,6 +1112,21 @@     cegisPostCond,     cegisPrePost,     genericCEGIS,+    genericCEGISWithRefinement,+    solverCegis,+    solverCegisExcept,+    solverCegisExceptMultiInputs,+    solverCegisExceptStdVC,+    solverCegisExceptStdVCMultiInputs,+    solverCegisExceptVC,+    solverCegisExceptVCMultiInputs,+    solverCegisForAll,+    solverCegisForAllExcept,+    solverCegisForAllExceptStdVC,+    solverCegisForAllExceptVC,+    solverCegisMultiInputs,+    solverGenericCEGIS,+    solverGenericCEGISWithRefinement,   ) import Grisette.Internal.Core.Data.Class.Error   ( TransformError (..),@@ -1212,10 +1248,15 @@     SolverCommand (..),     SolvingFailure (..),     UnionWithExcept (..),+    monadicSolverSolve,     solve,     solveExcept,     solveMulti,     solveMultiExcept,+    solverSolve,+    solverSolveExcept,+    solverSolveMulti,+    solverSolveMultiExcept,     withSolver,   ) import Grisette.Internal.Core.Data.Class.SubstituteSym@@ -1246,6 +1287,7 @@     identifier,     indexed,     simple,+    uniqueIdentifier,     withInfo,     withLoc,   )

@@ -88,23 +88,42 @@     lookupTerm,     sizeBiMap,   )-import Grisette.Internal.Core.Data.Class.ModelOps (ModelOps (emptyModel, insertValue))+import Grisette.Internal.Core.Data.Class.ModelOps+  ( ModelOps (emptyModel, insertValue),+  ) import Grisette.Internal.Core.Data.Class.Solver   ( ConfigurableSolver (newSolver),     MonadicSolver-      ( monadicSolverPop,+      ( monadicSolverAssert,+        monadicSolverCheckSat,+        monadicSolverPop,         monadicSolverPush,-        monadicSolverSolve+        monadicSolverResetAssertions       ),     Solver-      ( solverForceTerminate,+      ( solverCheckSat,+        solverForceTerminate,         solverRunCommand,-        solverSolve,         solverTerminate       ),-    SolverCommand (SolverPop, SolverPush, SolverSolve, SolverTerminate),+    SolverCommand+      ( SolverAssert,+        SolverCheckSat,+        SolverPop,+        SolverPush,+        SolverResetAssertions,+        SolverTerminate+      ),     SolvingFailure (SolvingError, Terminated, Unk, Unsat),   )+import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP+  ( sbvFPBinaryTerm,+    sbvFPFMATerm,+    sbvFPRoundingBinaryTerm,+    sbvFPRoundingUnaryTerm,+    sbvFPTraitTerm,+    sbvFPUnaryTerm,+  ) import Grisette.Internal.SymPrim.Prim.Internal.IsZero (KnownIsZero) import Grisette.Internal.SymPrim.Prim.Internal.Term   ( PEvalApplyTerm (sbvApplyTerm),@@ -122,6 +141,8 @@         sbvQuotIntegralTerm,         sbvRemIntegralTerm       ),+    PEvalFloatingTerm (sbvSqrtTerm),+    PEvalFractionalTerm (sbvFdivTerm, sbvRecipTerm),     PEvalNumTerm       ( sbvAbsNumTerm,         sbvAddNumTerm,@@ -157,6 +178,13 @@         ConTerm,         DivIntegralTerm,         EqTerm,+        FPBinaryTerm,+        FPFMATerm,+        FPRoundingBinaryTerm,+        FPRoundingUnaryTerm,+        FPTraitTerm,+        FPUnaryTerm,+        FdivTerm,         ITETerm,         LeOrdTerm,         LtOrdTerm,@@ -167,12 +195,14 @@         OrBitsTerm,         OrTerm,         QuotIntegralTerm,+        RecipTerm,         RemIntegralTerm,         RotateLeftTerm,         RotateRightTerm,         ShiftLeftTerm,         ShiftRightTerm,         SignumNumTerm,+        SqrtTerm,         SymTerm,         ToSignedTerm,         ToUnsignedTerm,@@ -384,19 +414,23 @@           runReaderT sbvIncrementalT config  instance (MonadIO m) => MonadicSolver (SBVIncrementalT n m) where-  monadicSolverSolve (SymBool formula) = do+  monadicSolverAssert (SymBool formula) = do     symBiMap <- get     config <- ask     (newSymBiMap, lowered) <- lowerSinglePrimCached config formula symBiMap     lift $ lift $ SBV.constrain lowered     put newSymBiMap+  monadicSolverCheckSat = do     checkSatResult <- SBVTC.checkSat+    config <- ask+    symBiMap <- get     case checkSatResult of       SBVC.Sat -> do         sbvModel <- SBVTC.getModel-        let model = parseModel config sbvModel newSymBiMap+        let model = parseModel config sbvModel symBiMap         return $ Right model       r -> return $ Left $ sbvCheckSatResult r+  monadicSolverResetAssertions = SBVTC.resetAssertions   monadicSolverPush = SBVTC.push   monadicSolverPop = SBVTC.pop @@ -435,8 +469,12 @@                 SolverPush n -> monadicSolverPush n >> loop                 SolverPop n -> monadicSolverPop n >> loop                 SolverTerminate -> return ()-                SolverSolve formula -> do-                  r <- monadicSolverSolve formula+                SolverResetAssertions -> monadicSolverResetAssertions >> loop+                SolverAssert formula -> do+                  monadicSolverAssert formula+                  loop+                SolverCheckSat -> do+                  r <- monadicSolverCheckSat                   liftIO $ atomically $ writeTChan sbvSolverHandleOutChan r                   loop         loop@@ -461,13 +499,13 @@       SBVSolverTerminated -> do         liftIO $ atomically $ setTerminated status         return $ Left Terminated-  solverSolve handle nextFormula =+  solverCheckSat handle =     solverRunCommand       ( \(SBVSolverHandle _ _ _ outChan) ->           liftIO $ atomically $ readTChan outChan       )       handle-      $ SolverSolve nextFormula+      SolverCheckSat   solverTerminate (SBVSolverHandle thread status inChan _) = do     liftIO $ atomically $ do       setTerminated status@@ -658,6 +696,41 @@   (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  #if MIN_VERSION_sbv(10,3,0)

@@ -0,0 +1,47 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++module Grisette.Internal.Core.Data.Class.BitCast (BitCast (..)) where++import Control.Monad.ST (ST, runST)+import Data.Array.ST (MArray (newArray), STUArray, readArray)+import Data.Array.Unsafe (castSTUArray)+import Data.Int (Int32, Int64)+import Data.Word (Word32, Word64)++class BitCast from to where+  bitCast :: from -> to++#define BITCAST_WITH_MARRAY(from, to) \+instance BitCast from to where \+  bitCast x = runST $ bitcastWithMArray x; \+  {-# INLINE bitCast #-}++#if 1+BITCAST_WITH_MARRAY(Int64, Double)+BITCAST_WITH_MARRAY(Double, Int64)+BITCAST_WITH_MARRAY(Word64, Double)+BITCAST_WITH_MARRAY(Double, Word64)+BITCAST_WITH_MARRAY(Word64, Int64)+BITCAST_WITH_MARRAY(Int64, Word64)+BITCAST_WITH_MARRAY(Int32, Float)+BITCAST_WITH_MARRAY(Float, Int32)+BITCAST_WITH_MARRAY(Word32, Float)+BITCAST_WITH_MARRAY(Float, Word32)+BITCAST_WITH_MARRAY(Word32, Int32)+BITCAST_WITH_MARRAY(Int32, Word32)+#endif++{-# INLINE bitcastWithMArray #-}+bitcastWithMArray ::+  ( MArray (STUArray s) a (ST s),+    MArray (STUArray s) b (ST s)+  ) =>+  a ->+  ST s b+bitcastWithMArray x =+  newArray (0 :: Int, 0) x >>= castSTUArray >>= flip readArray 0

@@ -25,16 +25,31 @@     -- solver is available in @PATH@.      -- * Generic CEGIS interface-    SynthesisConstraintFun,     VerifierResult (..),-    StatefulVerifierFun,+    SynthesisConstraintFun,+    VerifierFun,     CEGISResult (..),+    solverGenericCEGIS,+    solverGenericCEGISWithRefinement,     genericCEGIS,+    genericCEGISWithRefinement,      -- * CEGIS interfaces with pre/post conditions     CEGISCondition (..),     cegisPostCond,     cegisPrePost,+    solverCegisMultiInputs,+    solverCegis,+    solverCegisExcept,+    solverCegisExceptStdVC,+    solverCegisExceptVC,+    solverCegisExceptMultiInputs,+    solverCegisExceptStdVCMultiInputs,+    solverCegisExceptVCMultiInputs,+    solverCegisForAll,+    solverCegisForAllExcept,+    solverCegisForAllExceptStdVC,+    solverCegisForAllExceptVC,     cegisMultiInputs,     cegis,     cegisExcept,@@ -50,7 +65,6 @@   ) where -import Control.Monad (foldM, unless) import Data.List (partition) import GHC.Generics (Generic) import Generics.Deriving (Default (Default))@@ -79,14 +93,15 @@ import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con)) import Grisette.Internal.Core.Data.Class.Solver   ( ConfigurableSolver,-    Solver (solverSolve),+    Solver (solverResetAssertions),     SolvingFailure (Unsat),     UnionWithExcept (extractUnionExcept),-    solve,+    solverSolve,     withSolver,   ) import Grisette.Internal.SymPrim.Prim.Model (Model) import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Lib.Data.Foldable (symAll)  -- $setup -- >>> import Grisette.Core@@ -94,31 +109,23 @@ -- >>> import Grisette.SymPrim -- >>> import Grisette.Backend --- | Synthesis constraint function.------ The first argument is the iteration number, for angelic programs, you can use--- it to instantiate the angelic variables in the program.------ The second argument is the counter-example generated by the verifier.------ The synthesizer will try to find a program that is true for all the synthesis--- constraints.-type SynthesisConstraintFun input = Int -> input -> IO SymBool---- | The result of the verifier.-data VerifierResult input exception-  = CEGISVerifierFoundCex input+-- | The response from a verifier.+data VerifierResult cex exception+  = CEGISVerifierFoundCex cex   | CEGISVerifierNoCex   | CEGISVerifierException exception --- | The verifier function.------ The first argument is the state of the verifier.------ The second argument is the candidate model proposed by the synthesizer.-type StatefulVerifierFun state input exception =-  state -> Model -> IO (state, VerifierResult input exception)+-- | Build the synthesizer constraint from the verfication result. The first+-- argument will be guaranteed to be distinct during each invocation of the+-- function in the CEGIS algorithm, so it can be used to instantiate the+-- identifiers for fresh variables.+type SynthesisConstraintFun cex = cex -> IO SymBool +-- | The verifier.+type VerifierFun cex exception = Model -> IO (VerifierResult cex exception)++type RefinementConditionFun = Model -> IO SymBool+ -- | The result of the CEGIS procedure. data CEGISResult exception   = CEGISSuccess Model@@ -126,51 +133,152 @@   | CEGISSolverFailure SolvingFailure   deriving (Show) --- | Generic CEGIS procedure.+-- | Generic CEGIS procedure. See 'genericCEGIS' for more details. ----- The CEGIS procedure will try to find a model that satisfies the initial--- synthesis constraint, and satisfies all the inputs generated by the verifier.-genericCEGIS ::-  (ConfigurableSolver config handle) =>+-- The difference from 'genericCEGIS' is that this function accepts a solver+-- handle for the synthesizer, instead of a solver configuration.+solverGenericCEGIS ::+  (Solver handle) =>   -- | Configuration of the solver.-  config ->+  handle ->+  -- | Whether we should rerun the passed verifiers if any other verifier found+  -- a counter-example.+  Bool ->   -- | The initial synthesis constraint.   SymBool ->-  -- | The synthesis constraint function.+  -- | Synthesis constraint from counter-examples   SynthesisConstraintFun input ->-  -- | The initial state of the verifier.-  verifierState ->-  -- | The verifier function.-  StatefulVerifierFun verifierState input exception ->+  -- | The verifier functions.+  [VerifierFun input exception] ->   IO ([input], CEGISResult exception)-genericCEGIS config initConstr synthConstr initVerifierState verifier =-  withSolver config $ \solver -> do-    firstResult <- solverSolve solver initConstr-    case firstResult of-      Left err -> return ([], CEGISSolverFailure err)-      Right model -> go solver model 0 initVerifierState+solverGenericCEGIS solver rerun initConstr synthConstr verifiers = do+  firstResult <- solverSolve solver initConstr+  case firstResult of+    Left err -> return ([], CEGISSolverFailure err)+    Right model -> go model False verifiers   where-    go solver prevModel iterNum verifierState = do-      (newVerifierState, verifierResult) <--        verifier verifierState prevModel+    go prevModel needRerun (verifier : remainingVerifiers) = do+      verifierResult <- verifier prevModel       case verifierResult of         CEGISVerifierFoundCex cex -> do-          newResult <- solverSolve solver =<< synthConstr iterNum cex+          newResult <- solverSolve solver =<< synthConstr cex           case newResult of             Left err -> return ([], CEGISSolverFailure err)             Right model -> do-              (cexes, result) <- go solver model (iterNum + 1) newVerifierState+              (cexes, result) <-+                go model (needRerun || rerun) $+                  verifier : remainingVerifiers               return (cex : cexes, result)-        CEGISVerifierNoCex -> return ([], CEGISSuccess prevModel)+        CEGISVerifierNoCex -> go prevModel needRerun remainingVerifiers         CEGISVerifierException exception ->           return ([], CEGISVerifierFailure exception)+    go prevModel False [] = return ([], CEGISSuccess prevModel)+    go prevModel True [] = go prevModel False verifiers -data CEGISMultiInputsState input = CEGISMultiInputsState-  { _cegisMultiInputsRemainingSymInputs :: [input],-    _cegisMultiInputsPre :: SymBool,-    _cegisMultiInputsPost :: SymBool-  }+-- | Generic CEGIS procedure with refinement. See 'genericCEGISWithRefinement'+-- for more details.+--+-- The difference from 'genericCEGISWithRefinement' is that this function+-- accepts a solver handle for the synthesizer, instead of a solver+-- configuration.+solverGenericCEGISWithRefinement ::+  (Solver handle) =>+  -- | Configuration of the solver.+  handle ->+  -- | Whether we should rerun the passed verifiers if any other verifier found+  -- a counter-example.+  Bool ->+  -- | The initial synthesis constraint.+  SymBool ->+  -- | Synthesis constraint from counter-examples+  SynthesisConstraintFun input ->+  -- | Refinement condition generator.+  Maybe RefinementConditionFun ->+  -- | The verifier functions.+  [VerifierFun input exception] ->+  IO ([input], CEGISResult exception)+solverGenericCEGISWithRefinement+  solver+  rerun+  initConstr+  synthConstr+  refineCond+  verifiers = do+    (input, r) <-+      solverGenericCEGIS solver rerun initConstr synthConstr verifiers+    case r of+      CEGISSuccess model -> refine solver input model+      _ -> return (input, r)+    where+      refine solver input model = case refineCond of+        Just f -> do+          cond <- f model+          newResult <-+            solverGenericCEGIS solver rerun cond synthConstr verifiers+          case newResult of+            (newInputs, CEGISSuccess model) ->+              refine solver (input ++ newInputs) model+            _ -> return (input, CEGISSuccess model)+        Nothing -> return (input, CEGISSuccess model) +-- | Generic CEGIS procedure.+--+-- The CEGIS procedure will try to find a model that satisfies the initial+-- synthesis constraint, and satisfies all the inputs generated by the verifier.+genericCEGIS ::+  (ConfigurableSolver config handle) =>+  -- | Configuration of the solver.+  config ->+  -- | Whether we should rerun the passed verifiers if any other verifier found+  -- a counter-example.+  Bool ->+  -- | The initial synthesis constraint.+  SymBool ->+  -- | Synthesis constraint from counter-examples+  SynthesisConstraintFun input ->+  -- | The verifier functions.+  [VerifierFun input exception] ->+  IO ([input], CEGISResult exception)+genericCEGIS config rerun initConstr synthConstr verifier =+  withSolver config $ \solver ->+    solverGenericCEGIS solver rerun initConstr synthConstr verifier++-- | Generic CEGIS procedure.+--+-- The CEGIS procedure will try to find a model that satisfies the initial+-- synthesis constraint, and satisfies all the inputs generated by the verifier.+genericCEGISWithRefinement ::+  (ConfigurableSolver config handle) =>+  -- | Configuration of the solver.+  config ->+  -- | Whether we should rerun the passed verifiers if any other verifier found+  -- a counter-example.+  Bool ->+  -- | The initial synthesis constraint.+  SymBool ->+  -- | Synthesis constraint from counter-examples+  SynthesisConstraintFun input ->+  -- | Refinement condition generator.+  Maybe RefinementConditionFun ->+  -- | The verifier functions.+  [VerifierFun input exception] ->+  IO ([input], CEGISResult exception)+genericCEGISWithRefinement+  config+  rerun+  initConstr+  synthConstr+  refineCond+  verifier =+    withSolver config $ \solver -> do+      solverGenericCEGISWithRefinement+        solver+        rerun+        initConstr+        synthConstr+        refineCond+        verifier+ -- | The condition for CEGIS to solve. -- -- The first argument is the pre-condition, and the second argument is the@@ -206,7 +314,443 @@  deriving via (Default CEGISCondition) instance SimpleMergeable CEGISCondition +-- | CEGIS with multiple (possibly symbolic) inputs. See 'cegisMultiInputs' for+-- more details.+--+-- The difference from 'cegisMultiInputs' is that this function accepts two+-- solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisMultiInputs ::+  ( EvaluateSym input,+    ExtractSymbolics input,+    Solver handle+  ) =>+  -- The synthesizer solver handle+  handle ->+  -- The verifier solver handle+  handle ->+  -- | Initial symbolic inputs. The solver will try to find a+  -- program that works on all the inputs representable by these inputs (see+  -- 'CEGISCondition').+  [input] ->+  -- | The condition for the solver to solve. All the+  -- symbolic constants that are not in the inputs will+  -- be considered as part of the symbolic program.+  (input -> CEGISCondition) ->+  -- | The counter-examples generated+  -- during the CEGIS loop, and the+  -- model found by the solver.+  IO ([input], CEGISResult SolvingFailure)+solverCegisMultiInputs+  synthesizerSolver+  verifierSolver+  inputs+  toCEGISCondition = do+    solverGenericCEGIS+      synthesizerSolver+      True+      (symAll cexAssertFun conInputs)+      (return . cexAssertFun)+      $ getVerifier <$> symInputs+    where+      cexAssertFun input =+        case toCEGISCondition input of+          CEGISCondition pre post -> pre .&& post+      getVerifier input md = do+        let CEGISCondition pre post = toCEGISCondition input+        let evaluated =+              evaluateSym False (exceptFor (extractSymbolics input) md) $+                pre .&& symNot post+        solverResetAssertions verifierSolver+        r <- solverSolve verifierSolver evaluated+        case r of+          Left Unsat -> return CEGISVerifierNoCex+          Left err -> return $ CEGISVerifierException err+          Right model -> do+            let newCexInput =+                  evaluateSym True (exact (extractSymbolics input) model) input+            return $ CEGISVerifierFoundCex newCexInput+      (conInputs, symInputs) = partition (isEmptySet . extractSymbolics) inputs++-- | CEGIS with a single symbolic input to represent a set of inputs. See+-- 'cegis' for more details.+--+-- The difference from 'cegis' is that this function accepts two solver handles,+-- one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegis ::+  ( Solver handle,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    SEq inputs+  ) =>+  -- | The synthesizer solver handle+  handle ->+  -- | The verifier solver handle+  handle ->+  -- | Initial symbolic inputs. The solver will try to find a+  -- program that works on all the inputs representable by it (see+  -- 'CEGISCondition').+  inputs ->+  -- | The condition for the solver to solve. All the+  -- symbolic constants that are not in the inputs will+  -- be considered as part of the symbolic program.+  (inputs -> CEGISCondition) ->+  -- | The counter-examples generated+  -- during the CEGIS loop, and the+  -- model found by the solver.+  IO ([inputs], CEGISResult SolvingFailure)+solverCegis synthesizerSolver verifierSolver inputs =+  solverCegisMultiInputs synthesizerSolver verifierSolver [inputs]+ -- |+-- CEGIS for symbolic programs with error handling, using multiple (possibly+-- symbolic) inputs to represent a set of inputs.+--+-- The difference from 'cegisExceptMultiInputs' is that this function accepts+-- two solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisExceptMultiInputs ::+  ( Solver handle,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    UnionWithExcept t u e v,+    PlainUnion u,+    Monad u+  ) =>+  handle ->+  handle ->+  [inputs] ->+  (Either e v -> CEGISCondition) ->+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+solverCegisExceptMultiInputs+  synthesizerSolver+  verifierSolver+  cexes+  interpretFun+  f =+    solverCegisMultiInputs+      synthesizerSolver+      verifierSolver+      cexes+      (simpleMerge . (interpretFun <$>) . extractUnionExcept . f)++-- |+-- CEGIS for symbolic programs with error handling, using multiple (possibly+-- symbolic) inputs to represent a set of inputs.+--+-- The errors should be translated to assertion or assumption violations.+--+-- The difference from 'cegisExceptVCMultiInputs' is that this function accepts+-- two solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisExceptVCMultiInputs ::+  ( Solver handle,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    UnionWithExcept t u e v,+    PlainUnion u,+    Monad u+  ) =>+  handle ->+  handle ->+  [inputs] ->+  (Either e v -> u (Either VerificationConditions ())) ->+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+solverCegisExceptVCMultiInputs+  synthesizerSolver+  verifierSolver+  cexes+  interpretFun+  f =+    solverCegisMultiInputs+      synthesizerSolver+      verifierSolver+      cexes+      ( \v ->+          simpleMerge+            ( ( \case+                  Left AssumptionViolation ->+                    cegisPrePost (con False) (con True)+                  Left AssertionViolation -> cegisPostCond (con False)+                  _ -> cegisPostCond (con True)+              )+                <$> (extractUnionExcept (f v) >>= interpretFun)+            )+      )++-- |+-- CEGIS for symbolic programs with error handling, using multiple (possibly+-- symbolic) inputs to represent a set of inputs. See+-- 'cegisExceptStdVCMultiInputs' for more details.+--+-- The difference from 'cegisExceptStdVCMultiInputs' is that this function+-- accepts two solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisExceptStdVCMultiInputs ::+  ( Solver handle,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    UnionWithExcept t u VerificationConditions (),+    PlainUnion u,+    Monad u+  ) =>+  handle ->+  handle ->+  [inputs] ->+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+solverCegisExceptStdVCMultiInputs synthesizerSolver verifierSolver cexes =+  solverCegisExceptVCMultiInputs synthesizerSolver verifierSolver cexes return++-- |+-- CEGIS for symbolic programs with error handling, using a single symbolic+-- input to represent a set of inputs. See 'cegisExcept' for more details.+--+-- The difference from 'cegisExcept' is that this function accepts two solver+-- handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisExcept ::+  ( UnionWithExcept t u e v,+    PlainUnion u,+    Functor u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    Solver handle,+    SEq inputs+  ) =>+  handle ->+  handle ->+  inputs ->+  (Either e v -> CEGISCondition) ->+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+solverCegisExcept synthesizerSolver verifierSolver inputs f v =+  solverCegis synthesizerSolver verifierSolver inputs $+    \i -> simpleMerge $ f <$> extractUnionExcept (v i)++-- |+-- CEGIS for symbolic programs with error handling, using a single symbolic+-- input to represent a set of inputs.+--+-- The errors should be translated to assertion or assumption violations.+--+-- The difference from 'cegisExceptVC' is that this function accepts two solver+-- handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisExceptVC ::+  ( UnionWithExcept t u e v,+    PlainUnion u,+    Monad u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    Solver handle,+    SEq inputs+  ) =>+  handle ->+  handle ->+  inputs ->+  (Either e v -> u (Either VerificationConditions ())) ->+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+solverCegisExceptVC synthesizerSolver verifierSolver inputs f v = do+  solverCegis synthesizerSolver verifierSolver inputs $ \i ->+    simpleMerge $+      ( \case+          Left AssumptionViolation -> cegisPrePost (con False) (con True)+          Left AssertionViolation -> cegisPostCond (con False)+          _ -> cegisPostCond (con True)+      )+        <$> (extractUnionExcept (v i) >>= f)++-- |+-- CEGIS for symbolic programs with error handling, using a single symbolic+-- input to represent a set of inputs. See 'cegisExceptStdVC' for more details.+--+-- The difference from 'cegisExceptStdVC' is that this function accepts two+-- solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisExceptStdVC ::+  ( UnionWithExcept t u VerificationConditions (),+    PlainUnion u,+    Monad u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    Solver handle,+    SEq inputs+  ) =>+  handle ->+  handle ->+  inputs ->+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+solverCegisExceptStdVC synthesizerSolver verifierSolver inputs =+  solverCegisExceptVC synthesizerSolver verifierSolver inputs return++-- |+-- CEGIS with a single symbolic input to represent a set of inputs. See+-- 'cegisForAll' for more details.+--+-- The difference from 'cegisForAll' is that this function accepts two solver+-- handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisForAll ::+  ( ExtractSymbolics forallInput,+    Solver handle+  ) =>+  handle ->+  handle ->+  -- | A symbolic value. All the symbolic constants in the value are treated as+  -- for-all variables.+  forallInput ->+  CEGISCondition ->+  -- | First output are the counter-examples for all the for-all variables, and+  -- the second output is the model for all other variables if CEGIS succeeds.+  IO ([Model], CEGISResult SolvingFailure)+solverCegisForAll+  synthesizerSolver+  verifierSolver+  input+  (CEGISCondition pre post) = do+    (models, result) <-+      solverGenericCEGIS+        synthesizerSolver+        False+        phi+        (\md -> return $ evaluateSym False md phi)+        [verifier]+    let exactResult = case result of+          CEGISSuccess model -> CEGISSuccess $ exceptFor forallSymbols model+          _ -> result+    return (models, exactResult)+    where+      phi = pre .&& post+      negphi = pre .&& symNot post+      forallSymbols = extractSymbolics input+      verifier candidate = do+        let evaluated =+              evaluateSym False (exceptFor forallSymbols candidate) negphi+        solverResetAssertions verifierSolver+        r <- solverSolve verifierSolver evaluated+        case r of+          Left Unsat -> return CEGISVerifierNoCex+          Left err -> return $ CEGISVerifierException err+          Right model ->+            return $ CEGISVerifierFoundCex (exact forallSymbols model)++-- |+-- CEGIS for symbolic programs with error handling, with a forall variable.+--+-- See 'cegisForAllExcept', 'cegisForAll' and 'cegisExcept'.+--+-- The difference from 'cegisForAllExcept' is that this function accepts two+-- solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisForAllExcept ::+  ( UnionWithExcept t u e v,+    PlainUnion u,+    Functor u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    Solver handle,+    SEq inputs+  ) =>+  handle ->+  handle ->+  inputs ->+  (Either e v -> CEGISCondition) ->+  t ->+  IO ([Model], CEGISResult SolvingFailure)+solverCegisForAllExcept synthesizerSolver verifierSolver inputs f v =+  solverCegisForAll synthesizerSolver verifierSolver inputs $+    simpleMerge $+      f <$> extractUnionExcept v++-- |+-- CEGIS for symbolic programs with error handling, with a forall variable.+--+-- See 'cegisForAllExceptVC' 'cegisForAll' and 'cegisExceptVC'.+--+-- The difference from 'cegisForAllExceptVC' is that this function accepts two+-- solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisForAllExceptVC ::+  ( UnionWithExcept t u e v,+    PlainUnion u,+    Monad u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    Solver handle,+    SEq inputs+  ) =>+  handle ->+  handle ->+  inputs ->+  (Either e v -> u (Either VerificationConditions ())) ->+  t ->+  IO ([Model], CEGISResult SolvingFailure)+solverCegisForAllExceptVC synthesizerSolver verifierSolver inputs f v = do+  solverCegisForAll synthesizerSolver verifierSolver inputs $+    simpleMerge $+      ( \case+          Left AssumptionViolation -> cegisPrePost (con False) (con True)+          Left AssertionViolation -> cegisPostCond (con False)+          _ -> cegisPostCond (con True)+      )+        <$> (extractUnionExcept v >>= f)++-- |+-- CEGIS for symbolic programs with error handling, with a forall variable.+--+-- See 'cegisForAllExceptStdVC' 'cegisForAll' and 'cegisExceptStdVC'.+--+-- The difference from 'cegisForAllExceptStdVC' is that this function accepts+-- two solver handles, one for the synthesizer and one for the verifier.+--+-- The synthesizer solver will **not** be reset, while the verifier solver will+-- be reset after each iteration.+solverCegisForAllExceptStdVC ::+  ( UnionWithExcept t u VerificationConditions (),+    PlainUnion u,+    Monad u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    Solver handle,+    SEq inputs+  ) =>+  handle ->+  handle ->+  inputs ->+  t ->+  IO ([Model], CEGISResult SolvingFailure)+solverCegisForAllExceptStdVC synthesizerSolver verifierSolver inputs =+  solverCegisForAllExceptVC synthesizerSolver verifierSolver inputs return++-- | -- CEGIS with multiple (possibly symbolic) inputs. Solves the following formula -- (see 'CEGISCondition' for details). --@@ -222,54 +766,28 @@     ExtractSymbolics input,     ConfigurableSolver config handle   ) =>+  -- | The configuration of the solver   config ->+  -- | Initial symbolic inputs. The solver will try to find a+  -- program that works on all the inputs representable by these inputs (see+  -- 'CEGISCondition').   [input] ->+  -- | The condition for the solver to solve. All the+  -- symbolic constants that are not in the inputs will+  -- be considered as part of the symbolic program.   (input -> CEGISCondition) ->+  -- | The counter-examples generated+  -- during the CEGIS loop, and the+  -- model found by the solver.   IO ([input], CEGISResult SolvingFailure)-cegisMultiInputs config inputs toCEGISCondition = do-  initConstr <- cexesAssertFun conInputs-  genericCEGIS-    config-    initConstr-    synthConstr-    (CEGISMultiInputsState symInputs (con True) (con True))-    verifier-  where-    (conInputs, symInputs) = partition (isEmptySet . extractSymbolics) inputs-    forallSymbols = extractSymbolics symInputs-    cexAssertFun input = do-      unless (isEmptySet (extractSymbolics input)) $ error "BUG"-      CEGISCondition pre post <- return $ toCEGISCondition input-      return $ pre .&& post-    cexesAssertFun = foldM (\acc x -> (acc .&&) <$> cexAssertFun x) (con True)-    synthConstr _ = cexAssertFun-    verifier state@(CEGISMultiInputsState [] _ _) _ =-      return (state, CEGISVerifierNoCex)-    verifier-      (CEGISMultiInputsState (nextSymInput : symInputs) pre post)-      candidate = do-        CEGISCondition nextPre nextPost <--          return $ toCEGISCondition nextSymInput-        let newPre = pre .&& nextPre-        let newPost = post .&& nextPost-        let evaluated =-              evaluateSym False (exceptFor forallSymbols candidate) $-                newPre .&& symNot newPost-        r <- solve config evaluated-        case r of-          Left Unsat ->-            verifier (CEGISMultiInputsState symInputs newPre newPost) candidate-          Left err ->-            return-              ( CEGISMultiInputsState [] newPre newPost,-                CEGISVerifierException err-              )-          Right model ->-            return-              ( CEGISMultiInputsState (nextSymInput : symInputs) newPre newPost,-                CEGISVerifierFoundCex $-                  evaluateSym False (exact forallSymbols model) nextSymInput-              )+cegisMultiInputs config inputs toCEGISCondition =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisMultiInputs+        synthesizerSolver+        verifierSolver+        inputs+        toCEGISCondition  -- | -- CEGIS with a single symbolic input to represent a set of inputs.@@ -302,7 +820,10 @@   -- during the CEGIS loop, and the   -- model found by the solver.   IO ([inputs], CEGISResult SolvingFailure)-cegis config inputs = cegisMultiInputs config [inputs]+cegis config inputs condition =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegis synthesizerSolver verifierSolver inputs condition  -- | -- CEGIS for symbolic programs with error handling, using multiple (possibly@@ -321,10 +842,14 @@   (inputs -> t) ->   IO ([inputs], CEGISResult SolvingFailure) cegisExceptMultiInputs config cexes interpretFun f =-  cegisMultiInputs-    config-    cexes-    (simpleMerge . (interpretFun <$>) . extractUnionExcept . f)+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisExceptMultiInputs+        synthesizerSolver+        verifierSolver+        cexes+        interpretFun+        f  -- | -- CEGIS for symbolic programs with error handling, using multiple (possibly@@ -345,19 +870,14 @@   (inputs -> t) ->   IO ([inputs], CEGISResult SolvingFailure) cegisExceptVCMultiInputs config cexes interpretFun f =-  cegisMultiInputs-    config-    cexes-    ( \v ->-        simpleMerge-          ( ( \case-                Left AssumptionViolation -> cegisPrePost (con False) (con True)-                Left AssertionViolation -> cegisPostCond (con False)-                _ -> cegisPostCond (con True)-            )-              <$> (extractUnionExcept (f v) >>= interpretFun)-          )-    )+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisExceptVCMultiInputs+        synthesizerSolver+        verifierSolver+        cexes+        interpretFun+        f  -- | -- CEGIS for symbolic programs with error handling, using multiple (possibly@@ -380,8 +900,10 @@   [inputs] ->   (inputs -> t) ->   IO ([inputs], CEGISResult SolvingFailure)-cegisExceptStdVCMultiInputs config cexes =-  cegisExceptVCMultiInputs config cexes return+cegisExceptStdVCMultiInputs config cexes f =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisExceptStdVCMultiInputs synthesizerSolver verifierSolver cexes f  -- | -- CEGIS for symbolic programs with error handling, using a single symbolic@@ -430,7 +952,9 @@   (inputs -> t) ->   IO ([inputs], CEGISResult SolvingFailure) cegisExcept config inputs f v =-  cegis config inputs $ \i -> simpleMerge $ f <$> extractUnionExcept (v i)+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisExcept synthesizerSolver verifierSolver inputs f v  -- | -- CEGIS for symbolic programs with error handling, using a single symbolic@@ -451,15 +975,10 @@   (Either e v -> u (Either VerificationConditions ())) ->   (inputs -> t) ->   IO ([inputs], CEGISResult SolvingFailure)-cegisExceptVC config inputs f v = do-  cegis config inputs $ \i ->-    simpleMerge $-      ( \case-          Left AssumptionViolation -> cegisPrePost (con False) (con True)-          Left AssertionViolation -> cegisPostCond (con False)-          _ -> cegisPostCond (con True)-      )-        <$> (extractUnionExcept (v i) >>= f)+cegisExceptVC config inputs f v =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisExceptVC synthesizerSolver verifierSolver inputs f v  -- | -- CEGIS for symbolic programs with error handling, using a single symbolic@@ -501,7 +1020,10 @@   inputs ->   (inputs -> t) ->   IO ([inputs], CEGISResult SolvingFailure)-cegisExceptStdVC config inputs = cegisExceptVC config inputs return+cegisExceptStdVC config inputs f =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisExceptStdVC synthesizerSolver verifierSolver inputs f  -- | -- CEGIS with a single symbolic input to represent a set of inputs.@@ -526,26 +1048,14 @@   -- | First output are the counter-examples for all the for-all variables, and   -- the second output is the model for all other variables if CEGIS succeeds.   IO ([Model], CEGISResult SolvingFailure)-cegisForAll config input (CEGISCondition pre post) = do-  (models, result) <- genericCEGIS config phi synthConstr () verifier-  let exactResult = case result of-        CEGISSuccess model -> CEGISSuccess $ exceptFor forallSymbols model-        _ -> result-  return (models, exactResult)-  where-    phi = pre .&& post-    negphi = pre .&& symNot post-    forallSymbols = extractSymbolics input-    synthConstr _ model = return $ evaluateSym False model phi-    verifier () candidate = do-      let evaluated =-            evaluateSym False (exceptFor forallSymbols candidate) negphi-      r <- solve config evaluated-      case r of-        Left Unsat -> return ((), CEGISVerifierNoCex)-        Left err -> return ((), CEGISVerifierException err)-        Right model ->-          return ((), CEGISVerifierFoundCex $ exact forallSymbols model)+cegisForAll config input (CEGISCondition pre post) =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisForAll+        synthesizerSolver+        verifierSolver+        input+        (CEGISCondition pre post)  -- | -- CEGIS for symbolic programs with error handling, with a forall variable.@@ -566,7 +1076,9 @@   t ->   IO ([Model], CEGISResult SolvingFailure) cegisForAllExcept config inputs f v =-  cegisForAll config inputs $ simpleMerge $ f <$> extractUnionExcept v+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisForAllExcept synthesizerSolver verifierSolver inputs f v  -- | -- CEGIS for symbolic programs with error handling, with a forall variable.@@ -586,15 +1098,10 @@   (Either e v -> u (Either VerificationConditions ())) ->   t ->   IO ([Model], CEGISResult SolvingFailure)-cegisForAllExceptVC config inputs f v = do-  cegisForAll config inputs $-    simpleMerge $-      ( \case-          Left AssumptionViolation -> cegisPrePost (con False) (con True)-          Left AssertionViolation -> cegisPostCond (con False)-          _ -> cegisPostCond (con True)-      )-        <$> (extractUnionExcept v >>= f)+cegisForAllExceptVC config inputs f v =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisForAllExceptVC synthesizerSolver verifierSolver inputs f v  -- | -- CEGIS for symbolic programs with error handling, with a forall variable.@@ -613,4 +1120,7 @@   inputs ->   t ->   IO ([Model], CEGISResult SolvingFailure)-cegisForAllExceptStdVC config inputs = cegisForAllExceptVC config inputs return+cegisForAllExceptStdVC config inputs u =+  withSolver config $ \synthesizerSolver ->+    withSolver config $ \verifierSolver ->+      solverCegisForAllExceptStdVC synthesizerSolver verifierSolver inputs u

@@ -54,6 +54,7 @@ import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions) import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon)) 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)@@ -62,6 +63,7 @@     SymWordN (SymWordN),   ) import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))+import Grisette.Internal.SymPrim.SymFP (SymFP (SymFP), SymFPRoundingMode (SymFPRoundingMode)) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))@@ -126,12 +128,18 @@ CONCRETE_EVALUATESYM(Word16) CONCRETE_EVALUATESYM(Word32) CONCRETE_EVALUATESYM(Word64)+CONCRETE_EVALUATESYM(Float)+CONCRETE_EVALUATESYM(Double) CONCRETE_EVALUATESYM(B.ByteString) CONCRETE_EVALUATESYM(T.Text)+CONCRETE_EVALUATESYM(FPRoundingMode) CONCRETE_EVALUATESYM_BV(IntN) CONCRETE_EVALUATESYM_BV(WordN) #endif +instance (ValidFP eb fb) => EvaluateSym (FP eb fb) where+  evaluateSym _ _ = id+ -- () instance EvaluateSym () where   evaluateSym _ _ = id@@ -247,11 +255,16 @@ #if 1 EVALUATE_SYM_SIMPLE(SymBool) EVALUATE_SYM_SIMPLE(SymInteger)+EVALUATE_SYM_SIMPLE(SymFPRoundingMode) EVALUATE_SYM_BV(SymIntN) EVALUATE_SYM_BV(SymWordN) EVALUATE_SYM_FUN((=->), (=~>), SymTabularFun) EVALUATE_SYM_FUN((-->), (-~>), SymGeneralFun) #endif++instance (ValidFP eb sb) => EvaluateSym (SymFP eb sb) where+  evaluateSym fillDefault model (SymFP t) =+    SymFP $ evaluateTerm fillDefault model t  -- Exception deriving via (Default AssertionError) instance EvaluateSym AssertionError

@@ -50,6 +50,7 @@   ) import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions) 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   ( SymbolSet (SymbolSet),@@ -64,6 +65,10 @@     SymWordN (SymWordN),   ) import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))+import Grisette.Internal.SymPrim.SymFP+  ( SymFP (SymFP),+    SymFPRoundingMode (SymFPRoundingMode),+  ) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))@@ -114,12 +119,18 @@ CONCRETE_EXTRACT_SYMBOLICS(Word16) CONCRETE_EXTRACT_SYMBOLICS(Word32) CONCRETE_EXTRACT_SYMBOLICS(Word64)+CONCRETE_EXTRACT_SYMBOLICS(Float)+CONCRETE_EXTRACT_SYMBOLICS(Double) CONCRETE_EXTRACT_SYMBOLICS(B.ByteString) CONCRETE_EXTRACT_SYMBOLICS(T.Text)+CONCRETE_EXTRACT_SYMBOLICS(FPRoundingMode) CONCRETE_EXTRACT_SYMBOLICS_BV(WordN) CONCRETE_EXTRACT_SYMBOLICS_BV(IntN) #endif +instance (ValidFP eb sb) => ExtractSymbolics (FP eb sb) where+  extractSymbolics _ = mempty+ -- () instance ExtractSymbolics () where   extractSymbolics _ = mempty@@ -277,11 +288,15 @@ #if 1 EXTRACT_SYMBOLICS_SIMPLE(SymBool) EXTRACT_SYMBOLICS_SIMPLE(SymInteger)+EXTRACT_SYMBOLICS_SIMPLE(SymFPRoundingMode) EXTRACT_SYMBOLICS_BV(SymIntN) EXTRACT_SYMBOLICS_BV(SymWordN) EXTRACT_SYMBOLICS_FUN((=->), (=~>), SymTabularFun) EXTRACT_SYMBOLICS_FUN((-->), (-~>), SymGeneralFun) #endif++instance (ValidFP eb fb) => ExtractSymbolics (SymFP eb fb) where+  extractSymbolics (SymFP t) = SymbolSet $ extractSymbolicsTerm t  -- Exception deriving via (Default AssertionError) instance ExtractSymbolics AssertionError

@@ -15,6 +15,7 @@   ( GPretty (..),     groupedEnclose,     condEnclose,+    prettyWithConstructor,   ) where @@ -29,6 +30,8 @@ import qualified Data.ByteString as B import qualified Data.ByteString.Char8 as C import Data.Functor.Sum (Sum)+import qualified Data.HashMap.Lazy as HM+import qualified Data.HashSet as HS import Data.Int (Int16, Int32, Int64, Int8) import Data.String (IsString (fromString)) import qualified Data.Text as T@@ -52,6 +55,7 @@ import GHC.TypeLits (KnownNat, type (<=)) import Generics.Deriving (Default (Default, unDefault)) import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP) import Grisette.Internal.SymPrim.Prim.Term   ( LinkedRep,     SupportedPrim,@@ -62,6 +66,10 @@     SymWordN (SymWordN),   ) import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))+import Grisette.Internal.SymPrim.SymFP+  ( SymFP (SymFP),+    SymFPRoundingMode (SymFPRoundingMode),+  ) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))@@ -133,6 +141,9 @@ GPRETTY_SIMPLE(Word16) GPRETTY_SIMPLE(Word32) GPRETTY_SIMPLE(Word64)+GPRETTY_SIMPLE(Float)+GPRETTY_SIMPLE(Double)+GPRETTY_SIMPLE(FPRoundingMode) #endif  instance GPretty B.ByteString where@@ -147,6 +158,9 @@ instance (KnownNat n, 1 <= n) => GPretty (WordN n) where   gpretty = viaShow +instance (ValidFP eb sb) => GPretty (FP eb sb) where+  gpretty = viaShow+ -- () instance GPretty () where   gpretty = viaShow@@ -256,71 +270,40 @@   (GPretty (m (Maybe a))) =>   GPretty (MaybeT m a)   where-  gprettyPrec _ (MaybeT a) =-    group $-      nest 2 $-        vsep-          [ "MaybeT",-            gprettyPrec 11 a-          ]+  gprettyPrec n (MaybeT a) = prettyWithConstructor n "MaybeT" [gprettyPrec 11 a]  -- ExceptT instance   (GPretty (m (Either e a))) =>   GPretty (ExceptT e m a)   where-  gprettyPrec _ (ExceptT a) =-    group $-      nest 2 $-        vsep-          [ "ExceptT",-            gprettyPrec 11 a-          ]+  gprettyPrec n (ExceptT a) =+    prettyWithConstructor n "ExceptT" [gprettyPrec 11 a]  -- WriterT instance   (GPretty (m (a, w))) =>   GPretty (WriterLazy.WriterT w m a)   where-  gprettyPrec _ (WriterLazy.WriterT a) =-    group $-      nest 2 $-        vsep-          [ "WriterT",-            gprettyPrec 11 a-          ]+  gprettyPrec n (WriterLazy.WriterT a) =+    prettyWithConstructor n "WriterT" [gprettyPrec 11 a]  instance   (GPretty (m (a, w))) =>   GPretty (WriterStrict.WriterT w m a)   where-  gprettyPrec _ (WriterStrict.WriterT a) =-    group $-      nest 2 $-        vsep-          [ "WriterT",-            gprettyPrec 11 a-          ]+  gprettyPrec n (WriterStrict.WriterT a) =+    prettyWithConstructor n "WriterT" [gprettyPrec 11 a]  -- Identity instance (GPretty a) => GPretty (Identity a) where-  gprettyPrec _ (Identity a) =-    group $-      nest 2 $-        vsep-          [ "Identity",-            gprettyPrec 11 a-          ]+  gprettyPrec n (Identity a) =+    prettyWithConstructor n "Identity" [gprettyPrec 11 a]  -- IdentityT instance (GPretty (m a)) => GPretty (IdentityT m a) where-  gprettyPrec _ (IdentityT a) =-    group $-      nest 2 $-        vsep-          [ "IdentityT",-            gprettyPrec 11 a-          ]+  gprettyPrec n (IdentityT a) =+    prettyWithConstructor n "IdentityT" [gprettyPrec 11 a]  -- Prettyprint #define GPRETTY_SYM_SIMPLE(symtype) \@@ -339,12 +322,24 @@ #if 1 GPRETTY_SYM_SIMPLE(SymBool) GPRETTY_SYM_SIMPLE(SymInteger)+GPRETTY_SYM_SIMPLE(SymFPRoundingMode) GPRETTY_SYM_BV(SymIntN) GPRETTY_SYM_BV(SymWordN) GPRETTY_SYM_FUN(=~>, SymTabularFun) GPRETTY_SYM_FUN(-~>, SymGeneralFun) #endif +instance (ValidFP eb sb) => GPretty (SymFP eb sb) where+  gpretty (SymFP t) = prettyPrintTerm t++instance (GPretty a) => GPretty (HS.HashSet a) where+  gprettyPrec n s =+    prettyWithConstructor n "fromList" [gprettyPrec 11 $ HS.toList s]++instance (GPretty k, GPretty v) => GPretty (HM.HashMap k v) where+  gprettyPrec n s =+    prettyWithConstructor n "fromList" [gprettyPrec 11 $ HM.toList s]+ instance (Generic a, GPretty' (Rep a)) => GPretty (Default a) where   gprettyPrec i v = gprettyPrec' Pref i $ from $ unDefault v @@ -372,6 +367,10 @@ condEnclose :: Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann condEnclose b = if b then groupedEnclose else const $ const id +prettyWithConstructor :: Int -> Doc ann -> [Doc ann] -> Doc ann+prettyWithConstructor n c l =+  group $ condEnclose (n > 10) "(" ")" $ align $ nest 2 $ vsep (c : l)+ instance (GPretty' a, Constructor c) => GPretty' (M1 C c a) where   gprettyPrec' _ n c@(M1 x) =     case t of@@ -381,16 +380,12 @@         group $ condEnclose (n > m) "(" ")" $ gprettyPrec' t m x       _ ->         if isNullary x-          then pretty (conName c)+          then gpretty (conName c)           else-            group $-              condEnclose (n > 10) "(" ")" $-                align $-                  nest 2 $-                    vsep-                      [ pretty (conName c),-                        prettyBraces t (gprettyPrec' t 11 x)-                      ]+            prettyWithConstructor+              n+              (gpretty (conName c))+              [prettyBraces t (gprettyPrec' t 11 x)]     where       prettyBraces :: Type -> Doc ann -> Doc ann       prettyBraces Rec = groupedEnclose "{" "}"

@@ -128,6 +128,7 @@ import Grisette.Internal.Core.Data.Symbol (Identifier) import Grisette.Internal.Core.Data.Union (Union (UnionIf, UnionSingle)) 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.Term   ( LinkedRep,@@ -138,6 +139,7 @@     SymWordN,   ) import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>)) import Grisette.Internal.SymPrim.SymInteger (SymInteger) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))@@ -793,8 +795,11 @@ CONCRETE_GENSYM_SAME_SHAPE(Word16) CONCRETE_GENSYM_SAME_SHAPE(Word32) CONCRETE_GENSYM_SAME_SHAPE(Word64)+CONCRETE_GENSYM_SAME_SHAPE(Float)+CONCRETE_GENSYM_SAME_SHAPE(Double) CONCRETE_GENSYM_SAME_SHAPE(B.ByteString) CONCRETE_GENSYM_SAME_SHAPE(T.Text)+CONCRETE_GENSYM_SAME_SHAPE(FPRoundingMode) CONCRETE_GENSYM_SAME_SHAPE_BV(WordN) CONCRETE_GENSYM_SAME_SHAPE_BV(IntN) @@ -811,12 +816,23 @@ CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word16) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word32) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word64)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Float)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Double) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(B.ByteString) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(T.Text)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE(FPRoundingMode) CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(WordN) CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(IntN) #endif +instance (ValidFP eb sb) => GenSym (FP eb sb) (FP eb sb) where+  fresh = return . mrgSingle+  {-# INLINE fresh #-}++instance (ValidFP eb sb) => GenSymSimple (FP eb sb) (FP eb sb) where+  simpleFresh = return+  {-# INLINE simpleFresh #-}+ -- Bool instance GenSym () Bool where   fresh = derivedNoSpecFresh@@ -1671,6 +1687,10 @@ GENSYM_SIMPLE_SIMPLE(SymInteger) GENSYM_UNIT_SIMPLE(SymInteger) GENSYM_UNIT_SIMPLE_SIMPLE(SymInteger)+GENSYM_SIMPLE(SymFPRoundingMode)+GENSYM_SIMPLE_SIMPLE(SymFPRoundingMode)+GENSYM_UNIT_SIMPLE(SymFPRoundingMode)+GENSYM_UNIT_SIMPLE_SIMPLE(SymFPRoundingMode)  GENSYM_BV(SymIntN) GENSYM_SIMPLE_BV(SymIntN)@@ -1690,6 +1710,20 @@ GENSYM_UNIT_FUN((-->), (-~>)) GENSYM_UNIT_SIMPLE_FUN((-->), (-~>)) #endif++instance (ValidFP eb sb) => GenSym (SymFP eb sb) (SymFP eb sb)++instance (ValidFP eb sb) => GenSymSimple (SymFP eb sb) (SymFP eb sb) where+  simpleFresh _ = simpleFresh ()++instance (ValidFP eb sb) => GenSym () (SymFP eb sb) where+  fresh _ = mrgSingle <$> simpleFresh ()++instance (ValidFP eb sb) => GenSymSimple () (SymFP eb sb) where+  simpleFresh _ = do+    ident <- getIdentifier+    FreshIndex index <- nextFreshIndex+    return $ isym ident index  instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a) 

@@ -0,0 +1,338 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}++module Grisette.Internal.Core.Data.Class.IEEEFP+  ( fpIsNaN,+    fpIsPositiveZero,+    fpIsNegativeZero,+    fpIsPositiveInfinite,+    fpIsNegativeInfinite,+    fpIsPositive,+    fpIsNegative,+    fpIsInfinite,+    fpIsZero,+    fpIsNormal,+    fpIsSubnormal,+    fpIsPoint,+    SymIEEEFPTraits (..),+    IEEEConstants (..),+    IEEEFPOp (..),+    IEEEFPRoundingOp (..),+  )+where++import Data.SBV (infinity, nan)+import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))+import Grisette.Internal.SymPrim.FP (FP (FP), 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+{-# INLINE fpIsNaN #-}++-- | Check if a floating-point number is positive zero.+fpIsPositiveZero :: (RealFloat a) => a -> Bool+fpIsPositiveZero x = x == 0 && not (fpIsNegativeZero x)+{-# INLINE fpIsPositiveZero #-}++-- | Check if a floating-point number is negative zero.+fpIsNegativeZero :: (RealFloat a) => a -> Bool+fpIsNegativeZero = isNegativeZero+{-# INLINE fpIsNegativeZero #-}++-- | Check if a floating-point number is positive infinite.+fpIsPositiveInfinite :: (RealFloat a) => a -> Bool+fpIsPositiveInfinite x = isInfinite x && x > 0+{-# INLINE fpIsPositiveInfinite #-}++-- | Check if a floating-point number is negative infinite.+fpIsNegativeInfinite :: (RealFloat a) => a -> Bool+fpIsNegativeInfinite x = isInfinite x && x < 0+{-# INLINE fpIsNegativeInfinite #-}++-- | Check if a floating-point number is positive.+-- +0, +inf are considered positive. nan, -0, -inf are not positive.+fpIsPositive :: (RealFloat a) => a -> Bool+fpIsPositive x = not (fpIsNaN x) && (x > 0 || fpIsPositiveZero x)+{-# INLINE fpIsPositive #-}++-- | 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+{-# INLINE fpIsNegative #-}++-- | Check if a floating-point number is infinite.+fpIsInfinite :: (RealFloat a) => a -> Bool+fpIsInfinite x = fpIsPositiveInfinite x || fpIsNegativeInfinite x+{-# INLINE fpIsInfinite #-}++-- | Check if a floating-point number is zero.+fpIsZero :: (RealFloat a) => a -> Bool+fpIsZero x = fpIsPositiveZero x || fpIsNegativeZero x+{-# INLINE fpIsZero #-}++-- | Check if a floating-point number is normal, i.e., not 0, not inf, not+-- nan, and not denormalized.+fpIsNormal :: (RealFloat a) => a -> Bool+fpIsNormal x =+  not (fpIsZero x)+    && not (fpIsSubnormal x)+    && not (fpIsInfinite x)+    && not (fpIsNaN x)+{-# INLINE fpIsNormal #-}++-- | Check if a floating-point number is subnormal, i.e., denormalized. 0,+-- inf, or nan are not subnormal.+fpIsSubnormal :: (RealFloat a) => a -> Bool+fpIsSubnormal = isDenormalized+{-# INLINE fpIsSubnormal #-}++-- | Check if a floating-point number is a point, i.e., not inf, not nan.+fpIsPoint :: (RealFloat a) => a -> Bool+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+  -- | Positive infinity.+  fpPositiveInfinite :: a++  -- | Negative infinity.+  fpNegativeInfinite :: a++  -- | Not-a-number.+  fpNaN :: a++  -- | Negative zero.+  fpNegativeZero :: a++  -- | 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 #-}++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 #-}++class IEEEFPOp a where+  symFpAbs :: a -> a+  symFpNeg :: a -> a+  symFpRem :: a -> a -> a+  symFpMin :: a -> a -> a+  symFpMax :: a -> 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 #-}++class IEEEFPRoundingOp 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++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 #-}

@@ -19,6 +19,7 @@ where  import GHC.TypeNats (KnownNat, type (<=))+import Grisette.Internal.SymPrim.FP (ValidFP) import Grisette.Internal.SymPrim.GeneralFun (type (-->)) import Grisette.Internal.SymPrim.Prim.Term   ( LinkedRep,@@ -29,6 +30,10 @@     SymWordN (SymWordN),   ) import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))+import Grisette.Internal.SymPrim.SymFP+  ( SymFP (SymFP),+    SymFPRoundingMode (SymFPRoundingMode),+  ) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))@@ -72,8 +77,13 @@ #if 1 ITEOP_SIMPLE(SymBool) ITEOP_SIMPLE(SymInteger)+ITEOP_SIMPLE(SymFPRoundingMode) ITEOP_BV(SymIntN) ITEOP_BV(SymWordN) ITEOP_FUN((=->), (=~>), SymTabularFun) ITEOP_FUN((-->), (-~>), SymGeneralFun) #endif++instance (ValidFP eb sb) => ITEOp (SymFP eb sb) where+  symIte (SymBool c) (SymFP t) (SymFP f) = SymFP $ pevalITETerm c t f+  {-# INLINE symIte #-}

@@ -94,7 +94,7 @@     type (:~:) (Refl),   ) import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, type (<=))+import GHC.TypeNats (KnownNat, type (+), type (<=)) import Generics.Deriving   ( Default (Default),     Default1 (Default1),@@ -110,12 +110,19 @@     type (:+:) (L1, R1),   ) import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast)) import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte)) import Grisette.Internal.SymPrim.BV   ( BitwidthMismatch,     IntN,     WordN,   )+import Grisette.Internal.SymPrim.FP+  ( FP,+    FPRoundingMode,+    ValidFP,+    withValidFPProofs,+  ) import Grisette.Internal.SymPrim.GeneralFun (type (-->)) import Grisette.Internal.SymPrim.Prim.Term   ( LinkedRep,@@ -123,6 +130,7 @@   ) import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN) import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>)) import Grisette.Internal.SymPrim.SymInteger (SymInteger) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))@@ -403,12 +411,23 @@ CONCRETE_ORD_MERGEABLE(Word16) CONCRETE_ORD_MERGEABLE(Word32) CONCRETE_ORD_MERGEABLE(Word64)+CONCRETE_ORD_MERGEABLE(Float)+CONCRETE_ORD_MERGEABLE(Double) CONCRETE_ORD_MERGEABLE(B.ByteString) CONCRETE_ORD_MERGEABLE(T.Text)+CONCRETE_ORD_MERGEABLE(FPRoundingMode) CONCRETE_ORD_MERGEABLE_BV(WordN) CONCRETE_ORD_MERGEABLE_BV(IntN) #endif +instance (ValidFP eb sb) => Mergeable (FP eb sb) where+  rootStrategy =+    let sub = SimpleStrategy $ \_ t _ -> t+     in withValidFPProofs @eb @sb+          $ SortedStrategy+            (\fp -> (bitCast fp :: WordN (eb + sb)))+          $ const sub+ -- () deriving via (Default ()) instance Mergeable () @@ -911,11 +930,15 @@ #if 1 MERGEABLE_SIMPLE(SymBool) MERGEABLE_SIMPLE(SymInteger)+MERGEABLE_SIMPLE(SymFPRoundingMode) MERGEABLE_BV(SymIntN) MERGEABLE_BV(SymWordN) MERGEABLE_FUN((=->), (=~>)) MERGEABLE_FUN((-->), (-~>)) #endif++instance (ValidFP eb sb) => Mergeable (SymFP eb sb) where+  rootStrategy = SimpleStrategy symIte  -- Exceptions instance Mergeable ArithException where

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-}@@ -87,6 +88,18 @@           ++ fmap (first (.&& symNot c)) (toGuardedList r)       _ -> error "Should not happen" +  -- | Return all possible values in the union. Drop the path conditions.+  --+  -- >>> overestimateUnionValues (return 1 :: UnionM Integer)+  -- [1]+  --+  -- >>> overestimateUnionValues (mrgIf "a" (return 1) (return 2) :: UnionM Integer)+  -- [1,2]+  overestimateUnionValues :: (Mergeable a) => u a -> [a]+  overestimateUnionValues (Single v) = [v]+  overestimateUnionValues (If _ l r) =+    overestimateUnionValues l ++ overestimateUnionValues r+ -- | Pattern match to extract single values with 'singleView'. -- -- >>> case (return 1 :: UnionM Integer) of Single v -> v@@ -106,6 +119,10 @@   where     If c t f = mrgIf c t f +#if MIN_VERSION_base(4, 16, 4)+{-# COMPLETE Single, If #-}+#endif+ -- | Merge the simply mergeable values in a union, and extract the merged value. -- -- In the following example, 'mrgIfPropagatedStrategy' will not merge the results, and@@ -130,7 +147,6 @@ symIteMerge :: (ITEOp a, Mergeable a, PlainUnion u) => u a -> a symIteMerge (Single x) = x symIteMerge (If cond l r) = symIte cond (symIteMerge l) (symIteMerge r)-symIteMerge _ = error "Should not happen" {-# INLINE symIteMerge #-}  -- | Helper for applying functions on 'UnionLike' and 'SimpleMergeable'.

@@ -50,16 +50,24 @@     type (:*:) ((:*:)),     type (:+:) (L1, R1),   )-import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Internal.Core.Control.Exception+  ( AssertionError,+    VerificationConditions,+  ) import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&))) import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con)) import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP) import Grisette.Internal.SymPrim.Prim.Term (pevalEqTerm) import Grisette.Internal.SymPrim.SymBV   ( SymIntN (SymIntN),     SymWordN (SymWordN),   ) import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))+import Grisette.Internal.SymPrim.SymFP+  ( SymFP (SymFP),+    SymFPRoundingMode (SymFPRoundingMode),+  ) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))  -- $setup@@ -129,12 +137,19 @@ CONCRETE_SEQ(Word16) CONCRETE_SEQ(Word32) CONCRETE_SEQ(Word64)+CONCRETE_SEQ(Float)+CONCRETE_SEQ(Double) CONCRETE_SEQ(B.ByteString) CONCRETE_SEQ(T.Text)+CONCRETE_SEQ(FPRoundingMode) CONCRETE_SEQ_BV(WordN) CONCRETE_SEQ_BV(IntN) #endif +instance (ValidFP eb sb) => SEq (FP eb sb) where+  l .== r = con $ l == r+  {-# INLINE (.==) #-}+ -- List deriving via (Default [a]) instance (SEq a) => SEq [a] @@ -228,18 +243,25 @@ -- Symbolic types #define SEQ_SIMPLE(symtype) \ instance SEq symtype where \-  (symtype l) .== (symtype r) = SymBool $ pevalEqTerm l r+  (symtype l) .== (symtype r) = SymBool $ pevalEqTerm l r; \+  {-# INLINE (.==) #-}  #define SEQ_BV(symtype) \ instance (KnownNat n, 1 <= n) => SEq (symtype n) where \-  (symtype l) .== (symtype r) = SymBool $ pevalEqTerm l r+  (symtype l) .== (symtype r) = SymBool $ pevalEqTerm l r; \+  {-# INLINE (.==) #-}  #if 1 SEQ_SIMPLE(SymBool) SEQ_SIMPLE(SymInteger)+SEQ_SIMPLE(SymFPRoundingMode) SEQ_BV(SymIntN) SEQ_BV(SymWordN) #endif++instance (ValidFP eb sb) => SEq (SymFP eb sb) where+  (SymFP l) .== (SymFP r) = SymBool $ pevalEqTerm l r+  {-# INLINE (.==) #-}  -- Exceptions deriving via (Default AssertionError) instance SEq AssertionError

@@ -73,6 +73,7 @@     tryMerge,   ) import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP) import Grisette.Internal.SymPrim.Prim.Term   ( PEvalOrdTerm       ( pevalLeOrdTerm,@@ -86,6 +87,7 @@     SymWordN (SymWordN),   ) import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))+import Grisette.Internal.SymPrim.SymFP (SymFP (SymFP), SymFPRoundingMode (SymFPRoundingMode)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))  -- $setup@@ -189,10 +191,17 @@ CONCRETE_SORD(Word64) CONCRETE_SORD(B.ByteString) CONCRETE_SORD(T.Text)+CONCRETE_SORD(FPRoundingMode) CONCRETE_SORD_BV(WordN) CONCRETE_SORD_BV(IntN) #endif +instance (ValidFP eb sb) => SOrd (FP eb sb) where+  l .<= r = con $ l <= r+  l .< r = con $ l < r+  l .>= r = con $ l >= r+  l .> r = con $ l > r+ symCompareSingleList :: (SOrd a) => Bool -> Bool -> [a] -> [a] -> SymBool symCompareSingleList isLess isStrict = go   where@@ -337,6 +346,12 @@     (mrgSingle LT) \     (mrgIf (a .== b) (mrgSingle EQ) (mrgSingle GT)) +instance (ValidFP eb sb) => SOrd (SymFP eb sb) where+  (SymFP a) .<= (SymFP b) = SymBool $ pevalLeOrdTerm a b+  (SymFP a) .< (SymFP b) = SymBool $ pevalLtOrdTerm a b+  (SymFP a) .>= (SymFP b) = SymBool $ pevalGeOrdTerm a b+  (SymFP a) .> (SymFP b) = SymBool $ pevalGtOrdTerm a b+ instance SOrd SymBool where   l .<= r = symNot l .|| r   l .< r = symNot l .&& r@@ -350,6 +365,7 @@  #if 1 SORD_SIMPLE(SymInteger)+SORD_SIMPLE(SymFPRoundingMode) SORD_BV(SymIntN) SORD_BV(SymWordN) #endif

@@ -70,7 +70,10 @@     Mergeable3 (liftRootStrategy3),     MergingStrategy (SimpleStrategy),   )-import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge (tryMergeWithStrategy))+import Grisette.Internal.Core.Data.Class.TryMerge+  ( TryMerge (tryMergeWithStrategy),+  )+import Grisette.Internal.SymPrim.FP (ValidFP) import Grisette.Internal.SymPrim.GeneralFun (type (-->)) import Grisette.Internal.SymPrim.Prim.Term   ( LinkedRep,@@ -81,6 +84,7 @@     SymWordN,   ) import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>)) import Grisette.Internal.SymPrim.SymInteger (SymInteger) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))@@ -621,11 +625,16 @@ #if 1 SIMPLE_MERGEABLE_SIMPLE(SymBool) SIMPLE_MERGEABLE_SIMPLE(SymInteger)+SIMPLE_MERGEABLE_SIMPLE(SymFPRoundingMode) SIMPLE_MERGEABLE_BV(SymIntN) SIMPLE_MERGEABLE_BV(SymWordN) SIMPLE_MERGEABLE_FUN((=->), (=~>)) SIMPLE_MERGEABLE_FUN((-->), (-~>)) #endif++instance (ValidFP eb sb) => SimpleMergeable (SymFP eb sb) where+  mrgIte = symIte+  {-# INLINE mrgIte #-}  -- Exception deriving via (Default AssertionError) instance SimpleMergeable AssertionError

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-}@@ -33,22 +34,27 @@     -- * Solver interfaces     SolvingFailure (..),     MonadicSolver (..),+    monadicSolverSolve,     SolverCommand (..),     ConfigurableSolver (..),     Solver (..),+    solverSolve,     withSolver,     solve,+    solverSolveMulti,     solveMulti,      -- * Union with exceptions     UnionWithExcept (..),+    solverSolveExcept,     solveExcept,+    solverSolveMultiExcept,     solveMultiExcept,   ) where  import Control.DeepSeq (NFData)-import Control.Exception (SomeException, bracket)+import Control.Exception (SomeException, mask, onException) import Control.Monad.Except (ExceptT, runExceptT) import qualified Data.HashSet as S import Data.Hashable (Hashable)@@ -103,16 +109,26 @@ -- This interface abstract the monadic interface of a solver. All the operations -- performed in the monad are using a single solver instance. The solver -- instance is management by the monad's @run@ function.-class MonadicSolver m where+class (Monad m) => MonadicSolver m where   monadicSolverPush :: Int -> m ()   monadicSolverPop :: Int -> m ()-  monadicSolverSolve :: SymBool -> m (Either SolvingFailure Model)+  monadicSolverResetAssertions :: m ()+  monadicSolverAssert :: SymBool -> m ()+  monadicSolverCheckSat :: m (Either SolvingFailure Model) +monadicSolverSolve ::+  (MonadicSolver m) => SymBool -> m (Either SolvingFailure Model)+monadicSolverSolve formula = do+  monadicSolverAssert formula+  monadicSolverCheckSat+ -- | The commands that can be sent to a solver. data SolverCommand-  = SolverSolve SymBool+  = SolverAssert SymBool+  | SolverCheckSat   | SolverPush Int   | SolverPop Int+  | SolverResetAssertions   | SolverTerminate  -- | A class that abstracts the solver interface.@@ -124,8 +140,13 @@     SolverCommand ->     IO (Either SolvingFailure a) +  -- | Assert a formula.+  solverAssert :: handle -> SymBool -> IO (Either SolvingFailure ())+  solverAssert handle formula =+    solverRunCommand (const $ return $ Right ()) handle $ SolverAssert formula+   -- | Solve a formula.-  solverSolve :: handle -> SymBool -> IO (Either SolvingFailure Model)+  solverCheckSat :: handle -> IO (Either SolvingFailure Model)    -- | Push @n@ levels.   solverPush :: handle -> Int -> IO (Either SolvingFailure ())@@ -137,12 +158,119 @@   solverPop handle n =     solverRunCommand (const $ return $ Right ()) handle $ SolverPop n +  -- | Reset all assertions in the solver.+  --+  -- The solver keeps all the assertions used in the previous commands:+  --+  -- >>> solver <- newSolver (precise z3)+  -- >>> solverSolve solver "a"+  -- Right (Model {a -> True :: Bool})+  -- >>> solverSolve solver $ symNot "a"+  -- Left Unsat+  --+  -- You can clear the assertions using @solverResetAssertions@:+  --+  -- >>> solverResetAssertions solver+  -- Right ()+  -- >>> solverSolve solver $ symNot "a"+  -- Right (Model {a -> False :: Bool})+  solverResetAssertions :: handle -> IO (Either SolvingFailure ())+  solverResetAssertions handle =+    solverRunCommand (const $ return $ Right ()) handle SolverResetAssertions+   -- | Terminate the solver, wait until the last command is finished.   solverTerminate :: handle -> IO ()    -- | Force terminate the solver, do not wait for the last command to finish.   solverForceTerminate :: handle -> IO () +solverSolve ::+  (Solver handle) => handle -> SymBool -> IO (Either SolvingFailure Model)+solverSolve solver formula = do+  res <- solverAssert solver formula+  case res of+    Left err -> return $ Left err+    Right _ -> solverCheckSat solver++-- | Solve a single formula while returning multiple models to make it true.+-- The maximum number of desired models are given.+solverSolveMulti ::+  (Solver handle) =>+  -- | solver handle+  handle ->+  -- | maximum number of models to return+  Int ->+  -- | formula to solve, the solver will try to make it true+  SymBool ->+  IO ([Model], SolvingFailure)+solverSolveMulti solver numOfModelRequested formula = do+  firstModel <- solverSolve solver formula+  case firstModel of+    Left err -> return ([], err)+    Right model -> do+      (models, err) <- go solver model numOfModelRequested+      return (model : models, err)+  where+    allSymbols = extractSymbolics formula :: SymbolSet+    go solver prevModel n+      | n <= 1 = return ([], ResultNumLimitReached)+      | otherwise = do+          let newFormula =+                S.foldl'+                  ( \acc (SomeTypedSymbol _ v) ->+                      acc+                        .|| (symNot (SymBool $ fromJust $ equation v prevModel))+                  )+                  (con False)+                  (unSymbolSet allSymbols)+          res <- solverSolve solver newFormula+          case res of+            Left err -> return ([], err)+            Right model -> do+              (models, err) <- go solver model (n - 1)+              return (model : models, err)++-- |+-- Solver procedure for programs with error handling.+solverSolveExcept ::+  ( UnionWithExcept t u e v,+    PlainUnion u,+    Functor u,+    Solver handle+  ) =>+  -- | solver handle+  handle ->+  -- | mapping the results to symbolic boolean formulas, the solver would try to+  -- find a model to make the formula true+  (Either e v -> SymBool) ->+  -- | the program to be solved, should be a union of exception and values+  t ->+  IO (Either SolvingFailure Model)+solverSolveExcept solver f v =+  solverSolve solver (simpleMerge $ f <$> extractUnionExcept v)++-- |+-- Solver procedure for programs with error handling. Would return multiple+-- models if possible.+solverSolveMultiExcept ::+  ( UnionWithExcept t u e v,+    PlainUnion u,+    Functor u,+    Solver handle+  ) =>+  -- | solver configuration+  handle ->+  -- | maximum number of models to return+  Int ->+  -- | mapping the results to symbolic boolean formulas, the solver would try to+  -- find a model to make the formula true+  (Either e v -> SymBool) ->+  -- | the program to be solved, should be a union of exception and values+  t ->+  IO ([Model], SolvingFailure)+solverSolveMultiExcept handle n f v =+  solverSolveMulti handle n (simpleMerge $ f <$> extractUnionExcept v)+ -- | A class that abstracts the creation of a solver instance based on a -- configuration. --@@ -157,12 +285,26 @@  -- | Start a solver, run a computation with the solver, and terminate the -- solver after the computation finishes.+--+-- When an exception happens, this will forcibly terminate the solver.+--+-- Note: if Grisette is compiled with sbv < 10.10, the solver likely won't be+-- really terminated until it has finished the last action, and this will+-- result in long-running or zombie solver instances.+--+-- This was due to a bug in sbv, which is fixed in+-- https://github.com/LeventErkok/sbv/pull/695. withSolver ::   (ConfigurableSolver config handle) =>   config ->   (handle -> IO a) ->   IO a-withSolver config = bracket (newSolver config) solverTerminate+withSolver config action =+  mask $ \restore -> do+    handle <- newSolver config+    r <- restore (action handle) `onException` solverForceTerminate handle+    solverTerminate handle+    return r  -- | Solve a single formula. Find an assignment to it to make it true. --@@ -194,32 +336,8 @@   SymBool ->   IO ([Model], SolvingFailure) solveMulti config numOfModelRequested formula =-  withSolver config $ \solver -> do-    firstModel <- solverSolve solver formula-    case firstModel of-      Left err -> return ([], err)-      Right model -> do-        (models, err) <- go solver model numOfModelRequested-        return (model : models, err)-  where-    allSymbols = extractSymbolics formula :: SymbolSet-    go solver prevModel n-      | n <= 1 = return ([], ResultNumLimitReached)-      | otherwise = do-          let newFormula =-                S.foldl'-                  ( \acc (SomeTypedSymbol _ v) ->-                      acc-                        .|| (symNot (SymBool $ fromJust $ equation v prevModel))-                  )-                  (con False)-                  (unSymbolSet allSymbols)-          res <- solverSolve solver newFormula-          case res of-            Left err -> return ([], err)-            Right model -> do-              (models, err) <- go solver model (n - 1)-              return (model : models, err)+  withSolver config $+    \solver -> solverSolveMulti solver numOfModelRequested formula  -- | A class that abstracts the union-like structures that contains exceptions. class UnionWithExcept t u e v | t -> u e v where@@ -263,7 +381,9 @@   -- | the program to be solved, should be a union of exception and values   t ->   IO (Either SolvingFailure Model)-solveExcept config f v = solve config (simpleMerge $ f <$> extractUnionExcept v)+solveExcept config f v =+  withSolver config $+    \solver -> solverSolveExcept solver f v  -- | -- Solver procedure for programs with error handling. Would return multiple@@ -285,4 +405,5 @@   t ->   IO ([Model], SolvingFailure) solveMultiExcept config n f v =-  solveMulti config n (simpleMerge $ f <$> extractUnionExcept v)+  withSolver config $+    \solver -> solverSolveMultiExcept solver n f v

@@ -51,6 +51,7 @@   ) import Generics.Deriving.Instances () import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP) import Grisette.Internal.SymPrim.GeneralFun (substTerm, type (-->)) import Grisette.Internal.SymPrim.Prim.Term   ( LinkedRep (underlyingTerm),@@ -62,6 +63,10 @@     SymWordN (SymWordN),   ) import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))+import Grisette.Internal.SymPrim.SymFP+  ( SymFP (SymFP),+    SymFPRoundingMode (SymFPRoundingMode),+  ) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun)) import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))@@ -111,12 +116,18 @@ CONCRETE_SUBSTITUTESYM(Word16) CONCRETE_SUBSTITUTESYM(Word32) CONCRETE_SUBSTITUTESYM(Word64)+CONCRETE_SUBSTITUTESYM(Float)+CONCRETE_SUBSTITUTESYM(Double) CONCRETE_SUBSTITUTESYM(B.ByteString) CONCRETE_SUBSTITUTESYM(T.Text) CONCRETE_SUBSTITUTESYM_BV(WordN) CONCRETE_SUBSTITUTESYM_BV(IntN)+CONCRETE_SUBSTITUTESYM(FPRoundingMode) #endif +instance (ValidFP eb sb) => SubstituteSym (FP eb sb) where+  substituteSym _ _ = id+ instance SubstituteSym () where   substituteSym _ _ = id @@ -279,7 +290,11 @@ SUBSTITUTE_SYM_BV(SymWordN) SUBSTITUTE_SYM_FUN((=->), (=~>), SymTabularFun) SUBSTITUTE_SYM_FUN((-->), (-~>), SymGeneralFun)+SUBSTITUTE_SYM_SIMPLE(SymFPRoundingMode) #endif++instance (ValidFP eb sb) => SubstituteSym (SymFP eb sb) where+  substituteSym sym v (SymFP t) = SymFP $ substTerm sym (underlyingTerm v) t  -- | Auxiliary class for 'SubstituteSym' instance derivation class SubstituteSym' a where

@@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -45,11 +46,13 @@ import Generics.Deriving (Default (Default)) import Generics.Deriving.Instances () import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast)) import Grisette.Internal.Core.Data.Class.Solvable (Solvable (conView), pattern Con) import Grisette.Internal.SymPrim.BV   ( IntN (IntN),     WordN (WordN),   )+import Grisette.Internal.SymPrim.FP (FP, FP32, FP64, FPRoundingMode, ValidFP) import Grisette.Internal.SymPrim.GeneralFun (type (-->)) import Grisette.Internal.SymPrim.IntBitwidth (intBitwidthQ) import Grisette.Internal.SymPrim.Prim.Term@@ -61,6 +64,7 @@     SymWordN,   ) import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymFP (SymFP, SymFP32, SymFP64, SymFPRoundingMode) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>)) import Grisette.Internal.SymPrim.SymInteger (SymInteger) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))@@ -112,12 +116,18 @@ CONCRETE_TOCON(Word16) CONCRETE_TOCON(Word32) CONCRETE_TOCON(Word64)+CONCRETE_TOCON(Float)+CONCRETE_TOCON(Double) CONCRETE_TOCON(B.ByteString) CONCRETE_TOCON(T.Text) CONCRETE_TOCON_BV(WordN) CONCRETE_TOCON_BV(IntN)+CONCRETE_TOCON(FPRoundingMode) #endif +instance (ValidFP eb sb) => ToCon (FP eb sb) (FP eb sb) where+  toCon = Just+ -- Unit instance ToCon () () where   toCon = Just@@ -243,9 +253,12 @@ TO_CON_SYMID_BV(SymWordN) TO_CON_SYMID_FUN(=~>) TO_CON_SYMID_FUN(-~>)-+TO_CON_SYMID_SIMPLE(SymFPRoundingMode) #endif +instance (ValidFP eb sb) => ToCon (SymFP eb sb) (SymFP eb sb) where+  toCon = Just+ #define TO_CON_FROMSYM_SIMPLE(contype, symtype) \ instance ToCon symtype contype where \   toCon = conView@@ -266,8 +279,12 @@ TO_CON_FROMSYM_BV(WordN, SymWordN) TO_CON_FROMSYM_FUN((=->), (=~>)) TO_CON_FROMSYM_FUN((-->), (-~>))+TO_CON_FROMSYM_SIMPLE(FPRoundingMode, SymFPRoundingMode) #endif +instance (ValidFP eb sb) => ToCon (SymFP eb sb) (FP eb sb) where+  toCon = conView+ #define TOCON_MACHINE_INTEGER(sbvw, bvw, n, int) \ instance ToCon (sbvw n) int where \   toCon (Con (bvw v :: bvw n)) = Just $ fromIntegral v; \@@ -285,6 +302,14 @@ TOCON_MACHINE_INTEGER(SymIntN, IntN, $intBitwidthQ, Int) TOCON_MACHINE_INTEGER(SymWordN, WordN, $intBitwidthQ, Word) #endif++instance ToCon SymFP32 Float where+  toCon (Con (fp :: FP32)) = Just $ bitCast fp+  toCon _ = Nothing++instance ToCon SymFP64 Double where+  toCon (Con (fp :: FP64)) = Just $ bitCast fp+  toCon _ = Nothing  deriving via   (Default AssertionError)

@@ -53,11 +53,13 @@     type (:+:) (L1, R1),   ) import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast)) import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con)) 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.IntBitwidth (intBitwidthQ) import Grisette.Internal.SymPrim.Prim.Term@@ -69,6 +71,7 @@     SymWordN,   ) import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymFP (SymFP, SymFP32, SymFP64, SymFPRoundingMode) import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>)) import Grisette.Internal.SymPrim.SymInteger (SymInteger) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))@@ -110,12 +113,18 @@ CONCRETE_TOSYM(Word16) CONCRETE_TOSYM(Word32) CONCRETE_TOSYM(Word64)+CONCRETE_TOSYM(Float)+CONCRETE_TOSYM(Double) CONCRETE_TOSYM(B.ByteString) CONCRETE_TOSYM(T.Text)+CONCRETE_TOSYM(FPRoundingMode) CONCRETE_TOSYM_BV(IntN) CONCRETE_TOSYM_BV(WordN) #endif +instance (ValidFP eb sb) => ToSym (FP eb sb) (FP eb sb) where+  toSym = id+ -- Unit instance ToSym () () where   toSym = id@@ -238,8 +247,12 @@ TO_SYM_SYMID_BV(SymWordN) TO_SYM_SYMID_FUN(=~>) TO_SYM_SYMID_FUN(-~>)+TO_SYM_SYMID_SIMPLE(SymFPRoundingMode) #endif +instance (ValidFP eb sb) => ToSym (SymFP eb sb) (SymFP eb sb) where+  toSym = id+ #define TO_SYM_FROMCON_SIMPLE(contype, symtype) \ instance ToSym contype symtype where \   toSym = con@@ -260,8 +273,12 @@ TO_SYM_FROMCON_BV(WordN, SymWordN) TO_SYM_FROMCON_FUN((=->), (=~>)) TO_SYM_FROMCON_FUN((-->), (-~>))+TO_SYM_FROMCON_SIMPLE(FPRoundingMode, SymFPRoundingMode) #endif +instance (ValidFP eb sb) => ToSym (FP eb sb) (SymFP eb sb) where+  toSym = con+ #define TOSYM_MACHINE_INTEGER(int, bv) \ instance ToSym int (bv) where \   toSym = fromIntegral@@ -278,6 +295,14 @@ TOSYM_MACHINE_INTEGER(Int, SymIntN $intBitwidthQ) TOSYM_MACHINE_INTEGER(Word, SymWordN $intBitwidthQ) #endif++instance ToSym Float SymFP32 where+  toSym = con . bitCast+  {-# INLINE toSym #-}++instance ToSym Double SymFP64 where+  toSym = con . bitCast+  {-# INLINE toSym #-}  -- Exception deriving via

@@ -1,15 +1,17 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-}+{-# HLINT ignore "Unused LANGUAGE pragma" #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# HLINT ignore "Unused LANGUAGE pragma" #-}- -- | -- Module      :   Grisette.Internal.Core.Data.Symbol -- Copyright   :   (c) Sirui Lu 2024@@ -23,6 +25,7 @@     identifier,     withInfo,     withLoc,+    uniqueIdentifier,     Symbol (..),     simple,     indexed,@@ -31,11 +34,13 @@  import Control.DeepSeq (NFData (rnf)) import Data.Hashable (Hashable (hashWithSalt))+import Data.IORef (IORef, atomicModifyIORef', newIORef) import Data.String (IsString (fromString)) import qualified Data.Text as T import Data.Typeable (Proxy (Proxy), Typeable, eqT, typeRep, type (:~:) (Refl)) import Debug.Trace.LocationTH (__LOCATION__) import GHC.Generics (Generic)+import GHC.IO (unsafePerformIO) import Language.Haskell.TH.Syntax (Lift (liftTyped), unsafeTExpCoerce) import Language.Haskell.TH.Syntax.Compat (SpliceQ, liftSplice) @@ -192,6 +197,22 @@     s     (parseFileLocation $$(liftSplice $ unsafeTExpCoerce __LOCATION__))   ||]++identifierCount :: IORef Int+identifierCount = unsafePerformIO $ newIORef 0+{-# NOINLINE identifierCount #-}++newtype UniqueCount = UniqueCount Int+  deriving newtype (Eq, Ord, NFData, Hashable)+  deriving (Lift)++instance Show UniqueCount where+  show (UniqueCount i) = "unique<" <> show i <> ">"++uniqueIdentifier :: T.Text -> IO Identifier+uniqueIdentifier ident = do+  i <- atomicModifyIORef' identifierCount (\x -> (x + 1, x))+  return $ withInfo (identifier ident) (UniqueCount i)  -- | Symbol types for a symbolic variable. --

@@ -1,4 +1,5 @@ {-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-}@@ -27,7 +28,15 @@ module Grisette.Internal.SymPrim.BV   ( BitwidthMismatch (..),     IntN (..),+    IntN8,+    IntN16,+    IntN32,+    IntN64,     WordN (..),+    WordN8,+    WordN16,+    WordN32,+    WordN64,   ) where @@ -62,6 +71,8 @@ import Data.Hashable (Hashable) import Data.Maybe (fromMaybe, isJust) import Data.Proxy (Proxy (Proxy))+import Data.SBV (Int16, Int32, Int64, Int8, Word8)+import Data.Word (Word16, Word32, Word64) import GHC.Enum   ( boundedEnumFrom,     boundedEnumFromThen,@@ -85,6 +96,7 @@     type (+),     type (<=),   )+import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast)) import Grisette.Internal.Core.Data.Class.BitVector   ( SizedBV       ( sizedBVConcat,@@ -129,6 +141,14 @@ newtype WordN (n :: Nat) = WordN {unWordN :: Integer}   deriving (Eq, Ord, Generic, Lift, Hashable, NFData) +type WordN8 = WordN 8++type WordN16 = WordN 16++type WordN32 = WordN 32++type WordN64 = WordN 64+ instance (KnownNat n, 1 <= n) => Show (WordN n) where   show (WordN w) = if (bitwidth `mod` 4) == 0 then hexRepPre ++ hexRep else binRepPre ++ binRep     where@@ -171,6 +191,14 @@ newtype IntN (n :: Nat) = IntN {unIntN :: Integer}   deriving (Eq, Generic, Lift, Hashable, NFData) +type IntN8 = IntN 8++type IntN16 = IntN 16++type IntN32 = IntN 32++type IntN64 = IntN 64+ instance (KnownNat n, 1 <= n) => Show (IntN n) where   show (IntN w) = if (bitwidth `mod` 4) == 0 then hexRepPre ++ hexRep else binRepPre ++ binRep     where@@ -494,3 +522,66 @@   (DefaultFiniteBitsSymRotate (WordN n))   instance     (KnownNat n, 1 <= n) => SymRotate (WordN n)++#define BITCAST_FROM_INTEGRAL(from, to) \+  instance BitCast (from) (to) where \+    bitCast = fromIntegral++#if 1+BITCAST_FROM_INTEGRAL(WordN 8, Word8)+BITCAST_FROM_INTEGRAL(WordN 16, Word16)+BITCAST_FROM_INTEGRAL(WordN 32, Word32)+BITCAST_FROM_INTEGRAL(WordN 64, Word64)+BITCAST_FROM_INTEGRAL(WordN 8, Int8)+BITCAST_FROM_INTEGRAL(WordN 16, Int16)+BITCAST_FROM_INTEGRAL(WordN 32, Int32)+BITCAST_FROM_INTEGRAL(WordN 64, Int64)++BITCAST_FROM_INTEGRAL(Word8, WordN 8)+BITCAST_FROM_INTEGRAL(Word16, WordN 16)+BITCAST_FROM_INTEGRAL(Word32, WordN 32)+BITCAST_FROM_INTEGRAL(Word64, WordN 64)+BITCAST_FROM_INTEGRAL(Int8, WordN 8)+BITCAST_FROM_INTEGRAL(Int16, WordN 16)+BITCAST_FROM_INTEGRAL(Int32, WordN 32)+BITCAST_FROM_INTEGRAL(Int64, WordN 64)++BITCAST_FROM_INTEGRAL(IntN 8, Word8)+BITCAST_FROM_INTEGRAL(IntN 16, Word16)+BITCAST_FROM_INTEGRAL(IntN 32, Word32)+BITCAST_FROM_INTEGRAL(IntN 64, Word64)+BITCAST_FROM_INTEGRAL(IntN 8, Int8)+BITCAST_FROM_INTEGRAL(IntN 16, Int16)+BITCAST_FROM_INTEGRAL(IntN 32, Int32)+BITCAST_FROM_INTEGRAL(IntN 64, Int64)++BITCAST_FROM_INTEGRAL(Word8, IntN 8)+BITCAST_FROM_INTEGRAL(Word16, IntN 16)+BITCAST_FROM_INTEGRAL(Word32, IntN 32)+BITCAST_FROM_INTEGRAL(Word64, IntN 64)+BITCAST_FROM_INTEGRAL(Int8, IntN 8)+BITCAST_FROM_INTEGRAL(Int16, IntN 16)+BITCAST_FROM_INTEGRAL(Int32, IntN 32)+BITCAST_FROM_INTEGRAL(Int64, IntN 64)+#endif++instance (KnownNat n, 1 <= n) => BitCast (WordN n) (IntN n) where+  bitCast (WordN i) = IntN i++instance (KnownNat n, 1 <= n) => BitCast (IntN n) (WordN n) where+  bitCast (IntN i) = WordN i++#define BITCAST_VIA_WORDx(from, to, intermediate) \+  instance BitCast (from) (to) where \+    bitCast x = bitCast (bitCast x :: intermediate)++#if 1+BITCAST_VIA_WORDx(WordN64, Double, Word64)+BITCAST_VIA_WORDx(Double, WordN64, Word64)+BITCAST_VIA_WORDx(IntN64, Double, Word64)+BITCAST_VIA_WORDx(Double, IntN64, Word64)+BITCAST_VIA_WORDx(WordN32, Float, Word32)+BITCAST_VIA_WORDx(Float, WordN32, Word32)+BITCAST_VIA_WORDx(IntN32, Float, Word32)+BITCAST_VIA_WORDx(Float, IntN32, Word32)+#endif

@@ -0,0 +1,268 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveLift #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}++{- HLINT ignore "Unused LANGUAGE pragma" -}++module Grisette.Internal.SymPrim.FP+  ( ValidFP,+    FP (..),+    FP16,+    FP32,+    FP64,+    withValidFPProofs,+    FPRoundingMode (..),+    allFPRoundingMode,+  )+where++import Control.DeepSeq (NFData (rnf))+import Data.Bits (Bits (complement, shiftL, shiftR, xor, (.&.)))+import Data.Hashable (Hashable (hashWithSalt))+import Data.Int (Int16, Int32, Int64)+import Data.Maybe (fromJust)+import Data.Proxy (Proxy (Proxy))+import Data.SBV+  ( BVIsNonZero,+    FloatingPoint,+    SWord,+    SymVal (literal, unliteral),+    ValidFloat,+    Word16,+    Word32,+    Word64,+    infinity,+    nan,+    sFloatingPointAsSWord,+    sWordAsSFloatingPoint,+  )+import Data.Type.Equality (type (:~:) (Refl))+import GHC.Generics (Generic)+import GHC.TypeLits (KnownNat, Nat, natVal, type (+), type (<=))+import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))+import Grisette.Internal.Core.Data.Class.BitVector (SizedBV (sizedBVConcat))+import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.Utils.Parameterized+  ( KnownProof (KnownProof),+    knownAdd,+    unsafeAxiom,+    unsafeLeqProof,+    withKnownProof,+    withLeqProof,+  )+import Language.Haskell.TH.Syntax (Lift (liftTyped))+import Test.QuickCheck (frequency, oneof)+import qualified Test.QuickCheck as QC++bvIsNonZeroFromGEq1 ::+  forall w r proxy.+  (1 <= w) =>+  proxy w ->+  ((BVIsNonZero w) => r) ->+  r+bvIsNonZeroFromGEq1 _ r1 = case unsafeAxiom :: w :~: 1 of+  Refl -> r1++-- | A type-level proof that the given bit-widths are valid for a floating-point+-- number.+type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb++-- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand+-- bits.+newtype FP (eb :: Nat) (sb :: Nat) = FP {unFP :: FloatingPoint eb sb}+  deriving newtype (Eq, Show)++-- Workaround for https://github.com/GaloisInc/libBF-hs/pull/32, which affects+-- the correctness of the Ord instance for 'Data.SBV.FloatingPoint'.+instance (ValidFP eb sb) => Ord (FP eb sb) where+  FP x < FP y | isNaN x || isNaN y = False+  FP x < FP y = x < y+  FP x <= FP y | isNaN x || isNaN y = False+  FP x <= FP y = x <= y+  FP x > FP y | isNaN x || isNaN y = False+  FP x > FP y = x > y+  FP x >= FP y | isNaN x || isNaN y = False+  FP x >= FP y = x >= y++-- | IEEE 754 half-precision floating-point number.+type FP16 = FP 5 11++-- | IEEE 754 single-precision floating-point number.+type FP32 = FP 8 24++-- | IEEE 754 double-precision floating-point number.+type FP64 = FP 11 53++-- | Some type-level witnesses that could be derived from 'ValidFP'.+withValidFPProofs ::+  forall eb sb r.+  (ValidFP eb sb) =>+  ( ( KnownNat (eb + sb),+      BVIsNonZero (eb + sb),+      1 <= eb + sb,+      1 <= eb,+      1 <= sb+    ) =>+    r+  ) ->+  r+withValidFPProofs r =+  withKnownProof (knownAdd (KnownProof @eb) (KnownProof @sb)) $+    withLeqProof (unsafeLeqProof @1 @(eb + sb)) $+      withLeqProof (unsafeLeqProof @1 @eb) $+        withLeqProof (unsafeLeqProof @1 @sb) $+          bvIsNonZeroFromGEq1 (Proxy @(eb + sb)) r++instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (FP eb sb) (WordN r) where+  bitCast (FP f)+    | isNaN f =+        withValidFPProofs @eb @sb $+          sizedBVConcat (shiftR (-1) 1 :: WordN eb) highsb+    | otherwise = wordn+    where+      sb = fromIntegral $ natVal (Proxy @sb) :: Int+      highsb = withValidFPProofs @eb @sb $ shiftL 3 (sb - 2) :: WordN sb+      wordn :: WordN (eb + sb)+      wordn =+        withValidFPProofs @eb @sb $+          fromIntegral $+            fromJust $+              unliteral $+                sFloatingPointAsSWord $+                  literal f++instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (FP eb sb) (IntN r) where+  bitCast x = withValidFPProofs @eb @sb bitCast (bitCast x :: WordN r)++instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb) where+  bitCast v = FP fp+    where+      sword :: SWord r+      sword = withValidFPProofs @eb @sb fromIntegral v+      fp :: FloatingPoint eb sb+      fp =+        withValidFPProofs @eb @sb $+          fromJust $+            unliteral $+              sWordAsSFloatingPoint sword++instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb) where+  bitCast x = withValidFPProofs @eb @sb $ bitCast (bitCast x :: WordN (eb + sb))++#define BITCAST_VIA_INTERMEDIATE(from, to, intermediate) \+  instance BitCast (from) (to) where \+    bitCast x = bitCast (bitCast x :: intermediate)++#if 1+BITCAST_VIA_INTERMEDIATE(FP64, Double, WordN 64)+BITCAST_VIA_INTERMEDIATE(FP64, Int64, WordN 64)+BITCAST_VIA_INTERMEDIATE(FP64, Word64, WordN 64)+BITCAST_VIA_INTERMEDIATE(Double, FP64, WordN 64)+BITCAST_VIA_INTERMEDIATE(Int64, FP64, WordN 64)+BITCAST_VIA_INTERMEDIATE(Word64, FP64, WordN 64)++BITCAST_VIA_INTERMEDIATE(FP32, Float, WordN 32)+BITCAST_VIA_INTERMEDIATE(FP32, Int32, WordN 32)+BITCAST_VIA_INTERMEDIATE(FP32, Word32, WordN 32)+BITCAST_VIA_INTERMEDIATE(Float, FP32, WordN 32)+BITCAST_VIA_INTERMEDIATE(Int32, FP32, WordN 32)+BITCAST_VIA_INTERMEDIATE(Word32, FP32, WordN 32)++BITCAST_VIA_INTERMEDIATE(FP16, Word16, WordN 16)+BITCAST_VIA_INTERMEDIATE(FP16, Int16, WordN 16)+BITCAST_VIA_INTERMEDIATE(Word16, FP16, WordN 16)+BITCAST_VIA_INTERMEDIATE(Int16, FP16, WordN 16)+#endif+instance NFData (FP eb sb) where+  rnf (FP x) = x `seq` ()++instance (ValidFP eb sb) => Lift (FP eb sb) where+  liftTyped fp = [||bitCast wordnValue||]+    where+      wordnValue = bitCast fp :: WordN (eb + sb)++instance (ValidFP eb sb) => Hashable (FP eb sb) where+  hashWithSalt salt x = hashWithSalt salt (bitCast x :: WordN (eb + sb))++deriving newtype instance (ValidFloat eb sb) => Num (FP eb sb)++deriving newtype instance (ValidFloat eb sb) => Fractional (FP eb sb)++deriving newtype instance (ValidFloat eb sb) => Floating (FP eb sb)++deriving newtype instance (ValidFloat eb sb) => Real (FP eb sb)++deriving newtype instance (ValidFloat eb sb) => RealFrac (FP eb sb)++deriving newtype instance (ValidFloat eb sb) => RealFloat (FP eb sb)++instance (ValidFloat eb sb) => QC.Arbitrary (FP eb sb) where+  arbitrary = do+    frequency+      [ ( 3,+          withValidFPProofs @eb @sb $+            bitCast+              <$> (QC.arbitrary :: QC.Gen (WordN (eb + sb)))+        ),+        ( 5,+          -- mostly normalized numbers+          withValidFPProofs @eb @sb $ do+            e <- egen+            s <- sgen+            msb <- msbGen+            smsb <- smsbGen+            return $ bitCast (sizedBVConcat e s `xor` msb `xor` smsb)+        ),+        ( 4,+          -- mostly denormalized numbers+          withValidFPProofs @eb @sb $ do+            s <- sgen+            msb <- msbGen+            smsb <- smsbGen+            return $+              bitCast (sizedBVConcat 0 s `xor` msb .&. complement smsb)+        ),+        (1, oneof $ return <$> [nan, 0, -0, infinity, -infinity])+      ]+    where+      eb = fromIntegral $ natVal (Proxy @eb) :: Int+      sb = fromIntegral $ natVal (Proxy @sb) :: Int+      egen = withValidFPProofs @eb @sb $ QC.arbitrary :: QC.Gen (WordN eb)+      sgen = withValidFPProofs @eb @sb $ QC.arbitrary :: QC.Gen (WordN sb)+      msbGen =+        withValidFPProofs @eb @sb $+          oneof [return 0, return $ 1 `shiftL` (eb + sb - 1)] ::+          QC.Gen (WordN (eb + sb))+      smsbGen =+        withValidFPProofs @eb @sb $+          oneof [return 0, return $ 1 `shiftL` (sb - 1)] ::+          QC.Gen (WordN (eb + sb))++data FPRoundingMode = RNE | RNA | RTP | RTN | RTZ+  deriving (Eq, Ord, Show, Generic, Lift)+  deriving anyclass (Hashable, NFData)++allFPRoundingMode :: [FPRoundingMode]+allFPRoundingMode = [RNE, RNA, RTP, RTN, RTZ]++instance QC.Arbitrary FPRoundingMode where+  arbitrary = QC.elements [RNE, RNA, RTP, RTN, RTZ]

@@ -47,8 +47,11 @@   ) import Grisette.Internal.SymPrim.Prim.Internal.PartialEval (totalize2) import Grisette.Internal.SymPrim.Prim.Internal.Term-  ( SBVRep (SBVType),+  ( PEvalFloatingTerm (pevalSqrtTerm),+    PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),+    SBVRep (SBVType),     SupportedPrim (parseSMTModelResult, sbvEq),+    Term (FPBinaryTerm, FPFMATerm, FPRoundingBinaryTerm, FPRoundingUnaryTerm, FPTraitTerm, FdivTerm, RecipTerm, SqrtTerm),     partitionCVArg,   ) import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))@@ -103,6 +106,7 @@         ConTerm,         DivIntegralTerm,         EqTerm,+        FPUnaryTerm,         ITETerm,         LeOrdTerm,         LtOrdTerm,@@ -134,6 +138,12 @@     pevalAndTerm,     pevalDefaultEqTerm,     pevalEqTerm,+    pevalFPBinaryTerm,+    pevalFPFMATerm,+    pevalFPRoundingBinaryTerm,+    pevalFPRoundingUnaryTerm,+    pevalFPTraitTerm,+    pevalFPUnaryTerm,     pevalITEBasicTerm,     pevalNotTerm,     pevalOrTerm,@@ -683,3 +693,12 @@         ModIntegralTerm _ op1 op2 -> SomeTerm $ pevalModIntegralTerm (gov op1) (gov op2)         QuotIntegralTerm _ op1 op2 -> SomeTerm $ pevalQuotIntegralTerm (gov op1) (gov op2)         RemIntegralTerm _ op1 op2 -> SomeTerm $ pevalRemIntegralTerm (gov op1) (gov op2)+        FPTraitTerm _ trait op -> SomeTerm $ pevalFPTraitTerm trait (gov op)+        FdivTerm _ op1 op2 -> SomeTerm $ pevalFdivTerm (gov op1) (gov op2)+        RecipTerm _ op -> SomeTerm $ pevalRecipTerm (gov op)+        SqrtTerm _ op -> SomeTerm $ pevalSqrtTerm (gov op)+        FPUnaryTerm _ uop op -> SomeTerm $ pevalFPUnaryTerm uop (gov op)+        FPBinaryTerm _ bop op1 op2 -> SomeTerm $ pevalFPBinaryTerm bop (gov op1) (gov op2)+        FPRoundingUnaryTerm _ uop mode op -> SomeTerm $ pevalFPRoundingUnaryTerm uop mode (gov op)+        FPRoundingBinaryTerm _ bop mode op1 op2 -> SomeTerm $ pevalFPRoundingBinaryTerm bop mode (gov op1) (gov op2)+        FPFMATerm _ mode op1 op2 op3 -> SomeTerm $ pevalFPFMATerm (gov mode) (gov op1) (gov op2) (gov op3)

@@ -0,0 +1,218 @@+{-# LANGUAGE FlexibleContexts #-}++module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP+  ( pevalFPTraitTerm,+    sbvFPTraitTerm,+    pevalFPUnaryTerm,+    sbvFPUnaryTerm,+    pevalFPBinaryTerm,+    sbvFPBinaryTerm,+    pevalFPRoundingUnaryTerm,+    sbvFPRoundingUnaryTerm,+    pevalFPRoundingBinaryTerm,+    sbvFPRoundingBinaryTerm,+    pevalFPFMATerm,+    sbvFPFMATerm,+  )+where++import qualified Data.SBV as SBV+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)+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),+    SupportedPrim,+    Term (ConTerm),+    conTerm,+    fpBinaryTerm,+    fpFMATerm,+    fpRoundingBinaryTerm,+    fpRoundingUnaryTerm,+    fpTraitTerm,+    fpUnaryTerm,+  )+import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)++pevalFPTraitTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPTrait ->+  Term (FP eb sb) ->+  Term Bool+pevalFPTraitTerm trait = unaryUnfoldOnce doPevalFPTraitTerm (fpTraitTerm trait)+  where+    doPevalFPTraitTerm (ConTerm _ a) = case trait of+      FPIsNaN -> Just $ conTerm $ isNaN a+      FPIsPositive ->+        Just $+          conTerm $+            not (isNaN a) && a >= 0 && not (isNegativeZero a)+      FPIsNegative ->+        Just $ conTerm $ not (isNaN a) && (a < 0 || isNegativeZero a)+      FPIsInfinite -> Just $ conTerm $ isInfinite a+      FPIsPositiveInfinite -> Just $ conTerm $ isInfinite a && a > 0+      FPIsNegativeInfinite -> Just $ conTerm $ isInfinite a && a < 0+      FPIsPositiveZero ->+        Just $ conTerm $ a == 0 && not (isNegativeZero a)+      FPIsNegativeZero -> Just $ conTerm $ isNegativeZero a+      FPIsZero -> Just $ conTerm $ a == 0+      FPIsNormal ->+        Just $+          conTerm $+            not (a == 0 || isNaN a || isInfinite a || isDenormalized a)+      FPIsSubnormal -> Just $ conTerm $ isDenormalized a+      FPIsPoint -> Just $ conTerm $ not (isNaN a || isInfinite a)+    doPevalFPTraitTerm _ = Nothing++-- Workaround for https://github.com/GaloisInc/libBF-hs/pull/32, which affects+-- the correctness of the Ord instance for 'Data.SBV.FloatingPoint'.+goodFpIsPositive ::+  (ValidFP eb sb) =>+  SBV.SFloatingPoint eb sb ->+  SBV.SBool+goodFpIsPositive x =+  SBV.sNot (SBV.fpIsNaN x) SBV..&& SBV.fpIsPositive x+{-# INLINE goodFpIsPositive #-}++goodFpIsNegative ::+  (ValidFP eb sb) =>+  SBV.SFloatingPoint eb sb ->+  SBV.SBool+goodFpIsNegative x = SBV.sNot (SBV.fpIsNaN x) SBV..&& SBV.fpIsNegative x+{-# INLINE goodFpIsNegative #-}++sbvFPTraitTerm ::+  (ValidFP eb sb) =>+  FPTrait ->+  SBV.SFloatingPoint eb sb ->+  SBV.SBool+sbvFPTraitTerm FPIsNaN = SBV.fpIsNaN+sbvFPTraitTerm FPIsPositive = goodFpIsPositive+sbvFPTraitTerm FPIsNegative = goodFpIsNegative+sbvFPTraitTerm FPIsInfinite = SBV.fpIsInfinite+sbvFPTraitTerm FPIsPositiveInfinite = \f ->+  SBV.fpIsInfinite f SBV..&& goodFpIsPositive f+sbvFPTraitTerm FPIsNegativeInfinite = \f ->+  SBV.fpIsInfinite f SBV..&& goodFpIsNegative f+sbvFPTraitTerm FPIsPositiveZero =+  \f -> SBV.fpIsZero f SBV..&& goodFpIsPositive f+sbvFPTraitTerm FPIsNegativeZero =+  \f -> SBV.fpIsZero f SBV..&& goodFpIsNegative f+sbvFPTraitTerm FPIsZero = SBV.fpIsZero+sbvFPTraitTerm FPIsNormal = SBV.fpIsNormal+sbvFPTraitTerm FPIsSubnormal = SBV.fpIsSubnormal+sbvFPTraitTerm FPIsPoint = SBV.fpIsPoint++pevalFPUnaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPUnaryOp ->+  Term (FP eb sb) ->+  Term (FP eb sb)+pevalFPUnaryTerm = fpUnaryTerm+{-# INLINE pevalFPUnaryTerm #-}++sbvFPUnaryTerm ::+  (ValidFP eb sb) =>+  FPUnaryOp ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb+sbvFPUnaryTerm FPAbs = SBV.fpAbs+sbvFPUnaryTerm FPNeg = SBV.fpNeg+{-# INLINE sbvFPUnaryTerm #-}++pevalFPBinaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPBinaryOp ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb)+pevalFPBinaryTerm = fpBinaryTerm+{-# INLINE pevalFPBinaryTerm #-}++sbvFPBinaryTerm ::+  (ValidFP eb sb) =>+  FPBinaryOp ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb+sbvFPBinaryTerm FPRem = SBV.fpRem+sbvFPBinaryTerm FPMin = SBV.fpMin+sbvFPBinaryTerm FPMax = SBV.fpMax+{-# INLINE sbvFPBinaryTerm #-}++pevalFPRoundingUnaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPRoundingUnaryOp ->+  Term FPRoundingMode ->+  Term (FP eb sb) ->+  Term (FP eb sb)+pevalFPRoundingUnaryTerm = fpRoundingUnaryTerm+{-# INLINE pevalFPRoundingUnaryTerm #-}++sbvFPRoundingUnaryTerm ::+  (ValidFP eb sb) =>+  FPRoundingUnaryOp ->+  SBV.SRoundingMode ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb+sbvFPRoundingUnaryTerm FPSqrt = SBV.fpSqrt+sbvFPRoundingUnaryTerm FPRoundToIntegral = SBV.fpRoundToIntegral+{-# INLINE sbvFPRoundingUnaryTerm #-}++pevalFPRoundingBinaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPRoundingBinaryOp ->+  Term FPRoundingMode ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb)+pevalFPRoundingBinaryTerm = fpRoundingBinaryTerm+{-# INLINE pevalFPRoundingBinaryTerm #-}++sbvFPRoundingBinaryTerm ::+  (ValidFP eb sb) =>+  FPRoundingBinaryOp ->+  SBV.SRoundingMode ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb+sbvFPRoundingBinaryTerm FPAdd = SBV.fpAdd+sbvFPRoundingBinaryTerm FPSub = SBV.fpSub+sbvFPRoundingBinaryTerm FPMul = SBV.fpMul+sbvFPRoundingBinaryTerm FPDiv = SBV.fpDiv+{-# INLINE sbvFPRoundingBinaryTerm #-}++pevalFPFMATerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) =>+  Term FPRoundingMode ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb)+pevalFPFMATerm = fpFMATerm+{-# INLINE pevalFPFMATerm #-}++sbvFPFMATerm ::+  (ValidFP eb sb) =>+  SBV.SRoundingMode ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb ->+  SBV.SFloatingPoint eb sb+sbvFPFMATerm = SBV.fpFMA+{-# INLINE sbvFPFMATerm #-}

@@ -0,0 +1,25 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# HLINT ignore "Eta reduce" #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm () where++import Grisette.Internal.SymPrim.FP (FP, ValidFP)+import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()+import Grisette.Internal.SymPrim.Prim.Internal.Term+  ( PEvalFloatingTerm+      ( pevalSqrtTerm,+        withSbvFloatingTermConstraint+      ),+    SupportedPrim (withPrim),+    sqrtTerm,+  )+import Grisette.Internal.SymPrim.Prim.Internal.Unfold+  ( generalUnaryUnfolded,+  )++instance (ValidFP eb sb) => PEvalFloatingTerm (FP eb sb) where+  pevalSqrtTerm = generalUnaryUnfolded sqrt sqrtTerm+  withSbvFloatingTermConstraint p r = withPrim @(FP eb sb) p r

@@ -0,0 +1,26 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-# HLINT ignore "Eta reduce" #-}++module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm () where++import Grisette.Internal.SymPrim.FP (FP, ValidFP)+import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()+import Grisette.Internal.SymPrim.Prim.Internal.Term+  ( PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm, withSbvFractionalTermConstraint),+    SupportedPrim (withPrim),+    fdivTerm,+    recipTerm,+  )+import Grisette.Internal.SymPrim.Prim.Internal.Unfold+  ( generalBinaryUnfolded,+    generalUnaryUnfolded,+  )++instance (ValidFP eb sb) => PEvalFractionalTerm (FP eb sb) where+  pevalFdivTerm = generalBinaryUnfolded (/) fdivTerm+  pevalRecipTerm = generalUnaryUnfolded recip recipTerm+  withSbvFractionalTermConstraint p r = withPrim @(FP eb sb) p r

@@ -27,6 +27,7 @@ import Data.SBV (Bits (isSigned)) import GHC.TypeLits (KnownNat, type (<=)) import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, ValidFP) import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim () import Grisette.Internal.SymPrim.Prim.Internal.IsZero   ( IsZeroCases (IsZeroEvidence, NonZeroEvidence),@@ -53,6 +54,8 @@   ) import Grisette.Internal.SymPrim.Prim.Internal.Unfold   ( binaryUnfoldOnce,+    generalBinaryUnfolded,+    generalUnaryUnfolded,     unaryUnfoldOnce,   ) @@ -239,3 +242,11 @@   pevalAbsNumTerm = pevalBitsAbsNumTerm   pevalSignumNumTerm = pevalGeneralSignumNumTerm   withSbvNumTermConstraint p r = withPrim @(IntN n) p r++instance (ValidFP eb sb) => PEvalNumTerm (FP eb sb) where+  pevalAddNumTerm = generalBinaryUnfolded (+) addNumTerm+  pevalNegNumTerm = generalUnaryUnfolded negate negNumTerm+  pevalMulNumTerm = generalBinaryUnfolded (*) mulNumTerm+  pevalAbsNumTerm = generalUnaryUnfolded abs absNumTerm+  pevalSignumNumTerm = generalUnaryUnfolded signum signumNumTerm+  withSbvNumTermConstraint p r = withPrim @(FP eb sb) p r

@@ -23,14 +23,27 @@ where  import Control.Monad (msum)+import Data.Foldable (Foldable (foldl'))+import Data.Proxy (Proxy (Proxy))+import qualified Data.SBV as SBV import GHC.TypeNats (KnownNat, type (<=)) import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP, allFPRoundingMode) import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm ()-import Grisette.Internal.SymPrim.Prim.Internal.IsZero (IsZeroCases (IsZeroEvidence, NonZeroEvidence), KnownIsZero (isZero))+import Grisette.Internal.SymPrim.Prim.Internal.IsZero+  ( IsZeroCases (IsZeroEvidence, NonZeroEvidence),+    KnownIsZero (isZero),+  ) import Grisette.Internal.SymPrim.Prim.Internal.Term   ( PEvalNumTerm (pevalNegNumTerm),-    PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm, withSbvOrdTermConstraint),-    SupportedPrim (withPrim),+    PEvalOrdTerm+      ( pevalLeOrdTerm,+        pevalLtOrdTerm,+        sbvLeOrdTerm,+        sbvLtOrdTerm,+        withSbvOrdTermConstraint+      ),+    SupportedPrim (conSBVTerm, withPrim),     Term (AddNumTerm, ConTerm),     conTerm,     leOrdTerm,@@ -110,3 +123,50 @@   pevalLtOrdTerm = pevalGeneralLtOrdTerm   pevalLeOrdTerm = pevalGeneralLeOrdTerm   withSbvOrdTermConstraint p r = withPrim @(IntN n) p r++instance (ValidFP eb sb) => PEvalOrdTerm (FP eb sb) where+  pevalLtOrdTerm = pevalGeneralLtOrdTerm+  pevalLeOrdTerm = pevalGeneralLeOrdTerm+  withSbvOrdTermConstraint p r = withPrim @(FP eb sb) p r+  sbvLeOrdTerm _ x y =+    (SBV.sNot (SBV.fpIsNaN x) SBV..&& SBV.sNot (SBV.fpIsNaN y))+      SBV..&& (x SBV..<= y)++-- Use this table to avoid accidental breakage introduced by sbv.+fpRoundingModeLtTable :: [(SBV.SRoundingMode, SBV.SRoundingMode)]+fpRoundingModeLtTable =+  [ ( conSBVTerm @FPRoundingMode (Proxy @0) a,+      conSBVTerm @FPRoundingMode (Proxy @0) b+    )+    | a <- allFPRoundingMode,+      b <- allFPRoundingMode,+      a < b+  ]++fpRoundingModeLeTable :: [(SBV.SRoundingMode, SBV.SRoundingMode)]+fpRoundingModeLeTable =+  [ ( conSBVTerm @FPRoundingMode (Proxy @0) a,+      conSBVTerm @FPRoundingMode (Proxy @0) b+    )+    | a <- allFPRoundingMode,+      b <- allFPRoundingMode,+      a <= b+  ]++sbvTableLookup ::+  [(SBV.SRoundingMode, SBV.SRoundingMode)] ->+  SBV.SRoundingMode ->+  SBV.SRoundingMode ->+  SBV.SBV Bool+sbvTableLookup tbl lhs rhs =+  foldl'+    (\acc (a, b) -> acc SBV..|| ((lhs SBV..== a) SBV..&& (rhs SBV..== b)))+    SBV.sFalse+    tbl++instance PEvalOrdTerm FPRoundingMode where+  pevalLtOrdTerm = pevalGeneralLtOrdTerm+  pevalLeOrdTerm = pevalGeneralLeOrdTerm+  withSbvOrdTermConstraint p r = withPrim @FPRoundingMode p r+  sbvLtOrdTerm _ = sbvTableLookup fpRoundingModeLtTable+  sbvLeOrdTerm _ = sbvTableLookup fpRoundingModeLeTable

@@ -30,9 +30,13 @@ import qualified Data.SBV.Dynamic as SBVD import Data.Type.Bool (If) import Data.Type.Equality ((:~:) (Refl))-import Debug.Trace (trace)-import GHC.TypeNats (KnownNat, type (<=))+import GHC.TypeNats (KnownNat, natVal, type (<=)) import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP+  ( FP (FP),+    FPRoundingMode (RNA, RNE, RTN, RTP, RTZ),+    ValidFP,+  ) import Grisette.Internal.SymPrim.Prim.Internal.IsZero   ( IsZero,     IsZeroCases (IsZeroEvidence, NonZeroEvidence),@@ -52,6 +56,7 @@         pevalEqTerm,         pevalITETerm,         pformatCon,+        sbvIte,         symSBVName,         symSBVTerm,         withPrim@@ -59,6 +64,9 @@     SupportedPrimConstraint       ( PrimConstraint       ),+    Term (ConTerm),+    conTerm,+    eqTerm,     parseSMTModelResultError,     pevalDefaultEqTerm,     pevalITEBasicTerm,@@ -67,6 +75,7 @@ import Grisette.Internal.SymPrim.Prim.ModelValue (ModelValue, toModelValue) import Grisette.Internal.Utils.Parameterized (unsafeAxiom) import Type.Reflection (typeRep)+import Unsafe.Coerce (unsafeCoerce)  defaultValueForInteger :: Integer defaultValueForInteger = 0@@ -99,7 +108,7 @@   parseSMTModelResult :: Int -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> Integer   parseSMTModelResult _ ([], SBVD.CV SBVD.KUnbounded (SBVD.CInteger i)) = i   parseSMTModelResult _ ([([], SBVD.CV SBVD.KUnbounded (SBVD.CInteger i))], _) = i-  parseSMTModelResult _ cv = trace (show cv) $ parseSMTModelResultError (typeRep @Integer) cv+  parseSMTModelResult _ cv = parseSMTModelResultError (typeRep @Integer) cv  instance NonFuncSBVRep Integer where   type NonFuncSBVBaseType n Integer = If (IsZero n) Integer (SBV.IntN n)@@ -188,3 +197,91 @@   conNonFuncSBVTerm = conSBVTerm   symNonFuncSBVTerm = symSBVTerm @(WordN w)   withNonFuncPrim _ r = bvIsNonZeroFromGEq1 (Proxy @w) r++-- FP+instance (ValidFP eb sb) => SupportedPrimConstraint (FP eb sb) where+  type PrimConstraint _ (FP eb sb) = ValidFP eb sb++instance (ValidFP eb sb) => SBVRep (FP eb sb) where+  type SBVType _ (FP eb sb) = SBV.SBV (SBV.FloatingPoint eb sb)++instance (ValidFP eb sb) => SupportedPrim (FP eb sb) where+  defaultValue = 0+  pevalITETerm = pevalITEBasicTerm+  pevalEqTerm (ConTerm _ l) (ConTerm _ r) = conTerm $ l == r+  pevalEqTerm l@ConTerm {} r = pevalEqTerm r l+  pevalEqTerm l r = eqTerm l r+  conSBVTerm _ (FP fp) = SBV.literal fp+  symSBVName symbol _ = show symbol+  symSBVTerm _ name = sbvFresh name+  withPrim _ r = r+  parseSMTModelResult+    _+    ([], SBVD.CV (SBVD.KFP eb sb) (SBVD.CFP fp))+      | eb == fromIntegral (natVal (Proxy @eb))+          && sb == fromIntegral (natVal (Proxy @sb)) =+          -- Assumes that in SBV, FloatingPoint is a newtype of FP as the+          -- constructor isn't exposed+          fromIntegral $ unsafeCoerce fp+  parseSMTModelResult+    _+    ([([], SBVD.CV (SBVD.KFP eb sb) (SBVD.CFP fp))], _)+      | eb == fromIntegral (natVal (Proxy @eb))+          && sb == fromIntegral (natVal (Proxy @sb)) =+          -- Assumes that in SBV, FloatingPoint is a newtype of FP as the+          -- constructor isn't exposed+          fromIntegral $ unsafeCoerce fp+  parseSMTModelResult _ cv = parseSMTModelResultError (typeRep @(FP eb sb)) cv++  -- Workaround for sbv#702.+  sbvIte p = withPrim @(FP eb sb) p $ \c a b ->+    case (SBV.unliteral a, SBV.unliteral b) of+      (Just a', Just b')+        | isInfinite a' && isInfinite b' ->+            let correspondingZero x = if x > 0 then 0 else -0+             in 1+                  / sbvIte @(FP eb sb)+                    p+                    c+                    (conSBVTerm @(FP eb sb) p $ correspondingZero a')+                    (conSBVTerm @(FP eb sb) p $ correspondingZero b')+      _ -> SBV.ite c a b++instance (ValidFP eb sb) => NonFuncSBVRep (FP eb sb) where+  type NonFuncSBVBaseType _ (FP eb sb) = SBV.FloatingPoint eb sb++instance (ValidFP eb sb) => SupportedNonFuncPrim (FP eb sb) where+  conNonFuncSBVTerm = conSBVTerm+  symNonFuncSBVTerm = symSBVTerm @(FP eb sb)+  withNonFuncPrim _ r = r++-- FPRoundingMode+instance SupportedPrimConstraint FPRoundingMode++instance SBVRep FPRoundingMode where+  type SBVType _ FPRoundingMode = SBV.SBV SBV.RoundingMode++instance SupportedPrim FPRoundingMode where+  defaultValue = RNE+  pevalITETerm = pevalITEBasicTerm+  pevalEqTerm (ConTerm _ l) (ConTerm _ r) = conTerm $ l == r+  pevalEqTerm l@ConTerm {} r = pevalEqTerm r l+  pevalEqTerm l r = eqTerm l r+  conSBVTerm _ RNE = SBV.sRNE+  conSBVTerm _ RNA = SBV.sRNA+  conSBVTerm _ RTP = SBV.sRTP+  conSBVTerm _ RTN = SBV.sRTN+  conSBVTerm _ RTZ = SBV.sRTZ+  symSBVName symbol _ = show symbol+  symSBVTerm _ name = sbvFresh name+  withPrim _ r = r+  parseSMTModelResult _ cv =+    parseSMTModelResultError (typeRep @FPRoundingMode) cv++instance NonFuncSBVRep FPRoundingMode where+  type NonFuncSBVBaseType _ FPRoundingMode = SBV.RoundingMode++instance SupportedNonFuncPrim FPRoundingMode where+  conNonFuncSBVTerm = conSBVTerm+  symNonFuncSBVTerm = symSBVTerm @FPRoundingMode+  withNonFuncPrim _ r = r

@@ -58,6 +58,8 @@     PEvalDivModIntegralTerm (..),     PEvalBVSignConversionTerm (..),     PEvalBVTerm (..),+    PEvalFractionalTerm (..),+    PEvalFloatingTerm (..),      -- * Typed symbols     TypedSymbol (..),@@ -67,6 +69,11 @@     someTypedSymbol,      -- * Terms+    FPTrait (..),+    FPUnaryOp (..),+    FPBinaryOp (..),+    FPRoundingUnaryOp (..),+    FPRoundingBinaryOp (..),     Term (..),     identity,     identityWithTypeRep,@@ -115,6 +122,15 @@     modIntegralTerm,     quotIntegralTerm,     remIntegralTerm,+    fpTraitTerm,+    fdivTerm,+    recipTerm,+    sqrtTerm,+    fpUnaryTerm,+    fpBinaryTerm,+    fpRoundingUnaryTerm,+    fpRoundingBinaryTerm,+    fpFMATerm,      -- * Support for boolean type     trueTerm,@@ -171,6 +187,7 @@ import Data.String (IsString (fromString)) import Data.Typeable (Proxy (Proxy), cast) import GHC.Exts (sortWith)+import GHC.Generics (Generic) import GHC.IO (unsafeDupablePerformIO) import GHC.Stack (HasCallStack) import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))@@ -184,6 +201,7 @@   ( Identifier,     Symbol (IndexedSymbol, SimpleSymbol),   )+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP) import Grisette.Internal.SymPrim.Prim.Internal.Caches   ( typeMemoizedCache,   )@@ -414,7 +432,8 @@   sbvEq _ = (SBV..==)   parseSMTModelResult :: Int -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> t -parseSMTModelResultError :: TypeRep a -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> a+parseSMTModelResultError ::+  (HasCallStack) => TypeRep a -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> a parseSMTModelResultError ty cv =   error $     "BUG: cannot parse SBV model value \""@@ -775,6 +794,42 @@     SBVType int (bv n) ->     SBVType int (bv w) +class (SupportedPrim t, Fractional t) => PEvalFractionalTerm t where+  pevalFdivTerm :: Term t -> Term t -> Term t+  pevalRecipTerm :: Term t -> Term t+  withSbvFractionalTermConstraint ::+    (KnownIsZero n) =>+    proxy n ->+    (((Fractional (SBVType n t)) => r)) ->+    r+  sbvFdivTerm ::+    (KnownIsZero n) =>+    proxy n ->+    SBVType n t ->+    SBVType n t ->+    SBVType n t+  sbvFdivTerm p l r = withSbvFractionalTermConstraint @t p $ l / r+  sbvRecipTerm ::+    (KnownIsZero n) =>+    proxy n ->+    SBVType n t ->+    SBVType n t+  sbvRecipTerm p l = withSbvFractionalTermConstraint @t p $ recip l++class (SupportedPrim t, Floating t) => PEvalFloatingTerm t where+  pevalSqrtTerm :: Term t -> Term t+  withSbvFloatingTermConstraint ::+    (KnownIsZero n) =>+    proxy n ->+    (((Floating (SBVType n t)) => r)) ->+    r+  sbvSqrtTerm ::+    (KnownIsZero n) =>+    proxy n ->+    SBVType n t ->+    SBVType n t+  sbvSqrtTerm p l = withSbvFloatingTermConstraint @t p $ sqrt l+ class   (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) =>   UnaryOp tag arg t@@ -889,6 +944,66 @@  -- Terms +data FPTrait+  = FPIsNaN+  | FPIsPositive+  | FPIsNegative+  | FPIsPositiveInfinite+  | FPIsNegativeInfinite+  | FPIsInfinite+  | FPIsPositiveZero+  | FPIsNegativeZero+  | FPIsZero+  | FPIsNormal+  | FPIsSubnormal+  | FPIsPoint+  deriving (Eq, Ord, Generic, Hashable, Lift, NFData)++instance Show FPTrait where+  show FPIsNaN = "is_nan"+  show FPIsPositive = "is_pos"+  show FPIsNegative = "is_neg"+  show FPIsPositiveInfinite = "is_pos_inf"+  show FPIsNegativeInfinite = "is_neg_inf"+  show FPIsInfinite = "is_inf"+  show FPIsPositiveZero = "is_pos_zero"+  show FPIsNegativeZero = "is_neg_zero"+  show FPIsZero = "is_zero"+  show FPIsNormal = "is_normal"+  show FPIsSubnormal = "is_subnormal"+  show FPIsPoint = "is_point"++data FPUnaryOp = FPAbs | FPNeg+  deriving (Eq, Ord, Generic, Hashable, Lift, NFData)++instance Show FPUnaryOp where+  show FPAbs = "fp.abs"+  show FPNeg = "fp.neg"++data FPBinaryOp = FPRem | FPMin | FPMax+  deriving (Eq, Ord, Generic, Hashable, Lift, NFData)++instance Show FPBinaryOp where+  show FPRem = "fp.rem"+  show FPMin = "fp.min"+  show FPMax = "fp.max"++data FPRoundingUnaryOp = FPSqrt | FPRoundToIntegral+  deriving (Eq, Ord, Generic, Hashable, Lift, NFData)++instance Show FPRoundingUnaryOp where+  show FPSqrt = "fp.sqrt"+  show FPRoundToIntegral = "fp.roundToIntegral"++data FPRoundingBinaryOp = FPAdd | FPSub | FPMul | FPDiv+  deriving (Eq, Ord, Generic, Hashable, Lift, NFData)++instance Show FPRoundingBinaryOp where+  show FPAdd = "fp.add"+  show FPSub = "fp.sub"+  show FPMul = "fp.mul"+  show FPDiv = "fp.div"+ data Term t where   ConTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !t -> Term t   SymTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(TypedSymbol t) -> Term t@@ -1078,6 +1193,64 @@     !(Term t) ->     !(Term t) ->     Term t+  FPTraitTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    {-# UNPACK #-} !Id ->+    !FPTrait ->+    !(Term (FP eb sb)) ->+    Term Bool+  FdivTerm ::+    (PEvalFractionalTerm t) =>+    {-# UNPACK #-} !Id ->+    !(Term t) ->+    !(Term t) ->+    Term t+  RecipTerm ::+    (PEvalFractionalTerm t) =>+    {-# UNPACK #-} !Id ->+    !(Term t) ->+    Term t+  SqrtTerm ::+    (PEvalFloatingTerm t) =>+    {-# UNPACK #-} !Id ->+    !(Term t) ->+    Term t+  FPUnaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    {-# UNPACK #-} !Id ->+    !FPUnaryOp ->+    !(Term (FP eb sb)) ->+    Term (FP eb sb)+  FPBinaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    {-# UNPACK #-} !Id ->+    !FPBinaryOp ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    Term (FP eb sb)+  FPRoundingUnaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    {-# UNPACK #-} !Id ->+    !FPRoundingUnaryOp ->+    !(Term FPRoundingMode) ->+    !(Term (FP eb sb)) ->+    Term (FP eb sb)+  FPRoundingBinaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    {-# UNPACK #-} !Id ->+    !FPRoundingBinaryOp ->+    !(Term FPRoundingMode) ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    Term (FP eb sb)+  FPFMATerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) =>+    {-# UNPACK #-} !Id ->+    !(Term FPRoundingMode) ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    Term (FP eb sb)  identity :: Term t -> Id identity = snd . identityWithTypeRep@@ -1119,6 +1292,15 @@ identityWithTypeRep (ModIntegralTerm i _ _) = (someTypeRep (Proxy @t), i) identityWithTypeRep (QuotIntegralTerm i _ _) = (someTypeRep (Proxy @t), i) identityWithTypeRep (RemIntegralTerm i _ _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (FPTraitTerm i _ _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (FdivTerm i _ _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (RecipTerm i _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (SqrtTerm i _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (FPUnaryTerm i _ _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (FPBinaryTerm i _ _ _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (FPRoundingUnaryTerm i _ _ _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (FPRoundingBinaryTerm i _ _ _ _) = (someTypeRep (Proxy @t), i)+identityWithTypeRep (FPFMATerm i _ _ _ _) = (someTypeRep (Proxy @t), i) {-# INLINE identityWithTypeRep #-}  introSupportedPrimConstraint :: forall t a. Term t -> ((SupportedPrim t) => a) -> a@@ -1157,6 +1339,15 @@ introSupportedPrimConstraint ModIntegralTerm {} x = x introSupportedPrimConstraint QuotIntegralTerm {} x = x introSupportedPrimConstraint RemIntegralTerm {} x = x+introSupportedPrimConstraint FPTraitTerm {} x = x+introSupportedPrimConstraint FdivTerm {} x = x+introSupportedPrimConstraint RecipTerm {} x = x+introSupportedPrimConstraint SqrtTerm {} x = x+introSupportedPrimConstraint FPUnaryTerm {} x = x+introSupportedPrimConstraint FPBinaryTerm {} x = x+introSupportedPrimConstraint FPRoundingUnaryTerm {} x = x+introSupportedPrimConstraint FPRoundingBinaryTerm {} x = x+introSupportedPrimConstraint FPFMATerm {} x = x {-# INLINE introSupportedPrimConstraint #-}  pformat :: forall t. (SupportedPrim t) => Term t -> String@@ -1196,6 +1387,17 @@ pformat (ModIntegralTerm _ arg1 arg2) = "(mod " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")" pformat (QuotIntegralTerm _ arg1 arg2) = "(quot " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")" pformat (RemIntegralTerm _ arg1 arg2) = "(rem " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")"+pformat (FPTraitTerm _ trait arg) = "(" ++ show trait ++ " " ++ pformat arg ++ ")"+pformat (FdivTerm _ arg1 arg2) = "(fdiv " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")"+pformat (RecipTerm _ arg) = "(recip " ++ pformat arg ++ ")"+pformat (SqrtTerm _ arg) = "(sqrt " ++ pformat arg ++ ")"+pformat (FPUnaryTerm _ op arg) = "(" ++ show op ++ " " ++ pformat arg ++ ")"+pformat (FPBinaryTerm _ op arg1 arg2) = "(" ++ show op ++ " " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")"+pformat (FPRoundingUnaryTerm _ op mode arg) = "(" ++ show op ++ " " ++ show mode ++ " " ++ pformat arg ++ ")"+pformat (FPRoundingBinaryTerm _ op mode arg1 arg2) =+  "(" ++ show op ++ " " ++ show mode ++ " " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")"+pformat (FPFMATerm _ mode arg1 arg2 arg3) =+  "(fp.fma " ++ show mode ++ " " ++ pformat arg1 ++ " " ++ pformat arg2 ++ " " ++ pformat arg3 ++ ")" {-# INLINE pformat #-}  instance NFData (Term a) where@@ -1237,6 +1439,15 @@   liftTyped (ModIntegralTerm _ arg1 arg2) = [||modIntegralTerm arg1 arg2||]   liftTyped (QuotIntegralTerm _ arg1 arg2) = [||quotIntegralTerm arg1 arg2||]   liftTyped (RemIntegralTerm _ arg1 arg2) = [||remIntegralTerm arg1 arg2||]+  liftTyped (FPTraitTerm _ trait arg) = [||fpTraitTerm trait arg||]+  liftTyped (FdivTerm _ arg1 arg2) = [||fdivTerm arg1 arg2||]+  liftTyped (RecipTerm _ arg) = [||recipTerm arg||]+  liftTyped (SqrtTerm _ arg) = [||sqrtTerm arg||]+  liftTyped (FPUnaryTerm _ op arg) = [||fpUnaryTerm op arg||]+  liftTyped (FPBinaryTerm _ op arg1 arg2) = [||fpBinaryTerm op arg1 arg2||]+  liftTyped (FPRoundingUnaryTerm _ op mode arg) = [||fpRoundingUnaryTerm op mode arg||]+  liftTyped (FPRoundingBinaryTerm _ op mode arg1 arg2) = [||fpRoundingBinaryTerm op mode arg1 arg2||]+  liftTyped (FPFMATerm _ mode arg1 arg2 arg3) = [||fpFMATerm mode arg1 arg2 arg3||]  instance Show (Term ty) where   show (ConTerm i v) = "ConTerm{id=" ++ show i ++ ", v=" ++ show v ++ "}"@@ -1317,6 +1528,41 @@     "QuotIntegral{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"   show (RemIntegralTerm i arg1 arg2) =     "RemIntegral{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"+  show (FPTraitTerm i trait arg) =+    "FPTrait{id=" ++ show i ++ ", trait=" ++ show trait ++ ", arg=" ++ show arg ++ "}"+  show (FdivTerm i arg1 arg2) = "Fdiv{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"+  show (RecipTerm i arg) = "Recip{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"+  show (SqrtTerm i arg) = "Sqrt{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"+  show (FPUnaryTerm i op arg) = "FPUnary{id=" ++ show i ++ ", op=" ++ show op ++ ", arg=" ++ show arg ++ "}"+  show (FPBinaryTerm i op arg1 arg2) =+    "FPBinary{id=" ++ show i ++ ", op=" ++ show op ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"+  show (FPRoundingUnaryTerm i op mode arg) =+    "FPRoundingUnary{id=" ++ show i ++ ", op=" ++ show op ++ ", mode=" ++ show mode ++ ", arg=" ++ show arg ++ "}"+  show (FPRoundingBinaryTerm i op mode arg1 arg2) =+    "FPRoundingBinary{id="+      ++ show i+      ++ ", op="+      ++ show op+      ++ ", mode="+      ++ show mode+      ++ ", arg1="+      ++ show arg1+      ++ ", arg2="+      ++ show arg2+      ++ "}"+  show (FPFMATerm i mode arg1 arg2 arg3) =+    "FPFMA{id="+      ++ show i+      ++ ", mode="+      ++ show mode+      ++ ", arg1="+      ++ show arg1+      ++ ", arg2="+      ++ show arg2+      ++ ", arg3="+      ++ show arg3+      ++ "}"+  {-# INLINE show #-}  prettyPrintTerm :: Term t -> Doc ann prettyPrintTerm v =@@ -1439,6 +1685,45 @@     (PEvalDivModIntegralTerm t) => !(Term t) -> !(Term t) -> UTerm t   URemIntegralTerm ::     (PEvalDivModIntegralTerm t) => !(Term t) -> !(Term t) -> UTerm t+  UFPTraitTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    !FPTrait ->+    !(Term (FP eb sb)) ->+    UTerm Bool+  UFdivTerm :: (PEvalFractionalTerm t) => !(Term t) -> !(Term t) -> UTerm t+  URecipTerm :: (PEvalFractionalTerm t) => !(Term t) -> UTerm t+  USqrtTerm :: (PEvalFloatingTerm t) => !(Term t) -> UTerm t+  UFPUnaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    !FPUnaryOp ->+    !(Term (FP eb sb)) ->+    UTerm (FP eb sb)+  UFPBinaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    !FPBinaryOp ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    UTerm (FP eb sb)+  UFPRoundingUnaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    !FPRoundingUnaryOp ->+    !(Term FPRoundingMode) ->+    !(Term (FP eb sb)) ->+    UTerm (FP eb sb)+  UFPRoundingBinaryTerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+    !FPRoundingBinaryOp ->+    !(Term FPRoundingMode) ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    UTerm (FP eb sb)+  UFPFMATerm ::+    (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) =>+    !(Term FPRoundingMode) ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    !(Term (FP eb sb)) ->+    UTerm (FP eb sb)  eqTypedId :: (TypeRep a, Id) -> (TypeRep b, Id) -> Bool eqTypedId (a, i1) (b, i2) = i1 == i2 && eqTypeRepBool a b@@ -1519,6 +1804,15 @@     DModIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)     DQuotIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)     DRemIntegralTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)+    DFPTraitTerm :: FPTrait -> {-# UNPACK #-} !Id -> Description (Term Bool)+    DFdivTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term a)+    DRecipTerm :: {-# UNPACK #-} !Id -> Description (Term a)+    DSqrtTerm :: {-# UNPACK #-} !Id -> Description (Term a)+    DFPUnaryTerm :: FPUnaryOp -> {-# UNPACK #-} !Id -> Description (Term (FP eb sb))+    DFPBinaryTerm :: FPBinaryOp -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term (FP eb sb))+    DFPRoundingUnaryTerm :: FPRoundingUnaryOp -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term (FP eb sb))+    DFPRoundingBinaryTerm :: FPRoundingBinaryOp -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term (FP eb sb))+    DFPFMATerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term (FP eb sb))    describe (UConTerm v) = DConTerm v   describe ((USymTerm name) :: UTerm t) = DSymTerm @t name@@ -1566,6 +1860,15 @@   describe (UModIntegralTerm arg1 arg2) = DModIntegralTerm (identity arg1) (identity arg2)   describe (UQuotIntegralTerm arg1 arg2) = DRemIntegralTerm (identity arg1) (identity arg2)   describe (URemIntegralTerm arg1 arg2) = DQuotIntegralTerm (identity arg1) (identity arg2)+  describe (UFPTraitTerm trait arg) = DFPTraitTerm trait (identity arg)+  describe (UFdivTerm arg1 arg2) = DFdivTerm (identity arg1) (identity arg2)+  describe (URecipTerm arg) = DRecipTerm (identity arg)+  describe (USqrtTerm arg) = DSqrtTerm (identity arg)+  describe (UFPUnaryTerm op arg) = DFPUnaryTerm op (identity arg)+  describe (UFPBinaryTerm op arg1 arg2) = DFPBinaryTerm op (identity arg1) (identity arg2)+  describe (UFPRoundingUnaryTerm op mode arg) = DFPRoundingUnaryTerm op (identity mode) (identity arg)+  describe (UFPRoundingBinaryTerm op mode arg1 arg2) = DFPRoundingBinaryTerm op (identity mode) (identity arg1) (identity arg2)+  describe (UFPFMATerm mode arg1 arg2 arg3) = DFPFMATerm (identity mode) (identity arg1) (identity arg2) (identity arg3)    identify i = go     where@@ -1604,6 +1907,15 @@       go (UModIntegralTerm arg1 arg2) = ModIntegralTerm i arg1 arg2       go (UQuotIntegralTerm arg1 arg2) = QuotIntegralTerm i arg1 arg2       go (URemIntegralTerm arg1 arg2) = RemIntegralTerm i arg1 arg2+      go (UFPTraitTerm trait arg) = FPTraitTerm i trait arg+      go (UFdivTerm arg1 arg2) = FdivTerm i arg1 arg2+      go (URecipTerm arg) = RecipTerm i arg+      go (USqrtTerm arg) = SqrtTerm i arg+      go (UFPUnaryTerm op arg) = FPUnaryTerm i op arg+      go (UFPBinaryTerm op arg1 arg2) = FPBinaryTerm i op arg1 arg2+      go (UFPRoundingUnaryTerm op mode arg) = FPRoundingUnaryTerm i op mode arg+      go (UFPRoundingBinaryTerm op mode arg1 arg2) = FPRoundingBinaryTerm i op mode arg1 arg2+      go (UFPFMATerm mode arg1 arg2 arg3) = FPFMATerm i mode arg1 arg2 arg3   cache = termCache  instance (SupportedPrim t) => Eq (Description (Term t)) where@@ -1649,6 +1961,18 @@   DModIntegralTerm li1 li2 == DModIntegralTerm ri1 ri2 = li1 == ri1 && li2 == ri2   DQuotIntegralTerm li1 li2 == DQuotIntegralTerm ri1 ri2 = li1 == ri1 && li2 == ri2   DRemIntegralTerm li1 li2 == DRemIntegralTerm ri1 ri2 = li1 == ri1 && li2 == ri2+  DFPTraitTerm lt li == DFPTraitTerm rt ri = lt == rt && li == ri+  DFdivTerm li1 li2 == DFdivTerm ri1 ri2 = li1 == ri1 && li2 == ri2+  DRecipTerm li == DRecipTerm ri = li == ri+  DSqrtTerm li == DSqrtTerm ri = li == ri+  DFPUnaryTerm lop li == DFPUnaryTerm rop ri = lop == rop && li == ri+  DFPBinaryTerm lop li1 li2 == DFPBinaryTerm rop ri1 ri2 = lop == rop && li1 == ri1 && li2 == ri2+  DFPRoundingUnaryTerm lop lmode li == DFPRoundingUnaryTerm rop rmode ri =+    lop == rop && lmode == rmode && li == ri+  DFPRoundingBinaryTerm lop lmode li1 li2 == DFPRoundingBinaryTerm rop rmode ri1 ri2 =+    lop == rop && lmode == rmode && li1 == ri1 && li2 == ri2+  DFPFMATerm lmode li1 li2 li3 == DFPFMATerm rmode ri1 ri2 ri3 =+    lmode == rmode && li1 == ri1 && li2 == ri2 && li3 == ri3   _ == _ = False  instance (SupportedPrim t) => Hashable (Description (Term t)) where@@ -1707,6 +2031,18 @@   hashWithSalt s (DQuotIntegralTerm id1 id2) = s `hashWithSalt` (32 :: Int) `hashWithSalt` id1 `hashWithSalt` id2   hashWithSalt s (DRemIntegralTerm id1 id2) = s `hashWithSalt` (33 :: Int) `hashWithSalt` id1 `hashWithSalt` id2   hashWithSalt s (DApplyTerm id1 id2) = s `hashWithSalt` (38 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DFPTraitTerm trait id1) = s `hashWithSalt` (39 :: Int) `hashWithSalt` trait `hashWithSalt` id1+  hashWithSalt s (DFdivTerm id1 id2) = s `hashWithSalt` (40 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DRecipTerm id1) = s `hashWithSalt` (41 :: Int) `hashWithSalt` id1+  hashWithSalt s (DSqrtTerm id1) = s `hashWithSalt` (42 :: Int) `hashWithSalt` id1+  hashWithSalt s (DFPUnaryTerm op id1) = s `hashWithSalt` (43 :: Int) `hashWithSalt` op `hashWithSalt` id1+  hashWithSalt s (DFPBinaryTerm op id1 id2) = s `hashWithSalt` (44 :: Int) `hashWithSalt` op `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DFPRoundingUnaryTerm op mode id1) =+    s `hashWithSalt` (45 :: Int) `hashWithSalt` op `hashWithSalt` mode `hashWithSalt` id1+  hashWithSalt s (DFPRoundingBinaryTerm op mode id1 id2) =+    s `hashWithSalt` (46 :: Int) `hashWithSalt` op `hashWithSalt` mode `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DFPFMATerm mode id1 id2 id3) =+    s `hashWithSalt` (47 :: Int) `hashWithSalt` mode `hashWithSalt` id1 `hashWithSalt` id2 `hashWithSalt` id3  internTerm :: forall t. (SupportedPrim t) => Uninterned (Term t) -> Term t internTerm !bt = unsafeDupablePerformIO $ atomicModifyIORef' slot go@@ -1941,6 +2277,66 @@ remIntegralTerm :: (PEvalDivModIntegralTerm a) => Term a -> Term a -> Term a remIntegralTerm l r = internTerm $ URemIntegralTerm l r {-# INLINE remIntegralTerm #-}++fpTraitTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPTrait ->+  Term (FP eb sb) ->+  Term Bool+fpTraitTerm trait v = internTerm $ UFPTraitTerm trait v++fdivTerm :: (PEvalFractionalTerm a) => Term a -> Term a -> Term a+fdivTerm l r = internTerm $ UFdivTerm l r+{-# INLINE fdivTerm #-}++recipTerm :: (PEvalFractionalTerm a) => Term a -> Term a+recipTerm = internTerm . URecipTerm+{-# INLINE recipTerm #-}++sqrtTerm :: (PEvalFloatingTerm a) => Term a -> Term a+sqrtTerm = internTerm . USqrtTerm+{-# INLINE sqrtTerm #-}++fpUnaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPUnaryOp ->+  Term (FP eb sb) ->+  Term (FP eb sb)+fpUnaryTerm op v = internTerm $ UFPUnaryTerm op v++fpBinaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPBinaryOp ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb)+fpBinaryTerm op l r = internTerm $ UFPBinaryTerm op l r++fpRoundingUnaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPRoundingUnaryOp ->+  Term FPRoundingMode ->+  Term (FP eb sb) ->+  Term (FP eb sb)+fpRoundingUnaryTerm op mode v = internTerm $ UFPRoundingUnaryTerm op mode v++fpRoundingBinaryTerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>+  FPRoundingBinaryOp ->+  Term FPRoundingMode ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb)+fpRoundingBinaryTerm op mode l r = internTerm $ UFPRoundingBinaryTerm op mode l r++fpFMATerm ::+  (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) =>+  Term FPRoundingMode ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb) ->+  Term (FP eb sb)+fpFMATerm mode l r s = internTerm $ UFPFMATerm mode l r s  -- Support for boolean type defaultValueForBool :: Bool

@@ -1,3 +1,4 @@+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -13,6 +14,8 @@ module Grisette.Internal.SymPrim.Prim.Internal.Unfold   ( unaryUnfoldOnce,     binaryUnfoldOnce,+    generalUnaryUnfolded,+    generalBinaryUnfolded,   ) where @@ -28,7 +31,8 @@   ) import Grisette.Internal.SymPrim.Prim.Internal.Term   ( SupportedPrim (pevalITETerm),-    Term (ITETerm),+    Term (ConTerm, ITETerm),+    conTerm,   )  unaryPartialUnfoldOnce ::@@ -112,3 +116,32 @@   TotalRuleBinary a b c ->   TotalRuleBinary a b c binaryUnfoldOnce partial fallback = totalize2 (binaryPartialUnfoldOnce partial fallback) fallback++generalUnaryUnfolded ::+  forall a b.+  (Typeable a, SupportedPrim b) =>+  (a -> b) ->+  (Term a -> Term b) ->+  Term a ->+  Term b+generalUnaryUnfolded compute =+  unaryUnfoldOnce+    ( \case+        ConTerm _ lv -> Just $ conTerm $ compute lv+        _ -> Nothing+    )++generalBinaryUnfolded ::+  forall a b c.+  (Typeable a, Typeable b, SupportedPrim c) =>+  (a -> b -> c) ->+  (Term a -> Term b -> Term c) ->+  Term a ->+  Term b ->+  Term c+generalBinaryUnfolded compute =+  binaryUnfoldOnce+    ( \l r -> case (l, r) of+        (ConTerm _ lv, ConTerm _ rv) -> Just $ conTerm $ compute lv rv+        _ -> Nothing+    )

@@ -60,6 +60,15 @@   ) import Grisette.Internal.Core.Data.MemoUtils (htmemo) import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))+import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP+  ( pevalFPBinaryTerm,+    pevalFPFMATerm,+    pevalFPRoundingBinaryTerm,+    pevalFPRoundingUnaryTerm,+    pevalFPTraitTerm,+    pevalFPUnaryTerm,+  )+import Grisette.Internal.SymPrim.Prim.Internal.Term (Term (FPFMATerm)) import Grisette.Internal.SymPrim.Prim.ModelValue   ( ModelValue,     toModelValue,@@ -85,6 +94,8 @@         pevalQuotIntegralTerm,         pevalRemIntegralTerm       ),+    PEvalFloatingTerm (pevalSqrtTerm),+    PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),     PEvalNumTerm       ( pevalAbsNumTerm,         pevalAddNumTerm,@@ -114,6 +125,12 @@         ConTerm,         DivIntegralTerm,         EqTerm,+        FPBinaryTerm,+        FPRoundingBinaryTerm,+        FPRoundingUnaryTerm,+        FPTraitTerm,+        FPUnaryTerm,+        FdivTerm,         ITETerm,         LeOrdTerm,         LtOrdTerm,@@ -124,12 +141,14 @@         OrBitsTerm,         OrTerm,         QuotIntegralTerm,+        RecipTerm,         RemIntegralTerm,         RotateLeftTerm,         RotateRightTerm,         ShiftLeftTerm,         ShiftRightTerm,         SignumNumTerm,+        SqrtTerm,         SymTerm,         TernaryTerm,         ToSignedTerm,@@ -462,6 +481,20 @@       goBinary pevalQuotIntegralTerm arg1 arg2     go (SomeTerm (RemIntegralTerm _ arg1 arg2)) =       goBinary pevalRemIntegralTerm arg1 arg2+    go (SomeTerm (FPTraitTerm _ trait arg)) =+      goUnary (pevalFPTraitTerm trait) arg+    go (SomeTerm (FdivTerm _ arg1 arg2)) = goBinary pevalFdivTerm arg1 arg2+    go (SomeTerm (RecipTerm _ arg)) = goUnary pevalRecipTerm arg+    go (SomeTerm (SqrtTerm _ arg)) = goUnary pevalSqrtTerm arg+    go (SomeTerm (FPUnaryTerm _ op arg)) = goUnary (pevalFPUnaryTerm op) arg+    go (SomeTerm (FPBinaryTerm _ op arg1 arg2)) =+      goBinary (pevalFPBinaryTerm op) arg1 arg2+    go (SomeTerm (FPRoundingUnaryTerm _ op mode arg)) =+      goUnary (pevalFPRoundingUnaryTerm op mode) arg+    go (SomeTerm (FPRoundingBinaryTerm _ op mode arg1 arg2)) =+      goBinary (pevalFPRoundingBinaryTerm op mode) arg1 arg2+    go (SomeTerm (FPFMATerm _ mode arg1 arg2 arg3)) =+      SomeTerm $ pevalFPFMATerm (gotyped mode) (gotyped arg1) (gotyped arg2) (gotyped arg3)     goUnary :: (SupportedPrim a, SupportedPrim b) => (Term a -> Term b) -> Term a -> SomeTerm     goUnary f a = SomeTerm $ f (gotyped a)     goBinary ::

@@ -10,6 +10,7 @@ -- Portability :   GHC only module Grisette.Internal.SymPrim.Prim.Term   ( module Grisette.Internal.SymPrim.Prim.Internal.Term,+    module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP,     module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm,     module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm,     module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm,@@ -21,6 +22,9 @@ import Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval () import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm () import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm+import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP+import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm ()+import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm () import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm

@@ -53,6 +53,13 @@         ConTerm,         DivIntegralTerm,         EqTerm,+        FPBinaryTerm,+        FPFMATerm,+        FPRoundingBinaryTerm,+        FPRoundingUnaryTerm,+        FPTraitTerm,+        FPUnaryTerm,+        FdivTerm,         ITETerm,         LeOrdTerm,         LtOrdTerm,@@ -63,12 +70,14 @@         OrBitsTerm,         OrTerm,         QuotIntegralTerm,+        RecipTerm,         RemIntegralTerm,         RotateLeftTerm,         RotateRightTerm,         ShiftLeftTerm,         ShiftRightTerm,         SignumNumTerm,+        SqrtTerm,         SymTerm,         TernaryTerm,         ToSignedTerm,@@ -133,6 +142,20 @@     go (SomeTerm (ModIntegralTerm _ arg1 arg2)) = goBinary arg1 arg2     go (SomeTerm (QuotIntegralTerm _ arg1 arg2)) = goBinary arg1 arg2     go (SomeTerm (RemIntegralTerm _ arg1 arg2)) = goBinary arg1 arg2+    go (SomeTerm (FPTraitTerm _ _ arg)) = goUnary arg+    go (SomeTerm (FdivTerm _ arg1 arg2)) = goBinary arg1 arg2+    go (SomeTerm (RecipTerm _ arg)) = goUnary arg+    go (SomeTerm (SqrtTerm _ arg)) = goUnary arg+    go (SomeTerm (FPUnaryTerm _ _ arg)) = goUnary arg+    go (SomeTerm (FPBinaryTerm _ _ arg1 arg2)) = goBinary arg1 arg2+    go (SomeTerm (FPRoundingUnaryTerm _ _ _ arg)) = goUnary arg+    go (SomeTerm (FPRoundingBinaryTerm _ _ _ arg1 arg2)) = goBinary arg1 arg2+    go (SomeTerm (FPFMATerm _ mode arg1 arg2 arg3)) = do+      m <- gocached (SomeTerm mode)+      r1 <- gocached (SomeTerm arg1)+      r2 <- gocached (SomeTerm arg2)+      r3 <- gocached (SomeTerm arg3)+      return $ m <> r1 <> r2 <> r3     goUnary arg = gocached (SomeTerm arg)     goBinary arg1 arg2 = do       r1 <- gocached (SomeTerm arg1)@@ -185,6 +208,15 @@ castTerm t@ModIntegralTerm {} = cast t castTerm t@QuotIntegralTerm {} = cast t castTerm t@RemIntegralTerm {} = cast t+castTerm t@FPTraitTerm {} = cast t+castTerm t@FdivTerm {} = cast t+castTerm t@RecipTerm {} = cast t+castTerm t@SqrtTerm {} = cast t+castTerm t@FPUnaryTerm {} = cast t+castTerm t@FPBinaryTerm {} = cast t+castTerm t@FPRoundingUnaryTerm {} = cast t+castTerm t@FPRoundingBinaryTerm {} = cast t+castTerm t@FPFMATerm {} = cast t {-# INLINE castTerm #-}  someTermsSize :: [SomeTerm] -> Int@@ -230,6 +262,15 @@     go t@(ModIntegralTerm _ arg1 arg2) = goBinary t arg1 arg2     go t@(QuotIntegralTerm _ arg1 arg2) = goBinary t arg1 arg2     go t@(RemIntegralTerm _ arg1 arg2) = goBinary t arg1 arg2+    go t@(FPTraitTerm _ _ arg) = goUnary t arg+    go t@(FdivTerm _ arg1 arg2) = goBinary t arg1 arg2+    go t@(RecipTerm _ arg) = goUnary t arg+    go t@(SqrtTerm _ arg) = goUnary t arg+    go t@(FPUnaryTerm _ _ arg) = goUnary t arg+    go t@(FPBinaryTerm _ _ arg1 arg2) = goBinary t arg1 arg2+    go t@(FPRoundingUnaryTerm _ _ _ arg) = goUnary t arg+    go t@(FPRoundingBinaryTerm _ _ _ arg1 arg2) = goBinary t arg1 arg2+    go t@(FPFMATerm _ _ arg1 arg2 arg3) = goTernary t arg1 arg2 arg3     goUnary :: forall a b. (SupportedPrim a) => Term a -> Term b -> State (S.HashSet SomeTerm) ()     goUnary t arg = do       b <- exists t

@@ -204,6 +204,28 @@ -- >>> :set -XFunctionalDependencies  -- | Non-indexed bitvectors.+--+-- The creation of 'SomeBV' can be done with the `bv` function with a positive+-- bit width and a value:+--+-- >>> bv 4 0xf :: SomeBV IntN+-- 0xf+--+-- Operations on two 'SomeBV' values require the bitwidths to be the same. So+-- you should check for the bit width (via `finiteBitSize`) before performing+-- operations:+--+-- >>> bv 4 0x3 + bv 4 0x3 :: SomeBV IntN+-- 0x6+-- >>> bv 4 0x3 + bv 8 0x3 :: SomeBV IntN+-- *** Exception: BitwidthMismatch+--+-- One exception is that the equality testing (both concrete and symbolic via+-- 'SEq') does not require the bitwidths to be the same. Different bitwidths+-- means the values are not equal:+--+-- >>> (bv 4 0x3 :: SomeBV IntN) == (bv 8 0x3)+-- False data SomeBV bv where   SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv @@ -236,9 +258,15 @@   {-# INLINE rnf #-}  instance (forall n. (KnownNat n, 1 <= n) => Eq (bv n)) => Eq (SomeBV bv) where-  (==) = binSomeBV (==)+  SomeBV (l :: bv l) == SomeBV (r :: bv r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l == r+      Nothing -> False   {-# INLINE (==) #-}-  (/=) = binSomeBV (/=)+  SomeBV (l :: bv l) /= SomeBV (r :: bv r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l /= r+      Nothing -> True   {-# INLINE (/=) #-}  instance (forall n. (KnownNat n, 1 <= n) => Ord (bv n)) => Ord (SomeBV bv) where@@ -483,9 +511,15 @@       )  instance (forall n. (KnownNat n, 1 <= n) => SEq (bv n)) => SEq (SomeBV bv) where-  (.==) = binSomeBV (.==)+  SomeBV (l :: bv l) .== SomeBV (r :: bv r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l .== r+      Nothing -> con False   {-# INLINE (.==) #-}-  (./=) = binSomeBV (./=)+  SomeBV (l :: bv l) ./= SomeBV (r :: bv r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l ./= r+      Nothing -> con True   {-# INLINE (./=) #-}  instance

@@ -0,0 +1,169 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveLift #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Grisette.Internal.SymPrim.SymFP+  ( SymFP (SymFP),+    SymFP16,+    SymFP32,+    SymFP64,+    SymFPRoundingMode (..),+  )+where++import Control.DeepSeq (NFData)+import Data.Hashable (Hashable (hashWithSalt))+import Data.String (IsString (fromString))+import GHC.Generics (Generic)+import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))+import Grisette.Internal.Core.Data.Class.Solvable+  ( Solvable (con, conView, ssym, sym),+  )+import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSymsS), SomeSym (SomeSym))+import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)+import Grisette.Internal.SymPrim.Prim.Internal.Term+  ( ConRep (ConType),+    LinkedRep (underlyingTerm, wrapTerm),+    PEvalFloatingTerm (pevalSqrtTerm),+    PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),+    PEvalNumTerm+      ( pevalAbsNumTerm,+        pevalAddNumTerm,+        pevalMulNumTerm,+        pevalNegNumTerm,+        pevalSignumNumTerm+      ),+    SymRep (SymType),+    Term (ConTerm),+    conTerm,+    pevalSubNumTerm,+    pformat,+    symTerm,+  )+import Language.Haskell.TH.Syntax (Lift)++-- | Symbolic IEEE 754 floating-point number with @eb@ exponent bits and @sb@+-- significand bits.+newtype SymFP eb sb = SymFP {underlyingFPTerm :: Term (FP eb sb)}+  deriving (Lift, Generic)+  deriving anyclass (NFData)++-- | Symbolic IEEE 754 half-precision floating-point number.+type SymFP16 = SymFP 5 11++-- | Symbolic IEEE 754 single-precision floating-point number.+type SymFP32 = SymFP 8 24++-- | Symbolic IEEE 754 double-precision floating-point number.+type SymFP64 = SymFP 11 53++instance ConRep (SymFP eb sb) where+  type ConType (SymFP eb sb) = FP eb sb++instance (ValidFP eb sb) => SymRep (FP eb sb) where+  type SymType (FP eb sb) = SymFP eb sb++instance (ValidFP eb sb) => LinkedRep (FP eb sb) (SymFP eb sb) where+  underlyingTerm (SymFP a) = a+  wrapTerm = SymFP++instance (ValidFP eb sb) => Apply (SymFP eb sb) where+  type FunType (SymFP eb sb) = SymFP eb sb+  apply = id++instance (ValidFP eb sb) => Eq (SymFP eb sb) where+  SymFP a == SymFP b = a == b++instance (ValidFP eb sb) => Hashable (SymFP eb sb) where+  hashWithSalt s (SymFP a) = hashWithSalt s a++instance (ValidFP eb sb) => IsString (SymFP eb sb) where+  fromString = ssym . fromString++instance (ValidFP eb sb) => Solvable (FP eb sb) (SymFP eb sb) where+  con = SymFP . conTerm+  sym = SymFP . symTerm+  conView (SymFP (ConTerm _ t)) = Just t+  conView _ = Nothing++instance (ValidFP eb sb) => Show (SymFP eb sb) where+  show (SymFP a) = pformat a++instance (ValidFP eb sb) => AllSyms (SymFP eb sb) where+  allSymsS v = (SomeSym v :)++instance (ValidFP eb sb) => Num (SymFP eb sb) where+  (SymFP l) + (SymFP r) = SymFP $ pevalAddNumTerm l r+  (SymFP l) - (SymFP r) = SymFP $ pevalSubNumTerm l r+  (SymFP l) * (SymFP r) = SymFP $ pevalMulNumTerm l r+  negate (SymFP v) = SymFP $ pevalNegNumTerm v+  abs (SymFP v) = SymFP $ pevalAbsNumTerm v+  signum (SymFP v) = SymFP $ pevalSignumNumTerm v+  fromInteger = con . fromInteger++instance (ValidFP eb sb) => Fractional (SymFP eb sb) where+  (SymFP l) / (SymFP r) = SymFP $ pevalFdivTerm l r+  recip (SymFP v) = SymFP $ pevalRecipTerm v+  fromRational = con . fromRational++instance (ValidFP eb sb) => Floating (SymFP eb sb) where+  pi = error "pi isn't supported by the underlying sbv library"+  exp = error "exp isn't supported by the underlying sbv library"+  log = error "log isn't supported by the underlying sbv library"+  sqrt (SymFP v) = SymFP $ pevalSqrtTerm v+  (**) = error "(**) isn't supported by the underlying sbv library"+  logBase = error "logBase isn't supported by the underlying sbv library"+  sin = error "sin isn't supported by the underlying sbv library"+  cos = error "cos isn't supported by the underlying sbv library"+  asin = error "asin isn't supported by the underlying sbv library"+  acos = error "acos isn't supported by the underlying sbv library"+  atan = error "atan isn't supported by the underlying sbv library"+  sinh = error "sinh isn't supported by the underlying sbv library"+  cosh = error "cosh isn't supported by the underlying sbv library"+  asinh = error "asinh isn't supported by the underlying sbv library"+  acosh = error "acosh isn't supported by the underlying sbv library"+  atanh = error "atanh isn't supported by the underlying sbv library"++newtype SymFPRoundingMode = SymFPRoundingMode (Term FPRoundingMode)+  deriving (Lift, Generic)+  deriving anyclass (NFData)++instance ConRep SymFPRoundingMode where+  type ConType SymFPRoundingMode = FPRoundingMode++instance SymRep FPRoundingMode where+  type SymType FPRoundingMode = SymFPRoundingMode++instance LinkedRep FPRoundingMode SymFPRoundingMode where+  underlyingTerm (SymFPRoundingMode a) = a+  wrapTerm = SymFPRoundingMode++instance Apply SymFPRoundingMode where+  type FunType SymFPRoundingMode = SymFPRoundingMode+  apply = id++instance Eq SymFPRoundingMode where+  SymFPRoundingMode a == SymFPRoundingMode b = a == b++instance Hashable SymFPRoundingMode where+  hashWithSalt s (SymFPRoundingMode a) = hashWithSalt s a++instance IsString SymFPRoundingMode where+  fromString = ssym . fromString++instance Solvable FPRoundingMode SymFPRoundingMode where+  con = SymFPRoundingMode . conTerm+  sym = SymFPRoundingMode . symTerm+  conView (SymFPRoundingMode (ConTerm _ t)) = Just t+  conView _ = Nothing++instance Show SymFPRoundingMode where+  show (SymFPRoundingMode a) = pformat a++instance AllSyms SymFPRoundingMode where+  allSymsS v = (SomeSym v :)

@@ -1,6 +1,7 @@ {-# LANGUAGE BinaryLiterals #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-}@@ -14,13 +15,15 @@ import GHC.Stack (HasCallStack) import Grisette   ( Apply (apply),-    CEGISResult (CEGISSuccess),+    CEGISResult (CEGISSolverFailure, CEGISSuccess, CEGISVerifierFailure),     EvaluateSym (evaluateSym),     ExtractSymbolics,     Function ((#)),     GrisetteSMTConfig,     ITEOp (symIte),     LogicalOp (symNot, symXor, (.&&), (.||)),+    ModelRep (buildModel),+    ModelValuePair ((::=)),     SEq ((.==)),     SOrd ((.<), (.>=)),     SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext),@@ -29,6 +32,7 @@     VerificationConditions,     cegis,     cegisExceptVC,+    cegisForAll,     cegisForAllExceptVC,     cegisMultiInputs,     cegisPostCond,@@ -48,7 +52,7 @@   ) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase)-import Test.HUnit (Assertion, assertFailure, (@=?))+import Test.HUnit (Assertion, assertFailure, (@=?), (@?=))  testCegis ::   (HasCallStack, ExtractSymbolics a, EvaluateSym a, Show a, SEq a) =>@@ -404,5 +408,70 @@                                 .== (con 1 :: SymIntN 10)                             ]                     ]-                ]+                ],+          testCase "cegisMultiInputs" $ do+            r <-+              cegisMultiInputs+                unboundedConfig+                [["a" :: SymInteger], ["b", "c"]]+                ( \case+                    [a] ->+                      cegisPostCond $+                        symIte+                          (a .== 1)+                          "x"+                          ("x" .&& symNot "y")+                    [b, _] ->+                      cegisPostCond $+                        symIte+                          (b .== 1)+                          (symIte "x" "z" "w")+                          (symIte "x" (symNot "w") (symNot "z"))+                    _ -> cegisPostCond $ con True+                )+            case snd r of+              CEGISSuccess m -> do+                let expectedModel =+                      buildModel+                        ( "x" ::= True,+                          "y" ::= False,+                          "z" ::= True,+                          "w" ::= False+                        )+                m @?= expectedModel+              CEGISVerifierFailure _ -> fail "Verifier failed"+              CEGISSolverFailure failure -> fail $ show failure,+          testCase "cegisForAll" $ do+            let a = "a" :: SymInteger+            let b = "b"+            r <-+              cegisForAll+                unboundedConfig+                [a, b]+                ( cegisPostCond $+                    symIte+                      (a .== 1)+                      ( symIte+                          (b .== 1)+                          "x"+                          ("x" .&& symNot "y")+                      )+                      ( symIte+                          (b .== 1)+                          (symIte "x" "z" "w")+                          (symIte "x" (symNot "w") (symNot "z"))+                      )+                )+            case snd r of+              CEGISSuccess m -> do+                let expectedModel =+                      buildModel+                        ( "x" ::= True,+                          "y" ::= False,+                          "z" ::= True,+                          "w" ::= False+                        )+                m @?= expectedModel+              CEGISVerifierFailure _ -> fail "Verifier failed"+              CEGISSolverFailure failure -> fail $ show failure         ]

@@ -38,16 +38,19 @@   ( GrisetteSMTConfig (sbvConfig),     approx,     lowerSinglePrim,+    lowerSinglePrimCached,     precise,   ) import Grisette.Internal.Backend.SymBiMap   ( SymBiMap (biMapToSBV),   )+import Grisette.Internal.SymPrim.FP (FP32) import Grisette.Internal.SymPrim.Prim.SomeTerm   ( SomeTerm (SomeTerm),   ) import Grisette.Internal.SymPrim.Prim.Term-  ( SBVRep (SBVType),+  ( FPTrait (FPIsInfinite, FPIsNaN, FPIsNegative, FPIsNegativeInfinite, FPIsNegativeZero, FPIsNormal, FPIsPoint, FPIsPositive, FPIsPositiveInfinite, FPIsPositiveZero, FPIsSubnormal, FPIsZero),+    SBVRep (SBVType),     SupportedPrim,     Term,     absNumTerm,@@ -59,8 +62,10 @@     bvsignExtendTerm,     bvzeroExtendTerm,     complementBitsTerm,+    conTerm,     divIntegralTerm,     eqTerm,+    fpTraitTerm,     iteTerm,     leOrdTerm,     ltOrdTerm,@@ -70,6 +75,9 @@     notTerm,     orBitsTerm,     orTerm,+    pevalAndTerm,+    pevalFPTraitTerm,+    pevalNotTerm,     quotIntegralTerm,     remIntegralTerm,     rotateLeftTerm,@@ -130,22 +138,6 @@           SBV.Unsat -> return ()           _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula" --- testUnaryOpLowering' ::---   forall a b as n tag.---   ( HasCallStack,---     UnaryOp tag a b,---     SBV.EqSymbolic (SBVType n b),---     Typeable (SBVType n a),---     SBV.SymVal as,---     SBVType n a ~ SBV.SBV as,---     Show as---   ) =>---   GrisetteSMTConfig n ->---   tag ->---   (SBVType n a -> SBVType n b) ->---   Assertion--- testUnaryOpLowering' config t = testUnaryOpLowering @a @b @as config (constructUnary t) (show t)- testBinaryOpLowering ::   forall a b c as bs n.   ( HasCallStack,@@ -199,26 +191,6 @@           _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula"       _ -> lift $ assertFailure "Failed to extract the term" --- testBinaryOpLowering' ::---   forall a b c as bs n tag.---   ( HasCallStack,---     BinaryOp tag a b c,---     SBV.EqSymbolic (SBVType n c),---     Typeable (SBVType n a),---     Typeable (SBVType n b),---     SBV.SymVal as,---     SBV.SymVal bs,---     Show as,---     Show bs,---     SBVType n a ~ SBV.SBV as,---     SBVType n b ~ SBV.SBV bs---   ) =>---   GrisetteSMTConfig n ->---   tag ->---   (SBVType n a -> SBVType n b -> SBVType n c) ->---   Assertion--- testBinaryOpLowering' config t = testBinaryOpLowering @a @b @c @as @bs config (constructBinary t) (show t)- testTernaryOpLowering ::   forall a b c d as bs cs n.   ( HasCallStack,@@ -240,11 +212,12 @@     SBVType n c ~ SBV.SBV cs   ) =>   GrisetteSMTConfig n ->+  (Term a -> Term b -> Term c -> Term Bool) ->   (Term a -> Term b -> Term c -> Term d) ->   T.Text ->   (SBVType n a -> SBVType n b -> SBVType n c -> SBVType n d) ->   Assertion-testTernaryOpLowering config f name sbvfun = do+testTernaryOpLowering config precond f name sbvfun = do   let a :: Term a = ssymTerm "a"   let b :: Term b = ssymTerm "b"   let c :: Term c = ssymTerm "c"@@ -264,12 +237,13 @@       _ -> lift $ assertFailure "Failed to extract the term"   SBV.runSMTWith (sbvConfig config) $ do     (m, lt) <- lowerSinglePrim config fabc-    let sbva :: Maybe (SBVType n a) = M.lookup (SomeTerm a) (biMapToSBV m) >>= fromDynamic-    let sbvb :: Maybe (SBVType n b) = M.lookup (SomeTerm b) (biMapToSBV m) >>= fromDynamic-    let sbvc :: Maybe (SBVType n c) = M.lookup (SomeTerm c) (biMapToSBV m) >>= fromDynamic+    (m2, p) <- lowerSinglePrimCached config (precond a b c) m+    let sbva :: Maybe (SBVType n a) = M.lookup (SomeTerm a) (biMapToSBV m2) >>= fromDynamic+    let sbvb :: Maybe (SBVType n b) = M.lookup (SomeTerm b) (biMapToSBV m2) >>= fromDynamic+    let sbvc :: Maybe (SBVType n c) = M.lookup (SomeTerm c) (biMapToSBV m2) >>= fromDynamic     case (sbva, sbvb, sbvc) of       (Just sbvav, Just sbvbv, Just sbvcv) -> SBV.query $ do-        SBV.constrain $ lt SBV../= sbvfun sbvav sbvbv sbvcv+        SBV.constrain $ (lt SBV../= sbvfun sbvav sbvbv sbvcv) SBV..&& p         r <- SBV.checkSat         case r of           SBV.Sat -> do@@ -284,30 +258,6 @@           _ -> lift $ assertFailure $ T.unpack $ "Lowering for " <> name <> " generated unknown formula"       _ -> lift $ assertFailure "Failed to extract the term" --- testTernaryOpLowering' ::---   forall a b c d as bs cs n tag.---   ( HasCallStack,---     TernaryOp tag a b c d,---     SBV.EqSymbolic (SBVType n d),---     Typeable (SBVType n a),---     Typeable (SBVType n b),---     Typeable (SBVType n c),---     SBV.SymVal as,---     SBV.SymVal bs,---     SBV.SymVal cs,---     Show as,---     Show bs,---     Show cs,---     SBVType n a ~ SBV.SBV as,---     SBVType n b ~ SBV.SBV bs,---     SBVType n c ~ SBV.SBV cs---   ) =>---   GrisetteSMTConfig n ->---   tag ->---   (SBVType n a -> SBVType n b -> SBVType n c -> SBVType n d) ->---   Assertion--- testTernaryOpLowering' config t = testTernaryOpLowering @a @b @c @d @as @bs @cs config (constructTernary t) (show t)- loweringTests :: Test loweringTests =   let unboundedConfig = precise SBV.z3@@ -340,11 +290,18 @@                   "eqv"                   (\x y -> SBV.sNot (x SBV..<+> y)),               testCase "ITE" $ do-                testTernaryOpLowering @Bool @Bool @Bool @Bool unboundedConfig iteTerm "ite" SBV.ite+                let truePrecond _ _ _ = conTerm True                 testTernaryOpLowering @Bool @Bool @Bool @Bool                   unboundedConfig+                  truePrecond                   iteTerm                   "ite"+                  SBV.ite+                testTernaryOpLowering @Bool @Bool @Bool @Bool+                  unboundedConfig+                  truePrecond+                  iteTerm+                  "ite"                   (\c x y -> (c SBV..=> x) SBV..&& (SBV.sNot c SBV..=> y))             ],           testGroup@@ -802,6 +759,53 @@               testCase "ToSigned" $ do                 testUnaryOpLowering @(WordN 5) @(IntN 5) unboundedConfig toSignedTerm "toSigned" SBV.sFromIntegral                 testUnaryOpLowering @(WordN 5) @(IntN 5) boundedConfig toSignedTerm "toSigned" SBV.sFromIntegral+            ],+          testGroup+            "FP"+            [ testCase "Eqv" $+                testBinaryOpLowering @FP32 @FP32 @Bool unboundedConfig eqTerm "eqv" (SBV..==),+              testCase "ITE" $ do+                let precond _ l r =+                      pevalAndTerm+                        ( pevalNotTerm $+                            pevalFPTraitTerm FPIsNaN (l :: Term FP32)+                        )+                        ( pevalNotTerm $+                            pevalFPTraitTerm FPIsNaN (r :: Term FP32)+                        )+                testTernaryOpLowering @Bool @FP32 @FP32 @FP32+                  unboundedConfig+                  precond+                  iteTerm+                  "ite"+                  SBV.ite,+              testGroup "FPTrait" $ do+                (name, trait, op) <-+                  [ ("isNaN", FPIsNaN, SBV.fpIsNaN),+                    ("isPositive", FPIsPositive, SBV.fpIsPositive),+                    ("isNegative", FPIsNegative, SBV.fpIsNegative),+                    ( "isPositiveInfinite",+                      FPIsPositiveInfinite,+                      \x -> SBV.fpIsPositive x SBV..&& SBV.fpIsInfinite x+                    ),+                    ( "isNegativeInfinite",+                      FPIsNegativeInfinite,+                      \x -> SBV.fpIsNegative x SBV..&& SBV.fpIsInfinite x+                    ),+                    ("isInfinite", FPIsInfinite, SBV.fpIsInfinite),+                    ("isPositiveZero", FPIsPositiveZero, SBV.fpIsPositiveZero),+                    ("isNegativeZero", FPIsNegativeZero, SBV.fpIsNegativeZero),+                    ("isZero", FPIsZero, SBV.fpIsZero),+                    ("isNormal", FPIsNormal, SBV.fpIsNormal),+                    ("isSubnormal", FPIsSubnormal, SBV.fpIsSubnormal),+                    ("isPoint", FPIsPoint, SBV.fpIsPoint)+                    ]+                return $ testCase name $ do+                  testUnaryOpLowering @FP32 @Bool+                    unboundedConfig+                    (fpTraitTerm trait)+                    "isNaN"+                    op             ],           testCase "TabularFun" $ do             let f = "f" :: SymInteger =~> SymInteger =~> SymInteger

@@ -23,8 +23,11 @@     BoolWithLIASpec (..),     LIAWithBoolSpec (..),     BoolOnlySpec (..),+    constructUnarySpec,     constructUnarySpec',+    constructBinarySpec,     constructBinarySpec',+    constructTernarySpec,     constructTernarySpec',     divIntegralSpec,     modIntegralSpec,@@ -34,6 +37,9 @@     mulNumSpec,     addNumSpec,     absNumSpec,+    signumNumSpec,+    ltOrdSpec,+    leOrdSpec,     iteSpec,     eqvSpec,     notSpec,@@ -44,17 +50,66 @@     rotateLeftSpec,     rotateRightSpec,     xorBitsSpec,+    fpTraitSpec,+    fdivSpec,+    recipSpec,+    sqrtSpec,+    fpUnaryOpSpec,+    fpBinaryOpSpec,+    fpRoundingUnaryOpSpec,+    fpRoundingBinarySpec,+    fpFMASpec,+    IEEEFP32Spec (..),+    IEEEFP32BoolOpSpec (..),+    FPRoundingModeSpec (..),+    FPRoundingModeBoolOpSpec (..),   ) where  import Data.Bits (FiniteBits) import Data.Data (Proxy (Proxy), Typeable)+import Data.Functor ((<&>)) import Data.Kind (Type) import qualified Data.Text as T import GHC.TypeLits (KnownNat, Nat, type (+), type (<=)) import Grisette (Identifier, SizedBV, SymRotate, SymShift, withInfo)+import Grisette.Internal.SymPrim.FP+  ( FP,+    FP32,+    FPRoundingMode (RNA, RNE, RTN, RTP, RTZ),+    ValidFP,+  )+import Grisette.Internal.SymPrim.Prim.Internal.Term+  ( FPBinaryOp (FPMax, FPMin, FPRem),+    FPRoundingBinaryOp (FPAdd, FPDiv, FPMul, FPSub),+    FPRoundingUnaryOp (FPRoundToIntegral, FPSqrt),+    FPUnaryOp (FPAbs, FPNeg),+    PEvalFloatingTerm (pevalSqrtTerm),+    PEvalFractionalTerm (pevalRecipTerm),+    fdivTerm,+    fpBinaryTerm,+    fpFMATerm,+    fpRoundingBinaryTerm,+    fpRoundingUnaryTerm,+    fpUnaryTerm,+    sqrtTerm,+  ) import Grisette.Internal.SymPrim.Prim.Term   ( BinaryOp (pevalBinary),+    FPTrait+      ( FPIsInfinite,+        FPIsNaN,+        FPIsNegative,+        FPIsNegativeInfinite,+        FPIsNegativeZero,+        FPIsNormal,+        FPIsPoint,+        FPIsPositive,+        FPIsPositiveInfinite,+        FPIsPositiveZero,+        FPIsSubnormal,+        FPIsZero+      ),     PEvalBVTerm       ( pevalBVConcatTerm,         pevalBVExtendTerm,@@ -72,6 +127,7 @@         pevalQuotIntegralTerm,         pevalRemIntegralTerm       ),+    PEvalFractionalTerm (pevalFdivTerm),     PEvalNumTerm       ( pevalAbsNumTerm,         pevalAddNumTerm,@@ -106,6 +162,7 @@     constructUnary,     divIntegralTerm,     eqTerm,+    fpTraitTerm,     iteTerm,     leOrdTerm,     ltOrdTerm,@@ -117,10 +174,17 @@     orTerm,     pevalAndTerm,     pevalEqTerm,+    pevalFPBinaryTerm,+    pevalFPFMATerm,+    pevalFPRoundingBinaryTerm,+    pevalFPRoundingUnaryTerm,+    pevalFPTraitTerm,+    pevalFPUnaryTerm,     pevalNotTerm,     pevalOrTerm,     pformat,     quotIntegralTerm,+    recipTerm,     remIntegralTerm,     rotateLeftTerm,     rotateRightTerm,@@ -130,8 +194,10 @@     ssymTerm,     xorBitsTerm,   )-import Test.QuickCheck (Arbitrary (arbitrary), Gen, frequency, oneof, sized)+import Test.QuickCheck (Arbitrary (arbitrary), Gen, elements, frequency, oneof, sized) +-- import Grisette.Internal.SymPrim.FP (FPRoundingMode(RNE))+ class (SupportedPrim b) => TermRewritingSpec a b | a -> b where   norewriteVer :: a -> Term b   rewriteVer :: a -> Term b@@ -363,6 +429,84 @@ remIntegralSpec :: (TermRewritingSpec a b, PEvalDivModIntegralTerm b) => a -> a -> a remIntegralSpec = constructBinarySpec remIntegralTerm pevalRemIntegralTerm +fpTraitSpec ::+  ( ValidFP eb fb,+    TermRewritingSpec a (FP eb fb),+    TermRewritingSpec b Bool+  ) =>+  FPTrait ->+  a ->+  b+fpTraitSpec trait = constructUnarySpec (fpTraitTerm trait) (pevalFPTraitTerm trait)++fdivSpec :: (TermRewritingSpec a av, PEvalFractionalTerm av) => a -> a -> a+fdivSpec = constructBinarySpec fdivTerm pevalFdivTerm++recipSpec :: (TermRewritingSpec a av, PEvalFractionalTerm av) => a -> a+recipSpec = constructUnarySpec recipTerm pevalRecipTerm++sqrtSpec :: (TermRewritingSpec a av, PEvalFloatingTerm av) => a -> a+sqrtSpec = constructUnarySpec sqrtTerm pevalSqrtTerm++fpUnaryOpSpec ::+  ( ValidFP eb fb,+    TermRewritingSpec a (FP eb fb)+  ) =>+  FPUnaryOp ->+  a ->+  a+fpUnaryOpSpec op = constructUnarySpec (fpUnaryTerm op) (pevalFPUnaryTerm op)++fpBinaryOpSpec ::+  ( ValidFP eb fb,+    TermRewritingSpec a (FP eb fb)+  ) =>+  FPBinaryOp ->+  a ->+  a ->+  a+fpBinaryOpSpec op = constructBinarySpec (fpBinaryTerm op) (pevalFPBinaryTerm op)++fpRoundingUnaryOpSpec ::+  ( ValidFP eb fb,+    TermRewritingSpec a (FP eb fb),+    TermRewritingSpec r FPRoundingMode+  ) =>+  FPRoundingUnaryOp ->+  r ->+  a ->+  a+fpRoundingUnaryOpSpec op =+  constructBinarySpec (fpRoundingUnaryTerm op) (pevalFPRoundingUnaryTerm op)++fpRoundingBinarySpec ::+  ( ValidFP eb fb,+    TermRewritingSpec a (FP eb fb),+    TermRewritingSpec r FPRoundingMode+  ) =>+  FPRoundingBinaryOp ->+  r ->+  a ->+  a ->+  a+fpRoundingBinarySpec op =+  constructTernarySpec (fpRoundingBinaryTerm op) (pevalFPRoundingBinaryTerm op)++fpFMASpec ::+  ( ValidFP eb fb,+    TermRewritingSpec a (FP eb fb),+    TermRewritingSpec r FPRoundingMode+  ) =>+  r ->+  a ->+  a ->+  a ->+  a+fpFMASpec a b c d =+  wrap+    (fpFMATerm (norewriteVer a) (norewriteVer b) (norewriteVer c) (norewriteVer d))+    (pevalFPFMATerm (rewriteVer a) (rewriteVer b) (rewriteVer c) (norewriteVer d))+ data BoolOnlySpec = BoolOnlySpec (Term Bool) (Term Bool)  instance Show BoolOnlySpec where@@ -835,3 +979,140 @@   rewriteVer (GeneralSpec _ r) = r   wrap = GeneralSpec   same s = eqTerm (norewriteVer s) (rewriteVer s)++data IEEEFP32Spec = IEEEFP32Spec (Term FP32) (Term FP32)++instance Show IEEEFP32Spec where+  show (IEEEFP32Spec n r) =+    "IEEEFP32Spec { no: " ++ pformat n ++ ", re: " ++ pformat r ++ " }"++instance TermRewritingSpec IEEEFP32Spec FP32 where+  norewriteVer (IEEEFP32Spec n _) = n+  rewriteVer (IEEEFP32Spec _ r) = r+  wrap = IEEEFP32Spec+  same s = eqTerm (norewriteVer s) (rewriteVer s)++instance Arbitrary IEEEFP32Spec where+  arbitrary = do+    bool :: BoolOnlySpec <-+      oneof [conSpec <$> arbitrary, return $ symSpec "bool"]+    rounding :: FPRoundingModeSpec <- arbitrary+    let gen =+          oneof+            [conSpec <$> arbitrary, return $ symSpec "a", return $ symSpec "b"]+    a <- gen+    b <- gen+    c <- gen+    let regular =+          [ a,+            iteSpec bool a b,+            addNumSpec a a,+            negNumSpec a,+            mulNumSpec a b,+            absNumSpec a,+            signumNumSpec a,+            fdivSpec a b,+            recipSpec a,+            sqrtSpec a+          ]+    let uop = fpUnaryOpSpec <$> [FPAbs, FPNeg] <*> return a+    let bop = fpBinaryOpSpec <$> [FPRem, FPMin, FPMax] <*> [a] <*> [b]+    let ruop =+          fpRoundingUnaryOpSpec+            <$> [FPSqrt, FPRoundToIntegral]+            <*> [rounding]+            <*> [a]+    let rbop =+          fpRoundingBinarySpec+            <$> [FPAdd, FPSub, FPMul, FPDiv]+            <*> [rounding]+            <*> [a]+            <*> [b]+    oneof $+      return+        <$> regular+          ++ uop+          ++ bop+          ++ ruop+          ++ rbop+          ++ [fpFMASpec rounding a b c]++data IEEEFP32BoolOpSpec = IEEEFP32BoolOpSpec (Term Bool) (Term Bool)++instance Show IEEEFP32BoolOpSpec where+  show (IEEEFP32BoolOpSpec n r) =+    "IEEEFP32BoolOpSpec { no: " ++ pformat n ++ ", re: " ++ pformat r ++ " }"++instance TermRewritingSpec IEEEFP32BoolOpSpec Bool where+  norewriteVer (IEEEFP32BoolOpSpec n _) = n+  rewriteVer (IEEEFP32BoolOpSpec _ r) = r+  wrap = IEEEFP32BoolOpSpec+  same s = eqTerm (norewriteVer s) (rewriteVer s)++singleFP32BoolOpSpecGen :: Gen IEEEFP32BoolOpSpec+singleFP32BoolOpSpecGen = do+  s0 :: IEEEFP32Spec <- arbitrary+  s1 :: IEEEFP32Spec <- arbitrary+  let traitGens =+        [ FPIsNaN,+          FPIsPositive,+          FPIsNegative,+          FPIsPositiveInfinite,+          FPIsNegativeInfinite,+          FPIsInfinite,+          FPIsPositiveZero,+          FPIsNegativeZero,+          FPIsZero,+          FPIsNormal,+          FPIsSubnormal,+          FPIsPoint+        ]+          <&> (\trait -> return $ fpTraitSpec trait s0)+  let cmpGens = return <$> [eqvSpec s0 s1, ltOrdSpec s0 s1, leOrdSpec s0 s1]+  oneof $ traitGens ++ cmpGens++instance Arbitrary IEEEFP32BoolOpSpec where+  arbitrary = singleFP32BoolOpSpecGen++data FPRoundingModeSpec+  = FPRoundingModeSpec (Term FPRoundingMode) (Term FPRoundingMode)++instance Show FPRoundingModeSpec where+  show (FPRoundingModeSpec n r) =+    "FPRoundingModeSpec { no: " ++ pformat n ++ ", re: " ++ pformat r ++ " }"++instance TermRewritingSpec FPRoundingModeSpec FPRoundingMode where+  norewriteVer (FPRoundingModeSpec n _) = n+  rewriteVer (FPRoundingModeSpec _ r) = r+  wrap = FPRoundingModeSpec+  same s = eqTerm (norewriteVer s) (rewriteVer s)++instance Arbitrary FPRoundingModeSpec where+  arbitrary =+    elements+      [ conSpec RNE,+        conSpec RNA,+        conSpec RTP,+        conSpec RTN,+        conSpec RTZ,+        symSpec "a",+        symSpec "b"+      ]++data FPRoundingModeBoolOpSpec = FPRoundingModeBoolOpSpec (Term Bool) (Term Bool)++instance Show FPRoundingModeBoolOpSpec where+  show (FPRoundingModeBoolOpSpec n r) =+    "FPRoundingModeBoolOpSpec { no: " ++ pformat n ++ ", re: " ++ pformat r ++ " }"++instance TermRewritingSpec FPRoundingModeBoolOpSpec Bool where+  norewriteVer (FPRoundingModeBoolOpSpec n _) = n+  rewriteVer (FPRoundingModeBoolOpSpec _ r) = r+  wrap = FPRoundingModeBoolOpSpec+  same s = eqTerm (norewriteVer s) (rewriteVer s)++instance Arbitrary FPRoundingModeBoolOpSpec where+  arbitrary = do+    l :: FPRoundingModeSpec <- arbitrary+    r <- arbitrary+    elements [eqvSpec l r, ltOrdSpec l r, leOrdSpec l r]

@@ -1,4 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -8,14 +9,21 @@ module Grisette.Backend.TermRewritingTests   ( termRewritingTests,     validateSpec,+    bitwuzlaConfig,   ) where  import Data.Foldable (traverse_)+#if MIN_VERSION_sbv(8,17,0)+import Data.SBV (bitwuzla)+#endif import qualified Data.SBV as SBV import Grisette   ( GrisetteSMTConfig,+    ITEOp (symIte),     IntN,+    LogicalOp (symNot),+    Solvable (con),     SymBool (SymBool),     WordN,     precise,@@ -25,8 +33,11 @@   ( BoolOnlySpec,     BoolWithLIASpec,     DifferentSizeBVSpec,+    FPRoundingModeBoolOpSpec,     FixedSizedBVWithBoolSpec,     GeneralSpec,+    IEEEFP32BoolOpSpec (IEEEFP32BoolOpSpec),+    IEEEFP32Spec,     LIAWithBoolSpec,     TermRewritingSpec       ( conSpec,@@ -41,7 +52,9 @@     andSpec,     divIntegralSpec,     eqvSpec,+    fpTraitSpec,     iteSpec,+    leOrdSpec,     modIntegralSpec,     mulNumSpec,     negNumSpec,@@ -50,11 +63,27 @@     quotIntegralSpec,     remIntegralSpec,     shiftRightSpec,+    signumNumSpec,   )+import Grisette.Internal.Core.Data.Class.IEEEFP+  ( IEEEConstants (fpNaN, fpNegativeInfinite, fpPositiveInfinite),+    SymIEEEFPTraits (symFpIsPositiveInfinite),+  )+import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp ((.&&)))+import Grisette.Internal.Core.Data.Class.SEq (SEq ((./=), (.==)))+import Grisette.Internal.SymPrim.FP (FP32) import Grisette.Internal.SymPrim.Prim.Term-  ( SupportedPrim,+  ( FPTrait (FPIsPositive),+    SupportedPrim,+    Term,+    conTerm,+    fpTraitTerm,+    iteTerm,+    notTerm,     pformat,+    ssymTerm,   )+import Grisette.Internal.SymPrim.SymFP (SymFP32) import Test.Framework (Test, TestName, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.Framework.Providers.QuickCheck2 (testProperty)@@ -68,11 +97,39 @@   case (r, rs) of     (Left _, Right _) -> do       return ()-    (Left _, Left _) -> do+    (Left _, Left err) -> do+      print err       assertFailure $ "Bad rewriting with unsolvable formula: " ++ pformat (norewriteVer a) ++ " was rewritten to " ++ pformat (rewriteVer a)     (Right m, _) -> do       assertFailure $ "With model" ++ show m ++ "Bad rewriting: " ++ pformat (norewriteVer a) ++ " was rewritten to " ++ pformat (rewriteVer a) +bitwuzlaConfig :: IO (Maybe (GrisetteSMTConfig 0))+bitwuzlaConfig = do+#if MIN_VERSION_sbv(8,17,0)+  v <- solve (precise bitwuzla) $+         ("x" :: SymFP32) ./= "x" .&&+         symNot (symFpIsPositiveInfinite (con $ -4.7e-38 :: SymFP32)) .&&+         (symIte "bool"+            (con $ fpPositiveInfinite :: SymFP32)+            (con $ fpNegativeInfinite) .== "m")+  case v of+    Left _ -> return Nothing+    Right _ -> return $ Just $ precise bitwuzla+#else+  return Nothing+#endif++onlyWhenBitwuzlaIsAvailable :: (GrisetteSMTConfig 0 -> IO ()) -> IO ()+onlyWhenBitwuzlaIsAvailable action = do+  config <- bitwuzlaConfig+  case config of+    Just config -> action config+    Nothing ->+      putStrLn $+        "bitwuzla isn't available in the system, or the dependent sbv"+          <> " library does not work well with it. This test is marked as "+          <> " success."+ unboundedConfig = precise SBV.z3  divisionTest ::@@ -322,5 +379,78 @@           divisionTest @(GeneralSpec (WordN 4)) "mod" modIntegralSpec,           divisionTest @(GeneralSpec (WordN 4)) "quot" quotIntegralSpec,           divisionTest @(GeneralSpec (WordN 4)) "rem" remIntegralSpec+        ],+      testGroup+        "FP"+        [ testCase "0.0 == -0.0" $+            onlyWhenBitwuzlaIsAvailable+              ( `validateSpec`+                  ( eqvSpec+                      (conSpec 0.0 :: IEEEFP32Spec)+                      (conSpec $ -0.0) ::+                      IEEEFP32BoolOpSpec+                  )+              ),+          testCase "-0.0 <= -0.0" $+            onlyWhenBitwuzlaIsAvailable+              ( `validateSpec`+                  ( leOrdSpec+                      (conSpec 0.0 :: IEEEFP32Spec)+                      (conSpec $ -0.0) ::+                      IEEEFP32BoolOpSpec+                  )+              ),+          testCase "is_pos(nan)" $+            onlyWhenBitwuzlaIsAvailable+              ( `validateSpec`+                  ( fpTraitSpec FPIsPositive (conSpec fpNaN :: IEEEFP32Spec) ::+                      IEEEFP32BoolOpSpec+                  )+              ),+          testCase "is_pos(+inf)" $+            onlyWhenBitwuzlaIsAvailable+              ( `validateSpec`+                  ( fpTraitSpec+                      FPIsPositive+                      ( iteSpec+                          (symSpec "bool" :: BoolOnlySpec)+                          (conSpec fpNegativeInfinite)+                          (conSpec fpPositiveInfinite) ::+                          IEEEFP32Spec+                      ) ::+                      IEEEFP32BoolOpSpec+                  )+              ),+          testCase "regression 2" $+            onlyWhenBitwuzlaIsAvailable+              ( `validateSpec`+                  ( eqvSpec+                      (signumNumSpec (conSpec (1.175e-38) :: IEEEFP32Spec))+                      (symSpec "b") ::+                      IEEEFP32BoolOpSpec+                  )+              ),+          testCase "test sbv bug mitigation sbv#702" $+            onlyWhenBitwuzlaIsAvailable+              ( flip validateSpec $+                  IEEEFP32BoolOpSpec+                    ( fpTraitTerm+                        FPIsPositive+                        ( iteTerm+                            (ssymTerm "bool")+                            (conTerm fpNegativeInfinite :: Term FP32)+                            (conTerm fpPositiveInfinite :: Term FP32)+                        )+                    )+                    (notTerm $ ssymTerm "bool")+              ),+          testProperty "FP32BoolOp" $+            withMaxSuccess 1000 . mapSize (`min` 10) $+              ioProperty . \(x :: IEEEFP32BoolOpSpec) ->+                onlyWhenBitwuzlaIsAvailable (`validateSpec` x),+          testProperty "FPRoundingModeBoolOpSpec" $+            mapSize (`min` 10) $+              ioProperty . \(x :: FPRoundingModeBoolOpSpec) ->+                onlyWhenBitwuzlaIsAvailable (`validateSpec` x)         ]     ]

@@ -1,523 +0,0 @@-{-# LANGUAGE BinaryLiterals #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE NegativeLiterals #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}--module Grisette.Core.Data.BVTests (bvTests) where--import Control.DeepSeq (NFData (rnf), deepseq, force)-import Control.Exception-  ( ArithException,-    SomeException,-    catch,-    evaluate,-  )-import Control.Monad (when)-import Data.Bifunctor (Bifunctor (bimap))-import Data.Bits-  ( Bits-      ( bit,-        bitSizeMaybe,-        clearBit,-        complement,-        complementBit,-        isSigned,-        popCount,-        rotate,-        rotateL,-        rotateR,-        setBit,-        shift,-        shiftL,-        shiftR,-        testBit,-        xor,-        zeroBits,-        (.&.),-        (.|.)-      ),-    FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),-  )-import Data.Int (Int8)-import Data.Proxy (Proxy (Proxy))-import Data.Typeable (Typeable, typeRep)-import Data.Word (Word8)-import GHC.Stack (HasCallStack)-import Grisette-  ( BV (bv),-    SizedBV-      ( sizedBVConcat,-        sizedBVExt,-        sizedBVSelect,-        sizedBVSext,-        sizedBVZext-      ),-    SomeIntN,-    SomeWordN,-    pattern SomeIntN,-    pattern SomeWordN,-  )-import Grisette.Internal.SymPrim.BV-  ( IntN (IntN),-    WordN (unWordN),-  )-import Test.Framework (Test, TestName, testGroup)-import Test.Framework.Providers.HUnit (testCase)-import Test.Framework.Providers.QuickCheck2 (testProperty)-import Test.HUnit (Assertion, assertFailure, (@=?), (@?=))-import Test.QuickCheck (Arbitrary, Property, ioProperty)--unaryConform :: forall a b c d. (Show c, Eq c, HasCallStack) => (a -> b) -> (d -> c) -> (a -> c) -> (b -> d) -> a -> Property-unaryConform a2b d2c f g x = ioProperty $ f x @=? d2c (g (a2b x))--binaryConform ::-  forall a b c d e f.-  (Show e, Eq e, HasCallStack) =>-  (a -> b) ->-  (c -> d) ->-  (f -> e) ->-  (a -> c -> e) ->-  (b -> d -> f) ->-  a ->-  c ->-  Property-binaryConform a2b c2d f2e f g x y = ioProperty $ f x y @=? f2e (g (a2b x) (c2d y))--wordUnaryConform :: (HasCallStack) => (WordN 8 -> WordN 8) -> (Word8 -> Word8) -> Word8 -> Assertion-wordUnaryConform f g x = unWordN (f (fromIntegral x)) @=? toInteger (g x)--wordUnaryNonNegIntConform :: (HasCallStack) => (Int -> WordN 8) -> (Int -> Word8) -> Int -> Assertion-wordUnaryNonNegIntConform f g y = when (y >= 0) $ unWordN (f y) @=? toInteger (g y)--wordBinIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion-wordBinIntConform f g x y = unWordN (f (fromIntegral x) y) @=? toInteger (g x y)--wordBinNonNegIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion-wordBinNonNegIntConform f g x y = when (y >= 0) $ unWordN (f (fromIntegral x) y) @=? toInteger (g x y)--wordBinConform :: (HasCallStack) => (WordN 8 -> WordN 8 -> WordN 8) -> (Word8 -> Word8 -> Word8) -> Word8 -> Word8 -> Assertion-wordBinConform f g x y = unWordN (f (fromIntegral x) (fromIntegral y)) @=? toInteger (g x y)--intN8eqint8 :: IntN 8 -> Int8 -> Assertion-intN8eqint8 (IntN v) i-  | v < 0 = assertFailure "Bad IntN"-  | v <= 127 = v @=? fromIntegral i-  | v == 128 = i @=? -128-  | otherwise = 256 - v @=? fromIntegral (-i)--intUnaryConform :: (IntN 8 -> IntN 8) -> (Int8 -> Int8) -> Int8 -> Assertion-intUnaryConform f g x = intN8eqint8 (f (fromIntegral x)) (g x)--intUnaryNonNegIntConform :: (Int -> IntN 8) -> (Int -> Int8) -> Int -> Assertion-intUnaryNonNegIntConform f g y = when (y >= 0) $ intN8eqint8 (f y) (g y)--intBinIntConform :: (IntN 8 -> Int -> IntN 8) -> (Int8 -> Int -> Int8) -> Int8 -> Int -> Assertion-intBinIntConform f g x y = intN8eqint8 (f (fromIntegral x) y) (g x y)--intBinNonNegIntConform :: (IntN 8 -> Int -> IntN 8) -> (Int8 -> Int -> Int8) -> Int8 -> Int -> Assertion-intBinNonNegIntConform f g x y = when (y >= 0) $ intN8eqint8 (f (fromIntegral x) y) (g x y)--intBinConform :: (IntN 8 -> IntN 8 -> IntN 8) -> (Int8 -> Int8 -> Int8) -> Int8 -> Int8 -> Assertion-intBinConform f g x y = intN8eqint8 (f (fromIntegral x) (fromIntegral y)) (g x y)--finiteBitsConformTest ::-  forall ref typ.-  (Arbitrary ref, Typeable ref, Typeable typ, Show ref, Show typ, Eq ref, Eq typ, FiniteBits ref, FiniteBits typ, Integral ref, Integral typ) =>-  Proxy ref ->-  Proxy typ ->-  Int ->-  Test-finiteBitsConformTest pref ptyp numBits =-  testGroup-    (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for FiniteBits instances")-    [ testCase "finiteBitSize" $ finiteBitSize (0 :: typ) @=? numBits,-      testProperty "countLeadingZeros" $ unaryConform @ref @typ fromIntegral id countLeadingZeros countLeadingZeros,-      testProperty "countTrailingZeros" $ unaryConform @ref @typ fromIntegral id countTrailingZeros countTrailingZeros-    ]--boundedConformTest ::-  forall ref typ.-  (Typeable ref, Typeable typ, Bounded typ, Bounded ref, Integral ref, Num typ, Eq typ, Show typ) =>-  Proxy ref ->-  Proxy typ ->-  Test-boundedConformTest pref ptyp =-  testGroup-    (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Bounded instances")-    [ testCase "minBound" $ (minBound :: typ) @=? fromIntegral (minBound :: ref),-      testCase "maxBound" $ (maxBound :: typ) @=? fromIntegral (maxBound :: ref)-    ]--shouldThrow :: (NFData a) => String -> a -> IO ()-shouldThrow name x = do-  errored <- catch (evaluate $ x `deepseq` True) (\(_ :: SomeException) -> return False)-  when errored $ assertFailure $ name ++ " should throw an exception"--succPredLikeTest ::-  forall a b.-  (Arbitrary a, Eq a, Eq b, Show a, Show b, NFData b) =>-  TestName ->-  String ->-  (a -> b) ->-  (a -> a) ->-  (b -> b) ->-  a ->-  b ->-  Test-succPredLikeTest name boundName a2b fa fb bounda boundb =-  testGroup-    name-    [ testProperty (name ++ " non " ++ boundName) $-        ioProperty . \(x :: a) ->-          if x == bounda then return () else a2b (fa x) @=? fb (a2b x),-      testCase (name ++ " " ++ boundName) $ shouldThrow (name ++ " " ++ boundName) $ fb boundb-    ]--enumConformTest ::-  forall ref typ.-  ( Arbitrary ref,-    Typeable ref,-    Typeable typ,-    Eq ref,-    Eq typ,-    Show ref,-    Show typ,-    NFData typ,-    Integral ref,-    Integral typ,-    Bounded ref,-    Bounded typ-  ) =>-  Proxy ref ->-  Proxy typ ->-  Test-enumConformTest pref ptyp =-  testGroup-    (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Enum instances")-    [ succPredLikeTest @ref @typ "succ" "maxBound" fromIntegral succ succ maxBound maxBound,-      succPredLikeTest @ref @typ "pred" "minBound" fromIntegral pred pred minBound minBound,-      testGroup-        "toEnum"-        [ testProperty "toEnum in bounds" $-            ioProperty . \(x :: ref) ->-              toInteger (toEnum (fromIntegral x) :: ref) @=? toInteger (toEnum (fromIntegral x) :: typ),-          testCase "toEnum (fromIntegral minBound - 1)" $-            shouldThrow "toEnum (fromIntegral minBound - 1)" (toEnum (fromIntegral (minBound :: typ) - 1) :: typ),-          testCase "toEnum (fromIntegral maxBound + 1)" $-            shouldThrow "toEnum (fromIntegral maxBound + 1)" (toEnum (fromIntegral (maxBound :: typ) + 1) :: typ)-        ],-      testProperty "fromEnum" $ unaryConform @ref @typ fromIntegral id fromEnum fromEnum,-      testProperty "enumFrom" $ unaryConform @ref @typ fromIntegral (fromIntegral <$>) enumFrom enumFrom,-      testProperty "enumFromThen" $ \(x :: ref) y ->-        ioProperty $ do-          if x == y-            then return ()-            else do-              (fromIntegral <$> enumFromThen x y) @=? enumFromThen (fromIntegral x :: typ) (fromIntegral y),-      testProperty "enumFromTo" $ binaryConform @ref @typ fromIntegral fromIntegral (fromIntegral <$>) enumFromTo enumFromTo,-      testProperty "enumFromThenTo" $ \(x :: ref) y z ->-        ioProperty $-          if x == y-            then return ()-            else (fromIntegral <$> enumFromThenTo x y z) @=? enumFromThenTo (fromIntegral x :: typ) (fromIntegral y) (fromIntegral z)-    ]--newtype AEWrapper = AEWrapper ArithException deriving (Eq)--instance Show AEWrapper where-  show (AEWrapper x) = show x--instance NFData AEWrapper where-  rnf (AEWrapper x) = x `seq` ()--sameDiv :: (NFData a, NFData b, Eq b, Show b) => a -> a -> (a -> b) -> (a -> a -> a) -> (b -> b -> b) -> IO ()-sameDiv x y a2b fa fb = do-  xa <- evaluate (force $ Right $ fa x y) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e-  xb <- evaluate (force $ Right $ fb (a2b x) (a2b y)) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e-  xb @=? a2b <$> xa--sameDivMod :: (NFData a, NFData b, Eq b, Show b) => a -> a -> (a -> b) -> (a -> a -> (a, a)) -> (b -> b -> (b, b)) -> IO ()-sameDivMod x y a2b fa fb = do-  xa <- evaluate (force $ Right $ fa x y) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e-  xb <- evaluate (force $ Right $ fb (a2b x) (a2b y)) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e-  xb @=? bimap a2b a2b <$> xa--divLikeTest ::-  forall a b.-  (Arbitrary a, Eq a, Eq b, Num a, Show a, Bounded a, Bits a, Eq b, Show b, Num b, NFData b, Bounded b, Bits b, NFData a) =>-  TestName ->-  (a -> b) ->-  (a -> a -> a) ->-  (b -> b -> b) ->-  Test-divLikeTest name a2b fa fb =-  testGroup-    name-    [ testCase "divided by zero" $ do-        sameDiv 1 0 a2b fa fb-        sameDiv 0 0 a2b fa fb-        sameDiv (-1) 0 a2b fa fb-        sameDiv minBound 0 a2b fa fb-        sameDiv maxBound 0 a2b fa fb,-      testCase "min divided by -1" $ do-        sameDiv minBound (-1) a2b fa fb,-      testProperty "prop" $ \(x :: a) y -> ioProperty $ sameDiv x y a2b fa fb-    ]--divModLikeTest ::-  forall a b.-  (Arbitrary a, Eq a, Eq b, Num a, NFData a, Show a, Bounded a, Bits a, Eq b, Show b, Num b, NFData b, Bounded b, Bits b) =>-  TestName ->-  (a -> b) ->-  (a -> a -> (a, a)) ->-  (b -> b -> (b, b)) ->-  Test-divModLikeTest name a2b fa fb =-  testGroup-    name-    [ testCase "divided by zero" $ do-        sameDivMod 1 0 a2b fa fb-        sameDivMod 0 0 a2b fa fb-        sameDivMod (-1) 0 a2b fa fb-        sameDivMod minBound 0 a2b fa fb-        sameDivMod maxBound 0 a2b fa fb,-      testCase "min divided by -1" $ do-        sameDivMod minBound (-1) a2b fa fb,-      testProperty "prop" $ \(x :: a) y -> ioProperty $ sameDivMod x y a2b fa fb-    ]--realConformTest ::-  forall proxy ref typ.-  (Typeable ref, Typeable typ, Integral ref, Num typ, Arbitrary ref, Real typ, Show ref) =>-  proxy ref ->-  proxy typ ->-  Test-realConformTest pref ptyp =-  testGroup-    (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Real instances")-    [ testProperty "toRational" $ unaryConform @ref @typ fromIntegral id toRational toRational-    ]--integralConformTest ::-  forall ref typ.-  ( Arbitrary ref,-    Typeable ref,-    Typeable typ,-    Eq ref,-    Eq typ,-    Show ref,-    Show typ,-    Num ref,-    Num typ,-    Integral ref,-    Integral typ,-    Bits ref,-    Bits typ,-    Bounded ref,-    Bounded typ,-    NFData typ,-    NFData ref-  ) =>-  Proxy ref ->-  Proxy typ ->-  Test-integralConformTest pref ptyp =-  testGroup-    (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Integral instances")-    [ divLikeTest @ref @typ "quot" fromIntegral quot quot,-      divLikeTest @ref @typ "rem" fromIntegral rem rem,-      divModLikeTest @ref @typ "quotRem" fromIntegral quotRem quotRem,-      divLikeTest @ref @typ "div" fromIntegral div div,-      divLikeTest @ref @typ "mod" fromIntegral mod mod,-      divModLikeTest @ref @typ "divMod" fromIntegral divMod divMod,-      testProperty "toInteger" $ unaryConform @ref @typ fromIntegral id toInteger toInteger-    ]--sizedBVTests :: Test-sizedBVTests =-  testGroup-    "sizedBV"-    [ testGroup-        "WordN 8 conform to Word8 for Bits instances"-        [ testProperty "(.&.)" $ \x y -> ioProperty $ wordBinConform (.&.) (.&.) x y,-          testProperty "(.|.)" $ \x y -> ioProperty $ wordBinConform (.|.) (.|.) x y,-          testProperty "xor" $ \x y -> ioProperty $ wordBinConform xor xor x y,-          testProperty "complement" $ ioProperty . wordUnaryConform complement complement,-          testProperty "shift" $ \x y -> ioProperty $ wordBinIntConform shift shift x y,-          testProperty "rotate" $ \x y -> ioProperty $ wordBinIntConform rotate rotate x y,-          testCase "zeroBits" $ (zeroBits :: WordN 8) @=? 0,-          testProperty "bit" $ ioProperty . wordUnaryNonNegIntConform bit bit,-          testProperty "setBit" $ \x y -> ioProperty $ wordBinNonNegIntConform setBit setBit x y,-          testProperty "clearBit" $ \x y -> ioProperty $ wordBinNonNegIntConform clearBit clearBit x y,-          testProperty "complementBit" $ \x y -> ioProperty $ wordBinNonNegIntConform complementBit complementBit x y,-          testProperty "testBit" $ \(x :: Word8) i -> i < 0 || testBit x i == testBit (fromIntegral x :: WordN 8) i,-          testCase "bitSizeMaybe" $ bitSizeMaybe (0 :: WordN 8) @=? Just 8,-          testCase "isSigned" $ isSigned (0 :: WordN 8) @=? False,-          testProperty "shiftL" $ \x y -> ioProperty $ wordBinNonNegIntConform shiftL shiftL x y,-          testProperty "shiftR" $ \x y -> ioProperty $ wordBinNonNegIntConform shiftR shiftR x y,-          testProperty "rotateL" $ \x y -> ioProperty $ wordBinNonNegIntConform rotateL rotateL x y,-          testProperty "rotateR" $ \x y -> ioProperty $ wordBinNonNegIntConform rotateR rotateR x y,-          testProperty "popCount" $ ioProperty . \(x :: Word8) -> popCount x @=? popCount (fromIntegral x :: WordN 8)-        ],-      finiteBitsConformTest (Proxy @Word8) (Proxy @(WordN 8)) 8,-      boundedConformTest (Proxy @Word8) (Proxy @(WordN 8)),-      enumConformTest (Proxy @Word8) (Proxy @(WordN 8)),-      realConformTest (Proxy @Word8) (Proxy @(WordN 8)),-      integralConformTest (Proxy @Word8) (Proxy @(WordN 8)),-      testGroup-        "WordN 8 conform to Word8 for Num instances"-        [ testProperty "(+)" $ \x y -> ioProperty $ wordBinConform (+) (+) x y,-          testProperty "(*)" $ \x y -> ioProperty $ wordBinConform (*) (*) x y,-          testProperty "(-)" $ \x y -> ioProperty $ wordBinConform (-) (-) x y,-          testProperty "negate" $ ioProperty . wordUnaryConform negate negate,-          testProperty "abs" $ ioProperty . wordUnaryConform abs abs,-          testProperty "signum" $ ioProperty . wordUnaryConform signum signum,-          testProperty "fromInteger" $-            ioProperty . \(x :: Integer) ->-              unWordN (fromInteger x :: WordN 8) @=? toInteger (fromInteger x :: Word8)-        ],-      testGroup-        "WordN 8 conform to Word8 for Ord instances"-        [ testProperty "(<=)" $ \(x :: Word8) y -> ioProperty $ x <= y @=? (fromIntegral x :: WordN 8) <= (fromIntegral y :: WordN 8)-        ],-      testGroup-        "IntN 8 conform to Int8 for Bits instances"-        [ testProperty "(.&.)" $ \x y -> ioProperty $ intBinConform (.&.) (.&.) x y,-          testProperty "(.|.)" $ \x y -> ioProperty $ intBinConform (.|.) (.|.) x y,-          testProperty "xor" $ \x y -> ioProperty $ intBinConform xor xor x y,-          testProperty "complement" $ ioProperty . intUnaryConform complement complement,-          testProperty "shift" $ \x y -> ioProperty $ intBinIntConform shift shift x y,-          testProperty "rotate" $ \x y -> ioProperty $ intBinIntConform rotate rotate x y,-          testCase "zeroBits" $ (zeroBits :: IntN 8) @=? 0,-          testProperty "bit" $ ioProperty . intUnaryNonNegIntConform bit bit,-          testProperty "setBit" $ \x y -> ioProperty $ intBinNonNegIntConform setBit setBit x y,-          testProperty "clearBit" $ \x y -> ioProperty $ intBinNonNegIntConform clearBit clearBit x y,-          testProperty "complementBit" $ \x y -> ioProperty $ intBinNonNegIntConform complementBit complementBit x y,-          testProperty "testBit" $ \(x :: Int8) i -> i < 0 || testBit x i == testBit (fromIntegral x :: IntN 8) i,-          testCase "bitSizeMaybe" $ bitSizeMaybe (0 :: IntN 8) @=? Just 8,-          testCase "isSigned" $ isSigned (0 :: IntN 8) @=? True,-          testProperty "shiftL" $ \x y -> ioProperty $ intBinNonNegIntConform shiftL shiftL x y,-          testProperty "shiftR" $ \x y -> ioProperty $ intBinNonNegIntConform shiftR shiftR x y,-          testProperty "rotateL" $ \x y -> ioProperty $ intBinNonNegIntConform rotateL rotateL x y,-          testProperty "rotateR" $ \x y -> ioProperty $ intBinNonNegIntConform rotateR rotateR x y,-          testProperty "popCount" $ ioProperty . \(x :: Int8) -> popCount x @=? popCount (fromIntegral x :: IntN 8)-        ],-      finiteBitsConformTest (Proxy @Int8) (Proxy @(IntN 8)) 8,-      boundedConformTest (Proxy @Int8) (Proxy @(IntN 8)),-      enumConformTest (Proxy @Int8) (Proxy @(IntN 8)),-      realConformTest (Proxy @Int8) (Proxy @(IntN 8)),-      integralConformTest (Proxy @Int8) (Proxy @(IntN 8)),-      testGroup-        "IntN 8 conform to Int8 for Num instances"-        [ testProperty "(+)" $ \x y -> ioProperty $ intBinConform (+) (+) x y,-          testProperty "(*)" $ \x y -> ioProperty $ intBinConform (*) (*) x y,-          testProperty "(-)" $ \x y -> ioProperty $ intBinConform (-) (-) x y,-          testProperty "negate" $ ioProperty . wordUnaryConform negate negate,-          testProperty "abs" $ ioProperty . wordUnaryConform abs abs,-          testProperty "signum" $ ioProperty . wordUnaryConform signum signum,-          testProperty "fromInteger" $-            ioProperty . \(x :: Integer) ->-              intN8eqint8 (fromInteger x :: IntN 8) (fromInteger x :: Int8)-        ],-      testGroup-        "IntN 8 conform to IntN for Ord instances"-        [ testProperty "(<=)" $ \(x :: Int8) y -> ioProperty $ (fromIntegral x :: IntN 8) <= (fromIntegral y :: IntN 8) @=? x <= y-        ],-      testGroup-        "WordN bvops"-        [ testProperty "sizedBVConcat" $ \(x :: Integer) (y :: Integer) ->-            ioProperty $-              sizedBVConcat (fromInteger x :: WordN 5) (fromInteger y :: WordN 7) @=? fromInteger (x * 128 + y `mod` 128),-          testProperty "sizedBVZext" $ ioProperty . \(x :: Integer) -> sizedBVZext (Proxy :: Proxy 12) (fromInteger x :: WordN 7) @=? fromInteger (x `mod` 128),-          testCase "sizedBVSext" $ do-            sizedBVSext (Proxy :: Proxy 12) (0 :: WordN 8) @=? 0-            sizedBVSext (Proxy :: Proxy 12) (1 :: WordN 8) @=? 1-            sizedBVSext (Proxy :: Proxy 12) (127 :: WordN 8) @=? 127-            sizedBVSext (Proxy :: Proxy 12) (128 :: WordN 8) @=? 3968-            sizedBVSext (Proxy :: Proxy 12) (255 :: WordN 8) @=? 4095,-          testProperty "sizedBVExt is sizedBVZext" $-            ioProperty . \(x :: Integer) ->-              sizedBVExt (Proxy :: Proxy 12) (fromInteger x :: WordN 8) @=? sizedBVZext (Proxy :: Proxy 12) (fromInteger x :: WordN 8),-          testCase "sizedBVSelect" $ do-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b11100 :: WordN 8) @=? 0b11-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b111000 :: WordN 8) @=? 0b111-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b101000 :: WordN 8) @=? 0b101-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b1010000 :: WordN 8) @=? 0b10-        ],-      testGroup-        "IntN bvops"-        [ testProperty "sizedBVConcat" $ \(x :: Integer) (y :: Integer) ->-            ioProperty $-              sizedBVConcat (fromInteger x :: IntN 5) (fromInteger y :: IntN 7) @=? fromInteger (x * 128 + y `mod` 128),-          testProperty "sizedBVZext" $ ioProperty . \(x :: Integer) -> sizedBVZext (Proxy :: Proxy 12) (fromInteger x :: IntN 7) @=? fromInteger (x `mod` 128),-          testCase "sizedBVSext" $ do-            sizedBVSext (Proxy :: Proxy 12) (0 :: WordN 8) @=? 0-            sizedBVSext (Proxy :: Proxy 12) (1 :: WordN 8) @=? 1-            sizedBVSext (Proxy :: Proxy 12) (127 :: WordN 8) @=? 127-            sizedBVSext (Proxy :: Proxy 12) (128 :: WordN 8) @=? 3968-            sizedBVSext (Proxy :: Proxy 12) (255 :: WordN 8) @=? 4095,-          testProperty "sizedBVExt is sizedBVSext" $-            ioProperty . \(x :: Integer) ->-              sizedBVExt (Proxy :: Proxy 12) (fromInteger x :: IntN 8) @=? sizedBVSext (Proxy :: Proxy 12) (fromInteger x :: IntN 8),-          testCase "sizedBVSelect" $ do-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b11100 :: IntN 8) @=? 0b11-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b111000 :: IntN 8) @=? 0b111-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b101000 :: IntN 8) @=? 0b101-            sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b1010000 :: IntN 8) @=? 0b10-        ],-      testGroup-        "read"-        [ testProperty "read . show" $ \(x :: IntN 8) -> read (show x) == x,-          testProperty "read . show" $ \(x :: WordN 8) -> read (show x) == x,-          testProperty "read . show" $ \(x :: IntN 9) -> read (show x) == x,-          testProperty "read . show" $ \(x :: WordN 9) -> read (show x) == x-        ],-      testGroup-        "Regression"-        [ testCase "division of min bound and minus one for signed bit vector should throw" $ do-            shouldThrow "divMod" $ divMod (minBound :: IntN 8) (-1 :: IntN 8)-            shouldThrow "div" $ div (minBound :: IntN 8) (-1 :: IntN 8)-            shouldThrow "quotRem" $ quotRem (minBound :: IntN 8) (-1 :: IntN 8)-            shouldThrow "quot" $ quot (minBound :: IntN 8) (-1 :: IntN 8),-          testCase "toInteger for IntN 1" $ do-            toInteger (0 :: IntN 1) @=? 0-            toInteger (1 :: IntN 1) @=? (-1),-          testProperty "WordN shiftL by large amount" $ \(x :: WordN 128) ->-            ioProperty $ shiftL x maxBound @=? 0,-          testProperty "IntN shiftL by large amount" $ \(x :: IntN 128) ->-            ioProperty $ shiftL x maxBound @=? 0-        ]-    ]--someWordNTests :: Test-someWordNTests =-  testGroup-    "SomeWordN"-    [ testGroup-        "BV"-        [ testGroup-            "bv"-            [ testCase "bv 12 21" $-                (bv 12 21 :: SomeWordN) @?= SomeWordN (0x015 :: WordN 12)-            ]-        ]-    ]--someIntNTests :: Test-someIntNTests =-  testGroup-    "SomeIntN"-    [ testGroup-        "BV"-        [ testGroup-            "bv"-            [ testCase "bv 12 21" $-                (bv 12 21 :: SomeIntN) @?= SomeIntN (0x015 :: IntN 12)-            ]-        ]-    ]--bvTests :: Test-bvTests = testGroup "BV" [sizedBVTests, someWordNTests, someIntNTests]

@@ -8,6 +8,12 @@  module Grisette.Core.Data.Class.GPrettyTests (gprettyTests) where +import Control.Monad.Except (ExceptT (ExceptT))+import Control.Monad.Identity (Identity, IdentityT (IdentityT))+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))+import qualified Control.Monad.Trans.Writer.Lazy as WriterLazy+import qualified Data.HashMap.Lazy as HM+import qualified Data.HashSet as HS import Data.Int (Int16, Int32, Int64, Int8) import Data.Text as T (Text, pack, unpack) import Data.Word (Word16, Word32, Word64, Word8)@@ -63,7 +69,8 @@   Test propertyGPrettyShow n g =   testProperty n $ forAll g $ \(a :: a) -> do-    renderStrict (layoutPretty (LayoutOptions Unbounded) (gpretty a)) == T.pack (show a)+    renderStrict (layoutPretty (LayoutOptions Unbounded) (gpretty a))+      == T.pack (show a)  propertyGPrettyRead ::   forall a.@@ -340,7 +347,36 @@           propertyGPretty             "Record Record"             ( arbitrary :: Gen (Record (Record Int Int) (Record Int Int))-            )+            ),+          propertyGPretty+            "Maybe (MaybeT Identity Int)"+            (Just . MaybeT <$> arbitrary :: Gen (Maybe (MaybeT Identity Int))),+          propertyGPretty+            "Maybe (ExceptT Int Identity Int)"+            ( Just . ExceptT <$> arbitrary ::+                Gen (Maybe (ExceptT Int Identity Int))+            ),+          propertyGPretty+            "Maybe (LazyWriterT Int Identity Int)"+            ( Just . WriterLazy.WriterT <$> arbitrary ::+                Gen (Maybe (WriterLazy.WriterT Int Identity Int))+            ),+          propertyGPretty+            "Maybe (StrictWriterT Int Identity Int)"+            ( Just . WriterLazy.WriterT <$> arbitrary ::+                Gen (Maybe (WriterLazy.WriterT Int Identity Int))+            ),+          propertyGPretty+            "Maybe (IdentityT Identity Int)"+            ( Just . IdentityT <$> arbitrary ::+                Gen (Maybe (IdentityT Identity Int))+            ),+          propertyGPrettyShow+            "HS.HashSet Int"+            (HS.fromList <$> arbitrary :: Gen (HS.HashSet Int)),+          propertyGPrettyShow+            "HM.HashMap Int Int"+            (HM.fromList <$> arbitrary :: Gen (HM.HashMap Int Int))         ],       testGroup         "Symbolic types"

@@ -19,6 +19,9 @@     pattern If,     pattern Single,   )+import Grisette.Internal.Core.Data.Class.PlainUnion+  ( PlainUnion (overestimateUnionValues),+  ) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.HUnit ((@?=))@@ -60,18 +63,23 @@               If c l r -> do                 c @?= "a"                 l @?= return "b"-                r @?= return "c"-              _ -> fail "Should not happen",+                r @?= return "c",           testCase "Merged" $             case mrgIf "a" (return "b") (return "c") :: UnionM SymBool of               If {} -> fail "Expected Single"-              Single v -> v @?= symIte "a" "b" "c"-              _ -> fail "Should not happen",+              Single v -> v @?= symIte "a" "b" "c",           testCase "Construct single" $             (Single "a" :: UnionM SymBool) @?= mrgSingle "a",           testCase "Construct If" $ do             let actual = If "a" (return "b") (return "c") :: UnionM SymBool             let expected = mrgIf "a" (return "b") (return "c")             actual @?= expected-        ]+        ],+      testCase "overestimateUnionValues" $ do+        overestimateUnionValues (return 1 :: UnionM Int) @?= [1]+        overestimateUnionValues (mrgIf "a" (return 1) (return 2) :: UnionM Int)+          @?= [1, 2 :: Int]+        overestimateUnionValues+          (mrgIf "a" (return 1) (mrgIf "x" (return 3) (return 2)) :: UnionM Int)+          @?= [1, 2, 3 :: Int]     ]

@@ -1,382 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}--module Grisette.Core.Data.SomeBVTests (someBVTests) where--import Control.DeepSeq (NFData, force)-import Control.Exception (ArithException (Overflow), catch, evaluate)-import Control.Monad.Except (ExceptT)-import Data.Bits (FiniteBits (finiteBitSize))-import Data.Proxy (Proxy (Proxy))-import Grisette-  ( BV (bv, bvConcat, bvExt, bvSelect, bvSext, bvZext),-    ITEOp (symIte),-    LogicalOp (symNot),-    Mergeable (rootStrategy),-    SafeLinearArith (safeAdd, safeSub),-    Solvable (isym, ssym),-    genSym,-    genSymSimple,-    mrgIf,-    mrgSingle,-  )-import Grisette.Internal.Core.Control.Monad.UnionM (UnionM (UMrg))-import Grisette.Internal.Core.Data.Union (Union (UnionSingle), ifWithLeftMost)-import Grisette.Internal.SymPrim.BV (BitwidthMismatch (BitwidthMismatch), IntN)-import Grisette.Internal.SymPrim.SomeBV-  ( SomeBV (SomeBV),-    SomeIntN,-    SomeSymIntN,-    SomeWordN,-    arbitraryBV,-    binSomeBV,-    binSomeBVR1,-    binSomeBVR2,-    binSomeBVSafe,-    binSomeBVSafeR1,-    conBV,-    conBVView,-    isymBV,-    ssymBV,-    unarySomeBV,-    unarySomeBVR1,-    pattern ConBV,-    pattern SomeIntN,-  )-import Grisette.Internal.SymPrim.SymBV (SymIntN)-import Grisette.Lib.Control.Monad.Except (mrgThrowError)-import Grisette.Lib.Data.Functor (mrgFmap)-import Test.Framework (Test, testGroup)-import Test.Framework.Providers.HUnit (testCase)-import Test.Framework.Providers.QuickCheck2 (testProperty)-import Test.HUnit ((@?=))-import Test.QuickCheck (forAll, ioProperty)--testFuncMatch ::-  (Eq r, Show r) =>-  (SomeIntN -> SomeIntN -> r) ->-  SomeIntN ->-  SomeIntN ->-  r ->-  Test-testFuncMatch f a b r = testCase "bit width match" $ do-  let actual = f a b-  let expected = r-  actual @?= expected--testFuncMisMatch ::-  (NFData r, Show r, Eq r) =>-  (SomeIntN -> SomeIntN -> r) ->-  SomeIntN ->-  SomeIntN ->-  r ->-  Test-testFuncMisMatch f a b r = testCase "bit width mismatch" $ do-  actual <--    evaluate (force $ f a b)-      `catch` \(_ :: BitwidthMismatch) -> return r-  let expected = r-  actual @?= expected--testSafeFuncMatchException ::-  (Eq r, Show r, Mergeable r) =>-  ( SomeIntN ->-    SomeIntN ->-    ExceptT (Either BitwidthMismatch ArithException) UnionM r-  ) ->-  SomeIntN ->-  SomeIntN ->-  ArithException ->-  Test-testSafeFuncMatchException f a b e = testCase "bit width match" $ do-  let actual = f a b-  let expected = mrgThrowError (Right e)-  actual @?= expected--testSafeFuncMatch ::-  (Eq r, Show r, Mergeable r) =>-  ( SomeIntN ->-    SomeIntN ->-    ExceptT (Either BitwidthMismatch ArithException) UnionM r-  ) ->-  SomeIntN ->-  SomeIntN ->-  r ->-  Test-testSafeFuncMatch f a b r = testCase "bit width match" $ do-  let actual = f a b-  let expected = mrgSingle r-  actual @?= expected--testSafeFuncMisMatch ::-  (Eq r, Show r, Mergeable r) =>-  ( SomeIntN ->-    SomeIntN ->-    ExceptT (Either BitwidthMismatch ArithException) UnionM r-  ) ->-  SomeIntN ->-  SomeIntN ->-  Test-testSafeFuncMisMatch f a b = testCase "bit width mismatch" $ do-  let actual = f a b-  let expected = mrgThrowError (Left BitwidthMismatch)-  actual @?= expected--someBVTests :: Test-someBVTests =-  testGroup-    "SomeBV"-    [ testGroup-        "Helpers"-        [ testCase "conBV" $ do-            let actual = conBV (bv 4 5)-            let expected = bv 4 5 :: SomeSymIntN-            actual @?= expected,-          testGroup-            "conBVView"-            [ testCase "is concrete" $ do-                let value = bv 4 5 :: SomeSymIntN-                let actual = conBVView value-                let expected = Just (bv 4 5)-                actual @?= expected-                case value of-                  ConBV v -> v @?= bv 4 5-                  _ -> fail "is concrete",-              testCase "is not concrete" $ do-                let value = ssymBV 4 "a" :: SomeSymIntN-                let actual = conBVView value-                let expected = Nothing-                actual @?= expected-                case value of-                  ConBV _ -> fail "is not concrete"-                  _ -> return ()-            ],-          testCase "ssymBV" $ ssymBV 4 "a" @?= SomeBV (ssym "a" :: SymIntN 4),-          testCase "isymBV" $-            isymBV 4 "a" 1 @?= SomeBV (isym "a" 1 :: SymIntN 4),-          testCase "unarySomeBV" $ do-            let actual =-                  unarySomeBV @IntN @SomeIntN-                    (SomeIntN . negate)-                    (bv 4 5 :: SomeIntN)-            let expected = bv 4 (-5)-            actual @?= expected,-          testCase "unarySomeBVR1" $ do-            let actual = unarySomeBVR1 (negate) (bv 4 5 :: SomeIntN)-            let expected = bv 4 (-5)-            actual @?= expected,-          testGroup-            "binSomeBV"-            [ testFuncMatch @SomeIntN-                (binSomeBV (\l r -> SomeIntN $ l + r))-                (bv 4 5)-                (bv 4 2)-                (bv 4 7),-              testFuncMisMatch @SomeIntN-                (binSomeBV (\l r -> SomeIntN $ l + r))-                (bv 4 5)-                (bv 5 4)-                (bv 3 0)-            ],-          testGroup-            "binSomeBVR1"-            [ testFuncMatch (binSomeBVR1 (+)) (bv 4 5) (bv 4 2) (bv 4 7),-              testFuncMisMatch (binSomeBVR1 (+)) (bv 4 5) (bv 5 4) (bv 3 0)-            ],-          testGroup-            "binSomeBVR2"-            [ testFuncMatch-                (binSomeBVR2 (\l r -> (l + r, l - r)))-                (bv 4 5)-                (bv 4 2)-                (bv 4 7, bv 4 3),-              testFuncMisMatch-                (binSomeBVR2 (\l r -> (l + r, l - r)))-                (bv 4 5)-                (bv 5 4)-                (bv 3 0, bv 6 1)-            ],-          testGroup "binSomeBVSafe" $ do-            let func l r = mrgFmap SomeIntN $ safeAdd l r-            [ testSafeFuncMatch @SomeIntN-                (binSomeBVSafe func)-                (bv 4 5)-                (bv 4 2)-                (bv 4 7),-              testSafeFuncMatchException @SomeIntN-                (binSomeBVSafe func)-                (bv 4 5)-                (bv 4 5)-                Overflow,-              testSafeFuncMisMatch @SomeIntN-                (binSomeBVSafe func)-                (bv 4 5)-                (bv 5 4)-              ],-          testGroup-            "binSomeBVSafeR1"-            [ testSafeFuncMatch-                (binSomeBVSafeR1 safeAdd)-                (bv 4 5)-                (bv 4 2)-                (bv 4 7),-              testSafeFuncMatchException-                (binSomeBVSafeR1 safeAdd)-                (bv 4 5)-                (bv 4 5)-                Overflow,-              testSafeFuncMisMatch (binSomeBVSafeR1 safeAdd) (bv 4 5) (bv 5 4)-            ],-          testGroup "binSomeBVSafeR2" $ do-            let func l r = do-                  a <- safeAdd l r-                  b <- safeSub l r-                  mrgSingle (a, b)-            [ testSafeFuncMatch-                func-                (bv 4 5)-                (bv 4 2)-                (bv 4 7, bv 4 3),-              testSafeFuncMatchException-                func-                (bv 4 5)-                (bv 4 5)-                Overflow,-              testSafeFuncMisMatch func (bv 4 5) (bv 5 4)-              ]-        ],-      testGroup-        "BV"-        [ testCase "bvConcat" $ do-            bvConcat (bv 8 0x14 :: SomeIntN) (bv 4 2) @?= bv 12 0x142,-          testCase "bvZext" $ do-            bvZext 8 (bv 4 0x8 :: SomeIntN) @?= bv 8 0x08,-          testCase "bvSext" $ do-            bvSext 8 (bv 4 0x8 :: SomeIntN) @?= bv 8 0xF8,-          testCase "bvExt" $ do-            bvExt 8 (bv 4 0x8 :: SomeIntN) @?= bv 8 0xF8-            bvExt 8 (bv 4 0x8 :: SomeWordN) @?= bv 8 0x08,-          testCase "bvSelect" $ do-            bvSelect 1 4 (bv 8 0x17 :: SomeIntN) @?= bv 4 0xB,-          testCase "bv" $ bv 8 0x14 @?= (SomeIntN (0x14 :: IntN 8))-        ],-      testGroup-        "Mergeable"-        [ testGroup "SomeIntN" $ do-            (name, l, r, merged) <--              [ ( "same bitwidth",-                  bv 4 3,-                  bv 4 5,-                  ifWithLeftMost-                    True-                    "cond"-                    (UnionSingle $ bv 4 3)-                    (UnionSingle $ bv 4 5)-                ),-                ( "same bitwidth, should invert",-                  bv 4 5,-                  bv 4 2,-                  ifWithLeftMost-                    True-                    (symNot "cond")-                    (UnionSingle $ bv 4 2)-                    (UnionSingle $ bv 4 5)-                ),-                ( "different bitwidth",-                  bv 4 5,-                  bv 5 4,-                  ifWithLeftMost-                    True-                    "cond"-                    (UnionSingle $ bv 4 5)-                    (UnionSingle $ bv 5 4)-                ),-                ( "different bitwidth, should invert",-                  bv 5 4,-                  bv 4 5,-                  ifWithLeftMost-                    True-                    (symNot "cond")-                    (UnionSingle $ bv 4 5)-                    (UnionSingle $ bv 5 4)-                )-                ]-            return $ testCase name $ do-              let actual =-                    mrgIf "cond" (return l) (return r) :: UnionM SomeIntN-              let expected = UMrg rootStrategy merged-              actual @?= expected,-          testGroup "SomeSymIntN" $ do-            (name, l, r, merged) <--              [ ( "same bitwidth",-                  ssymBV 4 "a",-                  ssymBV 4 "b",-                  (UnionSingle $ symIte "cond" (ssymBV 4 "a") (ssymBV 4 "b"))-                ),-                ( "different bitwidth",-                  ssymBV 4 "a",-                  ssymBV 5 "b",-                  ifWithLeftMost-                    True-                    "cond"-                    (UnionSingle $ ssymBV 4 "a")-                    (UnionSingle $ ssymBV 5 "b")-                ),-                ( "different bitwidth, should invert",-                  ssymBV 5 "b",-                  ssymBV 4 "a",-                  ifWithLeftMost-                    True-                    (symNot "cond")-                    (UnionSingle $ ssymBV 4 "a")-                    (UnionSingle $ ssymBV 5 "b")-                )-                ]-            return $ testCase name $ do-              let actual =-                    mrgIf "cond" (return l) (return r) :: UnionM SomeSymIntN-              let expected = UMrg rootStrategy merged-              actual @?= expected-        ],-      testGroup-        "GenSym"-        [ testCase "Proxy n" $ do-            let actual = genSym (Proxy :: Proxy 4) "a" :: UnionM SomeSymIntN-            let expected = mrgSingle $ isymBV 4 "a" 0-            actual @?= expected,-          testCase "SomeBV" $ do-            let actual =-                  genSym (bv 4 1 :: SomeSymIntN) "a" :: UnionM SomeSymIntN-            let expected = mrgSingle $ isymBV 4 "a" 0-            actual @?= expected,-          testCase "Int" $ do-            let actual =-                  genSym (4 :: Int) "a" :: UnionM SomeSymIntN-            let expected = mrgSingle $ isymBV 4 "a" 0-            actual @?= expected-        ],-      testGroup-        "GenSymSimple"-        [ testCase "Proxy n" $ do-            let actual = genSymSimple (Proxy :: Proxy 4) "a" :: SomeSymIntN-            let expected = isymBV 4 "a" 0-            actual @?= expected,-          testCase "SomeBV" $ do-            let actual =-                  genSymSimple (bv 4 1 :: SomeSymIntN) "a" :: SomeSymIntN-            let expected = isymBV 4 "a" 0-            actual @?= expected,-          testCase "Int" $ do-            let actual = genSymSimple (4 :: Int) "a" :: SomeSymIntN-            let expected = isymBV 4 "a" 0-            actual @?= expected-        ],-      testProperty "arbitraryBV" $-        forAll (arbitraryBV 4) $-          \(bv :: SomeIntN) -> ioProperty $ finiteBitSize bv @?= 4-    ]