grisette 0.4.1.0 → 0.5.0.0

raw patch · 248 files changed

+35639/−30709 lines, 248 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +212/−66
• README.md +17/−7
• grisette.cabal +113/−90
• src/Grisette.hs +4/−4
• src/Grisette/Backend.hs +48/−0
• src/Grisette/Backend/SBV.hs +0/−48
• src/Grisette/Backend/SBV/Data/SMT/Lowering.hs +0/−1882
• src/Grisette/Backend/SBV/Data/SMT/Solving.hs +0/−418
• src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot +0/−54
• src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs +0/−54
• src/Grisette/Core.hs +130/−108
• src/Grisette/Core/BuiltinUnionWrappers.hs +0/−45
• src/Grisette/Core/Control/Exception.hs +0/−47
• src/Grisette/Core/Control/Monad/CBMCExcept.hs +0/−475
• src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs +0/−124
• src/Grisette/Core/Control/Monad/Union.hs +0/−29
• src/Grisette/Core/Control/Monad/UnionM.hs +0/−608
• src/Grisette/Core/Data/BV.hs +0/−844
• src/Grisette/Core/Data/Class/BitVector.hs +0/−234
• src/Grisette/Core/Data/Class/CEGISSolver.hs +0/−614
• src/Grisette/Core/Data/Class/Error.hs +0/−205
• src/Grisette/Core/Data/Class/EvaluateSym.hs +0/−286
• src/Grisette/Core/Data/Class/ExtractSymbolics.hs +0/−323
• src/Grisette/Core/Data/Class/Function.hs +0/−72
• src/Grisette/Core/Data/Class/GPretty.hs +0/−466
• src/Grisette/Core/Data/Class/GenSym.hs +0/−1815
• src/Grisette/Core/Data/Class/ITEOp.hs +0/−88
• src/Grisette/Core/Data/Class/LogicalOp.hs +0/−106
• src/Grisette/Core/Data/Class/Mergeable.hs +0/−1091
• src/Grisette/Core/Data/Class/ModelOps.hs +0/−170
• src/Grisette/Core/Data/Class/SEq.hs +0/−306
• src/Grisette/Core/Data/Class/SOrd.hs +0/−504
• src/Grisette/Core/Data/Class/SafeDivision.hs +0/−379
• src/Grisette/Core/Data/Class/SafeLinearArith.hs +0/−307
• src/Grisette/Core/Data/Class/SafeSymRotate.hs +0/−110
• src/Grisette/Core/Data/Class/SafeSymShift.hs +0/−190
• src/Grisette/Core/Data/Class/SignConversion.hs +0/−37
• src/Grisette/Core/Data/Class/SimpleMergeable.hs +0/−849
• src/Grisette/Core/Data/Class/Solvable.hs +0/−107
• src/Grisette/Core/Data/Class/Solver.hs +0/−288
• src/Grisette/Core/Data/Class/SubstituteSym.hs +0/−318
• src/Grisette/Core/Data/Class/SymRotate.hs +0/−64
• src/Grisette/Core/Data/Class/SymShift.hs +0/−73
• src/Grisette/Core/Data/Class/ToCon.hs +0/−343
• src/Grisette/Core/Data/Class/ToSym.hs +0/−349
• src/Grisette/Core/Data/FileLocation.hs +0/−94
• src/Grisette/Core/Data/MemoUtils.hs +0/−62
• src/Grisette/Core/Data/Union.hs +0/−305
• src/Grisette/Core/TH.hs +0/−142
• src/Grisette/Core/THCompat.hs +0/−74
• src/Grisette/Experimental/GenSymConstrained.hs +67/−57
• src/Grisette/Experimental/MonadParallelUnion.hs +144/−0
• src/Grisette/Experimental/Qualified/ParallelUnionDo.hs +22/−0
• src/Grisette/IR/SymPrim.hs +0/−87
• src/Grisette/IR/SymPrim/Data/IntBitwidth.hs +0/−15
• src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs +0/−124
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs +0/−55
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs +0/−448
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot +0/−237
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/SomeTerm.hs +0/−36
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs +0/−1194
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot +0/−402
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs +0/−194
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs-boot +0/−20
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs +0/−449
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs-boot +0/−31
• src/Grisette/IR/SymPrim/Data/Prim/Model.hs +0/−805
• src/Grisette/IR/SymPrim/Data/Prim/ModelValue.hs +0/−52
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs +0/−237
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs +0/−209
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bool.hs +0/−453
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs +0/−42
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs +0/−98
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs +0/−235
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs +0/−94
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs +0/−48
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs +0/−118
• src/Grisette/IR/SymPrim/Data/Prim/Utils.hs +0/−62
• src/Grisette/IR/SymPrim/Data/SymPrim.hs +0/−1349
• src/Grisette/IR/SymPrim/Data/TabularFun.hs +0/−57
• src/Grisette/Internal/Backend/SBV.hs +0/−20
• src/Grisette/Internal/Backend/Solving.hs +708/−0
• src/Grisette/Internal/Backend/SymBiMap.hs +54/−0
• src/Grisette/Internal/Core.hs +0/−37
• src/Grisette/Internal/Core/Control/Exception.hs +42/−0
• src/Grisette/Internal/Core/Control/Monad/CBMCExcept.hs +481/−0
• src/Grisette/Internal/Core/Control/Monad/Union.hs +30/−0
• src/Grisette/Internal/Core/Control/Monad/UnionM.hs +594/−0
• src/Grisette/Internal/Core/Data/Class/BitVector.hs +254/−0
• src/Grisette/Internal/Core/Data/Class/CEGISSolver.hs +616/−0
• src/Grisette/Internal/Core/Data/Class/Error.hs +206/−0
• src/Grisette/Internal/Core/Data/Class/EvaluateSym.hs +292/−0
• src/Grisette/Internal/Core/Data/Class/ExtractSymbolics.hs +320/−0
• src/Grisette/Internal/Core/Data/Class/Function.hs +66/−0
• src/Grisette/Internal/Core/Data/Class/GPretty.hs +456/−0
• src/Grisette/Internal/Core/Data/Class/GenSym.hs +1708/−0
• src/Grisette/Internal/Core/Data/Class/ITEOp.hs +79/−0
• src/Grisette/Internal/Core/Data/Class/LogicalOp.hs +106/−0
• src/Grisette/Internal/Core/Data/Class/Mergeable.hs +1040/−0
• src/Grisette/Internal/Core/Data/Class/ModelOps.hs +170/−0
• src/Grisette/Internal/Core/Data/Class/PlainUnion.hs +206/−0
• src/Grisette/Internal/Core/Data/Class/SEq.hs +284/−0
• src/Grisette/Internal/Core/Data/Class/SOrd.hs +516/−0
• src/Grisette/Internal/Core/Data/Class/SafeDivision.hs +290/−0
• src/Grisette/Internal/Core/Data/Class/SafeLinearArith.hs +226/−0
• src/Grisette/Internal/Core/Data/Class/SafeSymRotate.hs +138/−0
• src/Grisette/Internal/Core/Data/Class/SafeSymShift.hs +189/−0
• src/Grisette/Internal/Core/Data/Class/SignConversion.hs +37/−0
• src/Grisette/Internal/Core/Data/Class/SimpleMergeable.hs +631/−0
• src/Grisette/Internal/Core/Data/Class/Solvable.hs +143/−0
• src/Grisette/Internal/Core/Data/Class/Solver.hs +288/−0
• src/Grisette/Internal/Core/Data/Class/SubstituteSym.hs +314/−0
• src/Grisette/Internal/Core/Data/Class/SymRotate.hs +92/−0
• src/Grisette/Internal/Core/Data/Class/SymShift.hs +107/−0
• src/Grisette/Internal/Core/Data/Class/ToCon.hs +326/−0
• src/Grisette/Internal/Core/Data/Class/ToSym.hs +316/−0
• src/Grisette/Internal/Core/Data/Class/TryMerge.hs +210/−0
• src/Grisette/Internal/Core/Data/MemoUtils.hs +62/−0
• src/Grisette/Internal/Core/Data/Symbol.hs +217/−0
• src/Grisette/Internal/Core/Data/Union.hs +322/−0
• src/Grisette/Internal/Core/TH/MergeConstructor.hs +189/−0
• src/Grisette/Internal/IR/SymPrim.hs +0/−195
• src/Grisette/Internal/SymPrim/AllSyms.hs +329/−0
• src/Grisette/Internal/SymPrim/BV.hs +496/−0
• src/Grisette/Internal/SymPrim/GeneralFun.hs +686/−0
• src/Grisette/Internal/SymPrim/IntBitwidth.hs +15/−0
• src/Grisette/Internal/SymPrim/ModelRep.hs +44/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs +55/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/BVPEval.hs +582/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalBitwiseTerm.hs +117/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalDivModIntegralTerm.hs +158/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalNumTerm.hs +241/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalOrdTerm.hs +112/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalRotateTerm.hs +143/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalShiftTerm.hs +119/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/SupportedPrim.hs +190/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/IsZero.hs +44/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/PartialEval.hs +94/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs +2359/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Unfold.hs +114/−0
• src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs +62/−0
• src/Grisette/Internal/SymPrim/Prim/Model.hs +775/−0
• src/Grisette/Internal/SymPrim/Prim/ModelValue.hs +52/−0
• src/Grisette/Internal/SymPrim/Prim/SomeTerm.hs +36/−0
• src/Grisette/Internal/SymPrim/Prim/Term.hs +29/−0
• src/Grisette/Internal/SymPrim/Prim/TermUtils.hs +285/−0
• src/Grisette/Internal/SymPrim/SomeBV.hs +975/−0
• src/Grisette/Internal/SymPrim/SymBV.hs +541/−0
• src/Grisette/Internal/SymPrim/SymBool.hs +87/−0
• src/Grisette/Internal/SymPrim/SymGeneralFun.hs +216/−0
• src/Grisette/Internal/SymPrim/SymInteger.hs +101/−0
• src/Grisette/Internal/SymPrim/SymTabularFun.hs +168/−0
• src/Grisette/Internal/SymPrim/TabularFun.hs +483/−0
• src/Grisette/Internal/Utils/Parameterized.hs +272/−0
• src/Grisette/Lib/Base.hs +18/−67
• src/Grisette/Lib/Control/Applicative.hs +173/−0
• src/Grisette/Lib/Control/Monad.hs +447/−35
• src/Grisette/Lib/Control/Monad.hs-boot +10/−12
• src/Grisette/Lib/Control/Monad/Except.hs +92/−11
• src/Grisette/Lib/Control/Monad/State/Class.hs +11/−11
• src/Grisette/Lib/Control/Monad/Trans/Class.hs +4/−5
• src/Grisette/Lib/Control/Monad/Trans/Cont.hs +11/−8
• src/Grisette/Lib/Control/Monad/Trans/Except.hs +70/−0
• src/Grisette/Lib/Control/Monad/Trans/State/Lazy.hs +20/−20
• src/Grisette/Lib/Control/Monad/Trans/State/Strict.hs +20/−20
• src/Grisette/Lib/Data/Bool.hs +13/−0
• src/Grisette/Lib/Data/Either.hs +13/−0
• src/Grisette/Lib/Data/Foldable.hs +252/−24
• src/Grisette/Lib/Data/Functor.hs +79/−0
• src/Grisette/Lib/Data/Functor/Sum.hs +14/−0
• src/Grisette/Lib/Data/List.hs +584/−40
• src/Grisette/Lib/Data/Maybe.hs +13/−0
• src/Grisette/Lib/Data/Traversable.hs +55/−16
• src/Grisette/Lib/Data/Tuple.hs +31/−0
• src/Grisette/Qualified/ParallelUnionDo.hs +0/−22
• src/Grisette/SymPrim.hs +139/−0
• src/Grisette/Utils.hs +1/−3
• src/Grisette/Utils/Parameterized.hs +0/−244
• test/Grisette/Backend/CEGISTests.hs +408/−0
• test/Grisette/Backend/LoweringTests.hs +834/−0
• test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs +0/−415
• test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs +0/−800
• test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs +0/−863
• test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs +0/−331
• test/Grisette/Backend/TermRewritingGen.hs +837/−0
• test/Grisette/Backend/TermRewritingTests.hs +326/−0
• test/Grisette/Core/Control/ExceptionTests.hs +16/−30
• test/Grisette/Core/Control/Monad/UnionMTests.hs +341/−830
• test/Grisette/Core/Control/Monad/UnionTests.hs +7/−7
• test/Grisette/Core/Data/BVTests.hs +47/−7
• test/Grisette/Core/Data/Class/BoolTests.hs +1/−1
• test/Grisette/Core/Data/Class/EvaluateSymTests.hs +12/−13
• test/Grisette/Core/Data/Class/ExtractSymbolicsTests.hs +6/−8
• test/Grisette/Core/Data/Class/GPrettyTests.hs +8/−7
• test/Grisette/Core/Data/Class/GenSymTests.hs +30/−9
• test/Grisette/Core/Data/Class/MergeableTests.hs +8/−10
• test/Grisette/Core/Data/Class/PlainUnionTests.hs +77/−0
• test/Grisette/Core/Data/Class/SEqTests.hs +12/−7
• test/Grisette/Core/Data/Class/SOrdTests.hs +36/−11
• test/Grisette/Core/Data/Class/SafeDivisionTests.hs +278/−0
• test/Grisette/Core/Data/Class/SafeLinearArithTests.hs +191/−0
• test/Grisette/Core/Data/Class/SafeSymRotateTests.hs +15/−13
• test/Grisette/Core/Data/Class/SafeSymShiftTests.hs +15/−13
• test/Grisette/Core/Data/Class/SimpleMergeableTests.hs +7/−32
• test/Grisette/Core/Data/Class/SubstituteSymTests.hs +1/−3
• test/Grisette/Core/Data/Class/SymRotateTests.hs +42/−6
• test/Grisette/Core/Data/Class/SymShiftTests.hs +52/−12
• test/Grisette/Core/Data/Class/TestValues.hs +11/−11
• test/Grisette/Core/Data/Class/ToConTests.hs +7/−5
• test/Grisette/Core/Data/Class/ToSymTests.hs +8/−6
• test/Grisette/Core/Data/Class/TryMergeTests.hs +168/−0
• test/Grisette/Core/Data/Class/UnionLikeTests.hs +0/−298
• test/Grisette/Core/Data/SomeBVTests.hs +382/−0
• test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs +0/−122
• test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs +0/−312
• test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs +0/−738
• test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs +0/−191
• test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs +0/−282
• test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs +0/−408
• test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs +0/−59
• test/Grisette/IR/SymPrim/Data/SymPrimTests.hs +0/−1209
• test/Grisette/IR/SymPrim/Data/TabularFunTests.hs +0/−25
• test/Grisette/Lib/Control/ApplicativeTest.hs +223/−0
• test/Grisette/Lib/Control/Monad/ExceptTests.hs +63/−7
• test/Grisette/Lib/Control/Monad/State/ClassTests.hs +6/−7
• test/Grisette/Lib/Control/Monad/Trans/ClassTests.hs +6/−6
• test/Grisette/Lib/Control/Monad/Trans/ExceptTests.hs +64/−0
• test/Grisette/Lib/Control/Monad/Trans/State/Common.hs +52/−44
• test/Grisette/Lib/Control/Monad/Trans/State/LazyTests.hs +11/−12
• test/Grisette/Lib/Control/Monad/Trans/State/StrictTests.hs +11/−12
• test/Grisette/Lib/Control/MonadTests.hs +506/−37
• test/Grisette/Lib/Data/FoldableTests.hs +267/−100
• test/Grisette/Lib/Data/FunctorTests.hs +96/−0
• test/Grisette/Lib/Data/ListTests.hs +753/−0
• test/Grisette/Lib/Data/TraversableTests.hs +146/−85
• test/Grisette/SymPrim/Prim/BVTests.hs +924/−0
• test/Grisette/SymPrim/Prim/BitsTests.hs +318/−0
• test/Grisette/SymPrim/Prim/BoolTests.hs +734/−0
• test/Grisette/SymPrim/Prim/IntegralTests.hs +184/−0
• test/Grisette/SymPrim/Prim/ModelTests.hs +276/−0
• test/Grisette/SymPrim/Prim/NumTests.hs +405/−0
• test/Grisette/SymPrim/Prim/TabularFunTests.hs +55/−0
• test/Grisette/SymPrim/SymPrimTests.hs +1048/−0
• test/Grisette/SymPrim/TabularFunTests.hs +25/−0
• test/Grisette/TestUtil/NoMerge.hs +29/−0
• test/Grisette/TestUtil/PrettyPrint.hs +41/−0
• test/Grisette/TestUtil/SymbolicAssertion.hs +39/−7
• test/Main.hs +42/−26

@@ -3,61 +3,170 @@ All notable changes to this project will be documented in this file.  The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),-and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).+and this project adheres to [Semantic+Versioning](https://semver.org/spec/v2.0.0.html). +## [Unreleased]++## [0.5.0.0] -- 2024-04-18++### Added++- Added the creation of unparameterized bit vectors from run-time bit-widths.+  ([#168](https://github.com/lsrcz/grisette/pull/168),+  [#177](https://github.com/lsrcz/grisette/pull/177))+- Added all the functions available for the exception transformer in+  `transformers` and `mtl` packages.+  ([#171](https://github.com/lsrcz/grisette/pull/171))+- Improved the partial evaluation for bit vectors.+  ([#176](https://github.com/lsrcz/grisette/pull/176))+- Added `symRotateNegated` and `symShiftNegated`.+  ([#181](https://github.com/lsrcz/grisette/pull/181))+- Added `mrg` and `sym` variants for all reasonable operations from+  `Control.Monad`, `Control.Applicative`, `Data.Foldable`, `Data.List`, and+  `Data.Traversable`. ([#182](https://github.com/lsrcz/grisette/pull/182))+- Added `mrgIfPropagatedStrategy`.+  ([#184](https://github.com/lsrcz/grisette/pull/184))+- Added `freshString`. ([#188](https://github.com/lsrcz/grisette/pull/188))+- Added `localFreshIdent`. ([#190](https://github.com/lsrcz/grisette/pull/190))+- Added deriving for void types for builtin type classes.+  ([#191](https://github.com/lsrcz/grisette/pull/191))++### Fixed++- Fixed the merging for safe division.+  ([#173](https://github.com/lsrcz/grisette/pull/173))+- Fixed the behavior for safe `mod` and `rem` for signed, bounded concrete+  types. ([#173](https://github.com/lsrcz/grisette/pull/173))+- Fixed merging in `mrg*` operations for monad transformers to ensure that they+  merge the results. ([#187](https://github.com/lsrcz/grisette/pull/187))++### Changed++- [Breaking] Removed the `UnionLike` and `UnionPrjOp` interface, added the+  `TryMerge` and `PlainUnion` interface. This allows `mrg*` operations to be+  used with non-union programs.+  ([#170](https://github.com/lsrcz/grisette/pull/170))+- [Breaking] Refined the safe operations interface using `TryMerge`.+  ([#172](https://github.com/lsrcz/grisette/pull/172))+- [Breaking] Renamed `safeMinus` to `safeSub` to be more consistent.+  ([#172](https://github.com/lsrcz/grisette/pull/172))+- [Breaking] Unifies the implementation for all symbolic non-indexed+  bit-vectors. The legacy types are now type and pattern synonyms.+  ([#174](https://github.com/lsrcz/grisette/pull/174),+  [#179](https://github.com/lsrcz/grisette/pull/179),+  [#180](https://github.com/lsrcz/grisette/pull/180))+- [Breaking] Use functional dependency instead of type family for the `Function`+  class. ([#178](https://github.com/lsrcz/grisette/pull/178))+- [Breaking] Added `Mergeable` constraints to some `mrg*` list operators+  ([#182](https://github.com/lsrcz/grisette/pull/182))+- [Breaking] Refactored the `mrg*` constructor related template haskell code.+  ([#185](https://github.com/lsrcz/grisette/pull/185))+- [Breaking] Dropped symbols with extra information.+  ([#188](https://github.com/lsrcz/grisette/pull/188))+- [Breaking] The `FreshIdent` is removed. It is now changed to `Identifier` and+  `Symbol` types. ([#192](https://github.com/lsrcz/grisette/pull/192))+- Changed the internal representation of the terms.+  ([#193](https://github.com/lsrcz/grisette/pull/193))+- [Breaking] Refactored the project structures.+  ([#194](https://github.com/lsrcz/grisette/pull/194))+ ## [0.4.1.0] -- 2024-01-10  ### Added -- Added `cegisForAll` interfaces. ([#165])(https://github.com/lsrcz/grisette/pull/165)+- Added `cegisForAll` interfaces.+  ([#165](https://github.com/lsrcz/grisette/pull/165))  ## [0.4.0.0] -- 2024-01-08  ### Added -- Added wrappers for state transformers. ([#132](https://github.com/lsrcz/grisette/pull/132))-- Added `toGuardList` function. ([#137](https://github.com/lsrcz/grisette/pull/137))-- Exported some previously hidden API (`BVSignConversion`, `runFreshTFromIndex`) that we found useful or forgot to export. ([#138](https://github.com/lsrcz/grisette/pull/138), [#139](https://github.com/lsrcz/grisette/pull/139))-- Provided `mrgRunFreshT` to run `FreshT` with merging. ([#140](https://github.com/lsrcz/grisette/pull/140))-- Added `Grisette.Data.Class.SignConversion.SignConversion` for types from `Data.Int` and `Data.Word`. ([#142](https://github.com/lsrcz/grisette/pull/142))-- Added shift functions by symbolic shift amounts. ([#151](https://github.com/lsrcz/grisette/pull/151))-- Added `apply` for uninterpreted functions. ([#155](https://github.com/lsrcz/grisette/pull/155))-- Added `liftFresh` to lift a `Fresh` into `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/156))-- Added a handle types for SBV solvers. This allows users to use SBV solvers without the need to wrap everything in the SBV monads. ([#159](https://github.com/lsrcz/grisette/pull/159))-- Added a new generic CEGIS interface. This allows any verifier/fuzzer to be used in the CEGIS loop. ([#159](https://github.com/lsrcz/grisette/pull/159))+- Added wrappers for state transformers.+  ([#132](https://github.com/lsrcz/grisette/pull/132))+- Added `toGuardList` function.+  ([#137](https://github.com/lsrcz/grisette/pull/137))+- Exported some previously hidden API (`BVSignConversion`, `runFreshTFromIndex`)+  that we found useful or forgot to export.+  ([#138](https://github.com/lsrcz/grisette/pull/138),+  [#139](https://github.com/lsrcz/grisette/pull/139))+- Provided `mrgRunFreshT` to run `FreshT` with merging.+  ([#140](https://github.com/lsrcz/grisette/pull/140))+- Added `Grisette.Data.Class.SignConversion.SignConversion` for types from+  `Data.Int` and `Data.Word`.+  ([#142](https://github.com/lsrcz/grisette/pull/142))+- Added shift functions by symbolic shift amounts.+  ([#151](https://github.com/lsrcz/grisette/pull/151))+- Added `apply` for uninterpreted functions.+  ([#155](https://github.com/lsrcz/grisette/pull/155))+- Added `liftFresh` to lift a `Fresh` into `MonadFresh`.+  ([#156](https://github.com/lsrcz/grisette/pull/156))+- Added a handle types for SBV solvers. This allows users to use SBV solvers+  without the need to wrap everything in the SBV monads.+  ([#159](https://github.com/lsrcz/grisette/pull/159))+- Added a new generic CEGIS interface. This allows any verifier/fuzzer to be+  used in the CEGIS loop. ([#159](https://github.com/lsrcz/grisette/pull/159))  ### Removed -- [Breaking] Removed the `Grisette.Lib.Mtl` module. ([#132](https://github.com/lsrcz/grisette/pull/132))-- [Breaking] Removed `SymBoolOp` and `SymIntegerOp`. ([#146](https://github.com/lsrcz/grisette/pull/146))-- [Breaking] Removed `ExtractSymbolics` instance for `SymbolSet`. ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Removed the `Grisette.Lib.Mtl` module.+  ([#132](https://github.com/lsrcz/grisette/pull/132))+- [Breaking] Removed `SymBoolOp` and `SymIntegerOp`.+  ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Removed `ExtractSymbolics` instance for `SymbolSet`.+  ([#146](https://github.com/lsrcz/grisette/pull/146))  ### Fixed -- Removed the quotation marks around the pretty printed results for string-like data types. ([#127](https://github.com/lsrcz/grisette/pull/127))-- Fixed the `SOrd` instance for `VerificationConditions`. ([#131](https://github.com/lsrcz/grisette/pull/131))-- Fixed the missing `SubstituteSym` instance for `UnionM`. ([#131](https://github.com/lsrcz/grisette/pull/131))-- Fixed the symbolic generation order for `Maybe`. ([#131](https://github.com/lsrcz/grisette/pull/131))-- Fixed the `toInteger` function for `IntN 1`. ([#143](https://github.com/lsrcz/grisette/pull/143))-- Fixed the `abs` function for `WordN`. ([#144](https://github.com/lsrcz/grisette/pull/143))-- Fixed the QuickCheck shrink function for `WordN 1` and `IntN 1`. ([#149](https://github.com/lsrcz/grisette/pull/149))-- Fixed the heap overflow bug for `shiftL` for `WordN` and `IntN` by large numbers. ([#150](https://github.com/lsrcz/grisette/pull/150))+- Removed the quotation marks around the pretty printed results for string-like+  data types. ([#127](https://github.com/lsrcz/grisette/pull/127))+- Fixed the `SOrd` instance for `VerificationConditions`.+  ([#131](https://github.com/lsrcz/grisette/pull/131))+- Fixed the missing `SubstituteSym` instance for `UnionM`.+  ([#131](https://github.com/lsrcz/grisette/pull/131))+- Fixed the symbolic generation order for `Maybe`.+  ([#131](https://github.com/lsrcz/grisette/pull/131))+- Fixed the `toInteger` function for `IntN 1`.+  ([#143](https://github.com/lsrcz/grisette/pull/143))+- Fixed the `abs` function for `WordN`.+  ([#144](https://github.com/lsrcz/grisette/pull/143))+- Fixed the QuickCheck shrink function for `WordN 1` and `IntN 1`.+  ([#149](https://github.com/lsrcz/grisette/pull/149))+- Fixed the heap overflow bug for `shiftL` for `WordN` and `IntN` by large+  numbers. ([#150](https://github.com/lsrcz/grisette/pull/150))  ### Changed -- Reorganized the files for `MonadTrans`. ([#132](https://github.com/lsrcz/grisette/pull/132))-- [Breaking] Changed the name of `Union` constructors and patterns. ([#133](https://github.com/lsrcz/grisette/pull/133))-- The `Union` patterns, when used as constructors, now merges the result. ([#133](https://github.com/lsrcz/grisette/pull/133))-- Changed the symbolic identifier type from `String` to `Data.Text.Text`. ([#141](https://github.com/lsrcz/grisette/pull/141))-- [Breaking] `Grisette.Data.Class.BitVector.BVSignConversion` is now `Grisette.Data.Class.SignConversion.SignConversion`. ([#142](https://github.com/lsrcz/grisette/pull/142))-- [Breaking] Moved the `ITEOp`, `LogicalOp`, and `SEq` type classes to dedicated modules. ([#146](https://github.com/lsrcz/grisette/pull/146))-- [Breaking] Moved `Grisette.Data.Class.Evaluate` to `Grisette.Data.Class.EvaluateSym`. ([#146](https://github.com/lsrcz/grisette/pull/146))-- [Breaking] Moved `Grisette.Data.Class.Substitute` to `Grisette.Data.Class.SubstituteSym`. ([#146](https://github.com/lsrcz/grisette/pull/146))-- [Breaking] Split the `Grisette.Data.Class.SafeArith` module to `Grisette.Data.Class.SafeDivision` and `Grisette.Data.Class.SafeLinearArith`. ([#146](https://github.com/lsrcz/grisette/pull/146))-- [Breaking] Changed the API to `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/156))-- [Breaking] Renamed multiple symbolic operators. ([#158](https://github.com/lsrcz/grisette/pull/158))-- [Breaking] Changed the solver interface. ([#159](https://github.com/lsrcz/grisette/pull/159))-- [Breaking] Changed the CEGIS solver interface. ([#159](https://github.com/lsrcz/grisette/pull/159))+- Reorganized the files for `MonadTrans`.+  ([#132](https://github.com/lsrcz/grisette/pull/132))+- [Breaking] Changed the name of `Union` constructors and patterns.+  ([#133](https://github.com/lsrcz/grisette/pull/133))+- The `Union` patterns, when used as constructors, now merges the result.+  ([#133](https://github.com/lsrcz/grisette/pull/133))+- Changed the symbolic identifier type from `String` to `Data.Text.Text`.+  ([#141](https://github.com/lsrcz/grisette/pull/141))+- [Breaking] `Grisette.Data.Class.BitVector.BVSignConversion` is now+  `Grisette.Data.Class.SignConversion.SignConversion`.+  ([#142](https://github.com/lsrcz/grisette/pull/142))+- [Breaking] Moved the `ITEOp`, `LogicalOp`, and `SEq` type classes to dedicated+  modules. ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Moved `Grisette.Data.Class.Evaluate` to+  `Grisette.Data.Class.EvaluateSym`.+  ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Moved `Grisette.Data.Class.Substitute` to+  `Grisette.Data.Class.SubstituteSym`.+  ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Split the `Grisette.Data.Class.SafeArith` module to+  `Grisette.Data.Class.SafeDivision` and `Grisette.Data.Class.SafeLinearArith`.+  ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Changed the API to `MonadFresh`.+  ([#156](https://github.com/lsrcz/grisette/pull/156))+- [Breaking] Renamed multiple symbolic operators.+  ([#158](https://github.com/lsrcz/grisette/pull/158))+- [Breaking] Changed the solver interface.+  ([#159](https://github.com/lsrcz/grisette/pull/159))+- [Breaking] Changed the CEGIS solver interface.+  ([#159](https://github.com/lsrcz/grisette/pull/159))  ## [0.3.1.1] -- 2023-09-29 @@ -67,63 +176,98 @@  ### Added -- Added support to `Data.Text`. ([#95](https://github.com/lsrcz/grisette/pull/95))-- Added `Arbitrary` instances for bit vectors. ([#97](https://github.com/lsrcz/grisette/pull/97))-- Added pretty printers for Grisette data types. ([#101](https://github.com/lsrcz/grisette/pull/101))-- Added `ExtractSymbolics` instances for tuples longer than 2. ([#103](https://github.com/lsrcz/grisette/pull/103))+- Added support to `Data.Text`.+  ([#95](https://github.com/lsrcz/grisette/pull/95))+- Added `Arbitrary` instances for bit vectors.+  ([#97](https://github.com/lsrcz/grisette/pull/97))+- Added pretty printers for Grisette data types.+  ([#101](https://github.com/lsrcz/grisette/pull/101))+- Added `ExtractSymbolics` instances for tuples longer than 2.+  ([#103](https://github.com/lsrcz/grisette/pull/103))  ### Fixed -- Fixed the `Read` instance for bit vectors. ([#99](https://github.com/lsrcz/grisette/pull/99), [#100](https://github.com/lsrcz/grisette/pull/100))+- Fixed the `Read` instance for bit vectors.+  ([#99](https://github.com/lsrcz/grisette/pull/99),+  [#100](https://github.com/lsrcz/grisette/pull/100))  ## [0.3.0.0] -- 2023-07-07  ### Added -- Added the conversion between signed and unsigned bit vectors. ([#69](https://github.com/lsrcz/grisette/pull/69))-- Added the generation of `SomeSymIntN` and `SomeSymWordN` from a single `Int` for bit width. ([#73](https://github.com/lsrcz/grisette/pull/73))-- Added the `FiniteBits` instance for `SomeSymIntN` and `SomeSymWordN`. ([#83](https://github.com/lsrcz/grisette/pull/83))-- Added more flexible instances for symbolic generation for `Either`, `Maybe` and list types. ([#84](https://github.com/lsrcz/grisette/pull/84))-- Added an experimental `GenSymConstrained` type class. ([#89](https://github.com/lsrcz/grisette/pull/89))+- Added the conversion between signed and unsigned bit vectors.+  ([#69](https://github.com/lsrcz/grisette/pull/69))+- Added the generation of `SomeSymIntN` and `SomeSymWordN` from a single `Int`+  for bit width. ([#73](https://github.com/lsrcz/grisette/pull/73))+- Added the `FiniteBits` instance for `SomeSymIntN` and `SomeSymWordN`.+  ([#83](https://github.com/lsrcz/grisette/pull/83))+- Added more flexible instances for symbolic generation for `Either`, `Maybe`+  and list types. ([#84](https://github.com/lsrcz/grisette/pull/84))+- Added an experimental `GenSymConstrained` type class.+  ([#89](https://github.com/lsrcz/grisette/pull/89))  ### Changed -- Changed the operations for `SomeIntN` and `SomeWordN` to accepting dynamic runtime integers rather than compile-time integers. ([#71](https://github.com/lsrcz/grisette/pull/71))-- Comparing the equality of `SomeIntN`/`SomeWordN`/`SomeSymIntN`/`SomeSymWordN` with different bit widths returns false rather than crash now. ([#74](https://github.com/lsrcz/grisette/pull/74))+- Changed the operations for `SomeIntN` and `SomeWordN` to accepting dynamic+  runtime integers rather than compile-time integers.+  ([#71](https://github.com/lsrcz/grisette/pull/71))+- Comparing the equality of `SomeIntN`/`SomeWordN`/`SomeSymIntN`/`SomeSymWordN`+  with different bit widths returns false rather than crash now.+  ([#74](https://github.com/lsrcz/grisette/pull/74))  ### Fixed -- Fixed the compatibility issue with sbv 10+. ([#66](https://github.com/lsrcz/grisette/pull/66))-- Fixed build error with newer GHC. ([#70](https://github.com/lsrcz/grisette/pull/70))-- Fixed the merging for `SomeSymIntN` and `SomeSymWordN`. ([#72](https://github.com/lsrcz/grisette/pull/72))+- Fixed the compatibility issue with sbv 10+.+  ([#66](https://github.com/lsrcz/grisette/pull/66))+- Fixed build error with newer GHC.+  ([#70](https://github.com/lsrcz/grisette/pull/70))+- Fixed the merging for `SomeSymIntN` and `SomeSymWordN`.+  ([#72](https://github.com/lsrcz/grisette/pull/72))  ## [0.2.0.0] - 2023-04-13  ### Added -- Add term size count API. ([#48](https://github.com/lsrcz/grisette/pull/48), [#53](https://github.com/lsrcz/grisette/pull/53))-- Add timeout to solver interface. ([#49](https://github.com/lsrcz/grisette/pull/49), [#50](https://github.com/lsrcz/grisette/pull/50))-- Add parallel do-notation for parallel symbolic compilation. ([#51](https://github.com/lsrcz/grisette/pull/51))-- Added some missing instances for symbolic values and bit vectors. ([#46](https://github.com/lsrcz/grisette/pull/46), [#61](https://github.com/lsrcz/grisette/pull/61))-- Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59))+- Add term size count API. ([#48](https://github.com/lsrcz/grisette/pull/48),+  [#53](https://github.com/lsrcz/grisette/pull/53))+- Add timeout to solver interface.+  ([#49](https://github.com/lsrcz/grisette/pull/49),+  [#50](https://github.com/lsrcz/grisette/pull/50))+- Add parallel do-notation for parallel symbolic compilation.+  ([#51](https://github.com/lsrcz/grisette/pull/51))+- Added some missing instances for symbolic values and bit vectors.+  ([#46](https://github.com/lsrcz/grisette/pull/46),+  [#61](https://github.com/lsrcz/grisette/pull/61))+- Add missing instances for `MonadFresh` and `FreshT`.+  ([#59](https://github.com/lsrcz/grisette/pull/59))  ### Changed -- New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56))+- New safe operator interfaces.+  ([#56](https://github.com/lsrcz/grisette/pull/56)) - Redesigned symbolic value interface.-  - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced with `SymBool` and `SymInteger`. ([#41](https://github.com/lsrcz/grisette/pull/41))-  - New symbolic bit vector interface. Added unsized bit vector. ([#41](https://github.com/lsrcz/grisette/pull/41))+  - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced+    with `SymBool` and `SymInteger`.+    ([#41](https://github.com/lsrcz/grisette/pull/41))+  - New symbolic bit vector interface. Added unsized bit vector.+    ([#41](https://github.com/lsrcz/grisette/pull/41))  ### Removed -- Dropped merging cache for `UnionM`. This fixed some segmentation fault errors. ([#43](https://github.com/lsrcz/grisette/pull/43))+- Dropped merging cache for `UnionM`. This fixed some segmentation fault errors.+  ([#43](https://github.com/lsrcz/grisette/pull/43))  ### Fixed -- Fix CEGIS when no symbolic input is present. ([#52](https://github.com/lsrcz/grisette/pull/52))-- Fix overlapping `ToSym` and `ToCon` instances. ([#54](https://github.com/lsrcz/grisette/pull/54))-- Fix uninterpreted function lowering. ([#57](https://github.com/lsrcz/grisette/pull/57), [#58](https://github.com/lsrcz/grisette/pull/58))-- Fix CEGIS crash when subsequent solver calls introduces new symbolic constant. ([#60](https://github.com/lsrcz/grisette/pull/60))+- Fix CEGIS when no symbolic input is present.+  ([#52](https://github.com/lsrcz/grisette/pull/52))+- Fix overlapping `ToSym` and `ToCon` instances.+  ([#54](https://github.com/lsrcz/grisette/pull/54))+- Fix uninterpreted function lowering.+  ([#57](https://github.com/lsrcz/grisette/pull/57),+  [#58](https://github.com/lsrcz/grisette/pull/58))+- Fix CEGIS crash when subsequent solver calls introduces new symbolic constant.+  ([#60](https://github.com/lsrcz/grisette/pull/60))  ## [0.1.0.0] - 2023-01-20 @@ -131,8 +275,10 @@  - Initial release for Grisette. -[0.4.1.0]: https://github.com/lsrcz/grisette/compare/v0.4.1.0...v0.4.0.0-[0.4.0.0]: https://github.com/lsrcz/grisette/compare/v0.4.0.0...v0.3.1.0+[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.5.0.0...HEAD+[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+[0.4.0.0]: https://github.com/lsrcz/grisette/compare/v0.3.1.1...v0.4.0.0 [0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0 [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0

@@ -47,7 +47,7 @@ ```cabal library   ...-  build-depends: grisette >= 0.4.1 < 0.5+  build-depends: grisette >= 0.5 < 0.6 ```  #### Quick start template with `stack new`@@ -151,6 +151,15 @@ returned by a solver to replace the symbolic holes inside to concrete values.  ```haskell+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++import Grisette+import GHC.Generics+ data SExpr   -- `SConst` represents a constant in the syntax tree.   --@@ -180,8 +189,8 @@ -- >>> SConst 1 :: SExpr -- SConst 1 -- >>> mrgSConst 1 :: UnionM SExpr--- UMrg (Single (SConst 1))-$(makeUnionWrapper "mrg" ''SExpr)+-- {SConst 1}+mkMergeConstructor "mrg" ''SExpr ```  Then we can define the program space.@@ -204,7 +213,8 @@  ```haskell interpret :: SExpr -> SymInteger-interpret (SInt x) = x+interpret (SConst x) = x+interpret (SInput x) = x interpret (SPlus x y) = interpretU x + interpretU y interpret (SMul x y) = interpretU x * interpretU y @@ -227,7 +237,7 @@ ```haskell example :: IO () example = do-  Right model <- solve (UnboundedReasoning z3) $ executableSpace 2 ==~ 5+  Right model <- solve (precise z3) $ executableSpace 2 .== 5   print $ evaluateSym False model (space "x")   -- result: SPlus {SInput x} {SConst 3}   let synthesizedProgram :: Integer -> Integer =@@ -241,8 +251,8 @@ ## Documentation  - Haddock documentation at [grisette](https://hackage.haskell.org/package/grisette).-- Grisette essentials (WIP).-- Grisette tutorials (WIP).+- A tutorial to Grisette is in the [tutorials](tutorials) directory. They are+  provided as jupyter notebooks with the [IHaskell](https://github.com/IHaskell/IHaskell) kernel.  ## License 

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           grisette-version:        0.4.1.0+version:        0.5.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,7 +29,8 @@   , GHC == 9.0.2   , GHC == 9.2.8   , GHC == 9.4.8-  , GHC == 9.6.3+  , GHC == 9.6.4+  , GHC == 9.8.2 extra-source-files:     CHANGELOG.md     README.md@@ -46,94 +47,106 @@ library   exposed-modules:       Grisette-      Grisette.Backend.SBV-      Grisette.Backend.SBV.Data.SMT.Lowering-      Grisette.Backend.SBV.Data.SMT.Solving-      Grisette.Backend.SBV.Data.SMT.SymBiMap+      Grisette.Backend       Grisette.Core-      Grisette.Core.BuiltinUnionWrappers-      Grisette.Core.Control.Exception-      Grisette.Core.Control.Monad.CBMCExcept-      Grisette.Core.Control.Monad.Class.MonadParallelUnion-      Grisette.Core.Control.Monad.Union-      Grisette.Core.Control.Monad.UnionM-      Grisette.Core.Data.BV-      Grisette.Core.Data.Class.BitVector-      Grisette.Core.Data.Class.CEGISSolver-      Grisette.Core.Data.Class.Error-      Grisette.Core.Data.Class.EvaluateSym-      Grisette.Core.Data.Class.ExtractSymbolics-      Grisette.Core.Data.Class.Function-      Grisette.Core.Data.Class.GenSym-      Grisette.Core.Data.Class.GPretty-      Grisette.Core.Data.Class.ITEOp-      Grisette.Core.Data.Class.LogicalOp-      Grisette.Core.Data.Class.Mergeable-      Grisette.Core.Data.Class.ModelOps-      Grisette.Core.Data.Class.SafeDivision-      Grisette.Core.Data.Class.SafeLinearArith-      Grisette.Core.Data.Class.SafeSymRotate-      Grisette.Core.Data.Class.SafeSymShift-      Grisette.Core.Data.Class.SEq-      Grisette.Core.Data.Class.SignConversion-      Grisette.Core.Data.Class.SimpleMergeable-      Grisette.Core.Data.Class.Solvable-      Grisette.Core.Data.Class.Solver-      Grisette.Core.Data.Class.SOrd-      Grisette.Core.Data.Class.SubstituteSym-      Grisette.Core.Data.Class.SymRotate-      Grisette.Core.Data.Class.SymShift-      Grisette.Core.Data.Class.ToCon-      Grisette.Core.Data.Class.ToSym-      Grisette.Core.Data.FileLocation-      Grisette.Core.Data.MemoUtils-      Grisette.Core.Data.Union-      Grisette.Core.TH-      Grisette.Core.THCompat       Grisette.Experimental       Grisette.Experimental.GenSymConstrained-      Grisette.Internal.Backend.SBV-      Grisette.Internal.Core-      Grisette.Internal.IR.SymPrim-      Grisette.IR.SymPrim-      Grisette.IR.SymPrim.Data.IntBitwidth-      Grisette.IR.SymPrim.Data.Prim.Helpers-      Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches-      Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-      Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm-      Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-      Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution-      Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-      Grisette.IR.SymPrim.Data.Prim.Model-      Grisette.IR.SymPrim.Data.Prim.ModelValue-      Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits-      Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool-      Grisette.IR.SymPrim.Data.Prim.PartialEval.BV-      Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun-      Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral-      Grisette.IR.SymPrim.Data.Prim.PartialEval.Num-      Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval-      Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun-      Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold-      Grisette.IR.SymPrim.Data.Prim.Utils-      Grisette.IR.SymPrim.Data.SymPrim-      Grisette.IR.SymPrim.Data.TabularFun+      Grisette.Experimental.MonadParallelUnion+      Grisette.Experimental.Qualified.ParallelUnionDo+      Grisette.Internal.Backend.Solving+      Grisette.Internal.Backend.SymBiMap+      Grisette.Internal.Core.Control.Exception+      Grisette.Internal.Core.Control.Monad.CBMCExcept+      Grisette.Internal.Core.Control.Monad.Union+      Grisette.Internal.Core.Control.Monad.UnionM+      Grisette.Internal.Core.Data.Class.BitVector+      Grisette.Internal.Core.Data.Class.CEGISSolver+      Grisette.Internal.Core.Data.Class.Error+      Grisette.Internal.Core.Data.Class.EvaluateSym+      Grisette.Internal.Core.Data.Class.ExtractSymbolics+      Grisette.Internal.Core.Data.Class.Function+      Grisette.Internal.Core.Data.Class.GenSym+      Grisette.Internal.Core.Data.Class.GPretty+      Grisette.Internal.Core.Data.Class.ITEOp+      Grisette.Internal.Core.Data.Class.LogicalOp+      Grisette.Internal.Core.Data.Class.Mergeable+      Grisette.Internal.Core.Data.Class.ModelOps+      Grisette.Internal.Core.Data.Class.PlainUnion+      Grisette.Internal.Core.Data.Class.SafeDivision+      Grisette.Internal.Core.Data.Class.SafeLinearArith+      Grisette.Internal.Core.Data.Class.SafeSymRotate+      Grisette.Internal.Core.Data.Class.SafeSymShift+      Grisette.Internal.Core.Data.Class.SEq+      Grisette.Internal.Core.Data.Class.SignConversion+      Grisette.Internal.Core.Data.Class.SimpleMergeable+      Grisette.Internal.Core.Data.Class.Solvable+      Grisette.Internal.Core.Data.Class.Solver+      Grisette.Internal.Core.Data.Class.SOrd+      Grisette.Internal.Core.Data.Class.SubstituteSym+      Grisette.Internal.Core.Data.Class.SymRotate+      Grisette.Internal.Core.Data.Class.SymShift+      Grisette.Internal.Core.Data.Class.ToCon+      Grisette.Internal.Core.Data.Class.ToSym+      Grisette.Internal.Core.Data.Class.TryMerge+      Grisette.Internal.Core.Data.MemoUtils+      Grisette.Internal.Core.Data.Symbol+      Grisette.Internal.Core.Data.Union+      Grisette.Internal.Core.TH.MergeConstructor+      Grisette.Internal.SymPrim.AllSyms+      Grisette.Internal.SymPrim.BV+      Grisette.Internal.SymPrim.GeneralFun+      Grisette.Internal.SymPrim.IntBitwidth+      Grisette.Internal.SymPrim.ModelRep+      Grisette.Internal.SymPrim.Prim.Internal.Caches+      Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm+      Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim+      Grisette.Internal.SymPrim.Prim.Internal.IsZero+      Grisette.Internal.SymPrim.Prim.Internal.PartialEval+      Grisette.Internal.SymPrim.Prim.Internal.Term+      Grisette.Internal.SymPrim.Prim.Internal.Unfold+      Grisette.Internal.SymPrim.Prim.Internal.Utils+      Grisette.Internal.SymPrim.Prim.Model+      Grisette.Internal.SymPrim.Prim.ModelValue+      Grisette.Internal.SymPrim.Prim.SomeTerm+      Grisette.Internal.SymPrim.Prim.Term+      Grisette.Internal.SymPrim.Prim.TermUtils+      Grisette.Internal.SymPrim.SomeBV+      Grisette.Internal.SymPrim.SymBool+      Grisette.Internal.SymPrim.SymBV+      Grisette.Internal.SymPrim.SymGeneralFun+      Grisette.Internal.SymPrim.SymInteger+      Grisette.Internal.SymPrim.SymTabularFun+      Grisette.Internal.SymPrim.TabularFun+      Grisette.Internal.Utils.Parameterized       Grisette.Lib.Base+      Grisette.Lib.Control.Applicative       Grisette.Lib.Control.Monad       Grisette.Lib.Control.Monad.Except       Grisette.Lib.Control.Monad.State.Class       Grisette.Lib.Control.Monad.Trans       Grisette.Lib.Control.Monad.Trans.Class       Grisette.Lib.Control.Monad.Trans.Cont+      Grisette.Lib.Control.Monad.Trans.Except       Grisette.Lib.Control.Monad.Trans.State       Grisette.Lib.Control.Monad.Trans.State.Lazy       Grisette.Lib.Control.Monad.Trans.State.Strict+      Grisette.Lib.Data.Bool+      Grisette.Lib.Data.Either       Grisette.Lib.Data.Foldable+      Grisette.Lib.Data.Functor+      Grisette.Lib.Data.Functor.Sum       Grisette.Lib.Data.List+      Grisette.Lib.Data.Maybe       Grisette.Lib.Data.Traversable-      Grisette.Qualified.ParallelUnionDo+      Grisette.Lib.Data.Tuple+      Grisette.SymPrim       Grisette.Utils-      Grisette.Utils.Parameterized   other-modules:       Paths_grisette   hs-source-dirs:@@ -154,7 +167,7 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <10.4+    , sbv >=8.11 && <11     , stm ==2.5.*     , template-haskell >=2.16 && <2.22     , text >=1.2.4.1 && <2.2@@ -193,7 +206,7 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <10.4+    , sbv >=8.11 && <11     , stm ==2.5.*     , template-haskell >=2.16 && <2.22     , text >=1.2.4.1 && <2.2@@ -210,10 +223,10 @@   type: exitcode-stdio-1.0   main-is: Main.hs   other-modules:-      Grisette.Backend.SBV.Data.SMT.CEGISTests-      Grisette.Backend.SBV.Data.SMT.LoweringTests-      Grisette.Backend.SBV.Data.SMT.TermRewritingGen-      Grisette.Backend.SBV.Data.SMT.TermRewritingTests+      Grisette.Backend.CEGISTests+      Grisette.Backend.LoweringTests+      Grisette.Backend.TermRewritingGen+      Grisette.Backend.TermRewritingTests       Grisette.Core.Control.ExceptionTests       Grisette.Core.Control.Monad.UnionMTests       Grisette.Core.Control.Monad.UnionTests@@ -224,6 +237,9 @@       Grisette.Core.Data.Class.GenSymTests       Grisette.Core.Data.Class.GPrettyTests       Grisette.Core.Data.Class.MergeableTests+      Grisette.Core.Data.Class.PlainUnionTests+      Grisette.Core.Data.Class.SafeDivisionTests+      Grisette.Core.Data.Class.SafeLinearArithTests       Grisette.Core.Data.Class.SafeSymRotateTests       Grisette.Core.Data.Class.SafeSymShiftTests       Grisette.Core.Data.Class.SEqTests@@ -235,25 +251,32 @@       Grisette.Core.Data.Class.TestValues       Grisette.Core.Data.Class.ToConTests       Grisette.Core.Data.Class.ToSymTests-      Grisette.Core.Data.Class.UnionLikeTests-      Grisette.IR.SymPrim.Data.Prim.BitsTests-      Grisette.IR.SymPrim.Data.Prim.BoolTests-      Grisette.IR.SymPrim.Data.Prim.BVTests-      Grisette.IR.SymPrim.Data.Prim.IntegralTests-      Grisette.IR.SymPrim.Data.Prim.ModelTests-      Grisette.IR.SymPrim.Data.Prim.NumTests-      Grisette.IR.SymPrim.Data.Prim.TabularFunTests-      Grisette.IR.SymPrim.Data.SymPrimTests-      Grisette.IR.SymPrim.Data.TabularFunTests+      Grisette.Core.Data.Class.TryMergeTests+      Grisette.Core.Data.SomeBVTests+      Grisette.Lib.Control.ApplicativeTest       Grisette.Lib.Control.Monad.ExceptTests       Grisette.Lib.Control.Monad.State.ClassTests       Grisette.Lib.Control.Monad.Trans.ClassTests+      Grisette.Lib.Control.Monad.Trans.ExceptTests       Grisette.Lib.Control.Monad.Trans.State.Common       Grisette.Lib.Control.Monad.Trans.State.LazyTests       Grisette.Lib.Control.Monad.Trans.State.StrictTests       Grisette.Lib.Control.MonadTests       Grisette.Lib.Data.FoldableTests+      Grisette.Lib.Data.FunctorTests+      Grisette.Lib.Data.ListTests       Grisette.Lib.Data.TraversableTests+      Grisette.SymPrim.Prim.BitsTests+      Grisette.SymPrim.Prim.BoolTests+      Grisette.SymPrim.Prim.BVTests+      Grisette.SymPrim.Prim.IntegralTests+      Grisette.SymPrim.Prim.ModelTests+      Grisette.SymPrim.Prim.NumTests+      Grisette.SymPrim.Prim.TabularFunTests+      Grisette.SymPrim.SymPrimTests+      Grisette.SymPrim.TabularFunTests+      Grisette.TestUtil.NoMerge+      Grisette.TestUtil.PrettyPrint       Grisette.TestUtil.SymbolicAssertion       Paths_grisette   hs-source-dirs:@@ -276,7 +299,7 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <10.4+    , sbv >=8.11 && <11     , stm ==2.5.*     , template-haskell >=2.16 && <2.22     , test-framework >=0.8.2 && <0.9

@@ -17,18 +17,18 @@     module Grisette.Lib.Base,      -- * Symbolic primitives-    module Grisette.IR.SymPrim,+    module Grisette.SymPrim,      -- * Solver backend-    module Grisette.Backend.SBV,+    module Grisette.Backend,      -- * Utils     module Grisette.Utils,   ) where -import Grisette.Backend.SBV+import Grisette.Backend import Grisette.Core-import Grisette.IR.SymPrim import Grisette.Lib.Base+import Grisette.SymPrim import Grisette.Utils

@@ -0,0 +1,48 @@+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-}++-- |+-- Module      :   Grisette.Backend+-- Copyright   :   (c) Sirui Lu 2021-2023+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Backend+  ( -- * Grisette.Internal.SBV backend configuration+    ApproximationConfig (..),+    ExtraConfig (..),+    precise,+    approx,+    withTimeout,+    clearTimeout,+    withApprox,+    clearApprox,+    GrisetteSMTConfig (..),++    -- * SBV backend solver configuration+    SBV.SMTConfig (..),+    SBV.boolector,+    SBV.cvc4,+    SBV.yices,+    SBV.dReal,+    SBV.z3,+    SBV.mathSAT,+    SBV.abc,+    SBV.Timing (..),+  )+where++import qualified Data.SBV as SBV+import Grisette.Internal.Backend.Solving+  ( ApproximationConfig (..),+    ExtraConfig (..),+    GrisetteSMTConfig (..),+    approx,+    clearApprox,+    clearTimeout,+    precise,+    withApprox,+    withTimeout,+  )

@@ -1,48 +0,0 @@--- Disable this warning because we are re-exporting things.-{-# OPTIONS_GHC -Wno-missing-import-lists #-}---- |--- Module      :   Grisette.Backend.SBV--- Copyright   :   (c) Sirui Lu 2021-2023--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Backend.SBV-  ( -- * Grisette SBV backend configuration-    ApproximationConfig (..),-    ExtraConfig (..),-    precise,-    approx,-    withTimeout,-    clearTimeout,-    withApprox,-    clearApprox,-    GrisetteSMTConfig (..),--    -- * SBV backend solver configuration-    SBV.SMTConfig (..),-    SBV.boolector,-    SBV.cvc4,-    SBV.yices,-    SBV.dReal,-    SBV.z3,-    SBV.mathSAT,-    SBV.abc,-    SBV.Timing (..),-  )-where--import qualified Data.SBV as SBV-import Grisette.Backend.SBV.Data.SMT.Solving-  ( ApproximationConfig (..),-    ExtraConfig (..),-    GrisetteSMTConfig (..),-    approx,-    clearApprox,-    clearTimeout,-    precise,-    withApprox,-    withTimeout,-  )

@@ -1,1882 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE RoleAnnotations #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE ViewPatterns #-}---- |--- Module      :   Grisette.Backend.SBV.Data.SMT.Lowering--- Copyright   :   (c) Sirui Lu 2021-2023--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Backend.SBV.Data.SMT.Lowering-  ( lowerSinglePrim,-    lowerSinglePrimCached,-    parseModel,-    SymBiMap,-  )-where--import Control.Monad.IO.Class (MonadIO)-import Control.Monad.Reader (MonadTrans (lift), ReaderT)-import Control.Monad.State (StateT)-import Data.Bifunctor (Bifunctor (bimap, first, second))-import Data.Bits-  ( Bits (complement, xor, (.&.), (.|.)),-  )-import Data.Dynamic (Typeable, fromDyn, toDyn)-import Data.Foldable (Foldable (foldl'), asum)-import Data.Kind (Type)-import Data.Maybe (fromMaybe)-import Data.SBV (SIntegral, sRotateLeft, sRotateRight, sShiftLeft, sShiftRight)-import qualified Data.SBV as SBV-import qualified Data.SBV.Internals as SBVI-import qualified Data.SBV.Trans as SBVT-import qualified Data.SBV.Trans.Control as SBVTC-import Data.Type.Equality (type (~~))-import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))-import GHC.Exts (sortWith)-import GHC.Stack (HasCallStack)-import GHC.TypeNats-  ( KnownNat,-    Nat,-    natVal,-    type (+),-    type (-),-    type (<=),-  )-import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving-  ( ApproximationConfig (Approx, NoApprox),-    ExtraConfig (integerApprox),-    GrisetteSMTConfig (GrisetteSMTConfig),-    TermTy,-  )-import Grisette.Backend.SBV.Data.SMT.SymBiMap-  ( SymBiMap,-    addBiMap,-    addBiMapIntermediate,-    emptySymBiMap,-    findStringToSymbol,-    lookupTerm,-    sizeBiMap,-  )-import Grisette.Core.Data.BV (IntN (IntN, unIntN), WordN (WordN))-import Grisette.Core.Data.Class.ModelOps-  ( ModelOps (emptyModel, insertValue),-  )-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-  ( conTerm,-    symTerm,-  )-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm-  ( SomeTerm (SomeTerm),-  )-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-  ( SomeTypedSymbol (SomeTypedSymbol),-    SupportedPrim (withPrim),-    Term-      ( AbsNumTerm,-        AddNumTerm,-        AndBitsTerm,-        AndTerm,-        BVConcatTerm,-        BVExtendTerm,-        BVSelectTerm,-        BinaryTerm,-        ComplementBitsTerm,-        ConTerm,-        DivBoundedIntegralTerm,-        DivIntegralTerm,-        EqvTerm,-        GeneralFunApplyTerm,-        ITETerm,-        LENumTerm,-        LTNumTerm,-        ModBoundedIntegralTerm,-        ModIntegralTerm,-        NotTerm,-        OrBitsTerm,-        OrTerm,-        QuotBoundedIntegralTerm,-        QuotIntegralTerm,-        RemBoundedIntegralTerm,-        RemIntegralTerm,-        RotateLeftTerm,-        RotateRightTerm,-        ShiftLeftTerm,-        ShiftRightTerm,-        SignumNumTerm,-        SymTerm,-        TabularFunApplyTerm,-        TernaryTerm,-        TimesNumTerm,-        ToSignedTerm,-        ToUnsignedTerm,-        UMinusNumTerm,-        UnaryTerm,-        XorBitsTerm-      ),-    TypedSymbol (IndexedSymbol),-    buildGeneralFun,-    someTypedSymbol,-    withSymbolSupported,-    type (-->),-  )-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-  ( introSupportedPrimConstraint,-  )-import Grisette.IR.SymPrim.Data.Prim.Model as PM (Model)-import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool-  ( pevalEqvTerm,-    pevalITETerm,-  )-import Grisette.IR.SymPrim.Data.TabularFun-  ( type (=->) (TabularFun),-  )-import Grisette.Utils.Parameterized-  ( KnownProof (KnownProof),-    LeqProof (LeqProof),-    unsafeAxiom,-    unsafeKnownProof,-    unsafeLeqProof,-    withKnownProof,-  )-import qualified Type.Reflection as R--translateTypeError :: (HasCallStack) => R.TypeRep a -> b-translateTypeError ta =-  error $-    "Don't know how to translate the type " ++ show ta ++ " to SMT"--translateUnaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> c-translateUnaryError op ta tb =-  error $-    "Don't know how to translate the op "-      ++ show op-      ++ " :: "-      ++ show ta-      ++ " -> "-      ++ show tb-      ++ " to SMT"--translateBinaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> d-translateBinaryError op ta tb tc =-  error $-    "Don't know how to translate the op "-      ++ show op-      ++ " :: "-      ++ show ta-      ++ " -> "-      ++ show tb-      ++ " -> "-      ++ show tc-      ++ " to SMT"--translateTernaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> R.TypeRep d -> e-translateTernaryError op ta tb tc td =-  error $-    "Don't know how to translate the op "-      ++ show op-      ++ " :: "-      ++ show ta-      ++ " -> "-      ++ show tb-      ++ " -> "-      ++ show tc-      ++ " -> "-      ++ show td-      ++ " to SMT"--lowerValue ::-  forall integerBitWidth a.-  (SupportedPrim a, Typeable a) =>-  GrisetteSMTConfig integerBitWidth ->-  a ->-  TermTy integerBitWidth a-lowerValue config@ResolvedConfig {} v =-  case R.typeRep @a of-    BoolType -> if v then SBV.sTrue else SBV.sFalse-    IntegerType -> fromInteger v-    SignedBVType _ -> case v of-      IntN x -> fromInteger x-    UnsignedBVType _ -> case v of-      WordN x -> fromInteger x-    TFunType (l :: a1) (r :: a2) ->-      case ((config, l), (config, r)) of-        (ResolvedSimpleType, ResolvedMergeableType) ->-          lowerTFunCon config v-        _ -> translateTypeError (R.typeRep @a)-    _ -> translateTypeError (R.typeRep @a)-lowerValue _ _ = translateTypeError (R.typeRep @a)--lowerTFunCon ::-  forall integerBitWidth a b.-  (SupportedPrim a, SupportedPrim b, SBV.EqSymbolic (TermTy integerBitWidth a), SBV.Mergeable (TermTy integerBitWidth b)) =>-  GrisetteSMTConfig integerBitWidth ->-  (a =-> b) ->-  (TermTy integerBitWidth a -> TermTy integerBitWidth b)-lowerTFunCon config@ResolvedConfig {} (TabularFun l d) = go l d-  where-    go [] d _ = lowerValue config d-    go ((x, r) : xs) d v = SBV.ite (lowerValue config x SBV..== v) (lowerValue config r) (go xs d v)-lowerTFunCon _ TabularFun {} = translateTypeError (R.typeRep @a)--buildUTFun11 ::-  forall integerBitWidth s1 s2 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2))-buildUTFun11 config ta tb term@(SymTerm _ ts) m = case ((config, ta), (config, tb)) of-  (ResolvedSimpleType, ResolvedSimpleType) ->-    let name = "ufunc_" ++ show (sizeBiMap m)-        f = SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2) name-     in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-  _ -> Nothing-buildUTFun11 _ _ _ _ _ = error "Should only be called on SymTerm"--buildUTFun111 ::-  forall integerBitWidth s1 s2 s3 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3))-buildUTFun111 config ta tb tc term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3)-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUTFun111 _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUTFun1111 ::-  forall integerBitWidth s1 s2 s3 s4 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4))-buildUTFun1111 config ta tb tc td term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3 -> TermTy integerBitWidth s4)-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUTFun1111 _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUTFun11111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4, SupportedPrim s5) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5))-buildUTFun11111 config ta tb tc td te term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUTFun11111 _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUTFun111111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 s6 a.-  ( SupportedPrim a,-    SupportedPrim s1,-    SupportedPrim s2,-    SupportedPrim s3,-    SupportedPrim s4,-    SupportedPrim s5,-    SupportedPrim s6-  ) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  R.TypeRep s6 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6))-buildUTFun111111 config ta tb tc td te tf term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUTFun111111 _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUTFun1111111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 a.-  ( SupportedPrim a,-    SupportedPrim s1,-    SupportedPrim s2,-    SupportedPrim s3,-    SupportedPrim s4,-    SupportedPrim s5,-    SupportedPrim s6,-    SupportedPrim s7-  ) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  R.TypeRep s6 ->-  R.TypeRep s7 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7))-buildUTFun1111111 config ta tb tc td te tf tg term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUTFun1111111 _ _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUTFun11111111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 s8 a.-  ( SupportedPrim a,-    SupportedPrim s1,-    SupportedPrim s2,-    SupportedPrim s3,-    SupportedPrim s4,-    SupportedPrim s5,-    SupportedPrim s6,-    SupportedPrim s7,-    SupportedPrim s8-  ) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  R.TypeRep s6 ->-  R.TypeRep s7 ->-  R.TypeRep s8 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7 =-> s8))-buildUTFun11111111 config ta tb tc td te tf tg th term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg), (config, th)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7 =-> s8))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUTFun11111111 _ _ _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUGFun11 ::-  forall integerBitWidth s1 s2 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2))-buildUGFun11 config ta tb term@(SymTerm _ ts) m = case ((config, ta), (config, tb)) of-  (ResolvedSimpleType, ResolvedSimpleType) ->-    let name = "ufunc_" ++ show (sizeBiMap m)-        f = SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2) name-     in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-  _ -> Nothing-buildUGFun11 _ _ _ _ _ = error "Should only be called on SymTerm"--buildUGFun111 ::-  forall integerBitWidth s1 s2 s3 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3))-buildUGFun111 config ta tb tc term@(SymTerm _ ts) m = case ((config, ta), (config, tb), (config, tc)) of-  (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-    let name = "ufunc_" ++ show (sizeBiMap m)-        f =-          SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3)-            name-     in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-  _ -> Nothing-buildUGFun111 _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUGFun1111 ::-  forall integerBitWidth s1 s2 s3 s4 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4))-buildUGFun1111 config ta tb tc td term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3 -> TermTy integerBitWidth s4)-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUGFun1111 _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUGFun11111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4, SupportedPrim s5) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5))-buildUGFun11111 config ta tb tc td te term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUGFun11111 _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUGFun111111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 s6 a.-  ( SupportedPrim a,-    SupportedPrim s1,-    SupportedPrim s2,-    SupportedPrim s3,-    SupportedPrim s4,-    SupportedPrim s5,-    SupportedPrim s6-  ) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  R.TypeRep s6 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6))-buildUGFun111111 config ta tb tc td te tf term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUGFun111111 _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUGFun1111111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 a.-  ( SupportedPrim a,-    SupportedPrim s1,-    SupportedPrim s2,-    SupportedPrim s3,-    SupportedPrim s4,-    SupportedPrim s5,-    SupportedPrim s6,-    SupportedPrim s7-  ) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  R.TypeRep s6 ->-  R.TypeRep s7 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7))-buildUGFun1111111 config ta tb tc td te tf tg term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUGFun1111111 _ _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--buildUGFun11111111 ::-  forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 s8 a.-  ( SupportedPrim a,-    SupportedPrim s1,-    SupportedPrim s2,-    SupportedPrim s3,-    SupportedPrim s4,-    SupportedPrim s5,-    SupportedPrim s6,-    SupportedPrim s7,-    SupportedPrim s8-  ) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  R.TypeRep s3 ->-  R.TypeRep s4 ->-  R.TypeRep s5 ->-  R.TypeRep s6 ->-  R.TypeRep s7 ->-  R.TypeRep s8 ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7 --> s8))-buildUGFun11111111 config ta tb tc td te tf tg th term@(SymTerm _ ts) m =-  case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg), (config, th)) of-    (ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->-      let name = "ufunc_" ++ show (sizeBiMap m)-          f =-            SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7 --> s8))-              name-       in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-    _ -> Nothing-buildUGFun11111111 _ _ _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"--lowerSinglePrimUFun ::-  forall integerBitWidth a.-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SymBiMap ->-  Maybe (SymBiMap, TermTy integerBitWidth a)-lowerSinglePrimUFun config t@(SymTerm _ _) m =-  case R.typeRep @a of-    TFun8Type t1 t2 t3 t4 t5 t6 t7 t8 -> buildUTFun11111111 config t1 t2 t3 t4 t5 t6 t7 t8 t m-    TFun7Type t1 t2 t3 t4 t5 t6 t7 -> buildUTFun1111111 config t1 t2 t3 t4 t5 t6 t7 t m-    TFun6Type t1 t2 t3 t4 t5 t6 -> buildUTFun111111 config t1 t2 t3 t4 t5 t6 t m-    TFun5Type t1 t2 t3 t4 t5 -> buildUTFun11111 config t1 t2 t3 t4 t5 t m-    TFun4Type t1 t2 t3 t4 -> buildUTFun1111 config t1 t2 t3 t4 t m-    TFun3Type t1 t2 t3 -> buildUTFun111 config t1 t2 t3 t m-    TFunType t1 t2 -> buildUTFun11 config t1 t2 t m-    GFun8Type t1 t2 t3 t4 t5 t6 t7 t8 -> buildUGFun11111111 config t1 t2 t3 t4 t5 t6 t7 t8 t m-    GFun7Type t1 t2 t3 t4 t5 t6 t7 -> buildUGFun1111111 config t1 t2 t3 t4 t5 t6 t7 t m-    GFun6Type t1 t2 t3 t4 t5 t6 -> buildUGFun111111 config t1 t2 t3 t4 t5 t6 t m-    GFun5Type t1 t2 t3 t4 t5 -> buildUGFun11111 config t1 t2 t3 t4 t5 t m-    GFun4Type t1 t2 t3 t4 -> buildUGFun1111 config t1 t2 t3 t4 t m-    GFun3Type t1 t2 t3 -> buildUGFun111 config t1 t2 t3 t m-    GFunType t1 t2 -> buildUGFun11 config t1 t2 t m-    _ -> Nothing-lowerSinglePrimUFun _ _ _ = error "Should not call this function"--class (Monad m) => SBVFreshMonad m where-  sbvFresh :: (SBV.SymVal a) => String -> m (SBV.SBV a)--instance (MonadIO m) => SBVFreshMonad (SBVT.SymbolicT m) where-  sbvFresh = SBVT.free--instance (MonadIO m) => SBVFreshMonad (SBVTC.QueryT m) where-  sbvFresh = SBVTC.freshVar--instance (SBVFreshMonad m) => SBVFreshMonad (ReaderT r m) where-  sbvFresh = lift . sbvFresh--instance (SBVFreshMonad m) => SBVFreshMonad (StateT s m) where-  sbvFresh = lift . sbvFresh--lowerUnaryTerm ::-  forall integerBitWidth a a1 x x1 m.-  (Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, HasCallStack, SBVFreshMonad m) =>-  GrisetteSMTConfig integerBitWidth ->-  Term x ->-  Term a ->-  (a1 -> x1) ->-  SymBiMap ->-  m (SymBiMap, x1)-lowerUnaryTerm config orig t1 f m = do-  (m1, l1) <- lowerSinglePrimCached config t1 m-  let g = f l1-  return (addBiMapIntermediate (SomeTerm orig) (toDyn g) m1, g)--lowerBinaryTerm ::-  forall integerBitWidth a b a1 b1 x x1 m.-  (Typeable x1, a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack, SBVFreshMonad m) =>-  GrisetteSMTConfig integerBitWidth ->-  Term x ->-  Term a ->-  Term b ->-  (a1 -> b1 -> x1) ->-  SymBiMap ->-  m (SymBiMap, x1)-lowerBinaryTerm config orig t1 t2 f m = do-  (m1, l1) <- lowerSinglePrimCached config t1 m-  (m2, l2) <- lowerSinglePrimCached config t2 m1-  let g = f l1 l2-  return (addBiMapIntermediate (SomeTerm orig) (toDyn g) m2, g)--lowerSinglePrimCached ::-  forall integerBitWidth a m.-  (HasCallStack, SBVFreshMonad m) =>-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SymBiMap ->-  m (SymBiMap, TermTy integerBitWidth a)-lowerSinglePrimCached config t m =-  introSupportedPrimConstraint t $-    case (config, R.typeRep @a) of-      ResolvedDeepType ->-        case lookupTerm (SomeTerm t) m of-          Just x -> return (m, fromDyn x undefined)-          Nothing -> lowerSinglePrimImpl config t m-      _ -> translateTypeError (R.typeRep @a)--lowerSinglePrim ::-  forall integerBitWidth a m.-  (HasCallStack, SBVFreshMonad m) =>-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  m (SymBiMap, TermTy integerBitWidth a)-lowerSinglePrim config t = lowerSinglePrimCached config t emptySymBiMap--lowerSinglePrimImpl ::-  forall integerBitWidth a m.-  (HasCallStack, SBVFreshMonad m) =>-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SymBiMap ->-  m (SymBiMap, TermTy integerBitWidth a)-lowerSinglePrimImpl config@ResolvedConfig {} (ConTerm _ v) m = return (m, lowerValue config v)-lowerSinglePrimImpl config t@(SymTerm _ ts) m =-  fromMaybe errorMsg $ asum [simple, ufunc]-  where-    errorMsg :: forall x. x-    errorMsg = translateTypeError (R.typeRep @a)-    simple :: Maybe (m (SymBiMap, TermTy integerBitWidth a))-    simple = case (config, R.typeRep @a) of-      ResolvedSimpleType -> Just $ do-        let name = show ts-        (g :: TermTy integerBitWidth a) <- sbvFresh name-        return (addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts) m, g)-      _ -> Nothing-    ufunc :: (Maybe (m (SymBiMap, TermTy integerBitWidth a)))-    ufunc = return <$> lowerSinglePrimUFun config t m-lowerSinglePrimImpl _ (UnaryTerm _ op (_ :: Term x)) _ = errorMsg-  where-    errorMsg :: forall t1. t1-    errorMsg = translateUnaryError (show op) (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl _ (BinaryTerm _ op (_ :: Term x) (_ :: Term y)) _ = errorMsg-  where-    errorMsg :: forall t1. t1-    errorMsg = translateBinaryError (show op) (R.typeRep @x) (R.typeRep @y) (R.typeRep @a)-lowerSinglePrimImpl ResolvedConfig {} (TernaryTerm _ op (_ :: Term x) (_ :: Term y) (_ :: Term z)) _ = errorMsg-  where-    errorMsg :: forall t1. t1-    errorMsg = translateTernaryError (show op) (R.typeRep @x) (R.typeRep @y) (R.typeRep @z) (R.typeRep @a)-lowerSinglePrimImpl config t@(NotTerm _ arg) m = lowerUnaryTerm config t arg SBV.sNot m-lowerSinglePrimImpl config t@(OrTerm _ arg1 arg2) m = lowerBinaryTerm config t arg1 arg2 (SBV..||) m-lowerSinglePrimImpl config t@(AndTerm _ arg1 arg2) m = lowerBinaryTerm config t arg1 arg2 (SBV..&&) m-lowerSinglePrimImpl config t@(EqvTerm _ (arg1 :: Term x) arg2) m =-  case (config, R.typeRep @x) of-    ResolvedSimpleType -> lowerBinaryTerm config t arg1 arg2 (SBV..==) m-    _ -> translateBinaryError "(==)" (R.typeRep @x) (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl config t@(ITETerm _ cond arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedMergeableType -> do-      (m1, l1) <- lowerSinglePrimCached config cond m-      (m2, l2) <- lowerSinglePrimCached config arg1 m1-      (m3, l3) <- lowerSinglePrimCached config arg2 m2-      let g = SBV.ite l1 l2 l3-      return (addBiMapIntermediate (SomeTerm t) (toDyn g) m3, g)-    _ -> translateBinaryError "ite" (R.typeRep @Bool) (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(AddNumTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerBinaryTerm config t arg1 arg2 (+) m-    _ -> translateBinaryError "(+)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(UMinusNumTerm _ arg) m =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerUnaryTerm config t arg negate m-    _ -> translateUnaryError "negate" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(TimesNumTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerBinaryTerm config t arg1 arg2 (*) m-    _ -> translateBinaryError "(*)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(AbsNumTerm _ arg) m =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerUnaryTerm config t arg abs m-    _ -> translateUnaryError "abs" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(SignumNumTerm _ arg) m =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerUnaryTerm config t arg signum m-    _ -> translateUnaryError "signum" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(LTNumTerm _ (arg1 :: Term arg) arg2) m =-  case (config, R.typeRep @arg) of-    ResolvedNumOrdType -> lowerBinaryTerm config t arg1 arg2 (SBV..<) m-    _ -> translateBinaryError "(<)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @Bool)-lowerSinglePrimImpl config t@(LENumTerm _ (arg1 :: Term arg) arg2) m =-  case (config, R.typeRep @arg) of-    ResolvedNumOrdType -> lowerBinaryTerm config t arg1 arg2 (SBV..<=) m-    _ -> translateBinaryError "(<=)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @Bool)-lowerSinglePrimImpl config t@(AndBitsTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm config t arg1 arg2 (.&.) m-    _ -> translateBinaryError "(.&.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(OrBitsTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm config t arg1 arg2 (.|.) m-    _ -> translateBinaryError "(.|.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(XorBitsTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm config t arg1 arg2 xor m-    _ -> translateBinaryError "xor" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(ComplementBitsTerm _ arg) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm config t arg complement m-    _ -> translateUnaryError "complement" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(ShiftLeftTerm _ arg n) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm config t arg n sShiftLeft m-    _ -> translateBinaryError "shiftLeft" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl config t@(ShiftRightTerm _ arg n) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm config t arg n sShiftRight m-    _ -> translateBinaryError "shiftRight" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)--- SBV's rotateLeft and rotateRight are broken for signed values, so we have to--- do this--- https://github.com/LeventErkok/sbv/issues/673-lowerSinglePrimImpl config t@(RotateLeftTerm _ arg n) m =-  case (config, R.typeRep @a) of-    (_, SignedBVType (Proxy :: Proxy n)) ->-      lowerBinaryTerm-        config-        t-        arg-        n-        ( \x y ->-            SBV.sFromIntegral $-              sRotateLeft-                (SBV.sFromIntegral x :: SBV.SWord n)-                (SBV.sFromIntegral y :: SBV.SWord n)-        )-        m-    ResolvedBitsType -> lowerBinaryTerm config t arg n sRotateLeft m-    _ -> translateBinaryError "rotateLeft" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl config t@(RotateRightTerm _ arg n) m =-  case (config, R.typeRep @a) of-    (_, SignedBVType (Proxy :: Proxy n)) ->-      lowerBinaryTerm-        config-        t-        arg-        n-        ( \x y ->-            SBV.sFromIntegral $-              sRotateRight-                (SBV.sFromIntegral x :: SBV.SWord n)-                (SBV.sFromIntegral y :: SBV.SWord n)-        )-        m-    ResolvedBitsType -> lowerBinaryTerm config t arg n sRotateRight m-    _ -> translateBinaryError "rotateRight" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl config t@(ToSignedTerm _ (bv :: Term x)) m =-  case (R.typeRep @a, R.typeRep @x) of-    (SignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->-      case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of-        Just R.HRefl ->-          lowerUnaryTerm config t bv SBV.sFromIntegral m-        _ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)-    _ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl config t@(ToUnsignedTerm _ (bv :: Term x)) m =-  case (R.typeRep @a, R.typeRep @x) of-    (UnsignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->-      case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of-        Just R.HRefl ->-          lowerUnaryTerm config t bv SBV.sFromIntegral m-        _ -> translateUnaryError "s2u" (R.typeRep @x) (R.typeRep @a)-    _ -> translateUnaryError "s2u" (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) m =-  case (R.typeRep @a, R.typeRep @x, R.typeRep @y) of-    (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx), UnsignedBVType (_ :: Proxy ny)) ->-      case (unsafeAxiom @(nx + ny) @na) of-        Refl -> lowerBinaryTerm config t bv1 bv2 (SBV.#) m-    (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx), SignedBVType (_ :: Proxy ny)) ->-      case (unsafeAxiom @(nx + ny) @na) of-        Refl ->-          lowerBinaryTerm-            config-            t-            bv1-            bv2-            ( \(x :: SBV.SInt xn) (y :: SBV.SInt yn) ->-                SBV.sFromIntegral $-                  (SBV.sFromIntegral x :: SBV.SWord xn) SBV.# (SBV.sFromIntegral y :: SBV.SWord yn)-            )-            m-    _ -> translateBinaryError "bvconcat" (R.typeRep @x) (R.typeRep @y) (R.typeRep @a)-lowerSinglePrimImpl config t@(BVSelectTerm _ (ix :: R.TypeRep ix) w (bv :: Term x)) m =-  case (R.typeRep @a, R.typeRep @x) of-    (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy xn)) ->-      withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $-        case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,-               unsafeLeqProof @(na + ix - 1 + 1) @xn,-               unsafeLeqProof @ix @(na + ix - 1)-             ) of-          (Refl, LeqProof, LeqProof) ->-            lowerUnaryTerm config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix)) m-    (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->-      withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $-        case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,-               unsafeLeqProof @(na + ix - 1 + 1) @xn,-               unsafeLeqProof @ix @(na + ix - 1)-             ) of-          (Refl, LeqProof, LeqProof) ->-            lowerUnaryTerm config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix)) m-    _ -> translateTernaryError "bvselect" ix w (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl config t@(BVExtendTerm _ signed (n :: R.TypeRep n) (bv :: Term x)) m =-  case (R.typeRep @a, R.typeRep @x) of-    (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->-      withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @nx))) $-        case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of-          (LeqProof, LeqProof) ->-            bvIsNonZeroFromGEq1 @(na - nx) $-              lowerUnaryTerm config t bv (if signed then SBV.signExtend else SBV.zeroExtend) m-    (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->-      withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @nx))) $-        case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of-          (LeqProof, LeqProof) ->-            bvIsNonZeroFromGEq1 @(na - nx) $-              lowerUnaryTerm-                config-                t-                bv-                ( if signed-                    then SBV.signExtend-                    else \x ->-                      SBV.sFromIntegral-                        (SBV.zeroExtend (SBV.sFromIntegral x :: SBV.SBV (SBV.WordN nx)) :: SBV.SBV (SBV.WordN na))-                )-                m-    _ -> translateTernaryError "bvextend" (R.typeRep @Bool) n (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl config t@(TabularFunApplyTerm _ (f :: Term (b =-> a)) (arg :: Term b)) m =-  case (config, R.typeRep @a) of-    ResolvedDeepType -> do-      (m1, l1) <- lowerSinglePrimCached config f m-      (m2, l2) <- lowerSinglePrimCached config arg m1-      let g = l1 l2-      return (addBiMapIntermediate (SomeTerm t) (toDyn g) m2, g)-    _ -> translateBinaryError "tabularApply" (R.typeRep @(b =-> a)) (R.typeRep @b) (R.typeRep @a)-lowerSinglePrimImpl config t@(GeneralFunApplyTerm _ (f :: Term (b --> a)) (arg :: Term b)) m =-  case (config, R.typeRep @a) of-    ResolvedDeepType -> do-      (m1, l1) <- lowerSinglePrimCached config f m-      (m2, l2) <- lowerSinglePrimCached config arg m1-      let g = l1 l2-      return (addBiMapIntermediate (SomeTerm t) (toDyn g) m2, g)-    _ -> translateBinaryError "generalApply" (R.typeRep @(b --> a)) (R.typeRep @b) (R.typeRep @a)-lowerSinglePrimImpl config t@(DivIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m-    _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(ModIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m-    _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(QuotIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sQuot m-    _ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(RemIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sRem m-    _ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(DivBoundedIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m-    _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(ModBoundedIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m-    _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(QuotBoundedIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sQuot m-    _ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(RemBoundedIntegralTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sRem m-    _ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl _ _ _ = error "Should never happen"--bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r-bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of-  Refl -> r1--#if MIN_VERSION_sbv(10,3,0)-preprocessUIFuncs ::-  [(String, (Bool, SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->-  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]-preprocessUIFuncs =-  traverse-    (\case-      (a, (_, b, Right c)) -> Just (a, (b, c))-      _ -> Nothing)-#elif MIN_VERSION_sbv(10,0,0)-preprocessUIFuncs ::-  [(String, (SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->-  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]-preprocessUIFuncs =-  traverse-    (\case-      (a, (b, Right c)) -> Just (a, (b, c))-      _ -> Nothing)-#else-preprocessUIFuncs ::-  [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->-  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]-preprocessUIFuncs = Just-#endif--parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model-parseModel _ (SBVI.SMTModel _ _ assoc orguifuncs) mp =-  case preprocessUIFuncs orguifuncs of-    Just uifuncs -> foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs-    _ -> error "SBV Failed to parse model"-  where-    goassoc :: (String, SBVI.CV) -> PM.Model -> PM.Model-    goassoc (name, cv) m = case findStringToSymbol name mp of-      Just (SomeTypedSymbol tr s) ->-        insertValue s (resolveSingle tr cv) m-      Nothing -> error "Bad"-    resolveSingle :: R.TypeRep a -> SBVI.CV -> a-    resolveSingle t (SBVI.CV SBVI.KBool (SBVI.CInteger n)) =-      case R.eqTypeRep t (R.typeRep @Bool) of-        Just R.HRefl -> n /= 0-        Nothing -> error "Bad type"-    resolveSingle t (SBVI.CV SBVI.KUnbounded (SBVI.CInteger i)) =-      case R.eqTypeRep t (R.typeRep @Integer) of-        Just R.HRefl -> i-        Nothing -> error "Bad type"-    resolveSingle t (SBVI.CV (SBVI.KBounded _ bitWidth) (SBVI.CInteger i)) =-      case R.eqTypeRep t (R.typeRep @Integer) of-        Just R.HRefl -> i-        _ -> case t of-          R.App a (n :: R.TypeRep w) ->-            case R.eqTypeRep (R.typeRepKind n) (R.typeRep @Nat) of-              Just R.HRefl ->-                case (unsafeKnownProof @w (fromIntegral bitWidth), unsafeLeqProof @1 @w) of-                  (KnownProof, LeqProof) ->-                    case (R.eqTypeRep a (R.typeRep @IntN), R.eqTypeRep a (R.typeRep @WordN)) of-                      (Just R.HRefl, _) ->-                        fromInteger i-                      (_, Just R.HRefl) -> fromInteger i-                      _ -> error "Bad type"-              _ -> error "Bad type"-          _ -> error "Bad type"-    resolveSingle _ _ = error "Unknown cv"--    buildConstFun :: (SupportedPrim a, SupportedPrim r) => R.TypeRep a -> R.TypeRep r -> SBVI.CV -> a =-> r-    buildConstFun _ tr v = case tr of-      TFunType (ta2' :: R.TypeRep a2) (tr2' :: R.TypeRep r2) -> TabularFun [] $ buildConstFun ta2' tr2' v-      _ -> TabularFun [] $ resolveSingle tr v--    goutfuncResolve ::-      forall a r.-      (SupportedPrim a, SupportedPrim r) =>-      R.TypeRep a ->-      R.TypeRep r ->-      ([([SBVI.CV], SBVI.CV)], SBVI.CV) ->-      (a =-> r)-    goutfuncResolve ta1 ta2 (l, s) =-      case ta2 of-        TFunType (ta2' :: R.TypeRep a2) (tr2' :: R.TypeRep r2) ->-          TabularFun-            (second (\r -> goutfuncResolve ta2' tr2' (r, s)) <$> partition ta1 l)-            (buildConstFun ta2' tr2' s)-        _ ->-          TabularFun-            (bimap (resolveSingle ta1 . head) (resolveSingle ta2) <$> l)-            (resolveSingle ta2 s)--    gougfuncResolve ::-      forall a r.-      (SupportedPrim a, SupportedPrim r) =>-      Int ->-      R.TypeRep a ->-      R.TypeRep r ->-      ([([SBVI.CV], SBVI.CV)], SBVI.CV) ->-      (a --> r)-    gougfuncResolve idx ta1 ta2 (l, s) =-      case ta2 of-        GFunType (ta2' :: R.TypeRep a2) (tr2' :: R.TypeRep r2) ->-          let sym = IndexedSymbol "arg" idx-              funs = second (\r -> gougfuncResolve (idx + 1) ta2' tr2' (r, s)) <$> partition ta1 l-              def = gougfuncResolve (idx + 1) ta2' tr2' ([], s)-              body =-                foldl'-                  ( \acc (v, f) ->-                      pevalITETerm-                        (pevalEqvTerm (symTerm sym) (conTerm v))-                        (conTerm f)-                        acc-                  )-                  (conTerm def)-                  funs-           in buildGeneralFun sym body-        _ ->-          let sym = IndexedSymbol "arg" idx-              vs = bimap (resolveSingle ta1 . head) (resolveSingle ta2) <$> l-              def = resolveSingle ta2 s-              body =-                foldl'-                  ( \acc (v, a) ->-                      pevalITETerm-                        (pevalEqvTerm (symTerm sym) (conTerm v))-                        (conTerm a)-                        acc-                  )-                  (conTerm def)-                  vs-           in buildGeneralFun sym body-    partition :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]-    partition t = case (R.eqTypeRep t (R.typeRep @Bool), R.eqTypeRep t (R.typeRep @Integer)) of-      (Just R.HRefl, _) -> partitionWithOrd . resolveFirst t-      (_, Just R.HRefl) -> partitionWithOrd . resolveFirst t-      _ -> case t of-        R.App bv _ -> case (R.eqTypeRep bv (R.typeRep @IntN), R.eqTypeRep bv (R.typeRep @WordN)) of-          (Just R.HRefl, _) -> fmap (first IntN) . partitionWithOrd . fmap (first unIntN) . resolveFirst t-          (_, Just R.HRefl) -> partitionWithOrd . resolveFirst t-          _ -> error "Unknown type"-        _ -> error "Unknown type"--    resolveFirst :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]-    resolveFirst tf = fmap (\case (x : xs, v) -> (resolveSingle tf x, [(xs, v)]); _ -> error "impossible")--    partitionWithOrd :: forall a. (Ord a) => [(a, [([SBVI.CV], SBVI.CV)])] -> [(a, [([SBVI.CV], SBVI.CV)])]-    partitionWithOrd v = go sorted-      where-        sorted = sortWith fst v-        go (x : x1 : xs) =-          if fst x == fst x1-            then go $ (fst x, snd x ++ snd x1) : xs-            else x : go (x1 : xs)-        go x = x--    gouifuncs :: (String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV))) -> PM.Model -> PM.Model-    gouifuncs (name, (SBVI.SBVType _, l)) m = case findStringToSymbol name mp of-      Just (SomeTypedSymbol tr s) -> withSymbolSupported s $ case tr of-        t@(TFunType a r) -> R.withTypeable t $ insertValue s (goutfuncResolve a r l) m-        t@(GFunType a r) -> R.withTypeable t $ insertValue s (gougfuncResolve 0 a r l) m-        _ -> error "Bad"-      Nothing -> error "Bad"---- helpers--data BVTypeContainer bv k where-  BVTypeContainer :: (SBV.BVIsNonZero n, KnownNat n, 1 <= n, k ~ bv n) => Proxy n -> BVTypeContainer bv k--signedBVTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (BVTypeContainer IntN t)-signedBVTypeView t = case t of-  R.App s (n :: R.TypeRep w) ->-    case (R.eqTypeRep s (R.typeRep @IntN), R.eqTypeRep (R.typeRepKind n) (R.typeRep @Nat)) of-      (Just R.HRefl, Just R.HRefl) ->-        Just $ unsafeBVIsNonZero @w $ withPrim (Proxy @t) (BVTypeContainer Proxy)-      _ -> Nothing-  _ -> Nothing-  where-    unsafeBVIsNonZero :: forall w r. ((SBV.BVIsNonZero w) => r) -> r-    unsafeBVIsNonZero r1 = case unsafeAxiom :: w :~: 1 of-      Refl -> r1--pattern SignedBVType ::-  forall t.-  (SupportedPrim t) =>-  forall (n :: Nat).-  (t ~~ IntN n, KnownNat n, 1 <= n, SBV.BVIsNonZero n) =>-  Proxy n ->-  R.TypeRep t-pattern SignedBVType p <- (signedBVTypeView @t -> Just (BVTypeContainer p))--unsignedBVTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (BVTypeContainer WordN t)-unsignedBVTypeView t = case t of-  R.App s (n :: R.TypeRep w) ->-    case (R.eqTypeRep s (R.typeRep @WordN), R.eqTypeRep (R.typeRepKind n) (R.typeRep @Nat)) of-      (Just R.HRefl, Just R.HRefl) ->-        Just $ unsafeBVIsNonZero @w $ withPrim (Proxy @t) (BVTypeContainer Proxy)-      _ -> Nothing-  _ -> Nothing-  where-    unsafeBVIsNonZero :: forall w r. ((SBV.BVIsNonZero w) => r) -> r-    unsafeBVIsNonZero r1 = case unsafeAxiom :: w :~: 1 of-      Refl -> r1--pattern UnsignedBVType ::-  forall t.-  (SupportedPrim t) =>-  forall (n :: Nat).-  (t ~~ WordN n, KnownNat n, 1 <= n, SBV.BVIsNonZero n) =>-  Proxy n ->-  R.TypeRep t-pattern UnsignedBVType p <- (unsignedBVTypeView @t -> Just (BVTypeContainer p))--data TFunTypeContainer :: forall k. k -> Type where-  TFunTypeContainer :: (SupportedPrim a, SupportedPrim b) => R.TypeRep a -> R.TypeRep b -> TFunTypeContainer (a =-> b)--tFunTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (TFunTypeContainer t)-tFunTypeView t = case t of-  R.App (R.App arr (ta2' :: R.TypeRep a2)) (tr2' :: R.TypeRep r2) ->-    case R.eqTypeRep arr (R.typeRep @(=->)) of-      Just R.HRefl -> Just $ withPrim (Proxy @t) $ TFunTypeContainer ta2' tr2'-      Nothing -> Nothing-  _ -> Nothing--pattern TFunType ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type).-  (t ~~ (a =-> b), SupportedPrim a, SupportedPrim b) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep t-pattern TFunType a b <--  (tFunTypeView -> Just (TFunTypeContainer a b))-  where-    TFunType a b = R.App (R.App (R.typeRep @(=->)) a) b--pattern TFun3Type ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type) (c :: Type).-  (t ~~ (a =-> b =-> c), SupportedPrim a, SupportedPrim b, SupportedPrim c) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep t-pattern TFun3Type a b c = TFunType a (TFunType b c)--pattern TFun4Type ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type) (c :: Type) (d :: Type).-  ( t ~~ (a =-> b =-> c =-> d),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep t-pattern TFun4Type a b c d = TFunType a (TFunType b (TFunType c d))--pattern TFun5Type ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type).-  ( t ~~ (a =-> b =-> c =-> d =-> e),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep t-pattern TFun5Type a b c d e =-  TFunType-    a-    ( TFunType-        b-        ( TFunType-            c-            (TFunType d e)-          )-      )--pattern TFun6Type ::-  forall t.-  (SupportedPrim t) =>-  forall-    (a :: Type)-    (b :: Type)-    (c :: Type)-    (d :: Type)-    (e :: Type)-    (f :: Type).-  ( t ~~ (a =-> b =-> c =-> d =-> e =-> f),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e,-    SupportedPrim f-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep f ->-  R.TypeRep t-pattern TFun6Type a b c d e f =-  TFunType-    a-    ( TFunType-        b-        ( TFunType-            c-            ( TFunType-                d-                (TFunType e f)-              )-          )-      )--pattern TFun7Type ::-  forall t.-  (SupportedPrim t) =>-  forall-    (a :: Type)-    (b :: Type)-    (c :: Type)-    (d :: Type)-    (e :: Type)-    (f :: Type)-    (g :: Type).-  ( t ~~ (a =-> b =-> c =-> d =-> e =-> f =-> g),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e,-    SupportedPrim f,-    SupportedPrim g-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep f ->-  R.TypeRep g ->-  R.TypeRep t-pattern TFun7Type a b c d e f g =-  TFunType-    a-    ( TFunType-        b-        ( TFunType-            c-            ( TFunType-                d-                ( TFunType-                    e-                    (TFunType f g)-                  )-              )-          )-      )--pattern TFun8Type ::-  forall t.-  (SupportedPrim t) =>-  forall-    (a :: Type)-    (b :: Type)-    (c :: Type)-    (d :: Type)-    (e :: Type)-    (f :: Type)-    (g :: Type)-    (h :: Type).-  ( t ~~ (a =-> b =-> c =-> d =-> e =-> f =-> g =-> h),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e,-    SupportedPrim f,-    SupportedPrim g,-    SupportedPrim h-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep f ->-  R.TypeRep g ->-  R.TypeRep h ->-  R.TypeRep t-pattern TFun8Type a b c d e f g h =-  TFunType-    a-    ( TFunType-        b-        ( TFunType-            c-            ( TFunType-                d-                ( TFunType-                    e-                    ( TFunType-                        f-                        (TFunType g h)-                      )-                  )-              )-          )-      )--data GFunTypeContainer :: forall k. k -> Type where-  GFunTypeContainer :: (SupportedPrim a, SupportedPrim b) => R.TypeRep a -> R.TypeRep b -> GFunTypeContainer (a --> b)--gFunTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (GFunTypeContainer t)-gFunTypeView t = case t of-  R.App (R.App arr (ta2' :: R.TypeRep a2)) (tr2' :: R.TypeRep r2) ->-    case R.eqTypeRep arr (R.typeRep @(-->)) of-      Just R.HRefl -> Just $ withPrim (Proxy @t) $ GFunTypeContainer ta2' tr2'-      Nothing -> Nothing-  _ -> Nothing--pattern GFunType ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type).-  (t ~~ (a --> b), SupportedPrim a, SupportedPrim b) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep t-pattern GFunType a b <--  (gFunTypeView -> Just (GFunTypeContainer a b))-  where-    GFunType a b = R.App (R.App (R.typeRep @(-->)) a) b--pattern GFun3Type ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type) (c :: Type).-  (t ~~ (a --> b --> c), SupportedPrim a, SupportedPrim b, SupportedPrim c) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep t-pattern GFun3Type a b c = GFunType a (GFunType b c)--pattern GFun4Type ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type) (c :: Type) (d :: Type).-  ( t ~~ (a --> b --> c --> d),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep t-pattern GFun4Type a b c d = GFunType a (GFunType b (GFunType c d))--pattern GFun5Type ::-  forall t.-  (SupportedPrim t) =>-  forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type).-  ( t ~~ (a --> b --> c --> d --> e),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep t-pattern GFun5Type a b c d e =-  GFunType-    a-    ( GFunType-        b-        ( GFunType-            c-            (GFunType d e)-          )-      )--pattern GFun6Type ::-  forall t.-  (SupportedPrim t) =>-  forall-    (a :: Type)-    (b :: Type)-    (c :: Type)-    (d :: Type)-    (e :: Type)-    (f :: Type).-  ( t ~~ (a --> b --> c --> d --> e --> f),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e,-    SupportedPrim f-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep f ->-  R.TypeRep t-pattern GFun6Type a b c d e f =-  GFunType-    a-    ( GFunType-        b-        ( GFunType-            c-            ( GFunType-                d-                (GFunType e f)-              )-          )-      )--pattern GFun7Type ::-  forall t.-  (SupportedPrim t) =>-  forall-    (a :: Type)-    (b :: Type)-    (c :: Type)-    (d :: Type)-    (e :: Type)-    (f :: Type)-    (g :: Type).-  ( t ~~ (a --> b --> c --> d --> e --> f --> g),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e,-    SupportedPrim f,-    SupportedPrim g-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep f ->-  R.TypeRep g ->-  R.TypeRep t-pattern GFun7Type a b c d e f g =-  GFunType-    a-    ( GFunType-        b-        ( GFunType-            c-            ( GFunType-                d-                ( GFunType-                    e-                    (GFunType f g)-                  )-              )-          )-      )--pattern GFun8Type ::-  forall t.-  (SupportedPrim t) =>-  forall-    (a :: Type)-    (b :: Type)-    (c :: Type)-    (d :: Type)-    (e :: Type)-    (f :: Type)-    (g :: Type)-    (h :: Type).-  ( t ~~ (a --> b --> c --> d --> e --> f --> g --> h),-    SupportedPrim a,-    SupportedPrim b,-    SupportedPrim c,-    SupportedPrim d,-    SupportedPrim e,-    SupportedPrim f,-    SupportedPrim g,-    SupportedPrim h-  ) =>-  R.TypeRep a ->-  R.TypeRep b ->-  R.TypeRep c ->-  R.TypeRep d ->-  R.TypeRep e ->-  R.TypeRep f ->-  R.TypeRep g ->-  R.TypeRep h ->-  R.TypeRep t-pattern GFun8Type a b c d e f g h =-  GFunType-    a-    ( GFunType-        b-        ( GFunType-            c-            ( GFunType-                d-                ( GFunType-                    e-                    ( GFunType-                        f-                        (GFunType g h)-                      )-                  )-              )-          )-      )--pattern BoolType ::-  forall t.-  () =>-  (t ~~ Bool) =>-  R.TypeRep t-pattern BoolType <- (R.eqTypeRep (R.typeRep @Bool) -> Just R.HRefl)--pattern IntegerType ::-  forall t.-  () =>-  (t ~~ Integer) =>-  R.TypeRep t-pattern IntegerType <- (R.eqTypeRep (R.typeRep @Integer) -> Just R.HRefl)--type ConfigConstraint integerBitWidth s =-  ( SBV.SBV s ~ TermTy integerBitWidth Integer,-    SBV.SymVal s,-    SBV.HasKind s,-    Typeable s,-    Num (SBV.SBV s),-    Num s,-    SBV.OrdSymbolic (SBV.SBV s),-    Ord s,-    SBV.SDivisible (SBV.SBV s),-    SBV.OrdSymbolic (SBV.SBV s),-    SBV.Mergeable (SBV.SBV s)-  )--data DictConfig integerBitWidth where-  DictConfig ::-    forall s integerBitWidth.-    (ConfigConstraint integerBitWidth s) =>-    SBV.SMTConfig ->-    DictConfig integerBitWidth--resolveConfigView ::-  forall integerBitWidth.-  GrisetteSMTConfig integerBitWidth ->-  DictConfig integerBitWidth-resolveConfigView config = case config of-  GrisetteSMTConfig c extra ->-    case integerApprox extra of-      NoApprox -> DictConfig c-      Approx _ -> DictConfig c--pattern ResolvedConfig ::-  forall integerBitWidth.-  () =>-  forall s.-  (ConfigConstraint integerBitWidth s) =>-  SBV.SMTConfig ->-  GrisetteSMTConfig integerBitWidth-pattern ResolvedConfig c <- (resolveConfigView -> DictConfig c)--type MergeableTypeConstraint integerBitWidth s =-  ( Typeable (TermTy integerBitWidth s),-    SBV.Mergeable (TermTy integerBitWidth s)-  )---- has to declare this because GHC does not support impredicative polymorphism-data DictMergeableType integerBitWidth s where-  DictMergeableType ::-    forall integerBitWidth s.-    (MergeableTypeConstraint integerBitWidth s) =>-    DictMergeableType integerBitWidth s--resolveMergeableTypeView :: TypeResolver DictMergeableType-resolveMergeableTypeView (config@ResolvedConfig {}, s) = case s of-  BoolType -> Just DictMergeableType-  IntegerType -> Just DictMergeableType-  SignedBVType _ -> Just DictMergeableType-  UnsignedBVType _ -> Just DictMergeableType-  TFunType l r ->-    case (resolveSimpleTypeView (config, l), resolveMergeableTypeView (config, r)) of-      (Just DictSimpleType, Just DictMergeableType) -> Just DictMergeableType-      _ -> Nothing-  GFunType l r ->-    case (resolveSimpleTypeView (config, l), resolveMergeableTypeView (config, r)) of-      (Just DictSimpleType, Just DictMergeableType) -> Just DictMergeableType-      _ -> Nothing-  _ -> Nothing-resolveMergeableTypeView _ = error "Should never happen, make compiler happy"--pattern ResolvedMergeableType ::-  forall integerBitWidth s.-  (SupportedPrim s) =>-  (MergeableTypeConstraint integerBitWidth s) =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)-pattern ResolvedMergeableType <- (resolveMergeableTypeView -> Just DictMergeableType)--type SimpleTypeConstraint integerBitWidth s s' =-  ( SBV.SBV s' ~ TermTy integerBitWidth s,-    SBV.SymVal s',-    SBV.HasKind s',-    Typeable s',-    SBV.OrdSymbolic (SBV.SBV s'),-    SBV.Mergeable (SBV.SBV s')-  )--type TypeResolver dictType =-  forall integerBitWidth s.-  (SupportedPrim s) =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s) ->-  Maybe (dictType integerBitWidth s)---- has to declare this because GHC does not support impredicative polymorphism-data DictSimpleType integerBitWidth s where-  DictSimpleType ::-    forall integerBitWidth s s'.-    (SimpleTypeConstraint integerBitWidth s s') =>-    DictSimpleType integerBitWidth s--resolveSimpleTypeView :: TypeResolver DictSimpleType-resolveSimpleTypeView (ResolvedConfig {}, s) = case s of-  BoolType -> Just DictSimpleType-  IntegerType -> Just DictSimpleType-  SignedBVType _ -> Just DictSimpleType-  UnsignedBVType _ -> Just DictSimpleType-  _ -> Nothing-resolveSimpleTypeView _ = error "Should never happen, make compiler happy"--pattern ResolvedSimpleType ::-  forall integerBitWidth s.-  (SupportedPrim s) =>-  forall s'.-  (SimpleTypeConstraint integerBitWidth s s') =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)-pattern ResolvedSimpleType <- (resolveSimpleTypeView -> Just DictSimpleType)--type DeepTypeConstraint integerBitWidth s s' =-  ( s' ~ TermTy integerBitWidth s,-    Typeable s',-    SBV.Mergeable s'-  )--data DictDeepType integerBitWidth s where-  DictDeepType ::-    forall integerBitWidth s s'.-    (DeepTypeConstraint integerBitWidth s s') =>-    DictDeepType integerBitWidth s--resolveDeepTypeView :: TypeResolver DictDeepType-resolveDeepTypeView r = case r of-  ResolvedSimpleType -> Just DictDeepType-  (config, TFunType (ta :: R.TypeRep a) (tb :: R.TypeRep b)) ->-    case (resolveDeepTypeView (config, ta), resolveDeepTypeView (config, tb)) of-      (Just DictDeepType, Just DictDeepType) -> Just DictDeepType-      _ -> Nothing-  (config, GFunType (ta :: R.TypeRep a) (tb :: R.TypeRep b)) ->-    case (resolveDeepTypeView (config, ta), resolveDeepTypeView (config, tb)) of-      (Just DictDeepType, Just DictDeepType) -> Just DictDeepType-      _ -> Nothing-  _ -> Nothing--pattern ResolvedDeepType ::-  forall integerBitWidth s.-  (SupportedPrim s) =>-  forall s'.-  (DeepTypeConstraint integerBitWidth s s') =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)-pattern ResolvedDeepType <- (resolveDeepTypeView -> Just DictDeepType)--type NumTypeConstraint integerBitWidth s s' =-  ( SimpleTypeConstraint integerBitWidth s s',-    Num (SBV.SBV s'),-    Num s',-    Num s-  )--data DictNumType integerBitWidth s where-  DictNumType ::-    forall integerBitWidth s s'.-    (NumTypeConstraint integerBitWidth s s') =>-    DictNumType integerBitWidth s--resolveNumTypeView :: TypeResolver DictNumType-resolveNumTypeView (ResolvedConfig {}, s) = case s of-  IntegerType -> Just DictNumType-  SignedBVType _ -> Just DictNumType-  UnsignedBVType _ -> Just DictNumType-  _ -> Nothing-resolveNumTypeView _ = error "Should never happen, make compiler happy"--pattern ResolvedNumType ::-  forall integerBitWidth s.-  (SupportedPrim s) =>-  forall s'.-  (NumTypeConstraint integerBitWidth s s') =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)-pattern ResolvedNumType <- (resolveNumTypeView -> Just DictNumType)--type SDivisibleTypeConstraint integerBitWidth s s' =-  ( SimpleTypeConstraint integerBitWidth s s',-    SBV.SDivisible (SBV.SBV s'),-    Integral s-  )--data DictSDivisibleType integerBitWidth s where-  DictSDivisibleType ::-    forall integerBitWidth s s'.-    (SDivisibleTypeConstraint integerBitWidth s s') =>-    DictSDivisibleType integerBitWidth s--resolveSDivisibleTypeView :: TypeResolver DictSDivisibleType-resolveSDivisibleTypeView (ResolvedConfig {}, s) = case s of-  IntegerType -> Just DictSDivisibleType-  SignedBVType _ -> Just DictSDivisibleType-  UnsignedBVType _ -> Just DictSDivisibleType-  _ -> Nothing-resolveSDivisibleTypeView _ = error "Should never happen, make compiler happy"--pattern ResolvedSDivisibleType ::-  forall integerBitWidth s.-  (SupportedPrim s) =>-  forall s'.-  (SDivisibleTypeConstraint integerBitWidth s s') =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)-pattern ResolvedSDivisibleType <- (resolveSDivisibleTypeView -> Just DictSDivisibleType)--type NumOrdTypeConstraint integerBitWidth s s' =-  ( NumTypeConstraint integerBitWidth s s',-    SBV.OrdSymbolic (SBV.SBV s'),-    Ord s',-    Ord s-  )--data DictNumOrdType integerBitWidth s where-  DictNumOrdType ::-    forall integerBitWidth s s'.-    (NumOrdTypeConstraint integerBitWidth s s') =>-    DictNumOrdType integerBitWidth s--resolveNumOrdTypeView :: TypeResolver DictNumOrdType-resolveNumOrdTypeView (ResolvedConfig {}, s) = case s of-  IntegerType -> Just DictNumOrdType-  SignedBVType _ -> Just DictNumOrdType-  UnsignedBVType _ -> Just DictNumOrdType-  _ -> Nothing-resolveNumOrdTypeView _ = error "Should never happen, make compiler happy"--pattern ResolvedNumOrdType ::-  forall integerBitWidth s.-  (SupportedPrim s) =>-  forall s'.-  (NumOrdTypeConstraint integerBitWidth s s') =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)-pattern ResolvedNumOrdType <- (resolveNumOrdTypeView -> Just DictNumOrdType)--type BitsTypeConstraint integerBitWidth s s' =-  ( SimpleTypeConstraint integerBitWidth s s',-    Bits (SBV.SBV s'),-    Bits s',-    Bits s,-    SIntegral s',-    Integral s-  )--data DictBitsType integerBitWidth s where-  DictBitsType ::-    forall integerBitWidth s s'.-    (BitsTypeConstraint integerBitWidth s s') =>-    DictBitsType integerBitWidth s--resolveBitsTypeView :: TypeResolver DictBitsType-resolveBitsTypeView (ResolvedConfig {}, s) = case s of-  SignedBVType _ -> Just DictBitsType-  UnsignedBVType _ -> Just DictBitsType-  _ -> Nothing-resolveBitsTypeView _ = error "Should never happen, make compiler happy"--pattern ResolvedBitsType ::-  forall integerBitWidth s.-  (SupportedPrim s) =>-  forall s'.-  (BitsTypeConstraint integerBitWidth s s') =>-  (GrisetteSMTConfig integerBitWidth, R.TypeRep s)-pattern ResolvedBitsType <- (resolveBitsTypeView -> Just DictBitsType)