Language.Hasmtlib.Type.OMT

Documentation

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

Show SoftFormula

Defined in Language.Hasmtlib.Type.OMT

Methods

showsPrec :: Int -> SoftFormula -> ShowS

show :: SoftFormula -> String

showList :: [SoftFormula] -> ShowS

Render SoftFormula

Defined in Language.Hasmtlib.Type.OMT

Methods

render :: SoftFormula -> Builder

mWeight :: Lens' SoftFormula (Maybe Double)

mGroupId :: Lens' SoftFormula (Maybe String)

formula :: Lens' SoftFormula (Expr 'BoolSort)

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.Type.OMT

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.Type.OMT

Methods

render :: Maximize t -> Builder

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

RenderSeq OMT

Defined in Language.Hasmtlib.Type.OMT

Methods

renderSeq :: OMT -> Seq Builder

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

Default (Debugger OMT)

Defined in Language.Hasmtlib.Solver.Common

Methods

def :: Debugger OMT

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

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

softFormulas :: Lens' OMT (Seq SoftFormula)

smt :: Lens' OMT SMT