{- |
This module provides debugging capabilites for the problem definition and communication with the external solver.
-}
module Language.Hasmtlib.Type.Debugger
  (
    -- * Type
    Debugger(..), StateDebugger(..)

    -- * Construction
    -- ** Volume
  , silently
  , noisy
  , verbosely

    -- ** Information
  , 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)

-- | A type holding actions for debugging states holding SMT-Problems.
data Debugger s = Debugger
  { forall s. Debugger s -> s -> IO ()
debugState          :: s -> IO ()               -- ^ Debug the entire state
  , 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 ()      -- ^ Debug the solvers raw response for @(check-sat)@
  , forall s. Debugger s -> ByteString -> IO ()
debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@
  }

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

-- | The silent 'Debugger'. Does not debug at all.
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)

-- | The noisy 'Debugger'.
--
--   Debugs the entire problem definition.
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)

-- | The verbose 'Debugger'.
--
--   Debugs all communication between Haskell and the external solver.
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)

-- | A 'Debugger' for debugging all rendered options that have been set.
optionish :: Debugger s
optionish :: forall s. Debugger s
optionish = Debugger s
forall s. Debugger s
silently { debugOption = printer }

-- | A 'Debugger' for debugging the logic that has been set.
logicish :: Debugger s
logicish :: forall s. Debugger s
logicish = Debugger s
forall s. Debugger s
silently { debugLogic = printer }

-- | A 'Debugger' for debugging all variable declarations.
varish :: Debugger s
varish :: forall s. Debugger s
varish = Debugger s
forall s. Debugger s
silently { debugVar = printer }

-- | A 'Debugger' for debugging all assertions.
assertionish :: Debugger s
assertionish :: forall s. Debugger s
assertionish = Debugger s
forall s. Debugger s
silently { debugAssert = printer, debugAssertSoft = printer }

-- | A 'Debugger' for debugging every push/pop-interaction with the solvers incremental stack.
incrementalStackish :: Debugger s
incrementalStackish :: forall s. Debugger s
incrementalStackish = Debugger s
forall s. Debugger s
silently { debugPush = printer, debugPop = printer }

-- | A 'Debugger' for debugging every @(get-value)@ call to the solver.
getValueish :: Debugger s
getValueish :: forall s. Debugger s
getValueish = Debugger s
forall s. Debugger s
silently { debugGetValue = printer }

-- | A 'Debugger' for debugging the entire and raw responses of a solver for the commands @(check-sat)@ and @(get-model)@.
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
  }

-- | A class that allows debugging states.
class StateDebugger s where
  -- | Debugs information about the problem like the amount of variables and assertions.
  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))
    }