{-|
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 :: 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 :: 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 :: [(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 { UnaryBV p n -> NatRepr n
width :: !(NatRepr n)
             , UnaryBV p n -> IntMap p
unaryBVMap :: !(IntMap p)
             }

-- | Returns the number of distinct values that this could be.
size :: UnaryBV p n -> Int
size :: 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 :: (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)
traverse p -> f q
f IntMap p
m

instance Eq p => TestEquality (UnaryBV p) where
  testEquality :: 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 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 :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    else
      Maybe (a :~: b)
forall a. Maybe a
Nothing

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 :: sym -> NatRepr n -> Integer -> UnaryBV (Pred sym) n
constant sym
sym NatRepr n
w Integer
v = NatRepr n -> IntMap (Pred sym) -> UnaryBV (Pred sym) n
forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w (Integer -> Pred sym -> IntMap (Pred sym)
forall k a. k -> a -> Map k a
Map.singleton Integer
v' (sym -> Pred sym
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 :: 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 :: 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 :: [(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 :: [(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 :: 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 :: (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 :: (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 (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 :: (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 :: (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 (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 :: (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)
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 :: forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
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 :: (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 :: 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
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 (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 :: 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 (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 :: 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 :: 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 (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 (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 :: 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 (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 (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 :: 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 :: 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 (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 :: 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 :: 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)
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 :: 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 (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 -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
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 (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 :: 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 (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 :: 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 (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)
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)
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)
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)
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)
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 (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 :: 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 :: 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 -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^NatRepr r -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr r
w' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
2Integer -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^NatRepr u -> Natural
forall (n :: Nat). NatRepr n -> Natural
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 :: 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 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 (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 (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