Language.Hasmtlib.Type.OMT

This module provides a concrete implementation for MonadOMT with it's state OMT.

SoftFormula

Type

data SoftFormula

An assertion of a booolean expression in OMT that may be weighted.

Constructors

SoftFormula

Fields

• _formula :: Expr BoolSort

  The underlying soft formula

• _mWeight :: Maybe Double

  Weight of the soft formula

• _mGroupId :: Maybe String

  Group-Id of the soft formula

Instances

Render SoftFormula

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: SoftFormula -> Builder

Lens

formula :: Lens' SoftFormula (Expr 'BoolSort)

mWeight :: Lens' SoftFormula (Maybe Double)

mGroupId :: Lens' SoftFormula (Maybe String)

Optimization targets

newtype Minimize t

A newtype for numerical expressions that are target of a minimization.

Constructors

Minimize

Fields

• _targetMin :: Expr t

Instances

KnownSMTSort t => Render (Minimize t)

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Minimize t -> Builder

newtype Maximize t

A newtype for numerical expressions that are target of a maximization.

Constructors

Maximize

Fields

• _targetMax :: Expr t

Instances

KnownSMTSort t => Render (Maximize t)

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Maximize t -> Builder

OMT

Type

data OMT

The state of the OMT-problem.

Constructors

OMT

Fields

• _smt :: !SMT

  The underlying SMT-Problem

• _targetMinimize :: !(Seq (SomeKnownSMTSort Minimize))

  All expressions to minimize

• _targetMaximize :: !(Seq (SomeKnownSMTSort Maximize))

  All expressions to maximize

• _softFormulas :: !(Seq SoftFormula)

  All soft assertions of boolean expressions

Instances

Default OMT

Defined in Language.Hasmtlib.Type.OMT

Methods

def :: OMT

RenderProblem OMT

Defined in Language.Hasmtlib.Internal.Render

Methods

renderOptions :: OMT -> Seq Builder

renderLogic :: OMT -> Builder

renderDeclareVars :: OMT -> Seq Builder

renderAssertions :: OMT -> Seq Builder

renderSoftAssertions :: OMT -> Seq Builder

renderMinimizations :: OMT -> Seq Builder

renderMaximizations :: OMT -> Seq Builder

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 ()

StateDebugger OMT

Defined in Language.Hasmtlib.Type.Debugger

Methods

statistically :: Debugger OMT

MonadSMT OMT m => MonadOMT OMT m

Defined in Language.Hasmtlib.Type.OMT

Methods

minimize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

maximize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

assertSoft :: Expr 'BoolSort -> Maybe Double -> Maybe String -> m ()

MonadState OMT m => MonadSMT OMT m

Defined in Language.Hasmtlib.Type.OMT

Methods

smtvar' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (SMTVar t)

var' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (Expr t)

assert :: Expr 'BoolSort -> m ()

setOption :: SMTOption -> m ()

setLogic :: String -> m ()

type SharingMonad OMT

Defined in Language.Hasmtlib.Type.OMT

type SharingMonad OMT = Monad

Lens

smt :: Lens' OMT SMT

targetMinimize :: Lens' OMT (Seq (SomeKnownSMTSort Minimize))

targetMaximize :: Lens' OMT (Seq (SomeKnownSMTSort Maximize))

softFormulas :: Lens' OMT (Seq SoftFormula)