    {-|
    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 (void, when)
    import           Control.Monad.ST
    import           Control.Monad.State (MonadState(..), State, execState)
    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 { forall t (st :: Type -> Type) fs.
    NormCache t st fs -> ExprBuilder t st fs
    ncBuilder :: !(ExprBuilder t st fs)
                   , forall t (st :: Type -> Type) 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 :: forall t (st :: Type -> Type) fs (tp :: BaseType).
    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 a. a -> IO a
    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).
    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 a. a -> IO a
    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 :: 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 -> 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 {forall {k} (x :: k). Or x -> Bool
    unOr :: Bool}

    instance Functor Or where
      fmap :: forall a b. (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 :: forall a. a -> Or a
    pure a
    _ = Bool -> Or a
    forall {k} (x :: k). Bool -> Or x
    Or Bool
    False
      (Or Bool
    a) <*> :: forall a b. 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 . NormCache t st fs -> Expr t tp -> IO (Expr t tp)
    norm' :: 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 (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 (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 (w :: Natural).
    (1 <= w) =>
    ExprBuilder t st fs
    -> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
    forall sym (w :: Natural).
    (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)
    (Coefficient sr -> Const (BV w) (Coefficient sr))
    -> WeightedSum (Expr t) sr
    -> Const (BV w) (WeightedSum (Expr t) sr)
    forall (f1 :: BaseType -> Type) (sr :: SemiRing)
           (f2 :: Type -> Type).
    Functor f2 =>
    (Coefficient sr -> f2 (Coefficient sr))
    -> WeightedSum f1 sr -> f2 (WeightedSum f1 sr)
    WSum.sumOffset) IO (Expr t tp) -> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
    forall a b. IO a -> (a -> IO b) -> IO b
    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 =
                       (Expr t BaseBoolType -> 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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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 a b. IO a -> (a -> IO b) -> IO b
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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 a b. IO a -> (a -> IO b) -> IO b
    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 tp1 -> Maybe (App (Expr t) tp1)
    forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
    asApp -> Just (BaseIte BaseTypeRepr tp1
    _ Integer
    _ Expr t BaseBoolType
    x_c Expr t tp1
    x_t Expr t tp1
    x_f)) Expr t tp1
    y -> do
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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 tp1
    x_t SymBV (ExprBuilder t st fs) w
    Expr t tp1
    y
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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 tp1
    x_f SymBV (ExprBuilder t st fs) w
    Expr t tp1
    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)
    Expr t BaseBoolType
    x_c Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    z_t Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    z_f
        BaseEq (BaseBVRepr NatRepr w
    _w) Expr t tp1
    x (Expr t tp1 -> Maybe (App (Expr t) tp1)
    forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
    asApp -> Just (BaseIte BaseTypeRepr tp1
    _ Integer
    _ Expr t BaseBoolType
    y_c Expr t tp1
    y_t Expr t tp1
    y_f)) -> do
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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 tp1
    x SymBV (ExprBuilder t st fs) w
    Expr t tp1
    y_t
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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 tp1
    x SymBV (ExprBuilder t st fs) w
    Expr t tp1
    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)
    Expr t BaseBoolType
    y_c Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    z_t Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    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
    _ Expr t BaseBoolType
    x_c Expr t (BaseBVType w)
    x_t Expr t (BaseBVType w)
    x_f)) Expr t (BaseBVType w)
    y -> do
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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)
    Expr t BaseBoolType
    x_c Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    z_t Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    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
    _ Expr t BaseBoolType
    y_c Expr t (BaseBVType w)
    y_t Expr t (BaseBVType w)
    y_f)) -> do
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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
          Expr t BaseBoolType
    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 (w :: Natural).
    (1 <= w) =>
    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 :: Natural).
    (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)
    Expr t BaseBoolType
    y_c Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    z_t Pred (ExprBuilder t st fs)
    Expr t BaseBoolType
    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 a. a -> IO a
    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))
    -> forall (x :: BaseType).
       NonceApp t (Expr t) x -> IO (NonceApp t (Expr t) x)
    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)
    forall (f :: BaseType -> Type) (g :: BaseType -> Type)
           (m :: Type -> Type).
    Applicative m =>
    (forall (x :: BaseType). f x -> m (g x))
    -> forall (x :: BaseType). NonceApp t f x -> m (NonceApp 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 a. a -> IO a
    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 a. a -> IO a
    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 :: forall t (st :: Type -> Type) fs.
    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 { 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 :: forall t k (tp :: k). 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 k s (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 a. a -> StateT (Map Word64 Int) Identity a
    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' :: forall t (tp :: BaseType).
    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 a. a -> StateT (Map Word64 Int) Identity a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ()
        SemiRingLiteral{} -> () -> StateT (Map Word64 Int) Identity ()
    forall a. a -> StateT (Map Word64 Int) Identity a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ()
        StringExpr{} -> () -> StateT (Map Word64 Int) Identity ()
    forall a. a -> StateT (Map Word64 Int) Identity a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ()
        FloatExpr{} -> () -> StateT (Map Word64 Int) Identity ()
    forall a. a -> StateT (Map Word64 Int) Identity a
    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 ())
    -> forall (x :: BaseType).
       App (Expr t) x -> 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_ Expr t x -> StateT (Map Word64 Int) Identity ()
    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 ())
    -> forall (x :: BaseType).
       NonceApp t (Expr t) x -> 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_ Expr t x -> StateT (Map Word64 Int) Identity ()
    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 :: forall t (tp :: BaseType). 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 =
    -}