{- |
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 Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.SMTSort
import Data.Some.Constraint
import Data.Sequence as Seq hiding ((|>))
import Data.ByteString.Lazy (ByteString, split)
import Data.ByteString.Lazy.UTF8 (toString)
import Data.ByteString.Builder
import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8
import Data.Default
import Data.Functor.Contravariant
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

-- | Concats actions
instance Semigroup (Debugger s) where
  Debugger s
x <> :: Debugger s -> Debugger s -> Debugger s
<> Debugger s
y = (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
    (\s
input -> Debugger s -> s -> IO ()
forall s. Debugger s -> s -> IO ()
debugState Debugger s
x s
input          IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> s -> IO ()
forall s. Debugger s -> s -> IO ()
debugState Debugger s
y s
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugOption Debugger s
x Builder
input         IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugOption Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugLogic Debugger s
x Builder
input          IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugLogic Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugVar Debugger s
x Builder
input            IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugVar Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugAssert Debugger s
x Builder
input         IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugAssert Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugPop Debugger s
x Builder
input            IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugPop Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugCheckSat Debugger s
x Builder
input       IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugCheckSat Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugGetModel Debugger s
x Builder
input       IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugGetModel Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugGetValue Debugger s
x Builder
input       IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugGetValue Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMinimize Debugger s
x Builder
input       IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMinimize Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMaximize Debugger s
x Builder
input       IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMaximize Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMaximize Debugger s
x Builder
input       IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMaximize Debugger s
y Builder
input)
    (\Builder
input -> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugAssertSoft Debugger s
x Builder
input     IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugAssertSoft Debugger s
y Builder
input)
    (\ByteString
input -> Debugger s -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
debugResultResponse Debugger s
x ByteString
input IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
debugResultResponse Debugger s
y ByteString
input)
    (\ByteString
input -> Debugger s -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
debugModelResponse Debugger s
x ByteString
input  IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Debugger s -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
debugModelResponse Debugger s
y ByteString
input)

instance Monoid (Debugger s) where
  mempty :: Debugger s
mempty = Debugger s
forall s. Debugger s
silently

instance Contravariant Debugger where
  contramap :: forall a' a. (a' -> a) -> Debugger a -> Debugger a'
contramap a' -> a
f' Debugger a
debugger = Debugger a
debugger { debugState = f . f' }
    where
      f :: a -> IO ()
f = Debugger a -> a -> IO ()
forall s. Debugger s -> s -> IO ()
debugState Debugger a
debugger

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
"Bool Vars:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a. Seq a -> Int
Seq.length (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a b. (a -> b) -> a -> b
$ (Somes1 '[(~) SMTVar] '[KnownSMTSort] -> Bool)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a. (a -> Bool) -> Seq a -> Seq a
Seq.filter (\(Some1 f a
v) -> case SMTVar a -> SSMTSort a
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' f a
SMTVar a
v of SSMTSort a
SBoolSort -> Bool
True ; SSMTSort a
_ -> Bool
False) (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
 -> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a b. (a -> b) -> a -> b
$ SMT
sSMT
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     SMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall s a. s -> Getting a s a -> a
^.Getting
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
  SMT
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
Lens' SMT (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
vars)
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Arith Vars: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a. Seq a -> Int
Seq.length (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a b. (a -> b) -> a -> b
$ (Somes1 '[(~) SMTVar] '[KnownSMTSort] -> Bool)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a. (a -> Bool) -> Seq a -> Seq a
Seq.filter (\(Some1 f a
v) -> case SMTVar a -> SSMTSort a
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' f a
SMTVar a
v of SSMTSort a
SBoolSort -> Bool
False ; SSMTSort a
_ -> Bool
True) (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
 -> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a b. (a -> b) -> a -> b
$ SMT
sSMT
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     SMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall s a. s -> Getting a s a -> a
^.Getting
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
  SMT
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
Lens' SMT (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
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))
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Size:       " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Seq Integer -> Integer) -> Seq Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Expr 'BoolSort -> Integer) -> Seq (Expr 'BoolSort) -> Seq Integer
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'BoolSort -> Integer
forall (t :: SMTSort). KnownSMTSort t => Expr t -> Integer
exprSize (Seq (Expr 'BoolSort) -> Seq Integer)
-> Seq (Expr 'BoolSort) -> Seq Integer
forall a b. (a -> b) -> a -> b
$ 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
"Bool Vars:       " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a. Seq a -> Int
Seq.length (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a b. (a -> b) -> a -> b
$ (Somes1 '[(~) SMTVar] '[KnownSMTSort] -> Bool)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a. (a -> Bool) -> Seq a -> Seq a
Seq.filter (\(Some1 f a
v) -> case SMTVar a -> SSMTSort a
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' f a
SMTVar a
v of SSMTSort a
SBoolSort -> Bool
True ; SSMTSort a
_ -> Bool
False) (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
 -> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a b. (a -> b) -> a -> b
$ OMT
omtOMT
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     OMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall s a. s -> Getting a s a -> a
^.(SMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) SMT)
-> OMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) OMT
Lens' OMT SMT
smt((SMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) SMT)
 -> OMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) OMT)
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     SMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     OMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Getting
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
  SMT
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
Lens' SMT (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
vars)
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Arith Vars:      " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a. Seq a -> Int
Seq.length (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]) -> Int
forall a b. (a -> b) -> a -> b
$ (Somes1 '[(~) SMTVar] '[KnownSMTSort] -> Bool)
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a. (a -> Bool) -> Seq a -> Seq a
Seq.filter (\(Some1 f a
v) -> case SMTVar a -> SSMTSort a
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' f a
SMTVar a
v of SSMTSort a
SBoolSort -> Bool
False ; SSMTSort a
_ -> Bool
True) (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
 -> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall a b. (a -> b) -> a -> b
$ OMT
omtOMT
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     OMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])
forall s a. s -> Getting a s a -> a
^.(SMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) SMT)
-> OMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) OMT
Lens' OMT SMT
smt((SMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) SMT)
 -> OMT -> Const (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort])) OMT)
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     SMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
-> Getting
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
     OMT
     (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Getting
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
  SMT
  (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
Lens' SMT (Seq (Somes1 '[(~) SMTVar] '[KnownSMTSort]))
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))
      let omtSize :: Integer
omtSize = Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Expr 'BoolSort -> Integer) -> Seq (Expr 'BoolSort) -> Seq Integer
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'BoolSort -> Integer
forall (t :: SMTSort). KnownSMTSort t => Expr t -> Integer
exprSize (Seq (Expr 'BoolSort) -> Seq Integer)
-> Seq (Expr 'BoolSort) -> Seq Integer
forall a b. (a -> b) -> a -> b
$ 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)
                  Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((SoftFormula -> Integer) -> Seq SoftFormula -> Seq Integer
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Expr 'BoolSort -> Integer
forall (t :: SMTSort). KnownSMTSort t => Expr t -> Integer
exprSize (Expr 'BoolSort -> Integer)
-> (SoftFormula -> Expr 'BoolSort) -> SoftFormula -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Expr 'BoolSort) SoftFormula (Expr 'BoolSort)
-> SoftFormula -> Expr 'BoolSort
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Expr 'BoolSort) SoftFormula (Expr 'BoolSort)
Lens' SoftFormula (Expr 'BoolSort)
formula) (Seq SoftFormula -> Seq Integer) -> Seq SoftFormula -> Seq Integer
forall a b. (a -> b) -> a -> b
$ 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)
                  Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((SomeKnownSMTSort Minimize -> Integer)
-> Seq (SomeKnownSMTSort Minimize) -> Seq Integer
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Some1 (Minimize Expr a
expr)) -> Expr a -> Integer
forall (t :: SMTSort). KnownSMTSort t => Expr t -> Integer
exprSize Expr a
expr) (Seq (SomeKnownSMTSort Minimize) -> Seq Integer)
-> Seq (SomeKnownSMTSort Minimize) -> Seq Integer
forall a b. (a -> b) -> a -> b
$ 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)
                  Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((SomeKnownSMTSort Maximize -> Integer)
-> Seq (SomeKnownSMTSort Maximize) -> Seq Integer
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Some1 (Maximize Expr a
expr)) -> Expr a -> Integer
forall (t :: SMTSort). KnownSMTSort t => Expr t -> Integer
exprSize Expr a
expr) (Seq (SomeKnownSMTSort Maximize) -> Seq Integer)
-> Seq (SomeKnownSMTSort Maximize) -> Seq Integer
forall a b. (a -> b) -> a -> b
$ 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)
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Size:            " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
omtSize
    }