{-|
Module           : What4.Interface
Description      : Main interface for constructing What4 formulae
Copyright        : (c) Galois, Inc 2014-2020
License          : BSD3
Maintainer       : Joe Hendrix <jhendrix@galois.com>

Defines interface between the simulator and terms that are sent to the
SAT or SMT solver.  The simulator can use a richer set of types, but the
symbolic values must be representable by types supported by this interface.

A solver backend is defined in terms of a type parameter @sym@, which
is the type that tracks whatever state or context is needed by that
particular backend. To instantiate the solver interface, one must
provide several type family definitions and class instances for @sym@:

  [@type 'SymExpr' sym :: 'BaseType' -> *@]
  Type of symbolic expressions.

  [@type 'BoundVar' sym :: 'BaseType' -> *@]
  Representation of bound variables in symbolic expressions.

  [@type 'SymFn' sym :: Ctx BaseType -> BaseType -> *@]
  Representation of symbolic functions.

  [@instance 'IsExprBuilder' sym@]
  Functions for building expressions of various types.

  [@instance 'IsSymExprBuilder' sym@]
  Functions for building expressions with bound variables and quantifiers.

  [@instance 'IsExpr' ('SymExpr' sym)@]
  Recognizers for various kinds of literal expressions.

  [@instance 'OrdF' ('SymExpr' sym)@]

  [@instance 'TestEquality' ('SymExpr' sym)@]

  [@instance 'HashableF' ('SymExpr' sym)@]

The canonical implementation of these interface classes is found in "What4.Expr.Builder".
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE UndecidableInstances #-}

module What4.Interface
  ( -- * Interface classes
    -- ** Type Families
    SymExpr
  , BoundVar
  , SymFn
  , SymAnnotation

    -- ** Expression recognizers
  , IsExpr(..)
  , IsSymFn(..)
  , UnfoldPolicy(..)
  , shouldUnfold

    -- ** IsExprBuilder
  , IsExprBuilder(..)
  , IsSymExprBuilder(..)
  , SolverEvent(..)

    -- ** Bitvector operations
  , bvJoinVector
  , bvSplitVector
  , bvSwap
  , bvBitreverse

    -- ** Floating-point rounding modes
  , RoundingMode(..)

    -- ** Run-time statistics
  , Statistics(..)
  , zeroStatistics

    -- * Type Aliases
  , Pred
  , SymInteger
  , SymReal
  , SymFloat
  , SymString
  , SymCplx
  , SymStruct
  , SymBV
  , SymArray

    -- * Natural numbers
  , SymNat
  , asNat
  , natLit
  , natAdd
  , natSub
  , natMul
  , natDiv
  , natMod
  , natIte
  , natEq
  , natLe
  , natLt
  , natToInteger
  , bvToNat
  , natToReal
  , integerToNat
  , realToNat
  , freshBoundedNat
  , freshNat
  , printSymNat

    -- * Array utility types
  , IndexLit(..)
  , indexLit
  , ArrayResultWrapper(..)

    -- * Concrete values
  , asConcrete
  , concreteToSym
  , baseIsConcrete
  , baseDefaultValue
  , realExprAsInteger
  , rationalAsInteger
  , cplxExprAsRational
  , cplxExprAsInteger

    -- * SymEncoder
  , SymEncoder(..)

    -- * Utility combinators
    -- ** Boolean operations
  , backendPred
  , andAllOf
  , orOneOf
  , itePredM
  , iteM
  , iteList
  , predToReal

    -- ** Complex number operations
  , cplxDiv
  , cplxLog
  , cplxLogBase
  , mkRational
  , mkReal
  , isNonZero
  , isReal

    -- ** Indexing
  , muxRange

    -- * Exceptions
  , InvalidRange(..)

    -- * Reexports
  , module Data.Parameterized.NatRepr
  , module What4.BaseTypes
  , HasAbsValue
  , What4.Symbol.SolverSymbol
  , What4.Symbol.emptySymbol
  , What4.Symbol.userSymbol
  , What4.Symbol.safeSymbol
  , ValueRange(..)
  , StringLiteral(..)
  , stringLiteralInfo
  ) where

#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif

import           Control.Exception (assert, Exception)
import           Control.Lens
import           Control.Monad
import           Control.Monad.IO.Class
import qualified Data.BitVector.Sized as BV
import           Data.Coerce (coerce)
import           Data.Foldable
import           Data.Kind ( Type )
import qualified Data.Map as Map
import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Ctx
import           Data.Parameterized.Utils.Endian (Endian(..))
import           Data.Parameterized.NatRepr
import           Data.Parameterized.TraversableFC
import qualified Data.Parameterized.Vector as Vector
import           Data.Ratio
import           Data.Scientific (Scientific)
import           GHC.Generics (Generic)
import           Numeric.Natural
import           LibBF (BigFloat)
import           Prettyprinter (Doc)

import           What4.BaseTypes
import           What4.Config
import qualified What4.Expr.ArrayUpdateMap as AUM
import           What4.IndexLit
import           What4.ProgramLoc
import           What4.Concrete
import           What4.SatResult
import           What4.Symbol
import           What4.Utils.AbstractDomains
import           What4.Utils.Arithmetic
import           What4.Utils.Complex
import           What4.Utils.FloatHelpers (RoundingMode(..))
import           What4.Utils.StringLiteral

------------------------------------------------------------------------
-- SymExpr names

-- | Symbolic boolean values, AKA predicates.
type Pred sym = SymExpr sym BaseBoolType

-- | Symbolic integers.
type SymInteger sym = SymExpr sym BaseIntegerType

-- | Symbolic real numbers.
type SymReal sym = SymExpr sym BaseRealType

-- | Symbolic floating point numbers.
type SymFloat sym fpp = SymExpr sym (BaseFloatType fpp)

-- | Symbolic complex numbers.
type SymCplx sym = SymExpr sym BaseComplexType

-- | Symbolic structures.
type SymStruct sym flds = SymExpr sym (BaseStructType flds)

-- | Symbolic arrays.
type SymArray sym idx b = SymExpr sym (BaseArrayType idx b)

-- | Symbolic bitvectors.
type SymBV sym n = SymExpr sym (BaseBVType n)

-- | Symbolic strings.
type SymString sym si = SymExpr sym (BaseStringType si)

------------------------------------------------------------------------
-- Type families for the interface.

-- | The class for expressions.
type family SymExpr (sym :: Type) :: BaseType -> Type

------------------------------------------------------------------------
-- | Type of bound variable associated with symbolic state.
--
-- This type is used by some methods in class 'IsSymExprBuilder'.
type family BoundVar (sym :: Type) :: BaseType -> Type


------------------------------------------------------------------------
-- | Type used to uniquely identify expressions that have been annotated.
type family SymAnnotation (sym :: Type) :: BaseType -> Type

------------------------------------------------------------------------
-- IsBoolSolver

-- | Perform an ite on a predicate lazily.
itePredM :: (IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m)
         => sym
         -> Pred sym
         -> m (Pred sym)
         -> m (Pred sym)
         -> m (Pred sym)
itePredM :: sym -> Pred sym -> m (Pred sym) -> m (Pred sym) -> m (Pred sym)
itePredM sym
sym Pred sym
c m (Pred sym)
mx m (Pred sym)
my =
  case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
c of
    Just Bool
True -> m (Pred sym)
mx
    Just Bool
False -> m (Pred sym)
my
    Maybe Bool
Nothing -> do
      Pred sym
x <- m (Pred sym)
mx
      Pred sym
y <- m (Pred sym)
my
      IO (Pred sym) -> m (Pred sym)
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Pred sym) -> m (Pred sym)) -> IO (Pred sym) -> m (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c Pred sym
x Pred sym
y

------------------------------------------------------------------------
-- IsExpr

-- | This class provides operations for recognizing when symbolic expressions
--   represent concrete values, extracting the type from an expression,
--   and for providing pretty-printed representations of an expression.
class HasAbsValue e => IsExpr e where
  -- | Evaluate if predicate is constant.
  asConstantPred :: e BaseBoolType -> Maybe Bool
  asConstantPred e BaseBoolType
_ = Maybe Bool
forall a. Maybe a
Nothing

  -- | Return integer if this is a constant integer.
  asInteger :: e BaseIntegerType -> Maybe Integer
  asInteger e BaseIntegerType
_ = Maybe Integer
forall a. Maybe a
Nothing

  -- | Return any bounding information we have about the term
  integerBounds :: e BaseIntegerType -> ValueRange Integer

  -- | Return rational if this is a constant value.
  asRational :: e BaseRealType -> Maybe Rational
  asRational e BaseRealType
_ = Maybe Rational
forall a. Maybe a
Nothing

  -- | Return floating-point value if this is a constant
  asFloat :: e (BaseFloatType fpp) -> Maybe BigFloat

  -- | Return any bounding information we have about the term
  rationalBounds :: e BaseRealType -> ValueRange Rational

  -- | Return complex if this is a constant value.
  asComplex :: e BaseComplexType -> Maybe (Complex Rational)
  asComplex e BaseComplexType
_ = Maybe (Complex Rational)
forall a. Maybe a
Nothing

  -- | Return a bitvector if this is a constant bitvector.
  asBV :: e (BaseBVType w) -> Maybe (BV.BV w)
  asBV e (BaseBVType w)
_ = Maybe (BV w)
forall a. Maybe a
Nothing

  -- | If we have bounds information about the term, return unsigned
  -- upper and lower bounds as integers
  unsignedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)

  -- | If we have bounds information about the term, return signed
  -- upper and lower bounds as integers
  signedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)

  -- | If this expression syntactically represents an "affine" form, return its components.
  --   When @asAffineVar x = Just (c,r,o)@, then we have @x == c*r + o@.
  asAffineVar :: e tp -> Maybe (ConcreteVal tp, e tp, ConcreteVal tp)

  -- | Return the string value if this is a constant string
  asString :: e (BaseStringType si) -> Maybe (StringLiteral si)
  asString e (BaseStringType si)
_ = Maybe (StringLiteral si)
forall a. Maybe a
Nothing

  -- | Return the representation of the string info for a string-typed term.
  stringInfo :: e (BaseStringType si) -> StringInfoRepr si
  stringInfo e (BaseStringType si)
e =
    case e (BaseStringType si) -> BaseTypeRepr (BaseStringType si)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e (BaseStringType si)
e of
      BaseStringRepr StringInfoRepr si
si -> StringInfoRepr si
StringInfoRepr si
si

  -- | Return the unique element value if this is a constant array,
  --   such as one made with 'constantArray'.
  asConstantArray :: e (BaseArrayType idx bt) -> Maybe (e bt)
  asConstantArray e (BaseArrayType idx bt)
_ = Maybe (e bt)
forall a. Maybe a
Nothing

  -- | Return the struct fields if this is a concrete struct.
  asStruct :: e (BaseStructType flds) -> Maybe (Ctx.Assignment e flds)
  asStruct e (BaseStructType flds)
_ = Maybe (Assignment e flds)
forall a. Maybe a
Nothing

  -- | Get type of expression.
  exprType :: e tp -> BaseTypeRepr tp

  -- | Get the width of a bitvector
  bvWidth      :: e (BaseBVType w) -> NatRepr w
  bvWidth e (BaseBVType w)
e =
    case e (BaseBVType w) -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e (BaseBVType w)
e of
      BaseBVRepr NatRepr w
w -> NatRepr w
NatRepr w
w

  -- | Get the precision of a floating-point expression
  floatPrecision :: e (BaseFloatType fpp) -> FloatPrecisionRepr fpp
  floatPrecision e (BaseFloatType fpp)
e =
    case e (BaseFloatType fpp) -> BaseTypeRepr (BaseFloatType fpp)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e (BaseFloatType fpp)
e of
      BaseFloatRepr FloatPrecisionRepr fpp
fpp -> FloatPrecisionRepr fpp
FloatPrecisionRepr fpp
fpp

  -- | Print a sym expression for debugging or display purposes.
  printSymExpr :: e tp -> Doc ann


newtype ArrayResultWrapper f idx tp =
  ArrayResultWrapper { ArrayResultWrapper f idx tp -> f (BaseArrayType idx tp)
unwrapArrayResult :: f (BaseArrayType idx tp) }

instance TestEquality f => TestEquality (ArrayResultWrapper f idx) where
  testEquality :: ArrayResultWrapper f idx a
-> ArrayResultWrapper f idx b -> Maybe (a :~: b)
testEquality (ArrayResultWrapper f (BaseArrayType idx a)
x) (ArrayResultWrapper f (BaseArrayType idx b)
y) = do
    BaseArrayType idx a :~: BaseArrayType idx b
Refl <- f (BaseArrayType idx a)
-> f (BaseArrayType idx b)
-> Maybe (BaseArrayType idx a :~: BaseArrayType idx b)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f (BaseArrayType idx a)
x f (BaseArrayType idx b)
y
    (a :~: a) -> Maybe (a :~: a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl

instance HashableF e => HashableF (ArrayResultWrapper e idx) where
  hashWithSaltF :: Int -> ArrayResultWrapper e idx tp -> Int
hashWithSaltF Int
s (ArrayResultWrapper e (BaseArrayType idx tp)
v) = Int -> e (BaseArrayType idx tp) -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
s e (BaseArrayType idx tp)
v


-- | This datatype describes events that involve interacting with
--   solvers.  A @SolverEvent@ will be provided to the action
--   installed via @setSolverLogListener@ whenever an interesting
--   event occurs.
data SolverEvent
  = SolverStartSATQuery
    { SolverEvent -> String
satQuerySolverName :: !String
    , SolverEvent -> String
satQueryReason     :: !String
    }
  | SolverEndSATQuery
    { SolverEvent -> SatResult () ()
satQueryResult     :: !(SatResult () ())
    , SolverEvent -> Maybe String
satQueryError      :: !(Maybe String)
    }
 deriving (Int -> SolverEvent -> ShowS
[SolverEvent] -> ShowS
SolverEvent -> String
(Int -> SolverEvent -> ShowS)
-> (SolverEvent -> String)
-> ([SolverEvent] -> ShowS)
-> Show SolverEvent
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolverEvent] -> ShowS
$cshowList :: [SolverEvent] -> ShowS
show :: SolverEvent -> String
$cshow :: SolverEvent -> String
showsPrec :: Int -> SolverEvent -> ShowS
$cshowsPrec :: Int -> SolverEvent -> ShowS
Show, (forall x. SolverEvent -> Rep SolverEvent x)
-> (forall x. Rep SolverEvent x -> SolverEvent)
-> Generic SolverEvent
forall x. Rep SolverEvent x -> SolverEvent
forall x. SolverEvent -> Rep SolverEvent x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SolverEvent x -> SolverEvent
$cfrom :: forall x. SolverEvent -> Rep SolverEvent x
Generic)

------------------------------------------------------------------------
-- SymNat

-- | Symbolic natural numbers.
newtype SymNat sym =
  SymNat
  { -- Internal Invariant: the value in a SymNat is always nonnegative
    SymNat sym -> SymExpr sym BaseIntegerType
_symNat :: SymExpr sym BaseIntegerType
  }

-- | Return nat if this is a constant natural number.
asNat :: IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat :: SymNat sym -> Maybe Natural
asNat (SymNat SymExpr sym BaseIntegerType
x) = Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> (Integer -> Integer) -> Integer -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (Integer -> Natural) -> Maybe Integer -> Maybe Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymExpr sym BaseIntegerType -> Maybe Integer
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger SymExpr sym BaseIntegerType
x

-- | A natural number literal.
natLit :: IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
-- @Natural@ input is necessarily nonnegative
natLit :: sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
x = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
x)

-- | Add two natural numbers.
natAdd :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
-- Integer addition preserves nonnegative values
natAdd :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natAdd sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intAdd sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y

-- | Subtract one number from another.
--
-- The result is 0 if the subtraction would otherwise be negative.
natSub :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natSub :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natSub sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) =
  do SymExpr sym BaseIntegerType
z <- sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intSub sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
     SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMax sym
sym SymExpr sym BaseIntegerType
z (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> IO (SymExpr sym BaseIntegerType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0)

-- | Multiply one number by another.
natMul :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
-- Integer multiplication preserves nonnegative values
natMul :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMul sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMul sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y

-- | @'natDiv' sym x y@ performs division on naturals.
--
-- The result is undefined if @y@ equals @0@.
--
-- 'natDiv' and 'natMod' satisfy the property that given
--
-- @
--   d <- natDiv sym x y
--   m <- natMod sym x y
-- @
--
--  and @y > 0@, we have that @y * d + m = x@ and @m < y@.
natDiv :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
-- Integer division preserves nonnegative values.
natDiv :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natDiv sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intDiv sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y

-- | @'natMod' sym x y@ returns @x@ mod @y@.
--
-- See 'natDiv' for a description of the properties the return
-- value is expected to satisfy.
natMod :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
-- Integer modulus preserves nonnegative values.
natMod :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMod sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMod sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y

-- | If-then-else applied to natural numbers.
natIte :: IsExprBuilder sym => sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
-- ITE preserves nonnegative values.
natIte :: sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym Pred sym
p (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Pred sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
p SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y

-- | Equality predicate for natural numbers.
natEq :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq :: sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intEq sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y

-- | @'natLe' sym x y@ returns @true@ if @x <= y@.
natLe :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe :: sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y

-- | @'natLt' sym x y@ returns @true@ if @x < y@.
natLt :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt :: sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt sym
sym SymNat sym
x SymNat sym
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe sym
sym SymNat sym
y SymNat sym
x

-- | Convert a natural number to an integer.
natToInteger :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymInteger sym)
natToInteger :: sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
_sym (SymNat SymInteger sym
x) = SymInteger sym -> IO (SymInteger sym)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymInteger sym
x

-- | Convert the unsigned value of a bitvector to a natural.
bvToNat :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymNat sym)
-- The unsigned value of a bitvector is always nonnegative
bvToNat :: sym -> SymBV sym w -> IO (SymNat sym)
bvToNat sym
sym SymBV sym w
x = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> IO (SymExpr sym BaseIntegerType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
bvToInteger sym
sym SymBV sym w
x

-- | Convert a natural number to a real number.
natToReal :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymReal sym)
natToReal :: sym -> SymNat sym -> IO (SymReal sym)
natToReal sym
sym = sym -> SymNat sym -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
sym (SymNat sym -> IO (SymExpr sym BaseIntegerType))
-> (SymExpr sym BaseIntegerType -> IO (SymReal sym))
-> SymNat sym
-> IO (SymReal sym)
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> sym -> SymExpr sym BaseIntegerType -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym

-- | Convert an integer to a natural number.
--
-- For negative integers, the result is clamped to 0.
integerToNat :: IsExprBuilder sym => sym -> SymInteger sym -> IO (SymNat sym)
integerToNat :: sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym SymInteger sym
x = SymInteger sym -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymInteger sym -> SymNat sym)
-> IO (SymInteger sym) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMax sym
sym SymInteger sym
x (SymInteger sym -> IO (SymInteger sym))
-> IO (SymInteger sym) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0)

-- | Convert a real number to a natural number.
--
-- The result is undefined if the given real number does not represent a natural number.
realToNat :: IsExprBuilder sym => sym -> SymReal sym -> IO (SymNat sym)
realToNat :: sym -> SymReal sym -> IO (SymNat sym)
realToNat sym
sym SymReal sym
r = sym -> SymReal sym -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realToInteger sym
sym SymReal sym
r IO (SymExpr sym BaseIntegerType)
-> (SymExpr sym BaseIntegerType -> IO (SymNat sym))
-> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= sym -> SymExpr sym BaseIntegerType -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym

-- | Create a fresh natural number constant with optional lower and upper bounds.
--   If provided, the bounds are inclusive.
--   If inconsistent bounds are given, an InvalidRange exception will be thrown.
freshBoundedNat ::
  IsSymExprBuilder sym =>
  sym ->
  SolverSymbol ->
  Maybe Natural {- ^ lower bound -} ->
  Maybe Natural {- ^ upper bound -} ->
  IO (SymNat sym)
freshBoundedNat :: sym
-> SolverSymbol
-> Maybe Natural
-> Maybe Natural
-> IO (SymNat sym)
freshBoundedNat sym
sym SolverSymbol
s Maybe Natural
lo Maybe Natural
hi = SymExpr sym BaseIntegerType -> SymNat sym
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat (SymExpr sym BaseIntegerType -> SymNat sym)
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym
-> SolverSymbol
-> Maybe Integer
-> Maybe Integer
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Maybe Integer
-> Maybe Integer
-> IO (SymInteger sym)
freshBoundedInt sym
sym SolverSymbol
s Maybe Integer
lo' Maybe Integer
hi')
 where
   lo' :: Maybe Integer
lo' = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> (Natural -> Integer) -> Maybe Natural -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
0 Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Maybe Natural
lo)
   hi' :: Maybe Integer
hi' = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer) -> Maybe Natural -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Natural
hi

-- | Create a fresh natural number constant.
freshNat :: IsSymExprBuilder sym => sym -> SolverSymbol -> IO (SymNat sym)
freshNat :: sym -> SolverSymbol -> IO (SymNat sym)
freshNat sym
sym SolverSymbol
s = sym
-> SolverSymbol
-> Maybe Natural
-> Maybe Natural
-> IO (SymNat sym)
forall sym.
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Maybe Natural
-> Maybe Natural
-> IO (SymNat sym)
freshBoundedNat sym
sym SolverSymbol
s (Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
0) Maybe Natural
forall a. Maybe a
Nothing

printSymNat :: IsExpr (SymExpr sym) => SymNat sym -> Doc ann
printSymNat :: SymNat sym -> Doc ann
printSymNat (SymNat SymExpr sym BaseIntegerType
x) = SymExpr sym BaseIntegerType -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym BaseIntegerType
x

instance TestEquality (SymExpr sym) => Eq (SymNat sym) where
  SymNat SymExpr sym BaseIntegerType
x == :: SymNat sym -> SymNat sym -> Bool
== SymNat SymExpr sym BaseIntegerType
y = Maybe (BaseIntegerType :~: BaseIntegerType) -> Bool
forall a. Maybe a -> Bool
isJust (SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> Maybe (BaseIntegerType :~: BaseIntegerType)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y)

instance OrdF (SymExpr sym) => Ord (SymNat sym) where
  compare :: SymNat sym -> SymNat sym -> Ordering
compare (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = OrderingF BaseIntegerType BaseIntegerType -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> OrderingF BaseIntegerType BaseIntegerType
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y)

instance HashableF (SymExpr sym) => Hashable (SymNat sym) where
  hashWithSalt :: Int -> SymNat sym -> Int
hashWithSalt Int
s (SymNat SymExpr sym BaseIntegerType
x) = Int -> SymExpr sym BaseIntegerType -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
s SymExpr sym BaseIntegerType
x

------------------------------------------------------------------------
-- IsExprBuilder

-- | This class allows the simulator to build symbolic expressions.
--
-- Methods of this class refer to type families @'SymExpr' sym@
-- and @'SymFn' sym@.
--
-- Note: Some methods in this class represent operations that are
-- partial functions on their domain (e.g., division by 0).
-- Such functions will have documentation strings indicating that they
-- are undefined under some conditions.  When partial functions are applied
-- outside their defined domains, they will silently produce an unspecified
-- value of the expected type.  The unspecified value returned as the result
-- of an undefined function is _not_ guaranteed to be equivalant to a free
-- constant, and no guarantees are made about what properties such values
-- will satisfy.
class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
      , TestEquality (SymAnnotation sym), OrdF (SymAnnotation sym)
      , HashableF (SymAnnotation sym)
      ) => IsExprBuilder sym where

  -- | Retrieve the configuration object corresponding to this solver interface.
  getConfiguration :: sym -> Config


  -- | Install an action that will be invoked before and after calls to
  --   backend solvers.  This action is primarily intended to be used for
  --   logging\/profiling\/debugging purposes.  Passing 'Nothing' to this
  --   function disables logging.
  setSolverLogListener :: sym -> Maybe (SolverEvent -> IO ()) -> IO ()

  -- | Get the currently-installed solver log listener, if one has been installed.
  getSolverLogListener :: sym -> IO (Maybe (SolverEvent -> IO ()))

  -- | Provide the given event to the currently installed
  --   solver log listener, if any.
  logSolverEvent :: sym -> SolverEvent -> IO ()

  -- | Get statistics on execution from the initialization of the
  -- symbolic interface to this point.  May return zeros if gathering
  -- statistics isn't supported.
  getStatistics :: sym -> IO Statistics
  getStatistics sym
_ = Statistics -> IO Statistics
forall (m :: Type -> Type) a. Monad m => a -> m a
return Statistics
zeroStatistics

  ----------------------------------------------------------------------
  -- Program location operations

  -- | Get current location of program for term creation purposes.
  getCurrentProgramLoc :: sym -> IO ProgramLoc

  -- | Set current location of program for term creation purposes.
  setCurrentProgramLoc :: sym -> ProgramLoc -> IO ()

  -- | Return true if two expressions are equal. The default
  -- implementation dispatches 'eqPred', 'bvEq', 'natEq', 'intEq',
  -- 'realEq', 'cplxEq', 'structEq', or 'arrayEq', depending on the
  -- type.
  isEq :: sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
  isEq sym
sym SymExpr sym tp
x SymExpr sym tp
y =
    case SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymExpr sym tp
x of
      BaseTypeRepr tp
BaseBoolRepr     -> sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
eqPred sym
sym SymExpr sym tp
Pred sym
x SymExpr sym tp
Pred sym
y
      BaseBVRepr{}     -> sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym tp
SymBV sym w
x SymExpr sym tp
SymBV sym w
y
      BaseTypeRepr tp
BaseIntegerRepr  -> sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intEq sym
sym SymExpr sym tp
SymInteger sym
x SymExpr sym tp
SymInteger sym
y
      BaseTypeRepr tp
BaseRealRepr     -> sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymExpr sym tp
SymReal sym
x SymExpr sym tp
SymReal sym
y
      BaseFloatRepr{}  -> sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatEq sym
sym SymExpr sym tp
SymFloat sym fpp
x SymExpr sym tp
SymFloat sym fpp
y
      BaseTypeRepr tp
BaseComplexRepr  -> sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
cplxEq sym
sym SymExpr sym tp
SymCplx sym
x SymExpr sym tp
SymCplx sym
y
      BaseStringRepr{} -> sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
stringEq sym
sym SymExpr sym tp
SymString sym si
x SymExpr sym tp
SymString sym si
y
      BaseStructRepr{} -> sym -> SymStruct sym ctx -> SymStruct sym ctx -> IO (Pred sym)
forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> SymStruct sym flds -> IO (Pred sym)
structEq sym
sym SymExpr sym tp
SymStruct sym ctx
x SymExpr sym tp
SymStruct sym ctx
y
      BaseArrayRepr{}  -> sym
-> SymArray sym (idx ::> tp) xs
-> SymArray sym (idx ::> tp) xs
-> IO (Pred sym)
forall sym (idx :: Ctx BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym -> SymArray sym idx b -> SymArray sym idx b -> IO (Pred sym)
arrayEq sym
sym SymExpr sym tp
SymArray sym (idx ::> tp) xs
x SymExpr sym tp
SymArray sym (idx ::> tp) xs
y

  -- | Take the if-then-else of two expressions. The default
  -- implementation dispatches 'itePred', 'bvIte', 'natIte', 'intIte',
  -- 'realIte', 'cplxIte', 'structIte', or 'arrayIte', depending on
  -- the type.
  baseTypeIte :: sym
              -> Pred sym
              -> SymExpr sym tp
              -> SymExpr sym tp
              -> IO (SymExpr sym tp)
  baseTypeIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y =
    case SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymExpr sym tp
x of
      BaseTypeRepr tp
BaseBoolRepr     -> sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred   sym
sym Pred sym
c SymExpr sym tp
Pred sym
x SymExpr sym tp
Pred sym
y
      BaseBVRepr{}     -> sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte     sym
sym Pred sym
c SymExpr sym tp
SymBV sym w
x SymExpr sym tp
SymBV sym w
y
      BaseTypeRepr tp
BaseIntegerRepr  -> sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte    sym
sym Pred sym
c SymExpr sym tp
SymInteger sym
x SymExpr sym tp
SymInteger sym
y
      BaseTypeRepr tp
BaseRealRepr     -> sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte   sym
sym Pred sym
c SymExpr sym tp
SymReal sym
x SymExpr sym tp
SymReal sym
y
      BaseFloatRepr{}  -> sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatIte  sym
sym Pred sym
c SymExpr sym tp
SymFloat sym fpp
x SymExpr sym tp
SymFloat sym fpp
y
      BaseStringRepr{} -> sym
-> Pred sym
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
stringIte sym
sym Pred sym
c SymExpr sym tp
SymString sym si
x SymExpr sym tp
SymString sym si
y
      BaseTypeRepr tp
BaseComplexRepr  -> sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxIte   sym
sym Pred sym
c SymExpr sym tp
SymCplx sym
x SymExpr sym tp
SymCplx sym
y
      BaseStructRepr{} -> sym
-> Pred sym
-> SymStruct sym ctx
-> SymStruct sym ctx
-> IO (SymStruct sym ctx)
forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (SymStruct sym flds)
structIte sym
sym Pred sym
c SymExpr sym tp
SymStruct sym ctx
x SymExpr sym tp
SymStruct sym ctx
y
      BaseArrayRepr{}  -> sym
-> Pred sym
-> SymArray sym (idx ::> tp) xs
-> SymArray sym (idx ::> tp) xs
-> IO (SymArray sym (idx ::> tp) xs)
forall sym (idx :: Ctx BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (SymArray sym idx b)
arrayIte  sym
sym Pred sym
c SymExpr sym tp
SymArray sym (idx ::> tp) xs
x SymExpr sym tp
SymArray sym (idx ::> tp) xs
y

  -- | Given a symbolic expression, annotate it with a unique identifier
  --   that can be used to maintain a connection with the given term.
  --   The 'SymAnnotation' is intended to be used as the key in a hash
  --   table or map to additional data can be maintained alongside the terms.
  --   The returned 'SymExpr' has the same semantics as the argument, but
  --   has embedded in it the 'SymAnnotation' value so that it can be used
  --   later during term traversals.
  --
  --   Note, the returned annotation is not necessarily fresh; if an
  --   already-annotated term is passed in, the same annotation value will be
  --   returned.
  annotateTerm :: sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)

  -- | Project an annotation from an expression
  --
  -- It should be the case that using 'getAnnotation' on a term returned by
  -- 'annotateTerm' returns the same annotation that 'annotateTerm' did.
  getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)

  ----------------------------------------------------------------------
  -- Boolean operations.

  -- | Constant true predicate
  truePred  :: sym -> Pred sym

  -- | Constant false predicate
  falsePred :: sym -> Pred sym

  -- | Boolean negation
  notPred :: sym -> Pred sym -> IO (Pred sym)

  -- | Boolean conjunction
  andPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

  -- | Boolean disjunction
  orPred  :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

  -- | Boolean implication
  impliesPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
  impliesPred sym
sym Pred sym
x Pred sym
y = do
    Pred sym
nx <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
x
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
y Pred sym
nx

  -- | Exclusive-or operation
  xorPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

  -- | Equality of boolean values
  eqPred  :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

  -- | If-then-else on a predicate.
  itePred :: sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)

  ----------------------------------------------------------------------
  -- Integer operations

  -- | Create an integer literal.
  intLit :: sym -> Integer -> IO (SymInteger sym)

  -- | Negate an integer.
  intNeg :: sym -> SymInteger sym -> IO (SymInteger sym)

  -- | Add two integers.
  intAdd :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

  -- | Subtract one integer from another.
  intSub :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  intSub sym
sym SymInteger sym
x SymInteger sym
y = sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intAdd sym
sym SymInteger sym
x (SymInteger sym -> IO (SymInteger sym))
-> IO (SymInteger sym) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
intNeg sym
sym SymInteger sym
y

  -- | Multiply one integer by another.
  intMul :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

  -- | Return the minimum value of two integers.
  intMin :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  intMin sym
sym SymInteger sym
x SymInteger sym
y =
    do Pred sym
p <- sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
x SymInteger sym
y
       sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
p SymInteger sym
x SymInteger sym
y

  -- | Return the maximum value of two integers.
  intMax :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  intMax sym
sym SymInteger sym
x SymInteger sym
y =
    do Pred sym
p <- sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
x SymInteger sym
y
       sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
p SymInteger sym
y SymInteger sym
x

  -- | If-then-else applied to integers.
  intIte :: sym -> Pred sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

  -- | Integer equality.
  intEq  :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)

  -- | Integer less-than-or-equal.
  intLe  :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)

  -- | Integer less-than.
  intLt  :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
  intLt sym
sym SymInteger sym
x SymInteger sym
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
y SymInteger sym
x

  -- | Compute the absolute value of an integer.
  intAbs :: sym -> SymInteger sym -> IO (SymInteger sym)

  -- | @intDiv x y@ computes the integer division of @x@ by @y@.  This division is
  --   interpreted the same way as the SMT-Lib integer theory, which states that
  --   @div@ and @mod@ are the unique Euclidean division operations satisfying the
  --   following for all @y /= 0@:
  --
  --   * @y * (div x y) + (mod x y) == x@
  --   * @ 0 <= mod x y < abs y@
  --
  --   The value of @intDiv x y@ is undefined when @y = 0@.
  --
  --   Integer division requires nonlinear support whenever the divisor is
  --   not a constant.
  --
  --   Note: @div x y@ is @floor (x/y)@ when @y@ is positive
  --   (regardless of sign of @x@) and @ceiling (x/y)@ when @y@ is
  --   negative.  This is neither of the more common "round toward
  --   zero" nor "round toward -inf" definitions.
  --
  --   Some useful theorems that are true of this division/modulus pair:
  --
  --   * @mod x y == mod x (- y) == mod x (abs y)@
  --   * @div x (-y) == -(div x y)@
  intDiv :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

  -- | @intMod x y@ computes the integer modulus of @x@ by @y@.  See 'intDiv' for
  --   more details.
  --
  --   The value of @intMod x y@ is undefined when @y = 0@.
  --
  --   Integer modulus requires nonlinear support whenever the divisor is
  --   not a constant.
  intMod :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

  -- | @intDivisible x k@ is true whenever @x@ is an integer divisible
  --   by the known natural number @k@.  In other words `divisible x k`
  --   holds if there exists an integer `z` such that `x = k*z`.
  intDivisible :: sym -> SymInteger sym -> Natural -> IO (Pred sym)

  ----------------------------------------------------------------------
  -- Bitvector operations

  -- | Create a bitvector with the given width and value.
  bvLit :: (1 <= w) => sym -> NatRepr w -> BV.BV w -> IO (SymBV sym w)

  -- | Concatenate two bitvectors.
  bvConcat :: (1 <= u, 1 <= v)
           => sym
           -> SymBV sym u  -- ^ most significant bits
           -> SymBV sym v  -- ^ least significant bits
           -> IO (SymBV sym (u+v))

  -- | Select a subsequence from a bitvector.
  bvSelect :: forall idx n w. (1 <= n, idx + n <= w)
           => sym
           -> NatRepr idx  -- ^ Starting index, from 0 as least significant bit
           -> NatRepr n    -- ^ Number of bits to take
           -> SymBV sym w  -- ^ Bitvector to select from
           -> IO (SymBV sym n)

  -- | 2's complement negation.
  bvNeg :: (1 <= w)
        => sym
        -> SymBV sym w
        -> IO (SymBV sym w)

  -- | Add two bitvectors.
  bvAdd :: (1 <= w)
        => sym
        -> SymBV sym w
        -> SymBV sym w
        -> IO (SymBV sym w)

  -- | Subtract one bitvector from another.
  bvSub :: (1 <= w)
        => sym
        -> SymBV sym w
        -> SymBV sym w
        -> IO (SymBV sym w)
  bvSub sym
sym SymBV sym w
x SymBV sym w
y = sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymBV sym w
x (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvNeg sym
sym SymBV sym w
y

  -- | Multiply one bitvector by another.
  bvMul :: (1 <= w)
        => sym
        -> SymBV sym w
        -> SymBV sym w
        -> IO (SymBV sym w)

  -- | Unsigned bitvector division.
  --
  --   The result of @bvUdiv x y@ is undefined when @y@ is zero,
  --   but is otherwise equal to @floor( x / y )@.
  bvUdiv :: (1 <= w)
         => sym
         -> SymBV sym w
         -> SymBV sym w
         -> IO (SymBV sym w)

  -- | Unsigned bitvector remainder.
  --
  --   The result of @bvUrem x y@ is undefined when @y@ is zero,
  --   but is otherwise equal to @x - (bvUdiv x y) * y@.
  bvUrem :: (1 <= w)
         => sym
         -> SymBV sym w
         -> SymBV sym w
         -> IO (SymBV sym w)

  -- | Signed bitvector division.  The result is truncated to zero.
  --
  --   The result of @bvSdiv x y@ is undefined when @y@ is zero,
  --   but is equal to @floor(x/y)@ when @x@ and @y@ have the same sign,
  --   and equal to @ceiling(x/y)@ when @x@ and @y@ have opposite signs.
  --
  --   NOTE! However, that there is a corner case when dividing @MIN_INT@ by
  --   @-1@, in which case an overflow condition occurs, and the result is instead
  --   @MIN_INT@.
  bvSdiv :: (1 <= w)
         => sym
         -> SymBV sym w
         -> SymBV sym w
         -> IO (SymBV sym w)

  -- | Signed bitvector remainder.
  --
  --   The result of @bvSrem x y@ is undefined when @y@ is zero, but is
  --   otherwise equal to @x - (bvSdiv x y) * y@.
  bvSrem :: (1 <= w)
         => sym
         -> SymBV sym w
         -> SymBV sym w
         -> IO (SymBV sym w)

  -- | Returns true if the corresponding bit in the bitvector is set.
  testBitBV :: (1 <= w)
            => sym
            -> Natural -- ^ Index of bit (0 is the least significant bit)
            -> SymBV sym w
            -> IO (Pred sym)

  -- | Return true if bitvector is negative.
  bvIsNeg :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
  bvIsNeg sym
sym SymBV sym w
x = sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
x (SymBV sym w -> IO (Pred sym)) -> IO (SymBV sym w) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x) (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x))

  -- | If-then-else applied to bitvectors.
  bvIte :: (1 <= w)
        => sym
        -> Pred sym
        -> SymBV sym w
        -> SymBV sym w
        -> IO (SymBV sym w)

  -- | Return true if bitvectors are equal.
  bvEq  :: (1 <= w)
        => sym
        -> SymBV sym w
        -> SymBV sym w
        -> IO (Pred sym)

  -- | Return true if bitvectors are distinct.
  bvNe  :: (1 <= w)
        => sym
        -> SymBV sym w
        -> SymBV sym w
        -> IO (Pred sym)
  bvNe sym
sym SymBV sym w
x SymBV sym w
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
x SymBV sym w
y

  -- | Unsigned less-than.
  bvUlt  :: (1 <= w)
         => sym
         -> SymBV sym w
         -> SymBV sym w
         -> IO (Pred sym)

  -- | Unsigned less-than-or-equal.
  bvUle  :: (1 <= w)
         => sym
         -> SymBV sym w
         -> SymBV sym w
         -> IO (Pred sym)
  bvUle sym
sym SymBV sym w
x SymBV sym w
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
y SymBV sym w
x

  -- | Unsigned greater-than-or-equal.
  bvUge :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  bvUge sym
sym SymBV sym w
x SymBV sym w
y = sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym w
y SymBV sym w
x

  -- | Unsigned greater-than.
  bvUgt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  bvUgt sym
sym SymBV sym w
x SymBV sym w
y = sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
y SymBV sym w
x

  -- | Signed less-than.
  bvSlt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

  -- | Signed greater-than.
  bvSgt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  bvSgt sym
sym SymBV sym w
x SymBV sym w
y = sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
y SymBV sym w
x

  -- | Signed less-than-or-equal.
  bvSle :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  bvSle sym
sym SymBV sym w
x SymBV sym w
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
y SymBV sym w
x

  -- | Signed greater-than-or-equal.
  bvSge :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  bvSge sym
sym SymBV sym w
x SymBV sym w
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
x SymBV sym w
y

  -- | returns true if the given bitvector is non-zero.
  bvIsNonzero :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)

  -- | Left shift.  The shift amount is treated as an unsigned value.
  bvShl :: (1 <= w) => sym ->
                       SymBV sym w {- ^ Shift this -} ->
                       SymBV sym w {- ^ Amount to shift by -} ->
                       IO (SymBV sym w)

  -- | Logical right shift.  The shift amount is treated as an unsigned value.
  bvLshr :: (1 <= w) => sym ->
                        SymBV sym w {- ^ Shift this -} ->
                        SymBV sym w {- ^ Amount to shift by -} ->
                        IO (SymBV sym w)

  -- | Arithmetic right shift.  The shift amount is treated as an
  -- unsigned value.
  bvAshr :: (1 <= w) => sym ->
                        SymBV sym w {- ^ Shift this -} ->
                        SymBV sym w {- ^ Amount to shift by -} ->
                        IO (SymBV sym w)

  -- | Rotate left.  The rotate amount is treated as an unsigned value.
  bvRol :: (1 <= w) =>
    sym ->
    SymBV sym w {- ^ bitvector to rotate -} ->
    SymBV sym w {- ^ amount to rotate by -} ->
    IO (SymBV sym w)

  -- | Rotate right.  The rotate amount is treated as an unsigned value.
  bvRor :: (1 <= w) =>
    sym ->
    SymBV sym w {- ^ bitvector to rotate -} ->
    SymBV sym w {- ^ amount to rotate by -} ->
    IO (SymBV sym w)

  -- | Zero-extend a bitvector.
  bvZext :: (1 <= u, u+1 <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)

  -- | Sign-extend a bitvector.
  bvSext :: (1 <= u, u+1 <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)

  -- | Truncate a bitvector.
  bvTrunc :: (1 <= r, r+1 <= w) -- Assert result is less than input.
          => sym
          -> NatRepr r
          -> SymBV sym w
          -> IO (SymBV sym r)
  bvTrunc sym
sym NatRepr r
w SymBV sym w
x
    | LeqProof r w
LeqProof <- LeqProof r (r + 1) -> LeqProof (r + 1) w -> LeqProof r w
forall (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans
        (NatRepr r -> NatRepr 1 -> LeqProof r (r + 1)
forall (f :: Nat -> Type) (n :: Nat) (g :: Nat -> Type) (m :: Nat).
f n -> g m -> LeqProof n (n + m)
addIsLeq NatRepr r
w (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1))
        (NatRepr (r + 1) -> NatRepr w -> LeqProof (r + 1) w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (NatRepr r -> NatRepr (r + 1)
forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
incNat NatRepr r
w) (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x))
    = sym -> NatRepr 0 -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
bvSelect sym
sym (KnownNat 0 => NatRepr 0
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @0) NatRepr r
w SymBV sym w
x

  -- | Bitwise logical and.
  bvAndBits :: (1 <= w)
            => sym
            -> SymBV sym w
            -> SymBV sym w
            -> IO (SymBV sym w)

  -- | Bitwise logical or.
  bvOrBits  :: (1 <= w)
            => sym
            -> SymBV sym w
            -> SymBV sym w
            -> IO (SymBV sym w)

  -- | Bitwise logical exclusive or.
  bvXorBits :: (1 <= w)
            => sym
            -> SymBV sym w
            -> SymBV sym w
            -> IO (SymBV sym w)

  -- | Bitwise complement.
  bvNotBits :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)

  -- | @bvSet sym v i p@ returns a bitvector @v'@ where bit @i@ of @v'@ is set to
  -- @p@, and the bits at the other indices are the same as in @v@.
  bvSet :: forall w
         . (1 <= w)
        => sym         -- ^ Symbolic interface
        -> SymBV sym w -- ^ Bitvector to update
        -> Natural     -- ^ 0-based index to set
        -> Pred sym    -- ^ Predicate to set.
        -> IO (SymBV sym w)
  bvSet sym
sym SymBV sym w
v Natural
i Pred sym
p = Bool -> IO (SymBV sym w) -> IO (SymBV sym w)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
v)) (IO (SymBV sym w) -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$
    -- NB, this representation based on AND/XOR structure is designed so that a
    -- sequence of bvSet operations will collapse nicely into a xor-linear combination
    -- of the original term and bvFill terms. It has the nice property that we
    -- do not introduce any additional subterm sharing.
    do let w :: NatRepr w
w    = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
v
       let mask :: BV w
mask = NatRepr w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> Natural -> BV w
BV.bit' NatRepr w
w Natural
i
       SymBV sym w
pbits <- sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
bvFill sym
sym NatRepr w
w Pred sym
p
       SymBV sym w
vbits <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAndBits sym
sym SymBV sym w
v (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.complement NatRepr w
w BV w
mask)
       sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvXorBits sym
sym SymBV sym w
vbits (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAndBits sym
sym SymBV sym w
pbits (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
mask

  -- | @bvFill sym w p@ returns a bitvector @w@-bits long where every bit
  --   is given by the boolean value of @p@.
  bvFill :: forall w. (1 <= w) =>
    sym       {-^ symbolic interface -} ->
    NatRepr w {-^ output bitvector width -} ->
    Pred sym  {-^ predicate to fill the bitvector with -} ->
    IO (SymBV sym w)

  -- | Return the bitvector of the desired width with all 0 bits;
  --   this is the minimum unsigned integer.
  minUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  minUnsignedBV sym
sym NatRepr w
w = sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)

  -- | Return the bitvector of the desired width with all bits set;
  --   this is the maximum unsigned integer.
  maxUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  maxUnsignedBV sym
sym NatRepr w
w = sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w)

  -- | Return the bitvector representing the largest 2's complement
  --   signed integer of the given width.  This consists of all bits
  --   set except the MSB.
  maxSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  maxSignedBV sym
sym NatRepr w
w = sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
w)

  -- | Return the bitvector representing the smallest 2's complement
  --   signed integer of the given width. This consists of all 0 bits
  --   except the MSB, which is set.
  minSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  minSignedBV sym
sym NatRepr w
w = sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w)

  -- | Return the number of 1 bits in the input.
  bvPopcount :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)

  -- | Return the number of consecutive 0 bits in the input, starting from
  --   the most significant bit position.  If the input is zero, all bits are counted
  --   as leading.
  bvCountLeadingZeros :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)

  -- | Return the number of consecutive 0 bits in the input, starting from
  --   the least significant bit position.  If the input is zero, all bits are counted
  --   as leading.
  bvCountTrailingZeros :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)

  -- | Unsigned add with overflow bit.
  addUnsignedOF :: (1 <= w)
                => sym
                -> SymBV sym w
                -> SymBV sym w
                -> IO (Pred sym, SymBV sym w)
  addUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
    -- Compute result
    SymBV sym w
r   <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymBV sym w
x SymBV sym w
y
    -- Return that this overflows if r is less than either x or y
    Pred sym
ovx  <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
r SymBV sym w
x
    Pred sym
ovy  <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
r SymBV sym w
y
    Pred sym
ov   <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
ovx Pred sym
ovy
    (Pred sym, SymBV sym w) -> IO (Pred sym, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
r)

  -- | Signed add with overflow bit. Overflow is true if positive +
  -- positive = negative, or if negative + negative = positive.
  addSignedOF :: (1 <= w)
              => sym
              -> SymBV sym w
              -> SymBV sym w
              -> IO (Pred sym, SymBV sym w)
  addSignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
    SymBV sym w
xy  <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymBV sym w
x SymBV sym w
y
    Pred sym
sx  <- sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x
    Pred sym
sy  <- sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
y
    Pred sym
sxy <- sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
xy

    Pred sym
not_sx  <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
sx
    Pred sym
not_sy  <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
sy
    Pred sym
not_sxy <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
sxy

    -- Return this overflowed if the sign bits of sx and sy are equal,
    -- but different from sxy.
    Pred sym
ov1 <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
not_sxy (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
sx Pred sym
sy
    Pred sym
ov2 <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
sxy (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
not_sx Pred sym
not_sy

    Pred sym
ov  <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
ov1 Pred sym
ov2
    (Pred sym, SymBV sym w) -> IO (Pred sym, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
xy)

  -- | Unsigned subtract with overflow bit. Overflow is true if x < y.
  subUnsignedOF ::
    (1 <= w) =>
    sym ->
    SymBV sym w ->
    SymBV sym w ->
    IO (Pred sym, SymBV sym w)
  subUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
    SymBV sym w
xy <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
x SymBV sym w
y
    Pred sym
ov <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
x SymBV sym w
y
    (Pred sym, SymBV sym w) -> IO (Pred sym, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
xy)

  -- | Signed subtract with overflow bit. Overflow is true if positive
  -- - negative = negative, or if negative - positive = positive.
  subSignedOF :: (1 <= w)
              => sym
              -> SymBV sym w
              -> SymBV sym w
              -> IO (Pred sym, SymBV sym w)
  subSignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
       SymBV sym w
xy  <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
x SymBV sym w
y
       Pred sym
sx  <- sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x
       Pred sym
sy  <- sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
y
       Pred sym
sxy <- sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
xy
       Pred sym
ov  <- IO (IO (Pred sym)) -> IO (Pred sym)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join ((Pred sym -> Pred sym -> IO (Pred sym))
-> IO (Pred sym -> Pred sym -> IO (Pred sym))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym) IO (Pred sym -> Pred sym -> IO (Pred sym))
-> IO (Pred sym) -> IO (Pred sym -> IO (Pred sym))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
xorPred sym
sym Pred sym
sx Pred sym
sxy IO (Pred sym -> IO (Pred sym))
-> IO (Pred sym) -> IO (IO (Pred sym))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
xorPred sym
sym Pred sym
sx Pred sym
sy)
       (Pred sym, SymBV sym w) -> IO (Pred sym, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
xy)


  -- | Compute the carry-less multiply of the two input bitvectors.
  --   This operation is essentially the same as a standard multiply, except that
  --   the partial addends are simply XOR'd together instead of using a standard
  --   adder.  This operation is useful for computing on GF(2^n) polynomials.
  carrylessMultiply ::
    (1 <= w) =>
    sym ->
    SymBV sym w ->
    SymBV sym w ->
    IO (SymBV sym (w+w))
  carrylessMultiply sym
sym SymBV sym w
x0 SymBV sym w
y0
    | Just Integer
_  <- BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym w -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
x0
    , Maybe Integer
Nothing <- BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym w -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
y0
    = SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
forall (w :: Nat).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
go SymBV sym w
y0 SymBV sym w
x0
    | Bool
otherwise
    = SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
forall (w :: Nat).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
go SymBV sym w
x0 SymBV sym w
y0
   where
   go :: (1 <= w) => SymBV sym w -> SymBV sym w -> IO (SymBV sym (w+w))
   go :: SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
go SymBV sym w
x SymBV sym w
y =
    do let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
       let w2 :: NatRepr (w + w)
w2 = NatRepr w -> NatRepr w -> NatRepr (w + w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
       -- 1 <= w
       one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- LeqProof 1 w -> IO (LeqProof 1 w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr 1 -> NatRepr w -> LeqProof 1 w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
       -- 1 <= w implies 1 <= w + w
       LeqProof 1 (w + w)
LeqProof <- LeqProof 1 (w + w) -> IO (LeqProof 1 (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof 1 w -> NatRepr w -> LeqProof 1 (w + w)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
       -- w <= w
       w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- LeqProof w w -> IO (LeqProof w w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> NatRepr w -> LeqProof w w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
       -- w <= w, 1 <= w implies w + 1 <= w + w
       LeqProof (w + 1) (w + w)
LeqProof <- LeqProof (w + 1) (w + w) -> IO (LeqProof (w + 1) (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof w w -> LeqProof 1 w -> LeqProof (w + 1) (w + w)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
       SymBV sym (w + w)
z  <- sym -> NatRepr (w + w) -> BV (w + w) -> IO (SymBV sym (w + w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
w2 (NatRepr (w + w) -> BV (w + w)
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr (w + w)
w2)
       SymBV sym (w + w)
x' <- sym -> NatRepr (w + w) -> SymBV sym w -> IO (SymBV sym (w + w))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
w2 SymBV sym w
x
       [SymBV sym (w + w)]
xs <- [IO (SymBV sym (w + w))] -> IO [SymBV sym (w + w)]
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ do Pred sym
p <- sym -> Natural -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
testBitBV sym
sym (BV (w + w) -> Natural
forall (w :: Nat). BV w -> Natural
BV.asNatural BV (w + w)
i) SymBV sym w
y
                           (sym
 -> Pred sym
 -> SymBV sym (w + w)
 -> SymBV sym (w + w)
 -> IO (SymBV sym (w + w)))
-> sym
-> Pred sym
-> IO (SymBV sym (w + w))
-> IO (SymBV sym (w + w))
-> IO (SymBV sym (w + w))
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym
-> Pred sym
-> SymBV sym (w + w)
-> SymBV sym (w + w)
-> IO (SymBV sym (w + w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym
                             Pred sym
p
                             (sym
-> SymBV sym (w + w) -> SymBV sym (w + w) -> IO (SymBV sym (w + w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvShl sym
sym SymBV sym (w + w)
x' (SymBV sym (w + w) -> IO (SymBV sym (w + w)))
-> IO (SymBV sym (w + w)) -> IO (SymBV sym (w + w))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr (w + w) -> BV (w + w) -> IO (SymBV sym (w + w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
w2 BV (w + w)
i)
                             (SymBV sym (w + w) -> IO (SymBV sym (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym (w + w)
z)
                      | BV (w + w)
i <- BV (w + w) -> BV (w + w) -> [BV (w + w)]
forall (w :: Nat). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned (NatRepr (w + w) -> BV (w + w)
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr (w + w)
w2) (NatRepr (w + w) -> Integer -> BV (w + w)
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr (w + w)
w2 (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))
                      ]
       (SymBV sym (w + w) -> SymBV sym (w + w) -> IO (SymBV sym (w + w)))
-> SymBV sym (w + w)
-> [SymBV sym (w + w)]
-> IO (SymBV sym (w + w))
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sym
-> SymBV sym (w + w) -> SymBV sym (w + w) -> IO (SymBV sym (w + w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvXorBits sym
sym) SymBV sym (w + w)
z [SymBV sym (w + w)]
xs

  -- | @unsignedWideMultiplyBV sym x y@ multiplies two unsigned 'w' bit numbers 'x' and 'y'.
  --
  -- It returns a pair containing the top 'w' bits as the first element, and the
  -- lower 'w' bits as the second element.
  unsignedWideMultiplyBV :: (1 <= w)
                         => sym
                         -> SymBV sym w
                         -> SymBV sym w
                         -> IO (SymBV sym w, SymBV sym w)
  unsignedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y = do
       let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
       let dbl_w :: NatRepr (w + w)
dbl_w = NatRepr w -> NatRepr w -> NatRepr (w + w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
       -- 1 <= w
       one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- LeqProof 1 w -> IO (LeqProof 1 w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr 1 -> NatRepr w -> LeqProof 1 w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
       -- 1 <= w implies 1 <= w + w
       LeqProof 1 (w + w)
LeqProof <- LeqProof 1 (w + w) -> IO (LeqProof 1 (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof 1 w -> NatRepr w -> LeqProof 1 (w + w)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
       -- w <= w
       w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- LeqProof w w -> IO (LeqProof w w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> NatRepr w -> LeqProof w w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
       -- w <= w, 1 <= w implies w + 1 <= w + w
       LeqProof (w + 1) (w + w)
LeqProof <- LeqProof (w + 1) (w + w) -> IO (LeqProof (w + 1) (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof w w -> LeqProof 1 w -> LeqProof (w + 1) (w + w)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
       SymExpr sym (BaseBVType (w + w))
x'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
       SymExpr sym (BaseBVType (w + w))
y'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
       SymExpr sym (BaseBVType (w + w))
s   <- sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
       SymBV sym w
lo  <- sym
-> NatRepr w
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s
       SymExpr sym (BaseBVType (w + w))
n   <- sym
-> NatRepr (w + w)
-> BV (w + w)
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (NatRepr (w + w) -> BV w -> BV (w + w)
forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr (w + w)
dbl_w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.width NatRepr w
w))
       SymBV sym w
hi  <- sym
-> NatRepr w
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w (SymExpr sym (BaseBVType (w + w)) -> IO (SymBV sym w))
-> IO (SymExpr sym (BaseBVType (w + w))) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvLshr sym
sym SymExpr sym (BaseBVType (w + w))
s SymExpr sym (BaseBVType (w + w))
n
       (SymBV sym w, SymBV sym w) -> IO (SymBV sym w, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymBV sym w
hi, SymBV sym w
lo)

  -- | Compute the unsigned multiply of two values with overflow bit.
  mulUnsignedOF ::
    (1 <= w) =>
    sym ->
    SymBV sym w ->
    SymBV sym w ->
    IO (Pred sym, SymBV sym w)
  mulUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y =
    do let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
       let dbl_w :: NatRepr (w + w)
dbl_w = NatRepr w -> NatRepr w -> NatRepr (w + w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
       -- 1 <= w
       one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- LeqProof 1 w -> IO (LeqProof 1 w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr 1 -> NatRepr w -> LeqProof 1 w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
       -- 1 <= w implies 1 <= w + w
       LeqProof 1 (w + w)
LeqProof <- LeqProof 1 (w + w) -> IO (LeqProof 1 (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof 1 w -> NatRepr w -> LeqProof 1 (w + w)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
       -- w <= w
       w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- LeqProof w w -> IO (LeqProof w w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> NatRepr w -> LeqProof w w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
       -- w <= w, 1 <= w implies w + 1 <= w + w
       LeqProof (w + 1) (w + w)
LeqProof <- LeqProof (w + 1) (w + w) -> IO (LeqProof (w + 1) (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof w w -> LeqProof 1 w -> LeqProof (w + 1) (w + w)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
       SymExpr sym (BaseBVType (w + w))
x'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
       SymExpr sym (BaseBVType (w + w))
y'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
       SymExpr sym (BaseBVType (w + w))
s   <- sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
       SymBV sym w
lo  <- sym
-> NatRepr w
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s

       -- overflow if the result is greater than the max representable value in w bits
       Pred sym
ov  <- sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUgt sym
sym SymExpr sym (BaseBVType (w + w))
s (SymExpr sym (BaseBVType (w + w)) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType (w + w))) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> NatRepr (w + w)
-> BV (w + w)
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (NatRepr (w + w) -> BV w -> BV (w + w)
forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr (w + w)
dbl_w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w))

       (Pred sym, SymBV sym w) -> IO (Pred sym, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
lo)

  -- | @signedWideMultiplyBV sym x y@ multiplies two signed 'w' bit numbers 'x' and 'y'.
  --
  -- It returns a pair containing the top 'w' bits as the first element, and the
  -- lower 'w' bits as the second element.
  signedWideMultiplyBV :: (1 <= w)
                       => sym
                       -> SymBV sym w
                       -> SymBV sym w
                       -> IO (SymBV sym w, SymBV sym w)
  signedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y = do
       let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
       let dbl_w :: NatRepr (w + w)
dbl_w = NatRepr w -> NatRepr w -> NatRepr (w + w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
       -- 1 <= w
       one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- LeqProof 1 w -> IO (LeqProof 1 w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr 1 -> NatRepr w -> LeqProof 1 w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
       -- 1 <= w implies 1 <= w + w
       LeqProof 1 (w + w)
LeqProof <- LeqProof 1 (w + w) -> IO (LeqProof 1 (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof 1 w -> NatRepr w -> LeqProof 1 (w + w)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
       -- w <= w
       w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- LeqProof w w -> IO (LeqProof w w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> NatRepr w -> LeqProof w w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
       -- w <= w, 1 <= w implies w + 1 <= w + w
       LeqProof (w + 1) (w + w)
LeqProof <- LeqProof (w + 1) (w + w) -> IO (LeqProof (w + 1) (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof w w -> LeqProof 1 w -> LeqProof (w + 1) (w + w)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
       SymExpr sym (BaseBVType (w + w))
x'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
       SymExpr sym (BaseBVType (w + w))
y'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
       SymExpr sym (BaseBVType (w + w))
s   <- sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
       SymBV sym w
lo  <- sym
-> NatRepr w
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s
       SymExpr sym (BaseBVType (w + w))
n   <- sym
-> NatRepr (w + w)
-> BV (w + w)
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (NatRepr (w + w) -> BV w -> BV (w + w)
forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr (w + w)
dbl_w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.width NatRepr w
w))
       SymBV sym w
hi  <- sym
-> NatRepr w
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w (SymExpr sym (BaseBVType (w + w)) -> IO (SymBV sym w))
-> IO (SymExpr sym (BaseBVType (w + w))) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvLshr sym
sym SymExpr sym (BaseBVType (w + w))
s SymExpr sym (BaseBVType (w + w))
n
       (SymBV sym w, SymBV sym w) -> IO (SymBV sym w, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymBV sym w
hi, SymBV sym w
lo)

  -- | Compute the signed multiply of two values with overflow bit.
  mulSignedOF ::
    (1 <= w) =>
    sym ->
    SymBV sym w ->
    SymBV sym w ->
    IO (Pred sym, SymBV sym w)
  mulSignedOF sym
sym SymBV sym w
x SymBV sym w
y =
    do let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
       let dbl_w :: NatRepr (w + w)
dbl_w = NatRepr w -> NatRepr w -> NatRepr (w + w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
       -- 1 <= w
       one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- LeqProof 1 w -> IO (LeqProof 1 w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr 1 -> NatRepr w -> LeqProof 1 w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
       -- 1 <= w implies 1 <= w + w
       LeqProof 1 (w + w)
LeqProof <- LeqProof 1 (w + w) -> IO (LeqProof 1 (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof 1 w -> NatRepr w -> LeqProof 1 (w + w)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
       -- w <= w
       w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- LeqProof w w -> IO (LeqProof w w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> NatRepr w -> LeqProof w w
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
       -- w <= w, 1 <= w implies w + 1 <= w + w
       LeqProof (w + 1) (w + w)
LeqProof <- LeqProof (w + 1) (w + w) -> IO (LeqProof (w + 1) (w + w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LeqProof w w -> LeqProof 1 w -> LeqProof (w + 1) (w + w)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
       SymExpr sym (BaseBVType (w + w))
x'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
       SymExpr sym (BaseBVType (w + w))
y'  <- sym
-> NatRepr (w + w)
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
       SymExpr sym (BaseBVType (w + w))
s   <- sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
       SymBV sym w
lo  <- sym
-> NatRepr w
-> SymExpr sym (BaseBVType (w + w))
-> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s

       -- overflow if greater or less than max representable values
       Pred sym
ov1 <- sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymExpr sym (BaseBVType (w + w))
s (SymExpr sym (BaseBVType (w + w)) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType (w + w))) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> NatRepr (w + w)
-> BV (w + w)
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (NatRepr w -> NatRepr (w + w) -> BV w -> BV (w + w)
forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr w
w NatRepr (w + w)
dbl_w (NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w))
       Pred sym
ov2 <- sym
-> SymExpr sym (BaseBVType (w + w))
-> SymExpr sym (BaseBVType (w + w))
-> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym
sym SymExpr sym (BaseBVType (w + w))
s (SymExpr sym (BaseBVType (w + w)) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType (w + w))) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> NatRepr (w + w)
-> BV (w + w)
-> IO (SymExpr sym (BaseBVType (w + w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (NatRepr w -> NatRepr (w + w) -> BV w -> BV (w + w)
forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr w
w NatRepr (w + w)
dbl_w (NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
w))
       Pred sym
ov  <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
ov1 Pred sym
ov2
       (Pred sym, SymBV sym w) -> IO (Pred sym, SymBV sym w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
lo)

  ----------------------------------------------------------------------
  -- Struct operations

  -- | Create a struct from an assignment of expressions.
  mkStruct :: sym
           -> Ctx.Assignment (SymExpr sym) flds
           -> IO (SymStruct sym flds)

  -- | Get the value of a specific field in a struct.
  structField :: sym
              -> SymStruct sym flds
              -> Ctx.Index flds tp
              -> IO (SymExpr sym tp)

  -- | Check if two structs are equal.
  structEq  :: forall flds
            .  sym
            -> SymStruct sym flds
            -> SymStruct sym flds
            -> IO (Pred sym)
  structEq sym
sym SymStruct sym flds
x SymStruct sym flds
y = do
    case SymStruct sym flds -> BaseTypeRepr (BaseStructType flds)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymStruct sym flds
x of
      BaseStructRepr Assignment BaseTypeRepr ctx
fld_types -> do
        let sz :: Size ctx
sz = Assignment BaseTypeRepr ctx -> Size ctx
forall k (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment BaseTypeRepr ctx
fld_types
        -- Checks to see if the ith struct fields are equal, and all previous entries
        -- are as well.
        let f :: IO (Pred sym) -> Ctx.Index flds tp -> IO (Pred sym)
            f :: IO (Pred sym) -> Index flds tp -> IO (Pred sym)
f IO (Pred sym)
mp Index flds tp
i = do
              SymExpr sym tp
xi <- sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
structField sym
sym SymStruct sym flds
x Index flds tp
i
              SymExpr sym tp
yi <- sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
structField sym
sym SymStruct sym flds
y Index flds tp
i
              Pred sym
i_eq <- sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym
sym SymExpr sym tp
xi SymExpr sym tp
yi
              case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
i_eq of
                Just Bool
True -> IO (Pred sym)
mp
                Just Bool
False -> Pred sym -> IO (Pred sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
                Maybe Bool
_ ->  sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
i_eq (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (Pred sym)
mp
        Size ctx
-> (forall (tp :: BaseType).
    IO (Pred sym) -> Index ctx tp -> IO (Pred sym))
-> IO (Pred sym)
-> IO (Pred sym)
forall k (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex Size ctx
sz forall (tp :: BaseType).
IO (Pred sym) -> Index flds tp -> IO (Pred sym)
forall (tp :: BaseType).
IO (Pred sym) -> Index ctx tp -> IO (Pred sym)
f (Pred sym -> IO (Pred sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym))

  -- | Take the if-then-else of two structures.
  structIte :: sym
            -> Pred sym
            -> SymStruct sym flds
            -> SymStruct sym flds
            -> IO (SymStruct sym flds)

  -----------------------------------------------------------------------
  -- Array operations

  -- | Create an array where each element has the same value.
  constantArray :: sym -- Interface
                -> Ctx.Assignment BaseTypeRepr (idx::>tp) -- ^ Index type
                -> SymExpr sym b -- ^ Constant
                -> IO (SymArray sym (idx::>tp) b)

  -- | Create an array from an arbitrary symbolic function.
  --
  -- Arrays created this way can typically not be compared
  -- for equality when provided to backend solvers.
  arrayFromFn :: sym
              -> SymFn sym (idx ::> itp) ret
              -> IO (SymArray sym (idx ::> itp) ret)

  -- | Create an array by mapping a function over one or more existing arrays.
  arrayMap :: sym
           -> SymFn sym (ctx::>d) r
           -> Ctx.Assignment (ArrayResultWrapper (SymExpr sym) (idx ::> itp)) (ctx::>d)
           -> IO (SymArray sym (idx ::> itp) r)

  -- | Update an array at a specific location.
  arrayUpdate :: sym
              -> SymArray sym (idx::>tp) b
              -> Ctx.Assignment (SymExpr sym) (idx::>tp)
              -> SymExpr sym b
              -> IO (SymArray sym (idx::>tp) b)

  -- | Return element in array.
  arrayLookup :: sym
              -> SymArray sym (idx::>tp) b
              -> Ctx.Assignment (SymExpr sym) (idx::>tp)
              -> IO (SymExpr sym b)

  -- | Create an array from a map of concrete indices to values.
  --
  -- This is implemented, but designed to be overridden for efficiency.
  arrayFromMap :: sym
               -> Ctx.Assignment BaseTypeRepr (idx ::> itp)
                  -- ^ Types for indices
               -> AUM.ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
                  -- ^ Value for known indices.
               -> SymExpr sym tp
                  -- ^ Value for other entries.
               -> IO (SymArray sym (idx ::> itp) tp)
  arrayFromMap sym
sym Assignment BaseTypeRepr (idx ::> itp)
idx_tps ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m SymExpr sym tp
default_value = do
    SymArray sym (idx ::> itp) tp
a0 <- sym
-> Assignment BaseTypeRepr (idx ::> itp)
-> SymExpr sym tp
-> IO (SymArray sym (idx ::> itp) tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
constantArray sym
sym Assignment BaseTypeRepr (idx ::> itp)
idx_tps SymExpr sym tp
default_value
    sym
-> ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> SymArray sym (idx ::> itp) tp
-> IO (SymArray sym (idx ::> itp) tp)
forall sym (idx :: Ctx BaseType) (itp :: BaseType)
       (tp :: BaseType).
IsExprBuilder sym =>
sym
-> ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> SymArray sym (idx ::> itp) tp
-> IO (SymArray sym (idx ::> itp) tp)
arrayUpdateAtIdxLits sym
sym ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m SymArray sym (idx ::> itp) tp
a0

  -- | Update an array at specific concrete indices.
  --
  -- This is implemented, but designed to be overriden for efficiency.
  arrayUpdateAtIdxLits :: sym
                       -> AUM.ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
                       -- ^ Value for known indices.
                       -> SymArray sym (idx ::> itp) tp
                       -- ^ Value for existing array.
                       -> IO (SymArray sym (idx ::> itp) tp)
  arrayUpdateAtIdxLits sym
sym ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m SymArray sym (idx ::> itp) tp
a0 = do
    let updateAt :: SymArray sym (idx ::> itp) tp
-> (Assignment IndexLit (idx ::> itp), SymExpr sym tp)
-> IO (SymArray sym (idx ::> itp) tp)
updateAt SymArray sym (idx ::> itp) tp
a (Assignment IndexLit (idx ::> itp)
i,SymExpr sym tp
v) = do
          Assignment (SymExpr sym) (idx ::> itp)
idx <-  (forall (x :: BaseType). IndexLit x -> IO (SymExpr sym x))
-> Assignment IndexLit (idx ::> itp)
-> IO (Assignment (SymExpr sym) (idx ::> itp))
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (sym -> IndexLit x -> IO (SymExpr sym x)
forall sym (idx :: BaseType).
IsExprBuilder sym =>
sym -> IndexLit idx -> IO (SymExpr sym idx)
indexLit sym
sym) Assignment IndexLit (idx ::> itp)
i
          sym
-> SymArray sym (idx ::> itp) tp
-> Assignment (SymExpr sym) (idx ::> itp)
-> SymExpr sym tp
-> IO (SymArray sym (idx ::> itp) tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
arrayUpdate sym
sym SymArray sym (idx ::> itp) tp
a Assignment (SymExpr sym) (idx ::> itp)
idx SymExpr sym tp
v
    (SymArray sym (idx ::> itp) tp
 -> (Assignment IndexLit (idx ::> itp), SymExpr sym tp)
 -> IO (SymArray sym (idx ::> itp) tp))
-> SymArray sym (idx ::> itp) tp
-> [(Assignment IndexLit (idx ::> itp), SymExpr sym tp)]
-> IO (SymArray sym (idx ::> itp) tp)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM SymArray sym (idx ::> itp) tp
-> (Assignment IndexLit (idx ::> itp), SymExpr sym tp)
-> IO (SymArray sym (idx ::> itp) tp)
updateAt SymArray sym (idx ::> itp) tp
a0 (ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> [(Assignment IndexLit (idx ::> itp), SymExpr sym tp)]
forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
ArrayUpdateMap e ctx tp -> [(Assignment IndexLit ctx, e tp)]
AUM.toList ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m)

  -- | If-then-else applied to arrays.
  arrayIte :: sym
           -> Pred sym
           -> SymArray sym idx b
           -> SymArray sym idx b
           -> IO (SymArray sym idx b)

  -- | Return true if two arrays are equal.
  --
  -- Note that in the backend, arrays do not have a fixed number of elements, so
  -- this equality requires that arrays are equal on all elements.
  arrayEq :: sym
          -> SymArray sym idx b
          -> SymArray sym idx b
          -> IO (Pred sym)

  -- | Return true if all entries in the array are true.
  allTrueEntries :: sym -> SymArray sym idx BaseBoolType -> IO (Pred sym)
  allTrueEntries sym
sym SymArray sym idx BaseBoolType
a = do
    case SymArray sym idx BaseBoolType
-> BaseTypeRepr (BaseArrayType idx BaseBoolType)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymArray sym idx BaseBoolType
a of
      BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx_tps BaseTypeRepr xs
_ ->
        sym
-> SymExpr sym ('BaseArrayType (idx ::> tp) BaseBoolType)
-> SymExpr sym ('BaseArrayType (idx ::> tp) BaseBoolType)
-> IO (Pred sym)
forall sym (idx :: Ctx BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym -> SymArray sym idx b -> SymArray sym idx b -> IO (Pred sym)
arrayEq sym
sym SymArray sym idx BaseBoolType
SymExpr sym ('BaseArrayType (idx ::> tp) BaseBoolType)
a (SymExpr sym ('BaseArrayType (idx ::> tp) BaseBoolType)
 -> IO (Pred sym))
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) BaseBoolType))
-> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> Pred sym
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) BaseBoolType))
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
constantArray sym
sym Assignment BaseTypeRepr (idx ::> tp)
idx_tps (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)

  -- | Return true if the array has the value true at every index satisfying the
  -- given predicate.
  arrayTrueOnEntries
    :: sym
    -> SymFn sym (idx::>itp) BaseBoolType
    -- ^ Predicate that indicates if array should be true.
    -> SymArray sym (idx ::> itp) BaseBoolType
    -> IO (Pred sym)

  ----------------------------------------------------------------------
  -- Lossless (injective) conversions

  -- | Convert an integer to a real number.
  integerToReal :: sym -> SymInteger sym -> IO (SymReal sym)

  -- | Return the unsigned value of the given bitvector as an integer.
  bvToInteger :: (1 <= w) => sym -> SymBV sym w -> IO (SymInteger sym)

  -- | Return the signed value of the given bitvector as an integer.
  sbvToInteger :: (1 <= w) => sym -> SymBV sym w -> IO (SymInteger sym)

  -- | Return @1@ if the predicate is true; @0@ otherwise.
  predToBV :: (1 <= w) => sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)

  ----------------------------------------------------------------------
  -- Lossless combinators

  -- | Convert an unsigned bitvector to a real number.
  uintToReal :: (1 <= w) => sym -> SymBV sym w -> IO (SymReal sym)
  uintToReal sym
sym = sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
bvToInteger sym
sym (SymBV sym w -> IO (SymInteger sym))
-> (SymInteger sym -> IO (SymReal sym))
-> SymBV sym w
-> IO (SymReal sym)
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> sym -> SymInteger sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym

  -- | Convert an signed bitvector to a real number.
  sbvToReal :: (1 <= w) => sym -> SymBV sym w -> IO (SymReal sym)
  sbvToReal sym
sym = sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
sbvToInteger sym
sym (SymBV sym w -> IO (SymInteger sym))
-> (SymInteger sym -> IO (SymReal sym))
-> SymBV sym w
-> IO (SymReal sym)
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> sym -> SymInteger sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym

  ----------------------------------------------------------------------
  -- Lossy (non-injective) conversions

  -- | Round a real number to an integer.
  --
  -- Numbers are rounded to the nearest integer, with rounding away from
  -- zero when two integers are equidistant (e.g., 1.5 rounds to 2).
  realRound :: sym -> SymReal sym -> IO (SymInteger sym)

  -- | Round a real number to an integer.
  --
  -- Numbers are rounded to the nearest integer, with rounding toward
  -- even values when two integers are equidistant (e.g., 2.5 rounds to 2).
  realRoundEven :: sym -> SymReal sym -> IO (SymInteger sym)

  -- | Round down to the nearest integer that is at most this value.
  realFloor :: sym -> SymReal sym -> IO (SymInteger sym)

  -- | Round up to the nearest integer that is at least this value.
  realCeil :: sym -> SymReal sym -> IO (SymInteger sym)

  -- | Round toward zero.  This is @floor(x)@ when x is positive
  --   and @celing(x)@ when @x@ is negative.
  realTrunc :: sym -> SymReal sym -> IO (SymInteger sym)
  realTrunc sym
sym SymReal sym
x =
    do Pred sym
pneg <- sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt sym
sym SymReal sym
x (SymReal sym -> IO (Pred sym)) -> IO (SymReal sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Rational -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
0
       (sym
 -> Pred sym
 -> SymInteger sym
 -> SymInteger sym
 -> IO (SymInteger sym))
-> sym
-> Pred sym
-> IO (SymInteger sym)
-> IO (SymInteger sym)
-> IO (SymInteger sym)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
pneg (sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realCeil sym
sym SymReal sym
x) (sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realFloor sym
sym SymReal sym
x)

  -- | Convert an integer to a bitvector.  The result is the unique bitvector
  --   whose value (signed or unsigned) is congruent to the input integer, modulo @2^w@.
  --
  --   This operation has the following properties:
  --
  --   *  @bvToInteger (integerToBv x w) == mod x (2^w)@
  --   *  @bvToInteger (integerToBV x w) == x@     when @0 <= x < 2^w@.
  --   *  @sbvToInteger (integerToBV x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1)@
  --   *  @sbvToInteger (integerToBV x w) == x@    when @-2^(w-1) <= x < 2^(w-1)@
  --   *  @integerToBV (bvToInteger y) w == y@     when @y@ is a @SymBV sym w@
  --   *  @integerToBV (sbvToInteger y) w == y@    when @y@ is a @SymBV sym w@
  integerToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)

  ----------------------------------------------------------------------
  -- Lossy (non-injective) combinators

  -- | Convert a real number to an integer.
  --
  -- The result is undefined if the given real number does not represent an integer.
  realToInteger :: sym -> SymReal sym -> IO (SymInteger sym)

  -- | Convert a real number to an unsigned bitvector.
  --
  -- Numbers are rounded to the nearest representable number, with rounding away from
  -- zero when two integers are equidistant (e.g., 1.5 rounds to 2).
  -- When the real is negative the result is zero.
  realToBV :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
  realToBV sym
sym SymReal sym
r NatRepr w
w = do
    SymInteger sym
i <- sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realRound sym
sym SymReal sym
r
    sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToBV sym
sym SymInteger sym
i NatRepr w
w

  -- | Convert a real number to a signed bitvector.
  --
  -- Numbers are rounded to the nearest representable number, with rounding away from
  -- zero when two integers are equidistant (e.g., 1.5 rounds to 2).
  realToSBV  :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
  realToSBV sym
sym SymReal sym
r NatRepr w
w  = do
    SymInteger sym
i <- sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realRound sym
sym SymReal sym
r
    sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToSBV sym
sym SymInteger sym
i NatRepr w
w

  -- | Convert an integer to the nearest signed bitvector.
  --
  -- Numbers are rounded to the nearest representable number.
  clampedIntToSBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
  clampedIntToSBV sym
sym SymInteger sym
i NatRepr w
w
    | Just Integer
v <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger SymInteger sym
i = do
      sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (BV w -> IO (SymBV sym w)) -> BV w -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> BV w
BV.signedClamp NatRepr w
w Integer
v
    | Bool
otherwise = do
      -- Handle case where i < minSigned w
      let min_val :: Integer
min_val = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w
          min_val_bv :: BV w
min_val_bv = NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w
      SymInteger sym
min_sym <- sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
min_val
      Pred sym
is_lt <- sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
i SymInteger sym
min_sym
      (sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym
-> Pred sym
-> IO (SymBV sym w)
-> IO (SymBV sym w)
-> IO (SymBV sym w)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_lt (sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
min_val_bv) (IO (SymBV sym w) -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ do
        -- Handle case where i > maxSigned w
        let max_val :: Integer
max_val = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w
            max_val_bv :: BV w
max_val_bv = NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
w
        SymInteger sym
max_sym <- sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
max_val
        Pred sym
is_gt <- sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
max_sym SymInteger sym
i
        (sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym
-> Pred sym
-> IO (SymBV sym w)
-> IO (SymBV sym w)
-> IO (SymBV sym w)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_gt (sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
max_val_bv) (IO (SymBV sym w) -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ do
          -- Do unclamped conversion.
          sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
integerToBV sym
sym SymInteger sym
i NatRepr w
w

  -- | Convert an integer to the nearest unsigned bitvector.
  --
  -- Numbers are rounded to the nearest representable number.
  clampedIntToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
  clampedIntToBV sym
sym SymInteger sym
i NatRepr w
w
    | Just Integer
v <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger SymInteger sym
i = do
      sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (BV w -> IO (SymBV sym w)) -> BV w -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.unsignedClamp NatRepr w
w Integer
v
    | Bool
otherwise = do
      -- Handle case where i < 0
      SymInteger sym
min_sym <- sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0
      Pred sym
is_lt <- sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
i SymInteger sym
min_sym
      (sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym
-> Pred sym
-> IO (SymBV sym w)
-> IO (SymBV sym w)
-> IO (SymBV sym w)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_lt (sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)) (IO (SymBV sym w) -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ do
        -- Handle case where i > maxUnsigned w
        let max_val :: Integer
max_val = NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr w
w
            max_val_bv :: BV w
max_val_bv = NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w
        SymInteger sym
max_sym <- sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
max_val
        Pred sym
is_gt <- sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
max_sym SymInteger sym
i
        (sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym
-> Pred sym
-> IO (SymBV sym w)
-> IO (SymBV sym w)
-> IO (SymBV sym w)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_gt (sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
max_val_bv) (IO (SymBV sym w) -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$
          -- Do unclamped conversion.
          sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
integerToBV sym
sym SymInteger sym
i NatRepr w
w

  ----------------------------------------------------------------------
  -- Bitvector operations.

  -- | Convert a signed bitvector to the nearest signed bitvector with
  -- the given width. If the resulting width is smaller, this clamps
  -- the value to min-int or max-int when necessary.
  intSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  intSetWidth sym
sym SymBV sym m
e NatRepr n
n = do
    let m :: NatRepr m
m = SymBV sym m -> NatRepr m
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym m
e
    case NatRepr n
n NatRepr n -> NatRepr m -> NatCases n m
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
`testNatCases` NatRepr m
m of
      -- Truncate when the width of e is larger than w.
      NatCaseLT LeqProof (n + 1) m
LeqProof -> do
        -- Check if e underflows
        Pred sym
does_underflow <- sym -> SymBV sym m -> SymBV sym m -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym m
e (SymBV sym m -> IO (Pred sym)) -> IO (SymBV sym m) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr m -> BV m -> IO (SymBV sym m)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (NatRepr n -> NatRepr m -> BV n -> BV m
forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr n
n NatRepr m
m (NatRepr n -> BV n
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr n
n))
        (sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n))
-> sym
-> Pred sym
-> IO (SymBV sym n)
-> IO (SymBV sym n)
-> IO (SymBV sym n)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
does_underflow (sym -> NatRepr n -> BV n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
n (NatRepr n -> BV n
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr n
n)) (IO (SymBV sym n) -> IO (SymBV sym n))
-> IO (SymBV sym n) -> IO (SymBV sym n)
forall a b. (a -> b) -> a -> b
$ do
          -- Check if e overflows target signed representation.
          Pred sym
does_overflow <- sym -> SymBV sym m -> SymBV sym m -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym
sym SymBV sym m
e (SymBV sym m -> IO (Pred sym)) -> IO (SymBV sym m) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr m -> BV m -> IO (SymBV sym m)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (NatRepr m -> Integer -> BV m
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr m
m (NatRepr n -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr n
n))
          (sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n))
-> sym
-> Pred sym
-> IO (SymBV sym n)
-> IO (SymBV sym n)
-> IO (SymBV sym n)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
does_overflow (sym -> NatRepr n -> BV n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
n (NatRepr n -> BV n
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr n
n)) (IO (SymBV sym n) -> IO (SymBV sym n))
-> IO (SymBV sym n) -> IO (SymBV sym n)
forall a b. (a -> b) -> a -> b
$ do
            -- Just do truncation.
            sym -> NatRepr n -> SymBV sym m -> IO (SymBV sym n)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr n
n SymBV sym m
e
      NatCases n m
NatCaseEQ -> SymBV sym n -> IO (SymBV sym n)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym m
SymBV sym n
e
      NatCaseGT LeqProof (m + 1) n
LeqProof -> sym -> NatRepr n -> SymBV sym m -> IO (SymBV sym n)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr n
n SymBV sym m
e

  -- | Convert an unsigned bitvector to the nearest unsigned bitvector with
  -- the given width (clamp on overflow).
  uintSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  uintSetWidth sym
sym SymBV sym m
e NatRepr n
n = do
    let m :: NatRepr m
m = SymBV sym m -> NatRepr m
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym m
e
    case NatRepr n
n NatRepr n -> NatRepr m -> NatCases n m
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
`testNatCases` NatRepr m
m of
      NatCaseLT LeqProof (n + 1) m
LeqProof -> do
        Pred sym
does_overflow <- sym -> SymBV sym m -> SymBV sym m -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUgt sym
sym SymBV sym m
e (SymBV sym m -> IO (Pred sym)) -> IO (SymBV sym m) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr m -> BV m -> IO (SymBV sym m)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (NatRepr m -> Integer -> BV m
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr m
m (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n))
        (sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n))
-> sym
-> Pred sym
-> IO (SymBV sym n)
-> IO (SymBV sym n)
-> IO (SymBV sym n)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
does_overflow (sym -> NatRepr n -> BV n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
n (NatRepr n -> BV n
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr n
n)) (IO (SymBV sym n) -> IO (SymBV sym n))
-> IO (SymBV sym n) -> IO (SymBV sym n)
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr n -> SymBV sym m -> IO (SymBV sym n)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr n
n SymBV sym m
e
      NatCases n m
NatCaseEQ -> SymBV sym n -> IO (SymBV sym n)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym m
SymBV sym n
e
      NatCaseGT LeqProof (m + 1) n
LeqProof -> sym -> NatRepr n -> SymBV sym m -> IO (SymBV sym n)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr n
n SymBV sym m
e

  -- | Convert an signed bitvector to the nearest unsigned bitvector with
  -- the given width (clamp on overflow).
  intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  intToUInt sym
sym SymBV sym m
e NatRepr n
w = do
    Pred sym
p <- sym -> SymBV sym m -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym m
e
    (sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n))
-> sym
-> Pred sym
-> IO (SymBV sym n)
-> IO (SymBV sym n)
-> IO (SymBV sym n)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p (sym -> NatRepr n -> BV n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
w (NatRepr n -> BV n
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr n
w)) (sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
forall sym (m :: Nat) (n :: Nat).
(IsExprBuilder sym, 1 <= m, 1 <= n) =>
sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintSetWidth sym
sym SymBV sym m
e NatRepr n
w)

  -- | Convert an unsigned bitvector to the nearest signed bitvector with
  -- the given width (clamp on overflow).
  uintToInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  uintToInt sym
sym SymBV sym m
e NatRepr n
n = do
    let m :: NatRepr m
m = SymBV sym m -> NatRepr m
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym m
e
    case NatRepr n
n NatRepr n -> NatRepr m -> NatCases n m
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
`testNatCases` NatRepr m
m of
      NatCaseLT LeqProof (n + 1) m
LeqProof -> do
        -- Get maximum signed n-bit number.
        SymBV sym m
max_val <- sym -> NatRepr m -> BV m -> IO (SymBV sym m)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (NatRepr n -> NatRepr m -> BV n -> BV m
forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr n
n NatRepr m
m (NatRepr n -> BV n
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr n
n))
        -- Check if expression is less than maximum.
        Pred sym
p <- sym -> SymBV sym m -> SymBV sym m -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym m
e SymBV sym m
max_val
        -- Select appropriate number then truncate.
        sym -> NatRepr n -> SymBV sym m -> IO (SymBV sym n)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr n
n (SymBV sym m -> IO (SymBV sym n))
-> IO (SymBV sym m) -> IO (SymBV sym n)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> SymBV sym m -> SymBV sym m -> IO (SymBV sym m)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p SymBV sym m
e SymBV sym m
max_val
      NatCases n m
NatCaseEQ -> do
        SymBV sym n
max_val <- sym -> NatRepr n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr n
n
        Pred sym
p <- sym -> SymBV sym n -> SymBV sym n -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym m
SymBV sym n
e SymBV sym n
max_val
        sym -> Pred sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p SymBV sym m
SymBV sym n
e SymBV sym n
max_val
      NatCaseGT LeqProof (m + 1) n
LeqProof -> do
        sym -> NatRepr n -> SymBV sym m -> IO (SymBV sym n)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr n
n SymBV sym m
e

  ----------------------------------------------------------------------
  -- String operations

  -- | Create an empty string literal
  stringEmpty :: sym -> StringInfoRepr si -> IO (SymString sym si)

  -- | Create a concrete string literal
  stringLit :: sym -> StringLiteral si -> IO (SymString sym si)

  -- | Check the equality of two strings
  stringEq :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

  -- | If-then-else on strings
  stringIte :: sym -> Pred sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)

  -- | Concatenate two strings
  stringConcat :: sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)

  -- | Test if the first string contains the second string as a substring
  stringContains :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

  -- | Test if the first string is a prefix of the second string
  stringIsPrefixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

  -- | Test if the first string is a suffix of the second string
  stringIsSuffixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

  -- | Return the first position at which the second string can be found as a substring
  --   in the first string, starting from the given index.
  --   If no such position exists, return a negative value.
  stringIndexOf :: sym -> SymString sym si -> SymString sym si -> SymInteger sym -> IO (SymInteger sym)

  -- | Compute the length of a string
  stringLength :: sym -> SymString sym si -> IO (SymInteger sym)

  -- | @stringSubstring s off len@ extracts the substring of @s@ starting at index @off@ and
  --   having length @len@.  The result of this operation is undefined if @off@ and @len@
  --   do not specify a valid substring of @s@; in particular, we must have
  --   0 <= off@, @0 <= len@ and @off+len <= length(s)@.
  stringSubstring :: sym -> SymString sym si -> SymInteger sym -> SymInteger sym -> IO (SymString sym si)

  ----------------------------------------------------------------------
  -- Real operations

  -- | Return real number 0.
  realZero :: sym -> SymReal sym

  -- | Create a constant real literal.
  realLit :: sym -> Rational -> IO (SymReal sym)

  -- | Make a real literal from a scientific value. May be overridden
  -- if we want to avoid the overhead of converting scientific value
  -- to rational.
  sciLit :: sym -> Scientific -> IO (SymReal sym)
  sciLit sym
sym Scientific
s = sym -> Rational -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym (Scientific -> Rational
forall a. Real a => a -> Rational
toRational Scientific
s)

  -- | Check equality of two real numbers.
  realEq :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

  -- | Check non-equality of two real numbers.
  realNe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  realNe sym
sym SymReal sym
x SymReal sym
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymReal sym
x SymReal sym
y

  -- | Check @<=@ on two real numbers.
  realLe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

  -- | Check @<@ on two real numbers.
  realLt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  realLt sym
sym SymReal sym
x SymReal sym
y = sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
y SymReal sym
x

  -- | Check @>=@ on two real numbers.
  realGe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  realGe sym
sym SymReal sym
x SymReal sym
y = sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
y SymReal sym
x

  -- | Check @>@ on two real numbers.
  realGt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  realGt sym
sym SymReal sym
x SymReal sym
y = sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt sym
sym SymReal sym
y SymReal sym
x

  -- | If-then-else on real numbers.
  realIte :: sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

  -- | Return the minimum of two real numbers.
  realMin :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  realMin sym
sym SymReal sym
x SymReal sym
y =
    do Pred sym
p <- sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
x SymReal sym
y
       sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
p SymReal sym
x SymReal sym
y

  -- | Return the maxmimum of two real numbers.
  realMax :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  realMax sym
sym SymReal sym
x SymReal sym
y =
    do Pred sym
p <- sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
x SymReal sym
y
       sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
p SymReal sym
y SymReal sym
x

  -- | Negate a real number.
  realNeg :: sym -> SymReal sym -> IO (SymReal sym)

  -- | Add two real numbers.
  realAdd :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

  -- | Multiply two real numbers.
  realMul :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

  -- | Subtract one real from another.
  realSub :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  realSub sym
sym SymReal sym
x SymReal sym
y = sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
x (SymReal sym -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
y

  -- | @realSq sym x@ returns @x * x@.
  realSq :: sym -> SymReal sym -> IO (SymReal sym)
  realSq sym
sym SymReal sym
x = sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
x SymReal sym
x

  -- | @realDiv sym x y@ returns term equivalent to @x/y@.
  --
  -- The result is undefined when @y@ is zero.
  realDiv :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

  -- | @realMod x y@ returns the value of @x - y * floor(x / y)@ when
  -- @y@ is not zero and @x@ when @y@ is zero.
  realMod :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  realMod sym
sym SymReal sym
x SymReal sym
y = do
    Pred sym
isZero <- sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymReal sym
y (sym -> SymReal sym
forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
    (sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym))
-> sym
-> Pred sym
-> IO (SymReal sym)
-> IO (SymReal sym)
-> IO (SymReal sym)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
isZero (SymReal sym -> IO (SymReal sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymReal sym
x) (IO (SymReal sym) -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall a b. (a -> b) -> a -> b
$ do
      sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
x (SymReal sym -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
y
                    (SymReal sym -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymInteger sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym
                    (SymInteger sym -> IO (SymReal sym))
-> IO (SymInteger sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realFloor sym
sym
                    (SymReal sym -> IO (SymInteger sym))
-> IO (SymReal sym) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
x SymReal sym
y

  -- | Predicate that holds if the real number is an exact integer.
  isInteger :: sym -> SymReal sym -> IO (Pred sym)

  -- | Return true if the real is non-negative.
  realIsNonNeg :: sym -> SymReal sym -> IO (Pred sym)
  realIsNonNeg sym
sym SymReal sym
x = sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym (sym -> SymReal sym
forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym) SymReal sym
x

  -- | @realSqrt sym x@ returns sqrt(x).  Result is undefined
  -- if @x@ is negative.
  realSqrt :: sym -> SymReal sym -> IO (SymReal sym)

  -- | @realAtan2 sym y x@ returns the arctangent of @y/x@ with a range
  -- of @-pi@ to @pi@; this corresponds to the angle between the positive
  -- x-axis and the line from the origin @(x,y)@.
  --
  -- When @x@ is @0@ this returns @pi/2 * sgn y@.
  --
  -- When @x@ and @y@ are both zero, this function is undefined.
  realAtan2 :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

  -- | Return value denoting pi.
  realPi :: sym -> IO (SymReal sym)

  -- | Natural logarithm.  @realLog x@ is undefined
  --   for @x <= 0@.
  realLog :: sym -> SymReal sym -> IO (SymReal sym)

  -- | Natural exponentiation
  realExp :: sym -> SymReal sym -> IO (SymReal sym)

  -- | Sine trig function
  realSin :: sym -> SymReal sym -> IO (SymReal sym)

  -- | Cosine trig function
  realCos :: sym -> SymReal sym -> IO (SymReal sym)

  -- | Tangent trig function.  @realTan x@ is undefined
  --   when @cos x = 0@,  i.e., when @x = pi/2 + k*pi@ for
  --   some integer @k@.
  realTan :: sym -> SymReal sym -> IO (SymReal sym)
  realTan sym
sym SymReal sym
x = do
    SymReal sym
sin_x <- sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym SymReal sym
x
    SymReal sym
cos_x <- sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym SymReal sym
x
    sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
sin_x SymReal sym
cos_x

  -- | Hyperbolic sine
  realSinh :: sym -> SymReal sym -> IO (SymReal sym)

  -- | Hyperbolic cosine
  realCosh :: sym -> SymReal sym -> IO (SymReal sym)

  -- | Hyperbolic tangent
  realTanh :: sym -> SymReal sym -> IO (SymReal sym)
  realTanh sym
sym SymReal sym
x = do
    SymReal sym
sinh_x <- sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSinh sym
sym SymReal sym
x
    SymReal sym
cosh_x <- sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCosh sym
sym SymReal sym
x
    sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
sinh_x SymReal sym
cosh_x

  -- | Return absolute value of the real number.
  realAbs :: sym -> SymReal sym -> IO (SymReal sym)
  realAbs sym
sym SymReal sym
x = do
    Pred sym
c <- sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realGe sym
sym SymReal sym
x (sym -> SymReal sym
forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
    sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
c SymReal sym
x (SymReal sym -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
x

  -- | @realHypot x y@ returns sqrt(x^2 + y^2).
  realHypot :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  realHypot sym
sym SymReal sym
x SymReal sym
y = do
    case (SymReal sym -> Maybe Rational
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational SymReal sym
x, SymReal sym -> Maybe Rational
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational SymReal sym
y) of
      (Just Rational
0, Maybe Rational
_) -> sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realAbs sym
sym SymReal sym
y
      (Maybe Rational
_, Just Rational
0) -> sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realAbs sym
sym SymReal sym
x
      (Maybe Rational, Maybe Rational)
_ -> do
        SymReal sym
x2 <- sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
x
        SymReal sym
y2 <- sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
y
        sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSqrt sym
sym (SymReal sym -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
x2 SymReal sym
y2

  ----------------------------------------------------------------------
  -- IEEE-754 floating-point operations
  -- | Return floating point number @+0@.
  floatPZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

  -- | Return floating point number @-0@.
  floatNZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

  -- |  Return floating point NaN.
  floatNaN :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

  -- | Return floating point @+infinity@.
  floatPInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

  -- | Return floating point @-infinity@.
  floatNInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

  -- | Create a floating point literal from a rational literal.
  --   The rational value will be rounded if necessary using the
  --   "round to nearest even" rounding mode.
  floatLitRational
    :: sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
  floatLitRational sym
sym FloatPrecisionRepr fpp
fpp Rational
x = sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
realToFloat sym
sym FloatPrecisionRepr fpp
fpp RoundingMode
RNE (SymReal sym -> IO (SymFloat sym fpp))
-> IO (SymReal sym) -> IO (SymFloat sym fpp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Rational -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
x

  -- | Create a floating point literal from a @BigFloat@ value.
  floatLit :: sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)

  -- | Negate a floating point number.
  floatNeg
    :: sym
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Return the absolute value of a floating point number.
  floatAbs
    :: sym
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Compute the square root of a floating point number.
  floatSqrt
    :: sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Add two floating point numbers.
  floatAdd
    :: sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Subtract two floating point numbers.
  floatSub
    :: sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Multiply two floating point numbers.
  floatMul
    :: sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Divide two floating point numbers.
  floatDiv
    :: sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Compute the reminder: @x - y * n@, where @n@ in Z is nearest to @x / y@
  --   (breaking ties to even values of @n@).
  floatRem
    :: sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Return the minimum of two floating point numbers.
  --   If one argument is NaN, return the other argument.
  --   If the arguments are equal when compared as floating-point values,
  --   one of the two will be returned, but it is unspecified which;
  --   this underspecification can (only) be observed with zeros of different signs.
  floatMin
    :: sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Return the maximum of two floating point numbers.
  --   If one argument is NaN, return the other argument.
  --   If the arguments are equal when compared as floating-point values,
  --   one of the two will be returned, but it is unspecified which;
  --   this underspecification can (only) be observed with zeros of different signs.
  floatMax
    :: sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Compute the fused multiplication and addition: @(x * y) + z@.
  floatFMA
    :: sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)

  -- | Check logical equality of two floating point numbers.
  --
  --   NOTE! This does NOT accurately represent the equality test on floating point
  --   values typically found in programming languages.  See 'floatFpEq' instead.
  floatEq
    :: sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (Pred sym)

  -- | Check logical non-equality of two floating point numbers.
  --
  --   NOTE! This does NOT accurately represent the non-equality test on floating point
  --   values typically found in programming languages.  See 'floatFpEq' instead.
  floatNe
    :: sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (Pred sym)

  -- | Check IEEE-754 equality of two floating point numbers.
  --
  --   NOTE! This test returns false if either value is @NaN@; in particular
  --   @NaN@ is not equal to itself!  Moreover, positive and negative 0 will
  --   compare equal, despite having different bit patterns.
  --
  --   This test is most appropriate for interpreting the equality tests of
  --   typical languages using floating point.  Moreover, not-equal tests
  --   are usually the negation of this test, rather than the `floatFpNe`
  --   test below.
  floatFpEq
    :: sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (Pred sym)

  -- | Check IEEE-754 apartness of two floating point numbers.
  --
  --   NOTE! This test returns false if either value is @NaN@; in particular
  --   @NaN@ is not apart from any other value!  Moreover, positive and
  --   negative 0 will not compare apart, despite having different
  --   bit patterns.  Note that @x@ is apart from @y@ iff @x < y@ or @x > y@.
  --
  --   This test usually does NOT correspond to the not-equal tests found
  --   in programming languages.  Instead, one generally takes the logical
  --   negation of the `floatFpEq` test.
  floatFpApart
    :: sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (Pred sym)
  floatFpApart sym
sym SymFloat sym fpp
x SymFloat sym fpp
y =
    do Pred sym
l <- sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatLt sym
sym SymFloat sym fpp
x SymFloat sym fpp
y