grisette-0.11.0.0: Symbolic evaluation as a library

Copyright	(c) Sirui Lu 2021-2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.SymPrim.Prim.TermUtils

Description

Synopsis

extractTerm :: forall (knd :: SymbolKind) a. (IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) => HashSet SomeTypedConstantSymbol -> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b)
someTermsSize :: [SomeTerm] -> Int
someTermSize :: SomeTerm -> Int
termSize :: Term a -> Int
termsSize :: [Term a] -> Int

Documentation

extractTerm :: forall (knd :: SymbolKind) a. (IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) => HashSet SomeTypedConstantSymbol -> Term a -> Maybe (HashSet (SomeTypedSymbol knd)) Source #

Extract all the symbols in a term.

castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b) Source #

Cast a term to another type.

someTermsSize :: [SomeTerm] -> Int Source #

Compute the size of a list of terms. Do not count the same term twice.

someTermSize :: SomeTerm -> Int Source #

Compute the size of a list of terms. Do not count the same term twice.

termSize :: Term a -> Int Source #

Compute the size of a term.

termsSize :: [Term a] -> Int Source #

Compute the size of a list of terms. Do not count the same term twice.