-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- (The sbv library is hosted at <http://github.com/LeventErkok/sbv>.
-- Comments, bug reports, and patches are always welcome.)
--
-- SBV: SMT Based Verification
--
-- Express properties about Haskell programs and automatically prove
-- them using SMT solvers.
--
-- >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
-- Q.E.D.
--
-- >>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)
-- Falsifiable. Counter-example:
--   s0 = 64 :: Word8
--
-- And similarly, 'sat' finds a satisfying instance. The types involved are:
--
-- @
--     'prove' :: 'Provable' a => a -> 'IO' t'ThmResult'
--     'sat'   :: 'Data.SBV.Provers.Satisfiable' a => a -> 'IO' t'SatResult'
-- @
--
-- The classes 'Provable' and 'Data.SBV.Provers.Satisfiable' come with instances for n-ary predicates, for arbitrary n.
-- The predicates are just regular Haskell functions over symbolic types listed below.
-- Functions for checking satisfiability ('sat' and 'allSat') are also
-- provided.
--
-- __Symbolic Types__
--
-- The sbv library introduces the following symbolic types:
--
--   * 'SBool': Symbolic Booleans (bits).
--
--   * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned).
--
--   * 'SInt8',  'SInt16',  'SInt32',  'SInt64': Symbolic Ints (signed).
--
--   * 'SWord' @n@: Generalized symbolic words of arbitrary bit-size.
--
--   * 'SInt' @n@: Generalized symbolic ints of arbitrary bit-size.
--
--   * 'SInteger': Unbounded signed integers.
--
--   * 'SReal': Algebraic-real numbers.
--
--   * 'SFloat': IEEE-754 single-precision floating point values.
--
--   * 'SDouble': IEEE-754 double-precision floating point values.
--
--   * 'SRational': Rationals. (Ratio of two symbolic integers.)
--
--   * 'SFloatingPoint': Generalized IEEE-754 floating point values, with user specified exponent and
--   mantissa widths.
--
--   * 'SChar', 'SString', 'RegExp': Characters, strings and regular expressions.
--
--   * 'SList': Symbolic lists (which can be nested)
--
--   * 'STuple', 'STuple2', 'STuple3', .., 'STuple8' : Symbolic tuples (upto 8-tuples, can be nested)
--
--   * 'SEither': Symbolic sums
--
--   * 'SMaybe': Symbolic optional values.
--
--   * 'SSet': Symbolic sets.
--
--   * 'SArray': Arrays of symbolic values.
--
--   * Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
--
--   * Uninterpreted constants and functions over symbolic values, with user
--     defined SMT-Lib axioms.
--
--   * Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
--
--   * Ability to define SMTLib functions, generated directly from Haskell versions,
--     including support for recursive and mutually recursive functions.
--
--   * Express quantified formulas (both universals and existentials, including
--     alternating quantifiers), covering first-order logic.
--
--   * Model validation: SBV can validate models returned by solvers, which allows
--     for protection against bugs in SMT solvers and SBV itself. (See the 'validateModel'
--     parameter.)
--
-- The user can construct ordinary Haskell programs using these types, which behave
-- very similar to their concrete counterparts. In particular these types belong to the
-- standard classes 'Num', 'Bits', custom versions of 'Eq' ('EqSymbolic')
-- and 'Ord' ('OrdSymbolic'), along with several other custom classes for simplifying
-- programming with symbolic values. The framework takes full advantage of Haskell's type
-- inference to avoid many common mistakes.
--
-- Furthermore, predicates (i.e., functions that return 'SBool') built out of
-- these types can also be:
--
--   * proven correct via an external SMT solver (the 'prove' function)
--
--   * checked for satisfiability (the 'sat', 'allSat' functions)
--
--   * used in synthesis (the `sat` function with existentials)
--
--   * quick-checked
--
-- If a predicate is not valid, 'prove' will return a counterexample: An
-- assignment to inputs such that the predicate fails. The 'sat' function will
-- return a satisfying assignment, if there is one. The 'allSat' function returns
-- all satisfying assignments.
--
--
-- __Solvers__
--
-- The sbv library uses third-party SMT solvers via the standard SMT-Lib interface:
-- <https://smt-lib.org>
--
-- The SBV library is designed to work with any SMT-Lib compliant SMT-solver.
-- Currently, we support the following SMT-Solvers out-of-the box:
--
--   * ABC from University of Berkeley: <http://www.eecs.berkeley.edu/~alanmi/abc/>
--
--   * CVC4, and CVC5 from Stanford University and the University of Iowa. <https://cvc4.github.io/> and <https://cvc5.github.io>
--
--   * Boolector from Johannes Kepler University: <https://boolector.github.io> and its successor Bitwuzla from Stanford
--     university: <https://bitwuzla.github.io>
--
--   * MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: <http://mathsat.fbk.eu/>
--
--   * Yices from SRI: <http://yices.csl.sri.com/>
--
--   * DReal from CMU: <http://dreal.github.io/>
--
--   * OpenSMT from Università della Svizzera italiana <https://verify.inf.usi.ch/opensmt>
--
--   * Z3 from Microsoft: <http://github.com/Z3Prover/z3/wiki>
--
-- SBV requires recent versions of these solvers; please see the file
-- @SMTSolverVersions.md@ in the source distribution for specifics.
--
-- SBV also allows calling these solvers in parallel, either getting results from multiple solvers
-- or returning the fastest one. (See 'proveWithAll', 'proveWithAny', etc.)
--
-- Support for other compliant solvers can be added relatively easily, please
-- get in touch if there is a solver you'd like to see included.
--
--
-- __Semi-automated theorem proving__
--
-- While SMT solvers are quite powerful, there is a certain class of problems that they are just not well suited for. In particular, SMT
-- solvers are not good at proofs that require induction, or those that require complex chains of reasoning. Induction is necessary to reason about
-- any recursive algorithm, and most such proofs require carefully constructed equational steps. SBV allows for a
-- style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs.
-- The documentation includes example proofs for many list functions, and even inductive proofs for the familiar insertion
-- and merge-sort algorithms, along with a proof that the square-root of 2 is irrational. While a proper theorem prover (such as Lean, Isabelle
-- etc.) is a more appropriate choice for such proofs, with some guidance (and acceptance of a much larger trusted code base!), SBV can
-- be used to establish correctness of various mathematical claims and algorithms that are usually beyond the scope of SMT
-- solvers alone. See "Data.SBV.Tools.KnuckleDragger" for the API, and
--
--    - "Documentation.SBV.Examples.KnuckleDragger.InsertionSort"
--    - "Documentation.SBV.Examples.KnuckleDragger.MergeSort"
--    - "Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational"
--    - "Documentation.SBV.Examples.KnuckleDragger.ShefferStroke"
--    - "Documentation.SBV.Examples.KnuckleDragger.Lists"
--
-- for various proofs performed in this style.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV (
  -- $progIntro

  -- * Symbolic types

  -- ** Booleans
    SBool
  -- *** Boolean values and functions
  , sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), fromBool, oneIf
  -- *** Logical aggregations
  , sAnd, sOr, sAny, sAll
  -- ** Bit-vectors
  -- *** Unsigned bit-vectors
  , SWord8, SWord16, SWord32, SWord64, SWord, WordN
  -- *** Signed bit-vectors
  , SInt8, SInt16, SInt32, SInt64, SInt, IntN
  -- *** Converting between fixed-size and arbitrary bitvectors
  , BVIsNonZero, FromSized, ToSized, fromSized, toSized
  -- ** Unbounded integers
  -- $unboundedLimitations
  , SInteger
  -- ** Floating point numbers
  -- $floatingPoints
  , ValidFloat, SFloat, SDouble
  , SFloatingPoint, FloatingPoint
  , SFPHalf, FPHalf
  , SFPBFloat, FPBFloat
  , SFPSingle, FPSingle
  , SFPDouble, FPDouble
  , SFPQuad, FPQuad
  , fpFromInteger
  -- ** Rationals
  , SRational
  -- ** Algebraic reals
  -- $algReals
  , SReal, AlgReal(..), sRealToSInteger, algRealToRational, RealPoint(..), realPoint, RationalCV(..)
  -- ** Characters, Strings and Regular Expressions
  -- $strings
  , SChar, SString
  -- ** Symbolic lists
  -- $lists
  , SList
  -- ** Tuples
  -- $tuples
  , SymTuple, STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8
  -- ** Sum types
  , SMaybe, SEither
  -- ** Sets
  , RCSet(..), SSet
  -- * Arrays of symbolic values
  , SArray, sArray, sArray_, sArrays, readArray, writeArray, lambdaArray, listArray

  -- * Creating symbolic values
  -- ** Single value
  -- $createSym
  , sBool, sBool_
  , sWord8, sWord8_, sWord16, sWord16_, sWord32, sWord32_, sWord64, sWord64_, sWord, sWord_
  , sInt8,  sInt8_,  sInt16,  sInt16_,  sInt32,  sInt32_,  sInt64,  sInt64_, sInt, sInt_
  , sInteger, sInteger_
  , sReal, sReal_
  , sRational, sRational_
  , sFloat, sFloat_
  , sDouble, sDouble_
  , sFloatingPoint, sFloatingPoint_
  , sFPHalf, sFPHalf_
  , sFPBFloat, sFPBFloat_
  , sFPSingle, sFPSingle_
  , sFPDouble, sFPDouble_
  , sFPQuad, sFPQuad_
  , sChar, sChar_
  , sString, sString_
  , sList, sList_
  , sTuple, sTuple_
  , sEither, sEither_
  , sMaybe, sMaybe_
  , sSet, sSet_

  -- ** List of values
  -- $createSyms
  , sBools
  , sWord8s, sWord16s, sWord32s, sWord64s, sWords
  , sInt8s,  sInt16s,  sInt32s,  sInt64s, sInts
  , sIntegers
  , sReals
  , sRationals
  , sFloats
  , sDoubles
  , sFloatingPoints
  , sFPHalfs
  , sFPBFloats
  , sFPSingles
  , sFPDoubles
  , sFPQuads
  , sChars
  , sStrings
  , sLists
  , sTuples
  , sEithers
  , sMaybes
  , sSets

  -- * Symbolic Equality and Comparisons
  -- $distinctNote
  , EqSymbolic(..), OrdSymbolic(..), Equality(..)
  -- * Conditionals: Mergeable values
  , Mergeable(..), ite, iteLazy

  -- * Symbolic integral numbers
  , SIntegral
  -- * Division and Modulus
  , SDivisible(..)
  -- $euclidianNote
  , sEDivMod, sEDiv, sEMod, sDivides
  -- * Bit-vector operations
  -- ** Conversions
  , sFromIntegral
  -- ** Shifts and rotates
  -- $shiftRotate
  , sShiftLeft, sShiftRight, sRotateLeft, sBarrelRotateLeft, sRotateRight, sBarrelRotateRight, sSignedShiftArithRight
  -- ** Finite bit-vector operations
  , SFiniteBits(..)
  -- ** Splitting, joining, and extending bit-vectors
  , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake, ByteConverter(..)
  -- ** Exponentiation
  , (.^)
  -- * IEEE-floating point numbers
  , IEEEFloating(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity
  -- ** Rounding modes
  , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ
  -- ** Conversion to/from floats
  -- $conversionNote
  , IEEEFloatConvertible(..)

  -- ** Bit-pattern conversions
  , sFloatAsSWord32,       sWord32AsSFloat
  , sDoubleAsSWord64,      sWord64AsSDouble
  , sFloatingPointAsSWord, sWordAsSFloatingPoint

  -- ** Extracting bit patterns from floats
  , blastSFloat
  , blastSDouble
  , blastSFloatingPoint

  -- ** Showing values in detail
  , crack

  -- * Enumerations
  -- $enumerations
  , mkSymbolicEnumeration

  -- * Uninterpreted sorts, constants, and functions
  -- $uninterpreted
  , mkUninterpretedSort

  -- * Stopping unrolling: Defined functions
  , SMTDefinable(..), registerType

  -- * Special relations
  -- $specialRels
  , Relation, isPartialOrder, isLinearOrder, isTreeOrder, isPiecewiseLinearOrder, mkTransitiveClosure

  -- * Properties, proofs, and satisfiability
  -- $proveIntro
  -- $multiIntro
  , Predicate, ConstraintSet, Provable, Satisfiable
  , prove, proveWith
  , dprove, dproveWith
  , sat, satWith
  , dsat, dsatWith
  , allSat, allSatWith
  , isVacuousProof, isVacuousProofWith
  , isTheorem, isTheoremWith, isSatisfiable, isSatisfiableWith
  , proveWithAny, proveWithAll, proveConcurrentWithAny, proveConcurrentWithAll
  , satWithAny,   satWithAll,   satConcurrentWithAny,   satConcurrentWithAll
  , generateSMTBenchmarkSat, generateSMTBenchmarkProof
  , solve
  -- ** Partitioning result space
  -- $partitionIntro
  , allSatPartition

  -- * Constraints and Quantifiers
  -- $constrainIntro
  -- ** General constraints
  -- $generalConstraints
  , constrain, softConstrain

  -- ** Quantified constraints, quantifier elimination, and skolemization
  -- $quantifiers
  , QuantifiedBool, quantifiedBool, Forall(..), Exists(..), ExistsUnique(..), ForallN(..), ExistsN(..), QNot(..), Skolemize(..)

  -- ** Constraint Vacuity
  -- $constraintVacuity

  -- ** Named constraints and attributes
  -- $namedConstraints
  , namedConstraint, constrainWithAttribute

  -- ** Unsat cores
  -- $unsatCores

  -- ** Cardinality constraints
  -- $cardIntro
  , pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed

  -- * Checking safety
  -- $safeIntro
  , sAssert, isSafe, SExecutable, sName, safe, safeWith

  -- * Quick-checking
  , sbvQuickCheck

  -- * Optimization
  -- $optiIntro
  , optimize, optimizeWith
  , optLexicographic, optLexicographicWith
  , optPareto, optParetoWith
  , optIndependent, optIndependentWith

  -- ** Multiple optimization goals
  -- $multiOpt
  , OptimizeStyle(..)
  -- ** Objectives and Metrics
  , Objective(..)
  , Metric(..), minimize, maximize
  -- ** Soft assertions
  -- $softAssertions
  , assertWithPenalty , Penalty(..)
  -- ** Field extensions
  -- | If an optimization results in an infinity/epsilon value, the returned t'CV' value will be in the corresponding extension field.
  , ExtCV(..), GeneralizedCV(..)

  -- * Model extraction
  -- $modelExtraction

  -- ** Inspecting proof results
  -- $resultTypes
  , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..), SMTReasonUnknown(..)

  -- ** Observing expressions
  -- $observeInternal
  , observe, observeIf, sObserve

  -- ** Programmable model extraction
  -- $programmableExtraction
  , Modelable(..), displayModels, extractModels
  , getModelDictionaries, getModelValues, getModelUninterpretedValues

  -- * SMT Interface
  , SMTConfig(..), KDOptions(..), Timing(..), SMTLibVersion(..), Solver(..), SMTSolver(..)
  -- ** Controlling verbosity
  -- $verbosity

  -- ** Solvers
  , boolector, bitwuzla, cvc4, cvc5, yices, dReal, z3, mathSAT, abc, openSMT
  -- ** Configurations
  , defaultSolverConfig, defaultSMTCfg, defaultDeltaSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers
  , setLogic, Logic(..), setOption, setInfo, setTimeOut
  -- ** SBV exceptions
  , SBVException(..)

  -- * Abstract SBV type
  , SBV, HasKind(..), Kind(..)
  , SymVal, free, free_, mkFreeVars, symbolic, symbolics, literal, unliteral, fromCV
  , isConcrete, isSymbolic, isConcretely, mkSymVal
  , MonadSymbolic(..), Symbolic, SymbolicT, label, output, runSMT, runSMTWith
  , some

  -- * Queriable values
  , Queriable(..), freshVar, freshVar_

  -- * Module exports
  -- $moduleExportIntro

  , module Data.Bits
  , module Data.Word
  , module Data.Int
  , module Data.Ratio
  ) where

import Control.Monad       (unless)
import Control.Monad.Trans (MonadIO)

import Data.SBV.Core.AlgReals
import Data.SBV.Core.Data       hiding (free, free_, mkFreeVars,
                                        output, symbolic, symbolics, mkSymVal,
                                        bvExtract, bvDrop, bvTake, (#))
import Data.SBV.Core.Model      hiding (assertWithPenalty, minimize, maximize,
                                        solve, sBool, sBool_, sBools, sChar, sChar_, sChars,
                                        sDouble, sDouble_, sDoubles, sFloat, sFloat_, sFloats,
                                        sFloatingPoint, sFloatingPoint_, sFloatingPoints,
                                        sFPHalf, sFPHalf_, sFPHalfs, sFPBFloat, sFPBFloat_, sFPBFloats, sFPSingle, sFPSingle_, sFPSingles,
                                        sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads,
                                        sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s,
                                        sInt64, sInt64_, sInt64s, sInteger, sInteger_, sIntegers,
                                        sWord, sWords, sWord_, sInt, sInts, sInt_,
                                        sList, sList_, sLists, sTuple, sTuple_, sTuples,
                                        sReal, sReal_, sReals, sString, sString_, sStrings,
                                        sRational, sRational_, sRationals,
                                        sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s,
                                        sWord32, sWord32_, sWord32s, sWord64, sWord64_, sWord64s,
                                        sMaybe, sMaybe_, sMaybes, sEither, sEither_, sEithers, sSet, sSet_, sSets,
                                        sArray, sArray_, sArrays,
                                        sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend, sObserve)

import qualified Data.SBV.Core.Model as M  (sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend)
import qualified Data.SBV.Core.Data  as CD (bvExtract, (#), bvDrop, bvTake)

import Data.SBV.Core.Kind

import Data.SBV.Core.SizedFloats

import Data.SBV.Core.Floating
import Data.SBV.Core.Symbolic   ( MonadSymbolic(..), SymbolicT, registerKind
                                , ProgInfo(..), rProgInfo, SpecialRelOp(..), UICodeKind(UINone)
                                , getRootState, UIName(UIGiven)
                                )

import Data.SBV.Provers.Prover hiding (prove, proveWith, sat, satWith, allSat,
                                       dsat, dsatWith, dprove, dproveWith,
                                       allSatWith, optimize, optimizeWith,
                                       isVacuousProof, isVacuousProofWith,
                                       isTheorem, isTheoremWith, isSatisfiable,
                                       isSatisfiableWith, runSMT, runSMTWith,
                                       sName, safe, safeWith)

import Data.IORef (modifyIORef', readIORef)

import Data.SBV.Client
import Data.SBV.Client.BaseIO

import Data.SBV.Utils.TDiff (Timing(..))

import Data.Bits
import Data.Int
import Data.Ratio
import Data.Word

import Data.SBV.SMT.Utils (SBVException(..))

import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))
import Data.SBV.Control.Utils (getValue, freshVar, freshVar_)

import qualified Data.SBV.Utils.CrackNum as CN

import Data.Proxy (Proxy(..))
import Data.Kind  (Type)
import GHC.TypeLits (KnownNat, type (<=), type (+), type (-))

import Prelude hiding((+), (-)) -- to avoid the haddock ambiguity

import Data.Char (isSpace, isPunctuation)

--- $setup
--- >>> -- For doctest purposes only:
--- >>> :set -XDataKinds -XFlexibleContexts -XTypeApplications -XRankNTypes
--- >>> import Data.Proxy

-- | Show a value in detailed (cracked) form, if possible.
-- This makes most sense with numbers, and especially floating-point types.
crack :: Bool -> SBV a -> String
crack :: forall a. Bool -> SBV a -> String
crack Bool
verb (SBV (SVal Kind
_ (Left CV
cv))) | Just String
s <- CV -> Bool -> Maybe Integer -> Maybe String
forall a. CrackNum a => a -> Bool -> Maybe Integer -> Maybe String
CN.crackNum CV
cv Bool
verb Maybe Integer
forall a. Maybe a
Nothing = String
s
crack Bool
_    (SBV SVal
sv)                                                         = SVal -> String
forall a. Show a => a -> String
show SVal
sv

-- Haddock section documentation
{- $progIntro
The SBV library is really two things:

  * A framework for writing symbolic programs in Haskell, i.e., programs operating on
    symbolic values along with the usual concrete counterparts.

  * A framework for proving properties of such programs using SMT solvers.

The programming goal of SBV is to provide a /seamless/ experience, i.e., let people program
in the usual Haskell style without distractions of symbolic coding. While Haskell helps
in some aspects (the 'Num' and 'Bits' classes simplify coding), it makes life harder
in others. For instance, @if-then-else@ only takes 'Bool' as a test in Haskell, and
comparisons ('>' etc.) only return 'Bool's. Clearly we would like these values to be
symbolic (i.e., 'SBool'), thus stopping us from using some native Haskell constructs.
When symbolic versions of operators are needed, they are typically obtained by prepending a dot,
for instance '==' becomes '.=='. Care has been taken to make the transition painless. In
particular, any Haskell program you build out of symbolic components is fully concretely
executable within Haskell, without the need for any custom interpreters. (They are truly
Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated
feel of the system, one of the original design goals for SBV.

Incremental query mode: SBV provides a wide variety of ways to utilize SMT-solvers, without requiring the user to
deal with the solvers themselves. While this mode is convenient, advanced users might need
access to the underlying solver at a lower level. For such use cases, SBV allows
users to have an interactive session: The user can issue commands to the solver, inspect
the values/results, and formulate new constraints. This advanced feature is available through
the "Data.SBV.Control" module, where most SMTLib features are made available via a typed-API.
-}

{- $proveIntro
The SBV library provides a "push-button" verification system via automated SMT solving. The
design goal is to let SMT solvers be used without any knowledge of how SMT solvers work
or how different logics operate. The details are hidden behind the SBV framework, providing
Haskell programmers with a clean API that is unencumbered by the details of individual solvers.
To that end, we use the SMT-Lib standard (<https://smt-lib.org>)
to communicate with arbitrary SMT solvers.
-}

{- $multiIntro
=== Using multiple solvers
On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers,
using parallel threads. Even with machines with single-cores, threading can be helpful if you
want to try out multiple-solvers but do not know which one would work the best
for the problem at hand ahead of time.

SBV allows proving/satisfiability-checking with multiple
backends at the same time. Each function comes in two variants, one that
returns the results from all solvers, the other that returns the fastest one.

The @All@ variants, (i.e., 'proveWithAll', 'satWithAll') run all solvers and
return all the results. SBV internally makes sure that the result is lazily generated; so,
the order of solvers given does not matter. In other words, the order of results will follow
the order of the solvers as they finish, not as given by the user. These variants are useful when you
want to make sure multiple-solvers agree (or disagree!) on a given problem.

The @Any@ variants, (i.e., 'proveWithAny', 'satWithAny') will run all the solvers
in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants
are useful when you do not care if the solvers produce the same result, but rather want to get the
solution as quickly as possible, taking advantage of modern many-core machines.

Note that the function 'getAvailableSolvers' will return all the installed solvers, which can be
used as the first argument to all these functions, if you simply want to try all available solvers on a machine.
-}

{- $safeIntro

The 'sAssert' function allows users to introduce invariants to make sure
certain properties hold at all times. This is another mechanism to provide further documentation/contract info
into SBV code. The functions 'safe' and 'safeWith' can be used to statically discharge these proof assumptions.
If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.

Here's a simple example. Let's assume we have a function that does subtraction, and requires its
first argument to be larger than the second:

>>> let sub x y = sAssert Nothing "sub: x >= y must hold!" (x .>= y) (x - y)

Clearly, this function is not safe, as there's nothing that stops us from passing it a larger second argument.
We can use 'safe' to statically see if such a violation is possible before we use this function elsewhere.

>>> safe (sub :: SInt8 -> SInt8 -> SInt8)
[sub: x >= y must hold!: Violated. Model:
  s0 = 0 :: Int8
  s1 = 1 :: Int8]

What happens if we make sure to arrange for this invariant? Consider this version:

>>> let safeSub x y = ite (x .>= y) (sub x y) 0

Clearly, @safeSub@ must be safe. And indeed, SBV can prove that:

>>> safe (safeSub :: SInt8 -> SInt8 -> SInt8)
[sub: x >= y must hold!: No violations detected]

Note how we used @sub@ and @safeSub@ polymorphically. We only need to monomorphise our types when a proof
attempt is done, as we did in the 'safe' calls.

If required, the user can pass a @CallStack@ through the first argument to 'sAssert', which will be used
by SBV to print a diagnostic info to pinpoint the failure.

Also see "Documentation.SBV.Examples.Misc.NoDiv0" for the classic div-by-zero example.
-}


{- $optiIntro
  SBV can optimize metric functions, i.e., those that generate both bounded @SIntN@, @SWordN@, and unbounded 'SInteger'
  types, along with those produce 'SReal's. That is, it can find models satisfying all the constraints while minimizing
  or maximizing user given metrics. Currently, optimization requires the use of the z3 SMT solver as the backend,
  and a good review of these features is given
  in this paper: <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf>.

  Goals can be lexicographically (default), independently, or pareto-front optimized. The relevant functions are:

      * 'minimize': Minimize a given arithmetic goal
      * 'maximize': Minimize a given arithmetic goal

  Goals can be optimized at a regular or an extended value: An extended value is either positive or negative infinity
  (for unbounded integers and reals) or positive or negative epsilon differential from a real value (for reals).

  For instance, a call of the form

       @ 'minimize' "name-of-goal" $ x + 2*y @

  minimizes the arithmetic goal @x+2*y@, where @x@ and @y@ can be signed\/unsigned bit-vectors, reals,
  or integers.

== A simple example

  Here's an optimization example in action:

  >>> optimize Lexicographic $ \x y -> minimize "goal" (x+2*(y::SInteger))
  Optimal in an extension field:
    goal = -oo :: Integer

  We will describe the role of the constructor 'Lexicographic' shortly.

  Of course, this becomes more useful when the result is not in an extension field:

>>> :{
    optimize Lexicographic $ do
                  x <- sInteger "x"
                  y <- sInteger "y"
                  constrain $ x .> 0
                  constrain $ x .< 6
                  constrain $ y .> 2
                  constrain $ y .< 12
                  minimize "goal" $ x + 2 * y
    :}
Optimal model:
  x    = 1 :: Integer
  y    = 3 :: Integer
  goal = 7 :: Integer

  As usual, the programmatic API can be used to extract the values of objectives and model-values ('getModelObjectives',
  'getModelAssignment', etc.) to access these values and program with them further.

  The following examples illustrate the use of basic optimization routines:

     * "Documentation.SBV.Examples.Optimization.LinearOpt": Simple linear-optimization example.
     * "Documentation.SBV.Examples.Optimization.Production": Scheduling machines in a shop
     * "Documentation.SBV.Examples.Optimization.VM": Scheduling virtual-machines in a data-center
-}

{- $multiOpt

  Multiple goals can be specified, using the same syntax. In this case, the user gets to pick what style of
  optimization to perform, by passing the relevant 'OptimizeStyle' as the first argument to 'optimize'.

    * ['Lexicographic']. The solver will optimize the goals in the given order, optimizing
      the latter ones under the model that optimizes the previous ones.

    * ['Independent']. The solver will optimize the goals independently of each other. In this case the user will
      be presented a model for each goal given.

    * ['Pareto']. Finally, the user can query for pareto-fronts. A pareto front is an model such that no goal can be made
      "better" without making some other goal "worse."

      Pareto fronts only make sense when the objectives are bounded. If there are unbounded objective values, then the
      backend solver can loop infinitely. (This is what z3 does currently.) If you are not sure the objectives are
      bounded, you should first use 'Independent' mode to ensure the objectives are bounded, and then switch to
      pareto-mode to extract them further.

      The optional number argument to 'Pareto' specifies the maximum number of pareto-fronts the user is asking
      to get. If 'Nothing', SBV will query for all pareto-fronts. Note that pareto-fronts can be really large,
      so if 'Nothing' is used, there is a potential for waiting indefinitely for the SBV-solver interaction to finish. (If
      you suspect this might be the case, run in 'verbose' mode to see the interaction and put a limiting factor
      appropriately.)
-}

{- $softAssertions

  Related to optimization, SBV implements soft-asserts via 'assertWithPenalty' calls. A soft assertion
  is a hint to the SMT solver that we would like a particular condition to hold if **possible*.
  That is, if there is a solution satisfying it, then we would like it to hold, but it can be violated
  if there is no way to satisfy it. Each soft-assertion can be associated with a numeric penalty for
  not satisfying it, hence turning it into an optimization problem.

  Note that 'assertWithPenalty' works well with optimization goals ('minimize'/'maximize' etc.),
  and are most useful when we are optimizing a metric and thus some of the constraints
  can be relaxed with a penalty to obtain a good solution. Again
  see <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf>
  for a good overview of the features in Z3 that SBV is providing the bridge for.

  A soft assertion can be specified in one of the following three main ways:

       @
         'assertWithPenalty' "bounded_x" (x .< 5) 'DefaultPenalty'
         'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 2.3 Nothing
         'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 4.7 (Just "group-1") @

  In the first form, we are saying that the constraint @x .< 5@ must be satisfied, if possible,
  but if this constraint can not be satisfied to find a model, it can be violated with the default penalty of 1.

  In the second case, we are associating a penalty value of @2.3@.

  Finally in the third case, we are also associating this constraint with a group. The group
  name is only needed if we have classes of soft-constraints that should be considered together.

-}

{- $modelExtraction
The default 'Show' instances for prover calls provide all the counter-example information in a
human-readable form and should be sufficient for most casual uses of sbv. However, tools built
on top of sbv will inevitably need to look into the constructed models more deeply, programmatically
extracting their results and performing actions based on them. The API provided in this section
aims at simplifying this task.
-}

{- $resultTypes
t'ThmResult', t'SatResult', and t'AllSatResult' are simple newtype wrappers over t'SMTResult'. Their
main purpose is so that we can provide custom 'Show' instances to print results accordingly.
-}

{- $programmableExtraction
While default 'Show' instances are sufficient for most use cases, it is sometimes desirable (especially
for library construction) that the SMT-models are reinterpreted in terms of domain types. Programmable
extraction allows getting arbitrarily typed models out of SMT models.
-}

{- $moduleExportIntro
The SBV library exports the following modules wholesale, as user programs will have to import these
modules to make any sensible use of the SBV functionality.
-}

{- $createSym
These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms
for 'free' (specialized at the given type), but they might be easier to use. We provide both the named and anonymous
versions, latter with the underscore suffix.
-}

{- $createSyms
These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms
for 'mapM' 'free' (specialized at the given type), but they might be easier to use.
-}

{- $unboundedLimitations
The SBV library supports unbounded signed integers with the type 'SInteger', which are not subject to
overflow/underflow as it is the case with the bounded types, such as 'SWord8', 'SInt16', etc. However,
some bit-vector based operations are /not/ supported for the 'SInteger' type while in the verification mode. That
is, you can use these operations on 'SInteger' values during normal programming/simulation.
but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib.
Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size
bit-vectors. The operations that are restricted to bounded word/int sizes are:

   * Rotations and shifts: 'rotateL', 'rotateR', 'shiftL', 'shiftR'

   * Bitwise logical ops: '.&.', '.|.', 'xor', 'complement'

   * Extraction and concatenation: 'bvExtract', '#', 'zeroExtend', 'signExtend', 'bvDrop', and 'bvTake'

Usual arithmetic ('Prelude.+', 'Prelude.-', '*', 'sQuotRem', 'sQuot', 'sRem', 'sDivMod', 'sDiv', 'sMod') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are
supported for 'SInteger' fully, both in programming and verification modes.
-}

{- $algReals
Algebraic reals are roots of single-variable polynomials with rational coefficients. (See
<http://en.wikipedia.org/wiki/Algebraic_number>.) Note that algebraic reals are infinite
precision numbers, but they do not cover all /real/ numbers. (In particular, they cannot
represent transcendentals.) Some irrational numbers are algebraic (such as @sqrt 2@), while
others are not (such as pi and e).

SBV can deal with real numbers just fine, since the theory of reals is decidable. (See
<https://smt-lib.org/theories-Reals.shtml>.) In addition, by leveraging backend
solver capabilities, SBV can also represent and solve non-linear equations involving real-variables.
(For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)
-}

{- $floatingPoints
Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's
'Float' and 'Double' types. For SMT support with floating-point numbers, see the paper
by Rummer and Wahl: <http://www.philipp.ruemmer.org/publications/smt-fpa.pdf>.
-}

{- $strings
Support for characters, strings, and regular expressions (initial version contributed by Joel Burget)
adds support for QF_S logic, described here: <https://smt-lib.org/theories-UnicodeStrings.shtml>

See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for related functions.
-}

{- $lists
Support for symbolic lists (initial version contributed by Joel Burget) adds support for sequence support.

See "Data.SBV.List" for related functions.
-}

{- $tuples
Tuples can be used as symbolic values. This is useful in combination with lists, for example @SBV [(Integer, String)]@ is a valid type. These types can be arbitrarily nested, eg @SBV [(Integer, [(Char, (Integer, String))])]@. Instances of upto 8-tuples are provided.
-}

{- $shiftRotate
Symbolic words (both signed and unsigned) are an instance of Haskell's 'Bits' class, so regular
bitwise operations are automatically available for them. Shifts and rotates, however, require
specialized type-signatures since Haskell insists on an 'Int' second argument for them.
-}

{- $partitionIntro
The function 'allSatPartition' one to restrict the results returned by calls to 'Data.SBV.allSat'.
In certain cases, we might consider certain models to be "equivalent," i.e., we might want to
create equivalence classes over the search space when it comes to what we consider all satisfying
solutions. In these cases, we can use 'allSatPartition' tell SBV what classes of solutions to consider
as unique. Consider:

>>> :{
allSat $ do
   x <- sInteger "x"
   y <- sInteger "y"
   allSatPartition "p1" $ x .>= 0
   allSatPartition "p2" $ y .>= 0
:}
Solution #1:
  x  =     0 :: Integer
  y  =    -1 :: Integer
  p1 =  True :: Bool
  p2 = False :: Bool
Solution #2:
  x  =    -1 :: Integer
  y  =     0 :: Integer
  p1 = False :: Bool
  p2 =  True :: Bool
Solution #3:
  x  =    -1 :: Integer
  y  =    -1 :: Integer
  p1 = False :: Bool
  p2 = False :: Bool
Solution #4:
  x  =    0 :: Integer
  y  =    0 :: Integer
  p1 = True :: Bool
  p2 = True :: Bool
Found 4 different solutions.

Without the call to 'allSatPartition' the above example, 'allSat' would return all possible combinations of @x@ and @y@ subject to the constraints. (Since we have none here,
the call would try to enumerate the infinite set of all integer tuples!) But 'allSatPartition' us to restrict our attention to the examples that satisfy the partitioning
constraints. The first argument to 'allSatPartition' simply a name, for diagnostic purposes. Note that the conditions given by 'allSatPartition' /not/ imposed on the search
space at all: They're only used when we construct the search space. In the above example, we pick one example from each quadrant. Furthermore, while it is typical to pass
a boolean as a partitioning argument, it is not required: Any expression is OK, whose value creates the equivalence class:

>>> :{
allSat $ do
   x <- sInteger "x"
   allSatPartition "p" $ x `sMod` 3
:}
Solution #1:
  x = 2 :: Integer
  p = 2 :: Integer
Solution #2:
  x = 1 :: Integer
  p = 1 :: Integer
Solution #3:
  x = 0 :: Integer
  p = 0 :: Integer
Found 3 different solutions.

In the above, we get three examples, as the expression @x mod 3@ can take only three different values.
-}

{- $constrainIntro
A constraint is a means for restricting the input domain of a formula. Here's a simple
example:

@
   do x <- 'free' \"x\"
      y <- 'free' \"y\"
      'constrain' $ x .> y
      'constrain' $ x + y .>= 12
      'constrain' $ y .>= 3
      ...
@

The first constraint requires @x@ to be larger than @y@. The scond one says that
sum of @x@ and @y@ must be at least @12@, and the final one says that @y@ to be at least @3@.
Constraints provide an easy way to assert additional properties on the input domain, right at the point of
the introduction of variables.

Note that the proper reading of a constraint
depends on the context:

  * In a 'sat' (or 'allSat') call: The constraint added is asserted
    conjunctively. That is, the resulting satisfying model (if any) will
    always satisfy all the constraints given.

  * In a 'prove' call: In this case, the constraint acts as an implication.
    The property is proved under the assumption that the constraint
    holds. In other words, the constraint says that we only care about
    the input space that satisfies the constraint.

  * In a @quickCheck@ call: The constraint acts as a filter for @quickCheck@;
    if the constraint does not hold, then the input value is considered to be irrelevant
    and is skipped. Note that this is similar to 'prove', but is stronger: We do not
    accept a test case to be valid just because the constraints fail on them, although
    semantically the implication does hold. We simply skip that test case as a /bad/
    test vector.

  * In a 'Data.SBV.Tools.GenTest.genTest' call: Similar to @quickCheck@ and 'prove': If a constraint
    does not hold, the input value is ignored and is not included in the test
    set.
-}

{- $generalConstraints
A good use case (in fact the motivating use case) for 'constrain' is attaching a
constraint to a variable at the time of its creation.
Also, the conjunctive semantics for 'sat' and the implicative
semantics for 'prove' simplify programming by choosing the correct interpretation
automatically. However, one should be aware of the semantic difference. For instance, in
the presence of constraints, formulas that are /provable/ are not necessarily
/satisfiable/. To wit, consider:

 @
    do x <- 'free' \"x\"
       'constrain' $ x .< x
       return $ x .< (x :: 'SWord8')
 @

This predicate is unsatisfiable since no element of 'SWord8' is less than itself. But
it's (vacuously) true, since it excludes the entire domain of values, thus making the proof
trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given
constraints are not vacuous, the functions 'isVacuousProof' (and 'isVacuousProofWith') can be used.

Also note that this semantics imply that test case generation ('Data.SBV.Tools.GenTest.genTest') and
quick-check can take arbitrarily long in the presence of constraints, if the random input values generated
rarely satisfy the constraints. (As an extreme case, consider @'constrain' 'sFalse'@.)
-}

{- $quantifiers
You can write quantified formulas, and reason with them as in first-order logic. Here is a simple example:

@
    constrain $ \\(Forall x) (Exists y) -> y .> (x :: SInteger)
@

You can nest quantifiers as you wish, and the quantified parameters can be of arbitrary symbolic type.
Additionally, you can convert such a quantified formula to a regular boolean, via a call to 'quantifiedBool'
function, essentially performing quantifier elimination:

@
    other_condition .&& quantifiedBool (\\(Forall x) (Exists y) -> y .> (x :: SInteger))
@

Or you can prove/sat quantified formulas directly:

@
    prove $ \\(Forall x) (Exists y) -> y .> (x :: SInteger)
@

This facility makes quantifiers part of the regular SBV language, allowing them to be mixed/matched with all
your other symbolic computations.  See the following files demonstrating reasoning with quantifiers:

   * "Documentation.SBV.Examples.Puzzles.Birthday"
   * "Documentation.SBV.Examples.Puzzles.KnightsAndKnaves"
   * "Documentation.SBV.Examples.Puzzles.Rabbits"
   * "Documentation.SBV.Examples.Misc.FirstOrderLogic"

SBV also supports the constructors t'ExistsUnique' to create unique existentials, in addition
to t'ForallN' and t'ExistsN' for creating multiple variables at the same time.

In general, SBV will not display the values of quantified variables for a satisfying instance.
For a satisfiability problem, you can apply skolemization manually to have these values
computed by the backend solver. Note that skolemization will produce functions for
existentials under universals, and SBV generally cannot translate function values back
to Haskell, except in certain simple cases. However, for prefix existentials, the manual
transformation can pay off. As an example, compare:

>>> sat $ \(Exists x) (Forall y) -> x .<= (y :: SWord8)
Satisfiable

to:

>>> sat $ do { x <- free "x"; pure (quantifiedBool (\(Forall y) -> x .<= (y :: SWord8))) }
Satisfiable. Model:
  x = 0 :: Word8

where we have skolemized the top-level existential out, and received a witness value for it.
-}

{- $constraintVacuity

When adding constraints, one has to be careful about
making sure they are not inconsistent. The function 'isVacuousProof' can be used for this purpose.
Here is an example. Consider the following predicate:

    >>> let pred = do { x <- free "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }

This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the
values considered satisfy @x .< x@, i.e., they are less than themselves. Since there are no values that
satisfy this constraint, the proof will pass vacuously:

    >>> prove pred
    Q.E.D.

We can use 'isVacuousProof' to make sure to see that the pass was vacuous:

    >>> isVacuousProof pred
    True

While the above example is trivial, things can get complicated if there are multiple constraints with
non-straightforward relations; so if constraints are used one should make sure to check the predicate
is not vacuously true. Here's an example that is not vacuous:

     >>> let pred' = do { x <- free "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }

This time the proof passes as expected:

     >>> prove pred'
     Q.E.D.

And the proof is not vacuous:

     >>> isVacuousProof pred'
     False
-}

{- $namedConstraints

Constraints can be given names:

  @ 'namedConstraint' "a is at least 5" $ a .>= 5@

Similarly, arbitrary term attributes can also be associated:

  @ 'constrainWithAttribute' [(":solver-specific-attribute", "value")] $ a .>= 5@

Note that a 'namedConstraint' is equivalent to a 'constrainWithAttribute' call, setting the `":named"' attribute.
-}

{- $unsatCores
Named constraints are useful when used in conjunction with 'Data.SBV.Control.getUnsatCore' function
where the backend solver can be queried to obtain an unsat core in case the constraints are unsatisfiable.
See 'Data.SBV.Control.getUnsatCore' for details and "Documentation.SBV.Examples.Queries.UnsatCore" for an example use case.
-}

{- $uninterpreted
Users can introduce new uninterpreted sorts simply by defining an empty data-type in Haskell and registering it as such. The
following example demonstrates:

  @
     data B
     mkUninterpretedSort ''B
  @

(Note that you'll also need to use pragmas @TemplateHaskell@, @StandAloneDeriving@, @DeriveDataTypeable@, and @DeriveAnyClass@ for this to work, follow GHC's error messages!)

This is all it takes to introduce @B@ as an uninterpreted sort in SBV, which makes the type @SBV B@ automagically become available as the type
of symbolic values that ranges over @B@ values. Note that this will also introduce the type @SB@ into your environment, which is a synonym
for @SBV B@.


Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by
the 'Data.SBV.Core.Model.SMTDefinable' class.
-}

{- $enumerations
If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then
you can use the 'mkSymbolicEnumeration' function to turn it into an enumeration in SMTLib.
A simple example is:

@
    data X = A | B | C
    mkSymbolicEnumeration ''X
@

Note the magic incantation @mkSymbolicEnumeration ''X@. For this to work, you need to have the following
options turned on:

>   LANGUAGE TemplateHaskell
>   LANGUAGE StandaloneDeriving
>   LANGUAGE DeriveDataTypeable
>   LANGUAGE DeriveAnyClass

The declaration will automatically introduce the type:

@
    type SX = SBV X
@

along with symbolic values of each of the enumerated values @sA@, @sB@, and @sC@. This way,
you can refer to the symbolic version as @SX@, treating it as a regular symbolic type ranging over the values @A@, @B@, and @C@. Such values can be compared for equality, and with the usual
other comparison operators, such as @.==@, @./=@, @.>@, @.>=@, @<@, and @<=@. For each enumerated value @X@, the symbolic versions @sX@ is defined to be equal to @literal X@.

A simple query would look like:

@
     allSat $ \x -> x .== (x :: SX)
@

which would list all three elements of this domain as satisfying solutions.

@
     Solution #1:
       s0 = A :: X
     Solution #2:
       s0 = B :: X
     Solution #3:
       s0 = C :: X
     Found 3 different solutions.
@

Note that the result is properly typed as @X@ elements; these are not mere strings.

See "Documentation.SBV.Examples.Misc.Enumerate" for an extended example on how to use symbolic enumerations.
-}

{- $cardIntro
A pseudo-boolean function (<http://en.wikipedia.org/wiki/Pseudo-Boolean_function>) is a
function from booleans to reals, basically treating 'True' as @1@ and 'False' as @0@. They
are typically expressed in polynomial form. Such functions can be used to express cardinality
constraints, where we want to /count/ how many things satisfy a certain condition.

One can code such constraints using regular SBV programming: Simply
walk over the booleans and the corresponding coefficients, and assert the required relation.
For instance:

   > [b0, b1, b2, b3] `pbAtMost` 2

is precisely equivalent to:

   > sum (map (\b -> ite b 1 0) [b0, b1, b2, b3]) .<= 2

and they both express that at most /two/ of @b0@, @b1@, @b2@, and @b3@ can be 'sTrue'.
However, the equivalent forms give rise to long formulas and the cardinality constraint
can get lost in the translation. The idea here is that if you use these functions instead, SBV will
produce better translations to SMTLib for more efficient solving of cardinality constraints, assuming
the backend solver supports them. Currently, only Z3 supports pseudo-booleans directly. For all other solvers,
SBV will translate these to equivalent terms that do not require special functions.
-}

{- $verbosity

SBV provides various levels of verbosity to aid in debugging, by using the t'SMTConfig' fields:

  * ['verbose'] Print on stdout a shortened account of what is sent/received. This is specifically trimmed to reduce noise
    and is good for quick debugging. The output is not supposed to be machine-readable.
  * ['redirectVerbose'] Send the verbose output to a file. Note that you still have to set `verbose=True` for redirection to
    take effect. Otherwise, the output is the same as what you would see in `verbose`.
  * ['transcript'] Produce a file that is valid SMTLib2 format, containing everything sent and received. In particular, one can
    directly feed this file to the SMT-solver outside of the SBV since it is machine-readable. This is good for offline analysis
    situations, where you want to have a full account of what happened. For instance, it will print time-stamps at every interaction
    point, so you can see how long each command took.
-}

{- $observeInternal

The 'observe' command can be used to trace values of arbitrary expressions during a 'sat', 'prove', or perhaps more
importantly, in a @quickCheck@ call with the 'sObserve' variant.. This is useful for, for instance, recording expected vs. obtained expressions
as a symbolic program is executing.

>>> :{
prove $ do a1 <- free "i1"
           a2 <- free "i2"
           let spec, res :: SWord8
               spec = a1 + a2
               res  = ite (a1 .== 12 .&& a2 .== 22)   -- insert a malicious bug!
                          1
                          (a1 + a2)
           return $ observe "Expected" spec .== observe "Result" res
:}
Falsifiable. Counter-example:
  i1       = 12 :: Word8
  i2       = 22 :: Word8
  Expected = 34 :: Word8
  Result   =  1 :: Word8

The 'observeIf' variant allows the user to specify a boolean condition when the value is interesting to observe. Useful when
you have lots of "debugging" points, but not all are of interest. Use the 'sObserve' variant when you are at the 'Symbolic'
monad, which also supports quick-check applications.
-}

{- $distinctNote
Symbolic equality provides the notion of what it means to be equal, similar to Haskell's 'Eq' class, except allowing comparison of
symbolic values. The methods are '.==' and './=', returning 'SBool' results. We also provide a notion of strong equality ('.===' and './=='),
which is useful for floating-point value comparisons as it deals more uniformly with @NaN@ and positive/negative zeros. Additionally, we
provide 'distinct' that can be used to assert all elements of a list are different from each other, and 'distinctExcept' which is similar
to 'distinct' but allows for certain values to be considered different. These latter two functions are useful in modeling a variety of
puzzles and cardinality constraints:

>>> prove $ \a -> distinctExcept [a, a] [0::SInteger] .<=> a .== 0
Q.E.D.
>>> prove $ \a b -> distinctExcept [a, b] [0::SWord8] .<=> (a .== b .=> a .== 0)
Q.E.D.
>>> prove $ \a b c d -> distinctExcept [a, b, c, d] [] .== distinct [a, b, c, (d::SInteger)]
Q.E.D.
-}

{- $euclidianNote
=== Euclidian division and modulus

Euclidian division and modulus for integers differ from regular division modulus when
the divisor is negative. It satisfies the following desirable property: For any @m@, @n@, we have:

@
  Given @m@, @n@, s.t., n /= 0
  Let (q, r) = m `sEDivMod` n
  Then: m = n * q + r
   and 0 <= r <= |n| - 1
@

That is, the modulus is always positive.
There's no standard Haskell function that performs this operation. The main reason to prefer this
function is that SMT solvers can deal with them better.
Compare:

>>> sDivMod @SInteger 3 (-2)
(-2 :: SInteger,-1 :: SInteger)
>>> sEDivMod 3 (-2)
(-1 :: SInteger,1 :: SInteger)
>>> prove $ \x y -> y .> 0 .=> x `sDivMod` y .== x `sEDivMod` y
Q.E.D.
-}

{- $conversionNote
Capture convertability from/to FloatingPoint representations.

Conversions to float: 'toSFloat' and 'toSDouble' simply return the
nearest representable float from the given type based on the rounding
mode provided. Similarly, 'toSFloatingPoint' converts to a generalized
floating-point number with specified exponent and significand bith widths.

Conversions from float: 'fromSFloat', 'fromSDouble', 'fromSFloatingPoint' functions do
the reverse conversion. However some care is needed when given values
that are not representable in the integral target domain. For instance,
converting an 'SFloat' to an 'SInt8' is problematic. The rules are as follows:

If the input value is a finite point and when rounded in the given rounding mode to an
integral value lies within the target bounds, then that result is returned.
(This is the regular interpretation of rounding in IEEE754.)

Otherwise (i.e., if the integral value in the float or double domain) doesn't
fit into the target type, then the result is unspecified. Note that if the input
is @+oo@, @-oo@, or @NaN@, then the result is unspecified.

Due to the unspecified nature of conversions, SBV will never constant fold
conversions from floats to integral values. That is, you will always get a
symbolic value as output. (Conversions from floats to other floats will be
constant folded. Conversions from integral values to floats will also be
constant folded.)

Note that unspecified really means unspecified: In particular, SBV makes
no guarantees about matching the behavior between what you might get in
Haskell, via SMT-Lib, or the C-translation. If the input value is out-of-bounds
as defined above, or is @NaN@ or @oo@ or @-oo@, then all bets are off. In particular
C and SMTLib are decidedly undefine this case, though that doesn't mean they do the
same thing! Same goes for Haskell, which seems to convert via Int64, but we do
not model that behavior in SBV as it doesn't seem to be intentional nor well documented.

You can check for @NaN@, @oo@ and @-oo@, using the predicates 'fpIsNaN', 'fpIsInfinite',
and 'fpIsPositive', 'fpIsNegative' predicates, respectively; and do the proper conversion
based on your needs. (0 is a good choice, as are min/max bounds of the target type.)

Currently, SBV provides no predicates to check if a value would lie within range for a
particular conversion task, as this depends on the rounding mode and the types involved
and can be rather tricky to determine. (See <http://github.com/LeventErkok/sbv/issues/456>
for a discussion of the issues involved.) In a future release, we hope to be able to
provide underflow and overflow predicates for these conversions as well.

Some examples to illustrate the behavior follows:

>>> :{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
roundTrip m x = fromSFloat m (toSFloat m x) .== x
:}

>>> prove $ roundTrip @Int8
Q.E.D.
>>> prove $ roundTrip @Word8
Q.E.D.
>>> prove $ roundTrip @Int16
Q.E.D.
>>> prove $ roundTrip @Word16
Q.E.D.
>>> prove $ roundTrip @Int32
Falsifiable. Counter-example:
  s0 = RoundTowardPositive :: RoundingMode
  s1 =          1104019333 :: Int32

Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float:

>>> toRational (1104019333 :: Float)
1104019328 % 1

Note how the numerator is different, it is off by 5. This is hardly surprising, since floats become sparser as
the magnitude increases to be able to cover all the integer values representable.

>>> :{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
roundTrip m x = fromSDouble m (toSDouble m x) .== x
:}

>>> prove $ roundTrip @Int8
Q.E.D.
>>> prove $ roundTrip @Word8
Q.E.D.
>>> prove $ roundTrip @Int16
Q.E.D.
>>> prove $ roundTrip @Word16
Q.E.D.
>>> prove $ roundTrip @Int32
Q.E.D.
>>> prove $ roundTrip @Word32
Q.E.D.
>>> prove $ roundTrip @Int64
Falsifiable. Counter-example:
  s0 = RoundNearestTiesToEven :: RoundingMode
  s1 =   -2305843042984656748 :: Int64

Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the
integer value for all possible values:

>>> toRational (fromIntegral (-2305843042984656748 :: Int64) :: Double)
(-2305843042984656896) % 1

In this case the numerator is off by 148.
-}

-- | An implementation of rotate-left, using a barrel shifter like design. Only works when both
-- arguments are finite bitvectors, and furthermore when the second argument is unsigned.
-- The first condition is enforced by the type, but the second is dynamically checked.
-- We provide this implementation as an alternative to `sRotateLeft` since SMTLib logic
-- does not support variable argument rotates (as opposed to shifts), and thus this
-- implementation can produce better code for verification compared to `sRotateLeft`.
--
-- >>> prove $ \x y -> (x `sBarrelRotateLeft`  y) `sBarrelRotateRight` (y :: SWord32) .== (x :: SWord64)
-- Q.E.D.
sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
sBarrelRotateLeft :: forall a b.
(SFiniteBits a, SFiniteBits b) =>
SBV a -> SBV b -> SBV a
sBarrelRotateLeft = SBV a -> SBV b -> SBV a
forall a b.
(SFiniteBits a, SFiniteBits b) =>
SBV a -> SBV b -> SBV a
M.sBarrelRotateLeft

-- | An implementation of rotate-right, using a barrel shifter like design. See comments
-- for `sBarrelRotateLeft` for details.
--
-- >>> prove $ \x y -> (x `sBarrelRotateRight` y) `sBarrelRotateLeft`  (y :: SWord32) .== (x :: SWord64)
-- Q.E.D.
sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
sBarrelRotateRight :: forall a b.
(SFiniteBits a, SFiniteBits b) =>
SBV a -> SBV b -> SBV a
sBarrelRotateRight = SBV a -> SBV b -> SBV a
forall a b.
(SFiniteBits a, SFiniteBits b) =>
SBV a -> SBV b -> SBV a
M.sBarrelRotateRight

-- | Extract a portion of bits to form a smaller bit-vector.
--
-- >>> prove $ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
-- Q.E.D.
bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                                    , KnownNat i
                                    , KnownNat j
                                    , i + 1 <= n
                                    , j <= i
                                    , BVIsNonZero (i - j + 1)
                                    ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@
                                      -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold
                                      -> SBV (bv n)             -- ^ Input bit vector of size @n@
                                      -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@
bvExtract :: forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract = proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
CD.bvExtract

-- | Join two bitvectors.
--
-- >>> prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))
-- Q.E.D.
(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)
       , KnownNat m, BVIsNonZero m, SymVal (bv m)
       ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side
         -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side
         -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@
# :: forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
(#) = SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
(CD.#)
infixr 5 #

-- | Zero extend a bit-vector.
--
-- >>> prove $ \x -> bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0
-- Q.E.D.
zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                             , KnownNat m, BVIsNonZero m, SymVal (bv m)
                             , n + 1 <= m
                             , SIntegral (bv (m - n))
                             , BVIsNonZero (m - n)
                             ) => SBV (bv n)    -- ^ Input, of size @n@
                               -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold
zeroExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
 BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
zeroExtend = SBV (bv n) -> SBV (bv m)
forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
 BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
M.zeroExtend

-- | Sign extend a bit-vector.
--
-- >>> prove $ \x -> sNot (msb x) .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== 0
-- Q.E.D.
-- >>> prove $ \x ->       msb x  .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0
-- Q.E.D.
signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                             , KnownNat m, BVIsNonZero m, SymVal (bv m)
                             , n + 1 <= m
                             , SFiniteBits (bv n)
                             , SIntegral   (bv (m - n))
                             , BVIsNonZero (m - n)
                             ) => SBV (bv n)  -- ^ Input, of size @n@
                               -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold
signExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
 SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
signExtend = SBV (bv n) -> SBV (bv m)
forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
 SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
M.signExtend

-- | Drop bits from the top of a bit-vector.
--
-- >>> prove $ \x -> bvDrop (Proxy @0) (x :: SWord 43) .== x
-- Q.E.D.
-- >>> prove $ \x -> bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 (0 :: SWord 1)
-- Q.E.D.
bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n
                                 , KnownNat i
                                 , i + 1 <= n
                                 , i + m - n <= 0
                                 , BVIsNonZero (n - i)
                                 ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.
                                   -> SBV (bv n)                 -- ^ Input, of size @n@
                                   -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.
bvDrop :: forall (i :: Nat) (n :: Nat) (m :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n,
 ((i + m) - n) <= 0, BVIsNonZero (n - i)) =>
proxy i -> SBV (bv n) -> SBV (bv m)
bvDrop = proxy i -> SBV (bv n) -> SBV (bv m)
forall (i :: Nat) (n :: Nat) (m :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n,
 ((i + m) - n) <= 0, BVIsNonZero (n - i)) =>
proxy i -> SBV (bv n) -> SBV (bv m)
CD.bvDrop

-- | Take bits from the top of a bit-vector.
--
-- >>> prove $ \x -> bvTake (Proxy @13) (x :: SWord 13) .== x
-- Q.E.D.
-- >>> prove $ \x -> bvTake (Proxy @1) (x :: SWord 13) .== ite (msb x) 1 0
-- Q.E.D.
-- >>> prove $ \x -> bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23)
-- Q.E.D.
bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n
                               , KnownNat i, BVIsNonZero i
                               , i <= n
                               ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.
                                 -> SBV (bv n)               -- ^ Input, of size @n@
                                 -> SBV (bv i)               -- ^ Output, of size @i@
bvTake :: forall (i :: Nat) (n :: Nat) (bv :: Nat -> *) (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n) =>
proxy i -> SBV (bv n) -> SBV (bv i)
bvTake = proxy i -> SBV (bv n) -> SBV (bv i)
forall (i :: Nat) (n :: Nat) (bv :: Nat -> *) (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n) =>
proxy i -> SBV (bv n) -> SBV (bv i)
CD.bvTake

-- | A helper class to convert sized bit-vectors to/from bytes.
class ByteConverter a where
   -- | Convert to a sequence of bytes
   --
   -- >>> prove $ \a b c d -> toBytes ((fromBytes [a, b, c, d]) :: SWord 32) .== [a, b, c, d]
   -- Q.E.D.
   toBytes   :: a -> [SWord 8]

   -- | Convert from a sequence of bytes
   --
   -- >>> prove $ \r -> fromBytes (toBytes r) .== (r :: SWord 64)
   -- Q.E.D.
   fromBytes :: [SWord 8] -> a

-- NB. The following instances are automatically generated by buildUtils/genByteConverter.hs
-- It is possible to write these more compactly indeed, but this explicit form generates
-- better C code, and hence we allow the verbosity here.

-- | 'SWord' 8 instance for 'ByteConverter'
instance ByteConverter (SWord 8) where
   toBytes :: SWord 8 -> [SWord 8]
toBytes SWord 8
a = [SWord 8
a]

   fromBytes :: [SWord 8] -> SWord 8
fromBytes [SWord 8
x] = SWord 8
x
   fromBytes [SWord 8]
as  = String -> SWord 8
forall a. HasCallStack => String -> a
error (String -> SWord 8) -> String -> SWord 8
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 8: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as)

-- | 'SWord' 16 instance for 'ByteConverter'
instance ByteConverter (SWord 16) where
   toBytes :: SWord 16 -> [SWord 8]
toBytes SWord 16
a = [ Proxy 15 -> Proxy 8 -> SWord 16 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @15) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @8) SWord 16
a
               , Proxy 7 -> Proxy 0 -> SWord 16 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @7) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @0) SWord 16
a
               ]

   fromBytes :: [SWord 8] -> SWord 16
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
     = ([SWord 8] -> SWord 8
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 8) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
1 [SWord 8]
as) SWord 8 -> SWord 8 -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 8
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
1 [SWord 8]
as)
     | Bool
True
     = String -> SWord 16
forall a. HasCallStack => String -> a
error (String -> SWord 16) -> String -> SWord 16
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 16: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 32 instance for 'ByteConverter'
instance ByteConverter (SWord 32) where
   toBytes :: SWord 32 -> [SWord 8]
toBytes SWord 32
a = [ Proxy 31 -> Proxy 24 -> SWord 32 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @31) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @24) SWord 32
a, Proxy 23 -> Proxy 16 -> SWord 32 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @23) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @16) SWord 32
a, Proxy 15 -> Proxy 8 -> SWord 32 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @15) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @8) SWord 32
a, Proxy 7 -> Proxy 0 -> SWord 32 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @7) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @0) SWord 32
a
               ]

   fromBytes :: [SWord 8] -> SWord 32
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4
     = ([SWord 8] -> SWord 16
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 16) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
2 [SWord 8]
as) SWord 16 -> SWord 16 -> SBV (WordN (16 + 16))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 16
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
2 [SWord 8]
as)
     | Bool
True
     = String -> SWord 32
forall a. HasCallStack => String -> a
error (String -> SWord 32) -> String -> SWord 32
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 32: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 64 instance for 'ByteConverter'
instance ByteConverter (SWord 64) where
   toBytes :: SWord 64 -> [SWord 8]
toBytes SWord 64
a = [ Proxy 63 -> Proxy 56 -> SWord 64 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @63) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @56) SWord 64
a, Proxy 55 -> Proxy 48 -> SWord 64 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @55) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @48) SWord 64
a, Proxy 47 -> Proxy 40 -> SWord 64 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @47) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @40) SWord 64
a, Proxy 39 -> Proxy 32 -> SWord 64 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @39) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @32) SWord 64
a
               , Proxy 31 -> Proxy 24 -> SWord 64 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @31) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @24) SWord 64
a, Proxy 23 -> Proxy 16 -> SWord 64 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @23) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @16) SWord 64
a, Proxy 15 -> Proxy 8 -> SWord 64 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @15) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @8) SWord 64
a, Proxy 7 -> Proxy 0 -> SWord 64 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @7) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @0) SWord 64
a
               ]

   fromBytes :: [SWord 8] -> SWord 64
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8
     = ([SWord 8] -> SWord 32
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 32) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
4 [SWord 8]
as) SWord 32 -> SWord 32 -> SBV (WordN (32 + 32))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 32
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
4 [SWord 8]
as)
     | Bool
True
     = String -> SWord 64
forall a. HasCallStack => String -> a
error (String -> SWord 64) -> String -> SWord 64
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 64: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 128 instance for 'ByteConverter'
instance ByteConverter (SWord 128) where
   toBytes :: SWord 128 -> [SWord 8]
toBytes SWord 128
a = [ Proxy 127
-> Proxy 120 -> SWord 128 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @127) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @120) SWord 128
a, Proxy 119
-> Proxy 112 -> SWord 128 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @119) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @112) SWord 128
a, Proxy 111
-> Proxy 104 -> SWord 128 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @111) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @104) SWord 128
a, Proxy 103 -> Proxy 96 -> SWord 128 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @103) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @96) SWord 128
a
               , Proxy 95 -> Proxy 88 -> SWord 128 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @95) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @88) SWord 128
a, Proxy 87 -> Proxy 80 -> SWord 128 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @87) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @80) SWord 128
a, Proxy 79 -> Proxy 72 -> SWord 128 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @79) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @72) SWord 128
a, Proxy 71 -> Proxy 64 -> SWord 128 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @71) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @64) SWord 128
a
               , Proxy 63 -> Proxy 56 -> SWord 128 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @63) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @56) SWord 128
a, Proxy 55 -> Proxy 48 -> SWord 128 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @55) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @48) SWord 128
a, Proxy 47 -> Proxy 40 -> SWord 128 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @47) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @40) SWord 128
a, Proxy 39 -> Proxy 32 -> SWord 128 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @39) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @32) SWord 128
a
               , Proxy 31 -> Proxy 24 -> SWord 128 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @31) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @24) SWord 128
a, Proxy 23 -> Proxy 16 -> SWord 128 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @23) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @16) SWord 128
a, Proxy 15 -> Proxy 8 -> SWord 128 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @15) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @8) SWord 128
a, Proxy 7 -> Proxy 0 -> SWord 128 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @7) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @0) SWord 128
a
               ]

   fromBytes :: [SWord 8] -> SWord 128
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
16
     = ([SWord 8] -> SWord 64
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 64) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
8 [SWord 8]
as) SWord 64 -> SWord 64 -> SBV (WordN (64 + 64))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 64
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
8 [SWord 8]
as)
     | Bool
True
     = String -> SWord 128
forall a. HasCallStack => String -> a
error (String -> SWord 128) -> String -> SWord 128
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 128: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 256 instance for 'ByteConverter'
instance ByteConverter (SWord 256) where
   toBytes :: SWord 256 -> [SWord 8]
toBytes SWord 256
a = [ Proxy 255
-> Proxy 248 -> SWord 256 -> SBV (WordN ((255 - 248) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @255) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @248) SWord 256
a, Proxy 247
-> Proxy 240 -> SWord 256 -> SBV (WordN ((247 - 240) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @247) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @240) SWord 256
a, Proxy 239
-> Proxy 232 -> SWord 256 -> SBV (WordN ((239 - 232) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @239) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @232) SWord 256
a, Proxy 231
-> Proxy 224 -> SWord 256 -> SBV (WordN ((231 - 224) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @231) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @224) SWord 256
a
               , Proxy 223
-> Proxy 216 -> SWord 256 -> SBV (WordN ((223 - 216) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @223) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @216) SWord 256
a, Proxy 215
-> Proxy 208 -> SWord 256 -> SBV (WordN ((215 - 208) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @215) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @208) SWord 256
a, Proxy 207
-> Proxy 200 -> SWord 256 -> SBV (WordN ((207 - 200) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @207) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @200) SWord 256
a, Proxy 199
-> Proxy 192 -> SWord 256 -> SBV (WordN ((199 - 192) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @199) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @192) SWord 256
a
               , Proxy 191
-> Proxy 184 -> SWord 256 -> SBV (WordN ((191 - 184) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @191) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @184) SWord 256
a, Proxy 183
-> Proxy 176 -> SWord 256 -> SBV (WordN ((183 - 176) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @183) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @176) SWord 256
a, Proxy 175
-> Proxy 168 -> SWord 256 -> SBV (WordN ((175 - 168) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @175) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @168) SWord 256
a, Proxy 167
-> Proxy 160 -> SWord 256 -> SBV (WordN ((167 - 160) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @167) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @160) SWord 256
a
               , Proxy 159
-> Proxy 152 -> SWord 256 -> SBV (WordN ((159 - 152) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @159) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @152) SWord 256
a, Proxy 151
-> Proxy 144 -> SWord 256 -> SBV (WordN ((151 - 144) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @151) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @144) SWord 256
a, Proxy 143
-> Proxy 136 -> SWord 256 -> SBV (WordN ((143 - 136) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @143) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @136) SWord 256
a, Proxy 135
-> Proxy 128 -> SWord 256 -> SBV (WordN ((135 - 128) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @135) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @128) SWord 256
a
               , Proxy 127
-> Proxy 120 -> SWord 256 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @127) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @120) SWord 256
a, Proxy 119
-> Proxy 112 -> SWord 256 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @119) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @112) SWord 256
a, Proxy 111
-> Proxy 104 -> SWord 256 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @111) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @104) SWord 256
a, Proxy 103 -> Proxy 96 -> SWord 256 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @103) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @96) SWord 256
a
               , Proxy 95 -> Proxy 88 -> SWord 256 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @95) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @88) SWord 256
a, Proxy 87 -> Proxy 80 -> SWord 256 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @87) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @80) SWord 256
a, Proxy 79 -> Proxy 72 -> SWord 256 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @79) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @72) SWord 256
a, Proxy 71 -> Proxy 64 -> SWord 256 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @71) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @64) SWord 256
a
               , Proxy 63 -> Proxy 56 -> SWord 256 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @63) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @56) SWord 256
a, Proxy 55 -> Proxy 48 -> SWord 256 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @55) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @48) SWord 256
a, Proxy 47 -> Proxy 40 -> SWord 256 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @47) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @40) SWord 256
a, Proxy 39 -> Proxy 32 -> SWord 256 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @39) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @32) SWord 256
a
               , Proxy 31 -> Proxy 24 -> SWord 256 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @31) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @24) SWord 256
a, Proxy 23 -> Proxy 16 -> SWord 256 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @23) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @16) SWord 256
a, Proxy 15 -> Proxy 8 -> SWord 256 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @15) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @8) SWord 256
a, Proxy 7 -> Proxy 0 -> SWord 256 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @7) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @0) SWord 256
a
               ]

   fromBytes :: [SWord 8] -> SWord 256
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
32
     = ([SWord 8] -> SWord 128
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 128) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
16 [SWord 8]
as) SWord 128 -> SWord 128 -> SBV (WordN (128 + 128))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 128
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
16 [SWord 8]
as)
     | Bool
True
     = String -> SWord 256
forall a. HasCallStack => String -> a
error (String -> SWord 256) -> String -> SWord 256
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 256: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 512 instance for 'ByteConverter'
instance ByteConverter (SWord 512) where
   toBytes :: SWord 512 -> [SWord 8]
toBytes SWord 512
a = [ Proxy 511
-> Proxy 504 -> SWord 512 -> SBV (WordN ((511 - 504) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @511) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @504) SWord 512
a, Proxy 503
-> Proxy 496 -> SWord 512 -> SBV (WordN ((503 - 496) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @503) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @496) SWord 512
a, Proxy 495
-> Proxy 488 -> SWord 512 -> SBV (WordN ((495 - 488) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @495) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @488) SWord 512
a, Proxy 487
-> Proxy 480 -> SWord 512 -> SBV (WordN ((487 - 480) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @487) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @480) SWord 512
a
               , Proxy 479
-> Proxy 472 -> SWord 512 -> SBV (WordN ((479 - 472) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @479) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @472) SWord 512
a, Proxy 471
-> Proxy 464 -> SWord 512 -> SBV (WordN ((471 - 464) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @471) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @464) SWord 512
a, Proxy 463
-> Proxy 456 -> SWord 512 -> SBV (WordN ((463 - 456) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @463) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @456) SWord 512
a, Proxy 455
-> Proxy 448 -> SWord 512 -> SBV (WordN ((455 - 448) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @455) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @448) SWord 512
a
               , Proxy 447
-> Proxy 440 -> SWord 512 -> SBV (WordN ((447 - 440) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @447) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @440) SWord 512
a, Proxy 439
-> Proxy 432 -> SWord 512 -> SBV (WordN ((439 - 432) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @439) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @432) SWord 512
a, Proxy 431
-> Proxy 424 -> SWord 512 -> SBV (WordN ((431 - 424) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @431) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @424) SWord 512
a, Proxy 423
-> Proxy 416 -> SWord 512 -> SBV (WordN ((423 - 416) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @423) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @416) SWord 512
a
               , Proxy 415
-> Proxy 408 -> SWord 512 -> SBV (WordN ((415 - 408) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @415) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @408) SWord 512
a, Proxy 407
-> Proxy 400 -> SWord 512 -> SBV (WordN ((407 - 400) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @407) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @400) SWord 512
a, Proxy 399
-> Proxy 392 -> SWord 512 -> SBV (WordN ((399 - 392) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @399) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @392) SWord 512
a, Proxy 391
-> Proxy 384 -> SWord 512 -> SBV (WordN ((391 - 384) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @391) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @384) SWord 512
a
               , Proxy 383
-> Proxy 376 -> SWord 512 -> SBV (WordN ((383 - 376) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @383) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @376) SWord 512
a, Proxy 375
-> Proxy 368 -> SWord 512 -> SBV (WordN ((375 - 368) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @375) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @368) SWord 512
a, Proxy 367
-> Proxy 360 -> SWord 512 -> SBV (WordN ((367 - 360) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @367) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @360) SWord 512
a, Proxy 359
-> Proxy 352 -> SWord 512 -> SBV (WordN ((359 - 352) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @359) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @352) SWord 512
a
               , Proxy 351
-> Proxy 344 -> SWord 512 -> SBV (WordN ((351 - 344) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @351) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @344) SWord 512
a, Proxy 343
-> Proxy 336 -> SWord 512 -> SBV (WordN ((343 - 336) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @343) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @336) SWord 512
a, Proxy 335
-> Proxy 328 -> SWord 512 -> SBV (WordN ((335 - 328) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @335) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @328) SWord 512
a, Proxy 327
-> Proxy 320 -> SWord 512 -> SBV (WordN ((327 - 320) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @327) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @320) SWord 512
a
               , Proxy 319
-> Proxy 312 -> SWord 512 -> SBV (WordN ((319 - 312) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @319) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @312) SWord 512
a, Proxy 311
-> Proxy 304 -> SWord 512 -> SBV (WordN ((311 - 304) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @311) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @304) SWord 512
a, Proxy 303
-> Proxy 296 -> SWord 512 -> SBV (WordN ((303 - 296) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @303) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @296) SWord 512
a, Proxy 295
-> Proxy 288 -> SWord 512 -> SBV (WordN ((295 - 288) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @295) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @288) SWord 512
a
               , Proxy 287
-> Proxy 280 -> SWord 512 -> SBV (WordN ((287 - 280) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @287) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @280) SWord 512
a, Proxy 279
-> Proxy 272 -> SWord 512 -> SBV (WordN ((279 - 272) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @279) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @272) SWord 512
a, Proxy 271
-> Proxy 264 -> SWord 512 -> SBV (WordN ((271 - 264) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @271) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @264) SWord 512
a, Proxy 263
-> Proxy 256 -> SWord 512 -> SBV (WordN ((263 - 256) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @263) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @256) SWord 512
a
               , Proxy 255
-> Proxy 248 -> SWord 512 -> SBV (WordN ((255 - 248) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @255) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @248) SWord 512
a, Proxy 247
-> Proxy 240 -> SWord 512 -> SBV (WordN ((247 - 240) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @247) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @240) SWord 512
a, Proxy 239
-> Proxy 232 -> SWord 512 -> SBV (WordN ((239 - 232) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @239) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @232) SWord 512
a, Proxy 231
-> Proxy 224 -> SWord 512 -> SBV (WordN ((231 - 224) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @231) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @224) SWord 512
a
               , Proxy 223
-> Proxy 216 -> SWord 512 -> SBV (WordN ((223 - 216) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @223) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @216) SWord 512
a, Proxy 215
-> Proxy 208 -> SWord 512 -> SBV (WordN ((215 - 208) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @215) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @208) SWord 512
a, Proxy 207
-> Proxy 200 -> SWord 512 -> SBV (WordN ((207 - 200) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @207) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @200) SWord 512
a, Proxy 199
-> Proxy 192 -> SWord 512 -> SBV (WordN ((199 - 192) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @199) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @192) SWord 512
a
               , Proxy 191
-> Proxy 184 -> SWord 512 -> SBV (WordN ((191 - 184) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @191) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @184) SWord 512
a, Proxy 183
-> Proxy 176 -> SWord 512 -> SBV (WordN ((183 - 176) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @183) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @176) SWord 512
a, Proxy 175
-> Proxy 168 -> SWord 512 -> SBV (WordN ((175 - 168) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @175) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @168) SWord 512
a, Proxy 167
-> Proxy 160 -> SWord 512 -> SBV (WordN ((167 - 160) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @167) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @160) SWord 512
a
               , Proxy 159
-> Proxy 152 -> SWord 512 -> SBV (WordN ((159 - 152) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @159) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @152) SWord 512
a, Proxy 151
-> Proxy 144 -> SWord 512 -> SBV (WordN ((151 - 144) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @151) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @144) SWord 512
a, Proxy 143
-> Proxy 136 -> SWord 512 -> SBV (WordN ((143 - 136) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @143) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @136) SWord 512
a, Proxy 135
-> Proxy 128 -> SWord 512 -> SBV (WordN ((135 - 128) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @135) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @128) SWord 512
a
               , Proxy 127
-> Proxy 120 -> SWord 512 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @127) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @120) SWord 512
a, Proxy 119
-> Proxy 112 -> SWord 512 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @119) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @112) SWord 512
a, Proxy 111
-> Proxy 104 -> SWord 512 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @111) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @104) SWord 512
a, Proxy 103 -> Proxy 96 -> SWord 512 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @103) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @96) SWord 512
a
               , Proxy 95 -> Proxy 88 -> SWord 512 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @95) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @88) SWord 512
a, Proxy 87 -> Proxy 80 -> SWord 512 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @87) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @80) SWord 512
a, Proxy 79 -> Proxy 72 -> SWord 512 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @79) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @72) SWord 512
a, Proxy 71 -> Proxy 64 -> SWord 512 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @71) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @64) SWord 512
a
               , Proxy 63 -> Proxy 56 -> SWord 512 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @63) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @56) SWord 512
a, Proxy 55 -> Proxy 48 -> SWord 512 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @55) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @48) SWord 512
a, Proxy 47 -> Proxy 40 -> SWord 512 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @47) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @40) SWord 512
a, Proxy 39 -> Proxy 32 -> SWord 512 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @39) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @32) SWord 512
a
               , Proxy 31 -> Proxy 24 -> SWord 512 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @31) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @24) SWord 512
a, Proxy 23 -> Proxy 16 -> SWord 512 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @23) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @16) SWord 512
a, Proxy 15 -> Proxy 8 -> SWord 512 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @15) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @8) SWord 512
a, Proxy 7 -> Proxy 0 -> SWord 512 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @7) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @0) SWord 512
a
               ]

   fromBytes :: [SWord 8] -> SWord 512
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
64
     = ([SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 256) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
32 [SWord 8]
as) SWord 256 -> SWord 256 -> SBV (WordN (256 + 256))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
32 [SWord 8]
as)
     | Bool
True
     = String -> SWord 512
forall a. HasCallStack => String -> a
error (String -> SWord 512) -> String -> SWord 512
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 512: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 1024 instance for 'ByteConverter'
instance ByteConverter (SWord 1024) where
   toBytes :: SWord 1024 -> [SWord 8]
toBytes SWord 1024
a = [ Proxy 1023
-> Proxy 1016 -> SWord 1024 -> SBV (WordN ((1023 - 1016) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1023) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1016) SWord 1024
a, Proxy 1015
-> Proxy 1008 -> SWord 1024 -> SBV (WordN ((1015 - 1008) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1015) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1008) SWord 1024
a, Proxy 1007
-> Proxy 1000 -> SWord 1024 -> SBV (WordN ((1007 - 1000) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1007) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1000) SWord 1024
a, Proxy 999
-> Proxy 992 -> SWord 1024 -> SBV (WordN ((999 - 992) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @999) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @992) SWord 1024
a
               , Proxy 991
-> Proxy 984 -> SWord 1024 -> SBV (WordN ((991 - 984) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @991) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @984) SWord 1024
a, Proxy 983
-> Proxy 976 -> SWord 1024 -> SBV (WordN ((983 - 976) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @983) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @976) SWord 1024
a, Proxy 975
-> Proxy 968 -> SWord 1024 -> SBV (WordN ((975 - 968) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @975) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @968) SWord 1024
a, Proxy 967
-> Proxy 960 -> SWord 1024 -> SBV (WordN ((967 - 960) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @967) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @960) SWord 1024
a
               , Proxy 959
-> Proxy 952 -> SWord 1024 -> SBV (WordN ((959 - 952) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @959) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @952) SWord 1024
a, Proxy 951
-> Proxy 944 -> SWord 1024 -> SBV (WordN ((951 - 944) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @951) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @944) SWord 1024
a, Proxy 943
-> Proxy 936 -> SWord 1024 -> SBV (WordN ((943 - 936) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @943) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @936) SWord 1024
a, Proxy 935
-> Proxy 928 -> SWord 1024 -> SBV (WordN ((935 - 928) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @935) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @928) SWord 1024
a
               , Proxy 927
-> Proxy 920 -> SWord 1024 -> SBV (WordN ((927 - 920) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @927) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @920) SWord 1024
a, Proxy 919
-> Proxy 912 -> SWord 1024 -> SBV (WordN ((919 - 912) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @919) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @912) SWord 1024
a, Proxy 911
-> Proxy 904 -> SWord 1024 -> SBV (WordN ((911 - 904) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @911) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @904) SWord 1024
a, Proxy 903
-> Proxy 896 -> SWord 1024 -> SBV (WordN ((903 - 896) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @903) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @896) SWord 1024
a
               , Proxy 895
-> Proxy 888 -> SWord 1024 -> SBV (WordN ((895 - 888) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @895) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @888) SWord 1024
a, Proxy 887
-> Proxy 880 -> SWord 1024 -> SBV (WordN ((887 - 880) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @887) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @880) SWord 1024
a, Proxy 879
-> Proxy 872 -> SWord 1024 -> SBV (WordN ((879 - 872) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @879) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @872) SWord 1024
a, Proxy 871
-> Proxy 864 -> SWord 1024 -> SBV (WordN ((871 - 864) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @871) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @864) SWord 1024
a
               , Proxy 863
-> Proxy 856 -> SWord 1024 -> SBV (WordN ((863 - 856) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @863) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @856) SWord 1024
a, Proxy 855
-> Proxy 848 -> SWord 1024 -> SBV (WordN ((855 - 848) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @855) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @848) SWord 1024
a, Proxy 847
-> Proxy 840 -> SWord 1024 -> SBV (WordN ((847 - 840) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @847) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @840) SWord 1024
a, Proxy 839
-> Proxy 832 -> SWord 1024 -> SBV (WordN ((839 - 832) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @839) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @832) SWord 1024
a
               , Proxy 831
-> Proxy 824 -> SWord 1024 -> SBV (WordN ((831 - 824) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @831) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @824) SWord 1024
a, Proxy 823
-> Proxy 816 -> SWord 1024 -> SBV (WordN ((823 - 816) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @823) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @816) SWord 1024
a, Proxy 815
-> Proxy 808 -> SWord 1024 -> SBV (WordN ((815 - 808) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @815) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @808) SWord 1024
a, Proxy 807
-> Proxy 800 -> SWord 1024 -> SBV (WordN ((807 - 800) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @807) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @800) SWord 1024
a
               , Proxy 799
-> Proxy 792 -> SWord 1024 -> SBV (WordN ((799 - 792) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @799) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @792) SWord 1024
a, Proxy 791
-> Proxy 784 -> SWord 1024 -> SBV (WordN ((791 - 784) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @791) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @784) SWord 1024
a, Proxy 783
-> Proxy 776 -> SWord 1024 -> SBV (WordN ((783 - 776) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @783) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @776) SWord 1024
a, Proxy 775
-> Proxy 768 -> SWord 1024 -> SBV (WordN ((775 - 768) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @775) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @768) SWord 1024
a
               , Proxy 767
-> Proxy 760 -> SWord 1024 -> SBV (WordN ((767 - 760) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @767) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @760) SWord 1024
a, Proxy 759
-> Proxy 752 -> SWord 1024 -> SBV (WordN ((759 - 752) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @759) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @752) SWord 1024
a, Proxy 751
-> Proxy 744 -> SWord 1024 -> SBV (WordN ((751 - 744) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @751) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @744) SWord 1024
a, Proxy 743
-> Proxy 736 -> SWord 1024 -> SBV (WordN ((743 - 736) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @743) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @736) SWord 1024
a
               , Proxy 735
-> Proxy 728 -> SWord 1024 -> SBV (WordN ((735 - 728) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @735) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @728) SWord 1024
a, Proxy 727
-> Proxy 720 -> SWord 1024 -> SBV (WordN ((727 - 720) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @727) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @720) SWord 1024
a, Proxy 719
-> Proxy 712 -> SWord 1024 -> SBV (WordN ((719 - 712) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @719) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @712) SWord 1024
a, Proxy 711
-> Proxy 704 -> SWord 1024 -> SBV (WordN ((711 - 704) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @711) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @704) SWord 1024
a
               , Proxy 703
-> Proxy 696 -> SWord 1024 -> SBV (WordN ((703 - 696) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @703) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @696) SWord 1024
a, Proxy 695
-> Proxy 688 -> SWord 1024 -> SBV (WordN ((695 - 688) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @695) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @688) SWord 1024
a, Proxy 687
-> Proxy 680 -> SWord 1024 -> SBV (WordN ((687 - 680) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @687) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @680) SWord 1024
a, Proxy 679
-> Proxy 672 -> SWord 1024 -> SBV (WordN ((679 - 672) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @679) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @672) SWord 1024
a
               , Proxy 671
-> Proxy 664 -> SWord 1024 -> SBV (WordN ((671 - 664) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @671) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @664) SWord 1024
a, Proxy 663
-> Proxy 656 -> SWord 1024 -> SBV (WordN ((663 - 656) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @663) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @656) SWord 1024
a, Proxy 655
-> Proxy 648 -> SWord 1024 -> SBV (WordN ((655 - 648) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @655) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @648) SWord 1024
a, Proxy 647
-> Proxy 640 -> SWord 1024 -> SBV (WordN ((647 - 640) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @647) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @640) SWord 1024
a
               , Proxy 639
-> Proxy 632 -> SWord 1024 -> SBV (WordN ((639 - 632) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @639) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @632) SWord 1024
a, Proxy 631
-> Proxy 624 -> SWord 1024 -> SBV (WordN ((631 - 624) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @631) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @624) SWord 1024
a, Proxy 623
-> Proxy 616 -> SWord 1024 -> SBV (WordN ((623 - 616) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @623) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @616) SWord 1024
a, Proxy 615
-> Proxy 608 -> SWord 1024 -> SBV (WordN ((615 - 608) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @615) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @608) SWord 1024
a
               , Proxy 607
-> Proxy 600 -> SWord 1024 -> SBV (WordN ((607 - 600) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @607) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @600) SWord 1024
a, Proxy 599
-> Proxy 592 -> SWord 1024 -> SBV (WordN ((599 - 592) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @599) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @592) SWord 1024
a, Proxy 591
-> Proxy 584 -> SWord 1024 -> SBV (WordN ((591 - 584) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @591) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @584) SWord 1024
a, Proxy 583
-> Proxy 576 -> SWord 1024 -> SBV (WordN ((583 - 576) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @583) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @576) SWord 1024
a
               , Proxy 575
-> Proxy 568 -> SWord 1024 -> SBV (WordN ((575 - 568) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @575) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @568) SWord 1024
a, Proxy 567
-> Proxy 560 -> SWord 1024 -> SBV (WordN ((567 - 560) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @567) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @560) SWord 1024
a, Proxy 559
-> Proxy 552 -> SWord 1024 -> SBV (WordN ((559 - 552) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @559) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @552) SWord 1024
a, Proxy 551
-> Proxy 544 -> SWord 1024 -> SBV (WordN ((551 - 544) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @551) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @544) SWord 1024
a
               , Proxy 543
-> Proxy 536 -> SWord 1024 -> SBV (WordN ((543 - 536) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @543) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @536) SWord 1024
a, Proxy 535
-> Proxy 528 -> SWord 1024 -> SBV (WordN ((535 - 528) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @535) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @528) SWord 1024
a, Proxy 527
-> Proxy 520 -> SWord 1024 -> SBV (WordN ((527 - 520) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @527) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @520) SWord 1024
a, Proxy 519
-> Proxy 512 -> SWord 1024 -> SBV (WordN ((519 - 512) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @519) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @512) SWord 1024
a
               , Proxy 511
-> Proxy 504 -> SWord 1024 -> SBV (WordN ((511 - 504) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @511) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @504) SWord 1024
a, Proxy 503
-> Proxy 496 -> SWord 1024 -> SBV (WordN ((503 - 496) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @503) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @496) SWord 1024
a, Proxy 495
-> Proxy 488 -> SWord 1024 -> SBV (WordN ((495 - 488) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @495) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @488) SWord 1024
a, Proxy 487
-> Proxy 480 -> SWord 1024 -> SBV (WordN ((487 - 480) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @487) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @480) SWord 1024
a
               , Proxy 479
-> Proxy 472 -> SWord 1024 -> SBV (WordN ((479 - 472) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @479) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @472) SWord 1024
a, Proxy 471
-> Proxy 464 -> SWord 1024 -> SBV (WordN ((471 - 464) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @471) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @464) SWord 1024
a, Proxy 463
-> Proxy 456 -> SWord 1024 -> SBV (WordN ((463 - 456) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @463) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @456) SWord 1024
a, Proxy 455
-> Proxy 448 -> SWord 1024 -> SBV (WordN ((455 - 448) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @455) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @448) SWord 1024
a
               , Proxy 447
-> Proxy 440 -> SWord 1024 -> SBV (WordN ((447 - 440) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @447) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @440) SWord 1024
a, Proxy 439
-> Proxy 432 -> SWord 1024 -> SBV (WordN ((439 - 432) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @439) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @432) SWord 1024
a, Proxy 431
-> Proxy 424 -> SWord 1024 -> SBV (WordN ((431 - 424) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @431) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @424) SWord 1024
a, Proxy 423
-> Proxy 416 -> SWord 1024 -> SBV (WordN ((423 - 416) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @423) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @416) SWord 1024
a
               , Proxy 415
-> Proxy 408 -> SWord 1024 -> SBV (WordN ((415 - 408) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @415) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @408) SWord 1024
a, Proxy 407
-> Proxy 400 -> SWord 1024 -> SBV (WordN ((407 - 400) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @407) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @400) SWord 1024
a, Proxy 399
-> Proxy 392 -> SWord 1024 -> SBV (WordN ((399 - 392) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @399) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @392) SWord 1024
a, Proxy 391
-> Proxy 384 -> SWord 1024 -> SBV (WordN ((391 - 384) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @391) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @384) SWord 1024
a
               , Proxy 383
-> Proxy 376 -> SWord 1024 -> SBV (WordN ((383 - 376) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @383) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @376) SWord 1024
a, Proxy 375
-> Proxy 368 -> SWord 1024 -> SBV (WordN ((375 - 368) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @375) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @368) SWord 1024
a, Proxy 367
-> Proxy 360 -> SWord 1024 -> SBV (WordN ((367 - 360) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @367) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @360) SWord 1024
a, Proxy 359
-> Proxy 352 -> SWord 1024 -> SBV (WordN ((359 - 352) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @359) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @352) SWord 1024
a
               , Proxy 351
-> Proxy 344 -> SWord 1024 -> SBV (WordN ((351 - 344) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @351) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @344) SWord 1024
a, Proxy 343
-> Proxy 336 -> SWord 1024 -> SBV (WordN ((343 - 336) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @343) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @336) SWord 1024
a, Proxy 335
-> Proxy 328 -> SWord 1024 -> SBV (WordN ((335 - 328) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @335) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @328) SWord 1024
a, Proxy 327
-> Proxy 320 -> SWord 1024 -> SBV (WordN ((327 - 320) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @327) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @320) SWord 1024
a
               , Proxy 319
-> Proxy 312 -> SWord 1024 -> SBV (WordN ((319 - 312) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @319) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @312) SWord 1024
a, Proxy 311
-> Proxy 304 -> SWord 1024 -> SBV (WordN ((311 - 304) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @311) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @304) SWord 1024
a, Proxy 303
-> Proxy 296 -> SWord 1024 -> SBV (WordN ((303 - 296) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @303) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @296) SWord 1024
a, Proxy 295
-> Proxy 288 -> SWord 1024 -> SBV (WordN ((295 - 288) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @295) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @288) SWord 1024
a
               , Proxy 287
-> Proxy 280 -> SWord 1024 -> SBV (WordN ((287 - 280) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @287) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @280) SWord 1024
a, Proxy 279
-> Proxy 272 -> SWord 1024 -> SBV (WordN ((279 - 272) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @279) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @272) SWord 1024
a, Proxy 271
-> Proxy 264 -> SWord 1024 -> SBV (WordN ((271 - 264) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @271) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @264) SWord 1024
a, Proxy 263
-> Proxy 256 -> SWord 1024 -> SBV (WordN ((263 - 256) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @263) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @256) SWord 1024
a
               , Proxy 255
-> Proxy 248 -> SWord 1024 -> SBV (WordN ((255 - 248) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @255) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @248) SWord 1024
a, Proxy 247
-> Proxy 240 -> SWord 1024 -> SBV (WordN ((247 - 240) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @247) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @240) SWord 1024
a, Proxy 239
-> Proxy 232 -> SWord 1024 -> SBV (WordN ((239 - 232) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @239) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @232) SWord 1024
a, Proxy 231
-> Proxy 224 -> SWord 1024 -> SBV (WordN ((231 - 224) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @231) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @224) SWord 1024
a
               , Proxy 223
-> Proxy 216 -> SWord 1024 -> SBV (WordN ((223 - 216) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @223) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @216) SWord 1024
a, Proxy 215
-> Proxy 208 -> SWord 1024 -> SBV (WordN ((215 - 208) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @215) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @208) SWord 1024
a, Proxy 207
-> Proxy 200 -> SWord 1024 -> SBV (WordN ((207 - 200) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @207) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @200) SWord 1024
a, Proxy 199
-> Proxy 192 -> SWord 1024 -> SBV (WordN ((199 - 192) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @199) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @192) SWord 1024
a
               , Proxy 191
-> Proxy 184 -> SWord 1024 -> SBV (WordN ((191 - 184) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @191) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @184) SWord 1024
a, Proxy 183
-> Proxy 176 -> SWord 1024 -> SBV (WordN ((183 - 176) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @183) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @176) SWord 1024
a, Proxy 175
-> Proxy 168 -> SWord 1024 -> SBV (WordN ((175 - 168) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @175) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @168) SWord 1024
a, Proxy 167
-> Proxy 160 -> SWord 1024 -> SBV (WordN ((167 - 160) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @167) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @160) SWord 1024
a
               , Proxy 159
-> Proxy 152 -> SWord 1024 -> SBV (WordN ((159 - 152) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @159) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @152) SWord 1024
a, Proxy 151
-> Proxy 144 -> SWord 1024 -> SBV (WordN ((151 - 144) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @151) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @144) SWord 1024
a, Proxy 143
-> Proxy 136 -> SWord 1024 -> SBV (WordN ((143 - 136) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @143) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @136) SWord 1024
a, Proxy 135
-> Proxy 128 -> SWord 1024 -> SBV (WordN ((135 - 128) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @135) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @128) SWord 1024
a
               , Proxy 127
-> Proxy 120 -> SWord 1024 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @127) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @120) SWord 1024
a, Proxy 119
-> Proxy 112 -> SWord 1024 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @119) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @112) SWord 1024
a, Proxy 111
-> Proxy 104 -> SWord 1024 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @111) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @104) SWord 1024
a, Proxy 103 -> Proxy 96 -> SWord 1024 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy  @103) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @96) SWord 1024
a
               , Proxy 95 -> Proxy 88 -> SWord 1024 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @95) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @88) SWord 1024
a, Proxy 87 -> Proxy 80 -> SWord 1024 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @87) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @80) SWord 1024
a, Proxy 79 -> Proxy 72 -> SWord 1024 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @79) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @72) SWord 1024
a, Proxy 71 -> Proxy 64 -> SWord 1024 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @71) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @64) SWord 1024
a
               , Proxy 63 -> Proxy 56 -> SWord 1024 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @63) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @56) SWord 1024
a, Proxy 55 -> Proxy 48 -> SWord 1024 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @55) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @48) SWord 1024
a, Proxy 47 -> Proxy 40 -> SWord 1024 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @47) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @40) SWord 1024
a, Proxy 39 -> Proxy 32 -> SWord 1024 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @39) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @32) SWord 1024
a
               , Proxy 31 -> Proxy 24 -> SWord 1024 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @31) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @24) SWord 1024
a, Proxy 23 -> Proxy 16 -> SWord 1024 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @23) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @16) SWord 1024
a, Proxy 15 -> Proxy 8 -> SWord 1024 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy   @15) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy    @8) SWord 1024
a, Proxy 7 -> Proxy 0 -> SWord 1024 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy    @7) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy    @0) SWord 1024
a
               ]

   fromBytes :: [SWord 8] -> SWord 1024
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
128
     = ([SWord 8] -> SWord 512
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 512) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
64 [SWord 8]
as) SWord 512 -> SWord 512 -> SBV (WordN (512 + 512))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 512
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
64 [SWord 8]
as)
     | Bool
True
     = String -> SWord 1024
forall a. HasCallStack => String -> a
error (String -> SWord 1024) -> String -> SWord 1024
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 1024: Incorrect number of bytes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

{- $specialRels
A special relation is a binary relation that has additional properties. SBV allows for the checking of various kinds
of special relations respecting various axioms, and allows for creating transitive closures.
See "Documentation.SBV.Examples.Misc.FirstOrderLogic" for several examples.
-}

-- | A type synonym for binary relations.
type Relation a = (SBV a, SBV a) -> SBool

-- | Check if a relation is a partial order. The string argument must uniquely identify this order.
isPartialOrder :: SymVal a => String -> Relation a -> SBool
isPartialOrder :: forall a. SymVal a => String -> Relation a -> SBool
isPartialOrder = SpecialRelOp -> Relation a -> SBool
forall a. SymVal a => SpecialRelOp -> Relation a -> SBool
checkSpecialRelation (SpecialRelOp -> Relation a -> SBool)
-> (String -> SpecialRelOp) -> String -> Relation a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SpecialRelOp
IsPartialOrder

-- | Check if a relation is a linear order. The string argument must uniquely identify this order.
isLinearOrder :: SymVal a => String -> Relation a -> SBool
isLinearOrder :: forall a. SymVal a => String -> Relation a -> SBool
isLinearOrder = SpecialRelOp -> Relation a -> SBool
forall a. SymVal a => SpecialRelOp -> Relation a -> SBool
checkSpecialRelation (SpecialRelOp -> Relation a -> SBool)
-> (String -> SpecialRelOp) -> String -> Relation a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SpecialRelOp
IsLinearOrder

-- | Check if a relation is a tree order. The string argument must uniquely identify this order.
isTreeOrder :: SymVal a => String -> Relation a -> SBool
isTreeOrder :: forall a. SymVal a => String -> Relation a -> SBool
isTreeOrder = SpecialRelOp -> Relation a -> SBool
forall a. SymVal a => SpecialRelOp -> Relation a -> SBool
checkSpecialRelation (SpecialRelOp -> Relation a -> SBool)
-> (String -> SpecialRelOp) -> String -> Relation a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SpecialRelOp
IsTreeOrder

-- | Check if a relation is a piece-wise linear order. The string argument must uniquely identify this order.
isPiecewiseLinearOrder :: SymVal a => String -> Relation a -> SBool
isPiecewiseLinearOrder :: forall a. SymVal a => String -> Relation a -> SBool
isPiecewiseLinearOrder = SpecialRelOp -> Relation a -> SBool
forall a. SymVal a => SpecialRelOp -> Relation a -> SBool
checkSpecialRelation (SpecialRelOp -> Relation a -> SBool)
-> (String -> SpecialRelOp) -> String -> Relation a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SpecialRelOp
IsPiecewiseLinearOrder

-- | Make sure it's internally acceptable
sanitizeRelName :: String -> String
sanitizeRelName :: String -> String
sanitizeRelName String
s = String
"__internal_sbv_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
sanitize String
s
  where sanitize :: Char -> Char
sanitize Char
c | Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char -> Bool
isPunctuation Char
c = Char
'_'
                               | Bool
True             = Char
c

-- | Create the transitive closure of a given relation. The string argument must uniquely identify the newly created relation.
mkTransitiveClosure :: forall a. SymVal a => String -> Relation a -> Relation a
mkTransitiveClosure :: forall a. SymVal a => String -> Relation a -> Relation a
mkTransitiveClosure String
nm Relation a
rel = Relation a
res
  where ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)

        -- The internal name of this relation
        inm :: String
inm = String -> String
sanitizeRelName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"_TransitiveClosure_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_"
        key :: (String, String)
key = (String
inm, String
nm)

        res :: Relation a
res (SBV a
a, SBV a
b) = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
result
          where result :: State -> IO SV
result State
st = do -- Is this new? If so create it, otherwise reuse
                               ProgInfo{progTransClosures = curProgTransClosures} <- IORef ProgInfo -> IO ProgInfo
forall a. IORef a -> IO a
readIORef (State -> IORef ProgInfo
rProgInfo State
st)

                               unless (key `elem` curProgTransClosures) $ do

                                  registerKind st ka

                                  -- Add to the end so if we get incremental ones the order doesn't change for old ones!
                                  modifyIORef' (rProgInfo st) (\ProgInfo
u -> ProgInfo
u{progTransClosures = curProgTransClosures ++ [key]})

                                  -- Equate it to the relation we are given. We want to do this in the root state
                                  let SBV eq = quantifiedBool $ \(Forall SBV a
x) (Forall SBV a
y) -> Relation a
rel (SBV a
x, SBV a
y) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== String -> SBV a -> SBV a -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
inm SBV a
x SBV a
y
                                  internalConstraint (getRootState st) False [] eq

                               sa <- sbvToSV st a
                               sb <- sbvToSV st b

                               newExpr st KBool $ SBVApp (Uninterpreted nm) [sa, sb]

-- | Check if the given relation satisfies the required axioms
checkSpecialRelation :: forall a. SymVal a => SpecialRelOp -> Relation a -> SBool
checkSpecialRelation :: forall a. SymVal a => SpecialRelOp -> Relation a -> SBool
checkSpecialRelation SpecialRelOp
op Relation a
rel = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
result
  where ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)

        internalize :: String -> SpecialRelOp
internalize String
nm = case SpecialRelOp
op of
                           IsPartialOrder         String
_ -> String -> SpecialRelOp
IsPartialOrder         String
nm
                           IsLinearOrder          String
_ -> String -> SpecialRelOp
IsLinearOrder          String
nm
                           IsTreeOrder            String
_ -> String -> SpecialRelOp
IsTreeOrder            String
nm
                           IsPiecewiseLinearOrder String
_ -> String -> SpecialRelOp
IsPiecewiseLinearOrder String
nm

        result :: State -> IO SV
result State
st = do -- The internal name of this relation
                       let nm :: String
nm  = String -> String
sanitizeRelName (SpecialRelOp -> String
forall a. Show a => a -> String
show SpecialRelOp
op)
                           iop :: SpecialRelOp
iop = String -> SpecialRelOp
internalize String
nm

                       -- Is this new? If so create it, otherwise reuse
                       ProgInfo{progSpecialRels = curSpecialRels} <- IORef ProgInfo -> IO ProgInfo
forall a. IORef a -> IO a
readIORef (State -> IORef ProgInfo
rProgInfo State
st)

                       unless (op `elem` curSpecialRels) $ do

                          registerKind st ka
                          nm' <- newUninterpreted st (UIGiven nm) Nothing (SBVType [ka, ka, KBool]) (UINone True)

                          -- Add to the end so if we get incremental ones the order doesn't change for old ones!
                          modifyIORef' (rProgInfo st) (\ProgInfo
u -> ProgInfo
u{progSpecialRels = curSpecialRels ++ [iop]})

                          -- Equate it to the relation we are given. We want to do this in the parent state
                          let SBV eq = quantifiedBool $ \(Forall SBV a
x) (Forall SBV a
y) -> Relation a
rel (SBV a
x, SBV a
y) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== String -> SBV a -> SBV a -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
nm' SBV a
x SBV a
y
                          internalConstraint (getRootState st) False [] eq

                       newExpr st KBool $ SBVApp (SpecialRelOp ka iop) []

-- | Optimize lexicographically, with the default solver.
optLexicographic :: Satisfiable a => a -> IO SMTResult
optLexicographic :: forall a. Satisfiable a => a -> IO SMTResult
optLexicographic = SMTConfig -> a -> IO SMTResult
forall a. Satisfiable a => SMTConfig -> a -> IO SMTResult
optLexicographicWith SMTConfig
defaultSMTCfg

-- | Optimize lexicographically, using the given solver.
optLexicographicWith :: Satisfiable a => SMTConfig -> a -> IO SMTResult
optLexicographicWith :: forall a. Satisfiable a => SMTConfig -> a -> IO SMTResult
optLexicographicWith SMTConfig
config a
p = do
   res <- SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
forall a.
Satisfiable a =>
SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith SMTConfig
config OptimizeStyle
Lexicographic a
p
   case res of
     LexicographicResult SMTResult
r -> SMTResult -> IO SMTResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SMTResult
r
     OptimizeResult
_                     -> String -> IO SMTResult
forall a. HasCallStack => String -> a
error (String -> IO SMTResult) -> String -> IO SMTResult
forall a b. (a -> b) -> a -> b
$ String
"A lexicographic optimization call resulted in a bad result:"
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OptimizeResult -> String
forall a. Show a => a -> String
show OptimizeResult
res

-- | Pareto front optimization, with the default solver.
optPareto :: Satisfiable a => Maybe Int -> a -> IO (Bool, [SMTResult])
optPareto :: forall a. Satisfiable a => Maybe Int -> a -> IO (Bool, [SMTResult])
optPareto = SMTConfig -> Maybe Int -> a -> IO (Bool, [SMTResult])
forall a.
Satisfiable a =>
SMTConfig -> Maybe Int -> a -> IO (Bool, [SMTResult])
optParetoWith SMTConfig
defaultSMTCfg

-- | Pareto front optimization, with the given solver. The optional integer argument is the number of fronts to return. If 'Nothing', then
-- we will return all pareto fronts. If the first component of the result is 'True' then we reached the pareto-query limit specified by
-- the user, so there might be more unqueried results remaining. If 'False', it means that all the pareto fronts are returned.
optParetoWith :: Satisfiable a => SMTConfig -> Maybe Int -> a -> IO (Bool, [SMTResult])
optParetoWith :: forall a.
Satisfiable a =>
SMTConfig -> Maybe Int -> a -> IO (Bool, [SMTResult])
optParetoWith SMTConfig
config Maybe Int
mbLim a
p = do
   res <- SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
forall a.
Satisfiable a =>
SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith SMTConfig
config (Maybe Int -> OptimizeStyle
Pareto Maybe Int
mbLim) a
p
   case res of
     ParetoResult (Bool, [SMTResult])
r -> (Bool, [SMTResult]) -> IO (Bool, [SMTResult])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool, [SMTResult])
r
     OptimizeResult
_              -> String -> IO (Bool, [SMTResult])
forall a. HasCallStack => String -> a
error (String -> IO (Bool, [SMTResult]))
-> String -> IO (Bool, [SMTResult])
forall a b. (a -> b) -> a -> b
$ String
"A pareto optimization call resulted in a bad result:"
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OptimizeResult -> String
forall a. Show a => a -> String
show OptimizeResult
res

-- | Independent optimization, with the default solver. In each result, string is the name of the objective optimized given by the user.
optIndependent :: Satisfiable a => a -> IO [(String, SMTResult)]
optIndependent :: forall a. Satisfiable a => a -> IO [(String, SMTResult)]
optIndependent = SMTConfig -> a -> IO [(String, SMTResult)]
forall a.
Satisfiable a =>
SMTConfig -> a -> IO [(String, SMTResult)]
optIndependentWith SMTConfig
defaultSMTCfg

-- | Independent optimization, with the given solver. In each result, string is the name of the objective optimized given by the user.
optIndependentWith :: Satisfiable a => SMTConfig -> a -> IO [(String, SMTResult)]
optIndependentWith :: forall a.
Satisfiable a =>
SMTConfig -> a -> IO [(String, SMTResult)]
optIndependentWith SMTConfig
config a
p = do
   res <- SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
forall a.
Satisfiable a =>
SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith SMTConfig
config OptimizeStyle
Independent a
p
   case res of
     IndependentResult [(String, SMTResult)]
r -> [(String, SMTResult)] -> IO [(String, SMTResult)]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(String, SMTResult)]
r
     OptimizeResult
_                   -> String -> IO [(String, SMTResult)]
forall a. HasCallStack => String -> a
error (String -> IO [(String, SMTResult)])
-> String -> IO [(String, SMTResult)]
forall a b. (a -> b) -> a -> b
$ String
"An independent optimization call resulted in a bad result:"
                                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OptimizeResult -> String
forall a. Show a => a -> String
show OptimizeResult
res

-- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds
-- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.)
class Queriable m a where
  type QueryResult a :: Type

  -- | ^ Create a new symbolic value of type @a@
  create  :: QueryT m a

  -- | ^ Extract the current value in a SAT context
  project :: a -> QueryT m (QueryResult a)

  -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
  -- via the t'QueryT' monad transformer.
  embed   :: QueryResult a -> QueryT m a

  default project :: (a ~ t e, QueryResult (t e) ~ t (QueryResult e), Traversable t, Monad m, Queriable m e) =>  a -> QueryT m (QueryResult a)
  project = (e -> QueryT m (QueryResult e))
-> t e -> QueryT m (t (QueryResult e))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM e -> QueryT m (QueryResult e)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project

  default embed   :: (a ~ t e, QueryResult (t e) ~ t (QueryResult e), Traversable t, Monad m, Queriable m e) => QueryResult a -> QueryT m a
  embed = (QueryResult e -> QueryT m e)
-> t (QueryResult e) -> QueryT m (t e)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM QueryResult e -> QueryT m e
forall (m :: * -> *) a.
Queriable m a =>
QueryResult a -> QueryT m a
embed
  {-# MINIMAL create #-}

-- | Generic 'Queriable' instance for 'SymVal' values. This provides the base case for the generic definitions for project and embed
-- when we automatically derive them. We make this instance overlappable should the user have a different mapping in mind, for instance
-- mapping a symbolic boolean to a concrete integer for whatever reason.
instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where
  type QueryResult (SBV a) = a

  create :: QueryT m (SBV a)
create  = QueryT m (SBV a)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
  project :: SBV a -> QueryT m (QueryResult (SBV a))
project = SBV a -> QueryT m a
SBV a -> QueryT m (QueryResult (SBV a))
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue
  embed :: QueryResult (SBV a) -> QueryT m (SBV a)
embed   = SBV a -> QueryT m (SBV a)
forall a. a -> QueryT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV a -> QueryT m (SBV a))
-> (a -> SBV a) -> a -> QueryT m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal

{- HLint ignore module "Use import/export shortcut" -}