module Language.Fixpoint.Solver.Monad
(
SolveM
, runSolverM
, getBinds
, filterRequired
, filterValid
, filterValidGradual
, checkSat
, smtEnablembqi
, Stats
, tickIter
, stats
, numIter
)
where
import Control.DeepSeq
import GHC.Generics
import Language.Fixpoint.Utils.Progress
import Language.Fixpoint.Misc (mapSnd, groupList)
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.Types.Solutions as F
import Language.Fixpoint.Types (pprint)
import qualified Language.Fixpoint.Smt.Theories as Thy
import Language.Fixpoint.Smt.Types (tsInterp)
import Language.Fixpoint.Smt.Serialize ()
import Language.Fixpoint.Types.PrettyPrint ()
import Language.Fixpoint.Smt.Interface
import Language.Fixpoint.Solver.Sanitize
import Language.Fixpoint.SortCheck
import Language.Fixpoint.Graph.Types (SolverInfo (..))
import Data.List (partition)
import Text.PrettyPrint.HughesPJ (text)
import Control.Monad.State.Strict
import qualified Data.HashMap.Strict as M
import Data.Maybe (catMaybes)
import Control.Exception.Base (bracket)
type SolveM = StateT SolverState IO
data SolverState = SS { ssCtx :: !Context
, ssBinds :: !F.SolEnv
, ssStats :: !Stats
}
data Stats = Stats { numCstr :: !Int
, numIter :: !Int
, numBrkt :: !Int
, numChck :: !Int
, numVald :: !Int
} deriving (Show, Generic)
instance NFData Stats
stats0 :: F.GInfo c b -> Stats
stats0 fi = Stats nCs 0 0 0 0
where
nCs = M.size $ F.cm fi
instance F.PTable Stats where
ptable s = F.DocTable [ (text "# Constraints" , pprint (numCstr s))
, (text "# Refine Iterations" , pprint (numIter s))
, (text "# SMT Brackets" , pprint (numBrkt s))
, (text "# SMT Queries (Valid)" , pprint (numVald s))
, (text "# SMT Queries (Total)" , pprint (numChck s))
]
runSolverM :: Config -> SolverInfo b c -> Int -> SolveM a -> IO a
runSolverM cfg sI _ act =
bracket acquire release $ \ctx -> do
res <- runStateT act' (s0 ctx)
smtWrite ctx "(exit)"
return $ fst res
where
s0 ctx = SS ctx be (stats0 fi)
act' = declare initEnv lts >> assumesAxioms (F.asserts fi) >> act
release = cleanupContext
acquire = makeContextWithSEnv cfg file initEnv
initEnv = symbolEnv cfg fi
lts = F.toListSEnv (F.dLits fi)
be = F.SolEnv (F.bs fi)
file = C.srcFile cfg
fi = (siQuery sI) {F.hoInfo = F.HOI (C.allowHO cfg) (C.allowHOqs cfg)}
getBinds :: SolveM F.SolEnv
getBinds = ssBinds <$> get
getIter :: SolveM Int
getIter = numIter . ssStats <$> get
incIter, incBrkt :: SolveM ()
incIter = modifyStats $ \s -> s {numIter = 1 + numIter s}
incBrkt = modifyStats $ \s -> s {numBrkt = 1 + numBrkt s}
incChck, incVald :: Int -> SolveM ()
incChck n = modifyStats $ \s -> s {numChck = n + numChck s}
incVald n = modifyStats $ \s -> s {numVald = n + numVald s}
withContext :: (Context -> IO a) -> SolveM a
withContext k = (lift . k) =<< getContext
getContext :: SolveM Context
getContext = ssCtx <$> get
modifyStats :: (Stats -> Stats) -> SolveM ()
modifyStats f = modify $ \s -> s { ssStats = f (ssStats s) }
filterRequired :: F.Cand a -> F.Expr -> SolveM [a]
filterRequired = error "TBD:filterRequired"
filterValid :: F.Expr -> F.Cand a -> SolveM [a]
filterValid p qs = do
qs' <- withContext $ \me ->
smtBracket me "filterValidLHS" $
filterValid_ p qs me
incBrkt
incChck (length qs)
incVald (length qs')
return qs'
filterValid_ :: F.Expr -> F.Cand a -> Context -> IO [a]
filterValid_ p qs me = catMaybes <$> do
smtAssert me p
forM qs $ \(q, x) ->
smtBracket me "filterValidRHS" $ do
smtAssert me (F.PNot q)
valid <- smtCheckUnsat me
return $ if valid then Just x else Nothing
filterValidGradual :: [F.Expr] -> F.Cand a -> SolveM [a]
filterValidGradual p qs = do
qs' <- withContext $ \me ->
smtBracket me "filterValidGradualLHS" $
filterValidGradual_ p qs me
incBrkt
incChck (length qs)
incVald (length qs')
return qs'
filterValidGradual_ :: [F.Expr] -> F.Cand a -> Context -> IO [a]
filterValidGradual_ ps qs me
= (map snd . fst) <$> foldM partitionCandidates ([], qs) ps
where
partitionCandidates :: (F.Cand a, F.Cand a) -> F.Expr -> IO (F.Cand a, F.Cand a)
partitionCandidates (ok, candidates) p = do
(valids', invalids') <- partition snd <$> filterValidOne_ p candidates me
let (valids, invalids) = (fst <$> valids', fst <$> invalids')
return (ok ++ valids, invalids)
filterValidOne_ :: F.Expr -> F.Cand a -> Context -> IO [((F.Expr, a), Bool)]
filterValidOne_ p qs me = do
smtAssert me p
forM qs $ \(q, x) ->
smtBracket me "filterValidRHS" $ do
smtAssert me (F.PNot q)
valid <- smtCheckUnsat me
return $ ((q, x), valid)
smtEnablembqi :: SolveM ()
smtEnablembqi
= withContext $ \me ->
smtWrite me "(set-option :smt.mbqi true)"
checkSat :: F.Expr -> SolveM Bool
checkSat p
= withContext $ \me ->
smtBracket me "checkSat" $
smtCheckSat me p
declare :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)] -> SolveM ()
declare env lts = withContext $ \me -> do
forM_ thyXTs $ uncurry $ smtDecl me
forM_ qryXTs $ uncurry $ smtDecl me
forM_ ess $ smtDistinct me
forM_ axs $ smtAssert me
return ()
where
ess = distinctLiterals lts
axs = Thy.axiomLiterals lts
thyXTs = filter (isKind 1) xts
qryXTs = mapSnd tx <$> filter (isKind 2) xts
isKind n = (n ==) . symKind . fst
xts = F.toListSEnv env
tx = elaborate "declare" env
symKind :: F.Symbol -> Int
symKind x = case M.lookup x Thy.theorySymbols of
Just t -> if tsInterp t then 0 else 1
Nothing -> 2
assumesAxioms :: [F.Triggered F.Expr] -> SolveM ()
assumesAxioms es = withContext $ \me -> forM_ es $ smtAssertAxiom me
distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]
distinctLiterals xts = [ es | (_, es) <- tess ]
where
tess = groupList [(t, F.expr x) | (x, t) <- xts, notFun t]
notFun = not . F.isFunctionSortedReft . (`F.RR` F.trueReft)
stats :: SolveM Stats
stats = ssStats <$> get
tickIter :: Bool -> SolveM Int
tickIter newScc = progIter newScc >> incIter >> getIter
progIter :: Bool -> SolveM ()
progIter newScc = lift $ when newScc progressTick