    {-|
    Module      : What4.Expr.UnaryBV
    Description : A "unary" bitvector representation
    Copyright   : (c) Galois, Inc 2015-2020
    License     : BSD3
    Maintainer  : Joe Hendrix <jhendrix@galois.com>

    This module defines a data structure for representing a symbolic bitvector
    using a form of "unary" representation.

    The idea behind this representation is that we associate a predicate to
    each possible value of the bitvector that is true if the symbolic value
    is less than or equal to the possible value.

    As an example, if we had the unary term 'x' equal to
    "{ 0 -> false, 1 -> p, 2 -> q, 3 -> t }", then 'x' cannot be '0', has the
    value '1' if 'p' is true, the value '2' if 'q & not p' is true, and '3' if
    'not q' is true.  By construction, we should have that 'p => q'.
    -}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DoAndIfThenElse #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeOperators #-}
    #if MIN_VERSION_base(4,9,0)
    {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
    #endif
    module What4.Expr.UnaryBV
      ( UnaryBV
      , width
      , size
      , traversePreds
      , constant
      , asConstant
      , unsignedEntries
      , unsignedRanges
      , evaluate
      , sym_evaluate
      , instantiate
      , domain
        -- * Operations
      , add
      , neg
      , mux
      , eq
      , slt
      , ult
      , uext
      , sext
      , trunc
      ) where

    import           Control.Exception (assert)
    import           Control.Lens
    import           Control.Monad
    import           Data.Bits
    import           Data.Hashable
    import           Data.Parameterized.Classes
    import           Data.Parameterized.NatRepr
    import qualified GHC.TypeNats as Type

    import           What4.BaseTypes
    import           What4.Interface
    import           What4.Utils.BVDomain (BVDomain)
    import qualified What4.Utils.BVDomain as BVD

    import qualified Data.Map.Strict as Map

    type IntMap = Map.Map Integer

    -- | @splitLeq k m@ returns a pair @(l,h)@ where @l@ contains
    -- all the bindings with a key less than or equal to @k@, and
    -- @h@ contains the ones greater than @k@.
    splitLeq :: Integer -> IntMap a -> (IntMap a, IntMap a)
    splitLeq :: forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
    splitLeq Integer
    k IntMap a
    m =
      case Integer -> IntMap a -> (IntMap a, Maybe a, IntMap a)
    forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
    Map.splitLookup Integer
    k IntMap a
    m of
        (IntMap a
    l, Maybe a
    Nothing, IntMap a
    h) -> (IntMap a
    l,IntMap a
    h)
        (IntMap a
    l, Just a
    v, IntMap a
    h) -> (Integer -> a -> IntMap a -> IntMap a
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Integer
    k a
    v IntMap a
    l, IntMap a
    h)

    -- | Split a map into a lower bound, midpoint, and upperbound if non-empty.
    splitEntry :: IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
    splitEntry :: forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
    splitEntry IntMap a
    m0 = [IntMap a] -> Maybe (IntMap a, (Integer, a), IntMap a)
    forall {k} {a}.
    Ord k =>
    [Map k a] -> Maybe (Map k a, (k, a), Map k a)
    go (IntMap a -> [IntMap a]
    forall k b. Map k b -> [Map k b]
    Map.splitRoot IntMap a
    m0)
      where go :: [Map k a] -> Maybe (Map k a, (k, a), Map k a)
    go [] = Maybe (Map k a, (k, a), Map k a)
    forall a. Maybe a
    Nothing
            go [Map k a
    m] =
              case Map k a -> Maybe ((k, a), Map k a)
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.minViewWithKey Map k a
    m of
                Maybe ((k, a), Map k a)
    Nothing -> Maybe (Map k a, (k, a), Map k a)
    forall a. Maybe a
    Nothing
                Just ((k, a)
    p, Map k a
    h) -> (Map k a, (k, a), Map k a) -> Maybe (Map k a, (k, a), Map k a)
    forall a. a -> Maybe a
    Just (Map k a
    forall k a. Map k a
    Map.empty, (k, a)
    p, Map k a
    h)
            go (Map k a
    l:Map k a
    m:[Map k a]
    h) =
              case Map k a -> Maybe ((k, a), Map k a)
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.minViewWithKey Map k a
    m of
                Maybe ((k, a), Map k a)
    Nothing -> [Map k a] -> Maybe (Map k a, (k, a), Map k a)
    go (Map k a
    lMap k a -> [Map k a] -> [Map k a]
    forall a. a -> [a] -> [a]
    :[Map k a]
    h)
                Just ((k, a)
    p, Map k a
    m') | Map k a -> Bool
    forall k a. Map k a -> Bool
    Map.null Map k a
    m' -> (Map k a, (k, a), Map k a) -> Maybe (Map k a, (k, a), Map k a)
    forall a. a -> Maybe a
    Just (Map k a
    l, (k, a)
    p, [Map k a] -> Map k a
    forall (f :: Type -> Type) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions [Map k a]
    h)
                             | Bool
    otherwise   -> (Map k a, (k, a), Map k a) -> Maybe (Map k a, (k, a), Map k a)
    forall a. a -> Maybe a
    Just (Map k a
    l, (k, a)
    p, [Map k a] -> Map k a
    forall (f :: Type -> Type) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions (Map k a
    m'Map k a -> [Map k a] -> [Map k a]
    forall a. a -> [a] -> [a]
    :[Map k a]
    h))

    -- | This function eliminates entries where the predicate has the same
    -- value.
    stripDuplicatePreds :: Eq p => [(Integer,p)] -> [(Integer,p)]
    stripDuplicatePreds :: forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
    stripDuplicatePreds ((Integer
    l,p
    p):(Integer
    h,p
    q):[(Integer, p)]
    r)
      | p
    p p -> p -> Bool
    forall a. Eq a => a -> a -> Bool
    == p
    q = [(Integer, p)] -> [(Integer, p)]
    forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
    stripDuplicatePreds ((Integer
    l,p
    p)(Integer, p) -> [(Integer, p)] -> [(Integer, p)]
    forall a. a -> [a] -> [a]
    :[(Integer, p)]
    r)
      | Bool
    otherwise = (Integer
    l,p
    p)(Integer, p) -> [(Integer, p)] -> [(Integer, p)]
    forall a. a -> [a] -> [a]
    :[(Integer, p)] -> [(Integer, p)]
    forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
    stripDuplicatePreds ((Integer
    h,p
    q)(Integer, p) -> [(Integer, p)] -> [(Integer, p)]
    forall a. a -> [a] -> [a]
    :[(Integer, p)]
    r)
    stripDuplicatePreds [(Integer, p)
    p] = [(Integer, p)
    p]
    stripDuplicatePreds [] = []

    ------------------------------------------------------------------------
    -- UnaryBV

    -- | A unary bitvector encoding where the map contains predicates
    -- such as @u^.unaryBVMap^.at i@ holds iff the value represented by @u@
    -- is less than or equal to @i@.
    --
    -- The map stored in the representation should always have a single element,
    -- and the largest integer stored in the map should be associated with a
    -- predicate representing "true".  This means that if the map contains only
    -- a single binding, then it represents a constant.
    data UnaryBV p (n::Type.Nat)
       = UnaryBV { forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width :: !(NatRepr n)
                 , forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap :: !(IntMap p)
                 }

    -- | Returns the number of distinct values that this could be.
    size :: UnaryBV p n -> Int
    size :: forall p (n :: Nat). UnaryBV p n -> Int
    size UnaryBV p n
    x = Map Integer p -> Int
    forall k a. Map k a -> Int
    Map.size (UnaryBV p n -> Map Integer p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    x)

    traversePreds :: Traversal (UnaryBV p n) (UnaryBV q n) p q
    traversePreds :: forall p (n :: Nat) q (f :: Type -> Type).
    Applicative f =>
    (p -> f q) -> UnaryBV p n -> f (UnaryBV q n)
    traversePreds p -> f q
    f (UnaryBV NatRepr n
    w IntMap p
    m) = NatRepr n -> IntMap q -> UnaryBV q n
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV NatRepr n
    w (IntMap q -> UnaryBV q n) -> f (IntMap q) -> f (UnaryBV q n)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (p -> f q) -> IntMap p -> f (IntMap q)
    forall (t :: Type -> Type) (f :: Type -> Type) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Map Integer a -> f (Map Integer b)
    traverse p -> f q
    f IntMap p
    m

    instance Eq p => TestEquality (UnaryBV p) where
      testEquality :: forall (a :: Nat) (b :: Nat).
    UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b)
    testEquality UnaryBV p a
    x UnaryBV p b
    y = do
        a :~: b
    Refl <- NatRepr a -> NatRepr b -> Maybe (a :~: b)
    forall (a :: Nat) (b :: Nat).
    NatRepr a -> NatRepr b -> Maybe (a :~: b)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality (UnaryBV p a -> NatRepr a
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p a
    x) (UnaryBV p b -> NatRepr b
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p b
    y)
        if UnaryBV p a -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p a
    x IntMap p -> IntMap p -> Bool
    forall a. Eq a => a -> a -> Bool
    == UnaryBV p b -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p b
    y then
          (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
        else
          Maybe (a :~: b)
    forall a. Maybe a
    Nothing
    instance Eq p => Eq (UnaryBV p n) where
      UnaryBV p n
    x == :: UnaryBV p n -> UnaryBV p n -> Bool
    == UnaryBV p n
    y = Maybe (n :~: n) -> Bool
    forall a. Maybe a -> Bool
    isJust (UnaryBV p n -> UnaryBV p n -> Maybe (n :~: n)
    forall (a :: Nat) (b :: Nat).
    UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality UnaryBV p n
    x UnaryBV p n
    y)

    instance Hashable p => Hashable (UnaryBV p n) where
      hashWithSalt :: Int -> UnaryBV p n -> Int
    hashWithSalt Int
    s0 UnaryBV p n
    u = (Int -> Integer -> p -> Int) -> Int -> Map Integer p -> Int
    forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
    Map.foldlWithKey' Int -> Integer -> p -> Int
    forall {a} {a}. (Hashable a, Hashable a) => Int -> a -> a -> Int
    go Int
    s0 (UnaryBV p n -> Map Integer p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    u)
        where go :: Int -> a -> a -> Int
    go Int
    s a
    k a
    e = Int -> a -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt (Int -> a -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    s a
    k) a
    e

    -- | Create a unary bitvector term from a constant.
    constant :: IsExprBuilder sym
              => sym
              -> NatRepr n
              -> Integer
              -> UnaryBV (Pred sym) n
    constant :: forall sym (n :: Nat).
    IsExprBuilder sym =>
    sym -> NatRepr n -> Integer -> UnaryBV (Pred sym) n
    constant sym
    sym NatRepr n
    w Integer
    v = NatRepr n
    -> IntMap (SymExpr sym BaseBoolType)
    -> UnaryBV (SymExpr sym BaseBoolType) n
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV NatRepr n
    w (Integer
    -> SymExpr sym BaseBoolType -> IntMap (SymExpr sym BaseBoolType)
    forall k a. k -> a -> Map k a
    Map.singleton Integer
    v' (sym -> SymExpr sym BaseBoolType
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym))
      where v' :: Integer
    v' = NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    w Integer
    v

    -- | Create a unary bitvector term from a constant.
    asConstant :: IsExpr p => UnaryBV (p BaseBoolType) w -> Maybe Integer
    asConstant :: forall (p :: BaseType -> Type) (w :: Nat).
    IsExpr p =>
    UnaryBV (p BaseBoolType) w -> Maybe Integer
    asConstant UnaryBV (p BaseBoolType) w
    x
      | UnaryBV (p BaseBoolType) w -> Int
    forall p (n :: Nat). UnaryBV p n -> Int
    size UnaryBV (p BaseBoolType) w
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1, [(Integer
    v,p BaseBoolType
    _)] <- Map Integer (p BaseBoolType) -> [(Integer, p BaseBoolType)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (UnaryBV (p BaseBoolType) w -> Map Integer (p BaseBoolType)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (p BaseBoolType) w
    x) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    v
      | Bool
    otherwise = Maybe Integer
    forall a. Maybe a
    Nothing

    -- | @unsignedRanges v@ returns a set of predicates and ranges
    -- where we know that for each entry @(p,l,h)@ and each value
    -- @i : l <= i & i <= h@:
    --   @p@ iff. @v <= i@
    unsignedRanges :: UnaryBV p n
                   -> [(p, Integer, Integer)]
    unsignedRanges :: forall p (n :: Nat). UnaryBV p n -> [(p, Integer, Integer)]
    unsignedRanges UnaryBV p n
    v =
        case Map Integer p -> [(Integer, p)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (UnaryBV p n -> Map Integer p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    v) of
          [] -> [Char] -> [(p, Integer, Integer)]
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "internal: unsignedRanges given illegal UnaryBV"
          [(Integer, p)]
    l -> [(Integer, p)] -> [(p, Integer, Integer)]
    forall p. [(Integer, p)] -> [(p, Integer, Integer)]
    go [(Integer, p)]
    l
      where w :: Integer
            w :: Integer
    w = NatRepr n -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned (UnaryBV p n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p n
    v)

            next :: [(Integer,p)] -> Integer
            next :: forall p. [(Integer, p)] -> Integer
    next ((Integer
    h,p
    _):[(Integer, p)]
    _) = Integer
    hInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1
            next [] = Integer
    w

            go :: [(Integer, p)] -> [(p, Integer, Integer)]
            go :: forall p. [(Integer, p)] -> [(p, Integer, Integer)]
    go [] = []
            go ((Integer
    l,p
    p):[(Integer, p)]
    rest) = (p
    p,Integer
    l,[(Integer, p)] -> Integer
    forall p. [(Integer, p)] -> Integer
    next [(Integer, p)]
    rest) (p, Integer, Integer)
    -> [(p, Integer, Integer)] -> [(p, Integer, Integer)]
    forall a. a -> [a] -> [a]
    : [(Integer, p)] -> [(p, Integer, Integer)]
    forall p. [(Integer, p)] -> [(p, Integer, Integer)]
    go [(Integer, p)]
    rest

    unsignedEntries :: (1 <= n)
                    => UnaryBV p n
                    -> [(Integer, p)]
    unsignedEntries :: forall (n :: Nat) p. (1 <= n) => UnaryBV p n -> [(Integer, p)]
    unsignedEntries UnaryBV p n
    b = Map Integer p -> [(Integer, p)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (UnaryBV p n -> Map Integer p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    b)

    -- | Evaluate a unary bitvector as an integer given an evaluation function.
    evaluate :: Monad m => (p -> m Bool) -> UnaryBV p n -> m Integer
    evaluate :: forall (m :: Type -> Type) p (n :: Nat).
    Monad m =>
    (p -> m Bool) -> UnaryBV p n -> m Integer
    evaluate p -> m Bool
    f0 UnaryBV p n
    u = (p -> m Bool) -> IntMap p -> Integer -> m Integer
    forall (m :: Type -> Type) p.
    Monad m =>
    (p -> m Bool) -> IntMap p -> Integer -> m Integer
    go p -> m Bool
    f0 (UnaryBV p n -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    u) (NatRepr n -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned (UnaryBV p n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p n
    u))
      where go :: Monad m => (p -> m Bool) -> IntMap p -> Integer -> m Integer
            go :: forall (m :: Type -> Type) p.
    Monad m =>
    (p -> m Bool) -> IntMap p -> Integer -> m Integer
    go p -> m Bool
    f IntMap p
    m Integer
    bnd =
              case IntMap p -> Maybe (IntMap p, (Integer, p), IntMap p)
    forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
    splitEntry IntMap p
    m of
                Maybe (IntMap p, (Integer, p), IntMap p)
    Nothing -> Integer -> m Integer
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Integer
    bnd
                Just (IntMap p
    l,(Integer
    k,p
    v),IntMap p
    h) -> do
                  Bool
    b <- p -> m Bool
    f p
    v
                  case Bool
    b of
                    -- value <= k
                    Bool
    True -> (p -> m Bool) -> IntMap p -> Integer -> m Integer
    forall (m :: Type -> Type) p.
    Monad m =>
    (p -> m Bool) -> IntMap p -> Integer -> m Integer
    go p -> m Bool
    f IntMap p
    l Integer
    k
                    -- value > k
                    Bool
    False -> (p -> m Bool) -> IntMap p -> Integer -> m Integer
    forall (m :: Type -> Type) p.
    Monad m =>
    (p -> m Bool) -> IntMap p -> Integer -> m Integer
    go p -> m Bool
    f IntMap p
    h Integer
    bnd

    -- | Evaluate a unary bitvector given an evaluation function.
    --
    -- This function is used to convert a unary bitvector into some other representation
    -- such as a binary bitvector or vector of bits.
    --
    -- It is polymorphic over the result type 'r', and requires functions for manipulating
    -- values of type 'r' to construct it.
    sym_evaluate :: (Applicative m, Monad m)
                 => (Integer -> m r)
                    -- ^ Function for mapping an integer to its bitvector
                    -- representation.
                 -> (p -> r -> r -> m r)
                    -- ^ Function for performing an 'ite' expression on 'r'.
                 -> UnaryBV p n
                    -- ^ Unary bitvector to evaluate.
                 -> m r
    sym_evaluate :: forall (m :: Type -> Type) r p (n :: Nat).
    (Applicative m, Monad m) =>
    (Integer -> m r) -> (p -> r -> r -> m r) -> UnaryBV p n -> m r
    sym_evaluate Integer -> m r
    cns0 p -> r -> r -> m r
    ite0 UnaryBV p n
    u = (Integer -> m r)
    -> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
    forall (m :: Type -> Type) r p.
    (Applicative m, Monad m) =>
    (Integer -> m r)
    -> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
    go Integer -> m r
    cns0 p -> r -> r -> m r
    ite0 (UnaryBV p n -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    u) (NatRepr n -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned (UnaryBV p n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p n
    u))
      where go :: (Applicative m, Monad m)
               => (Integer -> m r)
               -> (p -> r -> r -> m r)
               -> IntMap p
               -> Integer
               -> m r
            go :: forall (m :: Type -> Type) r p.
    (Applicative m, Monad m) =>
    (Integer -> m r)
    -> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
    go Integer -> m r
    cns p -> r -> r -> m r
    ite IntMap p
    m Integer
    bnd =
              case IntMap p -> Maybe (IntMap p, (Integer, p), IntMap p)
    forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
    splitEntry IntMap p
    m of
                Maybe (IntMap p, (Integer, p), IntMap p)
    Nothing -> Integer -> m r
    cns Integer
    bnd
                Just (IntMap p
    l,(Integer
    k,p
    v),IntMap p
    h) -> do
                  m (m r) -> m r
    forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
    join (m (m r) -> m r) -> m (m r) -> m r
    forall a b. (a -> b) -> a -> b
    $ p -> r -> r -> m r
    ite p
    v (r -> r -> m r) -> m r -> m (r -> m r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> m r)
    -> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
    forall (m :: Type -> Type) r p.
    (Applicative m, Monad m) =>
    (Integer -> m r)
    -> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
    go Integer -> m r
    cns p -> r -> r -> m r
    ite IntMap p
    l Integer
    k m (r -> m r) -> m r -> m (m r)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> (Integer -> m r)
    -> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
    forall (m :: Type -> Type) r p.
    (Applicative m, Monad m) =>
    (Integer -> m r)
    -> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
    go Integer -> m r
    cns p -> r -> r -> m r
    ite IntMap p
    h Integer
    bnd

    -- | This function instantiates the predicates in a unary predicate with new predicates.
    --
    -- The mapping 'f' should be monotonic, that is for all predicates 'p' and 'q,
    -- such that 'p |- q', 'f' should satisfy the constraint that 'f p |- f q'.
    instantiate :: (Applicative m, Eq q) => (p -> m q) -> UnaryBV p w -> m (UnaryBV q w)
    instantiate :: forall (m :: Type -> Type) q p (w :: Nat).
    (Applicative m, Eq q) =>
    (p -> m q) -> UnaryBV p w -> m (UnaryBV q w)
    instantiate p -> m q
    f UnaryBV p w
    u = Map Integer q -> UnaryBV q w
    fin (Map Integer q -> UnaryBV q w)
    -> m (Map Integer q) -> m (UnaryBV q w)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (p -> m q) -> Map Integer p -> m (Map Integer q)
    forall (t :: Type -> Type) (f :: Type -> Type) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Map Integer a -> f (Map Integer b)
    traverse p -> m q
    f (UnaryBV p w -> Map Integer p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p w
    u)
      where fin :: Map Integer q -> UnaryBV q w
    fin Map Integer q
    m = UnaryBV { width :: NatRepr w
    width = UnaryBV p w -> NatRepr w
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p w
    u
                            , unaryBVMap :: Map Integer q
    unaryBVMap = [(Integer, q)] -> Map Integer q
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList [(Integer, q)]
    l
                            }
              where l :: [(Integer, q)]
    l = [(Integer, q)] -> [(Integer, q)]
    forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
    stripDuplicatePreds (Map Integer q -> [(Integer, q)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Integer q
    m)

    -- | Return potential values for abstract domain.
    domain :: forall p n
            . (1 <= n)
           => (p -> Maybe Bool)
           -> UnaryBV p n
           -> BVDomain n
    domain :: forall p (n :: Nat).
    (1 <= n) =>
    (p -> Maybe Bool) -> UnaryBV p n -> BVDomain n
    domain p -> Maybe Bool
    f UnaryBV p n
    u = NatRepr n -> [Integer] -> BVDomain n
    forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
    BVD.fromAscEltList (UnaryBV p n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p n
    u) (IntMap p -> [Integer]
    go (UnaryBV p n -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    u))
      where go :: IntMap p -> [Integer]
            go :: IntMap p -> [Integer]
    go IntMap p
    m =
              case IntMap p -> Maybe (IntMap p, (Integer, p), IntMap p)
    forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
    splitEntry IntMap p
    m of
                Maybe (IntMap p, (Integer, p), IntMap p)
    Nothing -> []
                Just (IntMap p
    l,(Integer
    k,p
    v),IntMap p
    h) -> do
                  case p -> Maybe Bool
    f p
    v of
                    -- value <= k
                    Just Bool
    True -> Integer
    kInteger -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    :IntMap p -> [Integer]
    go IntMap p
    l
                    -- value > k
                    Just Bool
    False -> IntMap p -> [Integer]
    go IntMap p
    h
                    Maybe Bool
    Nothing -> IntMap p -> [Integer]
    go IntMap p
    l [Integer] -> [Integer] -> [Integer]
    forall a. [a] -> [a] -> [a]
    ++ (Integer
    kInteger -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    :IntMap p -> [Integer]
    go IntMap p
    h)

    ------------------------------------------------------------------------
    -- Operations

    -- | This merges two maps used for a unary bitvector int a single map that
    -- combines them.
    --
    -- 'mergeWithKey sym cfn x y' should return a map 'z' such that for all constants
    -- 'c', 'z = c' iff 'cfn (x = c) (y = c)'.
    mergeWithKey :: forall sym
                  . IsExprBuilder sym
                 => sym
                 -> (Pred sym -> Pred sym -> IO (Pred sym))
                 -> IntMap (Pred sym)
                 -> IntMap (Pred sym)
                 -> IO (IntMap (Pred sym))
    mergeWithKey :: forall sym.
    IsExprBuilder sym =>
    sym
    -> (Pred sym -> Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    mergeWithKey sym
    sym Pred sym -> Pred sym -> IO (Pred sym)
    f IntMap (Pred sym)
    x IntMap (Pred sym)
    y =
        IntMap (Pred sym)
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> IO (IntMap (Pred sym))
    go IntMap (Pred sym)
    forall k a. Map k a
    Map.empty (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym) (IntMap (Pred sym) -> [(Integer, Pred sym)]
    forall k a. Map k a -> [(k, a)]
    Map.toList IntMap (Pred sym)
    x)
                     (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym) (IntMap (Pred sym) -> [(Integer, Pred sym)]
    forall k a. Map k a -> [(k, a)]
    Map.toList IntMap (Pred sym)
    y)
      where go :: IntMap (Pred sym)
               -> Pred sym
               -> [(Integer, Pred sym)]
               -> Pred sym
               -> [(Integer, Pred sym)]
               -> IO (IntMap (Pred sym))
            -- Force "m" to be evaluated"
            go :: IntMap (Pred sym)
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> IO (IntMap (Pred sym))
    go IntMap (Pred sym)
    m Pred sym
    _ [(Integer, Pred sym)]
    _ Pred sym
    _ [(Integer, Pred sym)]
    _ | IntMap (Pred sym) -> Bool -> Bool
    forall a b. a -> b -> b
    seq IntMap (Pred sym)
    m (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Bool
    False = [Char] -> IO (IntMap (Pred sym))
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "go bad"
            go IntMap (Pred sym)
    m Pred sym
    x_prev x_a :: [(Integer, Pred sym)]
    x_a@((Integer
    x_k,Pred sym
    x_p):[(Integer, Pred sym)]
    x_r) Pred sym
    y_prev y_a :: [(Integer, Pred sym)]
    y_a@((Integer
    y_k,Pred sym
    y_p):[(Integer, Pred sym)]
    y_r) =
              case Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    x_k Integer
    y_k of
                Ordering
    LT -> do
                  Pred sym
    p <- Pred sym -> Pred sym -> IO (Pred sym)
    f Pred sym
    x_p Pred sym
    y_prev
                  IntMap (Pred sym)
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> IO (IntMap (Pred sym))
    go (Integer -> Pred sym -> IntMap (Pred sym) -> IntMap (Pred sym)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Integer
    x_k Pred sym
    p IntMap (Pred sym)
    m) Pred sym
    x_p [(Integer, Pred sym)]
    x_r Pred sym
    y_prev [(Integer, Pred sym)]
    y_a
                Ordering
    GT -> do
                  Pred sym
    p <- Pred sym -> Pred sym -> IO (Pred sym)
    f Pred sym
    x_prev Pred sym
    y_p
                  IntMap (Pred sym)
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> IO (IntMap (Pred sym))
    go (Integer -> Pred sym -> IntMap (Pred sym) -> IntMap (Pred sym)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Integer
    y_k Pred sym
    p IntMap (Pred sym)
    m) Pred sym
    x_prev [(Integer, Pred sym)]
    x_a Pred sym
    y_p [(Integer, Pred sym)]
    y_r
                Ordering
    EQ -> do
                  Pred sym
    p <- Pred sym -> Pred sym -> IO (Pred sym)
    f Pred sym
    x_p Pred sym
    y_p
                  IntMap (Pred sym)
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> Pred sym
    -> [(Integer, Pred sym)]
    -> IO (IntMap (Pred sym))
    go (Integer -> Pred sym -> IntMap (Pred sym) -> IntMap (Pred sym)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Integer
    x_k Pred sym
    p IntMap (Pred sym)
    m) Pred sym
    x_p [(Integer, Pred sym)]
    x_r Pred sym
    y_p [(Integer, Pred sym)]
    y_r
            go IntMap (Pred sym)
    m Pred sym
    _ [] Pred sym
    _ [(Integer, Pred sym)]
    y_a = do
              IntMap (Pred sym)
    -> (Pred sym -> IO (Pred sym))
    -> [(Integer, Pred sym)]
    -> IO (IntMap (Pred sym))
    forall {m :: Type -> Type} {k} {a} {t}.
    (Monad m, Ord k) =>
    Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
    go1 IntMap (Pred sym)
    m (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym Pred sym -> Pred sym -> IO (Pred sym)
    `f`) [(Integer, Pred sym)]
    y_a
            go IntMap (Pred sym)
    m Pred sym
    _ [(Integer, Pred sym)]
    x_a Pred sym
    _ [] = do
              IntMap (Pred sym)
    -> (Pred sym -> IO (Pred sym))
    -> [(Integer, Pred sym)]
    -> IO (IntMap (Pred sym))
    forall {m :: Type -> Type} {k} {a} {t}.
    (Monad m, Ord k) =>
    Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
    go1 IntMap (Pred sym)
    m (Pred sym -> Pred sym -> IO (Pred sym)
    `f` sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym) [(Integer, Pred sym)]
    x_a

            go1 :: Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
    go1 Map k a
    m t -> m a
    fn ((k
    y_k,t
    y_p):[(k, t)]
    y_r) = do
              a
    p <- t -> m a
    fn t
    y_p
              Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
    go1 (k -> a -> Map k a -> Map k a
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert k
    y_k a
    p Map k a
    m) t -> m a
    fn [(k, t)]
    y_r
            go1 Map k a
    m t -> m a
    _ [] =
              Map k a -> m (Map k a)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Map k a
    m

    -- | @mux sym c x y@ returns value equal to if @c@ then @x@ else @y@.
    -- The number of entries in the return value is at most @size x@
    -- + @size y@.
    mux :: forall sym n
         . (1 <= n, IsExprBuilder sym)
        => sym
        -> Pred sym
        -> UnaryBV (Pred sym) n
        -> UnaryBV (Pred sym) n
        -> IO (UnaryBV (Pred sym) n)
    mux :: forall sym (n :: Nat).
    (1 <= n, IsExprBuilder sym) =>
    sym
    -> Pred sym
    -> UnaryBV (Pred sym) n
    -> UnaryBV (Pred sym) n
    -> IO (UnaryBV (Pred sym) n)
    mux sym
    sym Pred sym
    c UnaryBV (Pred sym) n
    x UnaryBV (Pred sym) n
    y = (IntMap (Pred sym) -> UnaryBV (Pred sym) n)
    -> IO (IntMap (Pred sym)) -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NatRepr n -> IntMap (Pred sym) -> UnaryBV (Pred sym) n
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV (UnaryBV (Pred sym) n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV (Pred sym) n
    x)) (IO (IntMap (Pred sym)) -> IO (UnaryBV (Pred sym) n))
    -> IO (IntMap (Pred sym)) -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $
      sym
    -> (Pred sym -> Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    forall sym.
    IsExprBuilder sym =>
    sym
    -> (Pred sym -> Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    mergeWithKey sym
    sym
                   (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)
                   (UnaryBV (Pred sym) n -> IntMap (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x)
                   (UnaryBV (Pred sym) n -> IntMap (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    y)

    -- | Return predicate that holds if bitvectors are equal.
    eq :: (1 <= n, IsExprBuilder sym)
       => sym
       -> UnaryBV (Pred sym) n
       -> UnaryBV (Pred sym) n
       -> IO (Pred sym)
    eq :: forall (n :: Nat) sym.
    (1 <= n, IsExprBuilder sym) =>
    sym
    -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
    eq sym
    sym0 UnaryBV (Pred sym) n
    x0 UnaryBV (Pred sym) n
    y0 =
        let (Integer
    x_k, Pred sym
    x_p) = Map Integer (Pred sym) -> (Integer, Pred sym)
    forall k a. Map k a -> (k, a)
    Map.findMin (UnaryBV (Pred sym) n -> Map Integer (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x0)
         in sym
    -> Pred sym
    -> Integer
    -> Pred sym
    -> Map Integer (Pred sym)
    -> Map Integer (Pred sym)
    -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> Integer
    -> Pred sym
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (Pred sym)
    go sym
    sym0 (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym0) Integer
    x_k Pred sym
    x_p (UnaryBV (Pred sym) n -> Map Integer (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x0) (UnaryBV (Pred sym) n -> Map Integer (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    y0)
      where go :: IsExprBuilder sym
                => sym
                -> Pred sym
                -> Integer
                -> Pred sym
                -> IntMap (Pred sym)
                -> IntMap (Pred sym)
                -> IO (Pred sym)
            go :: forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> Integer
    -> Pred sym
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (Pred sym)
    go sym
    sym Pred sym
    r Integer
    x_k Pred sym
    x_p IntMap (Pred sym)
    x IntMap (Pred sym)
    y
              | Just (Integer
    y_k, Pred sym
    y_p) <- Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupGE Integer
    x_k IntMap (Pred sym)
    y =
                case Integer
    x_k Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    y_k of
                  Bool
    False -> do
                    sym
    -> Pred sym
    -> Integer
    -> Pred sym
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> Integer
    -> Pred sym
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (Pred sym)
    go sym
    sym Pred sym
    r Integer
    y_k Pred sym
    y_p IntMap (Pred sym)
    y IntMap (Pred sym)
    x
                  Bool
    True -> do
                    let x_lt :: Pred sym
    x_lt = Pred sym
    -> ((Integer, Pred sym) -> Pred sym)
    -> Maybe (Integer, Pred sym)
    -> Pred sym
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym) (Integer, Pred sym) -> Pred sym
    forall a b. (a, b) -> b
    snd (Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupLT Integer
    x_k IntMap (Pred sym)
    x)
                    let y_lt :: Pred sym
    y_lt = Pred sym
    -> ((Integer, Pred sym) -> Pred sym)
    -> Maybe (Integer, Pred sym)
    -> Pred sym
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym) (Integer, Pred sym) -> Pred sym
    forall a b. (a, b) -> b
    snd (Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupLT Integer
    x_k IntMap (Pred sym)
    y)
                    Pred sym
    x_is_eq <- 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
    x_p (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 -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym Pred sym
    x_lt
                    Pred sym
    y_is_eq <- 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
    y_p (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 -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym Pred sym
    y_lt
                    Pred sym
    r' <- 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
    r (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
    x_is_eq Pred sym
    y_is_eq
                    case Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupGE (Integer
    x_kInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1) IntMap (Pred sym)
    x of
                      Just (Integer
    x_k', Pred sym
    x_p') -> sym
    -> Pred sym
    -> Integer
    -> Pred sym
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> Integer
    -> Pred sym
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (Pred sym)
    go sym
    sym Pred sym
    r' Integer
    x_k' Pred sym
    x_p' IntMap (Pred sym)
    x IntMap (Pred sym)
    y
                      Maybe (Integer, Pred sym)
    Nothing -> Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Pred sym
    r'
            go sym
    _ Pred sym
    r Integer
    _ Pred sym
    _ IntMap (Pred sym)
    _ IntMap (Pred sym)
    _ = Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Pred sym
    r

    -- | @compareLt sym x y@ returns predicate that holds
    -- if for any @k@, @x < k & not (y <= k)@.
    compareLt :: forall sym
               . IsExprBuilder sym
              => sym
              -> IntMap (Pred sym)
              -> IntMap (Pred sym)
              -> IO (Pred sym)
    compareLt :: forall sym.
    IsExprBuilder sym =>
    sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
    compareLt sym
    sym IntMap (Pred sym)
    x IntMap (Pred sym)
    y
        | IntMap (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null IntMap (Pred sym)
    y = Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym)
        | Bool
    otherwise  = Pred sym -> Integer -> IO (Pred sym)
    go (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym) Integer
    0
      where go :: Pred sym -- ^ Return predicate for cases where x is less than minimum.
               -> Integer  -- ^ Minimum value to consider for x.
               -> IO (Pred sym)
            go :: Pred sym -> Integer -> IO (Pred sym)
    go Pred sym
    r Integer
    min_x
                -- Let x_k0 be min entry in x to consider next.
              | Just (Integer
    x_k, Pred sym
    _) <- Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupGE Integer
    min_x IntMap (Pred sym)
    x
                -- Get smallest entry in y that is larger than x_k.
              , Just (Integer
    y_k, Pred sym
    _) <- Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupGT Integer
    x_k IntMap (Pred sym)
    y
                -- Lookup largest predicate in x for value that is less then y_k.
              , Just (Integer
    x_k_max, Pred sym
    x_p) <- Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupLT Integer
    y_k IntMap (Pred sym)
    x = do

                -- We know the following:
                -- 1. min_x <= x_k <= x_k_max < y_k.
                -- 2. y > x_k => y >= y_k
                -- 3. x < y_k => x_p

                -- Get predicate asserting x < y_k && not (y <= x_k)
                -- Get predicate asserting x < y_k && y > x_k
                Pred sym
    x_and_y_lt_x_k <-
                  case Integer -> IntMap (Pred sym) -> Maybe (Integer, Pred sym)
    forall k v. Ord k => k -> Map k v -> Maybe (k, v)
    Map.lookupLT Integer
    y_k IntMap (Pred sym)
    y of
                    Maybe (Integer, Pred sym)
    Nothing -> Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Pred sym -> IO (Pred sym)) -> Pred sym -> IO (Pred sym)
    forall a b. (a -> b) -> a -> b
    $ Pred sym
    x_p
                    Just (Integer
    _,Pred sym
    y_lt_y_k) -> 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
    x_p (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 -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym Pred sym
    y_lt_y_k

                Pred sym
    r' <- 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
    r Pred sym
    x_and_y_lt_x_k
                Pred sym -> Integer -> IO (Pred sym)
    go Pred sym
    r' (Integer
    x_k_maxInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1)

            go Pred sym
    r Integer
    _ = sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    andPred sym
    sym ((Integer, Pred sym) -> Pred sym
    forall a b. (a, b) -> b
    snd (IntMap (Pred sym) -> (Integer, Pred sym)
    forall k a. Map k a -> (k, a)
    Map.findMax IntMap (Pred sym)
    y)) Pred sym
    r

    -- | Return predicate that holds if first value is less than other.
    ult :: (1 <= n, IsExprBuilder sym)
        => sym
        -> UnaryBV (Pred sym) n
        -> UnaryBV (Pred sym) n
        -> IO (Pred sym)
    ult :: forall (n :: Nat) sym.
    (1 <= n, IsExprBuilder sym) =>
    sym
    -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
    ult sym
    sym UnaryBV (Pred sym) n
    x UnaryBV (Pred sym) n
    y = sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
    compareLt sym
    sym (UnaryBV (Pred sym) n -> IntMap (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x) (UnaryBV (Pred sym) n -> IntMap (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    y)

    -- | Return predicate that holds if first value is less than other.
    slt :: (1 <= n, IsExprBuilder sym)
        => sym
        -> UnaryBV (Pred sym) n
        -> UnaryBV (Pred sym) n
        -> IO (Pred sym)
    slt :: forall (n :: Nat) sym.
    (1 <= n, IsExprBuilder sym) =>
    sym
    -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
    slt sym
    sym UnaryBV (Pred sym) n
    x UnaryBV (Pred sym) n
    y = do
      let mid :: Integer
    mid = NatRepr n -> Integer
    forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
    maxSigned (UnaryBV (Pred sym) n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV (Pred sym) n
    x)

      -- Split map so that we separate the values that will remain positive
      -- from the values that will be negative.
      let (IntMap (Pred sym)
    x_pos,IntMap (Pred sym)
    x_neg) = Integer
    -> IntMap (Pred sym) -> (IntMap (Pred sym), IntMap (Pred sym))
    forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
    splitLeq Integer
    mid (UnaryBV (Pred sym) n -> IntMap (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x)

      -- Split map so that we separate the values that will remain positive
      -- from the values that will be negative.
      let (IntMap (Pred sym)
    y_pos,IntMap (Pred sym)
    y_neg) = Integer
    -> IntMap (Pred sym) -> (IntMap (Pred sym), IntMap (Pred sym))
    forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
    splitLeq Integer
    mid (UnaryBV (Pred sym) n -> IntMap (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    y)

      Pred sym
    x_is_neg <-
        if IntMap (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null IntMap (Pred sym)
    x_pos then
          Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Pred sym -> IO (Pred sym)) -> Pred sym -> IO (Pred sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym
        else
          sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym ((Integer, Pred sym) -> Pred sym
    forall a b. (a, b) -> b
    snd (IntMap (Pred sym) -> (Integer, Pred sym)
    forall k a. Map k a -> (k, a)
    Map.findMax IntMap (Pred sym)
    x_pos))

      Pred sym
    pos_case <- sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
    compareLt sym
    sym IntMap (Pred sym)
    x_pos IntMap (Pred sym)
    y_pos
      Pred sym
    neg_case <- 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
    x_is_neg (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 -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
    compareLt sym
    sym IntMap (Pred sym)
    x_neg IntMap (Pred sym)
    y_neg
      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
    pos_case Pred sym
    neg_case

    splitOnAddOverflow :: Integer -> UnaryBV p n -> (IntMap p, IntMap p)
    splitOnAddOverflow :: forall p (n :: Nat). Integer -> UnaryBV p n -> (IntMap p, IntMap p)
    splitOnAddOverflow Integer
    v UnaryBV p n
    x = Bool -> (IntMap p, IntMap p) -> (IntMap p, IntMap p)
    forall a. HasCallStack => Bool -> a -> a
    assert (Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    v Bool -> Bool -> Bool
    && Integer
    v Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    limit) ((IntMap p, IntMap p) -> (IntMap p, IntMap p))
    -> (IntMap p, IntMap p) -> (IntMap p, IntMap p)
    forall a b. (a -> b) -> a -> b
    $
                               Integer -> IntMap p -> (IntMap p, IntMap p)
    forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
    splitLeq Integer
    overflow_limit (UnaryBV p n -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p n
    x)
        where limit :: Integer
    limit = NatRepr n -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned (UnaryBV p n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p n
    x)
              overflow_limit :: Integer
    overflow_limit = Integer
    limit Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    v

    completeList :: IsExprBuilder sym
                 => sym
                 -> IntMap (Pred sym) -- ^ Map to merge into
                 -> (Integer -> Integer) -- ^ Monotonic function to update keys with
                 -> (Pred sym -> IO (Pred sym)) -- ^ Function on predicate.
                 -> IntMap (Pred sym)
                 -> IO (IntMap (Pred sym))
    completeList :: forall sym.
    IsExprBuilder sym =>
    sym
    -> IntMap (Pred sym)
    -> (Integer -> Integer)
    -> (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    completeList sym
    sym IntMap (Pred sym)
    x Integer -> Integer
    keyFn Pred sym -> IO (Pred sym)
    predFn IntMap (Pred sym)
    m0 = do
      let m1 :: IntMap (Pred sym)
    m1 = (Integer -> Integer) -> IntMap (Pred sym) -> IntMap (Pred sym)
    forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
    Map.mapKeysMonotonic Integer -> Integer
    keyFn IntMap (Pred sym)
    m0
      IntMap (Pred sym)
    m2 <- (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym) -> IO (IntMap (Pred sym))
    forall (t :: Type -> Type) (f :: Type -> Type) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Map Integer a -> f (Map Integer b)
    traverse Pred sym -> IO (Pred sym)
    predFn IntMap (Pred sym)
    m1
      sym
    -> (Pred sym -> Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    forall sym.
    IsExprBuilder sym =>
    sym
    -> (Pred sym -> Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    mergeWithKey sym
    sym (sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    orPred sym
    sym) IntMap (Pred sym)
    x IntMap (Pred sym)
    m2

    addConstant :: forall sym n
                 . (1 <= n, IsExprBuilder sym)
                => sym
                -> IntMap (Pred sym)
                -> Pred sym
                -> Integer
                -> Pred sym
                -> UnaryBV (Pred sym) n
                -> IO (IntMap (Pred sym))
    addConstant :: forall sym (n :: Nat).
    (1 <= n, IsExprBuilder sym) =>
    sym
    -> IntMap (Pred sym)
    -> Pred sym
    -> Integer
    -> Pred sym
    -> UnaryBV (Pred sym) n
    -> IO (IntMap (Pred sym))
    addConstant sym
    sym IntMap (Pred sym)
    m0 Pred sym
    x_lt Integer
    x_val Pred sym
    x_leq UnaryBV (Pred sym) n
    y = do
      let w :: NatRepr n
    w = UnaryBV (Pred sym) n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV (Pred sym) n
    y

      let (IntMap (Pred sym)
    y_low, IntMap (Pred sym)
    y_high) = Integer
    -> UnaryBV (Pred sym) n -> (IntMap (Pred sym), IntMap (Pred sym))
    forall p (n :: Nat). Integer -> UnaryBV p n -> (IntMap p, IntMap p)
    splitOnAddOverflow Integer
    x_val UnaryBV (Pred sym) n
    y

      IntMap (Pred sym)
    m1 <- sym
    -> IntMap (Pred sym)
    -> (Integer -> Integer)
    -> (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    forall sym.
    IsExprBuilder sym =>
    sym
    -> IntMap (Pred sym)
    -> (Integer -> Integer)
    -> (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    completeList sym
    sym IntMap (Pred sym)
    m0 (Integer
    x_val Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +) (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
    x_leq) IntMap (Pred sym)
    y_low

      -- Add entries when we don't overflow.
      -- If no overflow then continue
      case IntMap (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null IntMap (Pred sym)
    y_high of
        Bool
    True -> IntMap (Pred sym) -> IO (IntMap (Pred sym))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return IntMap (Pred sym)
    m1
        Bool
    False -> do
          -- See if there are any entries that do not overflow.
          -- Compute amount of offset to apply to y_val
          let x_off :: Integer
    x_off = Integer
    x_valInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    2Integer -> Nat -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^NatRepr n -> Nat
    forall (n :: Nat). NatRepr n -> Nat
    natValue NatRepr n
    w
          -- Generate predicate asserting that y overflows and x == x_val
          Pred sym
    x_eq <- 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
    x_leq (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 -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym Pred sym
    x_lt
          Pred sym
    p <-
            case IntMap (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null IntMap (Pred sym)
    y_low of
              Bool
    True -> Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Pred sym -> IO (Pred sym)) -> Pred sym -> IO (Pred sym)
    forall a b. (a -> b) -> a -> b
    $ Pred sym
    x_eq
              Bool
    False -> 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
    x_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
    =<< sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym ((Integer, Pred sym) -> Pred sym
    forall a b. (a, b) -> b
    snd (IntMap (Pred sym) -> (Integer, Pred sym)
    forall k a. Map k a -> (k, a)
    Map.findMax IntMap (Pred sym)
    y_low))
          -- Complete next entries
          sym
    -> IntMap (Pred sym)
    -> (Integer -> Integer)
    -> (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    forall sym.
    IsExprBuilder sym =>
    sym
    -> IntMap (Pred sym)
    -> (Integer -> Integer)
    -> (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    completeList sym
    sym IntMap (Pred sym)
    m1 (Integer
    x_off Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +) (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
    p) IntMap (Pred sym)
    y_high

    -- | Add two bitvectors.
    --
    -- The number of integers in the result will be at most the product of the sizes
    -- of the individual bitvectors.
    add :: forall sym n
         . (1 <= n, IsExprBuilder sym)
        => sym
        -> UnaryBV (Pred sym) n
        -> UnaryBV (Pred sym) n
        -> IO (UnaryBV (Pred sym) n)
    add :: forall sym (n :: Nat).
    (1 <= n, IsExprBuilder sym) =>
    sym
    -> UnaryBV (Pred sym) n
    -> UnaryBV (Pred sym) n
    -> IO (UnaryBV (Pred sym) n)
    add sym
    sym UnaryBV (Pred sym) n
    x UnaryBV (Pred sym) n
    y = IntMap (Pred sym)
    -> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
    go_x IntMap (Pred sym)
    forall k a. Map k a
    Map.empty (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym) (UnaryBV (Pred sym) n -> [(Integer, Pred sym)]
    forall (n :: Nat) p. (1 <= n) => UnaryBV p n -> [(Integer, p)]
    unsignedEntries UnaryBV (Pred sym) n
    x)
      where w :: NatRepr n
    w = UnaryBV (Pred sym) n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV (Pred sym) n
    x
            go_x :: IntMap (Pred sym)
                 -> Pred sym
                 -> [(Integer, Pred sym)]
                 -> IO (UnaryBV (Pred sym) n)
            go_x :: IntMap (Pred sym)
    -> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
    go_x IntMap (Pred sym)
    m0 Pred sym
    _ [] = do
              UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n))
    -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $! NatRepr n -> IntMap (Pred sym) -> UnaryBV (Pred sym) n
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV NatRepr n
    w IntMap (Pred sym)
    m0
            go_x IntMap (Pred sym)
    m0 Pred sym
    x_lt ((Integer
    x_val,Pred sym
    x_leq):[(Integer, Pred sym)]
    remaining) = do
              IntMap (Pred sym)
    m2 <- sym
    -> IntMap (Pred sym)
    -> Pred sym
    -> Integer
    -> Pred sym
    -> UnaryBV (Pred sym) n
    -> IO (IntMap (Pred sym))
    forall sym (n :: Nat).
    (1 <= n, IsExprBuilder sym) =>
    sym
    -> IntMap (Pred sym)
    -> Pred sym
    -> Integer
    -> Pred sym
    -> UnaryBV (Pred sym) n
    -> IO (IntMap (Pred sym))
    addConstant sym
    sym IntMap (Pred sym)
    m0 Pred sym
    x_lt Integer
    x_val Pred sym
    x_leq UnaryBV (Pred sym) n
    y
              IntMap (Pred sym)
    -> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
    go_x IntMap (Pred sym)
    m2 Pred sym
    x_leq [(Integer, Pred sym)]
    remaining

    -- | Negate a bitvector.
    -- The size of the result will be equal to the size of the input.
    neg :: forall sym n
         . (1 <= n, IsExprBuilder sym)
        => sym
        -> UnaryBV (Pred sym) n
        -> IO (UnaryBV (Pred sym) n)
    neg :: forall sym (n :: Nat).
    (1 <= n, IsExprBuilder sym) =>
    sym -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
    neg sym
    sym UnaryBV (Pred sym) n
    x
      | Map Integer (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null (UnaryBV (Pred sym) n -> Map Integer (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x) = [Char] -> IO (UnaryBV (Pred sym) n)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Illegal unary value"
      | Bool
    otherwise =
        case Map Integer (Pred sym)
    -> ((Integer, Pred sym), Map Integer (Pred sym))
    forall k a. Map k a -> ((k, a), Map k a)
    Map.deleteFindMin (UnaryBV (Pred sym) n -> Map Integer (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x) of
          -- Special case for constant 0.
          ((Integer
    0,Pred sym
    _), Map Integer (Pred sym)
    m) | Map Integer (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null Map Integer (Pred sym)
    m -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return UnaryBV (Pred sym) n
    x
          -- Treat 0 case specially, then recurse on remaining elements.
          ((Integer
    0,Pred sym
    x_p), Map Integer (Pred sym)
    m) -> [(Integer, Pred sym)]
    -> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
    go [(Integer
    0, Pred sym
    x_p)] Pred sym
    x_p             (Map Integer (Pred sym) -> [(Integer, Pred sym)]
    forall k a. Map k a -> [(k, a)]
    Map.toDescList Map Integer (Pred sym)
    m)
          -- Value can't be 0, so just recurse on all ements.
          ((Integer, Pred sym), Map Integer (Pred sym))
    _ ->            [(Integer, Pred sym)]
    -> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
    go []         (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred sym
    sym) (Map Integer (Pred sym) -> [(Integer, Pred sym)]
    forall k a. Map k a -> [(k, a)]
    Map.toDescList (UnaryBV (Pred sym) n -> Map Integer (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) n
    x))
      where w :: NatRepr n
    w = UnaryBV (Pred sym) n -> NatRepr n
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV (Pred sym) n
    x
            -- Iterate through remaining pairs in descending order.
            go :: [(Integer, Pred sym)]
                  -- ^ Entries in descending order
               -> Pred sym -- ^ Predicate for first false.
               -> [(Integer, Pred sym)]
                  -- ^ Remaining elements in descending order.
               -> IO (UnaryBV (Pred sym) n)
            go :: [(Integer, Pred sym)]
    -> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
    go [(Integer, Pred sym)]
    m Pred sym
    p ((Integer
    x_k,Pred sym
    _) : r :: [(Integer, Pred sym)]
    r@((Integer
    _,Pred sym
    y_p):[(Integer, Pred sym)]
    _)) = [(Integer, Pred sym)]
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. a -> b -> b
    seq [(Integer, Pred sym)]
    m (IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n))
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $ do
              let z_k :: Integer
    z_k = NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    w (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    x_k)
              Pred sym
    q <- 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
    p (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 -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym Pred sym
    y_p
              let pair :: (Integer, Pred sym)
    pair = (Integer
    z_k,Pred sym
    q)
              let m' :: [(Integer, Pred sym)]
    m' = (Integer, Pred sym)
    pair (Integer, Pred sym)
    -> [(Integer, Pred sym)] -> [(Integer, Pred sym)]
    forall a. a -> [a] -> [a]
    : [(Integer, Pred sym)]
    m
              Integer -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. a -> b -> b
    seq Integer
    z_k (IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n))
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $ (Integer, Pred sym)
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. a -> b -> b
    seq (Integer, Pred sym)
    pair (IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n))
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $ [(Integer, Pred sym)]
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. a -> b -> b
    seq [(Integer, Pred sym)]
    m' (IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n))
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $ do
              [(Integer, Pred sym)]
    -> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
    go [(Integer, Pred sym)]
    m' Pred sym
    p [(Integer, Pred sym)]
    r
            go [(Integer, Pred sym)]
    m Pred sym
    _ [(Integer
    x_k,Pred sym
    _)] = [(Integer, Pred sym)]
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. a -> b -> b
    seq [(Integer, Pred sym)]
    m (IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n))
    -> IO (UnaryBV (Pred sym) n) -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $ do
              let z_k :: Integer
    z_k = NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    w (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    x_k)
              let q :: Pred sym
    q = sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym
              UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n))
    -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
    forall a b. (a -> b) -> a -> b
    $! NatRepr n -> Map Integer (Pred sym) -> UnaryBV (Pred sym) n
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV NatRepr n
    w ([(Integer, Pred sym)] -> Map Integer (Pred sym)
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList ([(Integer, Pred sym)] -> [(Integer, Pred sym)]
    forall a. [a] -> [a]
    reverse ((Integer
    z_k,Pred sym
    q) (Integer, Pred sym)
    -> [(Integer, Pred sym)] -> [(Integer, Pred sym)]
    forall a. a -> [a] -> [a]
    : [(Integer, Pred sym)]
    m)))
            go [(Integer, Pred sym)]
    _ Pred sym
    _ [] = [Char] -> IO (UnaryBV (Pred sym) n)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Illegal value return in UnaryBV.neg"

    -- | Perform a unsigned extension
    uext :: (1 <= u, u+1 <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r
    uext :: forall (u :: Nat) (r :: Nat) p.
    (1 <= u, (u + 1) <= r) =>
    UnaryBV p u -> NatRepr r -> UnaryBV p r
    uext UnaryBV p u
    x NatRepr r
    w' = NatRepr r -> IntMap p -> UnaryBV p r
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV NatRepr r
    w' (UnaryBV p u -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p u
    x)

    -- | Perform a signed extension
    sext :: (1 <= u, u+1 <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r
    sext :: forall (u :: Nat) (r :: Nat) p.
    (1 <= u, (u + 1) <= r) =>
    UnaryBV p u -> NatRepr r -> UnaryBV p r
    sext UnaryBV p u
    x NatRepr r
    w' = NatRepr r -> IntMap p -> UnaryBV p r
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV NatRepr r
    w' (IntMap p -> IntMap p -> IntMap p
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union IntMap p
    neg_entries IntMap p
    l)
      where w :: NatRepr u
    w = UnaryBV p u -> NatRepr u
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV p u
    x
            mid :: Integer
    mid = NatRepr u -> Integer
    forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
    maxSigned NatRepr u
    w
            (IntMap p
    l,IntMap p
    h) = Integer -> IntMap p -> (IntMap p, IntMap p)
    forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
    splitLeq Integer
    mid (UnaryBV p u -> IntMap p
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV p u
    x)

            diff :: Integer
    diff = Integer
    2Integer -> Nat -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^NatRepr r -> Nat
    forall (n :: Nat). NatRepr n -> Nat
    natValue NatRepr r
    w' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    2Integer -> Nat -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^NatRepr u -> Nat
    forall (n :: Nat). NatRepr n -> Nat
    natValue NatRepr u
    w
            neg_entries :: IntMap p
    neg_entries = (Integer -> Integer) -> IntMap p -> IntMap p
    forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
    Map.mapKeysMonotonic (Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    diff) IntMap p
    h

    -- | Perform a struncation.
    trunc :: forall sym u r
           . (IsExprBuilder sym, 1 <= u, u <= r)
          => sym
          -> UnaryBV (Pred sym) r
          -> NatRepr u
          -> IO (UnaryBV (Pred sym) u)
    trunc :: forall sym (u :: Nat) (r :: Nat).
    (IsExprBuilder sym, 1 <= u, u <= r) =>
    sym
    -> UnaryBV (Pred sym) r -> NatRepr u -> IO (UnaryBV (Pred sym) u)
    trunc sym
    sym UnaryBV (Pred sym) r
    x NatRepr u
    w
      | Just u :~: r
    Refl <- NatRepr u -> NatRepr r -> Maybe (u :~: r)
    forall (a :: Nat) (b :: Nat).
    NatRepr a -> NatRepr b -> Maybe (a :~: b)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality NatRepr u
    w (UnaryBV (Pred sym) r -> NatRepr r
    forall p (n :: Nat). UnaryBV p n -> NatRepr n
    width UnaryBV (Pred sym) r
    x) = UnaryBV (Pred sym) u -> IO (UnaryBV (Pred sym) u)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return UnaryBV (Pred sym) u
    UnaryBV (Pred sym) r
    x
      | Bool
    otherwise = IntMap (Pred sym)
    -> Pred sym -> IntMap (Pred sym) -> IO (UnaryBV (Pred sym) u)
    go IntMap (Pred sym)
    forall k a. Map k a
    Map.empty (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym) (UnaryBV (Pred sym) r -> IntMap (Pred sym)
    forall p (n :: Nat). UnaryBV p n -> IntMap p
    unaryBVMap UnaryBV (Pred sym) r
    x)
      where go :: IntMap (Pred sym)
               -> Pred sym
               -> IntMap (Pred sym)
               -> IO (UnaryBV (Pred sym) u)
            go :: IntMap (Pred sym)
    -> Pred sym -> IntMap (Pred sym) -> IO (UnaryBV (Pred sym) u)
    go IntMap (Pred sym)
    result Pred sym
    toRemove IntMap (Pred sym)
    remaining
              | IntMap (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null IntMap (Pred sym)
    remaining =
                UnaryBV (Pred sym) u -> IO (UnaryBV (Pred sym) u)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (UnaryBV (Pred sym) u -> IO (UnaryBV (Pred sym) u))
    -> UnaryBV (Pred sym) u -> IO (UnaryBV (Pred sym) u)
    forall a b. (a -> b) -> a -> b
    $! NatRepr u -> IntMap (Pred sym) -> UnaryBV (Pred sym) u
    forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
    UnaryBV NatRepr u
    w IntMap (Pred sym)
    result
              | Bool
    otherwise = do
                let (Integer
    k,Pred sym
    _) = IntMap (Pred sym) -> (Integer, Pred sym)
    forall k a. Map k a -> (k, a)
    Map.findMin IntMap (Pred sym)
    remaining
                -- Get base offset
                let base :: Integer
    base = Integer
    k Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    `xor` (NatRepr u -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned NatRepr u
    w)
                let next :: Integer
    next = Integer
    base Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + NatRepr u -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned NatRepr u
    w
                let (IntMap (Pred sym)
    l,IntMap (Pred sym)
    h) = Integer
    -> IntMap (Pred sym) -> (IntMap (Pred sym), IntMap (Pred sym))
    forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
    splitLeq Integer
    next IntMap (Pred sym)
    remaining

                Bool -> IO (UnaryBV (Pred sym) u) -> IO (UnaryBV (Pred sym) u)
    forall a. HasCallStack => Bool -> a -> a
    assert (Bool -> Bool
    not (IntMap (Pred sym) -> Bool
    forall k a. Map k a -> Bool
    Map.null IntMap (Pred sym)
    l)) (IO (UnaryBV (Pred sym) u) -> IO (UnaryBV (Pred sym) u))
    -> IO (UnaryBV (Pred sym) u) -> IO (UnaryBV (Pred sym) u)
    forall a b. (a -> b) -> a -> b
    $ do
                -- Get entries to add.
                IntMap (Pred sym)
    result' <- sym
    -> IntMap (Pred sym)
    -> (Integer -> Integer)
    -> (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    forall sym.
    IsExprBuilder sym =>
    sym
    -> IntMap (Pred sym)
    -> (Integer -> Integer)
    -> (Pred sym -> IO (Pred sym))
    -> IntMap (Pred sym)
    -> IO (IntMap (Pred sym))
    completeList sym
    sym IntMap (Pred sym)
    result (NatRepr u -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr u
    w) (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
    toRemove) IntMap (Pred sym)
    l

                let (Integer
    _,Pred sym
    p) = IntMap (Pred sym) -> (Integer, Pred sym)
    forall k a. Map k a -> (k, a)
    Map.findMax IntMap (Pred sym)
    l
                Pred sym
    toRemove' <- sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym Pred sym
    p
                IntMap (Pred sym)
    -> Pred sym -> IntMap (Pred sym) -> IO (UnaryBV (Pred sym) u)
    go IntMap (Pred sym)
    result' Pred sym
    toRemove' IntMap (Pred sym)
    h