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

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
  ( identity,
    identityWithTypeRep,
    introSupportedPrimConstraint,
    extractSymbolicsTerm,
    castTerm,
    pformat,
    termSize,
    termsSize,
  )
where

import Control.Monad.State
import Data.HashMap.Strict as M
import Data.HashSet as S
import Data.Interned
import Data.Typeable
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.TabularFun ()
import qualified Type.Reflection as R

identity :: Term t -> Id
identity :: forall t. Term t -> Id
identity (ConTerm Id
i t
_) = Id
i
identity (SymTerm Id
i TypedSymbol t
_) = Id
i
identity (UnaryTerm Id
i tag
_ Term arg
_) = Id
i
identity (BinaryTerm Id
i tag
_ Term arg1
_ Term arg2
_) = Id
i
identity (TernaryTerm Id
i tag
_ Term arg1
_ Term arg2
_ Term arg3
_) = Id
i
identity (NotTerm Id
i Term Bool
_) = Id
i
identity (OrTerm Id
i Term Bool
_ Term Bool
_) = Id
i
identity (AndTerm Id
i Term Bool
_ Term Bool
_) = Id
i
identity (EqvTerm Id
i Term t1
_ Term t1
_) = Id
i
identity (ITETerm Id
i Term Bool
_ Term t
_ Term t
_) = Id
i
identity (AddNumTerm Id
i Term t
_ Term t
_) = Id
i
identity (UMinusNumTerm Id
i Term t
_) = Id
i
identity (TimesNumTerm Id
i Term t
_ Term t
_) = Id
i
identity (AbsNumTerm Id
i Term t
_) = Id
i
identity (SignumNumTerm Id
i Term t
_) = Id
i
identity (LTNumTerm Id
i Term t1
_ Term t1
_) = Id
i
identity (LENumTerm Id
i Term t1
_ Term t1
_) = Id
i
identity (AndBitsTerm Id
i Term t
_ Term t
_) = Id
i
identity (OrBitsTerm Id
i Term t
_ Term t
_) = Id
i
identity (XorBitsTerm Id
i Term t
_ Term t
_) = Id
i
identity (ComplementBitsTerm Id
i Term t
_) = Id
i
identity (ShiftBitsTerm Id
i Term t
_ Id
_) = Id
i
identity (RotateBitsTerm Id
i Term t
_ Id
_) = Id
i
identity (BVConcatTerm Id
i Term (bv a)
_ Term (bv b)
_) = Id
i
identity (BVSelectTerm Id
i TypeRep ix
_ TypeRep w
_ Term (bv a)
_) = Id
i
identity (BVExtendTerm Id
i Bool
_ TypeRep n
_ Term (bv a)
_) = Id
i
identity (TabularFunApplyTerm Id
i Term (a =-> t)
_ Term a
_) = Id
i
identity (GeneralFunApplyTerm Id
i Term (a --> t)
_ Term a
_) = Id
i
identity (DivIntegerTerm Id
i Term Integer
_ Term Integer
_) = Id
i
identity (ModIntegerTerm Id
i Term Integer
_ Term Integer
_) = Id
i
{-# INLINE identity #-}

identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
identityWithTypeRep (ConTerm Id
i t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (SymTerm Id
i TypedSymbol t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (UnaryTerm Id
i tag
_ Term arg
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BinaryTerm Id
i tag
_ Term arg1
_ Term arg2
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TernaryTerm Id
i tag
_ Term arg1
_ Term arg2
_ Term arg3
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (NotTerm Id
i Term Bool
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (OrTerm Id
i Term Bool
_ Term Bool
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AndTerm Id
i Term Bool
_ Term Bool
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (EqvTerm Id
i Term t1
_ Term t1
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ITETerm Id
i Term Bool
_ Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AddNumTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (UMinusNumTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TimesNumTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AbsNumTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (SignumNumTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (LTNumTerm Id
i Term t1
_ Term t1
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (LENumTerm Id
i Term t1
_ Term t1
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AndBitsTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (OrBitsTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (XorBitsTerm Id
i Term t
_ Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ComplementBitsTerm Id
i Term t
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ShiftBitsTerm Id
i Term t
_ Id
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RotateBitsTerm Id
i Term t
_ Id
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVConcatTerm Id
i Term (bv a)
_ Term (bv b)
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVSelectTerm Id
i TypeRep ix
_ TypeRep w
_ Term (bv a)
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVExtendTerm Id
i Bool
_ TypeRep n
_ Term (bv a)
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TabularFunApplyTerm Id
i Term (a =-> t)
_ Term a
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (GeneralFunApplyTerm Id
i Term (a --> t)
_ Term a
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (DivIntegerTerm Id
i Term Integer
_ Term Integer
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ModIntegerTerm Id
i Term Integer
_ Term Integer
_) = (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
{-# INLINE identityWithTypeRep #-}

introSupportedPrimConstraint :: forall t a. Term t -> ((SupportedPrim t) => a) -> a
introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint ConTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint SymTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint UnaryTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BinaryTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint TernaryTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint NotTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint OrTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AndTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint EqvTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ITETerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AddNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint UMinusNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint TimesNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AbsNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint SignumNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint LTNumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint LENumTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint AndBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint OrBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint XorBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ComplementBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ShiftBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint RotateBitsTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BVConcatTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BVSelectTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint BVExtendTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint TabularFunApplyTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint GeneralFunApplyTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint DivIntegerTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
introSupportedPrimConstraint ModIntegerTerm {} SupportedPrim t => a
x = a
SupportedPrim t => a
x
{-# INLINE introSupportedPrimConstraint #-}

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 (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 (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 (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 (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 (EqvTerm 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 (UMinusNumTerm 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 (TimesNumTerm 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 (LTNumTerm 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 (LENumTerm 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 (ShiftBitsTerm Id
_ Term a
arg Id
_)) = 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 (RotateBitsTerm Id
_ Term a
arg Id
_)) = 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 (BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2)) = Term (bv a)
-> Term (bv b)
-> 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 a)
arg1 Term (bv b)
arg2
    go (SomeTerm (BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv a)
arg)) = Term (bv a)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (bv a)
arg
    go (SomeTerm (BVExtendTerm Id
_ Bool
_ TypeRep n
_ Term (bv a)
arg)) = Term (bv a)
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (bv a)
arg
    go (SomeTerm (TabularFunApplyTerm Id
_ Term (a =-> a)
func Term a
arg)) = Term (a =-> 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 =-> a)
func Term a
arg
    go (SomeTerm (GeneralFunApplyTerm Id
_ Term (a --> a)
func Term a
arg)) = Term (a --> 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 --> a)
func Term a
arg
    go (SomeTerm (DivIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2)) = Term Integer
-> Term Integer
-> 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 Integer
arg1 Term Integer
arg2
    go (SomeTerm (ModIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2)) = Term Integer
-> Term Integer
-> 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 Integer
arg1 Term Integer
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 (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 (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@EqvTerm {} = 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@UMinusNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TimesNumTerm {} = 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@LTNumTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@LENumTerm {} = 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@ShiftBitsTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RotateBitsTerm {} = 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@TabularFunApplyTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@GeneralFunApplyTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@DivIntegerTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ModIntegerTerm {} = Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
{-# INLINE castTerm #-}

pformat :: forall t. (SupportedPrim t) => Term t -> String
pformat :: forall t. SupportedPrim t => Term t -> String
pformat (ConTerm Id
_ t
t) = t -> String
forall t. SupportedPrim t => t -> String
pformatCon t
t
pformat (SymTerm Id
_ TypedSymbol t
sym) = TypedSymbol t -> String
forall t. SupportedPrim t => TypedSymbol t -> String
pformatSym TypedSymbol t
sym
pformat (UnaryTerm Id
_ tag
tag Term arg
arg1) = tag -> Term arg -> String
forall tag arg t. UnaryOp tag arg t => tag -> Term arg -> String
pformatUnary tag
tag Term arg
arg1
pformat (BinaryTerm Id
_ tag
tag Term arg1
arg1 Term arg2
arg2) = tag -> Term arg1 -> Term arg2 -> String
forall tag arg1 arg2 t.
BinaryOp tag arg1 arg2 t =>
tag -> Term arg1 -> Term arg2 -> String
pformatBinary tag
tag Term arg1
arg1 Term arg2
arg2
pformat (TernaryTerm Id
_ tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
forall tag arg1 arg2 arg3 t.
TernaryOp tag arg1 arg2 arg3 t =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
pformatTernary tag
tag Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
pformat (NotTerm Id
_ Term Bool
arg) = String
"(! " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = String
"(|| " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = String
"(&& " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (EqvTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ITETerm Id
_ Term Bool
cond Term t
arg1 Term t
arg2) = String
"(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Bool
cond String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AddNumTerm Id
_ Term t
arg1 Term t
arg2) = String
"(+ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (UMinusNumTerm Id
_ Term t
arg) = String
"(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (TimesNumTerm Id
_ Term t
arg1 Term t
arg2) = String
"(* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AbsNumTerm Id
_ Term t
arg) = String
"(abs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (SignumNumTerm Id
_ Term t
arg) = String
"(signum " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (LTNumTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(< " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (LENumTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t1 -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AndBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(& " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (OrBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(| " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (XorBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(^ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ComplementBitsTerm Id
_ Term t
arg) = String
"(~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ShiftBitsTerm Id
_ Term t
arg Id
n) = String
"(shift " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RotateBitsTerm Id
_ Term t
arg Id
n) = String
"(rotate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term t -> String
forall t. SupportedPrim t => Term t -> String
pformat Term t
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2) = String
"(bvconcat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv a)
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv b) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv b)
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVSelectTerm Id
_ TypeRep ix
ix TypeRep w
w Term (bv a)
arg) = String
"(bvselect " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep ix -> String
forall a. Show a => a -> String
show TypeRep ix
ix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep w -> String
forall a. Show a => a -> String
show TypeRep w
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv a)
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVExtendTerm Id
_ Bool
signed TypeRep n
n Term (bv a)
arg) =
  (if Bool
signed then String
"(bvsext " else String
"(bvzext") String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep n -> String
forall a. Show a => a -> String
show TypeRep n
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (bv a) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (bv a)
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (TabularFunApplyTerm Id
_ Term (a =-> t)
func Term a
arg) = String
"(apply " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (a =-> t) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (a =-> t)
func String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall t. SupportedPrim t => Term t -> String
pformat Term a
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (GeneralFunApplyTerm Id
_ Term (a --> t)
func Term a
arg) = String
"(apply " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term (a --> t) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (a --> t)
func String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall t. SupportedPrim t => Term t -> String
pformat Term a
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (DivIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) = String
"(div " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Integer
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Integer
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ModIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) = String
"(mod " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Integer
arg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Integer -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Integer
arg2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
{-# INLINE pformat #-}

termsSize :: [Term a] -> Int
termsSize :: forall a. [Term a] -> Id
termsSize [Term a]
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 ((Term a -> StateT (HashSet SomeTerm) Identity ())
-> [Term a] -> State (HashSet SomeTerm) [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term a -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go [Term a]
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))
    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@(EqvTerm 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@(UMinusNumTerm 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@(TimesNumTerm 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@(LTNumTerm 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@(LENumTerm 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@(ShiftBitsTerm Id
_ Term b
arg Id
_) = 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@(RotateBitsTerm Id
_ Term b
arg Id
_) = 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@(BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2) = Term b
-> Term (bv a)
-> Term (bv 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 (bv a)
arg1 Term (bv b)
arg2
    go t :: Term b
t@(BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv a)
arg) = Term b -> Term (bv a) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv a)
arg
    go t :: Term b
t@(BVExtendTerm Id
_ Bool
_ TypeRep n
_ Term (bv a)
arg) = Term b -> Term (bv a) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv a)
arg
    go t :: Term b
t@(TabularFunApplyTerm Id
_ Term (a =-> b)
func Term a
arg) = Term b
-> Term (a =-> b)
-> 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 (a =-> b)
func Term a
arg
    go t :: Term b
t@(GeneralFunApplyTerm Id
_ Term (a --> b)
func Term a
arg) = Term b
-> Term (a --> b)
-> 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 (a --> b)
func Term a
arg
    go t :: Term b
t@(DivIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) = Term b
-> Term Integer
-> Term Integer
-> 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 Integer
arg1 Term Integer
arg2
    go t :: Term b
t@(ModIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) = Term b
-> Term Integer
-> Term Integer
-> 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 Integer
arg1 Term Integer
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 (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 (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 (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 termsSize #-}

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