{-# 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,
    someTermsSize,
    someTermSize,
    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 = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Term t -> (TypeRep, Id)
identityWithTypeRep
{-# INLINE identity #-}

identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
identityWithTypeRep (ConTerm Id
i t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (SymTerm Id
i TypedSymbol t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (UnaryTerm Id
i tag
_ Term arg
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BinaryTerm Id
i tag
_ Term arg1
_ Term arg2
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TernaryTerm Id
i tag
_ Term arg1
_ Term arg2
_ Term arg3
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (NotTerm Id
i Term Bool
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (OrTerm Id
i Term Bool
_ Term Bool
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AndTerm Id
i Term Bool
_ Term Bool
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (EqvTerm Id
i Term t1
_ Term t1
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ITETerm Id
i Term Bool
_ Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AddNumTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (UMinusNumTerm Id
i Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TimesNumTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AbsNumTerm Id
i Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (SignumNumTerm Id
i Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (LTNumTerm Id
i Term t1
_ Term t1
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (LENumTerm Id
i Term t1
_ Term t1
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (AndBitsTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (OrBitsTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (XorBitsTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ComplementBitsTerm Id
i Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ShiftBitsTerm Id
i Term t
_ Id
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RotateBitsTerm Id
i Term t
_ Id
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVConcatTerm Id
i Term (bv a)
_ Term (bv b)
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVSelectTerm Id
i TypeRep ix
_ TypeRep w
_ Term (bv n)
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (BVExtendTerm Id
i Bool
_ TypeRep r
_ Term (bv l)
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (TabularFunApplyTerm Id
i Term (a =-> t)
_ Term a
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (GeneralFunApplyTerm Id
i Term (a --> t)
_ Term a
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (DivIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ModIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (QuotIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RemIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (DivBoundedIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (ModBoundedIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (QuotBoundedIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t), Id
i)
identityWithTypeRep (RemBoundedIntegralTerm Id
i Term t
_ Term t
_) = (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (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 = SupportedPrim t => a
x
introSupportedPrimConstraint SymTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint UnaryTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint BinaryTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint TernaryTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint NotTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint OrTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint AndTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint EqvTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint ITETerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint AddNumTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint UMinusNumTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint TimesNumTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint AbsNumTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint SignumNumTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint LTNumTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint LENumTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint AndBitsTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint OrBitsTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint XorBitsTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint ComplementBitsTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint ShiftBitsTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint RotateBitsTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint BVConcatTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint BVSelectTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint BVExtendTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint TabularFunApplyTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint GeneralFunApplyTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint DivIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint ModIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint QuotIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint RemIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint DivBoundedIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint ModBoundedIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint QuotBoundedIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
introSupportedPrimConstraint RemBoundedIntegralTerm {} SupportedPrim t => a
x = SupportedPrim t => a
x
{-# INLINE introSupportedPrimConstraint #-}

extractSymbolicsSomeTerm :: SomeTerm -> S.HashSet SomeTypedSymbol
extractSymbolicsSomeTerm :: SomeTerm -> HashSet SomeTypedSymbol
extractSymbolicsSomeTerm SomeTerm
t1 = forall s a. State s a -> s -> a
evalState (SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached SomeTerm
t1) 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (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 -> 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 <- forall s (m :: * -> *). MonadState s m => m s
get
          forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ 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
          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 {}) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. HashSet a
S.empty
    go (SomeTerm (SymTerm Id
_ (TypedSymbol a
sym :: TypedSymbol a))) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Hashable a => a -> HashSet a
S.singleton forall a b. (a -> b) -> a -> b
$ forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
SomeTypedSymbol (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) TypedSymbol a
sym
    go (SomeTerm (UnaryTerm Id
_ tag
_ Term arg
arg)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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)) = forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term a
arg
    go (SomeTerm (SignumNumTerm Id
_ Term a
arg)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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)) = 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
_)) = 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
_)) = 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)) = 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 n)
arg)) = 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)) = forall {a}.
SupportedPrim a =>
Term a
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
goUnary Term (bv l)
arg
    go (SomeTerm (TabularFunApplyTerm Id
_ Term (a =-> a)
func Term a
arg)) = 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)) = 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 (DivIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = 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)) = 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)) = 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)) = 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 (DivBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = 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 (ModBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = 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 (QuotBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = 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 (RemBoundedIntegralTerm Id
_ Term a
arg1 Term a
arg2)) = 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 (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 (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg1)
      HashSet SomeTypedSymbol
r2 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg2)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
r1 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 (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg1)
      HashSet SomeTypedSymbol
r2 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg2)
      HashSet SomeTypedSymbol
r3 <- SomeTerm
-> State
     (HashMap SomeTerm (HashSet SomeTypedSymbol))
     (HashSet SomeTypedSymbol)
gocached (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
arg3)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
r1 forall a. Semigroup a => a -> a -> a
<> HashSet SomeTypedSymbol
r2 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 (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 {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@SymTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@UnaryTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BinaryTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TernaryTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@NotTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@OrTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AndTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@EqvTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ITETerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AddNumTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@UMinusNumTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TimesNumTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AbsNumTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@SignumNumTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@LTNumTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@LENumTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@AndBitsTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@OrBitsTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@XorBitsTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ComplementBitsTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ShiftBitsTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RotateBitsTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVConcatTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVSelectTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@BVExtendTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@TabularFunApplyTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@GeneralFunApplyTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@DivIntegralTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ModIntegralTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@QuotIntegralTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RemIntegralTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@DivBoundedIntegralTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@ModBoundedIntegralTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@QuotBoundedIntegralTerm {} = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
castTerm t :: Term a
t@RemBoundedIntegralTerm {} = 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) = forall t. SupportedPrim t => t -> String
pformatCon t
t
pformat (SymTerm Id
_ TypedSymbol t
sym) = forall t. SupportedPrim t => TypedSymbol t -> String
pformatSym TypedSymbol t
sym
pformat (UnaryTerm Id
_ tag
tag Term arg
arg1) = 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) = 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) = 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
"(! " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = String
"(|| " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = String
"(&& " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term Bool
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (EqvTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(= " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ITETerm Id
_ Term Bool
cond Term t
arg1 Term t
arg2) = String
"(ite " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term Bool
cond forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AddNumTerm Id
_ Term t
arg1 Term t
arg2) = String
"(+ " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (UMinusNumTerm Id
_ Term t
arg) = String
"(- " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (TimesNumTerm Id
_ Term t
arg1 Term t
arg2) = String
"(* " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AbsNumTerm Id
_ Term t
arg) = String
"(abs " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (SignumNumTerm Id
_ Term t
arg) = String
"(signum " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (LTNumTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(< " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (LENumTerm Id
_ Term t1
arg1 Term t1
arg2) = String
"(<= " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t1
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (AndBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(& " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (OrBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(| " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (XorBitsTerm Id
_ Term t
arg1 Term t
arg2) = String
"(^ " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ComplementBitsTerm Id
_ Term t
arg) = String
"(~ " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ShiftBitsTerm Id
_ Term t
arg Id
n) = String
"(shift " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Id
n forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RotateBitsTerm Id
_ Term t
arg Id
n) = String
"(rotate " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Id
n forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2) = String
"(bvconcat " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term (bv a)
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term (bv b)
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVSelectTerm Id
_ TypeRep ix
ix TypeRep w
w Term (bv n)
arg) = String
"(bvselect " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep ix
ix forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep w
w forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term (bv n)
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (BVExtendTerm Id
_ Bool
signed TypeRep r
n Term (bv l)
arg) =
  (if Bool
signed then String
"(bvsext " else String
"(bvzext ") forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep r
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term (bv l)
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (TabularFunApplyTerm Id
_ Term (a =-> t)
func Term a
arg) = String
"(apply " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term (a =-> t)
func forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term a
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (GeneralFunApplyTerm Id
_ Term (a --> t)
func Term a
arg) = String
"(apply " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term (a --> t)
func forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term a
arg forall a. [a] -> [a] -> [a]
++ String
")"
pformat (DivIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(div " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ModIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(mod " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (QuotIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(quot " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RemIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(rem " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (DivBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(div " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (ModBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(mod " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (QuotBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(quot " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
pformat (RemBoundedIntegralTerm Id
_ Term t
arg1 Term t
arg2) = String
"(rem " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall t. SupportedPrim t => Term t -> String
pformat Term t
arg2 forall a. [a] -> [a] -> [a]
++ String
")"
{-# INLINE pformat #-}

someTermsSize :: [SomeTerm] -> Int
someTermsSize :: [SomeTerm] -> Id
someTermsSize [SomeTerm]
terms = forall a. HashSet a -> Id
S.size forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> s
execState (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse SomeTerm -> State (HashSet SomeTerm) ()
goSome [SomeTerm]
terms) forall a. HashSet a
S.empty
  where
    exists :: Term a -> m Bool
exists Term a
t = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
    add :: Term a -> m ()
add Term a
t = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
    goSome :: SomeTerm -> State (S.HashSet SomeTerm) ()
    goSome :: SomeTerm -> State (HashSet SomeTerm) ()
goSome (SomeTerm Term a
b) = forall b. Term b -> State (HashSet SomeTerm) ()
go Term a
b
    go :: forall b. Term b -> State (S.HashSet SomeTerm) ()
    go :: forall b. Term b -> State (HashSet SomeTerm) ()
go t :: Term b
t@ConTerm {} = forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
    go t :: Term b
t@SymTerm {} = 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) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term arg
arg
    go t :: Term b
t@(BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
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) = forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a -> Term b -> Term c -> Term d -> State (HashSet SomeTerm) ()
goTernary Term b
t Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
    go t :: Term b
t@(NotTerm Id
_ Term Bool
arg) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term Bool
arg
    go t :: Term b
t@(OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
    go t :: Term b
t@(AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
    go t :: Term b
t@(EqvTerm Id
_ Term t1
arg1 Term t1
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
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) = forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a -> Term b -> Term c -> Term d -> State (HashSet SomeTerm) ()
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) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(UMinusNumTerm Id
_ Term b
arg) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(TimesNumTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(AbsNumTerm Id
_ Term b
arg) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(SignumNumTerm Id
_ Term b
arg) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(LTNumTerm Id
_ Term t1
arg1 Term t1
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(LENumTerm Id
_ Term t1
arg1 Term t1
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
    go t :: Term b
t@(AndBitsTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(OrBitsTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(XorBitsTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(ComplementBitsTerm Id
_ Term b
arg) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(ShiftBitsTerm Id
_ Term b
arg Id
_) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(RotateBitsTerm Id
_ Term b
arg Id
_) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term b
arg
    go t :: Term b
t@(BVConcatTerm Id
_ Term (bv a)
arg1 Term (bv b)
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
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 n)
arg) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term (bv n)
arg
    go t :: Term b
t@(BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg) = forall a b.
SupportedPrim a =>
Term a -> Term b -> State (HashSet SomeTerm) ()
goUnary Term b
t Term (bv l)
arg
    go t :: Term b
t@(TabularFunApplyTerm Id
_ Term (a =-> b)
func Term a
arg) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
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) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term (a --> b)
func Term a
arg
    go t :: Term b
t@(DivIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(ModIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(QuotIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(RemIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(DivBoundedIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(ModBoundedIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(QuotBoundedIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
goBinary Term b
t Term b
arg1 Term b
arg2
    go t :: Term b
t@(RemBoundedIntegralTerm Id
_ Term b
arg1 Term b
arg2) = forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> State (HashSet SomeTerm) ()
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 -> State (HashSet SomeTerm) ()
goUnary Term a
t Term b
arg = do
      Bool
b <- forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          forall b. Term b -> State (HashSet SomeTerm) ()
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 -> State (HashSet SomeTerm) ()
goBinary Term a
t Term b
arg1 Term c
arg2 = do
      Bool
b <- forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          forall b. Term b -> State (HashSet SomeTerm) ()
go Term b
arg1
          forall b. Term b -> State (HashSet SomeTerm) ()
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 -> State (HashSet SomeTerm) ()
goTernary Term a
t Term b
arg1 Term c
arg2 Term d
arg3 = do
      Bool
b <- forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
      if Bool
b
        then forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
          forall b. Term b -> State (HashSet SomeTerm) ()
go Term b
arg1
          forall b. Term b -> State (HashSet SomeTerm) ()
go Term c
arg2
          forall b. Term b -> State (HashSet SomeTerm) ()
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 forall a b. (a -> b) -> a -> b
$ (\Term a
x -> forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
x forall a b. (a -> b) -> a -> b
$ forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term a]
terms
{-# INLINEABLE termsSize #-}

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