{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.TermUtils
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.TermUtils
  ( extractSymbolicsTerm,
    castTerm,
    someTermsSize,
    someTermSize,
    termSize,
    termsSize,
  )
where

import Control.Monad.State
  ( MonadState (get, put),
    State,
    evalState,
    execState,
    gets,
    modify',
  )
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.Typeable
  ( Typeable,
    cast,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( SomeTypedSymbol (SomeTypedSymbol),
    SupportedPrim,
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        ApplyTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        BinaryTerm,
        ComplementBitsTerm,
        ConTerm,
        DivIntegralTerm,
        EqTerm,
        ITETerm,
        LeOrdTerm,
        LtOrdTerm,
        ModIntegralTerm,
        MulNumTerm,
        NegNumTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        QuotIntegralTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        TernaryTerm,
        ToSignedTerm,
        ToUnsignedTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TypedSymbol,
    introSupportedPrimConstraint,
  )
import Grisette.Internal.SymPrim.Prim.SomeTerm
  ( SomeTerm (SomeTerm),
  )
import qualified Type.Reflection as R

extractSymbolicsSomeTerm :: SomeTerm -> S.HashSet SomeTypedSymbol
extractSymbolicsSomeTerm :: SomeTerm -> HashSet SomeTypedSymbol
extractSymbolicsSomeTerm SomeTerm
t1 = State
  (HashMap SomeTerm (HashSet SomeTypedSymbol))
  (HashSet SomeTypedSymbol)
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> HashSet SomeTypedSymbol
forall s a. State s a -> s -> a
evalState (SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached SomeTerm
t1) HashMap SomeTerm (HashSet SomeTypedSymbol)
forall k v. HashMap k v
M.empty
  where
    gocached :: SomeTerm -> State (M.HashMap SomeTerm (S.HashSet SomeTypedSymbol)) (S.HashSet SomeTypedSymbol)
    gocached :: SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached SomeTerm
t = do
      Maybe (HashSet SomeTypedSymbol)
v <- (HashMap SomeTerm (HashSet SomeTypedSymbol)
 -> Maybe (HashSet SomeTypedSymbol))
-> StateT
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     Identity
     (Maybe (HashSet SomeTypedSymbol))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SomeTerm
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> Maybe (HashSet SomeTypedSymbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SomeTerm
t)
      case Maybe (HashSet SomeTypedSymbol)
v of
        Just HashSet SomeTypedSymbol
x -> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet SomeTypedSymbol
x
        Maybe (HashSet SomeTypedSymbol)
Nothing -> do
          HashSet SomeTypedSymbol
res <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
go SomeTerm
t
          HashMap SomeTerm (HashSet SomeTypedSymbol)
st <- StateT
  (HashMap SomeTerm (HashSet SomeTypedSymbol))
  Identity
  (HashMap SomeTerm (HashSet SomeTypedSymbol))
forall s (m :: * -> *). MonadState s m => m s
get
          HashMap SomeTerm (HashSet SomeTypedSymbol)
-> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (HashMap SomeTerm (HashSet SomeTypedSymbol)
 -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity ())
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity ()
forall a b. (a -> b) -> a -> b
$ SomeTerm
-> HashSet SomeTypedSymbol
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
-> HashMap SomeTerm (HashSet SomeTypedSymbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTerm
t HashSet SomeTypedSymbol
res HashMap SomeTerm (HashSet SomeTypedSymbol)
st
          HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet SomeTypedSymbol
res
    go :: SomeTerm -> State (M.HashMap SomeTerm (S.HashSet SomeTypedSymbol)) (S.HashSet SomeTypedSymbol)
    go :: SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
go (SomeTerm ConTerm {}) = HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet SomeTypedSymbol
forall a. HashSet a
S.empty
    go (SomeTerm (SymTerm Id
_ (TypedSymbol a
sym :: TypedSymbol a))) = HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet SomeTypedSymbol
 -> State
      (HashMap SomeTerm (HashSet SomeTypedSymbol))
      (HashSet SomeTypedSymbol))
-> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Hashable a => a -> HashSet a
S.singleton (SomeTypedSymbol -> HashSet SomeTypedSymbol)
-> SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a b. (a -> b) -> a -> b
$ TypeRep a -> TypedSymbol a -> SomeTypedSymbol
forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
SomeTypedSymbol (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) TypedSymbol a
sym
    go (SomeTerm (UnaryTerm Id
_ tag
_ Term arg
arg)) = Term arg
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term arg
arg
    go (SomeTerm (BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2)) = Term arg1
-> Term arg2
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term arg1
arg1 Term arg2
arg2
    go (SomeTerm (TernaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2 Term arg3
arg3)) = Term arg1
-> Term arg2
-> Term arg3
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a} {a}.
(SupportedPrim a, SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goTernary Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
    go (SomeTerm (NotTerm Id
_ Term Bool
arg)) = Term Bool
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term Bool
arg
    go (SomeTerm (OrTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = Term Bool
-> Term Bool
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term Bool
arg1 Term Bool
arg2
    go (SomeTerm (AndTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = Term Bool
-> Term Bool
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term Bool
arg1 Term Bool
arg2
    go (SomeTerm (EqTerm Id
_ Term t1
arg1 Term t1
arg2)) = Term t1
-> Term t1
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (ITETerm Id
_ Term Bool
cond Term a
arg1 Term a
arg2)) = Term Bool
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a} {a}.
(SupportedPrim a, SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goTernary Term Bool
cond Term a
arg1 Term a
arg2
    go (SomeTerm (AddNumTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (NegNumTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (MulNumTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (AbsNumTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (SignumNumTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (LtOrdTerm Id
_ Term t1
arg1 Term t1
arg2)) = Term t1
-> Term t1
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (LeOrdTerm Id
_ Term t1
arg1 Term t1
arg2)) = Term t1
-> Term t1
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term t1
arg1 Term t1
arg2
    go (SomeTerm (AndBitsTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (OrBitsTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (XorBitsTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (ComplementBitsTerm Id
_ Term a
arg)) = Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (ShiftLeftTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (ShiftRightTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (RotateLeftTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (RotateRightTerm Id
_ Term a
arg Term a
n1)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg Term a
n1
    go (SomeTerm (ToSignedTerm Id
_ Term (u n)
arg)) = Term (u n)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (u n)
arg
    go (SomeTerm (ToUnsignedTerm Id
_ Term (s n)
arg)) = Term (s n)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (s n)
arg
    go (SomeTerm (BVConcatTerm Id
_ Term (bv l)
arg1 Term (bv r)
arg2)) = Term (bv l)
-> Term (bv r)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term (bv l)
arg1 Term (bv r)
arg2
    go (SomeTerm (BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv n)
arg)) = Term (bv n)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (bv n)
arg
    go (SomeTerm (BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg)) = Term (bv l)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (bv l)
arg
    go (SomeTerm (ApplyTerm Id
_ Term f
func Term a
arg)) = Term f
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term f
func Term a
arg
    go (SomeTerm (DivIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (ModIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (QuotIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    go (SomeTerm (RemIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a} {a}.
(SupportedPrim a, SupportedPrim a) =>
Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2
    goUnary :: Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg = SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg)
    goBinary :: Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goBinary Term a
arg1 Term a
arg2 = do
      HashSet SomeTypedSymbol
r1 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg1)
      HashSet SomeTypedSymbol
r2 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg2)
      HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet SomeTypedSymbol
 -> State
      (HashMap SomeTerm (HashSet SomeTypedSymbol))
      (HashSet SomeTypedSymbol))
-> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
r1 HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Semigroup a => a -> a -> a
<> HashSet SomeTypedSymbol
r2
    goTernary :: Term a
-> Term a
-> Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goTernary Term a
arg1 Term a
arg2 Term a
arg3 = do
      HashSet SomeTypedSymbol
r1 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg1)
      HashSet SomeTypedSymbol
r2 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg2)
      HashSet SomeTypedSymbol
r3 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg3)
      HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a.
a -> StateT (HashMap SomeTerm (HashSet SomeTypedSymbol)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet SomeTypedSymbol
 -> State
      (HashMap SomeTerm (HashSet SomeTypedSymbol))
      (HashSet SomeTypedSymbol))
-> HashSet SomeTypedSymbol
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
r1 HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Semigroup a => a -> a -> a
<> HashSet SomeTypedSymbol
r2 HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Semigroup a => a -> a -> a
<> HashSet SomeTypedSymbol
r3
{-# INLINEABLE extractSymbolicsSomeTerm #-}

extractSymbolicsTerm :: (SupportedPrim a) => Term a -> S.HashSet SomeTypedSymbol
extractSymbolicsTerm :: forall a. SupportedPrim a => Term a -> HashSet SomeTypedSymbol
extractSymbolicsTerm Term a
t = SomeTerm -> HashSet SomeTypedSymbol
extractSymbolicsSomeTerm (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t)
{-# INLINE extractSymbolicsTerm #-}

castTerm :: forall a b. (Typeable b) => Term a -> Maybe (Term b)
castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm t :: Term a
t@ConTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@SymTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@UnaryTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BinaryTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TernaryTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@NotTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@OrTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AndTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@EqTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ITETerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AddNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@NegNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@MulNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AbsNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@SignumNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@LtOrdTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@LeOrdTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AndBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@OrBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@XorBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ComplementBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ShiftLeftTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ShiftRightTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RotateLeftTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RotateRightTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ToSignedTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ToUnsignedTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVConcatTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVSelectTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVExtendTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ApplyTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@DivIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ModIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@QuotIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RemIntegralTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
{-# INLINE castTerm #-}

someTermsSize :: [SomeTerm] -> Int
someTermsSize :: [SomeTerm] -> Id
someTermsSize [SomeTerm]
terms = HashSet SomeTerm -> Id
forall a. HashSet a -> Id
S.size (HashSet SomeTerm -> Id) -> HashSet SomeTerm -> Id
forall a b. (a -> b) -> a -> b
$ State (HashSet SomeTerm) [()]
-> HashSet SomeTerm -> HashSet SomeTerm
forall s a. State s a -> s -> s
execState ((SomeTerm -> StateT (HashSet SomeTerm) Identity ())
-> [SomeTerm] -> State (HashSet SomeTerm) [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse SomeTerm -> StateT (HashSet SomeTerm) Identity ()
goSome [SomeTerm]
terms) HashSet SomeTerm
forall a. HashSet a
S.empty
  where
    exists :: Term a -> m Bool
exists Term a
t = (HashSet SomeTerm -> Bool) -> m Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SomeTerm -> HashSet SomeTerm -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
    add :: Term a -> m ()
add Term a
t = (HashSet SomeTerm -> HashSet SomeTerm) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (SomeTerm -> HashSet SomeTerm -> HashSet SomeTerm
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
    goSome :: SomeTerm -> State (S.HashSet SomeTerm) ()
    goSome :: SomeTerm -> StateT (HashSet SomeTerm) Identity ()
goSome (SomeTerm Term a
b) = Term a -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term a
b
    go :: forall b. Term b -> State (S.HashSet SomeTerm) ()
    go :: forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go t :: Term b
t@ConTerm {} = Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
    go t :: Term b
t@SymTerm {} = Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
    go t :: Term b
t@(UnaryTerm Id
_ tag
_ Term arg
arg) = Term b -> Term arg -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term arg
arg
    go t :: Term b
t@(BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2) = Term b
-> Term arg1 -> Term arg2 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term arg1
arg1 Term arg2
arg2
    go t :: Term b
t@(TernaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = Term b
-> Term arg1
-> Term arg2
-> Term arg3
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
    go t :: Term b
t@(NotTerm Id
_ Term Bool
arg) = Term b -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term Bool
arg
    go t :: Term b
t@(OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = Term b
-> Term Bool -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
    go t :: Term b
t@(AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = Term b
-> Term Bool -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
    go t :: Term b
t@(EqTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(ITETerm Id
_ Term Bool
cond Term b
arg1 Term b
arg2) = Term b
-> Term Bool
-> Term b
-> Term b
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term Bool
cond Term b
arg1 Term b
arg2
    go t :: Term b
t@(AddNumTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(NegNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(MulNumTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(AbsNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(SignumNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(LtOrdTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(LeOrdTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(AndBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(OrBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(XorBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(ComplementBitsTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(ShiftLeftTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(ShiftRightTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(RotateLeftTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(RotateRightTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
    go t :: Term b
t@(ToSignedTerm Id
_ Term (u n)
arg) = Term b -> Term (u n) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (u n)
arg
    go t :: Term b
t@(ToUnsignedTerm Id
_ Term (s n)
arg) = Term b -> Term (s n) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (s n)
arg
    go t :: Term b
t@(BVConcatTerm Id
_ Term (bv l)
arg1 Term (bv r)
arg2) = Term b
-> Term (bv l)
-> Term (bv r)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term (bv l)
arg1 Term (bv r)
arg2
    go t :: Term b
t@(BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv n)
arg) = Term b -> Term (bv n) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv n)
arg
    go t :: Term b
t@(BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg) = Term b -> Term (bv l) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv l)
arg
    go t :: Term b
t@(ApplyTerm Id
_ Term f
func Term a
arg) = Term b -> Term f -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term f
func Term a
arg
    go t :: Term b
t@(DivIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(ModIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(QuotIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(RemIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
    goUnary :: forall a b. (SupportedPrim a) => Term a -> Term b -> State (S.HashSet SomeTerm) ()
    goUnary :: forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term a
t Term b
arg = do
      Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg
    goBinary ::
      forall a b c.
      (SupportedPrim a, SupportedPrim b) =>
      Term a ->
      Term b ->
      Term c ->
      State (S.HashSet SomeTerm) ()
    goBinary :: forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term a
t Term b
arg1 Term c
arg2 = do
      Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg1
          Term c -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term c
arg2
    goTernary ::
      forall a b c d.
      (SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
      Term a ->
      Term b ->
      Term c ->
      Term d ->
      State (S.HashSet SomeTerm) ()
    goTernary :: forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term a
t Term b
arg1 Term c
arg2 Term d
arg3 = do
      Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg1
          Term c -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term c
arg2
          Term d -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term d
arg3
{-# INLINEABLE someTermsSize #-}

someTermSize :: SomeTerm -> Int
someTermSize :: SomeTerm -> Id
someTermSize SomeTerm
term = [SomeTerm] -> Id
someTermsSize [SomeTerm
term]
{-# INLINE someTermSize #-}

termsSize :: [Term a] -> Int
termsSize :: forall a. [Term a] -> Id
termsSize [Term a]
terms = [SomeTerm] -> Id
someTermsSize ([SomeTerm] -> Id) -> [SomeTerm] -> Id
forall a b. (a -> b) -> a -> b
$ (\Term a
x -> Term a -> (SupportedPrim a => SomeTerm) -> SomeTerm
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
x ((SupportedPrim a => SomeTerm) -> SomeTerm)
-> (SupportedPrim a => SomeTerm) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
x) (Term a -> SomeTerm) -> [Term a] -> [SomeTerm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term a]
terms
{-# INLINEABLE termsSize #-}

termSize :: Term a -> Int
termSize :: forall a. Term a -> Id
termSize Term a
term = [Term a] -> Id
forall a. [Term a] -> Id
termsSize [Term a
term]
{-# INLINE termSize #-}