Language.Hasmtlib.Type.Debugger

This module provides debugging capabilites for the problem definition and communication with the external solver.

Type

data Debugger s

A type holding actions for debugging states holding SMT-Problems.

Constructors

Debugger

Fields

• debugState :: s -> IO ()

  Debug the entire state

• debugOption :: Builder -> IO ()
• debugLogic :: Builder -> IO ()
• debugVar :: Builder -> IO ()
• debugAssert :: Builder -> IO ()
• debugPush :: Builder -> IO ()
• debugPop :: Builder -> IO ()
• debugCheckSat :: Builder -> IO ()
• debugGetModel :: Builder -> IO ()
• debugGetValue :: Builder -> IO ()
• debugMinimize :: Builder -> IO ()
• debugMaximize :: Builder -> IO ()
• debugAssertSoft :: Builder -> IO ()
• debugResultResponse :: ByteString -> IO ()

  Debug the solvers raw response for (check-sat)

• debugModelResponse :: ByteString -> IO ()

  Debug the solvers raw response for (get-model)

Instances

Contravariant Debugger

Defined in Language.Hasmtlib.Type.Debugger

Methods

contramap :: (a' -> a) -> Debugger a -> Debugger a'

(>$) :: b -> Debugger b -> Debugger a

Monoid (Debugger s)

Defined in Language.Hasmtlib.Type.Debugger

Methods

mempty :: Debugger s

mappend :: Debugger s -> Debugger s -> Debugger s

mconcat :: [Debugger s] -> Debugger s

Semigroup (Debugger s)

Concats actions

Defined in Language.Hasmtlib.Type.Debugger

Methods

(<>) :: Debugger s -> Debugger s -> Debugger s

sconcat :: NonEmpty (Debugger s) -> Debugger s

stimes :: Integral b => b -> Debugger s -> Debugger s

Default (Debugger s)

Defined in Language.Hasmtlib.Type.Debugger

Methods

def :: Debugger s

class StateDebugger s where

A class that allows debugging states.

Methods

statistically :: Debugger s

Debugs information about the problem like the amount of variables and assertions.

Instances

StateDebugger OMT

Defined in Language.Hasmtlib.Type.Debugger

Methods

statistically :: Debugger OMT

StateDebugger SMT

Defined in Language.Hasmtlib.Type.Debugger

Methods

statistically :: Debugger SMT

Construction

Volume

silently :: Debugger s

The silent Debugger. Does not debug at all.

noisy :: Debugger s

The noisy Debugger.

Debugs the entire problem definition.

verbosely :: Debugger s

The verbose Debugger.

Debugs all communication between Haskell and the external solver.

Information

optionish :: Debugger s

A Debugger for debugging all rendered options that have been set.

logicish :: Debugger s

A Debugger for debugging the logic that has been set.

varish :: Debugger s

A Debugger for debugging all variable declarations.

assertionish :: Debugger s

A Debugger for debugging all assertions.

incrementalStackish :: Debugger s

A Debugger for debugging every push/pop-interaction with the solvers incremental stack.

getValueish :: Debugger s

A Debugger for debugging every (get-value) call to the solver.

responseish :: Debugger s

A Debugger for debugging the entire and raw responses of a solver for the commands (check-sat) and (get-model).