{-|
Module      : What4.Solver.SimpleBackend.Simplify
Description : Simplification procedure for distributing operations through if/then/else
Copyright   : (c) Galois, Inc 2016-2020
License     : BSD3
Maintainer  : Joe Hendrix <jhendrix@galois.com>

This module provides a minimalistic interface for manipulating Boolean formulas
and execution contexts in the symbolic simulator.
-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Expr.Simplify
  ( simplify
  , count_subterms
  ) where

import           Control.Lens ((^.))
import           Control.Monad.ST
import           Control.Monad.State
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe
import qualified Data.Parameterized.HashTable as PH
import           Data.Parameterized.Nonce
import           Data.Parameterized.TraversableFC
import           Data.Word

import           What4.Interface
import qualified What4.SemiRing as SR
import           What4.Expr.Builder
import qualified What4.Expr.WeightedSum as WSum

------------------------------------------------------------------------
-- simplify

data NormCache t st fs
   = NormCache { NormCache t st fs -> ExprBuilder t st fs
ncBuilder :: !(ExprBuilder t st fs)
               , NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
ncTable :: !(PH.HashTable RealWorld (Expr t) (Expr t))
               }

norm :: NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm :: NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
c Expr t tp
e = do
  Maybe (Expr t tp)
mr <- ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp)))
-> ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (Expr t) (Expr t)
-> Expr t tp -> ST RealWorld (Maybe (Expr t tp))
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup (NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
forall t (st :: Type -> Type) fs.
NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
ncTable NormCache t st fs
c) Expr t tp
e
  case Maybe (Expr t tp)
mr of
    Just Expr t tp
r -> Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
r
    Maybe (Expr t tp)
Nothing -> do
      Expr t tp
r <- NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
HashableF (Expr t) =>
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm' NormCache t st fs
c Expr t tp
e
      ST RealWorld () -> IO ()
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld () -> IO ()) -> ST RealWorld () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (Expr t) (Expr t)
-> Expr t tp -> Expr t tp -> ST RealWorld ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert (NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
forall t (st :: Type -> Type) fs.
NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
ncTable NormCache t st fs
c) Expr t tp
e Expr t tp
r
      Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
r

bvIteDist :: (BoolExpr t -> r -> r -> IO r)
          -> Expr t i
          -> (Expr t i -> IO r)
          -> IO r
bvIteDist :: (BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist BoolExpr t -> r -> r -> IO r
muxFn (Expr t i -> Maybe (App (Expr t) i)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr i
_ Integer
_ BoolExpr t
c Expr t i
t Expr t i
f)) Expr t i -> IO r
atomFn = do
  r
t' <- (BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
forall t r (i :: BaseType).
(BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist BoolExpr t -> r -> r -> IO r
muxFn Expr t i
t Expr t i -> IO r
atomFn
  r
f' <- (BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
forall t r (i :: BaseType).
(BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist BoolExpr t -> r -> r -> IO r
muxFn Expr t i
f Expr t i -> IO r
atomFn
  BoolExpr t -> r -> r -> IO r
muxFn BoolExpr t
c r
t' r
f'
bvIteDist BoolExpr t -> r -> r -> IO r
_ Expr t i
u Expr t i -> IO r
atomFn = Expr t i -> IO r
atomFn Expr t i
u

newtype Or x = Or {Or x -> Bool
unOr :: Bool}

instance Functor Or where
  fmap :: (a -> b) -> Or a -> Or b
fmap a -> b
_f (Or Bool
b) = (Bool -> Or b
forall k (x :: k). Bool -> Or x
Or Bool
b)
instance Applicative Or where
  pure :: a -> Or a
pure a
_ = Bool -> Or a
forall k (x :: k). Bool -> Or x
Or Bool
False
  (Or Bool
a) <*> :: Or (a -> b) -> Or a -> Or b
<*> (Or Bool
b) = Bool -> Or b
forall k (x :: k). Bool -> Or x
Or (Bool
a Bool -> Bool -> Bool
|| Bool
b)

norm' :: forall t st fs tp . PH.HashableF (Expr t) => NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm' :: NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm' NormCache t st fs
nc (AppExpr AppExpr t tp
a0) = do
  let sb :: ExprBuilder t st fs
sb = NormCache t st fs -> ExprBuilder t st fs
forall t (st :: Type -> Type) fs.
NormCache t st fs -> ExprBuilder t st fs
ncBuilder NormCache t st fs
nc
  case AppExpr t tp -> App (Expr t) tp
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
a0 of
    SemiRingSum WeightedSum (Expr t) sr
s
      | let sr :: SemiRingRepr sr
sr = WeightedSum (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
s
      , SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVArithRepr NatRepr w
w <- SemiRingRepr sr
sr
      , Or (WeightedSum (Expr t) sr) -> Bool
forall k (x :: k). Or x -> Bool
unOr ((Expr t (SemiRingBase sr) -> Or (Expr t (SemiRingBase sr)))
-> WeightedSum (Expr t) sr -> Or (WeightedSum (Expr t) sr)
forall (k :: BaseType -> Type) (j :: BaseType -> Type)
       (m :: Type -> Type) (sr :: SemiRing).
(Applicative m, Tm k) =>
(j (SemiRingBase sr) -> m (k (SemiRingBase sr)))
-> WeightedSum j sr -> m (WeightedSum k sr)
WSum.traverseVars @(Expr t) (\Expr t (SemiRingBase sr)
x -> Bool -> Or (Expr t (BaseBVType w))
forall k (x :: k). Bool -> Or x
Or (Expr t (BaseBVType w) -> Integer
forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t (BaseBVType w)
Expr t (SemiRingBase sr)
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
1)) WeightedSum (Expr t) sr
s)
      -> do let tms :: [(BV w, Expr t (BaseBVType w))]
tms = ([(BV w, Expr t (BaseBVType w))]
 -> [(BV w, Expr t (BaseBVType w))]
 -> [(BV w, Expr t (BaseBVType w))])
-> (Coefficient sr
    -> Expr t (SemiRingBase sr) -> [(BV w, Expr t (BaseBVType w))])
-> (Coefficient sr -> [(BV w, Expr t (BaseBVType w))])
-> WeightedSum (Expr t) sr
-> [(BV w, Expr t (BaseBVType w))]
forall r (sr :: SemiRing) (f :: BaseType -> Type).
(r -> r -> r)
-> (Coefficient sr -> f (SemiRingBase sr) -> r)
-> (Coefficient sr -> r)
-> WeightedSum f sr
-> r
WSum.eval [(BV w, Expr t (BaseBVType w))]
-> [(BV w, Expr t (BaseBVType w))]
-> [(BV w, Expr t (BaseBVType w))]
forall a. [a] -> [a] -> [a]
(++) (\Coefficient sr
c Expr t (SemiRingBase sr)
x -> [(BV w
Coefficient sr
c,Expr t (BaseBVType w)
Expr t (SemiRingBase sr)
x)]) ([(BV w, Expr t (BaseBVType w))]
-> BV w -> [(BV w, Expr t (BaseBVType w))]
forall a b. a -> b -> a
const []) WeightedSum (Expr t) sr
s
            let f :: [(BV w, Expr t (BaseBVType w))]
-> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
f [] Expr t tp -> IO (Expr t tp)
k = ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit ExprBuilder t st fs
sb NatRepr w
w (WeightedSum (Expr t) sr
sWeightedSum (Expr t) sr
-> Getting (BV w) (WeightedSum (Expr t) sr) (BV w) -> BV w
forall s a. s -> Getting a s a -> a
^.Getting (BV w) (WeightedSum (Expr t) sr) (BV w)
forall (f :: BaseType -> Type) (sr :: SemiRing).
Lens' (WeightedSum f sr) (Coefficient sr)
WSum.sumOffset) IO (Expr t tp) -> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr t tp -> IO (Expr t tp)
k
                f ((BV w
c,Expr t (BaseBVType w)
x):[(BV w, Expr t (BaseBVType w))]
xs) Expr t tp -> IO (Expr t tp)
k =
                   (BoolExpr t -> Expr t tp -> Expr t tp -> IO (Expr t tp))
-> Expr t (BaseBVType w)
-> (Expr t (BaseBVType w) -> IO (Expr t tp))
-> IO (Expr t tp)
forall t r (i :: BaseType).
(BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte ExprBuilder t st fs
sb) Expr t (BaseBVType w)
x ((Expr t (BaseBVType w) -> IO (Expr t tp)) -> IO (Expr t tp))
-> (Expr t (BaseBVType w) -> IO (Expr t tp)) -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$ \Expr t (BaseBVType w)
x' ->
                   ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sb SemiRingRepr sr
sr BV w
Coefficient sr
c Expr t (BaseBVType w)
Expr t (SemiRingBase sr)
x' IO (Expr t (BaseBVType w))
-> (Expr t (BaseBVType w) -> IO (Expr t tp)) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Expr t (BaseBVType w)
cx' ->
                   [(BV w, Expr t (BaseBVType w))]
-> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
f [(BV w, Expr t (BaseBVType w))]
xs ((Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp))
-> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$ \Expr t tp
xs' ->
                   ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
cx' SymBV (ExprBuilder t st fs) w
Expr t tp
xs' IO (Expr t tp) -> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr t tp -> IO (Expr t tp)
k
            [(BV w, Expr t (BaseBVType w))]
-> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
f [(BV w, Expr t (BaseBVType w))]
tms (NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc)

    BaseEq (BaseBVRepr NatRepr w
_w) (Expr t tp -> Maybe (App (Expr t) tp)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr tp
_ Integer
_ BoolExpr t
x_c Expr t tp
x_t Expr t tp
x_f)) Expr t tp
y -> do
      BoolExpr t
z_t <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t tp
x_t SymBV (ExprBuilder t st fs) w
Expr t tp
y
      BoolExpr t
z_f <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t tp
x_f SymBV (ExprBuilder t st fs) w
Expr t tp
y
      NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Pred (ExprBuilder t st fs)
BoolExpr t
x_c Pred (ExprBuilder t st fs)
BoolExpr t
z_t Pred (ExprBuilder t st fs)
BoolExpr t
z_f
    BaseEq (BaseBVRepr NatRepr w
_w) Expr t tp
x (Expr t tp -> Maybe (App (Expr t) tp)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr tp
_ Integer
_ BoolExpr t
y_c Expr t tp
y_t Expr t tp
y_f)) -> do
      BoolExpr t
z_t <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t tp
x SymBV (ExprBuilder t st fs) w
Expr t tp
y_t
      BoolExpr t
z_f <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t tp
x SymBV (ExprBuilder t st fs) w
Expr t tp
y_f
      NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Pred (ExprBuilder t st fs)
BoolExpr t
y_c Pred (ExprBuilder t st fs)
BoolExpr t
z_t Pred (ExprBuilder t st fs)
BoolExpr t
z_f
    BVSlt (Expr t (BaseBVType w) -> Maybe (App (Expr t) (BaseBVType w))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr (BaseBVType w)
_ Integer
_ BoolExpr t
x_c Expr t (BaseBVType w)
x_t Expr t (BaseBVType w)
x_f)) Expr t (BaseBVType w)
y -> do
      BoolExpr t
z_t <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
x_t SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
y
      BoolExpr t
z_f <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
x_f SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
y
      NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Pred (ExprBuilder t st fs)
BoolExpr t
x_c Pred (ExprBuilder t st fs)
BoolExpr t
z_t Pred (ExprBuilder t st fs)
BoolExpr t
z_f
    BVSlt Expr t (BaseBVType w)
x (Expr t (BaseBVType w) -> Maybe (App (Expr t) (BaseBVType w))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr (BaseBVType w)
_ Integer
_ BoolExpr t
y_c Expr t (BaseBVType w)
y_t Expr t (BaseBVType w)
y_f)) -> do
      BoolExpr t
z_t <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
x SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
y_t
      BoolExpr t
z_f <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
x SymBV (ExprBuilder t st fs) w
Expr t (BaseBVType w)
y_f
      NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Pred (ExprBuilder t st fs)
BoolExpr t
y_c Pred (ExprBuilder t st fs)
BoolExpr t
z_t Pred (ExprBuilder t st fs)
BoolExpr t
z_f
    App (Expr t) tp
app -> do
      App (Expr t) tp
app' <- (forall (tp :: BaseType). Expr t tp -> IO (Expr t tp))
-> App (Expr t) tp -> IO (App (Expr t) tp)
forall (m :: Type -> Type) (f :: BaseType -> Type)
       (e :: BaseType -> Type) (utp :: BaseType).
(Applicative m, OrdF f, Eq (f BaseBoolType), HashableF f,
 HasAbsValue f) =>
(forall (tp :: BaseType). e tp -> m (f tp))
-> App e utp -> m (App f utp)
traverseApp (NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc) App (Expr t) tp
app
      if App (Expr t) tp
app' App (Expr t) tp -> App (Expr t) tp -> Bool
forall a. Eq a => a -> a -> Bool
== App (Expr t) tp
app then
        Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AppExpr t tp -> Expr t tp
forall t (tp :: BaseType). AppExpr t tp -> Expr t tp
AppExpr AppExpr t tp
a0)
       else
        NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sb App (Expr t) tp
app'
norm' NormCache t st fs
nc (NonceAppExpr NonceAppExpr t tp
p0) = do
  let predApp :: NonceApp t (Expr t) tp
predApp = NonceAppExpr t tp -> NonceApp t (Expr t) tp
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
p0
  NonceApp t (Expr t) tp
p <- (forall (tp :: BaseType). Expr t tp -> IO (Expr t tp))
-> NonceApp t (Expr t) tp -> IO (NonceApp t (Expr t) tp)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (NormCache t st fs -> Expr t x -> IO (Expr t x)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc) NonceApp t (Expr t) tp
predApp
  if NonceApp t (Expr t) tp
p NonceApp t (Expr t) tp -> NonceApp t (Expr t) tp -> Bool
forall a. Eq a => a -> a -> Bool
== NonceApp t (Expr t) tp
predApp then
    Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t tp -> IO (Expr t tp)) -> Expr t tp -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$! NonceAppExpr t tp -> Expr t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr NonceAppExpr t tp
p0
   else
    NormCache t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp) -> IO (Expr t tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
sbNonceExpr (NormCache t st fs -> ExprBuilder t st fs
forall t (st :: Type -> Type) fs.
NormCache t st fs -> ExprBuilder t st fs
ncBuilder NormCache t st fs
nc) NonceApp t (Expr t) tp
p
norm' NormCache t st fs
_ Expr t tp
e = Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e

-- | Simplify a Boolean expression by distributing over ite.
simplify :: ExprBuilder t st fs -> BoolExpr t -> IO (BoolExpr t)
simplify :: ExprBuilder t st fs -> BoolExpr t -> IO (BoolExpr t)
simplify ExprBuilder t st fs
sb BoolExpr t
p = do
  HashTable RealWorld (Expr t) (Expr t)
tbl <- ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
-> IO (HashTable RealWorld (Expr t) (Expr t))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
 -> IO (HashTable RealWorld (Expr t) (Expr t)))
-> ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
-> IO (HashTable RealWorld (Expr t) (Expr t))
forall a b. (a -> b) -> a -> b
$ ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
forall k s (key :: k -> Type) (val :: k -> Type).
ST s (HashTable s key val)
PH.new
  let nc :: NormCache t st fs
nc = NormCache :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs
-> HashTable RealWorld (Expr t) (Expr t) -> NormCache t st fs
NormCache { ncBuilder :: ExprBuilder t st fs
ncBuilder = ExprBuilder t st fs
sb
                     , ncTable :: HashTable RealWorld (Expr t) (Expr t)
ncTable = HashTable RealWorld (Expr t) (Expr t)
tbl
                     }
  NormCache t st fs -> BoolExpr t -> IO (BoolExpr t)
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc BoolExpr t
p

------------------------------------------------------------------------
-- count_subterm

type Counter = State (Map Word64 Int)

-- | Record an element occurs, and return condition indicating if it is new.
recordExpr :: Nonce t (tp::k) -> Counter Bool
recordExpr :: Nonce t tp -> Counter Bool
recordExpr Nonce t tp
n = do
  Map Word64 Int
m <- StateT (Map Word64 Int) Identity (Map Word64 Int)
forall s (m :: Type -> Type). MonadState s m => m s
get
  let (Maybe Int
mr, Map Word64 Int
m') = (Word64 -> Int -> Int -> Int)
-> Word64 -> Int -> Map Word64 Int -> (Maybe Int, Map Word64 Int)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey (\Word64
_ -> Int -> Int -> Int
forall a. Num a => a -> a -> a
(+)) (Nonce t tp -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue Nonce t tp
n) Int
1 Map Word64 Int
m
  Map Word64 Int -> StateT (Map Word64 Int) Identity ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (Map Word64 Int -> StateT (Map Word64 Int) Identity ())
-> Map Word64 Int -> StateT (Map Word64 Int) Identity ()
forall a b. (a -> b) -> a -> b
$ Map Word64 Int
m'
  Bool -> Counter Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> Counter Bool) -> Bool -> Counter Bool
forall a b. (a -> b) -> a -> b
$! Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Int
mr

count_subterms' :: Expr t tp -> Counter ()
count_subterms' :: Expr t tp -> StateT (Map Word64 Int) Identity ()
count_subterms' Expr t tp
e0 =
  case Expr t tp
e0 of
    BoolExpr{} -> () -> StateT (Map Word64 Int) Identity ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure () 
    SemiRingLiteral{} -> () -> StateT (Map Word64 Int) Identity ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    StringExpr{} -> () -> StateT (Map Word64 Int) Identity ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    FloatExpr{} -> () -> StateT (Map Word64 Int) Identity ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    AppExpr AppExpr t tp
ae -> do
      Bool
is_new <- Nonce t tp -> Counter Bool
forall t k (tp :: k). Nonce t tp -> Counter Bool
recordExpr (AppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
ae)
      Bool
-> StateT (Map Word64 Int) Identity ()
-> StateT (Map Word64 Int) Identity ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
is_new (StateT (Map Word64 Int) Identity ()
 -> StateT (Map Word64 Int) Identity ())
-> StateT (Map Word64 Int) Identity ()
-> StateT (Map Word64 Int) Identity ()
forall a b. (a -> b) -> a -> b
$ do
        (forall (x :: BaseType).
 Expr t x -> StateT (Map Word64 Int) Identity ())
-> App (Expr t) tp -> StateT (Map Word64 Int) Identity ()
forall k l (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       (f :: k -> Type) a.
(FoldableFC t, Applicative m) =>
(forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
traverseFC_ forall t (tp :: BaseType).
Expr t tp -> StateT (Map Word64 Int) Identity ()
forall (x :: BaseType).
Expr t x -> StateT (Map Word64 Int) Identity ()
count_subterms' (AppExpr t tp -> App (Expr t) tp
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
ae)
    NonceAppExpr NonceAppExpr t tp
nae -> do
      Bool
is_new <- Nonce t tp -> Counter Bool
forall t k (tp :: k). Nonce t tp -> Counter Bool
recordExpr (NonceAppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
nae)
      Bool
-> StateT (Map Word64 Int) Identity ()
-> StateT (Map Word64 Int) Identity ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
is_new (StateT (Map Word64 Int) Identity ()
 -> StateT (Map Word64 Int) Identity ())
-> StateT (Map Word64 Int) Identity ()
-> StateT (Map Word64 Int) Identity ()
forall a b. (a -> b) -> a -> b
$ do
        (forall (x :: BaseType).
 Expr t x -> StateT (Map Word64 Int) Identity ())
-> NonceApp t (Expr t) tp -> StateT (Map Word64 Int) Identity ()
forall k l (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       (f :: k -> Type) a.
(FoldableFC t, Applicative m) =>
(forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
traverseFC_ forall t (tp :: BaseType).
Expr t tp -> StateT (Map Word64 Int) Identity ()
forall (x :: BaseType).
Expr t x -> StateT (Map Word64 Int) Identity ()
count_subterms' (NonceAppExpr t tp -> NonceApp t (Expr t) tp
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
nae)
    BoundVarExpr ExprBoundVar t tp
v -> do
      Counter Bool -> StateT (Map Word64 Int) Identity ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Counter Bool -> StateT (Map Word64 Int) Identity ())
-> Counter Bool -> StateT (Map Word64 Int) Identity ()
forall a b. (a -> b) -> a -> b
$ Nonce t tp -> Counter Bool
forall t k (tp :: k). Nonce t tp -> Counter Bool
recordExpr (ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
v)

-- | Return a map from nonce indices to the number of times an elt with that
-- nonce appears in the subterm.
count_subterms :: Expr t tp -> Map Word64 Int
count_subterms :: Expr t tp -> Map Word64 Int
count_subterms Expr t tp
e = StateT (Map Word64 Int) Identity ()
-> Map Word64 Int -> Map Word64 Int
forall s a. State s a -> s -> s
execState (Expr t tp -> StateT (Map Word64 Int) Identity ()
forall t (tp :: BaseType).
Expr t tp -> StateT (Map Word64 Int) Identity ()
count_subterms' Expr t tp
e) Map Word64 Int
forall k a. Map k a
Map.empty

{-
------------------------------------------------------------------------
-- nnf

-- | Convert formula into negation normal form.
nnf :: SimpleBuilder Expr t BoolType -> IO (Expr T BoolType)
nnf e =
-}