{-# LANGUAGE OverloadedStrings #-}

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

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

         -- * Execution
       , runSolverM

         -- * Get Binds
       , getBinds
       , getContext

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

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

import           Control.Monad (foldM, 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 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 ann = StateT (SolverState ann) IO

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

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 c -> SolveM ann a -> IO a
--------------------------------------------------------------------------------
runSolverM :: forall ann c a. Config -> SolverInfo ann c -> SolveM ann a -> IO a
runSolverM Config
cfg SolverInfo ann c
sI 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
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 -> BindEnv ann -> Stats -> SolverState ann
forall ann. Context -> BindEnv ann -> Stats -> SolverState ann
SS Context
ctx BindEnv ann
be (GInfo SimpC ann -> Stats
forall (c :: * -> *) b. GInfo c b -> Stats
stats0 GInfo SimpC ann
fi)
    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 -> [Equation] -> IO Context
makeContextWithSEnv Config
cfg FilePath
file SymEnv
initEnv (GInfo SimpC ann -> [Equation]
forall (c :: * -> *) a. GInfo c a -> [Equation]
F.defns GInfo SimpC ann
fi)
    initEnv :: SymEnv
initEnv  = Config -> GInfo SimpC ann -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg GInfo SimpC ann
fi
    be :: BindEnv ann
be       = GInfo SimpC ann -> BindEnv ann
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs 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 c -> GInfo SimpC ann
forall a b. SolverInfo a b -> SInfo a
siQuery SolverInfo ann c
sI) {F.hoInfo = F.cfgHoInfo cfg }


--------------------------------------------------------------------------------
getBinds :: SolveM ann (F.BindEnv ann)
--------------------------------------------------------------------------------
getBinds :: forall ann. SolveM ann (BindEnv ann)
getBinds = SolverState ann -> BindEnv ann
forall ann. SolverState ann -> BindEnv ann
ssBinds (SolverState ann -> BindEnv ann)
-> StateT (SolverState ann) IO (SolverState ann)
-> StateT (SolverState ann) IO (BindEnv ann)
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

--------------------------------------------------------------------------------
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}

withContext :: (Context -> IO a) -> SolveM ann a
withContext :: forall a ann. (Context -> IO a) -> SolveM ann a
withContext Context -> IO a
k = (IO a -> StateT (SolverState ann) IO a
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 -> StateT (SolverState ann) IO a)
-> (Context -> IO a) -> Context -> StateT (SolverState ann) IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> IO a
k) (Context -> StateT (SolverState ann) IO a)
-> StateT (SolverState ann) IO Context
-> StateT (SolverState ann) IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< StateT (SolverState ann) IO Context
forall ann. SolveM ann Context
getContext

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) }

--------------------------------------------------------------------------------
-- | 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.IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT :: forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
known IBindEnv -> SolveM ann a
act = do
  BindEnv ann
be <- SolveM ann (BindEnv ann)
forall ann. SolveM ann (BindEnv ann)
getBinds
  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') <- (Context -> IO (a, SolverState ann))
-> SolveM ann (a, SolverState ann)
forall a ann. (Context -> IO a) -> SolveM ann a
withContext ((Context -> IO (a, SolverState ann))
 -> SolveM ann (a, SolverState ann))
-> (Context -> IO (a, SolverState ann))
-> SolveM ann (a, SolverState ann)
forall a b. (a -> b) -> a -> b
$ \Context
me -> do
    Context
-> FilePath -> IO (a, SolverState ann) -> IO (a, SolverState ann)
forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"" (IO (a, SolverState ann) -> IO (a, SolverState ann))
-> IO (a, SolverState ann) -> IO (a, SolverState ann)
forall a b. (a -> b) -> a -> b
$ do
      [(Int, Expr)] -> ((Int, Expr) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Expr)]
concretePreds (((Int, Expr) -> IO ()) -> IO ())
-> ((Int, Expr) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
i, Expr
e) ->
        Context -> Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> IO ()
smtDefineFunc Context
me (SubcId -> Symbol
F.bindSymbol (Int -> SubcId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)) [] Sort
F.boolSort Expr
e
      (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
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
  SolverState ann -> StateT (SolverState ann) IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SolverState ann
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' <- (Context -> IO [a]) -> SolveM ann [a]
forall a ann. (Context -> IO a) -> SolveM ann a
withContext ((Context -> IO [a]) -> SolveM ann [a])
-> (Context -> IO [a]) -> SolveM ann [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 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 -> Context -> IO [a]
filterValid_ :: forall a. 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
forall v. ExprV v -> ExprV v
F.PNot Expr
q)
      Bool
valid <- Context -> IO Bool
smtCheckUnsat Context
me
      Maybe a -> IO (Maybe a)
forall a. a -> IO 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 ann [a]
--------------------------------------------------------------------------------
filterValidGradual :: forall a ann. [Expr] -> Cand a -> SolveM ann [a]
filterValidGradual [Expr]
p Cand a
qs = do
  [a]
qs' <- (Context -> IO [a]) -> SolveM ann [a]
forall a ann. (Context -> IO a) -> SolveM ann a
withContext ((Context -> IO [a]) -> SolveM ann [a])
-> (Context -> IO [a]) -> SolveM ann [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 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'

filterValidGradual_ :: [F.Expr] -> F.Cand a -> Context -> IO [a]
filterValidGradual_ :: forall a. [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 :: forall a. (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 a. a -> IO 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_ :: forall a. 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
forall v. ExprV v -> ExprV v
F.PNot Expr
q)
      Bool
valid <- Context -> IO Bool
smtCheckUnsat Context
me
      ((Expr, a), Bool) -> IO ((Expr, a), Bool)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr
q, a
x), Bool
valid)

smtEnablembqi :: SolveM ann ()
smtEnablembqi :: forall ann. SolveM ann ()
smtEnablembqi
  = (Context -> IO ()) -> SolveM ann ()
forall a ann. (Context -> IO a) -> SolveM ann a
withContext Context -> IO ()
smtSetMbqi

--------------------------------------------------------------------------------
checkSat :: F.Expr -> SolveM ann Bool
--------------------------------------------------------------------------------
checkSat :: forall ann. Expr -> SolveM ann Bool
checkSat Expr
p
  = (Context -> IO Bool) -> SolveM ann Bool
forall a ann. (Context -> IO a) -> SolveM ann a
withContext ((Context -> IO Bool) -> SolveM ann Bool)
-> (Context -> IO Bool) -> SolveM ann 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 ann ()
--------------------------------------------------------------------------------
assumesAxioms :: forall ann. [Triggered Expr] -> SolveM ann ()
assumesAxioms [Triggered Expr]
es = (Context -> IO ()) -> SolveM ann ()
forall a ann. (Context -> IO a) -> SolveM ann a
withContext ((Context -> IO ()) -> SolveM ann ())
-> (Context -> IO ()) -> SolveM ann ()
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 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