Language.Hasmtlib.Internal.Sharing

Documentation

class Sharing s where

States that can share expressions by comparing their StableNames.

Associated Types

type SharingMonad s :: (Type -> Type) -> Constraint

A constraint on the monad used when asserting the shared node in assertSharedNode.

Methods

stableMap :: Lens' s (HashMap (StableName ()) (SomeKnownSMTSort Expr))

A Lens' on a mapping between a StableName and it's Expr we may share.

assertSharedNode :: (MonadState s m, SharingMonad s m) => StableName () -> Expr BoolSort -> m ()

Asserts that a node-expression is represented by it's auxiliary node-variable: nodeExpr :: Expr t === nodeVar. Also gives access to the StableName of the original expression.

setSharingMode :: MonadState s m => SharingMode -> m ()

Sets the mode used for sharing common expressions. Defaults to StableNames.

Instances

Sharing OMT

Defined in Language.Hasmtlib.Type.OMT

Associated Types

type SharingMonad OMT :: (Type -> Type) -> Constraint

Methods

stableMap :: Lens' OMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))

assertSharedNode :: (MonadState OMT m, SharingMonad OMT m) => StableName () -> Expr 'BoolSort -> m ()

setSharingMode :: MonadState OMT m => SharingMode -> m ()

Sharing Pipe

Defined in Language.Hasmtlib.Type.Pipe

Associated Types

type SharingMonad Pipe :: (Type -> Type) -> Constraint

Methods

stableMap :: Lens' Pipe (HashMap (StableName ()) (SomeKnownSMTSort Expr))

assertSharedNode :: (MonadState Pipe m, SharingMonad Pipe m) => StableName () -> Expr 'BoolSort -> m ()

setSharingMode :: MonadState Pipe m => SharingMode -> m ()

Sharing SMT

Defined in Language.Hasmtlib.Type.SMT

Associated Types

type SharingMonad SMT :: (Type -> Type) -> Constraint

Methods

stableMap :: Lens' SMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))

assertSharedNode :: (MonadState SMT m, SharingMonad SMT m) => StableName () -> Expr 'BoolSort -> m ()

setSharingMode :: MonadState SMT m => SharingMode -> m ()

data SharingMode

Mode used for sharing.

Constructors

None

Common expressions are not shared at all

StableNames

Expressions that resolve to the same StableName are shared

Instances

Show SharingMode

Defined in Language.Hasmtlib.Internal.Sharing

Methods

showsPrec :: Int -> SharingMode -> ShowS

show :: SharingMode -> String

showList :: [SharingMode] -> ShowS

Default SharingMode

Defined in Language.Hasmtlib.Internal.Sharing

Methods

def :: SharingMode

runSharing :: (KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => SharingMode -> Expr t -> m (Expr t)

Shares all possible sub-expressions in given expression. Replaces each node in the expression-tree with an auxiliary variable. All nodes x y where makeStableName x == makeStableName y are replaced with the same auxiliary variable. Therefore this creates a DAG.

share :: (Equatable (Expr t), KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => Expr t -> m (Expr t) -> m (Expr t)

Returns an auxiliary variable representing this expression node. If such a shared auxiliary variable exists already, returns that. Otherwise creates one and returns it.