{-# 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
, 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 :: Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq :: forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
k IntMap a
m =
case 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) -> (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)
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 = forall {k} {a}.
Ord k =>
[Map k a] -> Maybe (Map k a, (k, a), Map k a)
go (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 [] = forall a. Maybe a
Nothing
go [Map k a
m] =
case 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 -> forall a. Maybe a
Nothing
Just ((k, a)
p, Map k a
h) -> forall a. a -> Maybe a
Just (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 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
lforall a. a -> [a] -> [a]
:[Map k a]
h)
Just ((k, a)
p, Map k a
m') | forall k a. Map k a -> Bool
Map.null Map k a
m' -> forall a. a -> Maybe a
Just (Map k a
l, (k, a)
p, 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 -> forall a. a -> Maybe a
Just (Map k a
l, (k, a)
p, forall (f :: Type -> Type) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (Map k a
m'forall a. a -> [a] -> [a]
:[Map k a]
h))
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 forall a. Eq a => a -> a -> Bool
== p
q = forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
stripDuplicatePreds ((Integer
l,p
p)forall a. a -> [a] -> [a]
:[(Integer, p)]
r)
| Bool
otherwise = (Integer
l,p
p)forall a. a -> [a] -> [a]
:forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
stripDuplicatePreds ((Integer
h,p
q)forall a. a -> [a] -> [a]
:[(Integer, p)]
r)
stripDuplicatePreds [(Integer, p)
p] = [(Integer, p)
p]
stripDuplicatePreds [] = []
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)
}
size :: UnaryBV p n -> Int
size :: forall p (n :: Nat). UnaryBV p n -> Int
size UnaryBV p n
x = forall k a. Map k a -> Int
Map.size (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. Traversal (UnaryBV p n) (UnaryBV q n) p q
traversePreds p -> f q
f (UnaryBV NatRepr n
w IntMap p
m) = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 :: 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 <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p a
x) (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p b
y)
if forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p a
x forall a. Eq a => a -> a -> Bool
== forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p b
y then
forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
else
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 = forall a. Maybe a -> Bool
isJust (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 = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' forall {a} {a}. (Hashable a, Hashable a) => Int -> a -> a -> Int
go Int
s0 (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 = forall a. Hashable a => Int -> a -> Int
hashWithSalt (forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s a
k) a
e
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 = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w (forall k a. k -> a -> Map k a
Map.singleton Integer
v' (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym))
where v' :: Integer
v' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
v
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
| forall p (n :: Nat). UnaryBV p n -> Int
size UnaryBV (p BaseBoolType) w
x forall a. Eq a => a -> a -> Bool
== Int
1, [(Integer
v,p BaseBoolType
_)] <- forall k a. Map k a -> [(k, a)]
Map.toList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (p BaseBoolType) w
x) = forall a. a -> Maybe a
Just Integer
v
| Bool
otherwise = forall a. Maybe a
Nothing
unsignedRanges :: UnaryBV p n
-> [(p, Integer, Integer)]
unsignedRanges :: forall p (n :: Nat). UnaryBV p n -> [(p, Integer, Integer)]
unsignedRanges UnaryBV p n
v =
case forall k a. Map k a -> [(k, a)]
Map.toList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
v) of
[] -> forall a. HasCallStack => [Char] -> a
error [Char]
"internal: unsignedRanges given illegal UnaryBV"
[(Integer, p)]
l -> forall p. [(Integer, p)] -> [(p, Integer, Integer)]
go [(Integer, p)]
l
where w :: Integer
w :: Integer
w = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (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
hforall 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,forall p. [(Integer, p)] -> Integer
next [(Integer, p)]
rest) forall a. a -> [a] -> [a]
: 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 = forall k a. Map k a -> [(k, a)]
Map.toList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
b)
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 = forall (m :: Type -> Type) p.
Monad m =>
(p -> m Bool) -> IntMap p -> Integer -> m Integer
go p -> m Bool
f0 (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
u) (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (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 forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
splitEntry IntMap p
m of
Maybe (IntMap p, (Integer, p), IntMap p)
Nothing -> 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
Bool
True -> 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
Bool
False -> 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
sym_evaluate :: (Applicative m, Monad m)
=> (Integer -> m r)
-> (p -> r -> r -> m r)
-> UnaryBV p n
-> 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 = 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 (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
u) (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (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 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
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ p -> r -> r -> m r
ite p
v forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> 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
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 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (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 = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p w
u
, unaryBVMap :: Map Integer q
unaryBVMap = forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(Integer, q)]
l
}
where l :: [(Integer, q)]
l = forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
stripDuplicatePreds (forall k a. Map k a -> [(k, a)]
Map.toList Map Integer q
m)
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 = forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
BVD.fromAscEltList (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p n
u) (IntMap p -> [Integer]
go (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 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
Just Bool
True -> Integer
kforall a. a -> [a] -> [a]
:IntMap p -> [Integer]
go IntMap p
l
Just Bool
False -> IntMap p -> [Integer]
go IntMap p
h
Maybe Bool
Nothing -> IntMap p -> [Integer]
go IntMap p
l forall a. [a] -> [a] -> [a]
++ (Integer
kforall a. a -> [a] -> [a]
:IntMap p -> [Integer]
go IntMap p
h)
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 forall k a. Map k a
Map.empty (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) (forall k a. Map k a -> [(k, a)]
Map.toList IntMap (Pred sym)
x)
(forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
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))
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)]
_ | seq :: forall a b. a -> b -> b
seq IntMap (Pred sym)
m forall a b. (a -> b) -> a -> b
$ Bool
False = 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 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 (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 (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 (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
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 (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
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` 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 (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
_ [] =
forall (m :: Type -> Type) a. Monad m => a -> m a
return Map k a
m
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 = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
x)) forall a b. (a -> b) -> a -> b
$
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
(forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c)
(forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x)
(forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
y)
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) = forall k a. Map k a -> (k, a)
Map.findMin (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x0)
in forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> Integer
-> Pred sym
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (Pred sym)
go sym
sym0 (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym0) Integer
x_k Pred sym
x_p (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x0) (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) <- 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 forall a. Eq a => a -> a -> Bool
== Integer
y_k of
Bool
False -> do
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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) forall a b. (a, b) -> b
snd (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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) forall a b. (a, b) -> b
snd (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 <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
x_lt
Pred sym
y_is_eq <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
y_p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
y_lt
Pred sym
r' <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
r forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGE (Integer
x_kforall a. Num a => a -> a -> a
+Integer
1) IntMap (Pred sym)
x of
Just (Integer
x_k', Pred sym
x_p') -> 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 -> 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)
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return Pred sym
r
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
| forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
y = forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
| Bool
otherwise = Pred sym -> Integer -> IO (Pred sym)
go (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) Integer
0
where go :: Pred sym
-> Integer
-> IO (Pred sym)
go :: Pred sym -> Integer -> IO (Pred sym)
go Pred sym
r Integer
min_x
| Just (Integer
x_k, Pred sym
_) <- forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGE Integer
min_x IntMap (Pred sym)
x
, Just (Integer
y_k, Pred sym
_) <- forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGT Integer
x_k IntMap (Pred sym)
y
, Just (Integer
x_k_max, Pred sym
x_p) <- forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT Integer
y_k IntMap (Pred sym)
x = do
Pred sym
x_and_y_lt_x_k <-
case 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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pred sym
x_p
Just (Integer
_,Pred sym
y_lt_y_k) -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
y_lt_y_k
Pred sym
r' <- 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_maxforall a. Num a => a -> a -> a
+Integer
1)
go Pred sym
r Integer
_ = forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym (forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
y)) Pred sym
r
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 = forall sym.
IsExprBuilder sym =>
sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
compareLt sym
sym (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x) (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
y)
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 = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
x)
let (IntMap (Pred sym)
x_pos,IntMap (Pred sym)
x_neg) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
mid (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x)
let (IntMap (Pred sym)
y_pos,IntMap (Pred sym)
y_neg) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
mid (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
y)
Pred sym
x_is_neg <-
if forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
x_pos then
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym
else
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
x_pos))
Pred sym
pos_case <- 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 <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_is_neg forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
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 = forall a. HasCallStack => Bool -> a -> a
assert (Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
v Bool -> Bool -> Bool
&& Integer
v forall a. Ord a => a -> a -> Bool
<= Integer
limit) forall a b. (a -> b) -> a -> b
$
forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
overflow_limit (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
x)
where limit :: Integer
limit = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p n
x)
overflow_limit :: Integer
overflow_limit = Integer
limit forall a. Num a => a -> a -> a
- Integer
v
completeList :: IsExprBuilder sym
=> sym
-> IntMap (Pred sym)
-> (Integer -> Integer)
-> (Pred sym -> IO (Pred sym))
-> 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 = 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 <- 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
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 (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 = 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) = 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 <- 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 forall a. Num a => a -> a -> a
+) (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_leq) IntMap (Pred sym)
y_low
case forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
y_high of
Bool
True -> forall (m :: Type -> Type) a. Monad m => a -> m a
return IntMap (Pred sym)
m1
Bool
False -> do
let x_off :: Integer
x_off = Integer
x_valforall a. Num a => a -> a -> a
-Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
w
Pred sym
x_eq <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_leq forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
x_lt
Pred sym
p <-
case forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
y_low of
Bool
True -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pred sym
x_eq
Bool
False -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_eq forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
y_low))
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 forall a. Num a => a -> a -> a
+) (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p) IntMap (Pred sym)
y_high
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 forall k a. Map k a
Map.empty (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) (forall (n :: Nat) p. (1 <= n) => UnaryBV p n -> [(Integer, p)]
unsignedEntries UnaryBV (Pred sym) n
x)
where w :: NatRepr n
w = 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
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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 <- 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
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
| forall k a. Map k a -> Bool
Map.null (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x) = forall a. HasCallStack => [Char] -> a
error [Char]
"Illegal unary value"
| Bool
otherwise =
case forall k a. Map k a -> ((k, a), Map k a)
Map.deleteFindMin (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x) of
((Integer
0,Pred sym
_), Map Integer (Pred sym)
m) | forall k a. Map k a -> Bool
Map.null Map Integer (Pred sym)
m -> forall (m :: Type -> Type) a. Monad m => a -> m a
return UnaryBV (Pred sym) n
x
((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 (forall k a. Map k a -> [(k, a)]
Map.toDescList Map Integer (Pred sym)
m)
((Integer, Pred sym), Map Integer (Pred sym))
_ -> [(Integer, Pred sym)]
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go [] (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) (forall k a. Map k a -> [(k, a)]
Map.toDescList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x))
where w :: NatRepr n
w = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
x
go :: [(Integer, Pred sym)]
-> Pred sym
-> [(Integer, Pred sym)]
-> 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)]
_)) = seq :: forall a b. a -> b -> b
seq [(Integer, Pred sym)]
m forall a b. (a -> b) -> a -> b
$ do
let z_k :: Integer
z_k = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (forall a. Num a => a -> a
negate Integer
x_k)
Pred sym
q <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 forall a. a -> [a] -> [a]
: [(Integer, Pred sym)]
m
seq :: forall a b. a -> b -> b
seq Integer
z_k forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq (Integer, Pred sym)
pair forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq [(Integer, Pred sym)]
m' 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
_)] = seq :: forall a b. a -> b -> b
seq [(Integer, Pred sym)]
m forall a b. (a -> b) -> a -> b
$ do
let z_k :: Integer
z_k = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (forall a. Num a => a -> a
negate Integer
x_k)
let q :: Pred sym
q = forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w (forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList (forall a. [a] -> [a]
reverse ((Integer
z_k,Pred sym
q) forall a. a -> [a] -> [a]
: [(Integer, Pred sym)]
m)))
go [(Integer, Pred sym)]
_ Pred sym
_ [] = forall a. HasCallStack => [Char] -> a
error [Char]
"Illegal value return in UnaryBV.neg"
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' = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr r
w' (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p u
x)
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' = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr r
w' (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Integer p
neg_entries Map Integer p
l)
where w :: NatRepr u
w = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p u
x
mid :: Integer
mid = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr u
w
(Map Integer p
l,Map Integer p
h) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
mid (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p u
x)
diff :: Integer
diff = Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr r
w' forall a. Num a => a -> a -> a
- Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr u
w
neg_entries :: Map Integer p
neg_entries = forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (forall a. Num a => a -> a -> a
+ Integer
diff) Map Integer p
h
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 <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr u
w (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) r
x) = forall (m :: Type -> Type) a. Monad m => a -> m a
return UnaryBV (Pred sym) r
x
| Bool
otherwise = IntMap (Pred sym)
-> Pred sym -> IntMap (Pred sym) -> IO (UnaryBV (Pred sym) u)
go forall k a. Map k a
Map.empty (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
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
| forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
remaining =
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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
_) = forall k a. Map k a -> (k, a)
Map.findMin IntMap (Pred sym)
remaining
let base :: Integer
base = Integer
k forall a. Bits a => a -> a -> a
`xor` (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr u
w)
let next :: Integer
next = Integer
base forall a. Num a => a -> a -> a
+ forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr u
w
let (IntMap (Pred sym)
l,IntMap (Pred sym)
h) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
next IntMap (Pred sym)
remaining
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
l)) forall a b. (a -> b) -> a -> b
$ do
IntMap (Pred sym)
result' <- 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 (forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w) (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) = forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
l
Pred sym
toRemove' <- 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