{-# LANGUAGE OverloadedStrings #-}

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

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

         -- * Execution
       , runSolverM

       , getContext

         -- * SMT Query
       , filterRequired
       , filterValid
       , smtEnablembqi
       , sendConcreteBindingsToSMT

         -- * Debug
       , Stats
       , tickIter
       , stats
       , numIter
       , SolverState(..)

       , modifyContext
       )
       where

import           Control.Monad (forM, forM_, when)
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.Visitor 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           Language.Fixpoint.Smt.Types (SmtM)
-- 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.Char            (isUpper)
import qualified Control.Monad.State as ST
import           Control.Monad.State.Strict
import qualified Data.HashMap.Strict as M
import           Data.Maybe (catMaybes)
import           Control.Exception.Base (bracket)
import Language.Fixpoint.SortCheck (ElabParam)

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

type SolveM ann = StateT (SolverState ann) IO

data SolverState ann = SS
  { forall ann. SolverState ann -> Context
ssCtx     :: !Context         -- ^ SMT Solver Context
  , forall ann. SolverState ann -> Stats
ssStats   :: !Stats           -- ^ Solver Statistics
  , forall ann. SolverState ann -> ElabParam
ssElabParam :: !ElabParam      -- ^ Elaboration Parameters
  }

stats0    :: F.GInfo c b -> Stats
stats0 :: forall (c :: * -> *) b. 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 ann -> ElabParam -> SolveM ann a -> IO a
--------------------------------------------------------------------------------
runSolverM :: forall ann a.
Config -> SolverInfo ann -> ElabParam -> SolveM ann a -> IO a
runSolverM Config
cfg SolverInfo ann
sI ElabParam
elabParam SolveM ann a
act =
  IO Context -> (Context -> IO ()) -> (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 ()
release ((Context -> IO a) -> IO a) -> (Context -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \Context
ctx -> do
    (a, SolverState ann)
res <- SolveM ann a -> SolverState ann -> IO (a, SolverState ann)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SolveM ann a
act' (Context -> SolverState ann
forall {ann}. Context -> SolverState ann
s0 Context
ctx)
    a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, SolverState ann) -> a
forall a b. (a, b) -> a
fst (a, SolverState ann)
res)
  where
    s0 :: Context -> SolverState ann
s0 Context
ctx   = Context -> Stats -> ElabParam -> SolverState ann
forall ann. Context -> Stats -> ElabParam -> SolverState ann
SS Context
ctx (GInfo SimpC ann -> Stats
forall (c :: * -> *) b. GInfo c b -> Stats
stats0 GInfo SimpC ann
fi) ElabParam
elabParam
    act' :: SolveM ann a
act'     = [Triggered Expr] -> SolveM ann ()
forall ann. [Triggered Expr] -> SolveM ann ()
assumesAxioms (GInfo SimpC ann -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
F.asserts GInfo SimpC ann
fi) SolveM ann () -> SolveM ann a -> SolveM ann a
forall a b.
StateT (SolverState ann) IO a
-> StateT (SolverState ann) IO b -> StateT (SolverState ann) IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SolveM ann a
act
    release :: Context -> IO ()
release  = Context -> IO ()
cleanupContext
    acquire :: IO Context
acquire  = Config -> FilePath -> SymEnv -> DefinedFuns -> IO Context
makeContextWithSEnv Config
cfg FilePath
file SymEnv
initEnv (GInfo SimpC ann -> DefinedFuns
forall (c :: * -> *) a. GInfo c a -> DefinedFuns
F.defns GInfo SimpC ann
fi)
    initEnv :: SymEnv
initEnv  = Config -> GInfo SimpC ann -> SymEnv
forall a. HasCallStack => Config -> SInfo a -> SymEnv
symbolEnv Config
cfg GInfo SimpC ann
fi
    file :: FilePath
file     = Config -> FilePath
C.srcFile Config
cfg
    -- only linear arithmetic when: linear flag is on or solver /= Z3
    -- lar     = linear cfg || Z3 /= solver cfg
    fi :: GInfo SimpC ann
fi       = (SolverInfo ann -> GInfo SimpC ann
forall a. SolverInfo a -> SInfo a
siQuery SolverInfo ann
sI) {F.hoInfo = F.cfgHoInfo cfg }

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

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

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

liftSMT :: SmtM a -> SolveM ann a
liftSMT :: forall a ann. SmtM a -> SolveM ann a
liftSMT SmtM a
k =
  do SolverState ann
es <- StateT (SolverState ann) IO (SolverState ann)
forall s (m :: * -> *). MonadState s m => m s
get
     let ctx :: Context
ctx = SolverState ann -> Context
forall ann. SolverState ann -> Context
ssCtx SolverState ann
es
     (a
a, Context
ctx') <- IO (a, Context) -> StateT (SolverState ann) IO (a, Context)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState ann) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (a, Context) -> StateT (SolverState ann) IO (a, Context))
-> IO (a, Context) -> StateT (SolverState ann) IO (a, Context)
forall a b. (a -> b) -> a -> b
$ SmtM a -> Context -> IO (a, Context)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
ST.runStateT SmtM a
k Context
ctx
     SolverState ann -> StateT (SolverState ann) IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (SolverState ann
es {ssCtx = ctx'})
     a -> SolveM ann a
forall a. a -> StateT (SolverState ann) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

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

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

modifyContext :: (Context -> Context) -> SolveM ann ()
modifyContext :: forall ann. (Context -> Context) -> SolveM ann ()
modifyContext Context -> Context
f = (SolverState ann -> SolverState ann)
-> StateT (SolverState ann) IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SolverState ann -> SolverState ann)
 -> StateT (SolverState ann) IO ())
-> (SolverState ann -> SolverState ann)
-> StateT (SolverState ann) IO ()
forall a b. (a -> b) -> a -> b
$ \SolverState ann
s -> SolverState ann
s { ssCtx = f (ssCtx s) }

--------------------------------------------------------------------------------
-- | SMT Interface -------------------------------------------------------------
--------------------------------------------------------------------------------

-- | Takes the environment of bindings already known to the SMT,
-- and the environment of all bindings that need to be known.
--
-- Yields the ids of bindings known to the SMT
sendConcreteBindingsToSMT
  :: F.IBindEnv -> F.BindEnv ann -> (F.IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT :: forall ann a.
IBindEnv
-> BindEnv ann -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
known BindEnv ann
be IBindEnv -> SolveM ann a
act = do
  let concretePreds :: [(Int, Expr)]
concretePreds =
        [ (Int
i, Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Expr
p (Symbol
v, Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
s))
        | (Int
i, (Symbol
s, F.RR Sort
_ (F.Reft (Symbol
v, Expr
p)),ann
_)) <- BindEnv ann -> [(Int, (Symbol, SortedReft, ann))]
forall a. BindEnv a -> [(Int, (Symbol, SortedReft, a))]
F.bindEnvToList BindEnv ann
be
        , Expr -> Bool
F.isConc Expr
p
        , Bool -> Bool
not (Expr -> Bool
forall {v}. ExprV v -> Bool
isShortExpr Expr
p)
        , Bool -> Bool
not (Int -> IBindEnv -> Bool
F.memberIBindEnv Int
i IBindEnv
known)
        ]
  SolverState ann
st <- StateT (SolverState ann) IO (SolverState ann)
forall s (m :: * -> *). MonadState s m => m s
get
  (a
a, SolverState ann
st'') <- SmtM (a, SolverState ann) -> SolveM ann (a, SolverState ann)
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM (a, SolverState ann) -> SolveM ann (a, SolverState ann))
-> SmtM (a, SolverState ann) -> SolveM ann (a, SolverState ann)
forall a b. (a -> b) -> a -> b
$
    FilePath -> SmtM (a, SolverState ann) -> SmtM (a, SolverState ann)
forall a. FilePath -> SmtM a -> SmtM a
smtBracket FilePath
"sendConcreteBindingsToSMT" (SmtM (a, SolverState ann) -> SmtM (a, SolverState ann))
-> SmtM (a, SolverState ann) -> SmtM (a, SolverState ann)
forall a b. (a -> b) -> a -> b
$ do
      [(Int, Expr)]
-> ((Int, Expr) -> StateT Context IO ()) -> StateT Context IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Expr)]
concretePreds (((Int, Expr) -> StateT Context IO ()) -> StateT Context IO ())
-> ((Int, Expr) -> StateT Context IO ()) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
i, Expr
e) ->
        Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> StateT Context IO ()
smtDefineFunc (SubcId -> Symbol
F.bindSymbol (Int -> SubcId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)) [] Sort
F.boolSort Expr
e
      Context
ctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
      let st' :: SolverState ann
st' = SolverState ann
st { ssCtx = ctx }
      (a
a, SolverState ann
st'') <- IO (a, SolverState ann) -> SmtM (a, SolverState ann)
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (a, SolverState ann) -> SmtM (a, SolverState ann))
-> IO (a, SolverState ann) -> SmtM (a, SolverState ann)
forall a b. (a -> b) -> a -> b
$ (SolveM ann a -> SolverState ann -> IO (a, SolverState ann))
-> SolverState ann -> SolveM ann a -> IO (a, SolverState ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SolveM ann a -> SolverState ann -> IO (a, SolverState ann)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SolverState ann
forall {ann}. SolverState ann
st' (SolveM ann a -> IO (a, SolverState ann))
-> SolveM ann a -> IO (a, SolverState ann)
forall a b. (a -> b) -> a -> b
$ IBindEnv -> SolveM ann a
act (IBindEnv -> SolveM ann a) -> IBindEnv -> SolveM ann a
forall a b. (a -> b) -> a -> b
$ IBindEnv -> IBindEnv -> IBindEnv
F.unionIBindEnv IBindEnv
known (IBindEnv -> IBindEnv) -> IBindEnv -> IBindEnv
forall a b. (a -> b) -> a -> b
$ [Int] -> IBindEnv
F.fromListIBindEnv ([Int] -> IBindEnv) -> [Int] -> IBindEnv
forall a b. (a -> b) -> a -> b
$ ((Int, Expr) -> Int) -> [(Int, Expr)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Expr) -> Int
forall a b. (a, b) -> a
fst [(Int, Expr)]
concretePreds
      Context -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (SolverState ann -> Context
forall ann. SolverState ann -> Context
ssCtx SolverState ann
st'')
      (a, SolverState ann) -> SmtM (a, SolverState ann)
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, SolverState ann
st'')
  (SolverState ann -> SolverState ann)
-> StateT (SolverState ann) IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SolverState ann -> SolverState ann)
 -> StateT (SolverState ann) IO ())
-> (SolverState ann -> SolverState ann)
-> StateT (SolverState ann) IO ()
forall a b. (a -> b) -> a -> b
$ \SolverState ann
st''' -> SolverState ann
st'' { ssCtx = ssCtx st''' }
  a -> SolveM ann a
forall a. a -> StateT (SolverState ann) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  where
    isShortExpr :: ExprV v -> Bool
isShortExpr ExprV v
F.PTrue = Bool
True
    isShortExpr ExprV v
F.PTop = Bool
True
    isShortExpr ExprV v
_ = Bool
False

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

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

{-# SCC filterValid_ #-}
filterValid_ :: F.SrcSpan -> F.Expr -> F.Cand a -> SmtM [a]
filterValid_ :: forall a. SrcSpan -> Expr -> Cand a -> SmtM [a]
filterValid_ SrcSpan
sp Expr
p Cand a
qs = [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe a] -> [a])
-> StateT Context IO [Maybe a] -> StateT Context IO [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  HasCallStack => Expr -> StateT Context IO ()
Expr -> StateT Context IO ()
smtAssertDecl Expr
p
  Cand a
-> ((Expr, a) -> StateT Context IO (Maybe a))
-> StateT Context 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) -> StateT Context IO (Maybe a))
 -> StateT Context IO [Maybe a])
-> ((Expr, a) -> StateT Context IO (Maybe a))
-> StateT Context IO [Maybe a]
forall a b. (a -> b) -> a -> b
$ \(Expr
q, a
x) ->
    SrcSpan
-> FilePath
-> StateT Context IO (Maybe a)
-> StateT Context IO (Maybe a)
forall a. SrcSpan -> FilePath -> SmtM a -> SmtM a
smtBracketAt SrcSpan
sp FilePath
"filterValidRHS" (StateT Context IO (Maybe a) -> StateT Context IO (Maybe a))
-> StateT Context IO (Maybe a) -> StateT Context IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
      HasCallStack => Expr -> StateT Context IO ()
Expr -> StateT Context IO ()
smtAssertDecl (Expr -> Expr
forall v. ExprV v -> ExprV v
F.PNot Expr
q)
      Bool
valid <- SmtM Bool
HasCallStack => SmtM Bool
smtCheckUnsat
      Maybe a -> StateT Context IO (Maybe a)
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> StateT Context IO (Maybe a))
-> Maybe a -> StateT Context 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

smtEnablembqi :: SolveM ann ()
smtEnablembqi :: forall ann. SolveM ann ()
smtEnablembqi
  = StateT Context IO () -> SolveM ann ()
forall a ann. SmtM a -> SolveM ann a
liftSMT StateT Context IO ()
smtSetMbqi

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


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

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

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