grisette 0.1.0.0 → 0.2.0.0

raw patch · 71 files changed

+8893/−4247 lines, 71 filesdep +parallelPVP ok

version bump matches the API change (PVP)

Dependencies added: parallel

API changes (from Hackage documentation)

Files

• CHANGELOG.md +23/−0
• LICENSE +35/−0
• README.md +3/−0
• grisette.cabal +15/−7
• src/Grisette.hs +4/−0
• src/Grisette/Backend/SBV.hs +9/−1
• src/Grisette/Backend/SBV/Data/SMT/Lowering.hs +1652/−1156
• src/Grisette/Backend/SBV/Data/SMT/Solving.hs +203/−78
• src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot +14/−8
• src/Grisette/Core.hs +34/−28
• src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs +123/−0
• src/Grisette/Core/Control/Monad/Union.hs +1/−1
• src/Grisette/Core/Control/Monad/UnionM.hs +95/−48
• src/Grisette/Core/Control/Monad/UnionM.hs-boot +0/−2
• src/Grisette/Core/Data/BV.hs +691/−0
• src/Grisette/Core/Data/Class/BitVector.hs +263/−55
• src/Grisette/Core/Data/Class/Bool.hs +49/−8
• src/Grisette/Core/Data/Class/Bool.hs-boot +5/−0
• src/Grisette/Core/Data/Class/CEGISSolver.hs +14/−14
• src/Grisette/Core/Data/Class/Error.hs +12/−0
• src/Grisette/Core/Data/Class/Evaluate.hs +12/−0
• src/Grisette/Core/Data/Class/ExtractSymbolics.hs +13/−1
• src/Grisette/Core/Data/Class/GenSym.hs +173/−11
• src/Grisette/Core/Data/Class/Integer.hs +0/−72
• src/Grisette/Core/Data/Class/Mergeable.hs +75/−3
• src/Grisette/Core/Data/Class/ModelOps.hs +7/−1
• src/Grisette/Core/Data/Class/SOrd.hs +16/−0
• src/Grisette/Core/Data/Class/SafeArith.hs +428/−0
• src/Grisette/Core/Data/Class/SimpleMergeable.hs +34/−2
• src/Grisette/Core/Data/Class/Solver.hs +7/−7
• src/Grisette/Core/Data/Class/Substitute.hs +18/−3
• src/Grisette/Core/Data/Class/ToCon.hs +12/−0
• src/Grisette/Core/Data/Class/ToSym.hs +12/−0
• src/Grisette/Core/Data/Union.hs +5/−1
• src/Grisette/IR/SymPrim.hs +17/−10
• src/Grisette/IR/SymPrim/Data/BV.hs +0/−330
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs +89/−51
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot +65/−44
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs +184/−66
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot +82/−39
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs +9/−3
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs +64/−45
• src/Grisette/IR/SymPrim/Data/Prim/Model.hs +133/−9
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs +88/−75
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs +3/−0
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integer.hs +0/−36
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs +88/−0
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs +1/−0
• src/Grisette/IR/SymPrim/Data/SymPrim.hs +1593/−631
• src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot +106/−13
• src/Grisette/Internal/IR/SymPrim.hs +6/−5
• src/Grisette/Lib/Data/List.hs +1/−1
• src/Grisette/Qualified/ParallelUnionDo.hs +19/−0
• src/Grisette/Utils.hs +50/−0
• src/Grisette/Utils/Parameterized.hs +234/−0
• test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs +70/−32
• test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs +42/−11
• test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs +42/−171
• test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs +166/−152
• test/Grisette/Core/Control/Monad/UnionMTests.hs +20/−0
• test/Grisette/Core/Data/BVTests.hs +430/−0
• test/Grisette/IR/SymPrim/Data/BVTests.hs +0/−419
• test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs +1/−1
• test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs +1/−1
• test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs +1/−1
• test/Grisette/IR/SymPrim/Data/Prim/IntegerTests.hs +0/−48
• test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs +170/−0
• test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs +1/−1
• test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs +1/−1
• test/Grisette/IR/SymPrim/Data/SymPrimTests.hs +1045/−539
• test/Main.hs +14/−5

@@ -1,4 +1,27 @@ # Changes +## Version 0.2.0.0++### Feature+- 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))+- 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))+- New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56))+++### Bugfix+- Dropped merging cache for `UnionM`. This fixed some segmentation fault errors. ([#43](https://github.com/lsrcz/grisette/pull/43))+- 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))+- 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))+- Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59))+- Fix CEGIS crash when subsequent solver calls introduces new symbolic constant. ([#60](https://github.com/lsrcz/grisette/pull/60))+++ ## Version 0.1.0.0 Initial release.

@@ -28,3 +28,38 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.++-------------------------------------------------------------------------------++This repository contains code from the parameterized-utils package:++Copyright (c) 2013-2022 Galois Inc.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++  * Redistributions of source code must retain the above copyright+    notice, this list of conditions and the following disclaimer.++  * Redistributions in binary form must reproduce the above copyright+    notice, this list of conditions and the following disclaimer in+    the documentation and/or other materials provided with the+    distribution.++  * Neither the name of Galois, Inc. nor the names of its contributors+    may be used to endorse or promote products derived from this+    software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -6,6 +6,9 @@ programs into constraints, Grisette can help the development of program reasoning tools, including verification and synthesis. +For a detailed description of the system, please refer to our POPL'23 paper+[Grisette: Symbolic Compilation as a Functional Programming Library](https://lsrcz.github.io/files/POPL23.pdf).+ ## Features  - **Multi-path** symbolic evaluation with efficient (customizable) state merging.

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.0.+-- This file has been generated from package.yaml by hpack version 0.35.1. -- -- see: https://github.com/sol/hpack  name:           grisette-version:        0.1.0.0+version:        0.2.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@@ -48,8 +48,10 @@       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.Bool       Grisette.Core.Data.Class.CEGISSolver@@ -58,9 +60,9 @@       Grisette.Core.Data.Class.ExtractSymbolics       Grisette.Core.Data.Class.Function       Grisette.Core.Data.Class.GenSym-      Grisette.Core.Data.Class.Integer       Grisette.Core.Data.Class.Mergeable       Grisette.Core.Data.Class.ModelOps+      Grisette.Core.Data.Class.SafeArith       Grisette.Core.Data.Class.SimpleMergeable       Grisette.Core.Data.Class.Solvable       Grisette.Core.Data.Class.Solver@@ -77,7 +79,6 @@       Grisette.Internal.Core       Grisette.Internal.IR.SymPrim       Grisette.IR.SymPrim-      Grisette.IR.SymPrim.Data.BV       Grisette.IR.SymPrim.Data.IntBitwidth       Grisette.IR.SymPrim.Data.Prim.Helpers       Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches@@ -92,7 +93,7 @@       Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool       Grisette.IR.SymPrim.Data.Prim.PartialEval.BV       Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun-      Grisette.IR.SymPrim.Data.Prim.PartialEval.Integer+      Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral       Grisette.IR.SymPrim.Data.Prim.PartialEval.Num       Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval       Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun@@ -109,6 +110,9 @@       Grisette.Lib.Data.List       Grisette.Lib.Data.Traversable       Grisette.Lib.Mtl+      Grisette.Qualified.ParallelUnionDo+      Grisette.Utils+      Grisette.Utils.Parameterized   other-modules:       Paths_grisette   hs-source-dirs:@@ -126,6 +130,7 @@     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.3     , once >=0.2 && <0.5+    , parallel     , sbv >=8.11 && <9.1     , template-haskell >=2.16 && <2.20     , th-compat >=0.1.2 && <0.2@@ -161,6 +166,7 @@     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.3     , once >=0.2 && <0.5+    , parallel     , sbv >=8.11 && <9.1     , template-haskell >=2.16 && <2.20     , th-compat >=0.1.2 && <0.2@@ -181,11 +187,12 @@       Grisette.Backend.SBV.Data.SMT.LoweringTests       Grisette.Backend.SBV.Data.SMT.TermRewritingGen       Grisette.Backend.SBV.Data.SMT.TermRewritingTests-      Grisette.IR.SymPrim.Data.BVTests+      Grisette.Core.Control.Monad.UnionMTests+      Grisette.Core.Data.BVTests       Grisette.IR.SymPrim.Data.Prim.BitsTests       Grisette.IR.SymPrim.Data.Prim.BoolTests       Grisette.IR.SymPrim.Data.Prim.BVTests-      Grisette.IR.SymPrim.Data.Prim.IntegerTests+      Grisette.IR.SymPrim.Data.Prim.IntegralTests       Grisette.IR.SymPrim.Data.Prim.ModelTests       Grisette.IR.SymPrim.Data.Prim.NumTests       Grisette.IR.SymPrim.Data.Prim.TabularFunTests@@ -208,6 +215,7 @@     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.3     , once >=0.2 && <0.5+    , parallel     , sbv >=8.11 && <9.1     , tasty >=1.1.0.3 && <1.5     , tasty-hunit ==0.10.*

@@ -19,6 +19,9 @@      -- * Solver backend     module Grisette.Backend.SBV,++    -- * Utils+    module Grisette.Utils,   ) where @@ -27,3 +30,4 @@ import Grisette.IR.SymPrim import Grisette.Lib.Base import Grisette.Lib.Mtl+import Grisette.Utils

@@ -8,8 +8,16 @@ -- Portability :   GHC only module Grisette.Backend.SBV   ( -- * Grisette SBV backend configuration+    ApproximationConfig (..),+    ExtraConfig (..),+    precise,+    approx,+    withTimeout,+    clearTimeout,+    withApprox,+    clearApprox,     GrisetteSMTConfig (..),-    sbvConfig,+    SolvingFailure (..),      -- * SBV backend solver configuration     SBV.SMTConfig (..),

@@ -2,1162 +2,1658 @@ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# 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,-    lowerSinglePrim',-    parseModel,-    SymBiMap,-  )-where--import Control.Monad.State.Strict-import Data.Bifunctor-import Data.Bits-import Data.Dynamic-import Data.Foldable-import Data.Kind-import Data.Maybe-import qualified Data.SBV as SBV-import qualified Data.SBV.Internals as SBVI-import Data.Type.Equality (type (~~))-import Data.Typeable-import GHC.Exts (sortWith)-import GHC.Natural-import GHC.Stack-import GHC.TypeNats-import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving-import Grisette.Backend.SBV.Data.SMT.SymBiMap-import Grisette.Core.Data.Class.ModelOps-import Grisette.IR.SymPrim.Data.BV-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-import Grisette.IR.SymPrim.Data.Prim.Model as PM-import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool-import Grisette.IR.SymPrim.Data.TabularFun-import qualified Type.Reflection as R-import Unsafe.Coerce--newtype NatRepr (n :: Nat) = NatRepr Natural--withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r-withKnownNat (NatRepr nVal) v =-  case someNatVal nVal of-    SomeNat (Proxy :: Proxy n') ->-      case unsafeAxiom :: n :~: n' of-        Refl -> v--data LeqProof (m :: Nat) (n :: Nat) where-  LeqProof :: m <= n => LeqProof m n---- | Assert a proof of equality between two types.--- This is unsafe if used improperly, so use this with caution!-unsafeAxiom :: forall a b. a :~: b-unsafeAxiom = unsafeCoerce (Refl @a)-{-# NOINLINE unsafeAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]--unsafeLeqProof :: forall m n. LeqProof m n-unsafeLeqProof = unsafeCoerce (LeqProof @0 @0)-{-# NOINLINE unsafeLeqProof #-} -- Note [Mark unsafe axioms as NOINLINE]--cachedResult ::-  forall integerBitWidth a.-  (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>-  Term a ->-  State SymBiMap (Maybe (TermTy integerBitWidth a))-cachedResult t = gets $ \m -> do-  d <- lookupTerm (SomeTerm t) m-  Just $ fromDyn d undefined--addResult ::-  forall integerBitWidth a.-  (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>-  Term a ->-  TermTy integerBitWidth a ->-  State SymBiMap ()-addResult tm sbvtm = modify $ addBiMapIntermediate (SomeTerm tm) (toDyn sbvtm)--lowerSinglePrim' ::-  forall integerBitWidth a.-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SymBiMap ->-  (TermTy integerBitWidth a, SymBiMap)-lowerSinglePrim' config t = runState (lowerSinglePrimCached' config t)--lowerSinglePrimCached' ::-  forall integerBitWidth a.-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  State SymBiMap (TermTy integerBitWidth a)-lowerSinglePrimCached' config t = introSupportedPrimConstraint t $-  case (config, R.typeRep @a) of-    ResolvedDeepType -> do-      r <- cachedResult @integerBitWidth t-      case r of-        Just v -> return v-        _ -> lowerSinglePrimImpl' config t-    _ -> translateTypeError (R.typeRep @a)--lowerUnaryTerm' ::-  forall integerBitWidth a a1 x x1.-  (Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, x1 ~ TermTy integerBitWidth x) =>-  GrisetteSMTConfig integerBitWidth ->-  Term x ->-  Term a ->-  (a1 -> x1) ->-  State SymBiMap (TermTy integerBitWidth x)-lowerUnaryTerm' config orig t1 f = do-  l1 <- lowerSinglePrimCached' config t1-  let g = f l1-  addResult @integerBitWidth orig g-  return g--lowerBinaryTerm' ::-  forall integerBitWidth a b a1 b1 x.-  ( Typeable (TermTy integerBitWidth x),-    a1 ~ TermTy integerBitWidth a,-    b1 ~ TermTy integerBitWidth b,-    SupportedPrim x-  ) =>-  GrisetteSMTConfig integerBitWidth ->-  Term x ->-  Term a ->-  Term b ->-  (a1 -> b1 -> TermTy integerBitWidth x) ->-  State SymBiMap (TermTy integerBitWidth x)-lowerBinaryTerm' config orig t1 t2 f = do-  l1 <- lowerSinglePrimCached' config t1-  l2 <- lowerSinglePrimCached' config t2-  let g = f l1 l2-  addResult @integerBitWidth orig g-  return g--lowerSinglePrimImpl' ::-  forall integerBitWidth a.-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  State SymBiMap (TermTy integerBitWidth a)-lowerSinglePrimImpl' ResolvedConfig {} (ConTerm _ v) =-  case R.typeRep @a of-    BoolType -> return $ if v then SBV.sTrue else SBV.sFalse-    IntegerType -> return $ fromInteger v-    SignedBVType _ -> case v of-      IntN x -> return $ fromInteger x-    UnsignedBVType _ -> case v of-      WordN x -> return $ fromInteger x-    _ -> translateTypeError (R.typeRep @a)-lowerSinglePrimImpl' _ t@SymTerm {} =-  error $-    "The symbolic term should have already been lowered "-      ++ show t-      ++ " to SMT with collectedPrims.\n"-      ++ "We don't support adding new symbolics after collectedPrims with SBV backend"-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) = lowerUnaryTerm' config t arg SBV.sNot-lowerSinglePrimImpl' config t@(OrTerm _ arg1 arg2) = lowerBinaryTerm' config t arg1 arg2 (SBV..||)-lowerSinglePrimImpl' config t@(AndTerm _ arg1 arg2) = lowerBinaryTerm' config t arg1 arg2 (SBV..&&)-lowerSinglePrimImpl' config t@(EqvTerm _ (arg1 :: Term x) arg2) =-  case (config, R.typeRep @x) of-    ResolvedSimpleType -> lowerBinaryTerm' config t arg1 arg2 (SBV..==)-    _ -> translateBinaryError "(==)" (R.typeRep @x) (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl' config t@(ITETerm _ cond arg1 arg2) =-  case (config, R.typeRep @a) of-    ResolvedSimpleType -> do-      l1 <- lowerSinglePrimCached' config cond-      l2 <- lowerSinglePrimCached' config arg1-      l3 <- lowerSinglePrimCached' config arg2-      let g = SBV.ite l1 l2 l3-      addResult @integerBitWidth t g-      return g-    _ -> translateTernaryError "ite" (R.typeRep @Bool) (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(AddNumTerm _ arg1 arg2) =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerBinaryTerm' config t arg1 arg2 (+)-    _ -> translateBinaryError "(+)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(UMinusNumTerm _ arg) =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerUnaryTerm' config t arg negate-    _ -> translateUnaryError "negate" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(TimesNumTerm _ arg1 arg2) =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerBinaryTerm' config t arg1 arg2 (*)-    _ -> translateBinaryError "(*)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(AbsNumTerm _ arg) =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerUnaryTerm' config t arg abs-    _ -> translateUnaryError "abs" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(SignumNumTerm _ arg) =-  case (config, R.typeRep @a) of-    ResolvedNumType -> lowerUnaryTerm' config t arg signum-    _ -> translateUnaryError "signum" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(LTNumTerm _ (arg1 :: Term arg) arg2) =-  case (config, R.typeRep @arg) of-    ResolvedNumOrdType -> lowerBinaryTerm' config t arg1 arg2 (SBV..<)-    _ -> translateBinaryError "(<)" (R.typeRep @arg) (R.typeRep @arg) (R.typeRep @Bool)-lowerSinglePrimImpl' config t@(LENumTerm _ (arg1 :: Term arg) arg2) =-  case (config, R.typeRep @arg) of-    ResolvedNumOrdType -> lowerBinaryTerm' config t arg1 arg2 (SBV..<=)-    _ -> translateBinaryError "(<=)" (R.typeRep @arg) (R.typeRep @arg) (R.typeRep @Bool)-lowerSinglePrimImpl' config t@(AndBitsTerm _ arg1 arg2) =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm' config t arg1 arg2 (.&.)-    _ -> translateBinaryError "(.&.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(OrBitsTerm _ arg1 arg2) =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm' config t arg1 arg2 (.|.)-    _ -> translateBinaryError "(.|.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(XorBitsTerm _ arg1 arg2) =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerBinaryTerm' config t arg1 arg2 xor-    _ -> translateBinaryError "xor" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(ComplementBitsTerm _ arg) =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm' config t arg complement-    _ -> translateUnaryError "complement" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(ShiftBitsTerm _ arg n) =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm' config t arg (`shift` n)-    _ -> translateBinaryError "shift" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl' config t@(RotateBitsTerm _ arg n) =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm' config t arg (`rotate` n)-    _ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl' config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) =-  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.#)-    (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)-            )-    _ -> translateBinaryError "bvconcat" (R.typeRep @x) (R.typeRep @y) (R.typeRep @a)-lowerSinglePrimImpl' config t@(BVSelectTerm _ (ix :: R.TypeRep ix) w (bv :: Term x)) =-  case (R.typeRep @a, R.typeRep @x) of-    (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy xn)) ->-      withKnownNat n1 $-        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))-      where-        n1 :: NatRepr (na + ix - 1)-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)-    (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->-      withKnownNat n1 $-        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))-      where-        n1 :: NatRepr (na + ix - 1)-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)-    _ -> translateTernaryError "bvselect" ix w (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl' config t@(BVExtendTerm _ signed (n :: R.TypeRep n) (bv :: Term x)) =-  case (R.typeRep @a, R.typeRep @x) of-    (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - 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)-    (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - 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))-                )-    _ -> translateTernaryError "bvextend" (R.typeRep @Bool) n (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl' config t@(TabularFunApplyTerm _ (f :: Term (b =-> a)) (arg :: Term b)) =-  case (config, R.typeRep @a) of-    ResolvedDeepType -> do-      l1 <- lowerSinglePrimCached' config f-      l2 <- lowerSinglePrimCached' config arg-      let g = l1 l2-      addResult @integerBitWidth t g-      return g-    _ -> translateBinaryError "tabularApply" (R.typeRep @(b =-> a)) (R.typeRep @b) (R.typeRep @a)-lowerSinglePrimImpl' config t@(GeneralFunApplyTerm _ (f :: Term (b --> a)) (arg :: Term b)) =-  case (config, R.typeRep @a) of-    ResolvedDeepType -> do-      l1 <- lowerSinglePrimCached' config f-      l2 <- lowerSinglePrimCached' config arg-      let g = l1 l2-      addResult @integerBitWidth t g-      return g-    _ -> translateBinaryError "generalApply" (R.typeRep @(b --> a)) (R.typeRep @b) (R.typeRep @a)-lowerSinglePrimImpl' config t@(DivIntegerTerm _ arg1 arg2) =-  case (config, R.typeRep @a) of-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm' config t arg1 arg2 SBV.sDiv-    _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' config t@(ModIntegerTerm _ arg1 arg2) =-  case (config, R.typeRep @a) of-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm' config t arg1 arg2 SBV.sMod-    _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl' _ _ = undefined--buildUTFun11 ::-  forall integerBitWidth s1 s2 a.-  (SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>-  GrisetteSMTConfig integerBitWidth ->-  R.TypeRep s1 ->-  R.TypeRep s2 ->-  Term a ->-  SymBiMap ->-  Maybe (SBV.Symbolic (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 $ return (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 (SBV.Symbolic (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 $ return (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-  _ -> Nothing-buildUTFun111 _ _ _ _ _ _ = 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 (SBV.Symbolic (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 $ return (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 (SBV.Symbolic (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 $ return (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)-  _ -> Nothing-buildUGFun111 _ _ _ _ _ _ = error "Should only be called on SymTerm"--lowerSinglePrimUFun ::-  forall integerBitWidth a.-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SymBiMap ->-  Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a))-lowerSinglePrimUFun config t@(SymTerm _ _) m =-  case R.typeRep @a of-    TFun3Type (t1 :: R.TypeRep a1) (t2 :: R.TypeRep a2) (t3 :: R.TypeRep a3) -> buildUTFun111 config t1 t2 t3 t m-    TFunType (ta :: R.TypeRep b) (tb :: R.TypeRep b1) -> buildUTFun11 config ta tb t m-    GFun3Type (t1 :: R.TypeRep a1) (t2 :: R.TypeRep a2) (t3 :: R.TypeRep a3) -> buildUGFun111 config t1 t2 t3 t m-    GFunType (ta :: R.TypeRep b) (tb :: R.TypeRep b1) -> buildUGFun11 config ta tb t m-    _ -> Nothing-lowerSinglePrimUFun _ _ _ = error "Should not call this function"--lowerUnaryTerm ::-  forall integerBitWidth a a1 x x1.-  (Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, HasCallStack) =>-  GrisetteSMTConfig integerBitWidth ->-  Term x ->-  Term a ->-  (a1 -> x1) ->-  SymBiMap ->-  SBV.Symbolic (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.-  (Typeable x1, a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>-  GrisetteSMTConfig integerBitWidth ->-  Term x ->-  Term a ->-  Term b ->-  (a1 -> b1 -> x1) ->-  SymBiMap ->-  SBV.Symbolic (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.-  HasCallStack =>-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SymBiMap ->-  SBV.Symbolic (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.-  HasCallStack =>-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)-lowerSinglePrim config t = lowerSinglePrimCached config t emptySymBiMap--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"--lowerSinglePrimImpl ::-  forall integerBitWidth a.-  HasCallStack =>-  GrisetteSMTConfig integerBitWidth ->-  Term a ->-  SymBiMap ->-  SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)-lowerSinglePrimImpl ResolvedConfig {} (ConTerm _ v) m =-  case R.typeRep @a of-    BoolType -> return (m, if v then SBV.sTrue else SBV.sFalse)-    IntegerType -> return (m, fromInteger v)-    SignedBVType _ -> case v of-      IntN x -> return (m, fromInteger x)-    UnsignedBVType _ -> case v of-      WordN x -> return (m, fromInteger x)-    _ -> translateTypeError (R.typeRep @a)-lowerSinglePrimImpl config t@(SymTerm _ ts) m =-  fromMaybe errorMsg $ asum [simple, ufunc]-  where-    errorMsg :: forall x. x-    errorMsg = translateTypeError (R.typeRep @a)-    simple :: Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a))-    simple = case (config, R.typeRep @a) of-      ResolvedSimpleType -> Just $ do-        let name = show ts-        (g :: TermTy integerBitWidth a) <- SBV.free name-        return (addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts) m, g)-      _ -> Nothing-    ufunc :: (Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)))-    ufunc = 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-    ResolvedSimpleType -> 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@(ShiftBitsTerm _ arg n) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm config t arg (`shift` n) m-    _ -> translateBinaryError "shift" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl config t@(RotateBitsTerm _ arg n) m =-  case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm config t arg (`rotate` n) m-    _ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (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)) ->-      withKnownNat n1 $-        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-      where-        n1 :: NatRepr (na + ix - 1)-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)-    (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->-      withKnownNat n1 $-        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-      where-        n1 :: NatRepr (na + ix - 1)-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)-    _ -> 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)) ->-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - 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)) ->-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - 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@(DivIntegerTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m-    _ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(ModIntegerTerm _ arg1 arg2) m =-  case (config, R.typeRep @a) of-    (ResolvedConfig {}, IntegerType) -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m-    _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl _ _ _ = error "Should never happen"--unsafeMkNatRepr :: Int -> NatRepr w-unsafeMkNatRepr x = NatRepr (fromInteger $ toInteger x)--unsafeWithNonZeroKnownNat :: forall w r. Int -> ((KnownNat w, 1 <= w) => r) -> r-unsafeWithNonZeroKnownNat i r-  | i <= 0 = error "Not an nonzero natural number"-  | otherwise = withKnownNat @w (unsafeMkNatRepr i) $ unsafeBVIsNonZero r-  where-    unsafeBVIsNonZero :: ((1 <= w) => r) -> r-    unsafeBVIsNonZero r1 = case unsafeAxiom :: w :~: 1 of-      Refl -> r1--bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r-bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of-  Refl -> r1--parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model-parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs-  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 ->-                unsafeWithNonZeroKnownNat @w bitWidth $-                  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 = WithInfo (IndexedSymbol "arg" idx) FunArg-              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 (iinfosymTerm "arg" idx FunArg) (conTerm v))-                        (conTerm f)-                        acc-                  )-                  (conTerm def)-                  funs-           in GeneralFun sym body-        _ ->-          let sym = WithInfo (IndexedSymbol "arg" idx) FunArg-              vs = bimap (resolveSingle ta1 . head) (resolveSingle ta2) <$> l-              def = resolveSingle ta2 s-              body =-                foldl'-                  ( \acc (v, a) ->-                      pevalITETerm-                        (pevalEqvTerm (iinfosymTerm "arg" idx FunArg) (conTerm v))-                        (conTerm a)-                        acc-                  )-                  (conTerm def)-                  vs-           in GeneralFun 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)--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 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-  UnboundedReasoning c -> DictConfig c-  BoundedReasoning c -> DictConfig c--pattern ResolvedConfig ::-  forall integerBitWidth.-  () =>-  forall s.-  ConfigConstraint integerBitWidth s =>-  SBV.SMTConfig ->-  GrisetteSMTConfig integerBitWidth-pattern ResolvedConfig c <- (resolveConfigView -> DictConfig c)--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)+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# 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.State.Strict+import Data.Bifunctor+import Data.Bits+import Data.Dynamic+import Data.Foldable+import Data.Kind+import Data.Maybe+import qualified Data.SBV as SBV+import qualified Data.SBV.Control as SBVC+import qualified Data.SBV.Internals as SBVI+import Data.Type.Equality (type (~~))+import Data.Typeable+import GHC.Exts (sortWith)+import GHC.Natural+import GHC.Stack+import GHC.TypeNats+import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving+import Grisette.Backend.SBV.Data.SMT.SymBiMap+import Grisette.Core.Data.BV+import Grisette.Core.Data.Class.ModelOps+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils+import Grisette.IR.SymPrim.Data.Prim.Model as PM+import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+import Grisette.IR.SymPrim.Data.TabularFun+import Grisette.Utils.Parameterized+import qualified Type.Reflection as R+import Unsafe.Coerce++cachedResult ::+  forall integerBitWidth a.+  (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>+  Term a ->+  State SymBiMap (Maybe (TermTy integerBitWidth a))+cachedResult t = gets $ \m -> do+  d <- lookupTerm (SomeTerm t) m+  Just $ fromDyn d undefined++addResult ::+  forall integerBitWidth a.+  (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>+  Term a ->+  TermTy integerBitWidth a ->+  State SymBiMap ()+addResult tm sbvtm = modify $ addBiMapIntermediate (SomeTerm tm) (toDyn sbvtm)++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 config v = 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 v = 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 l d) = 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 SBVFreshMonad SBV.Symbolic where+  sbvFresh = SBV.free++instance SBVFreshMonad SBVC.Query where+  sbvFresh = SBVC.freshVar++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@(ShiftBitsTerm _ arg n) m =+  case (config, R.typeRep @a) of+    ResolvedBitsType -> lowerUnaryTerm config t arg (`shift` n) m+    _ -> translateBinaryError "shift" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)+lowerSinglePrimImpl config t@(RotateBitsTerm _ arg n) m =+  case (config, R.typeRep @a) of+    ResolvedBitsType -> lowerUnaryTerm config t arg (`rotate` n) m+    _ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (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++parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model+parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs+  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',

@@ -23,13 +23,22 @@ -- Stability   :   Experimental -- Portability :   GHC only module Grisette.Backend.SBV.Data.SMT.Solving-  ( GrisetteSMTConfig (..),-    sbvConfig,+  ( ApproximationConfig (..),+    ExtraConfig (..),+    precise,+    approx,+    withTimeout,+    clearTimeout,+    withApprox,+    clearApprox,+    GrisetteSMTConfig (..),+    SolvingFailure (..),     TermTy,   ) where  import Control.DeepSeq+import Control.Exception import Control.Monad.Except import qualified Data.HashSet as S import Data.Hashable@@ -41,6 +50,7 @@ import qualified Data.SBV.Control as SBVC import GHC.TypeNats import Grisette.Backend.SBV.Data.SMT.Lowering+import Grisette.Core.Data.BV import Grisette.Core.Data.Class.Bool import Grisette.Core.Data.Class.CEGISSolver import Grisette.Core.Data.Class.Evaluate@@ -49,7 +59,6 @@ import Grisette.Core.Data.Class.ModelOps import Grisette.Core.Data.Class.Solvable import Grisette.Core.Data.Class.Solver-import Grisette.IR.SymPrim.Data.BV import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term import Grisette.IR.SymPrim.Data.Prim.Model as PM@@ -62,6 +71,7 @@ -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim -- >>> import Grisette.Backend.SBV+-- >>> import Data.Proxy  type Aux :: Bool -> Nat -> Type type family Aux o n where@@ -83,6 +93,51 @@   TermTy n (a --> b) = TermTy n a -> TermTy n b   TermTy _ v = v +-- | Configures how to approximate unbounded values.+--+-- For example, if we use @'Approx' ('Data.Proxy' :: 'Data.Proxy' 4)@ to approximate the+-- following unbounded integer:+--+-- > (+ a 9)+--+-- We will get+--+-- > (bvadd a #x9)+--+-- Here the value 9 will be approximated to a 4-bit bit vector, and the+-- operation `bvadd` will be used instead of `+`.+--+-- Note that this approximation may not be sound. See 'GrisetteSMTConfig' for+-- more details.+data ApproximationConfig (n :: Nat) where+  NoApprox :: ApproximationConfig 0+  Approx :: (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) => p n -> ApproximationConfig n++data ExtraConfig (i :: Nat) = ExtraConfig+  { -- | Timeout in milliseconds for each solver call. CEGIS may call the+    -- solver multiple times and each call has its own timeout.+    timeout :: Maybe Int,+    -- | Configures how to approximate unbounded integer values.+    integerApprox :: ApproximationConfig i+  }++preciseExtraConfig :: ExtraConfig 0+preciseExtraConfig =+  ExtraConfig+    { timeout = Nothing,+      integerApprox = NoApprox+    }++approximateExtraConfig ::+  (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) =>+  p n ->+  ExtraConfig n+approximateExtraConfig p =+  ExtraConfig+    { timeout = Nothing,+      integerApprox = Approx p+    }+ -- | Solver configuration for the Grisette SBV backend. -- A Grisette solver configuration consists of a SBV solver configuration and -- the reasoning precision.@@ -101,7 +156,7 @@ -- infinite precision during the symbolic evaluation, but when solving the -- queries, they are translated to bit vectors for better performance. ----- For example, the Grisette term @5 * "a" :: SymInteger@ should be translated+-- For example, the Grisette term @5 * "a" :: 'SymInteger'@ should be translated -- to the following SMT with the unbounded reasoning configuration (the term -- is @t1@): --@@ -134,56 +189,109 @@ -- -- >>> :set -XTypeApplications -XOverloadedStrings -XDataKinds -- >>> let a = "a" :: SymInteger--- >>> solve (UnboundedReasoning z3) $ a >~ 7 &&~ a <~ 9+-- >>> solve (precise z3) $ a >~ 7 &&~ a <~ 9 -- Right (Model {a -> 8 :: Integer})--- >>> solve (BoundedReasoning @4 z3) $ a >~ 7 &&~ a <~ 9+-- >>> solve (approx (Proxy @4) z3) $ a >~ 7 &&~ a <~ 9 -- Left Unsat ----- This should be avoided by setting an large enough reasoning precision to prevent+-- This may be avoided by setting an large enough reasoning precision to prevent -- overflows.-data GrisetteSMTConfig (integerBitWidth :: Nat) where-  UnboundedReasoning :: SBV.SMTConfig -> GrisetteSMTConfig 0-  BoundedReasoning ::-    (KnownNat integerBitWidth, IsZero integerBitWidth ~ 'False, SBV.BVIsNonZero integerBitWidth) =>-    SBV.SMTConfig ->-    GrisetteSMTConfig integerBitWidth+data GrisetteSMTConfig (i :: Nat) = GrisetteSMTConfig {sbvConfig :: SBV.SMTConfig, extraConfig :: ExtraConfig i} --- | Extract the SBV solver configuration from the Grisette solver configuration.-sbvConfig :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBV.SMTConfig-sbvConfig (UnboundedReasoning config) = config-sbvConfig (BoundedReasoning config) = config+-- | A precise reasoning configuration with the given SBV solver configuration.+precise :: SBV.SMTConfig -> GrisetteSMTConfig 0+precise config = GrisetteSMTConfig config preciseExtraConfig +-- | An approximate reasoning configuration with the given SBV solver configuration.+approx ::+  forall p n.+  (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) =>+  p n ->+  SBV.SMTConfig ->+  GrisetteSMTConfig n+approx p config = GrisetteSMTConfig config (approximateExtraConfig p)++-- | Set the timeout for the solver configuration.+withTimeout :: Int -> GrisetteSMTConfig i -> GrisetteSMTConfig i+withTimeout t config = config {extraConfig = (extraConfig config) {timeout = Just t}}++-- | Clear the timeout for the solver configuration.+clearTimeout :: GrisetteSMTConfig i -> GrisetteSMTConfig i+clearTimeout config = config {extraConfig = (extraConfig config) {timeout = Nothing}}++-- | Set the reasoning precision for the solver configuration.+withApprox :: (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) => p n -> GrisetteSMTConfig i -> GrisetteSMTConfig n+withApprox p config = config {extraConfig = (extraConfig config) {integerApprox = Approx p}}++-- | Clear the reasoning precision and perform precise reasoning with the+-- solver configuration.+clearApprox :: GrisetteSMTConfig i -> GrisetteSMTConfig 0+clearApprox config = config {extraConfig = (extraConfig config) {integerApprox = NoApprox}}++data SolvingFailure+  = DSat (Maybe String)+  | Unsat+  | Unk+  | ResultNumLimitReached+  | SolvingError SBV.SBVException+  deriving (Show)++sbvCheckSatResult :: SBVC.CheckSatResult -> SolvingFailure+sbvCheckSatResult SBVC.Sat = error "Should not happen"+sbvCheckSatResult (SBVC.DSat msg) = DSat msg+sbvCheckSatResult SBVC.Unsat = Unsat+sbvCheckSatResult SBVC.Unk = Unk++applyTimeout :: GrisetteSMTConfig i -> Query a -> Query a+applyTimeout config q = case timeout (extraConfig config) of+  Nothing -> q+  Just t -> SBVC.timeout t q+ solveTermWith ::   forall integerBitWidth.   GrisetteSMTConfig integerBitWidth ->   Term Bool ->-  IO (SymBiMap, Either SBVC.CheckSatResult PM.Model)-solveTermWith config term = SBV.runSMTWith (sbvConfig config) $ do-  (m, a) <- lowerSinglePrim config term-  SBVC.query $ do-    SBV.constrain a-    r <- SBVC.checkSat-    case r of-      SBVC.Sat -> do-        md <- SBVC.getModel-        return (m, Right $ parseModel config md m)-      _ -> return (m, Left r)+  IO (Either SolvingFailure PM.Model)+solveTermWith config term =+  handle (return . Left . SolvingError) $+    SBV.runSMTWith (sbvConfig config) $ do+      (m, a) <- lowerSinglePrim config term+      SBVC.query $ applyTimeout config $ do+        SBV.constrain a+        r <- SBVC.checkSat+        case r of+          SBVC.Sat -> do+            md <- SBVC.getModel+            return (Right $ parseModel config md m)+          _ -> return (Left $ sbvCheckSatResult r) -instance Solver (GrisetteSMTConfig n) SBVC.CheckSatResult where-  solve config (Sym t) = snd <$> solveTermWith config t-  solveMulti config n s@(Sym t)-    | n > 0 = SBV.runSMTWith (sbvConfig config) $ do-        (newm, a) <- lowerSinglePrim config t-        SBVC.query $ do-          SBV.constrain a-          r <- SBVC.checkSat-          case r of-            SBVC.Sat -> do-              md <- SBVC.getModel-              let model = parseModel config md newm-              remainingModels n model newm-            _ -> return []-    | otherwise = return []+instance Solver (GrisetteSMTConfig n) SolvingFailure where+  solve config (SymBool t) = solveTermWith config t+  solveMulti config n s@(SymBool t)+    | n > 0 =+        handle+          ( \(x :: SBV.SBVException) -> do+              print "An SBV Exception occurred:"+              print x+              print $+                "Warning: Note that solveMulti do not fully support "+                  ++ "timeouts, and will return an empty list if the solver"+                  ++ "timeouts in any iteration."+              return ([], SolvingError x)+          )+          $ SBV.runSMTWith (sbvConfig config)+          $ do+            (newm, a) <- lowerSinglePrim config t+            SBVC.query $ applyTimeout config $ do+              SBV.constrain a+              r <- SBVC.checkSat+              case r of+                SBVC.Sat -> do+                  md <- SBVC.getModel+                  let model = parseModel config md newm+                  remainingModels n model newm+                _ -> return ([], sbvCheckSatResult r)+    | otherwise = return ([], ResultNumLimitReached)     where       allSymbols = extractSymbolics s :: SymbolSet       next :: PM.Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)@@ -193,7 +301,7 @@                 (\acc (SomeTypedSymbol _ v) -> pevalOrTerm acc (pevalNotTerm (fromJust $ equation v md)))                 (conTerm False)                 (unSymbolSet allSymbols)-        let (lowered, newm) = lowerSinglePrim' config newtm origm+        (newm, lowered) <- lowerSinglePrimCached config newtm origm         SBV.constrain lowered         r <- SBVC.checkSat         case r of@@ -202,41 +310,57 @@             let model = parseModel config md1 newm             return (newm, Right model)           _ -> return (newm, Left r)-      remainingModels :: Int -> PM.Model -> SymBiMap -> Query [PM.Model]+      remainingModels :: Int -> PM.Model -> SymBiMap -> Query ([PM.Model], SolvingFailure)       remainingModels n1 md origm         | n1 > 1 = do             (newm, r) <- next md origm             case r of-              Left _ -> return [md]+              Left r -> return ([md], sbvCheckSatResult r)               Right mo -> do-                rmmd <- remainingModels (n1 - 1) mo newm-                return $ md : rmmd-        | otherwise = return [md]+                (rmmd, e) <- remainingModels (n1 - 1) mo newm+                return (md : rmmd, e)+        | otherwise = return ([md], ResultNumLimitReached)   solveAll = undefined -instance CEGISSolver (GrisetteSMTConfig n) SBVC.CheckSatResult where+instance CEGISSolver (GrisetteSMTConfig n) SolvingFailure where   cegisMultiInputs ::     forall inputs spec.     (ExtractSymbolics inputs, EvaluateSym inputs) =>     GrisetteSMTConfig n ->     [inputs] ->     (inputs -> CEGISCondition) ->-    IO (Either SBVC.CheckSatResult ([inputs], PM.Model))+    IO ([inputs], Either SolvingFailure PM.Model)   cegisMultiInputs config inputs func =-    go1 (cexesAssertFun conInputs) conInputs (error "Should have at least one gen") [] (con True) (con True) symInputs+    case symInputs of+      [] -> do+        m <- solve config (cexesAssertFun conInputs)+        return (conInputs, m)+      _ ->+        handle+          ( \(x :: SBV.SBVException) -> do+              print "An SBV Exception occurred:"+              print x+              print $+                "Warning: Note that CEGIS procedures do not fully support "+                  ++ "timeouts, and will return an empty counter example list if "+                  ++ "the solver timeouts during guessing phase."+              return ([], Left $ SolvingError x)+          )+          $ go1 (cexesAssertFun conInputs) conInputs (error "Should have at least one gen") [] (con True) (con True) symInputs     where       (conInputs, symInputs) = partition (isEmptySet . extractSymbolics) inputs+      go1 :: SymBool -> [inputs] -> PM.Model -> [inputs] -> SymBool -> SymBool -> [inputs] -> IO ([inputs], Either SolvingFailure PM.Model)       go1 cexFormula cexes previousModel inputs pre post remainingSymInputs = do         case remainingSymInputs of-          [] -> return $ Right (cexes, previousModel)+          [] -> return (cexes, Right previousModel)           newInput : vs -> do             let CEGISCondition nextPre nextPost = func newInput             let finalPre = pre &&~ nextPre             let finalPost = post &&~ nextPost             r <- go cexFormula newInput (newInput : inputs) finalPre finalPost             case r of-              Left failure -> return $ Left failure-              Right (newCexes, mo) -> do+              (newCexes, Left failure) -> return (cexes ++ newCexes, Left failure)+              (newCexes, Right mo) -> do                 go1                   (cexFormula &&~ cexesAssertFun newCexes)                   (cexes ++ newCexes)@@ -255,27 +379,28 @@         [inputs] ->         SymBool ->         SymBool ->-        IO (Either SBVC.CheckSatResult ([inputs], PM.Model))+        IO ([inputs], Either SolvingFailure PM.Model)       go cexFormula inputs allInputs pre post =         SBV.runSMTWith (sbvConfig config) $ do-          let Sym t = phi &&~ cexFormula+          let SymBool t = phi &&~ cexFormula           (newm, a) <- lowerSinglePrim config t           SBVC.query $-            snd <$> do-              SBV.constrain a-              r <- SBVC.checkSat-              mr <- case r of-                SBVC.Sat -> do-                  md <- SBVC.getModel-                  return $ Right $ parseModel config md newm-                _ -> return $ Left r-              loop ((forallSymbols `exceptFor`) <$> mr) [] newm+            applyTimeout config $+              snd <$> do+                SBV.constrain a+                r <- SBVC.checkSat+                mr <- case r of+                  SBVC.Sat -> do+                    md <- SBVC.getModel+                    return $ Right $ parseModel config md newm+                  _ -> return $ Left $ sbvCheckSatResult r+                loop ((forallSymbols `exceptFor`) <$> mr) [] newm         where           forallSymbols :: SymbolSet           forallSymbols = extractSymbolics allInputs           phi = pre &&~ post           negphi = pre &&~ nots post-          check :: Model -> IO (Either SBVC.CheckSatResult (inputs, PM.Model))+          check :: Model -> IO (Either SolvingFailure (inputs, PM.Model))           check candidate = do             let evaluated = evaluateSym False candidate negphi             r <- solve config evaluated@@ -283,10 +408,10 @@               m <- r               let newm = exact forallSymbols m               return (evaluateSym False newm inputs, newm)-          guess :: Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)+          guess :: Model -> SymBiMap -> Query (SymBiMap, Either SolvingFailure PM.Model)           guess candidate origm = do-            let Sym evaluated = evaluateSym False candidate phi-            let (lowered, newm) = lowerSinglePrim' config evaluated origm+            let SymBool evaluated = evaluateSym False candidate phi+            (newm, lowered) <- lowerSinglePrimCached config evaluated origm             SBV.constrain lowered             r <- SBVC.checkSat             case r of@@ -294,21 +419,21 @@                 md <- SBVC.getModel                 let model = parseModel config md newm                 return (newm, Right $ exceptFor forallSymbols model)-              _ -> return (newm, Left r)+              _ -> return (newm, Left $ sbvCheckSatResult r)           loop ::-            Either SBVC.CheckSatResult PM.Model ->+            Either SolvingFailure PM.Model ->             [inputs] ->             SymBiMap ->-            Query (SymBiMap, Either SBVC.CheckSatResult ([inputs], PM.Model))-          loop (Right mo) cexs origm = do+            Query (SymBiMap, ([inputs], Either SolvingFailure PM.Model))+          loop (Right mo) cexes origm = do             r <- liftIO $ check mo             case r of-              Left SBVC.Unsat -> return (origm, Right (cexs, mo))-              Left v -> return (origm, Left v)+              Left Unsat -> return (origm, (cexes, Right mo))+              Left v -> return (origm, (cexes, Left v))               Right (cex, cexm) -> do                 (newm, res) <- guess cexm origm-                loop res (cex : cexs) newm-          loop (Left v) _ origm = return (origm, Left v)+                loop res (cex : cexes) newm+          loop (Left v) cexes origm = return (origm, (cexes, Left v))  newtype CegisInternal = CegisInternal Int   deriving (Eq, Show, Ord, Lift)

@@ -6,7 +6,9 @@ {-# LANGUAGE UndecidableInstances #-}  module Grisette.Backend.SBV.Data.SMT.Solving-  ( GrisetteSMTConfig (..),+  ( ApproximationConfig (..),+    ExtraConfig (..),+    GrisetteSMTConfig (..),     TermTy,   ) where@@ -14,7 +16,7 @@ import Data.Kind import qualified Data.SBV as SBV import GHC.TypeNats-import Grisette.IR.SymPrim.Data.BV+import Grisette.Core.Data.BV import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term import Grisette.IR.SymPrim.Data.TabularFun @@ -38,9 +40,13 @@   TermTy n (a --> b) = TermTy n a -> TermTy n b   TermTy _ v = v -data GrisetteSMTConfig (integerBitWidth :: Nat) where-  UnboundedReasoning :: SBV.SMTConfig -> GrisetteSMTConfig 0-  BoundedReasoning ::-    (KnownNat integerBitWidth, IsZero integerBitWidth ~ 'False, SBV.BVIsNonZero integerBitWidth) =>-    SBV.SMTConfig ->-    GrisetteSMTConfig integerBitWidth+data ApproximationConfig (n :: Nat) where+  NoApprox :: ApproximationConfig 0+  Approx :: (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) => p n -> ApproximationConfig n++data ExtraConfig (i :: Nat) = ExtraConfig+  { timeout :: Maybe Int,+    integerApprox :: ApproximationConfig i+  }++data GrisetteSMTConfig (i :: Nat) = GrisetteSMTConfig {sbvConfig :: SBV.SMTConfig, extraConfig :: ExtraConfig i}

@@ -74,7 +74,8 @@     -- The values of unsolvable types are __/partially/__ merged in a symbolic     -- union, which is essentially an if-then-else tree.     ---    -- For example, assume that the lists have the type @[SymBool]@.+    -- For example, assume that the lists have the type+    -- @['Grisette.IR.SymPrim.SymBool']@.     -- In the following example, the result shows that @[b]@ and @[c]@ can be     -- merged together in the same symbolic union because they have the same     -- length:@@ -125,11 +126,15 @@     -- Grisette     -- currently provides an implementation for the following solvable types:     ---    -- * @SymBool@ or @Sym Bool@ (symbolic Booleans)-    -- * @SymInteger@ or @Sym Integer@ (symbolic unbounded integers)-    -- * @SymIntN n@ or @Sym (IntN n)@ (symbolic signed bit vectors of length @n@)-    -- * @SymWordN n@ or @Sym (WordN n)@ (symbolic unsigned bit vectors of length @n@)+    -- * 'Grisette.IR.SymPrim.SymBool' (symbolic Booleans)+    -- * 'Grisette.IR.SymPrim.SymInteger' (symbolic unbounded integers)+    -- * @'Grisette.IR.SymPrim.SymIntN' n@ (symbolic signed bit vectors of length @n@)+    -- * @'Grisette.IR.SymPrim.SymWordN' n@ (symbolic unsigned bit vectors of length @n@)     --+    -- The two bit vector types has their lengths checked at compile time.+    -- Grisette also provides runtime-checked versions of these types:+    -- 'Grisette.IR.SymPrim.SomeSymIntN' and 'Grisette.IR.SymPrim.SomeSymWordN'.+    --     -- Values of a solvable type can consist of concrete values, symbolic     -- constants (placeholders for concrete values that can be assigned by a     -- solver to satisfy a formula), and complex symbolic formulas with@@ -176,13 +181,17 @@     SEq (..),     SymBoolOp,     SOrd (..),-    BVConcat (..),-    BVExtend (..),-    BVSelect (..),-    bvextract,-    SignedDivMod (..),-    UnsignedDivMod (..),-    SignedQuotRem (..),+    SomeBV (..),+    someBVZext',+    someBVSext',+    someBVExt',+    someBVSelect',+    someBVExtract,+    someBVExtract',+    SizedBV (..),+    sizedBVExtract,+    SafeDivision (..),+    SafeLinearArith (..),     SymIntegerOp,     Function (..), @@ -555,6 +564,7 @@     makeUnionWrapper,     makeUnionWrapper',     liftToMonadUnion,+    unionSize,      -- *** Merging @@ -596,6 +606,7 @@     pattern SingleU,     pattern IfU,     MonadUnion,+    MonadParallelUnion (..),     simpleMerge,     onUnion,     onUnion2,@@ -758,7 +769,7 @@     -- >>> res = mrgIf a (throwError Error1) (mrgIf b (return c) (throwError Error2)) :: ExceptT Error UnionM SymBool     -- >>> res     -- ExceptT {If (|| a (! b)) (If a (Left Error1) (Left Error2)) (Right c)}-    -- >>> solveExcept (UnboundedReasoning z3) (\case Left _ -> con False; Right x -> x) res+    -- >>> solveExcept (precise z3) (\case Left _ -> con False; Right x -> x) res     -- Right (Model {a -> False :: Bool, b -> True :: Bool, c -> True :: Bool})     --     -- The solver call in the above example means that we want the solver to@@ -782,6 +793,7 @@     TransformError (..),     symAssert,     symAssume,+    symAssertWith,     symAssertTransformableError,     symThrowTransformableError, @@ -827,9 +839,9 @@     -- >>> import Grisette.Backend.SBV     -- >>> let x = "x" :: SymInteger     -- >>> let y = "y" :: SymInteger-    -- >>> solve (UnboundedReasoning z3) (x + y ==~ 6 &&~ x - y ==~ 20)+    -- >>> solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)     -- Right (Model {x -> 13 :: Integer, y -> -7 :: Integer})-    -- >>> solve (UnboundedReasoning z3) (x + y ==~ 6 &&~ x - y ==~ 19)+    -- >>> solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 19)     -- Left Unsat     --     -- The first parameter of 'solve' is the solver configuration.@@ -848,7 +860,7 @@     -- evaluate symbolic values. The following code evaluates the product of     -- x and y under the solution of the equation system.     ---    -- >>> Right m <- solve (UnboundedReasoning z3) (x + y ==~ 6 &&~ x - y ==~ 20)+    -- >>> Right m <- solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)     -- >>> evaluateSym False m (x * y)     -- -91     --@@ -890,15 +902,6 @@     --   deriving (Mergeable, SEq) via (Default Error)     -- :}     ---    -- Then we define how to transform the generic errors to the error type.-    ---    -- >>> :{-    --   instance TransformError ArithException Error where-    --     transformError _ = Arith-    --   instance TransformError AssertionError Error where-    --     transformError _ = Assert-    -- :}-    --     -- Then we can perform the symbolic evaluation. The `divs` function throws     -- 'ArithException' when the divisor is 0, which would be transformed to     -- @Arith@, and the `symAssert` function would throw 'AssertionError' when@@ -906,14 +909,16 @@     --     -- >>> let x = "x" :: SymInteger     -- >>> let y = "y" :: SymInteger+    -- >>> assert = symAssertWith Assert+    -- >>> sdiv = safeDiv' (const Arith)     -- >>> :{     --   -- equivalent concrete program:     --   -- let x = x `div` y     --   -- if z > 0 then assert (x >= y) else return ()     --   res :: ExceptT Error UnionM ()     --   res = do-    --     z <- x `divs` y-    --     mrgIf (z >~ 0) (symAssert (x >=~ y)) (return ())+    --     z <- x `sdiv` y+    --     mrgIf (z >~ 0) (assert (x >=~ y)) (return ())     -- :}     --     -- Then we can ask the solver to find a counter-example that would lead to@@ -1010,6 +1015,7 @@ import Grisette.Core.BuiltinUnionWrappers import Grisette.Core.Control.Exception import Grisette.Core.Control.Monad.CBMCExcept+import Grisette.Core.Control.Monad.Class.MonadParallelUnion import Grisette.Core.Control.Monad.Union import Grisette.Core.Control.Monad.UnionM import Grisette.Core.Data.Class.BitVector@@ -1020,10 +1026,10 @@ import Grisette.Core.Data.Class.ExtractSymbolics import Grisette.Core.Data.Class.Function import Grisette.Core.Data.Class.GenSym-import Grisette.Core.Data.Class.Integer import Grisette.Core.Data.Class.Mergeable import Grisette.Core.Data.Class.ModelOps import Grisette.Core.Data.Class.SOrd+import Grisette.Core.Data.Class.SafeArith import Grisette.Core.Data.Class.SimpleMergeable import Grisette.Core.Data.Class.Solvable import Grisette.Core.Data.Class.Solver

@@ -0,0 +1,123 @@+{-# LANGUAGE LambdaCase #-}++-- |+-- Module      :   Grisette.Core.Control.Monad.Class.MonadParallelUnion+-- Copyright   :   (c) Sirui Lu 2023+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Core.Control.Monad.Class.MonadParallelUnion+  ( MonadParallelUnion (..),+  )+where++import Control.DeepSeq+import Control.Monad.Cont+import Control.Monad.Except+import Control.Monad.Identity+import qualified Control.Monad.RWS.Lazy as RWSLazy+import qualified Control.Monad.RWS.Strict as RWSStrict+import Control.Monad.Reader+import qualified Control.Monad.State.Lazy as StateLazy+import qualified Control.Monad.State.Strict as StateStrict+import Control.Monad.Trans.Maybe+import qualified Control.Monad.Writer.Lazy as WriterLazy+import qualified Control.Monad.Writer.Strict as WriterStrict+import Grisette.Core.Data.Class.Mergeable+import Grisette.Core.Data.Class.SimpleMergeable+import Grisette.Lib.Control.Monad++-- | Parallel union monad.+--+-- With the @QualifiedDo@ extension and the "Grisette.Qualified.ParallelUnionDo"+-- module, one can execute the paths in parallel and merge the results with:+--+-- > :set -XQualifiedDo -XOverloadedStrings+-- > import Grisette+-- > import qualified Grisette.Qualified.ParallelUnionDo as P+-- > P.do+-- >   x <- mrgIf "a" (return 1) (return 2) :: UnionM Int+-- >   return $ x + 1+-- >+-- > -- {If a 2 3}+class (UnionLike m, Monad m) => MonadParallelUnion m where+  parBindUnion :: (Mergeable b, NFData b) => m a -> (a -> m b) -> m b++instance (MonadParallelUnion m) => MonadParallelUnion (MaybeT m) where+  parBindUnion (MaybeT x) f =+    MaybeT $+      x `parBindUnion` \case+        Nothing -> return Nothing+        Just x'' -> runMaybeT $ f x''+  {-# INLINE parBindUnion #-}++instance (MonadParallelUnion m, Mergeable e, NFData e) => MonadParallelUnion (ExceptT e m) where+  parBindUnion (ExceptT x) f =+    ExceptT $+      x `parBindUnion` \case+        Left e -> return $ Left e+        Right x'' -> runExceptT $ f x''+  {-# INLINE parBindUnion #-}++instance (MonadParallelUnion m, Mergeable s, NFData s) => MonadParallelUnion (StateLazy.StateT s m) where+  parBindUnion (StateLazy.StateT x) f = StateLazy.StateT $ \s ->+    x s `parBindUnion` \case+      ~(a, s') -> StateLazy.runStateT (f a) s'+  {-# INLINE parBindUnion #-}++instance (MonadParallelUnion m, Mergeable s, NFData s) => MonadParallelUnion (StateStrict.StateT s m) where+  parBindUnion (StateStrict.StateT x) f = StateStrict.StateT $ \s ->+    x s `parBindUnion` \case+      (a, s') -> StateStrict.runStateT (f a) s'+  {-# INLINE parBindUnion #-}++instance (MonadParallelUnion m, Mergeable s, Monoid s, NFData s) => MonadParallelUnion (WriterLazy.WriterT s m) where+  parBindUnion (WriterLazy.WriterT x) f =+    WriterLazy.WriterT $+      x `parBindUnion` \case+        ~(a, w) ->+          WriterLazy.runWriterT (f a) `parBindUnion` \case+            ~(b, w') -> return (b, w <> w')+  {-# INLINE parBindUnion #-}++instance (MonadParallelUnion m, Mergeable s, Monoid s, NFData s) => MonadParallelUnion (WriterStrict.WriterT s m) where+  parBindUnion (WriterStrict.WriterT x) f =+    WriterStrict.WriterT $+      x `parBindUnion` \case+        (a, w) ->+          WriterStrict.runWriterT (f a) `parBindUnion` \case+            (b, w') -> return (b, w <> w')+  {-# INLINE parBindUnion #-}++instance (MonadParallelUnion m, Mergeable a, NFData a) => MonadParallelUnion (ReaderT a m) where+  parBindUnion (ReaderT x) f = ReaderT $ \a ->+    x a `parBindUnion` \a' -> runReaderT (f a') a+  {-# INLINE parBindUnion #-}++instance (MonadParallelUnion m) => MonadParallelUnion (IdentityT m) where+  parBindUnion (IdentityT x) f = IdentityT $ x `parBindUnion` (merge . runIdentityT . f)+  {-# INLINE parBindUnion #-}++instance+  (MonadParallelUnion m, Mergeable s, Mergeable r, Mergeable w, Monoid w, NFData r, NFData w, NFData s) =>+  MonadParallelUnion (RWSStrict.RWST r w s m)+  where+  parBindUnion m k = RWSStrict.RWST $ \r s ->+    RWSStrict.runRWST m r s `parBindUnion` \case+      (a, s', w) ->+        RWSStrict.runRWST (k a) r s' `parBindUnion` \case+          (b, s'', w') -> return (b, s'', w <> w')+  {-# INLINE parBindUnion #-}++instance+  (MonadParallelUnion m, Mergeable s, Mergeable r, Mergeable w, Monoid w, NFData r, NFData w, NFData s) =>+  MonadParallelUnion (RWSLazy.RWST r w s m)+  where+  parBindUnion m k = RWSLazy.RWST $ \r s ->+    RWSLazy.runRWST m r s `parBindUnion` \case+      ~(a, s', w) ->+        RWSLazy.runRWST (k a) r s' `parBindUnion` \case+          ~(b, s'', w') -> return (b, s'', w <> w')+  {-# INLINE parBindUnion #-}

@@ -25,5 +25,5 @@ -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim --- | Class for monads that support union-like operations and 'Mergeable' knowledge propagation.+-- | Class for monads that support union-like operations and 'Grisette.Core.Data.Class.Mergeable' knowledge propagation. type MonadUnion u = (UnionLike u, Monad u)

@@ -1,4 +1,7 @@ {-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# HLINT ignore "Use <&>" #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}@@ -11,10 +14,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}-{-# OPTIONS_GHC -fno-cse #-} -{-# HLINT ignore "Use <&>" #-}- -- {-# OPTIONS_GHC -fno-full-laziness #-}  -- |@@ -33,19 +33,24 @@     isMerged,     (#~),     IsConcrete,+    unionSize,   ) where  import Control.DeepSeq import Control.Monad.Identity (Identity (..))+import Control.Parallel.Strategies import Data.Functor.Classes import qualified Data.HashMap.Lazy as HML import Data.Hashable import Data.IORef import Data.String import GHC.IO hiding (evaluate)+import GHC.TypeNats import Grisette.Core.Control.Monad.CBMCExcept+import Grisette.Core.Control.Monad.Class.MonadParallelUnion import Grisette.Core.Control.Monad.Union+import Grisette.Core.Data.BV import Grisette.Core.Data.Class.Bool import Grisette.Core.Data.Class.Evaluate import Grisette.Core.Data.Class.ExtractSymbolics@@ -60,6 +65,9 @@ import Grisette.Core.Data.Class.ToCon import Grisette.Core.Data.Class.ToSym import Grisette.Core.Data.Union+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+import Grisette.IR.SymPrim.Data.SymPrim+import Grisette.IR.SymPrim.Data.TabularFun import Language.Haskell.TH.Syntax import Language.Haskell.TH.Syntax.Compat (unTypeSplice) @@ -172,8 +180,6 @@ data UnionM a where   -- | 'UnionM' with no 'Mergeable' knowledge.   UAny ::-    -- | (Possibly) cached merging result.-    IORef (Either (Union a) (UnionM a)) ->     -- | Original 'Union'.     Union a ->     UnionM a@@ -189,18 +195,14 @@   rnf = rnf1  instance NFData1 UnionM where-  liftRnf _a (UAny i m) = rnf i `seq` liftRnf _a m+  liftRnf _a (UAny m) = liftRnf _a m   liftRnf _a (UMrg _ m) = liftRnf _a m  instance (Lift a) => Lift (UnionM a) where-  liftTyped (UAny _ v) = [||freshUAny v||]-  liftTyped (UMrg _ v) = [||freshUAny v||]+  liftTyped (UAny v) = [||UAny v||]+  liftTyped (UMrg _ v) = [||UAny v||]   lift = unTypeSplice . liftTyped -freshUAny :: Union a -> UnionM a-freshUAny v = UAny (unsafeDupablePerformIO $ newIORef $ Left v) v-{-# NOINLINE freshUAny #-}- instance (Show a) => (Show (UnionM a)) where   showsPrec = showsPrec1 @@ -228,7 +230,7 @@ wrapBracket l r p = showChar l . p . showChar r  instance Show1 UnionM where-  liftShowsPrec sp sl i (UAny _ a) =+  liftShowsPrec sp sl i (UAny a) =     wrapBracket '<' '>'       . liftShowsPrecUnion sp sl 0       $ a@@ -239,7 +241,7 @@  -- | Extract the underlying Union. May be unmerged. underlyingUnion :: UnionM a -> Union a-underlyingUnion (UAny _ a) = a+underlyingUnion (UAny a) = a underlyingUnion (UMrg _ a) = a {-# INLINE underlyingUnion #-} @@ -252,8 +254,8 @@ instance UnionPrjOp UnionM where   singleView = singleView . underlyingUnion   {-# INLINE singleView #-}-  ifView (UAny _ u) = case ifView u of-    Just (c, t, f) -> Just (c, freshUAny t, freshUAny f)+  ifView (UAny u) = case ifView u of+    Just (c, t, f) -> Just (c, UAny t, UAny f)     Nothing -> Nothing   ifView (UMrg m u) = case ifView u of     Just (c, t, f) -> Just (c, UMrg m t, UMrg m f)@@ -282,6 +284,24 @@   a >>= f = bindUnion (underlyingUnion a) f   {-# INLINE (>>=) #-} +parBindUnion'' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b+parBindUnion'' (Single a) f = merge $ f a+parBindUnion'' u f = parBindUnion' u f++parBindUnion' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b+parBindUnion' (Single a') f' = f' a'+parBindUnion' (If _ _ cond ifTrue ifFalse) f' = runEval $ do+  l <- rpar $ force $ parBindUnion' ifTrue f'+  r <- rpar $ force $ parBindUnion' ifFalse f'+  l' <- rseq l+  r' <- rseq r+  rseq $ mrgIf cond l' r'+{-# INLINE parBindUnion' #-}++instance MonadParallelUnion UnionM where+  parBindUnion = parBindUnion'' . underlyingUnion+  {-# INLINE parBindUnion #-}+ instance (Mergeable a) => Mergeable (UnionM a) where   rootStrategy = SimpleStrategy $ \cond t f -> unionIf cond t f >>= mrgSingle   {-# INLINE rootStrategy #-}@@ -300,21 +320,16 @@  instance UnionLike UnionM where   mergeWithStrategy _ m@(UMrg _ _) = m-  mergeWithStrategy s (UAny ref u) = unsafeDupablePerformIO $-    atomicModifyIORef' ref $ \case-      x@(Right r) -> (x, r)-      Left _ -> (Right r, r)-        where-          !r = UMrg s $ fullReconstruct s u -- m >>= mrgSingle-  {-# NOINLINE mergeWithStrategy #-}+  mergeWithStrategy s (UAny u) = UMrg s $ fullReconstruct s u+  {-# INLINE mergeWithStrategy #-}   mrgIfWithStrategy s (Con c) l r = if c then mergeWithStrategy s l else mergeWithStrategy s r   mrgIfWithStrategy s cond l r =     mergeWithStrategy s $ unionIf cond l r   {-# INLINE mrgIfWithStrategy #-}-  single = freshUAny . single+  single = UAny . single   {-# INLINE single #-}-  unionIf cond (UAny _ a) (UAny _ b) = freshUAny $ unionIf cond a b-  unionIf cond (UMrg m a) (UAny _ b) = UMrg m $ ifWithStrategy m cond a b+  unionIf cond (UAny a) (UAny b) = UAny $ unionIf cond a b+  unionIf cond (UMrg m a) (UAny b) = UMrg m $ ifWithStrategy m cond a b   unionIf cond a (UMrg m b) = UMrg m $ ifWithStrategy m cond (underlyingUnion a) b   {-# INLINE unionIf #-} @@ -353,19 +368,46 @@     y1 <- y     x1 `symCompare` y1 -instance {-# OVERLAPPABLE #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where+instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where   toSym = mrgSingle . toSym -instance {-# OVERLAPPING #-} (ToSym a b, Mergeable b) => ToSym (UnionM a) (UnionM b) where+instance (ToSym a b, Mergeable b) => ToSym (UnionM a) (UnionM b) where   toSym = merge . fmap toSym -instance {-# OVERLAPPABLE #-} (ToCon a b) => ToCon (UnionM a) b where+#define TO_SYM_FROM_UNION_CON_SIMPLE(contype, symtype) \+instance ToSym (UnionM contype) symtype where \+  toSym = simpleMerge . fmap con++#define TO_SYM_FROM_UNION_CON_BV(contype, symtype) \+instance (KnownNat n, 1 <= n) => ToSym (UnionM (contype n)) (symtype n) where \+  toSym = simpleMerge . fmap con++#define TO_SYM_FROM_UNION_CON_FUN(conop, symop) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (conop ca cb)) (symop sa sb) where \+  toSym = simpleMerge . fmap con++#define TO_SYM_FROM_UNION_CON_BV_SOME(contype, symtype) \+instance ToSym (UnionM contype) symtype where \+  toSym = simpleMerge . fmap (toSym :: contype -> symtype)++#if 1+TO_SYM_FROM_UNION_CON_SIMPLE(Bool, SymBool)+TO_SYM_FROM_UNION_CON_SIMPLE(Integer, SymInteger)+TO_SYM_FROM_UNION_CON_BV(IntN, SymIntN)+TO_SYM_FROM_UNION_CON_BV(WordN, SymWordN)+TO_SYM_FROM_UNION_CON_FUN((=->), (=~>))+TO_SYM_FROM_UNION_CON_FUN((-->), (-~>))+TO_SYM_FROM_UNION_CON_BV_SOME(SomeIntN, SomeSymIntN)+TO_SYM_FROM_UNION_CON_BV_SOME(SomeWordN, SomeSymWordN)+#endif++instance {-# INCOHERENT #-} (ToCon a b) => ToCon (UnionM a) b where   toCon v = go $ underlyingUnion v     where       go (Single x) = toCon x       go _ = Nothing -instance {-# OVERLAPPING #-} (ToCon a b, Mergeable b) => ToCon (UnionM a) (UnionM b) where+instance (ToCon a b, Mergeable b) => ToCon (UnionM a) (UnionM b) where   toCon v = go $ underlyingUnion v     where       go (Single x) = case toCon x of@@ -387,6 +429,7 @@           (go t)           (go f) +{- instance (Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) where   substituteSym sym val x = go $ underlyingUnion x     where@@ -397,6 +440,7 @@           (substituteSym sym val cond)           (go t)           (go f)+          -}  instance   (ExtractSymbolics a) =>@@ -408,11 +452,11 @@       go (If _ _ cond t f) = extractSymbolics cond <> go t <> go f  instance (Hashable a) => Hashable (UnionM a) where-  s `hashWithSalt` (UAny _ u) = s `hashWithSalt` (0 :: Int) `hashWithSalt` u+  s `hashWithSalt` (UAny u) = s `hashWithSalt` (0 :: Int) `hashWithSalt` u   s `hashWithSalt` (UMrg _ u) = s `hashWithSalt` (1 :: Int) `hashWithSalt` u  instance (Eq a) => Eq (UnionM a) where-  UAny _ l == UAny _ r = l == r+  UAny l == UAny r = l == r   UMrg _ l == UMrg _ r = l == r   _ == _ = False @@ -481,22 +525,6 @@ instance (IsString a, Mergeable a) => IsString (UnionM a) where   fromString = mrgSingle . fromString -{--foldMapUnion :: (Monoid m) => (a -> m) -> Union a -> m-foldMapUnion f (Single v) = f v-foldMapUnion f (If _ _ _ l r) = foldMapUnion f l <> foldMapUnion f r--instance Foldable UnionM where-  foldMap f u = foldMapUnion f (underlyingUnion u)--sequenceAUnion :: (Applicative m, SymBoolOp bool) => Union (m a) -> m (Union a)-sequenceAUnion (Single v) = single <$> v-sequenceAUnion (If _ _ cond l r) = unionIf cond <$> sequenceAUnion l <*> sequenceAUnion r--instance  Traversable UnionM where-  sequenceA u = freshUAny <$> sequenceAUnion (underlyingUnion u)-  -}- -- GenSym instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a) @@ -514,6 +542,10 @@       go (Single x) = fresh x       go (If _ _ _ t f) = mrgIf <$> simpleFresh () <*> go t <*> go f +-- AllSyms+instance AllSyms a => AllSyms (UnionM a) where+  allSymsS = allSymsS . underlyingUnion+ -- Concrete Key HashMaps  -- | Tag for concrete types.@@ -554,3 +586,18 @@  instance UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v where   extractUnionExcept = fmap runCBMCEither++-- | The size of a union is defined as the number of branches.+-- For example,+--+-- >>> unionSize (single True)+-- 1+-- >>> unionSize (mrgIf "a" (single 1) (single 2) :: UnionM Integer)+-- 2+-- >>> unionSize (choose [1..7] "a" :: UnionM Integer)+-- 7+unionSize :: UnionM a -> Int+unionSize = unionSize' . underlyingUnion+  where+    unionSize' (Single _) = 1+    unionSize' (If _ _ _ l r) = unionSize' l + unionSize' r

@@ -13,8 +13,6 @@ data UnionM a where   -- | 'UnionM' with no 'Mergeable' knowledge.   UAny ::-    -- | (Possibly) cached merging result.-    IORef (Either (Union a) (UnionM a)) ->     -- | Original 'Union'.     Union a ->     UnionM a

@@ -0,0 +1,691 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveLift #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -funbox-strict-fields #-}++-- |+-- Module      :   Grisette.Core.Data.BV+-- 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.Core.Data.BV+  ( BitwidthMismatch (..),+    IntN (..),+    WordN (..),+    SomeIntN (..),+    SomeWordN (..),+    unarySomeIntN,+    unarySomeIntNR1,+    binSomeIntN,+    binSomeIntNR1,+    binSomeIntNR2,+    unarySomeWordN,+    unarySomeWordNR1,+    binSomeWordN,+    binSomeWordNR1,+    binSomeWordNR2,+  )+where++import Control.DeepSeq+import Control.Exception+import Data.Bits+import Data.CallStack+import Data.Hashable+import Data.Proxy+import Data.Typeable+import GHC.Enum+import GHC.Generics+import GHC.Read+import GHC.Real+import GHC.TypeNats+import Grisette.Core.Data.Class.BitVector+import Grisette.Utils.Parameterized+import Language.Haskell.TH.Syntax+import Numeric+import Text.Read+import qualified Text.Read.Lex as L++data BitwidthMismatch = BitwidthMismatch+  deriving (Show, Eq, Ord, Generic)++instance Exception BitwidthMismatch where+  displayException BitwidthMismatch = "Bit width does not match"++-- |+-- Symbolic unsigned bit vectors.+newtype WordN (n :: Nat) = WordN {unWordN :: Integer}+  deriving (Eq, Ord, Generic, Lift, Hashable, NFData)++-- |+-- A non-indexed version of 'WordN'.+data SomeWordN where+  SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN++unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r+unarySomeWordN op (SomeWordN (w :: WordN w)) = op w+{-# INLINE unarySomeWordN #-}++unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN+unarySomeWordNR1 op (SomeWordN (w :: WordN w)) = SomeWordN $ op w+{-# INLINE unarySomeWordNR1 #-}++binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r+binSomeWordN op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =+  case sameNat (Proxy @l) (Proxy @r) of+    Just Refl -> op l r+    Nothing -> throw BitwidthMismatch+{-# INLINE binSomeWordN #-}++binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN+binSomeWordNR1 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =+  case sameNat (Proxy @l) (Proxy @r) of+    Just Refl -> SomeWordN $ op l r+    Nothing -> throw BitwidthMismatch+{-# INLINE binSomeWordNR1 #-}++binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)+binSomeWordNR2 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =+  case sameNat (Proxy @l) (Proxy @r) of+    Just Refl ->+      case op l r of+        (a, b) -> (SomeWordN a, SomeWordN b)+    Nothing -> throw BitwidthMismatch+{-# INLINE binSomeWordNR2 #-}++instance Eq SomeWordN where+  (==) = binSomeWordN (==)+  {-# INLINE (==) #-}+  (/=) = binSomeWordN (/=)+  {-# INLINE (/=) #-}++instance Ord SomeWordN where+  (<=) = binSomeWordN (<=)+  {-# INLINE (<=) #-}+  (<) = binSomeWordN (<)+  {-# INLINE (<) #-}+  (>=) = binSomeWordN (>=)+  {-# INLINE (>=) #-}+  (>) = binSomeWordN (>)+  {-# INLINE (>) #-}+  max = binSomeWordNR1 max+  {-# INLINE max #-}+  min = binSomeWordNR1 min+  {-# INLINE min #-}+  compare = binSomeWordN compare+  {-# INLINE compare #-}++instance Lift SomeWordN where+  liftTyped (SomeWordN w) = [||SomeWordN w||]++instance Hashable SomeWordN where+  s `hashWithSalt` (SomeWordN (w :: WordN n)) = s `hashWithSalt` natVal (Proxy @n) `hashWithSalt` w++instance NFData SomeWordN where+  rnf (SomeWordN w) = rnf w++instance (KnownNat n, 1 <= n) => Show (WordN n) where+  show (WordN w) = if (bitwidth `mod` 4) == 0 then hexRepPre ++ hexRep else binRepPre ++ binRep+    where+      bitwidth = natVal (Proxy :: Proxy n)+      hexRepPre = "0x" ++ replicate (fromIntegral (bitwidth `div` 4) - length hexRep) '0'+      hexRep = showHex w ""+      binRepPre = "0b" ++ replicate (fromIntegral bitwidth - length binRep) '0'+      binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w ""++convertInt :: Num a => L.Lexeme -> ReadPrec a+convertInt (L.Number n)+  | Just i <- L.numberToInteger n = return (fromInteger i)+convertInt _ = pfail++instance (KnownNat n, 1 <= n) => Read (WordN n) where+  readPrec = readNumber convertInt+  readListPrec = readListPrecDefault+  readList = readListDefault++instance Show SomeWordN where+  show (SomeWordN w) = show w++-- |+-- Symbolic signed bit vectors.+newtype IntN (n :: Nat) = IntN {unIntN :: Integer}+  deriving (Eq, Generic, Lift, Hashable, NFData)++-- |+-- A non-indexed version of 'IntN'.+data SomeIntN where+  SomeIntN :: (KnownNat n, 1 <= n) => IntN n -> SomeIntN++unarySomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> r) -> SomeIntN -> r+unarySomeIntN op (SomeIntN (w :: IntN w)) = op w+{-# INLINE unarySomeIntN #-}++unarySomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n) -> SomeIntN -> SomeIntN+unarySomeIntNR1 op (SomeIntN (w :: IntN w)) = SomeIntN $ op w+{-# INLINE unarySomeIntNR1 #-}++binSomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> r) -> SomeIntN -> SomeIntN -> r+binSomeIntN op (SomeIntN (l :: IntN l)) (SomeIntN (r :: IntN r)) =+  case sameNat (Proxy @l) (Proxy @r) of+    Just Refl -> op l r+    Nothing -> throw BitwidthMismatch+{-# INLINE binSomeIntN #-}++binSomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> IntN n) -> SomeIntN -> SomeIntN -> SomeIntN+binSomeIntNR1 op (SomeIntN (l :: IntN l)) (SomeIntN (r :: IntN r)) =+  case sameNat (Proxy @l) (Proxy @r) of+    Just Refl -> SomeIntN $ op l r+    Nothing -> throw BitwidthMismatch+{-# INLINE binSomeIntNR1 #-}++binSomeIntNR2 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> (IntN n, IntN n)) -> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)+binSomeIntNR2 op (SomeIntN (l :: IntN l)) (SomeIntN (r :: IntN r)) =+  case sameNat (Proxy @l) (Proxy @r) of+    Just Refl ->+      case op l r of+        (a, b) -> (SomeIntN a, SomeIntN b)+    Nothing -> throw BitwidthMismatch+{-# INLINE binSomeIntNR2 #-}++instance Eq SomeIntN where+  (==) = binSomeIntN (==)+  {-# INLINE (==) #-}+  (/=) = binSomeIntN (/=)+  {-# INLINE (/=) #-}++instance Ord SomeIntN where+  (<=) = binSomeIntN (<=)+  {-# INLINE (<=) #-}+  (<) = binSomeIntN (<)+  {-# INLINE (<) #-}+  (>=) = binSomeIntN (>=)+  {-# INLINE (>=) #-}+  (>) = binSomeIntN (>)+  {-# INLINE (>) #-}+  max = binSomeIntNR1 max+  {-# INLINE max #-}+  min = binSomeIntNR1 min+  {-# INLINE min #-}+  compare = binSomeIntN compare+  {-# INLINE compare #-}++instance Lift SomeIntN where+  liftTyped (SomeIntN w) = [||SomeIntN w||]++instance Hashable SomeIntN where+  s `hashWithSalt` (SomeIntN (w :: IntN n)) = s `hashWithSalt` natVal (Proxy @n) `hashWithSalt` w++instance NFData SomeIntN where+  rnf (SomeIntN w) = rnf w++instance (KnownNat n, 1 <= n) => Show (IntN n) where+  show (IntN w) = if (bitwidth `mod` 4) == 0 then hexRepPre ++ hexRep else binRepPre ++ binRep+    where+      bitwidth = natVal (Proxy :: Proxy n)+      hexRepPre = "0x" ++ replicate (fromIntegral (bitwidth `div` 4) - length hexRep) '0'+      hexRep = showHex w ""+      binRepPre = "0b" ++ replicate (fromIntegral bitwidth - length binRep) '0'+      binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w ""++instance (KnownNat n, 1 <= n) => Read (IntN n) where+  readPrec = readNumber convertInt+  readListPrec = readListPrecDefault+  readList = readListDefault++instance Show SomeIntN where+  show (SomeIntN w) = show w++instance (KnownNat n, 1 <= n) => Bits (WordN n) where+  WordN a .&. WordN b = WordN (a .&. b)+  WordN a .|. WordN b = WordN (a .|. b)+  WordN a `xor` WordN b = WordN (a `xor` b)+  complement a = maxBound `xor` a++  -- shift use default implementation+  -- rotate use default implementation+  zeroBits = WordN 0+  bit i+    | i < 0 || i >= fromIntegral (natVal (Proxy :: Proxy n)) = zeroBits+    | otherwise = WordN (bit i)++  -- setBit use default implementation+  clearBit (WordN a) i = WordN (clearBit a i)++  -- complementBit use default implementation+  testBit (WordN a) = testBit a+  bitSizeMaybe _ = Just $ fromIntegral (natVal (Proxy :: Proxy n))+  bitSize _ = fromIntegral (natVal (Proxy :: Proxy n))+  isSigned _ = False+  shiftL (WordN a) i = WordN (a `shiftL` i) .&. maxBound++  -- unsafeShiftL use default implementation+  shiftR (WordN a) i = WordN (a `shiftR` i)++  -- unsafeShiftR use default implementation+  rotateL a 0 = a+  rotateL (WordN a) k+    | k >= n = rotateL (WordN a) (k `mod` n)+    | otherwise = WordN $ l + h+    where+      n = fromIntegral $ natVal (Proxy :: Proxy n)+      s = n - k+      l = a `shiftR` s+      h = (a - (l `shiftL` s)) `shiftL` k+  rotateR a 0 = a+  rotateR (WordN a) k+    | k >= n = rotateR (WordN a) (k `mod` n)+    | otherwise = WordN $ l + h+    where+      n = fromIntegral $ natVal (Proxy :: Proxy n)+      s = n - k+      l = a `shiftR` k+      h = (a - (l `shiftL` k)) `shiftL` s+  popCount (WordN n) = popCount n++instance Bits SomeWordN where+  (.&.) = binSomeWordNR1 (.&.)+  (.|.) = binSomeWordNR1 (.|.)+  xor = binSomeWordNR1 xor+  complement = unarySomeWordNR1 complement+  shift s i = unarySomeWordNR1 (`shift` i) s+  rotate s i = unarySomeWordNR1 (`rotate` i) s+  zeroBits = error "zeroBits is not defined for SomeWordN as no bitwidth is known"+  bit = error "bit is not defined for SomeWordN as no bitwidth is known"+  setBit s i = unarySomeWordNR1 (`setBit` i) s+  clearBit s i = unarySomeWordNR1 (`clearBit` i) s+  complementBit s i = unarySomeWordNR1 (`complementBit` i) s+  testBit s i = unarySomeWordN (`testBit` i) s+  bitSizeMaybe (SomeWordN (n :: WordN n)) = Just $ fromIntegral $ natVal n+  bitSize (SomeWordN (n :: WordN n)) = fromIntegral $ natVal n+  isSigned _ = False+  shiftL s i = unarySomeWordNR1 (`shiftL` i) s+  unsafeShiftL s i = unarySomeWordNR1 (`unsafeShiftL` i) s+  shiftR s i = unarySomeWordNR1 (`shiftR` i) s+  unsafeShiftR s i = unarySomeWordNR1 (`unsafeShiftR` i) s+  rotateL s i = unarySomeWordNR1 (`rotateL` i) s+  rotateR s i = unarySomeWordNR1 (`rotateR` i) s+  popCount = unarySomeWordN popCount++instance (KnownNat n, 1 <= n) => FiniteBits (WordN n) where+  finiteBitSize _ = fromIntegral (natVal (Proxy :: Proxy n))++instance FiniteBits SomeWordN where+  finiteBitSize (SomeWordN (n :: WordN n)) = fromIntegral $ natVal n+  countLeadingZeros = unarySomeWordN countLeadingZeros+  countTrailingZeros = unarySomeWordN countTrailingZeros++instance (KnownNat n, 1 <= n) => Bounded (WordN n) where+  maxBound = WordN ((1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n))) - 1)+  minBound = WordN 0++instance (KnownNat n, 1 <= n) => Enum (WordN n) where+  succ x+    | x /= maxBound = x + 1+    | otherwise = succError $ "WordN " ++ show (natVal (Proxy :: Proxy n))+  pred x+    | x /= minBound = x - 1+    | otherwise = predError $ "WordN " ++ show (natVal (Proxy :: Proxy n))+  toEnum i+    | i >= 0 && toInteger i <= toInteger (maxBound :: WordN n) = WordN (toInteger i)+    | otherwise = toEnumError ("WordN " ++ show (natVal (Proxy :: Proxy n))) i (minBound :: WordN n, maxBound :: WordN n)+  fromEnum (WordN n) = fromEnum n+  enumFrom = boundedEnumFrom+  {-# INLINE enumFrom #-}+  enumFromThen = boundedEnumFromThen+  {-# INLINE enumFromThen #-}++instance Enum SomeWordN where+  toEnum = error "SomeWordN is not really a Enum type as the bit width is unknown, please consider using WordN instead"+  fromEnum = error "SomeWordN is not really a Enum type as the bit width is unknown, please consider using WordN instead"++instance (KnownNat n, 1 <= n) => Real (WordN n) where+  toRational (WordN n) = n % 1++instance Real SomeWordN where+  toRational = unarySomeWordN toRational++instance (KnownNat n, 1 <= n) => Integral (WordN n) where+  quot (WordN x) (WordN y) = WordN (x `quot` y)+  rem (WordN x) (WordN y) = WordN (x `rem` y)+  quotRem (WordN x) (WordN y) = case quotRem x y of+    (q, r) -> (WordN q, WordN r)+  div = quot+  mod = rem+  divMod = quotRem+  toInteger (WordN n) = n++instance Integral SomeWordN where+  quot = binSomeWordNR1 quot+  rem = binSomeWordNR1 rem+  quotRem = binSomeWordNR2 quotRem+  div = binSomeWordNR1 div+  mod = binSomeWordNR1 mod+  divMod = binSomeWordNR2 divMod+  toInteger = unarySomeWordN toInteger++instance (KnownNat n, 1 <= n) => Num (WordN n) where+  WordN x + WordN y = WordN (x + y) .&. maxBound+  WordN x * WordN y = WordN (x * y) .&. maxBound+  WordN x - WordN y+    | x >= y = WordN (x - y)+    | otherwise = WordN ((1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n))) + x - y)+  negate (WordN 0) = WordN 0+  negate a = complement a + WordN 1+  abs x = x+  signum (WordN 0) = 0+  signum _ = 1+  fromInteger !x+    | x == 0 = WordN 0+    | x > 0 = WordN (x .&. unWordN (maxBound :: WordN n))+    | otherwise = -fromInteger (-x)++instance Num SomeWordN where+  (+) = binSomeWordNR1 (+)+  (-) = binSomeWordNR1 (-)+  (*) = binSomeWordNR1 (*)+  negate = unarySomeWordNR1 negate+  abs = unarySomeWordNR1 abs+  signum = unarySomeWordNR1 signum+  fromInteger = error "fromInteger is not defined for SomeWordN as no bitwidth is known"++minusOneIntN :: forall proxy n. KnownNat n => proxy n -> IntN n+minusOneIntN _ = IntN (1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n)) - 1)++instance (KnownNat n, 1 <= n) => Bits (IntN n) where+  IntN a .&. IntN b = IntN (a .&. b)+  IntN a .|. IntN b = IntN (a .|. b)+  IntN a `xor` IntN b = IntN (a `xor` b)+  complement a = minusOneIntN (Proxy :: Proxy n) `xor` a++  -- shift use default implementation+  -- rotate use default implementation+  zeroBits = IntN 0+  bit i = IntN (unWordN (bit i :: WordN n))++  -- setBit use default implementation+  clearBit (IntN a) i = IntN (clearBit a i)++  -- complementBit use default implementation+  testBit (IntN a) = testBit a+  bitSizeMaybe _ = Just $ fromIntegral (natVal (Proxy :: Proxy n))+  bitSize _ = fromIntegral (natVal (Proxy :: Proxy n))+  isSigned _ = True++  shiftL (IntN a) i = IntN (unWordN $ (WordN a :: WordN n) `shiftL` i)++  -- unsafeShiftL use default implementation+  shiftR i 0 = i+  shiftR (IntN i) k+    | k >= n = if b then IntN (maxi - 1) else IntN 0+    | otherwise = if b then IntN (maxi - noi + (i `shiftR` k)) else IntN (i `shiftR` k)+    where+      b = testBit i (n - 1)+      n = fromIntegral $ natVal (Proxy :: Proxy n)+      maxi = (1 :: Integer) `shiftL` n+      noi = (1 :: Integer) `shiftL` (n - k)++  -- unsafeShiftR use default implementation+  rotateL (IntN i) k = IntN $ unWordN $ rotateL (WordN i :: WordN n) k+  rotateR (IntN i) k = IntN $ unWordN $ rotateR (WordN i :: WordN n) k+  popCount (IntN i) = popCount i++instance Bits SomeIntN where+  (.&.) = binSomeIntNR1 (.&.)+  (.|.) = binSomeIntNR1 (.|.)+  xor = binSomeIntNR1 xor+  complement = unarySomeIntNR1 complement+  shift s i = unarySomeIntNR1 (`shift` i) s+  rotate s i = unarySomeIntNR1 (`rotate` i) s+  zeroBits = error "zeroBits is not defined for SomeIntN as no bitwidth is known"+  bit = error "bit is not defined for SomeIntN as no bitwidth is known"+  setBit s i = unarySomeIntNR1 (`setBit` i) s+  clearBit s i = unarySomeIntNR1 (`clearBit` i) s+  complementBit s i = unarySomeIntNR1 (`complementBit` i) s+  testBit s i = unarySomeIntN (`testBit` i) s+  bitSizeMaybe (SomeIntN (n :: IntN n)) = Just $ fromIntegral $ natVal n+  bitSize (SomeIntN (n :: IntN n)) = fromIntegral $ natVal n+  isSigned _ = False+  shiftL s i = unarySomeIntNR1 (`shiftL` i) s+  unsafeShiftL s i = unarySomeIntNR1 (`unsafeShiftL` i) s+  shiftR s i = unarySomeIntNR1 (`shiftR` i) s+  unsafeShiftR s i = unarySomeIntNR1 (`unsafeShiftR` i) s+  rotateL s i = unarySomeIntNR1 (`rotateL` i) s+  rotateR s i = unarySomeIntNR1 (`rotateR` i) s+  popCount = unarySomeIntN popCount++instance (KnownNat n, 1 <= n) => FiniteBits (IntN n) where+  finiteBitSize _ = fromIntegral (natVal (Proxy :: Proxy n))++instance FiniteBits SomeIntN where+  finiteBitSize (SomeIntN (n :: IntN n)) = fromIntegral $ natVal n+  countLeadingZeros = unarySomeIntN countLeadingZeros+  countTrailingZeros = unarySomeIntN countTrailingZeros++instance (KnownNat n, 1 <= n) => Bounded (IntN n) where+  maxBound = IntN (1 `shiftL` (fromIntegral (natVal (Proxy :: Proxy n)) - 1) - 1)+  minBound = maxBound + 1++instance (KnownNat n, 1 <= n) => Enum (IntN n) where+  succ x+    | x /= maxBound = x + 1+    | otherwise = succError $ "IntN " ++ show (natVal (Proxy :: Proxy n))+  pred x+    | x /= minBound = x - 1+    | otherwise = predError $ "IntN " ++ show (natVal (Proxy :: Proxy n))+  toEnum i+    | i >= fromIntegral (minBound :: IntN n) && i <= fromIntegral (maxBound :: IntN n) = fromIntegral i+    | otherwise = toEnumError ("IntN " ++ show (natVal (Proxy :: Proxy n))) i (minBound :: WordN n, maxBound :: WordN n)+  fromEnum = fromEnum . toInteger+  enumFrom = boundedEnumFrom+  {-# INLINE enumFrom #-}+  enumFromThen = boundedEnumFromThen+  {-# INLINE enumFromThen #-}++instance Enum SomeIntN where+  toEnum = error "SomeIntN is not really a Enum type as the bit width is unknown, please consider using IntN instead"+  fromEnum = error "SomeIntN is not really a Enum type as the bit width is unknown, please consider using IntN instead"++instance (KnownNat n, 1 <= n) => Real (IntN n) where+  toRational i = toInteger i % 1++instance Real SomeIntN where+  toRational = unarySomeIntN toRational++instance (KnownNat n, 1 <= n) => Integral (IntN n) where+  quot x y =+    if x == minBound && y == -1+      then throw Overflow+      else fromInteger (toInteger x `quot` toInteger y)+  rem x y = fromInteger (toInteger x `rem` toInteger y)+  quotRem x y =+    if x == minBound && y == -1+      then throw Overflow+      else case quotRem (toInteger x) (toInteger y) of+        (q, r) -> (fromInteger q, fromInteger r)+  div x y =+    if x == minBound && y == -1+      then throw Overflow+      else fromInteger (toInteger x `div` toInteger y)+  mod x y = fromInteger (toInteger x `mod` toInteger y)+  divMod x y =+    if x == minBound && y == -1+      then throw Overflow+      else case divMod (toInteger x) (toInteger y) of+        (q, r) -> (fromInteger q, fromInteger r)+  toInteger i@(IntN n) = case signum i of+    0 -> 0+    1 -> n+    -1 ->+      let x = negate i+       in if signum x == -1 then -n else negate (toInteger x)+    _ -> undefined++instance Integral SomeIntN where+  quot = binSomeIntNR1 quot+  rem = binSomeIntNR1 rem+  quotRem = binSomeIntNR2 quotRem+  div = binSomeIntNR1 div+  mod = binSomeIntNR1 mod+  divMod = binSomeIntNR2 divMod+  toInteger = unarySomeIntN toInteger++instance (KnownNat n, 1 <= n) => Num (IntN n) where+  IntN x + IntN y = IntN (x + y) .&. minusOneIntN (Proxy :: Proxy n)+  IntN x * IntN y = IntN (x * y) .&. minusOneIntN (Proxy :: Proxy n)+  IntN x - IntN y+    | x >= y = IntN (x - y)+    | otherwise = IntN ((1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n))) + x - y)+  negate (IntN 0) = IntN 0+  negate a = complement a + IntN 1+  abs x = if testBit x (fromIntegral $ natVal (Proxy :: Proxy n) - 1) then negate x else x+  signum (IntN 0) = IntN 0+  signum i = if testBit i (fromIntegral $ natVal (Proxy :: Proxy n) - 1) then -1 else 1+  fromInteger !x = IntN $ if v >= 0 then v else (1 `shiftL` n) + v+    where+      v = unWordN (fromInteger (x + maxn) :: WordN n) - maxn+      n = fromIntegral (natVal (Proxy :: Proxy n))+      maxn = 1 `shiftL` (n - 1) - 1++instance Num SomeIntN where+  (+) = binSomeIntNR1 (+)+  (-) = binSomeIntNR1 (-)+  (*) = binSomeIntNR1 (*)+  negate = unarySomeIntNR1 negate+  abs = unarySomeIntNR1 abs+  signum = unarySomeIntNR1 signum+  fromInteger = error "fromInteger is not defined for SomeIntN as no bitwidth is known"++instance (KnownNat n, 1 <= n) => Ord (IntN n) where+  IntN a <= IntN b+    | as && not bs = True+    | not as && bs = False+    | otherwise = a <= b+    where+      n = fromIntegral (natVal (Proxy :: Proxy n))+      as = testBit a (n - 1)+      bs = testBit b (n - 1)++instance SizedBV WordN where+  sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)+  sizedBVConcat (WordN a) (WordN b) = WordN ((a `shiftL` fromIntegral (natVal (Proxy :: Proxy r))) .|. b)+  sizedBVZext _ (WordN v) = WordN v+  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r+  sizedBVSext pr (WordN v) = if s then WordN (maxi - noi + v) else WordN v+    where+      r = fromIntegral $ natVal pr+      l = fromIntegral $ natVal (Proxy :: Proxy l)+      s = testBit v (l - 1)+      maxi = (1 :: Integer) `shiftL` r+      noi = (1 :: Integer) `shiftL` l+  sizedBVExt = sizedBVZext+  sizedBVSelect ::+    forall n ix w proxy.+    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>+    proxy ix ->+    proxy w ->+    WordN n ->+    WordN w+  sizedBVSelect pix pw (WordN v) = WordN ((v `shiftR` ix) .&. mask)+    where+      ix = fromIntegral $ natVal pix+      w = fromIntegral $ natVal pw+      mask = (1 `shiftL` w) - 1++instance SizedBV IntN where+  sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r)+  sizedBVConcat (IntN a) (IntN b) = IntN $ unWordN $ sizedBVConcat (WordN a :: WordN l) (WordN b :: WordN r)+  sizedBVZext _ (IntN v) = IntN v+  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r+  sizedBVSext pr (IntN v) = IntN $ unWordN $ sizedBVSext pr (WordN v :: WordN l)+  sizedBVExt = sizedBVSext+  sizedBVSelect ::+    forall n ix w proxy.+    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>+    proxy ix ->+    proxy w ->+    IntN n ->+    IntN w+  sizedBVSelect pix pw (IntN v) = IntN $ unWordN $ sizedBVSelect pix pw (WordN v :: WordN n)++instance SomeBV SomeWordN where+  someBVConcat (SomeWordN (a :: WordN l)) (SomeWordN (b :: WordN r)) =+    case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of+      (LeqProof, KnownProof) ->+        SomeWordN $ sizedBVConcat a b+  someBVZext (p :: p l) (SomeWordN (a :: WordN n))+    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"+    | otherwise =+        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of+          (LeqProof, LeqProof) -> SomeWordN $ sizedBVZext p a+    where+      l = natVal p+      n = natVal (Proxy @n)+  someBVSext (p :: p l) (SomeWordN (a :: WordN n))+    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"+    | otherwise =+        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of+          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSext p a+    where+      l = natVal p+      n = natVal (Proxy @n)+  someBVExt = someBVZext+  someBVSelect (p :: p ix) (q :: q w) (SomeWordN (a :: WordN n))+    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"+    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"+    | otherwise =+        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of+          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a+    where+      ix = natVal p+      w = natVal q+      n = natVal (Proxy @n)++instance SomeBV SomeIntN where+  someBVConcat (SomeIntN (a :: IntN l)) (SomeIntN (b :: IntN r)) =+    case (leqAddPos (Proxy @l) (Proxy @r), knownAdd (KnownProof @l) (KnownProof @r)) of+      (LeqProof, KnownProof) ->+        SomeIntN $ sizedBVConcat a b+  someBVZext (p :: p l) (SomeIntN (a :: IntN n))+    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"+    | otherwise =+        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of+          (LeqProof, LeqProof) -> SomeIntN $ sizedBVZext p a+    where+      l = natVal p+      n = natVal (Proxy @n)+  someBVSext (p :: p l) (SomeIntN (a :: IntN n))+    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"+    | otherwise =+        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of+          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSext p a+    where+      l = natVal p+      n = natVal (Proxy @n)+  someBVExt = someBVZext+  someBVSelect (p :: p ix) (q :: q w) (SomeIntN (a :: IntN n))+    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"+    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"+    | otherwise =+        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of+          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSelect (Proxy @ix) (Proxy @w) a+    where+      ix = natVal p+      w = natVal q+      n = natVal (Proxy @n)

@@ -1,7 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -19,110 +19,318 @@ -- Portability :   GHC only module Grisette.Core.Data.Class.BitVector   ( -- * Bit vector operations-    BVConcat (..),-    BVExtend (..),-    BVSelect (..),-    bvextract,+    SomeBV (..),+    someBVZext',+    someBVSext',+    someBVExt',+    someBVSelect',+    someBVExtract,+    someBVExtract',+    SizedBV (..),+    sizedBVExtract,   ) where  import Data.Proxy import GHC.TypeNats+import Grisette.Utils.Parameterized  -- $setup -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim+-- >>> import Grisette.Utils.Parameterized -- >>> :set -XDataKinds -- >>> :set -XBinaryLiterals -- >>> :set -XFlexibleContexts -- >>> :set -XFlexibleInstances -- >>> :set -XFunctionalDependencies --- | Bitwise concatenation ('bvconcat') of the given bit vector values.-class BVConcat bv1 bv2 bv3 | bv1 bv2 -> bv3 where-  -- | Bitwise concatenation of the given bit vector values.+-- | Bit vector operations. Including concatenation ('someBVConcat'),+-- extension ('someBVZext', 'someBVSext', 'someBVExt'), and selection+-- ('someBVSelect').+class SomeBV bv where+  -- | Concatenation of two bit vectors.   ---  -- >>> bvconcat (0b101 :: SymIntN 3) (0b010 :: SymIntN 3)+  -- >>> someBVConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))   -- 0b101010-  bvconcat :: bv1 -> bv2 -> bv3+  someBVConcat :: bv -> bv -> bv --- | Bitwise extension of the given bit vector values.-class BVExtend bv1 (n :: Nat) bv2 | bv1 n -> bv2 where-  -- | Bitwise zero extension of the given bit vector values.+  -- | Zero extension of a bit vector.   ---  -- >>> bvzeroExtend (Proxy @6) (0b101 :: SymIntN 3)+  -- >>> someBVZext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))   -- 0b000101-  bvzeroExtend ::+  someBVZext ::+    forall p l.+    KnownNat l =>+    -- | Desired output length+    p l ->+    -- | Bit vector to extend+    bv ->+    bv++  -- | Sign extension of a bit vector.+  --+  -- >>> someBVSext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))+  -- 0b111101+  someBVSext ::+    forall p l.+    KnownNat l =>+    -- | Desired output length+    p l ->+    -- | Bit vector to extend+    bv ->+    bv++  -- | Extension of a bit vector.+  -- Signedness is determined by the input bit vector type.+  --+  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b101 :: SymIntN 3))+  -- 0b111101+  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b001 :: SymIntN 3))+  -- 0b000001+  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))+  -- 0b000101+  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b001 :: SymWordN 3))+  -- 0b000001+  someBVExt ::+    forall p l.+    KnownNat l =>+    -- | Desired output length+    p l ->+    -- | Bit vector to extend+    bv ->+    bv++  -- | Slicing out a smaller bit vector from a larger one,+  -- selecting a slice with width @w@ starting from index @ix@.+  --+  -- The least significant bit is indexed as 0.+  --+  -- >>> someBVSelect (Proxy @1) (Proxy @3) (SomeSymIntN (0b001010 :: SymIntN 6))+  -- 0b101+  someBVSelect ::+    forall p ix q w.+    (KnownNat ix, KnownNat w) =>+    -- | Index of the least significant bit of the slice+    p ix ->+    -- | Desired output width, @ix + w <= n@ must hold where @n@ is+    -- the size of the input bit vector+    q w ->+    -- | Bit vector to select from+    bv ->+    bv++-- | Zero extension of a bit vector.+--+-- >>> someBVZext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))+-- 0b000101+someBVZext' ::+  forall l bv.+  SomeBV bv =>+  -- | Desired output length+  NatRepr l ->+  -- | Bit vector to extend+  bv ->+  bv+someBVZext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVZext (Proxy @l)+{-# INLINE someBVZext' #-}++-- | Sign extension of a bit vector.+--+-- >>> someBVSext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))+-- 0b111101+someBVSext' ::+  forall l bv.+  SomeBV bv =>+  NatRepr l ->+  -- | Desired output length+  bv ->+  -- | Bit vector to extend+  bv+someBVSext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVSext (Proxy @l)+{-# INLINE someBVSext' #-}++-- | Extension of a bit vector.+-- Signedness is determined by the input bit vector type.+--+-- >>> someBVExt' (natRepr @6) (SomeSymIntN (0b101 :: SymIntN 3))+-- 0b111101+-- >>> someBVExt' (natRepr @6) (SomeSymIntN (0b001 :: SymIntN 3))+-- 0b000001+-- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))+-- 0b000101+-- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b001 :: SymWordN 3))+-- 0b000001+someBVExt' ::+  forall l bv.+  SomeBV bv =>+  -- | Desired output length+  NatRepr l ->+  -- | Bit vector to extend+  bv ->+  bv+someBVExt' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVExt (Proxy @l)+{-# INLINE someBVExt' #-}++-- | Slicing out a smaller bit vector from a larger one,+-- selecting a slice with width @w@ starting from index @ix@.+--+-- The least significant bit is indexed as 0.+--+-- >>> someBVSelect' (natRepr @1) (natRepr @3) (SomeSymIntN (0b001010 :: SymIntN 6))+-- 0b101+someBVSelect' ::+  forall ix w bv.+  SomeBV bv =>+  -- | Index of the least significant bit of the slice+  NatRepr ix ->+  -- | Desired output width, @ix + w <= n@ must hold where @n@ is+  -- the size of the input bit vector+  NatRepr w ->+  -- | Bit vector to select from+  bv ->+  bv+someBVSelect' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVSelect p q+{-# INLINE someBVSelect' #-}++-- | Slicing out a smaller bit vector from a larger one, extract a slice from+-- bit @i@ down to @j@.+--+-- The least significant bit is indexed as 0.+--+-- >>> someBVExtract (Proxy @4) (Proxy @2) (SomeSymIntN (0b010100 :: SymIntN 6))+-- 0b101+someBVExtract ::+  forall p (i :: Nat) q (j :: Nat) bv.+  (SomeBV bv, KnownNat i, KnownNat j) =>+  -- | The start position to extract from, @i < n@ must hold where @n@ is+  -- the size of the output bit vector+  p i ->+  -- | The end position to extract from, @j <= i@ must hold+  q j ->+  -- | Bit vector to extract from+  bv ->+  bv+someBVExtract _ _ =+  withKnownProof (unsafeKnownProof @(i - j + 1) (fromIntegral (natVal (Proxy @i)) - fromIntegral (natVal (Proxy @j)) + 1)) $+    someBVSelect (Proxy @j) (Proxy @(i - j + 1))+{-# INLINE someBVExtract #-}++-- | Slicing out a smaller bit vector from a larger one, extract a slice from+-- bit @i@ down to @j@.+--+-- The least significant bit is indexed as 0.+--+-- >>> someBVExtract' (natRepr @4) (natRepr @2) (SomeSymIntN (0b010100 :: SymIntN 6))+-- 0b101+someBVExtract' ::+  forall (i :: Nat) (j :: Nat) bv.+  SomeBV bv =>+  -- | The start position to extract from, @i < n@ must hold where @n@ is+  -- the size of the output bit vector+  NatRepr i ->+  -- | The end position to extract from, @j <= i@ must hold+  NatRepr j ->+  -- | Bit vector to extract from+  bv ->+  bv+someBVExtract' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVExtract p q+{-# INLINE someBVExtract' #-}++-- | Sized bit vector operations. Including concatenation ('sizedBVConcat'),+-- extension ('sizedBVZext', 'sizedBVSext', 'sizedBVExt'), and selection+-- ('sizedBVSelect').+class SizedBV bv where+  -- | Concatenation of two bit vectors.+  --+  -- >>> sizedBVConcat (0b101 :: SymIntN 3) (0b010 :: SymIntN 3)+  -- 0b101010+  sizedBVConcat :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => bv l -> bv r -> bv (l + r)++  -- | Zero extension of a bit vector.+  --+  -- >>> sizedBVZext (Proxy @6) (0b101 :: SymIntN 3)+  -- 0b000101+  sizedBVZext ::+    (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>     -- | Desired output width-    proxy n ->+    proxy r ->     -- | Bit vector to extend-    bv1 ->-    bv2+    bv l ->+    bv r -  -- | Bitwise signed extension of the given bit vector values.+  -- | Signed extension of a bit vector.   ---  -- >>> bvsignExtend (Proxy @6) (0b101 :: SymIntN 3)+  -- >>> sizedBVSext (Proxy @6) (0b101 :: SymIntN 3)   -- 0b111101-  bvsignExtend ::+  sizedBVSext ::+    (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>     -- | Desired output width-    proxy n ->+    proxy r ->     -- | Bit vector to extend-    bv1 ->-    bv2+    bv l ->+    bv r -  -- | Bitwise extension of the given bit vector values.+  -- | Extension of a bit vector.   -- Signedness is determined by the input bit vector type.   ---  -- >>> bvextend (Proxy @6) (0b101 :: SymIntN 3)+  -- >>> sizedBVExt (Proxy @6) (0b101 :: SymIntN 3)   -- 0b111101-  -- >>> bvextend (Proxy @6) (0b001 :: SymIntN 3)+  -- >>> sizedBVExt (Proxy @6) (0b001 :: SymIntN 3)   -- 0b000001-  -- >>> bvextend (Proxy @6) (0b101 :: SymWordN 3)+  -- >>> sizedBVExt (Proxy @6) (0b101 :: SymWordN 3)   -- 0b000101-  -- >>> bvextend (Proxy @6) (0b001 :: SymWordN 3)+  -- >>> sizedBVExt (Proxy @6) (0b001 :: SymWordN 3)   -- 0b000001-  bvextend ::+  sizedBVExt ::+    (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>     -- | Desired output width-    proxy n ->+    proxy r ->     -- | Bit vector to extend-    bv1 ->-    bv2+    bv l ->+    bv r --- | Slicing out a smaller bit vector from a larger one, selecting a slice with--- width @w@ starting from index @ix@.-class BVSelect bv1 (ix :: Nat) (w :: Nat) bv2 | bv1 w -> bv2 where   -- | Slicing out a smaller bit vector from a larger one, selecting a slice with   -- width @w@ starting from index @ix@.   ---  -- The indices are counting from zero from the least significant bit.+  -- The least significant bit is indexed as 0.   ---  -- >>> bvselect (Proxy @1) (Proxy @3) (con 0b001010 :: SymIntN 6)+  -- >>> sizedBVSelect (Proxy @2) (Proxy @3) (con 0b010100 :: SymIntN 6)   -- 0b101-  bvselect ::-    -- | Index to start selecting from+  sizedBVSelect ::+    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>+    -- | Index of the least significant bit of the slice     proxy ix ->-    -- | Desired output width, @0 <= ix@ and @ix + w < n@ must hold where @n@ is+    -- | Desired output width, @ix + w <= n@ must hold where @n@ is     -- the size of the input bit vector     proxy w ->     -- | Bit vector to select from-    bv1 ->-    bv2+    bv n ->+    bv w --- | Extract a smaller bit vector from a larger one from bits @i@ down to @j@.+-- | Slicing out a smaller bit vector from a larger one, extract a slice from+-- bit @i@ down to @j@. ----- The indices are counting from zero from the least significant bit.--- >>> bvextract (Proxy @3) (Proxy @1) (con 0b001010 :: SymIntN 6)+-- The least significant bit is indexed as 0.+--+-- >>> sizedBVExtract (Proxy @4) (Proxy @2) (con 0b010100 :: SymIntN 6) -- 0b101-bvextract ::-  forall proxy i j bv1 bv2.-  (BVSelect bv1 j (i - j + 1) bv2) =>-  -- | The start position to extract from, @0 <= i < n@ must hold where @n@ is+sizedBVExtract ::+  forall proxy i j n bv.+  (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, i + 1 <= n, j <= i) =>+  -- | The start position to extract from, @i < n@ must hold where @n@ is   -- the size of the output bit vector   proxy i ->-  -- | The end position to extract from, @0 <= j <= i@ must hold+  -- | The end position to extract from, @j <= i@ must hold   proxy j ->   -- | Bit vector to extract from-  bv1 ->-  bv2-bvextract _ _ = bvselect (Proxy @j) (Proxy @(i - j + 1))-{-# INLINE bvextract #-}+  bv n ->+  bv (i - j + 1)+sizedBVExtract _ _ =+  case ( hasRepr (addNat (subNat (natRepr @i) (natRepr @j)) (natRepr @1)),+         unsafeLeqProof @(j + (i - j + 1)) @n,+         unsafeLeqProof @1 @(i - j + 1)+       ) of+    (KnownProof, LeqProof, LeqProof) ->+      sizedBVSelect (Proxy @j) (Proxy @(i - j + 1))+{-# INLINE sizedBVExtract #-}

@@ -1,7 +1,9 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE Trustworthy #-}@@ -40,7 +42,9 @@ import Data.Functor.Sum import Data.Int import Data.Word+import GHC.TypeNats import Generics.Deriving+import Grisette.Core.Data.BV import {-# SOURCE #-} Grisette.Core.Data.Class.SimpleMergeable import Grisette.Core.Data.Class.Solvable import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term@@ -220,6 +224,11 @@   l ==~ r = con $ l == r; \   {-# INLINE (==~) #-} +#define CONCRETE_SEQ_BV(type) \+instance (KnownNat n, 1 <= n) => SEq (type n) where \+  l ==~ r = con $ l == r; \+  {-# INLINE (==~) #-}+ #if 1 CONCRETE_SEQ(Bool) CONCRETE_SEQ(Integer)@@ -235,6 +244,10 @@ CONCRETE_SEQ(Word32) CONCRETE_SEQ(Word64) CONCRETE_SEQ(B.ByteString)+CONCRETE_SEQ_BV(WordN)+CONCRETE_SEQ_BV(IntN)+CONCRETE_SEQ(SomeWordN)+CONCRETE_SEQ(SomeIntN) #endif  -- List@@ -327,12 +340,40 @@   (IdentityT l) ==~ (IdentityT r) = l ==~ r   {-# INLINE (==~) #-} -instance (SupportedPrim a) => ITEOp (Sym a) where-  ites (Sym c) (Sym t) (Sym f) = Sym $ pevalITETerm c t f+#define ITEOP_SIMPLE(type) \+instance ITEOp type where \+  ites (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \+  {-# INLINE ites #-} -instance LogicalOp (Sym Bool) where-  (Sym l) ||~ (Sym r) = Sym $ pevalOrTerm l r-  (Sym l) &&~ (Sym r) = Sym $ pevalAndTerm l r-  nots (Sym v) = Sym $ pevalNotTerm v-  (Sym l) `xors` (Sym r) = Sym $ pevalXorTerm l r-  (Sym l) `implies` (Sym r) = Sym $ pevalImplyTerm l r+#define ITEOP_BV(type) \+instance (KnownNat n, 1 <= n) => ITEOp (type n) where \+  ites (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \+  {-# INLINE ites #-}++#define ITEOP_BV_SOME(symtype, bf) \+instance ITEOp symtype where \+  ites c = bf (ites c) "ites"; \+  {-# INLINE ites #-}++#define ITEOP_FUN(op, cons) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa op sb) where \+  ites (SymBool c) (cons t) (cons f) = cons $ pevalITETerm c t f; \+  {-# INLINE ites #-}++#if 1+ITEOP_SIMPLE(SymBool)+ITEOP_SIMPLE(SymInteger)+ITEOP_BV(SymIntN)+ITEOP_BV(SymWordN)+ITEOP_BV_SOME(SomeSymIntN, binSomeSymIntNR1)+ITEOP_BV_SOME(SomeSymWordN, binSomeSymWordNR1)+ITEOP_FUN(=~>, SymTabularFun)+ITEOP_FUN(-~>, SymGeneralFun)+#endif++instance LogicalOp SymBool where+  (SymBool l) ||~ (SymBool r) = SymBool $ pevalOrTerm l r+  (SymBool l) &&~ (SymBool r) = SymBool $ pevalAndTerm l r+  nots (SymBool v) = SymBool $ pevalNotTerm v+  (SymBool l) `xors` (SymBool r) = SymBool $ pevalXorTerm l r+  (SymBool l) `implies` (SymBool r) = SymBool $ pevalImplyTerm l r

@@ -1,5 +1,7 @@ module Grisette.Core.Data.Class.Bool (LogicalOp (..)) where +import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+ class LogicalOp b where   -- | Symbolic disjunction   (||~) :: b -> b -> b@@ -29,3 +31,6 @@   {-# INLINE implies #-}    {-# MINIMAL (||~), nots | (&&~), nots #-}++class ITEOp v where+  ites :: SymBool -> v -> v -> v

@@ -124,7 +124,7 @@     -- | The counter-examples generated     -- during the CEGIS loop, and the     -- model found by the solver.-    IO (Either failure ([inputs], Model))+    IO ([inputs], Either failure Model)  -- | -- CEGIS with a single symbolic input to represent a set of inputs.@@ -135,8 +135,8 @@ -- -- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger]--- >>> cegis (UnboundedReasoning z3) x (cegisPrePost (x >~ 0) (x * c <~ 0 &&~ c >~ -2))--- Right ([],Model {c -> -1 :: Integer})+-- >>> cegis (precise z3) x (cegisPrePost (x >~ 0) (x * c <~ 0 &&~ c >~ -2))+-- ([],Right (Model {c -> -1 :: Integer})) cegis ::   ( CEGISSolver config failure,     EvaluateSym inputs,@@ -155,7 +155,7 @@   -- | The counter-examples generated   -- during the CEGIS loop, and the   -- model found by the solver.-  IO (Either failure ([inputs], Model))+  IO ([inputs], Either failure Model) cegis config inputs cond = cegisMultiInputs config [inputs] (const cond)  -- |@@ -173,7 +173,7 @@   [inputs] ->   (Either e v -> CEGISCondition) ->   (inputs -> t) ->-  IO (Either failure ([inputs], Model))+  IO ([inputs], Either failure Model) cegisExceptMultiInputs config cexes interpretFun f =   cegisMultiInputs config cexes (simpleMerge . (interpretFun <$>) . extractUnionExcept . f) @@ -194,7 +194,7 @@   [inputs] ->   (Either e v -> u (Either VerificationConditions ())) ->   (inputs -> t) ->-  IO (Either failure ([inputs], Model))+  IO ([inputs], Either failure Model) cegisExceptVCMultiInputs config cexes interpretFun f =   cegisMultiInputs     config@@ -230,7 +230,7 @@   config ->   [inputs] ->   (inputs -> t) ->-  IO (Either failure ([inputs], Model))+  IO ([inputs], Either failure Model) cegisExceptStdVCMultiInputs config cexes =   cegisExceptVCMultiInputs config cexes return @@ -264,8 +264,8 @@ --   translation _ = cegisPostCond (con True) -- :} ----- >>> cegisExcept (UnboundedReasoning z3) x translation res--- Right ([],Model {c -> -1 :: Integer})+-- >>> cegisExcept (precise z3) x translation res+-- ([],Right (Model {c -> -1 :: Integer})) cegisExcept ::   ( UnionWithExcept t u e v,     UnionPrjOp u,@@ -278,7 +278,7 @@   inputs ->   (Either e v -> CEGISCondition) ->   t ->-  IO (Either failure ([inputs], Model))+  IO ([inputs], Either failure Model) cegisExcept config inputs f v = cegis config inputs $ simpleMerge $ f <$> extractUnionExcept v  -- |@@ -298,7 +298,7 @@   inputs ->   (Either e v -> u (Either VerificationConditions ())) ->   t ->-  IO (Either failure ([inputs], Model))+  IO ([inputs], Either failure Model) cegisExceptVC config inputs f v =   cegis config inputs $     simpleMerge $@@ -334,8 +334,8 @@ --     symAssert $ c >~ -2 -- :} ----- >>> cegisExceptStdVC (UnboundedReasoning z3) x res--- Right ([],Model {c -> -1 :: Integer})+-- >>> cegisExceptStdVC (precise z3) x res+-- ([],Right (Model {c -> -1 :: Integer})) cegisExceptStdVC ::   ( UnionWithExcept t u VerificationConditions (),     UnionPrjOp u,@@ -347,5 +347,5 @@   config ->   inputs ->   t ->-  IO (Either failure ([inputs], Model))+  IO ([inputs], Either failure Model) cegisExceptStdVC config inputs = cegisExceptVC config inputs return

@@ -15,6 +15,7 @@     TransformError (..),      -- * Throwing error+    symAssertWith,     symAssertTransformableError,     symThrowTransformableError,   )@@ -104,3 +105,14 @@   erm () symAssertTransformableError err cond = mrgIf cond (return ()) (symThrowTransformableError err) {-# INLINE symAssertTransformableError #-}++symAssertWith ::+  ( Mergeable e,+    MonadError e erm,+    MonadUnion erm+  ) =>+  e ->+  SymBool ->+  erm ()+symAssertWith err cond = mrgIf cond (return ()) (throwError err)+{-# INLINE symAssertWith #-}

@@ -1,7 +1,9 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE Trustworthy #-}@@ -33,8 +35,10 @@ import Data.Int import Data.Maybe import Data.Word+import GHC.TypeNats import Generics.Deriving import Generics.Deriving.Instances ()+import Grisette.Core.Data.BV import Grisette.Core.Data.Class.ModelOps import Grisette.Core.Data.Class.ToCon import Grisette.IR.SymPrim.Data.Prim.Model@@ -102,6 +106,10 @@ instance EvaluateSym type where \   evaluateSym _ _ = id +#define CONCRETE_EVALUATESYM_BV(type) \+instance (KnownNat n, 1 <= n) => EvaluateSym (type n) where \+  evaluateSym _ _ = id+ #if 1 CONCRETE_EVALUATESYM(Bool) CONCRETE_EVALUATESYM(Integer)@@ -116,7 +124,11 @@ CONCRETE_EVALUATESYM(Word16) CONCRETE_EVALUATESYM(Word32) CONCRETE_EVALUATESYM(Word64)+CONCRETE_EVALUATESYM(SomeIntN)+CONCRETE_EVALUATESYM(SomeWordN) CONCRETE_EVALUATESYM(B.ByteString)+CONCRETE_EVALUATESYM_BV(IntN)+CONCRETE_EVALUATESYM_BV(WordN) #endif  -- ()

@@ -1,7 +1,9 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE Trustworthy #-}@@ -31,7 +33,9 @@ import Data.Functor.Sum import Data.Int import Data.Word+import GHC.TypeNats import Generics.Deriving+import Grisette.Core.Data.BV import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.Model  -- $setup@@ -87,9 +91,13 @@ -- instances  #define CONCRETE_EXTRACT_SYMBOLICS(type) \-instance  ExtractSymbolics type where \+instance ExtractSymbolics type where \   extractSymbolics _ = mempty +#define CONCRETE_EXTRACT_SYMBOLICS_BV(type) \+instance (KnownNat n, 1 <= n) => ExtractSymbolics (type n) where \+  extractSymbolics _ = mempty+ #if 1 CONCRETE_EXTRACT_SYMBOLICS(Bool) CONCRETE_EXTRACT_SYMBOLICS(Integer)@@ -104,7 +112,11 @@ CONCRETE_EXTRACT_SYMBOLICS(Word16) CONCRETE_EXTRACT_SYMBOLICS(Word32) CONCRETE_EXTRACT_SYMBOLICS(Word64)+CONCRETE_EXTRACT_SYMBOLICS(SomeWordN)+CONCRETE_EXTRACT_SYMBOLICS(SomeIntN) CONCRETE_EXTRACT_SYMBOLICS(B.ByteString)+CONCRETE_EXTRACT_SYMBOLICS_BV(WordN)+CONCRETE_EXTRACT_SYMBOLICS_BV(IntN) #endif  -- ()

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-}@@ -65,10 +66,21 @@ where  import Control.DeepSeq+import Control.Monad.Cont import Control.Monad.Except import Control.Monad.Identity+import Control.Monad.RWS.Class+import qualified Control.Monad.RWS.Lazy as RWSLazy+import qualified Control.Monad.RWS.Strict as RWSStrict+import Control.Monad.Reader import Control.Monad.Signatures+import Control.Monad.State+import qualified Control.Monad.State.Lazy as StateLazy+import qualified Control.Monad.State.Strict as StateStrict import Control.Monad.Trans.Maybe+import Control.Monad.Writer+import qualified Control.Monad.Writer.Lazy as WriterLazy+import qualified Control.Monad.Writer.Strict as WriterStrict import Data.Bifunctor import qualified Data.ByteString as B import Data.Hashable@@ -76,9 +88,11 @@ import Data.String import Data.Typeable import Data.Word+import GHC.TypeNats import Generics.Deriving hiding (index) import Grisette.Core.Control.Monad.Union import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM+import Grisette.Core.Data.BV import Grisette.Core.Data.Class.Bool import Grisette.Core.Data.Class.Mergeable import Grisette.Core.Data.Class.SimpleMergeable@@ -287,6 +301,53 @@   throwError = lift . throwError   catchError = liftFreshTCache catchError +instance (MonadWriter w m) => MonadWriter w (FreshT m) where+  writer p = FreshT $ \ident index -> (,index) <$> writer p+  listen (FreshT r) = FreshT $ \ident index -> (\((a, b), c) -> ((a, c), b)) <$> listen (r ident index)+  pass (FreshT r) = FreshT $ \ident index -> pass $ (\((a, b), c) -> ((a, c), b)) <$> r ident index++instance (MonadState s m) => MonadState s (FreshT m) where+  get = FreshT $ \ident index -> gets (,index)+  put s = FreshT $ \ident index -> (,index) <$> put s++instance (MonadReader r m) => MonadReader r (FreshT m) where+  local t (FreshT r) = FreshT $ \ident index -> local t (r ident index)+  ask = FreshT $ \ident index -> asks (,index)++instance (MonadRWS r w s m) => MonadRWS r w s (FreshT m)++instance (MonadFresh m) => MonadFresh (ExceptT e m) where+  nextFreshIndex = ExceptT $ Right <$> nextFreshIndex+  getFreshIdent = ExceptT $ Right <$> getFreshIdent++instance (MonadFresh m, Monoid w) => MonadFresh (WriterLazy.WriterT w m) where+  nextFreshIndex = WriterLazy.WriterT $ (,mempty) <$> nextFreshIndex+  getFreshIdent = WriterLazy.WriterT $ (,mempty) <$> getFreshIdent++instance (MonadFresh m, Monoid w) => MonadFresh (WriterStrict.WriterT w m) where+  nextFreshIndex = WriterStrict.WriterT $ (,mempty) <$> nextFreshIndex+  getFreshIdent = WriterStrict.WriterT $ (,mempty) <$> getFreshIdent++instance (MonadFresh m) => MonadFresh (StateLazy.StateT s m) where+  nextFreshIndex = StateLazy.StateT $ \s -> (,s) <$> nextFreshIndex+  getFreshIdent = StateLazy.StateT $ \s -> (,s) <$> getFreshIdent++instance (MonadFresh m) => MonadFresh (StateStrict.StateT s m) where+  nextFreshIndex = StateStrict.StateT $ \s -> (,s) <$> nextFreshIndex+  getFreshIdent = StateStrict.StateT $ \s -> (,s) <$> getFreshIdent++instance (MonadFresh m) => MonadFresh (ReaderT r m) where+  nextFreshIndex = ReaderT $ const nextFreshIndex+  getFreshIdent = ReaderT $ const getFreshIdent++instance (MonadFresh m, Monoid w) => MonadFresh (RWSLazy.RWST r w s m) where+  nextFreshIndex = RWSLazy.RWST $ \r s -> (,s,mempty) <$> nextFreshIndex+  getFreshIdent = RWSLazy.RWST $ \r s -> (,s,mempty) <$> getFreshIdent++instance (MonadFresh m, Monoid w) => MonadFresh (RWSStrict.RWST r w s m) where+  nextFreshIndex = RWSStrict.RWST $ \r s -> (,s,mempty) <$> nextFreshIndex+  getFreshIdent = RWSStrict.RWST $ \r s -> (,s,mempty) <$> getFreshIdent+ -- | 'FreshT' specialized with Identity. type Fresh = FreshT Identity @@ -449,7 +510,7 @@ -- use this 'fresh' implementation to implement 'GenSym' for your own types. -- -- This 'fresh' implementation is for the types that does not need any specification.--- It will generate product types by generating each fields with '()' as specification,+-- It will generate product types by generating each fields with @()@ as specification, -- and generate all possible values for a sum type. -- -- __Note:__ __Never__ use on recursive types.@@ -674,6 +735,12 @@ #define CONCRETE_GENSYMSIMPLE_SAME_SHAPE(type) \ instance GenSymSimple type type where simpleFresh = return +#define CONCRETE_GENSYM_SAME_SHAPE_BV(type) \+instance (KnownNat n, 1 <= n) => GenSym (type n) (type n) where fresh = return . mrgSingle++#define CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(type) \+instance (KnownNat n, 1 <= n) => GenSymSimple (type n) (type n) where simpleFresh = return+ #if 1 CONCRETE_GENSYM_SAME_SHAPE(Bool) CONCRETE_GENSYM_SAME_SHAPE(Integer)@@ -688,7 +755,11 @@ CONCRETE_GENSYM_SAME_SHAPE(Word16) CONCRETE_GENSYM_SAME_SHAPE(Word32) CONCRETE_GENSYM_SAME_SHAPE(Word64)+CONCRETE_GENSYM_SAME_SHAPE(SomeWordN)+CONCRETE_GENSYM_SAME_SHAPE(SomeIntN) CONCRETE_GENSYM_SAME_SHAPE(B.ByteString)+CONCRETE_GENSYM_SAME_SHAPE_BV(WordN)+CONCRETE_GENSYM_SAME_SHAPE_BV(IntN)  CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Bool) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Integer)@@ -703,7 +774,11 @@ CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word16) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word32) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word64)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeWordN)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeIntN) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(B.ByteString)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(WordN)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(IntN) #endif  -- Bool@@ -1457,18 +1532,105 @@   ) =>   GenSym (ExceptT e m a) (ExceptT e m a) -instance (SupportedPrim a) => GenSym (Sym a) (Sym a)--instance (SupportedPrim a) => GenSymSimple (Sym a) (Sym a) where+#define GENSYM_SIMPLE(symtype) \+instance GenSym symtype symtype+#define GENSYM_SIMPLE_SIMPLE(symtype) \+instance GenSymSimple symtype symtype where \   simpleFresh _ = simpleFresh ()+#define GENSYM_UNIT_SIMPLE(symtype) \+instance GenSym () symtype where \+  fresh _ = mrgSingle <$> simpleFresh ()+#define GENSYM_UNIT_SIMPLE_SIMPLE(symtype) \+instance GenSymSimple () symtype where \+  simpleFresh _ = do; \+    ident <- getFreshIdent; \+    FreshIndex i <- nextFreshIndex; \+    case ident of; \+      FreshIdent s -> return $ isym s i; \+      FreshIdentWithInfo s info -> return $ iinfosym s i info -instance (SupportedPrim a) => GenSym () (Sym a) where+#define GENSYM_BV(symtype) \+instance (KnownNat n, 1 <= n) => GenSym (symtype n) (symtype n)+#define GENSYM_SIMPLE_BV(symtype) \+instance (KnownNat n, 1 <= n) => GenSymSimple (symtype n) (symtype n) where \+  simpleFresh _ = simpleFresh ()+#define GENSYM_UNIT_BV(symtype) \+instance (KnownNat n, 1 <= n) => GenSym () (symtype n) where \   fresh _ = mrgSingle <$> simpleFresh ()+#define GENSYM_UNIT_SIMPLE_BV(symtype) \+instance (KnownNat n, 1 <= n) => GenSymSimple () (symtype n) where \+  simpleFresh _ = do; \+    ident <- getFreshIdent; \+    FreshIndex i <- nextFreshIndex; \+    case ident of; \+      FreshIdent s -> return $ isym s i; \+      FreshIdentWithInfo s info -> return $ iinfosym s i info -instance (SupportedPrim a) => GenSymSimple () (Sym a) where-  simpleFresh _ = do-    ident <- getFreshIdent-    FreshIndex i <- nextFreshIndex-    case ident of-      FreshIdent s -> return $ isym s i+#define GENSYM_BV_SOME(symtype) \+instance GenSym symtype symtype+#define GENSYM_SIMPLE_BV_SOME(symtype) \+instance GenSymSimple symtype symtype where \+  simpleFresh (symtype v) = simpleFresh v+#define GENSYM_N_BV_SOME(symtype) \+instance (KnownNat n, 1 <= n) => GenSym (p n) symtype where \+  fresh p = mrgSingle <$> simpleFresh p+#define GENSYM_N_SIMPLE_BV_SOME(symtype, origtype) \+instance (KnownNat n, 1 <= n) => GenSymSimple (p n) symtype where \+  simpleFresh _ = do; \+    i :: origtype n <- simpleFresh (); \+    return $ symtype i++#define GENSYM_FUN(op) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSym (sa op sb) (sa op sb)+#define GENSYM_SIMPLE_FUN(op) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple (sa op sb) (sa op sb) where \+  simpleFresh _ = simpleFresh ()+#define GENSYM_UNIT_FUN(op) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSym () (sa op sb) where \+  fresh _ = mrgSingle <$> simpleFresh ()+#define GENSYM_UNIT_SIMPLE_FUN(op) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple () (sa op sb) where \+  simpleFresh _ = do; \+    ident <- getFreshIdent; \+    FreshIndex i <- nextFreshIndex; \+    case ident of; \+      FreshIdent s -> return $ isym s i; \       FreshIdentWithInfo s info -> return $ iinfosym s i info++#if 1+GENSYM_SIMPLE(SymBool)+GENSYM_SIMPLE_SIMPLE(SymBool)+GENSYM_UNIT_SIMPLE(SymBool)+GENSYM_UNIT_SIMPLE_SIMPLE(SymBool)+GENSYM_SIMPLE(SymInteger)+GENSYM_SIMPLE_SIMPLE(SymInteger)+GENSYM_UNIT_SIMPLE(SymInteger)+GENSYM_UNIT_SIMPLE_SIMPLE(SymInteger)++GENSYM_BV(SymIntN)+GENSYM_SIMPLE_BV(SymIntN)+GENSYM_UNIT_BV(SymIntN)+GENSYM_UNIT_SIMPLE_BV(SymIntN)+GENSYM_BV(SymWordN)+GENSYM_SIMPLE_BV(SymWordN)+GENSYM_UNIT_BV(SymWordN)+GENSYM_UNIT_SIMPLE_BV(SymWordN)++GENSYM_BV_SOME(SomeSymIntN)+GENSYM_SIMPLE_BV_SOME(SomeSymIntN)+GENSYM_N_BV_SOME(SomeSymIntN)+GENSYM_N_SIMPLE_BV_SOME(SomeSymIntN, SymIntN)+GENSYM_BV_SOME(SomeSymWordN)+GENSYM_SIMPLE_BV_SOME(SomeSymWordN)+GENSYM_N_BV_SOME(SomeSymWordN)+GENSYM_N_SIMPLE_BV_SOME(SomeSymWordN, SymWordN)++GENSYM_FUN(=~>)+GENSYM_SIMPLE_FUN(=~>)+GENSYM_UNIT_FUN(=~>)+GENSYM_UNIT_SIMPLE_FUN(=~>)+GENSYM_FUN(-~>)+GENSYM_SIMPLE_FUN(-~>)+GENSYM_UNIT_FUN(-~>)+GENSYM_UNIT_SIMPLE_FUN(-~>)+#endif

@@ -1,72 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Trustworthy #-}---- |--- Module      :   Grisette.Core.Data.Class.Integer--- 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.Core.Data.Class.Integer-  ( -- * Symbolic integer operations-    ArithException (..),-    SignedDivMod (..),-    UnsignedDivMod (..),-    SignedQuotRem (..),-    SymIntegerOp,-  )-where--import Control.Exception-import Control.Monad.Except-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Error-import Grisette.Core.Data.Class.SOrd-import Grisette.Core.Data.Class.Solvable---- $setup--- >>> import Grisette.Core--- >>> import Grisette.IR.SymPrim---- | Safe signed 'div' and 'mod' with monadic error handling in multi-path--- execution. These procedures show throw 'DivideByZero' exception when the--- divisor is zero. The result should be able to handle errors with--- `MonadError`, and the error type should be compatible with 'ArithException'--- (see 'TransformError' for more details).-class SignedDivMod a where-  -- | Safe signed 'div' with monadic error handling in multi-path execution.-  ---  -- >>> divs (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymInteger-  -- ExceptT {If (= b 0) (Left AssertionError) (Right (div a b))}-  divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a--  -- | Safe signed 'mod' with monadic error handling in multi-path execution.-  ---  -- >>> mods (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymInteger-  -- ExceptT {If (= b 0) (Left AssertionError) (Right (mod a b))}-  mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a---- | Safe unsigned 'div' and 'mod' with monadic error handling in multi-path--- execution. These procedures show throw 'DivideByZero' exception when the--- divisor is zero. The result should be able to handle errors with--- `MonadError`, and the error type should be compatible with 'ArithException'--- (see 'TransformError' for more details).-class UnsignedDivMod a where-  udivs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a-  umods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a---- | Safe signed 'quot' and 'rem' with monadic error handling in multi-path--- execution. These procedures show throw 'DivideByZero' exception when the--- divisor is zero. The result should be able to handle errors with--- `MonadError`, and the error type should be compatible with 'ArithException'--- (see 'TransformError' for more details).-class SignedQuotRem a where-  quots :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a-  rems :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a---- | Aggregation for the operations on symbolic integer types-class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a

@@ -50,6 +50,7 @@   ) where +import Control.Exception import Control.Monad.Cont import Control.Monad.Except import Control.Monad.Identity@@ -69,7 +70,11 @@ import qualified Data.Monoid as Monoid import Data.Typeable import Data.Word+import GHC.Natural+import qualified GHC.TypeLits+import GHC.TypeNats import Generics.Deriving+import Grisette.Core.Data.BV import Grisette.Core.Data.Class.Bool import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim@@ -429,9 +434,14 @@ instance Mergeable type where \   rootStrategy = \     let sub = SimpleStrategy $ \_ t _ -> t \-     in SortedStrategy id $ const sub; \-  {-# INLINE rootStrategy #-}+     in SortedStrategy id $ const sub +#define CONCRETE_ORD_MERGEABLE_BV(type) \+instance (KnownNat n, 1 <= n) => Mergeable (type n) where \+  rootStrategy = \+    let sub = SimpleStrategy $ \_ t _ -> t \+     in SortedStrategy id $ const sub+ #if 1 CONCRETE_ORD_MERGEABLE(Bool) CONCRETE_ORD_MERGEABLE(Integer)@@ -447,8 +457,30 @@ CONCRETE_ORD_MERGEABLE(Word32) CONCRETE_ORD_MERGEABLE(Word64) CONCRETE_ORD_MERGEABLE(B.ByteString)+CONCRETE_ORD_MERGEABLE_BV(WordN)+CONCRETE_ORD_MERGEABLE_BV(IntN) #endif +instance Mergeable SomeIntN where+  rootStrategy =+    SortedStrategy @Natural+      (\(SomeIntN (v :: IntN n)) -> natVal (Proxy @n))+      ( \n ->+          SortedStrategy @Integer+            (\(SomeIntN (IntN i)) -> toInteger i)+            (const $ SimpleStrategy $ \_ l _ -> l)+      )++instance Mergeable SomeWordN where+  rootStrategy =+    SortedStrategy @Natural+      (\(SomeWordN (v :: WordN n)) -> natVal (Proxy @n))+      ( \n ->+          SortedStrategy @Integer+            (\(SomeWordN (WordN i)) -> toInteger i)+            (const $ SimpleStrategy $ \_ l _ -> l)+      )+ -- () deriving via (Default ()) instance Mergeable () @@ -935,5 +967,45 @@  deriving via (Default1 Monoid.Sum) instance Mergeable1 Monoid.Sum -instance (SupportedPrim a) => Mergeable (Sym a) where+#define MERGEABLE_SIMPLE(symtype) \+instance Mergeable symtype where \   rootStrategy = SimpleStrategy ites++#define MERGEABLE_BV(symtype) \+instance (KnownNat n, 1 <= n) => Mergeable (symtype n) where \+  rootStrategy = SimpleStrategy ites++#define MERGEABLE_BV_SOME(symtype) \+instance Mergeable symtype where \+  rootStrategy = SimpleStrategy ites++#define MERGEABLE_FUN(op) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa op sb) where \+  rootStrategy = SimpleStrategy ites++#if 1+MERGEABLE_SIMPLE(SymBool)+MERGEABLE_SIMPLE(SymInteger)+MERGEABLE_BV(SymIntN)+MERGEABLE_BV(SymWordN)+MERGEABLE_BV_SOME(SomeSymIntN)+MERGEABLE_BV_SOME(SomeSymWordN)+MERGEABLE_FUN(=~>)+MERGEABLE_FUN(-~>)+#endif++-- Exceptions+instance Mergeable ArithException where+  rootStrategy =+    SortedStrategy+      ( \case+          Overflow -> 0 :: Int+          Underflow -> 1 :: Int+          LossOfPrecision -> 2 :: Int+          DivideByZero -> 3 :: Int+          Denormal -> 4 :: Int+          RatioZeroDenominator -> 5 :: Int+      )+      (const $ SimpleStrategy $ \_ l r -> l)++deriving via (Default BitwidthMismatch) instance (Mergeable BitwidthMismatch)

@@ -130,6 +130,9 @@   -- | Check if the model is empty   isEmptyModel :: model -> Bool +  -- | Check if the model contains the given symbol+  modelContains :: typedSymbol a -> model -> Bool+   -- | Extract the assigned value for a given symbolic constant   valueOf :: typedSymbol t -> model -> Maybe t @@ -140,6 +143,9 @@   -- constants in the set   exceptFor :: symbolSet -> model -> model +  -- | Returns a model that removed the assignments for the symbolic constants+  exceptFor' :: typedSymbol t -> model -> model+   -- | Returns a model that only keeps the assignments for the symbolic   -- constants in the set   restrictTo :: symbolSet -> model -> model@@ -156,7 +162,7 @@   exact s = restrictTo s . extendTo s  -- | A type class for building a model manually from a model representation-class ModelOps model symbolSet typedSymbol => ModelRep rep model symbolSet (typedSymbol :: * -> *) where+class ModelRep rep model | rep -> model where   -- | Build a model   --   -- >>> let aBool = "a" :: TypedSymbol Bool

@@ -1,7 +1,9 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -33,8 +35,10 @@ import Data.Functor.Sum import Data.Int import Data.Word+import GHC.TypeLits import Generics.Deriving import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM+import Grisette.Core.Data.BV import Grisette.Core.Data.Class.Bool import Grisette.Core.Data.Class.SimpleMergeable import Grisette.Core.Data.Class.Solvable@@ -220,6 +224,14 @@   l >~ r = con $ l > r; \   symCompare l r = mrgSingle $ compare l r +#define CONCRETE_SORD_BV(type) \+instance (KnownNat n, 1 <= n) => SOrd (type n) where \+  l <=~ r = con $ l <= r; \+  l <~ r = con $ l < r; \+  l >=~ r = con $ l >= r; \+  l >~ r = con $ l > r; \+  symCompare l r = mrgSingle $ compare l r+ #if 1 CONCRETE_SORD(Bool) CONCRETE_SORD(Integer)@@ -234,7 +246,11 @@ CONCRETE_SORD(Word16) CONCRETE_SORD(Word32) CONCRETE_SORD(Word64)+CONCRETE_SORD(SomeWordN)+CONCRETE_SORD(SomeIntN) CONCRETE_SORD(B.ByteString)+CONCRETE_SORD_BV(WordN)+CONCRETE_SORD_BV(IntN) #endif  symCompareSingleList :: (SOrd a) => Bool -> Bool -> [a] -> [a] -> SymBool

@@ -0,0 +1,428 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{- HLINT ignore "Redundant bracket" -}++-- |+-- Module      :   Grisette.Core.Data.Class.SafeArith+-- 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.Core.Data.Class.SafeArith+  ( -- * Symbolic integer operations+    ArithException (..),+    SafeDivision (..),+    SafeLinearArith (..),+    SymIntegerOp,+  )+where++import Control.Exception+import Control.Monad.Except+import Data.Int+import Data.Typeable+import Data.Word+import GHC.TypeNats+import Grisette.Core.Control.Monad.Union+import Grisette.Core.Data.BV+import Grisette.Core.Data.Class.Bool+import Grisette.Core.Data.Class.Error+import Grisette.Core.Data.Class.Mergeable+import Grisette.Core.Data.Class.SOrd+import Grisette.Core.Data.Class.SimpleMergeable+import Grisette.Core.Data.Class.Solvable++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.IR.SymPrim++-- | Safe division with monadic error handling in multi-path+-- execution. These procedures throw an exception when the+-- divisor is zero. The result should be able to handle errors with+-- `MonadError`.+class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where+  -- | Safe signed 'div' with monadic error handling in multi-path execution.+  --+  -- >>> safeDiv (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger+  -- ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}+  safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a+  safeDiv l r = do+    (d, _) <- safeDivMod l r+    mrgSingle d++  -- | Safe signed 'mod' with monadic error handling in multi-path execution.+  --+  -- >>> safeMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger+  -- ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}+  safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a+  safeMod l r = do+    (_, m) <- safeDivMod l r+    mrgSingle m++  -- | Safe signed 'divMod' with monadic error handling in multi-path execution.+  --+  -- >>> safeDivMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymInteger, SymInteger)+  -- ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}+  safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)+  safeDivMod l r = do+    d <- safeDiv l r+    m <- safeMod l r+    mrgSingle (d, m)++  -- | Safe signed 'quot' with monadic error handling in multi-path execution.+  safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a+  safeQuot l r = do+    (d, m) <- safeDivMod l r+    mrgIf+      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)+      (mrgSingle d)+      (mrgSingle $ d + 1)++  -- | Safe signed 'rem' with monadic error handling in multi-path execution.+  safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a+  safeRem l r = do+    (d, m) <- safeDivMod l r+    mrgIf+      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)+      (mrgSingle m)+      (mrgSingle $ m - r)++  -- | Safe signed 'quotRem' with monadic error handling in multi-path execution.+  safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)+  safeQuotRem l r = do+    (d, m) <- safeDivMod l r+    mrgIf+      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)+      (mrgSingle (d, m))+      (mrgSingle (d + 1, m - r))++  -- | Safe signed 'div' with monadic error handling in multi-path execution.+  -- The error is transformed.+  --+  -- >>> safeDiv' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger+  -- ExceptT {If (= b 0) (Left ()) (Right (div a b))}+  safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a+  safeDiv' t l r = do+    (d, _) <- safeDivMod' t l r+    mrgSingle d++  -- | Safe signed 'mod' with monadic error handling in multi-path execution.+  -- The error is transformed.+  --+  -- >>> safeMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger+  -- ExceptT {If (= b 0) (Left ()) (Right (mod a b))}+  safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a+  safeMod' t l r = do+    (_, m) <- safeDivMod' t l r+    mrgSingle m++  -- | Safe signed 'divMod' with monadic error handling in multi-path execution.+  -- The error is transformed.+  --+  -- >>> safeDivMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM (SymInteger, SymInteger)+  -- ExceptT {If (= b 0) (Left ()) (Right ((div a b),(mod a b)))}+  safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)+  safeDivMod' t l r = do+    d <- safeDiv' t l r+    m <- safeMod' t l r+    mrgSingle (d, m)++  -- | Safe signed 'quot' with monadic error handling in multi-path execution.+  -- The error is transformed.+  safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a+  safeQuot' t l r = do+    (d, m) <- safeDivMod' t l r+    mrgIf+      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)+      (mrgSingle d)+      (mrgSingle $ d + 1)++  -- | Safe signed 'rem' with monadic error handling in multi-path execution.+  -- The error is transformed.+  safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a+  safeRem' t l r = do+    (d, m) <- safeDivMod' t l r+    mrgIf+      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)+      (mrgSingle m)+      (mrgSingle $ m - r)++  -- | Safe signed 'quotRem' with monadic error handling in multi-path execution.+  -- The error is transformed.+  safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)+  safeQuotRem' t l r = do+    (d, m) <- safeDivMod' t l r+    mrgIf+      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)+      (mrgSingle (d, m))+      (mrgSingle (d + 1, m - r))++  {-# MINIMAL (safeDivMod | (safeDiv, safeMod)), (safeDivMod' | (safeDiv', safeMod')) #-}++#define QUOTE() '+#define QID(a) a+#define QRIGHT(a) QID(a)'++#define QRIGHTT(a) QID(a)' t'++#define SAFE_DIVISION_FUNC(name, op) \+name _ r | r == 0 = merge $ throwError DivideByZero; \+name l r = mrgSingle $ l `op` r; \+QRIGHTT(name) _ r | r == 0 = let t1 = t' in merge $ throwError (t' DivideByZero); \+QRIGHTT(name) l r = mrgSingle $ l `op` r++#define SAFE_DIVISION_CONCRETE(type) \+instance SafeDivision ArithException type where \+  SAFE_DIVISION_FUNC(safeDiv, div); \+  SAFE_DIVISION_FUNC(safeMod, mod); \+  SAFE_DIVISION_FUNC(safeDivMod, divMod); \+  SAFE_DIVISION_FUNC(safeQuot, quot); \+  SAFE_DIVISION_FUNC(safeRem, rem); \+  SAFE_DIVISION_FUNC(safeQuotRem, quotRem)++#define SAFE_DIVISION_CONCRETE_BV(type) \+instance (KnownNat n, 1 <= n) => SafeDivision ArithException (type n) where \+  SAFE_DIVISION_FUNC(safeDiv, div); \+  SAFE_DIVISION_FUNC(safeMod, mod); \+  SAFE_DIVISION_FUNC(safeDivMod, divMod); \+  SAFE_DIVISION_FUNC(safeQuot, quot); \+  SAFE_DIVISION_FUNC(safeRem, rem); \+  SAFE_DIVISION_FUNC(safeQuotRem, quotRem)++#if 1+SAFE_DIVISION_CONCRETE(Integer)+SAFE_DIVISION_CONCRETE(Int8)+SAFE_DIVISION_CONCRETE(Int16)+SAFE_DIVISION_CONCRETE(Int32)+SAFE_DIVISION_CONCRETE(Int64)+SAFE_DIVISION_CONCRETE(Int)+SAFE_DIVISION_CONCRETE(Word8)+SAFE_DIVISION_CONCRETE(Word16)+SAFE_DIVISION_CONCRETE(Word32)+SAFE_DIVISION_CONCRETE(Word64)+SAFE_DIVISION_CONCRETE(Word)+#endif++#define SAFE_DIVISION_FUNC_SOME(stype, type, name, op) \+  name (stype (l :: type l)) (stype (r :: type r)) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> \+        if r == 0 \+          then merge $ throwError $ Right DivideByZero \+          else mrgSingle $ stype $ l `op` r; \+      Nothing -> merge $ throwError $ Left BitwidthMismatch); \+  QRIGHT(name) t (stype (l :: type l)) (stype (r :: type r)) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> \+        if r == 0 \+          then merge $ throwError $ t (Right DivideByZero) \+          else mrgSingle $ stype $ l `op` r; \+      Nothing -> merge $ throwError $ t (Left BitwidthMismatch))++#define SAFE_DIVISION_FUNC_SOME_DIVMOD(stype, type, name, op) \+  name (stype (l :: type l)) (stype (r :: type r)) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> \+        if r == 0 \+          then merge $ throwError $ Right DivideByZero \+          else (case l `op` r of (d, m) -> mrgSingle (stype d, stype m)); \+      Nothing -> merge $ throwError $ Left BitwidthMismatch); \+  QRIGHT(name) t (stype (l :: type l)) (stype (r :: type r)) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> \+        if r == 0 \+          then merge $ throwError $ t (Right DivideByZero) \+          else (case l `op` r of (d, m) -> mrgSingle (stype d, stype m)); \+      Nothing -> merge $ throwError $ t (Left BitwidthMismatch))++#if 1+SAFE_DIVISION_CONCRETE_BV(IntN)+SAFE_DIVISION_CONCRETE_BV(WordN)+instance SafeDivision (Either BitwidthMismatch ArithException) SomeIntN where+  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeDiv, div)+  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeMod, mod)+  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeIntN, IntN, safeDivMod, divMod)+  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeQuot, quot)+  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeRem, rem)+  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeIntN, IntN, safeQuotRem, quotRem)++instance SafeDivision (Either BitwidthMismatch ArithException) SomeWordN where+  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeDiv, div)+  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeMod, mod)+  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeWordN, WordN, safeDivMod, divMod)+  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeQuot, quot)+  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeRem, rem)+  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeWordN, WordN, safeQuotRem, quotRem)+#endif++-- | Safe division with monadic error handling in multi-path+-- execution. These procedures throw an exception when overflow or underflow happens.+-- The result should be able to handle errors with `MonadError`.+class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e where+  -- | Safe '+' with monadic error handling in multi-path execution.+  -- Overflows or underflows are treated as errors.+  --+  -- >>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger+  -- ExceptT {Right (+ a b)}+  -- >>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)+  -- ExceptT {If (ite (< 0x0 a) (&& (< 0x0 b) (< (+ a b) 0x0)) (&& (< a 0x0) (&& (< b 0x0) (<= 0x0 (+ a b))))) (If (< 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a b))}+  safeAdd :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a++  -- | Safe 'negate' with monadic error handling in multi-path execution.+  -- Overflows or underflows are treated as errors.+  --+  -- >>> safeNeg (ssym "a") :: ExceptT ArithException UnionM SymInteger+  -- ExceptT {Right (- a)}+  -- >>> safeNeg (ssym "a") :: ExceptT ArithException UnionM (SymIntN 4)+  -- ExceptT {If (= a 0x8) (Left arithmetic overflow) (Right (- a))}+  safeNeg :: (MonadError e uf, MonadUnion uf) => a -> uf a++  -- | Safe '-' with monadic error handling in multi-path execution.+  -- Overflows or underflows are treated as errors.+  --+  -- >>> safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger+  -- ExceptT {Right (+ a (- b))}+  -- >>> safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)+  -- ExceptT {If (ite (<= 0x0 a) (&& (< b 0x0) (< (+ a (- b)) 0x0)) (&& (< a 0x0) (&& (< 0x0 b) (< 0x0 (+ a (- b)))))) (If (<= 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a (- b)))}+  safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a++  -- | Safe '+' with monadic error handling in multi-path execution.+  -- Overflows or underflows are treated as errors.+  -- The error is transformed.+  safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a++  -- | Safe 'negate' with monadic error handling in multi-path execution.+  -- Overflows or underflows are treated as errors.+  -- The error is transformed.+  safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a++  -- | Safe '-' with monadic error handling in multi-path execution.+  -- Overflows or underflows are treated as errors.+  -- The error is transformed.+  safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a++instance SafeLinearArith ArithException Integer where+  safeAdd l r = mrgSingle (l + r)+  safeNeg l = mrgSingle (-l)+  safeMinus l r = mrgSingle (l - r)+  safeAdd' _ l r = mrgSingle (l + r)+  safeNeg' _ l = mrgSingle (-l)+  safeMinus' _ l r = mrgSingle (l - r)++#define SAFE_LINARITH_SIGNED_CONCRETE_BODY \+  safeAdd l r = let res = l + r in \+    mrgIf (con $ l > 0 && r > 0 && res < 0) \+          (throwError Overflow) \+          (mrgIf (con $ l < 0 && r < 0 && res >= 0) \+                 (throwError Underflow) \+                 (return res));\+  safeAdd' t' l r = let res = l + r in \+    mrgIf (con $ l > 0 && r > 0 && res < 0) \+          (throwError (t' Overflow)) \+          (mrgIf (con $ l < 0 && r < 0 && res >= 0) \+                 (throwError (t' Underflow)) \+                 (return res)); \+  safeMinus l r = let res = l - r in \+    mrgIf (con $ l >= 0 && r < 0 && res < 0) \+          (throwError Overflow) \+          (mrgIf (con $ l < 0 && r > 0 && res > 0) \+                 (throwError Underflow) \+                 (return res));\+  safeMinus' t' l r = let res = l - r in \+    mrgIf (con $ l >= 0 && r < 0 && res < 0) \+          (throwError (t' Overflow)) \+          (mrgIf (con $ l < 0 && r > 0 && res > 0) \+                 (throwError (t' Underflow)) \+                 (return res)); \+  safeNeg v = mrgIf (con $ v == minBound) (throwError Overflow) (return $ -v);\+  safeNeg' t' v = mrgIf (con $ v == minBound) (throwError (t' Overflow)) (return $ -v)++#define SAFE_LINARITH_SIGNED_CONCRETE(type) \+instance SafeLinearArith ArithException type where \+  SAFE_LINARITH_SIGNED_CONCRETE_BODY++#define SAFE_LINARITH_SIGNED_BV_CONCRETE(type) \+instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (type n) where \+  SAFE_LINARITH_SIGNED_CONCRETE_BODY++#define SAFE_LINARITH_UNSIGNED_CONCRETE_BODY \+  safeAdd l r = let res = l + r in \+    mrgIf (con $ l > res || r > res) \+          (throwError Overflow) \+          (return res);\+  safeAdd' t' l r = let res = l + r in \+    mrgIf (con $ l > res || r > res) \+          (throwError (t' Overflow)) \+          (return res); \+  safeMinus l r = \+    mrgIf (con $ r > l) \+          (throwError Underflow) \+          (return $ l - r);\+  safeMinus' t' l r = \+    mrgIf (con $ r > l) \+          (throwError $ t' Underflow) \+          (return $ l - r);\+  safeNeg v = mrgIf (con $ v /= 0) (throwError Underflow) (return $ -v);\+  safeNeg' t' v = mrgIf (con $ v /= 0) (throwError (t' Underflow)) (return $ -v)++#define SAFE_LINARITH_UNSIGNED_CONCRETE(type) \+instance SafeLinearArith ArithException type where \+  SAFE_LINARITH_UNSIGNED_CONCRETE_BODY++#define SAFE_LINARITH_UNSIGNED_BV_CONCRETE(type) \+instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (type n) where \+  SAFE_LINARITH_UNSIGNED_CONCRETE_BODY++#define SAFE_LINARITH_SOME_CONCRETE(type, ctype) \+instance SafeLinearArith (Either BitwidthMismatch ArithException) type where \+  safeAdd (type (l :: ctype l)) (type (r :: ctype r)) = merge (\+    case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> type <$> safeAdd' Right l r; \+      _ -> throwError $ Left BitwidthMismatch); \+  safeAdd' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\+    case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> type <$> safeAdd' (t . Right) l r; \+      _ -> let t' = t; t''' = t in throwError $ t' $ Left BitwidthMismatch); \+  safeMinus (type (l :: ctype l)) (type (r :: ctype r)) = merge (\+    case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> type <$> safeMinus' Right l r; \+      _ -> throwError $ Left BitwidthMismatch); \+  safeMinus' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\+    case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> type <$> safeMinus' (t . Right) l r; \+      _ -> let t' = t; t''' = t in throwError $ t' $ Left BitwidthMismatch); \+  safeNeg (type l) = merge $ type <$> safeNeg' Right l; \+  safeNeg' t (type l) = merge $ type <$> safeNeg' (t . Right) l++#if 1+SAFE_LINARITH_SIGNED_CONCRETE(Int8)+SAFE_LINARITH_SIGNED_CONCRETE(Int16)+SAFE_LINARITH_SIGNED_CONCRETE(Int32)+SAFE_LINARITH_SIGNED_CONCRETE(Int64)+SAFE_LINARITH_SIGNED_CONCRETE(Int)+SAFE_LINARITH_SIGNED_BV_CONCRETE(IntN)+SAFE_LINARITH_SOME_CONCRETE(SomeIntN, IntN)+SAFE_LINARITH_UNSIGNED_CONCRETE(Word8)+SAFE_LINARITH_UNSIGNED_CONCRETE(Word16)+SAFE_LINARITH_UNSIGNED_CONCRETE(Word32)+SAFE_LINARITH_UNSIGNED_CONCRETE(Word64)+SAFE_LINARITH_UNSIGNED_CONCRETE(Word)+SAFE_LINARITH_UNSIGNED_BV_CONCRETE(WordN)+SAFE_LINARITH_SOME_CONCRETE(SomeWordN, WordN)+#endif++-- | Aggregation for the operations on symbolic integer types+class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a