module Language.Hasmtlib.Type.Debugger
(
Debugger(..), StateDebugger(..)
, silently
, noisy
, verbosely
, optionish
, logicish
, varish
, assertionish
, incrementalStackish, getValueish
, responseish
)
where
import Language.Hasmtlib.Type.SMT
import Language.Hasmtlib.Type.OMT
import Data.Sequence as Seq hiding ((|>), filter)
import Data.ByteString.Lazy hiding (singleton)
import Data.ByteString.Lazy.UTF8 (toString)
import Data.ByteString.Builder
import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8
import Data.Default
import Control.Lens hiding (op)
data Debugger s = Debugger
{ forall s. Debugger s -> s -> IO ()
debugState :: s -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugOption :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugLogic :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugVar :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugAssert :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugPush :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugPop :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugCheckSat :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugGetModel :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugGetValue :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugMinimize :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugMaximize :: Builder -> IO ()
, forall s. Debugger s -> Builder -> IO ()
debugAssertSoft :: Builder -> IO ()
, forall s. Debugger s -> ByteString -> IO ()
debugResultResponse :: ByteString -> IO ()
, forall s. Debugger s -> ByteString -> IO ()
debugModelResponse :: ByteString -> IO ()
}
instance Default (Debugger s) where
def :: Debugger s
def = Debugger s
forall s. Debugger s
verbosely
printer :: Builder -> IO ()
printer :: Builder -> IO ()
printer = ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ())
-> (Builder -> ByteString) -> Builder -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> ByteString
toLazyByteString
silently :: Debugger s
silently :: forall s. Debugger s
silently = (s -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (ByteString -> IO ())
-> (ByteString -> IO ())
-> Debugger s
forall s.
(s -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (ByteString -> IO ())
-> (ByteString -> IO ())
-> Debugger s
Debugger
(IO () -> s -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> Builder -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> ByteString -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> ByteString -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
noisy :: Debugger s
noisy :: forall s. Debugger s
noisy = (s -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (ByteString -> IO ())
-> (ByteString -> IO ())
-> Debugger s
forall s.
(s -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (ByteString -> IO ())
-> (ByteString -> IO ())
-> Debugger s
Debugger
(IO () -> s -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
(IO () -> ByteString -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
(IO () -> ByteString -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
verbosely :: Debugger s
verbosely :: forall s. Debugger s
verbosely = (s -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (ByteString -> IO ())
-> (ByteString -> IO ())
-> Debugger s
forall s.
(s -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (Builder -> IO ())
-> (ByteString -> IO ())
-> (ByteString -> IO ())
-> Debugger s
Debugger
(IO () -> s -> IO ()
forall a b. a -> b -> a
const IO ()
forall a. Monoid a => a
mempty)
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
Builder -> IO ()
printer
(ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ())
-> (ByteString -> ByteString) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ByteString
s -> ByteString
"\n" ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
s ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
"\n"))
((ByteString -> IO ()) -> [ByteString] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ()) -> (ByteString -> String) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> String
toString) ([ByteString] -> IO ())
-> (ByteString -> [ByteString]) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> ByteString -> [ByteString]
split Word8
13)
optionish :: Debugger s
optionish :: forall s. Debugger s
optionish = Debugger s
forall s. Debugger s
silently { debugOption = printer }
logicish :: Debugger s
logicish :: forall s. Debugger s
logicish = Debugger s
forall s. Debugger s
silently { debugLogic = printer }
varish :: Debugger s
varish :: forall s. Debugger s
varish = Debugger s
forall s. Debugger s
silently { debugVar = printer }
assertionish :: Debugger s
assertionish :: forall s. Debugger s
assertionish = Debugger s
forall s. Debugger s
silently { debugAssert = printer, debugAssertSoft = printer }
incrementalStackish :: Debugger s
incrementalStackish :: forall s. Debugger s
incrementalStackish = Debugger s
forall s. Debugger s
silently { debugPush = printer, debugPop = printer }
getValueish :: Debugger s
getValueish :: forall s. Debugger s
getValueish = Debugger s
forall s. Debugger s
silently { debugGetValue = printer }
responseish :: Debugger s
responseish :: forall s. Debugger s
responseish = Debugger s
forall s. Debugger s
silently
{ debugResultResponse = ByteString.Char8.putStrLn . (\ByteString
s -> ByteString
"\n" ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
s ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
"\n")
, debugModelResponse = mapM_ (putStrLn . toString) . split 13
}
class StateDebugger s where
statistically :: Debugger s
instance StateDebugger SMT where
statistically :: Debugger SMT
statistically = Debugger Any
forall s. Debugger s
silently
{ debugState = \SMT
s -> do
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Variables: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (SomeKnownSMTSort SMTVar) -> Int
forall a. Seq a -> Int
Seq.length (SMT
sSMT
-> Getting
(Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
-> Seq (SomeKnownSMTSort SMTVar)
forall s a. s -> Getting a s a -> a
^.Getting
(Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
vars))
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Assertions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Expr 'BoolSort) -> Int
forall a. Seq a -> Int
Seq.length (SMT
sSMT
-> Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
-> Seq (Expr 'BoolSort)
forall s a. s -> Getting a s a -> a
^.Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
Lens' SMT (Seq (Expr 'BoolSort))
formulas))
}
instance StateDebugger OMT where
statistically :: Debugger OMT
statistically = Debugger Any
forall s. Debugger s
silently
{ debugState = \OMT
omt -> do
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Variables: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (SomeKnownSMTSort SMTVar) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting
(Seq (SomeKnownSMTSort SMTVar)) OMT (Seq (SomeKnownSMTSort SMTVar))
-> Seq (SomeKnownSMTSort SMTVar)
forall s a. s -> Getting a s a -> a
^.(SMT -> Const (Seq (SomeKnownSMTSort SMTVar)) SMT)
-> OMT -> Const (Seq (SomeKnownSMTSort SMTVar)) OMT
Lens' OMT SMT
smt((SMT -> Const (Seq (SomeKnownSMTSort SMTVar)) SMT)
-> OMT -> Const (Seq (SomeKnownSMTSort SMTVar)) OMT)
-> Getting
(Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
-> Getting
(Seq (SomeKnownSMTSort SMTVar)) OMT (Seq (SomeKnownSMTSort SMTVar))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Getting
(Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
vars))
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Hard assertions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Expr 'BoolSort) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting (Seq (Expr 'BoolSort)) OMT (Seq (Expr 'BoolSort))
-> Seq (Expr 'BoolSort)
forall s a. s -> Getting a s a -> a
^.(SMT -> Const (Seq (Expr 'BoolSort)) SMT)
-> OMT -> Const (Seq (Expr 'BoolSort)) OMT
Lens' OMT SMT
smt((SMT -> Const (Seq (Expr 'BoolSort)) SMT)
-> OMT -> Const (Seq (Expr 'BoolSort)) OMT)
-> Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
-> Getting (Seq (Expr 'BoolSort)) OMT (Seq (Expr 'BoolSort))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
Lens' SMT (Seq (Expr 'BoolSort))
formulas))
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Soft assertions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq SoftFormula -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting (Seq SoftFormula) OMT (Seq SoftFormula)
-> Seq SoftFormula
forall s a. s -> Getting a s a -> a
^.Getting (Seq SoftFormula) OMT (Seq SoftFormula)
Lens' OMT (Seq SoftFormula)
softFormulas))
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Optimizations: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (SomeKnownSMTSort Minimize) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting
(Seq (SomeKnownSMTSort Minimize))
OMT
(Seq (SomeKnownSMTSort Minimize))
-> Seq (SomeKnownSMTSort Minimize)
forall s a. s -> Getting a s a -> a
^.Getting
(Seq (SomeKnownSMTSort Minimize))
OMT
(Seq (SomeKnownSMTSort Minimize))
Lens' OMT (Seq (SomeKnownSMTSort Minimize))
targetMinimize) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq (SomeKnownSMTSort Maximize) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting
(Seq (SomeKnownSMTSort Maximize))
OMT
(Seq (SomeKnownSMTSort Maximize))
-> Seq (SomeKnownSMTSort Maximize)
forall s a. s -> Getting a s a -> a
^.Getting
(Seq (SomeKnownSMTSort Maximize))
OMT
(Seq (SomeKnownSMTSort Maximize))
Lens' OMT (Seq (SomeKnownSMTSort Maximize))
targetMaximize))
}