{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE OverloadedStrings #-}

-- | This is a wrapper around IO that permits SMT queries

module Language.Fixpoint.Solver.Monad
       ( -- * Type
         SolveM

         -- * Execution
       , runSolverM

         -- * Get Binds
       , getBinds

         -- * SMT Query
       , filterRequired
       , filterValid
       , filterValidGradual
       , checkSat
       , smtEnablembqi

         -- * Debug
       , Stats
       , tickIter
       , stats
       , numIter
       )
       where

import           Language.Fixpoint.Utils.Progress
import qualified Language.Fixpoint.Types.Config  as C
import           Language.Fixpoint.Types.Config  (Config)
import qualified Language.Fixpoint.Types   as F
-- import qualified Language.Fixpoint.Misc    as Misc
-- import           Language.Fixpoint.SortCheck
import qualified Language.Fixpoint.Types.Solutions as F
-- import qualified Language.Fixpoint.Types.Errors  as E
import           Language.Fixpoint.Smt.Serialize ()
import           Language.Fixpoint.Types.PrettyPrint ()
import           Language.Fixpoint.Smt.Interface
-- import qualified Language.Fixpoint.Smt.Theories as Thy
import           Language.Fixpoint.Solver.Sanitize
import           Language.Fixpoint.Solver.Stats
import           Language.Fixpoint.Graph.Types (SolverInfo (..))
-- import           Language.Fixpoint.Solver.Solution
-- import           Data.Maybe           (catMaybes)
import           Data.List            (partition)
-- import           Data.Char            (isUpper)
import           Control.Monad.State.Strict
import qualified Data.HashMap.Strict as M
import           Data.Maybe (catMaybes)
import           Control.Exception.Base (bracket)

--------------------------------------------------------------------------------
-- | Solver Monadic API --------------------------------------------------------
--------------------------------------------------------------------------------

type SolveM = StateT SolverState IO

data SolverState = SS 
  { SolverState -> Context
ssCtx     :: !Context          -- ^ SMT Solver Context
  , SolverState -> BindEnv
ssBinds   :: !F.BindEnv        -- ^ All variables and types
  , SolverState -> Stats
ssStats   :: !Stats            -- ^ Solver Statistics
  }

stats0    :: F.GInfo c b -> Stats
stats0 :: GInfo c b -> Stats
stats0 GInfo c b
fi = Int -> Int -> Int -> Int -> Int -> Stats
Stats Int
nCs Int
0 Int
0 Int
0 Int
0
  where
    nCs :: Int
nCs   = HashMap SubcId (c b) -> Int
forall k v. HashMap k v -> Int
M.size (HashMap SubcId (c b) -> Int) -> HashMap SubcId (c b) -> Int
forall a b. (a -> b) -> a -> b
$ GInfo c b -> HashMap SubcId (c b)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c b
fi

--------------------------------------------------------------------------------
runSolverM :: Config -> SolverInfo b c -> SolveM a -> IO a
--------------------------------------------------------------------------------
runSolverM :: Config -> SolverInfo b c -> SolveM a -> IO a
runSolverM Config
cfg SolverInfo b c
sI SolveM a
act =
  IO Context -> (Context -> IO ExitCode) -> (Context -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket IO Context
acquire Context -> IO ExitCode
release ((Context -> IO a) -> IO a) -> (Context -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \Context
ctx -> do
    (a, SolverState)
res <- SolveM a -> SolverState -> IO (a, SolverState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SolveM a
act' (Context -> SolverState
s0 Context
ctx)
    Context -> Raw -> IO ()
smtWrite Context
ctx Raw
"(exit)"
    a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, SolverState) -> a
forall a b. (a, b) -> a
fst (a, SolverState)
res)
  where
    s0 :: Context -> SolverState
s0 Context
ctx   = Context -> BindEnv -> Stats -> SolverState
SS Context
ctx BindEnv
be (GInfo SimpC b -> Stats
forall (c :: * -> *) b. GInfo c b -> Stats
stats0 GInfo SimpC b
fi)
    act' :: SolveM a
act'     = [Triggered Expr] -> SolveM ()
assumesAxioms (GInfo SimpC b -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
F.asserts GInfo SimpC b
fi) SolveM () -> SolveM a -> SolveM a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SolveM a
act
    release :: Context -> IO ExitCode
release  = Context -> IO ExitCode
cleanupContext
    acquire :: IO Context
acquire  = Config -> FilePath -> SymEnv -> IO Context
makeContextWithSEnv Config
cfg FilePath
file SymEnv
initEnv
    initEnv :: SymEnv
initEnv  = Config -> GInfo SimpC b -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv   Config
cfg GInfo SimpC b
fi
    be :: BindEnv
be       = GInfo SimpC b -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs GInfo SimpC b
fi
    file :: FilePath
file     = Config -> FilePath
C.srcFile Config
cfg
    -- only linear arithmentic when: linear flag is on or solver /= Z3
    -- lar     = linear cfg || Z3 /= solver cfg
    fi :: GInfo SimpC b
fi       = (SolverInfo b c -> GInfo SimpC b
forall a b. SolverInfo a b -> SInfo a
siQuery SolverInfo b c
sI) {hoInfo :: HOInfo
F.hoInfo = Bool -> Bool -> HOInfo
F.HOI (Config -> Bool
C.allowHO Config
cfg) (Config -> Bool
C.allowHOqs Config
cfg)}


--------------------------------------------------------------------------------
getBinds :: SolveM F.BindEnv 
--------------------------------------------------------------------------------
getBinds :: SolveM BindEnv
getBinds = SolverState -> BindEnv
ssBinds (SolverState -> BindEnv)
-> StateT SolverState IO SolverState -> SolveM BindEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SolverState IO SolverState
forall s (m :: * -> *). MonadState s m => m s
get

--------------------------------------------------------------------------------
getIter :: SolveM Int
--------------------------------------------------------------------------------
getIter :: SolveM Int
getIter = Stats -> Int
numIter (Stats -> Int) -> (SolverState -> Stats) -> SolverState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverState -> Stats
ssStats (SolverState -> Int)
-> StateT SolverState IO SolverState -> SolveM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SolverState IO SolverState
forall s (m :: * -> *). MonadState s m => m s
get

--------------------------------------------------------------------------------
incIter, incBrkt :: SolveM ()
--------------------------------------------------------------------------------
incIter :: SolveM ()
incIter   = (Stats -> Stats) -> SolveM ()
modifyStats ((Stats -> Stats) -> SolveM ()) -> (Stats -> Stats) -> SolveM ()
forall a b. (a -> b) -> a -> b
$ \Stats
s -> Stats
s {numIter :: Int
numIter = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numIter Stats
s}
incBrkt :: SolveM ()
incBrkt   = (Stats -> Stats) -> SolveM ()
modifyStats ((Stats -> Stats) -> SolveM ()) -> (Stats -> Stats) -> SolveM ()
forall a b. (a -> b) -> a -> b
$ \Stats
s -> Stats
s {numBrkt :: Int
numBrkt = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numBrkt Stats
s}

--------------------------------------------------------------------------------
incChck, incVald :: Int -> SolveM ()
--------------------------------------------------------------------------------
incChck :: Int -> SolveM ()
incChck Int
n = (Stats -> Stats) -> SolveM ()
modifyStats ((Stats -> Stats) -> SolveM ()) -> (Stats -> Stats) -> SolveM ()
forall a b. (a -> b) -> a -> b
$ \Stats
s -> Stats
s {numChck :: Int
numChck = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numChck Stats
s}
incVald :: Int -> SolveM ()
incVald Int
n = (Stats -> Stats) -> SolveM ()
modifyStats ((Stats -> Stats) -> SolveM ()) -> (Stats -> Stats) -> SolveM ()
forall a b. (a -> b) -> a -> b
$ \Stats
s -> Stats
s {numVald :: Int
numVald = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numVald Stats
s}

withContext :: (Context -> IO a) -> SolveM a
withContext :: (Context -> IO a) -> SolveM a
withContext Context -> IO a
k = (IO a -> SolveM a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO a -> SolveM a) -> (Context -> IO a) -> Context -> SolveM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> IO a
k) (Context -> SolveM a) -> StateT SolverState IO Context -> SolveM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< StateT SolverState IO Context
getContext

getContext :: SolveM Context
getContext :: StateT SolverState IO Context
getContext = SolverState -> Context
ssCtx (SolverState -> Context)
-> StateT SolverState IO SolverState
-> StateT SolverState IO Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SolverState IO SolverState
forall s (m :: * -> *). MonadState s m => m s
get

modifyStats :: (Stats -> Stats) -> SolveM ()
modifyStats :: (Stats -> Stats) -> SolveM ()
modifyStats Stats -> Stats
f = (SolverState -> SolverState) -> SolveM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SolverState -> SolverState) -> SolveM ())
-> (SolverState -> SolverState) -> SolveM ()
forall a b. (a -> b) -> a -> b
$ \SolverState
s -> SolverState
s { ssStats :: Stats
ssStats = Stats -> Stats
f (SolverState -> Stats
ssStats SolverState
s) }

--------------------------------------------------------------------------------
-- | SMT Interface -------------------------------------------------------------
--------------------------------------------------------------------------------
-- | `filterRequired [(x1, p1),...,(xn, pn)] q` returns a minimal list [xi] s.t.
--   /\ [pi] => q
--------------------------------------------------------------------------------
filterRequired :: F.Cand a -> F.Expr -> SolveM [a]
--------------------------------------------------------------------------------
filterRequired :: Cand a -> Expr -> SolveM [a]
filterRequired = FilePath -> Cand a -> Expr -> SolveM [a]
forall a. HasCallStack => FilePath -> a
error FilePath
"TBD:filterRequired"

{-
(set-option :produce-unsat-cores true)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)

; Z3 will only track assertions that are named.

(assert (< 0 x))
(assert (! (< 0 y)       :named b2))
(assert (! (< x 10)      :named b3))
(assert (! (< y 10)      :named b4))
(assert (! (< (+ x y) 0) :named bR))
(check-sat)
(get-unsat-core)

> unsat (b2 bR)
-}

--------------------------------------------------------------------------------
-- | `filterValid p [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]`
--------------------------------------------------------------------------------
filterValid :: F.SrcSpan -> F.Expr -> F.Cand a -> SolveM [a]
--------------------------------------------------------------------------------
filterValid :: SrcSpan -> Expr -> Cand a -> SolveM [a]
filterValid SrcSpan
sp Expr
p Cand a
qs = do
  [a]
qs' <- (Context -> IO [a]) -> SolveM [a]
forall a. (Context -> IO a) -> SolveM a
withContext ((Context -> IO [a]) -> SolveM [a])
-> (Context -> IO [a]) -> SolveM [a]
forall a b. (a -> b) -> a -> b
$ \Context
me ->
           Context -> FilePath -> IO [a] -> IO [a]
forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"filterValidLHS" (IO [a] -> IO [a]) -> IO [a] -> IO [a]
forall a b. (a -> b) -> a -> b
$
             SrcSpan -> Expr -> Cand a -> Context -> IO [a]
forall a. SrcSpan -> Expr -> Cand a -> Context -> IO [a]
filterValid_ SrcSpan
sp Expr
p Cand a
qs Context
me
  -- stats
  SolveM ()
incBrkt
  Int -> SolveM ()
incChck (Cand a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Cand a
qs)
  Int -> SolveM ()
incVald ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
qs')
  [a] -> SolveM [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
qs'

filterValid_ :: F.SrcSpan -> F.Expr -> F.Cand a -> Context -> IO [a]
filterValid_ :: SrcSpan -> Expr -> Cand a -> Context -> IO [a]
filterValid_ SrcSpan
sp Expr
p Cand a
qs Context
me = [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe a] -> [a]) -> IO [Maybe a] -> IO [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  Context -> Expr -> IO ()
smtAssert Context
me Expr
p
  Cand a -> ((Expr, a) -> IO (Maybe a)) -> IO [Maybe a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Cand a
qs (((Expr, a) -> IO (Maybe a)) -> IO [Maybe a])
-> ((Expr, a) -> IO (Maybe a)) -> IO [Maybe a]
forall a b. (a -> b) -> a -> b
$ \(Expr
q, a
x) ->
    SrcSpan -> Context -> FilePath -> IO (Maybe a) -> IO (Maybe a)
forall a. SrcSpan -> Context -> FilePath -> IO a -> IO a
smtBracketAt SrcSpan
sp Context
me FilePath
"filterValidRHS" (IO (Maybe a) -> IO (Maybe a)) -> IO (Maybe a) -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
      Context -> Expr -> IO ()
smtAssert Context
me (Expr -> Expr
F.PNot Expr
q)
      Bool
valid <- Context -> IO Bool
smtCheckUnsat Context
me
      Maybe a -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> IO (Maybe a)) -> Maybe a -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ if Bool
valid then a -> Maybe a
forall a. a -> Maybe a
Just a
x else Maybe a
forall a. Maybe a
Nothing


--------------------------------------------------------------------------------
-- | `filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]`
-- | for some p in the list ps
--------------------------------------------------------------------------------
filterValidGradual :: [F.Expr] -> F.Cand a -> SolveM [a]
--------------------------------------------------------------------------------
filterValidGradual :: [Expr] -> Cand a -> SolveM [a]
filterValidGradual [Expr]
p Cand a
qs = do
  [a]
qs' <- (Context -> IO [a]) -> SolveM [a]
forall a. (Context -> IO a) -> SolveM a
withContext ((Context -> IO [a]) -> SolveM [a])
-> (Context -> IO [a]) -> SolveM [a]
forall a b. (a -> b) -> a -> b
$ \Context
me ->
           Context -> FilePath -> IO [a] -> IO [a]
forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"filterValidGradualLHS" (IO [a] -> IO [a]) -> IO [a] -> IO [a]
forall a b. (a -> b) -> a -> b
$
             [Expr] -> Cand a -> Context -> IO [a]
forall a. [Expr] -> Cand a -> Context -> IO [a]
filterValidGradual_ [Expr]
p Cand a
qs Context
me
  -- stats
  SolveM ()
incBrkt
  Int -> SolveM ()
incChck (Cand a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Cand a
qs)
  Int -> SolveM ()
incVald ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
qs')
  [a] -> SolveM [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
qs'

filterValidGradual_ :: [F.Expr] -> F.Cand a -> Context -> IO [a]
filterValidGradual_ :: [Expr] -> Cand a -> Context -> IO [a]
filterValidGradual_ [Expr]
ps Cand a
qs Context
me
  = (((Expr, a) -> a) -> Cand a -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, a) -> a
forall a b. (a, b) -> b
snd (Cand a -> [a])
-> ((Cand a, Cand a) -> Cand a) -> (Cand a, Cand a) -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cand a, Cand a) -> Cand a
forall a b. (a, b) -> a
fst) ((Cand a, Cand a) -> [a]) -> IO (Cand a, Cand a) -> IO [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Cand a, Cand a) -> Expr -> IO (Cand a, Cand a))
-> (Cand a, Cand a) -> [Expr] -> IO (Cand a, Cand a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Cand a, Cand a) -> Expr -> IO (Cand a, Cand a)
forall a. (Cand a, Cand a) -> Expr -> IO (Cand a, Cand a)
partitionCandidates ([], Cand a
qs) [Expr]
ps
  where
    partitionCandidates :: (F.Cand a, F.Cand a) -> F.Expr -> IO (F.Cand a, F.Cand a)
    partitionCandidates :: (Cand a, Cand a) -> Expr -> IO (Cand a, Cand a)
partitionCandidates (Cand a
ok, Cand a
candidates) Expr
p = do
      ([((Expr, a), Bool)]
valids', [((Expr, a), Bool)]
invalids')  <- (((Expr, a), Bool) -> Bool)
-> [((Expr, a), Bool)]
-> ([((Expr, a), Bool)], [((Expr, a), Bool)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Expr, a), Bool) -> Bool
forall a b. (a, b) -> b
snd ([((Expr, a), Bool)] -> ([((Expr, a), Bool)], [((Expr, a), Bool)]))
-> IO [((Expr, a), Bool)]
-> IO ([((Expr, a), Bool)], [((Expr, a), Bool)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Cand a -> Context -> IO [((Expr, a), Bool)]
forall a. Expr -> Cand a -> Context -> IO [((Expr, a), Bool)]
filterValidOne_ Expr
p Cand a
candidates Context
me
      let (Cand a
valids, Cand a
invalids) = (((Expr, a), Bool) -> (Expr, a)
forall a b. (a, b) -> a
fst (((Expr, a), Bool) -> (Expr, a)) -> [((Expr, a), Bool)] -> Cand a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((Expr, a), Bool)]
valids', ((Expr, a), Bool) -> (Expr, a)
forall a b. (a, b) -> a
fst (((Expr, a), Bool) -> (Expr, a)) -> [((Expr, a), Bool)] -> Cand a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((Expr, a), Bool)]
invalids')
      (Cand a, Cand a) -> IO (Cand a, Cand a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Cand a
ok Cand a -> Cand a -> Cand a
forall a. [a] -> [a] -> [a]
++ Cand a
valids, Cand a
invalids)

filterValidOne_ :: F.Expr -> F.Cand a -> Context -> IO [((F.Expr, a), Bool)]
filterValidOne_ :: Expr -> Cand a -> Context -> IO [((Expr, a), Bool)]
filterValidOne_ Expr
p Cand a
qs Context
me = do
  Context -> Expr -> IO ()
smtAssert Context
me Expr
p
  Cand a
-> ((Expr, a) -> IO ((Expr, a), Bool)) -> IO [((Expr, a), Bool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Cand a
qs (((Expr, a) -> IO ((Expr, a), Bool)) -> IO [((Expr, a), Bool)])
-> ((Expr, a) -> IO ((Expr, a), Bool)) -> IO [((Expr, a), Bool)]
forall a b. (a -> b) -> a -> b
$ \(Expr
q, a
x) ->
    Context -> FilePath -> IO ((Expr, a), Bool) -> IO ((Expr, a), Bool)
forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"filterValidRHS" (IO ((Expr, a), Bool) -> IO ((Expr, a), Bool))
-> IO ((Expr, a), Bool) -> IO ((Expr, a), Bool)
forall a b. (a -> b) -> a -> b
$ do
      Context -> Expr -> IO ()
smtAssert Context
me (Expr -> Expr
F.PNot Expr
q)
      Bool
valid <- Context -> IO Bool
smtCheckUnsat Context
me
      ((Expr, a), Bool) -> IO ((Expr, a), Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (((Expr, a), Bool) -> IO ((Expr, a), Bool))
-> ((Expr, a), Bool) -> IO ((Expr, a), Bool)
forall a b. (a -> b) -> a -> b
$ ((Expr
q, a
x), Bool
valid)

smtEnablembqi :: SolveM ()
smtEnablembqi :: SolveM ()
smtEnablembqi
  = (Context -> IO ()) -> SolveM ()
forall a. (Context -> IO a) -> SolveM a
withContext ((Context -> IO ()) -> SolveM ())
-> (Context -> IO ()) -> SolveM ()
forall a b. (a -> b) -> a -> b
$ \Context
me ->
      Context -> Raw -> IO ()
smtWrite Context
me Raw
"(set-option :smt.mbqi true)"

--------------------------------------------------------------------------------
checkSat :: F.Expr -> SolveM  Bool
--------------------------------------------------------------------------------
checkSat :: Expr -> SolveM Bool
checkSat Expr
p
  = (Context -> IO Bool) -> SolveM Bool
forall a. (Context -> IO a) -> SolveM a
withContext ((Context -> IO Bool) -> SolveM Bool)
-> (Context -> IO Bool) -> SolveM Bool
forall a b. (a -> b) -> a -> b
$ \Context
me ->
      Context -> FilePath -> IO Bool -> IO Bool
forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"checkSat" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
        Context -> Expr -> IO Bool
smtCheckSat Context
me Expr
p

--------------------------------------------------------------------------------
assumesAxioms :: [F.Triggered F.Expr] -> SolveM ()
--------------------------------------------------------------------------------
assumesAxioms :: [Triggered Expr] -> SolveM ()
assumesAxioms [Triggered Expr]
es = (Context -> IO ()) -> SolveM ()
forall a. (Context -> IO a) -> SolveM a
withContext ((Context -> IO ()) -> SolveM ())
-> (Context -> IO ()) -> SolveM ()
forall a b. (a -> b) -> a -> b
$ \Context
me -> [Triggered Expr] -> (Triggered Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_  [Triggered Expr]
es ((Triggered Expr -> IO ()) -> IO ())
-> (Triggered Expr -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Triggered Expr -> IO ()
smtAssertAxiom Context
me


---------------------------------------------------------------------------
stats :: SolveM Stats
---------------------------------------------------------------------------
stats :: SolveM Stats
stats = SolverState -> Stats
ssStats (SolverState -> Stats)
-> StateT SolverState IO SolverState -> SolveM Stats
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SolverState IO SolverState
forall s (m :: * -> *). MonadState s m => m s
get

---------------------------------------------------------------------------
tickIter :: Bool -> SolveM Int
---------------------------------------------------------------------------
tickIter :: Bool -> SolveM Int
tickIter Bool
newScc = Bool -> SolveM ()
progIter Bool
newScc SolveM () -> SolveM () -> SolveM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SolveM ()
incIter SolveM () -> SolveM Int -> SolveM Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SolveM Int
getIter

progIter :: Bool -> SolveM ()
progIter :: Bool -> SolveM ()
progIter Bool
newScc = IO () -> SolveM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> SolveM ()) -> IO () -> SolveM ()
forall a b. (a -> b) -> a -> b
$ Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
newScc IO ()
progressTick