{-# 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
       , sendConcreteBindingsToSMT

         -- * Debug
       , Stats
       , tickIter
       , stats
       , numIter
       , SolverState(..)
       )
       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.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   = forall k v. HashMap k v -> Int
M.size forall a b. (a -> b) -> a -> 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 =
  forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket IO Context
acquire Context -> IO ()
release forall a b. (a -> b) -> a -> b
$ \Context
ctx -> do
    (a, SolverState ann)
res <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SolveM ann a
act' (Context -> SolverState ann
s0 Context
ctx)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst (a, SolverState ann)
res)
  where
    s0 :: Context -> SolverState ann
s0 Context
ctx   = forall ann. Context -> BindEnv ann -> Stats -> SolverState ann
SS Context
ctx BindEnv ann
be (forall (c :: * -> *) b. GInfo c b -> Stats
stats0 GInfo SimpC ann
fi)
    act' :: SolveM ann a
act'     = forall ann. [Triggered Expr] -> SolveM ann ()
assumesAxioms (forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
F.asserts GInfo SimpC ann
fi) 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 -> IO Context
makeContextWithSEnv Config
cfg FilePath
file SymEnv
initEnv
    initEnv :: SymEnv
initEnv  = forall a. Config -> SInfo a -> SymEnv
symbolEnv   Config
cfg GInfo SimpC ann
fi
    be :: BindEnv ann
be       = 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 arithmentic when: linear flag is on or solver /= Z3
    -- lar     = linear cfg || Z3 /= solver cfg
    fi :: GInfo SimpC ann
fi       = (forall a b. SolverInfo a b -> SInfo a
siQuery SolverInfo ann 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 ann (F.BindEnv ann)
--------------------------------------------------------------------------------
getBinds :: forall ann. SolveM ann (BindEnv ann)
getBinds = forall ann. SolverState ann -> BindEnv ann
ssBinds forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get

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

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

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

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

getContext :: SolveM ann Context
getContext :: forall ann. SolveM ann Context
getContext = forall ann. SolverState ann -> Context
ssCtx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \SolverState ann
s -> SolverState ann
s { ssStats :: Stats
ssStats = Stats -> Stats
f (forall ann. SolverState ann -> Stats
ssStats SolverState ann
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 <- forall ann. SolveM ann (BindEnv ann)
getBinds
  let concretePreds :: [(Int, Expr)]
concretePreds =
        [ (Int
i, forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Expr
p (Symbol
v, Symbol -> Expr
F.EVar Symbol
s))
        | (Int
i, (Symbol
s, F.RR Sort
_ (F.Reft (Symbol
v, Expr
p)),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
isShortExpr Expr
p)
        , Bool -> Bool
not (Int -> IBindEnv -> Bool
F.memberIBindEnv Int
i IBindEnv
known)
        ]
  SolverState ann
st <- forall s (m :: * -> *). MonadState s m => m s
get
  (a
a, SolverState ann
st') <- forall a ann. (Context -> IO a) -> SolveM ann a
withContext forall a b. (a -> b) -> a -> b
$ \Context
me -> do
    forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"" forall a b. (a -> b) -> a -> b
$ do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Expr)]
concretePreds 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 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)) [] Sort
F.boolSort Expr
e
      forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SolverState ann
st forall a b. (a -> b) -> a -> b
$ IBindEnv -> SolveM ann a
act forall a b. (a -> b) -> a -> b
$ IBindEnv -> IBindEnv -> IBindEnv
F.unionIBindEnv IBindEnv
known forall a b. (a -> b) -> a -> b
$ [Int] -> IBindEnv
F.fromListIBindEnv forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, Expr)]
concretePreds
  forall s (m :: * -> *). MonadState s m => s -> m ()
put SolverState ann
st'
  forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  where
    isShortExpr :: Expr -> Bool
isShortExpr Expr
F.PTrue = Bool
True
    isShortExpr Expr
F.PTop = Bool
True
    isShortExpr Expr
_ = 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 = 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 [(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' <- forall a ann. (Context -> IO a) -> SolveM ann a
withContext forall a b. (a -> b) -> a -> b
$ \Context
me ->
           forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"filterValidLHS" forall a b. (a -> b) -> a -> b
$
             forall a. SrcSpan -> Expr -> Cand a -> Context -> IO [a]
filterValid_ SrcSpan
sp Expr
p Cand a
qs Context
me
  -- stats
  forall ann. SolveM ann ()
incBrkt
  forall ann. Int -> SolveM ann ()
incChck (forall (t :: * -> *) a. Foldable t => t a -> Int
length Cand a
qs)
  forall ann. Int -> SolveM ann ()
incVald (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
qs')
  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 = forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  Context -> Expr -> IO ()
smtAssert Context
me Expr
p
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Cand a
qs forall a b. (a -> b) -> a -> b
$ \(Expr
q, a
x) ->
    forall a. SrcSpan -> Context -> FilePath -> IO a -> IO a
smtBracketAt SrcSpan
sp Context
me FilePath
"filterValidRHS" 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
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
valid then forall a. a -> Maybe a
Just a
x else 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' <- forall a ann. (Context -> IO a) -> SolveM ann a
withContext forall a b. (a -> b) -> a -> b
$ \Context
me ->
           forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"filterValidGradualLHS" forall a b. (a -> b) -> a -> b
$
             forall a. [Expr] -> Cand a -> Context -> IO [a]
filterValidGradual_ [Expr]
p Cand a
qs Context
me
  -- stats
  forall ann. SolveM ann ()
incBrkt
  forall ann. Int -> SolveM ann ()
incChck (forall (t :: * -> *) a. Foldable t => t a -> Int
length Cand a
qs)
  forall ann. Int -> SolveM ann ()
incVald (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
qs')
  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
  = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM 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')  <- forall a. (a -> Bool) -> [a] -> ([a], [a])
partition forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((Expr, a), Bool)]
valids', forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((Expr, a), Bool)]
invalids')
      forall (m :: * -> *) a. Monad m => a -> m a
return (Cand a
ok 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
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Cand a
qs forall a b. (a -> b) -> a -> b
$ \(Expr
q, a
x) ->
    forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"filterValidRHS" 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
      forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr
q, a
x), Bool
valid)

smtEnablembqi :: SolveM ann ()
smtEnablembqi :: forall ann. SolveM ann ()
smtEnablembqi
  = 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
  = forall a ann. (Context -> IO a) -> SolveM ann a
withContext forall a b. (a -> b) -> a -> b
$ \Context
me ->
      forall a. Context -> FilePath -> IO a -> IO a
smtBracket Context
me FilePath
"checkSat" 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 = forall a ann. (Context -> IO a) -> SolveM ann a
withContext forall a b. (a -> b) -> a -> b
$ \Context
me -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_  [Triggered Expr]
es 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 = forall ann. SolverState ann -> Stats
ssStats forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get

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

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