{-# LANGUAGE PatternGuards     #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections     #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

--------------------------------------------------------------------------------
-- | Solve a system of horn-clause constraints ---------------------------------
--------------------------------------------------------------------------------

module Language.Fixpoint.Solver.Solve (solve) where

import           Control.Monad (forM, when, filterM)
import           Control.Monad.Reader
import           Language.Fixpoint.Misc
import qualified Language.Fixpoint.Misc            as Misc
import qualified Language.Fixpoint.Types           as F
import qualified Language.Fixpoint.Types.Solutions as Sol
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Config hiding (stats)
import           Language.Fixpoint.SortCheck          (ElabParam(..), elaborate)
import           Language.Fixpoint.Solver.Sanitize (symbolEnv)
import qualified Language.Fixpoint.Solver.Solution  as S
import qualified Language.Fixpoint.Smt.Types as T
import qualified Language.Fixpoint.Solver.Worklist  as W
import qualified Language.Fixpoint.Solver.Eliminate as E
import           Language.Fixpoint.Solver.Monad
import           Language.Fixpoint.Utils.Progress
import           Language.Fixpoint.Graph
import           Text.PrettyPrint.HughesPJ
import           Text.Printf
import           System.Console.CmdArgs.Verbosity -- (whenNormal, whenLoud)
import           Control.DeepSeq
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
-- import qualified Data.Maybe          as Mb
import qualified Data.List           as L
import Language.Fixpoint.Types (resStatus, FixResult(Unsafe))
import Language.Fixpoint.Smt.Interface (smtComment)
import Language.Fixpoint.Solver.Interpreter (instInterpreter)
import qualified Language.Fixpoint.Solver.PLE as PLE      (instantiate)
import Data.Maybe (maybeToList)

mytrace :: String -> a -> a
mytrace :: forall a. String -> a -> a
mytrace
  -- s x = trace s x
  String
_ a
x = a
x
{-
solve_ :: (NFData a, F.Fixpoint a, F.Loc a)
       => Config
       -> F.SInfo a
       -> Sol.Solution
       -> W.Worklist a
       -> SolveM a (F.Result (Integer, a), Stats)
       -}
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
solve
  :: forall a. (NFData a, F.Fixpoint a, Show a, F.Loc a)
  => Config -> ElabParam -> F.SInfo a -> IO (F.Result (Integer, a))
--------------------------------------------------------------------------------

solve :: forall a.
(NFData a, Fixpoint a, Show a, Loc a) =>
Config -> ElabParam -> SInfo a -> IO (Result (Integer, a))
solve Config
cfg ElabParam
elabParam SInfo a
fi = do
    IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
donePhase Moods
Misc.Loud String
"Worklist Initialize"
    Verbosity
vb <- IO Verbosity
getVerbosity
    (Result (Integer, a)
res, Stats
stat) <- (if Verbosity
Quiet Verbosity -> Verbosity -> Bool
forall a. Eq a => a -> a -> Bool
== Verbosity
vb then IO (Result (Integer, a), Stats) -> IO (Result (Integer, a), Stats)
forall a. a -> a
id else SolverInfo a
-> IO (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall a b. SolverInfo a -> IO b -> IO b
withProgressFI SolverInfo a
sI) (IO (Result (Integer, a), Stats)
 -> IO (Result (Integer, a), Stats))
-> IO (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall a b. (a -> b) -> a -> b
$ Config
-> SolverInfo a
-> ElabParam
-> SolveM a (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall ann a.
Config -> SolverInfo ann -> ElabParam -> SolveM ann a -> IO a
runSolverM Config
cfg SolverInfo a
sI ElabParam
elabParam SolveM a (Result (Integer, a), Stats)
act
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
solverStats Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ SInfo a -> Worklist a -> Stats -> IO ()
forall a. SInfo a -> Worklist a -> Stats -> IO ()
printStats SInfo a
fi Worklist a
wkl Stats
stat
    -- print (numIter stat)
    Result (Integer, a) -> IO (Result (Integer, a))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result (Integer, a)
res
  where
    act :: SolveM a (F.Result (Integer, a), Stats)
    act :: SolveM a (Result (Integer, a), Stats)
act = do
      Context
ctx <- SolveM a Context
forall ann. SolveM ann Context
getContext
      let sEnv :: SymEnv
sEnv = Config -> SInfo a -> SymEnv
forall a. HasCallStack => Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi
          s1 :: Sol QBind
s1 = Sol QBind
s0{Sol.sMap = M.map (elabQBind ctx "solve" sEnv) (Sol.sMap s0)}
      Config
-> SInfo a
-> Sol QBind
-> Worklist a
-> SolveM a (Result (Integer, a), Stats)
forall a.
(NFData a, Fixpoint a, Loc a) =>
Config
-> SInfo a
-> Sol QBind
-> Worklist a
-> SolveM a (Result (Integer, a), Stats)
solve_ Config
cfg SInfo a
fi Sol QBind
s1 Worklist a
wkl
    -- solverInfo computes the set of cut and non-cut kvars, then initializes
    -- the solutions of the non-cut KVars (in the sHyp field)
    --
    -- S.init provides an initial solution for the cut KVars
    sI :: SolverInfo a
sI  = Config -> SInfo a -> SolverInfo a
forall a. Config -> SInfo a -> SolverInfo a
solverInfo Config
cfg SInfo a
fi
    wkl :: Worklist a
wkl = SolverInfo a -> Worklist a
forall a. SolverInfo a -> Worklist a
W.init SolverInfo a
sI
    s0 :: Sol QBind
s0  = (SolverInfo a -> Sol QBind
forall a. SolverInfo a -> Sol QBind
siSol SolverInfo a
sI) { Sol.sMap = S.init cfg fi ks }
    ks :: HashSet KVar
ks  = SolverInfo a -> HashSet KVar
forall a. SolverInfo a -> HashSet KVar
siVars SolverInfo a
sI
    elabQBind :: Context -> String -> SymEnv -> QBind -> QBind
elabQBind Context
ctx String
msg SymEnv
env (Sol.QB [EQual]
xs) = [EQual] -> QBind
Sol.QB ((EQual -> EQual) -> [EQual] -> [EQual]
forall a b. (a -> b) -> [a] -> [b]
map EQual -> EQual
elabEQual [EQual]
xs)
      where
        elabEQual :: EQual -> EQual
elabEQual EQual
eq =
          EQual
eq { Sol.eqPred =
                elaborate
                 (ElabParam (T.ctxElabF ctx) (F.atLoc F.dummySpan msg) env)
                 (Sol.eqPred eq)
             }


--------------------------------------------------------------------------------
-- | Progress Bar
--------------------------------------------------------------------------------
withProgressFI :: SolverInfo a -> IO b -> IO b
withProgressFI :: forall a b. SolverInfo a -> IO b -> IO b
withProgressFI = Int -> IO b -> IO b
forall a. Int -> IO a -> IO a
withProgress (Int -> IO b -> IO b)
-> (SolverInfo a -> Int) -> SolverInfo a -> IO b -> IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Int) -> (SolverInfo a -> Int) -> SolverInfo a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (SolverInfo a -> Int) -> SolverInfo a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CDeps -> Int
cNumScc (CDeps -> Int) -> (SolverInfo a -> CDeps) -> SolverInfo a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverInfo a -> CDeps
forall a. SolverInfo a -> CDeps
siDeps
--------------------------------------------------------------------------------

printStats :: F.SInfo a ->  W.Worklist a -> Stats -> IO ()
printStats :: forall a. SInfo a -> Worklist a -> Stats -> IO ()
printStats SInfo a
fi Worklist a
w Stats
s = String -> IO ()
putStrLn String
"\n" IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [DocTable] -> IO ()
ppTs [ SInfo a -> DocTable
forall a. PTable a => a -> DocTable
ptable SInfo a
fi, Stats -> DocTable
forall a. PTable a => a -> DocTable
ptable Stats
s, Worklist a -> DocTable
forall a. PTable a => a -> DocTable
ptable Worklist a
w ]
  where
    ppTs :: [DocTable] -> IO ()
ppTs          = String -> IO ()
putStrLn (String -> IO ()) -> ([DocTable] -> String) -> [DocTable] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DocTable -> String
forall a. PPrint a => a -> String
showpp (DocTable -> String)
-> ([DocTable] -> DocTable) -> [DocTable] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DocTable] -> DocTable
forall a. Monoid a => [a] -> a
mconcat

--------------------------------------------------------------------------------
solverInfo :: Config -> F.SInfo a -> SolverInfo a
--------------------------------------------------------------------------------
solverInfo :: forall a. Config -> SInfo a -> SolverInfo a
solverInfo Config
cfg SInfo a
fI
  | Config -> Bool
useElim Config
cfg = Config -> SInfo a -> SolverInfo a
forall a. Config -> SInfo a -> SolverInfo a
E.solverInfo Config
cfg SInfo a
fI
  | Bool
otherwise   = Sol QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a
forall a.
Sol QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a
SI Sol QBind
forall a. Monoid a => a
mempty SInfo a
fI CDeps
cD (SInfo a -> HashSet KVar
forall a. SInfo a -> HashSet KVar
siKvars SInfo a
fI)
  where
    cD :: CDeps
cD          = SInfo a -> [CEdge] -> HashSet KVar -> CDeps
forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> HashSet KVar -> CDeps
elimDeps SInfo a
fI (SInfo a -> [CEdge]
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> [CEdge]
kvEdges SInfo a
fI) HashSet KVar
forall a. Monoid a => a
mempty

siKvars :: F.SInfo a -> S.HashSet F.KVar
siKvars :: forall a. SInfo a -> HashSet KVar
siKvars = [KVar] -> HashSet KVar
forall a. Hashable a => [a] -> HashSet a
S.fromList ([KVar] -> HashSet KVar)
-> (SInfo a -> [KVar]) -> SInfo a -> HashSet KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap KVar (WfC a) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys (HashMap KVar (WfC a) -> [KVar])
-> (SInfo a -> HashMap KVar (WfC a)) -> SInfo a -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws

doInterpret :: (F.Loc a) =>  Config -> F.SInfo a -> [F.SubcId] -> SolveM a (F.BindEnv a)
doInterpret :: forall a.
Loc a =>
Config -> SInfo a -> [Integer] -> SolveM a (BindEnv a)
doInterpret Config
cfg SInfo a
fi [Integer]
subcIds = IO (BindEnv a) -> StateT (SolverState a) IO (BindEnv a)
forall a. IO a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (BindEnv a) -> StateT (SolverState a) IO (BindEnv a))
-> IO (BindEnv a) -> StateT (SolverState a) IO (BindEnv a)
forall a b. (a -> b) -> a -> b
$ Config -> SInfo a -> Maybe [Integer] -> IO (BindEnv a)
forall a.
Loc a =>
Config -> SInfo a -> Maybe [Integer] -> IO (BindEnv a)
instInterpreter Config
cfg SInfo a
fi ([Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just [Integer]
subcIds)

--------------------------------------------------------------------------------
{-# SCC solve_ #-}
solve_ :: (NFData a, F.Fixpoint a, F.Loc a)
       => Config
       -> F.SInfo a
       -> Sol.Solution
       -> W.Worklist a
       -> SolveM a (F.Result (Integer, a), Stats)
--------------------------------------------------------------------------------
solve_ :: forall a.
(NFData a, Fixpoint a, Loc a) =>
Config
-> SInfo a
-> Sol QBind
-> Worklist a
-> SolveM a (Result (Integer, a), Stats)
solve_ Config
cfg SInfo a
fi Sol QBind
s2 Worklist a
wkl = do
  SmtM () -> SolveM a ()
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM () -> SolveM a ()) -> SmtM () -> SolveM a ()
forall a b. (a -> b) -> a -> b
$ Text -> SmtM ()
smtComment Text
"solve: start"
  (Sol QBind
s3, Result (Integer, a)
res0) <- IBindEnv
-> BindEnv a
-> (IBindEnv -> SolveM a (Sol QBind, Result (Integer, a)))
-> SolveM a (Sol QBind, Result (Integer, a))
forall ann a.
IBindEnv
-> BindEnv ann -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi) ((IBindEnv -> SolveM a (Sol QBind, Result (Integer, a)))
 -> SolveM a (Sol QBind, Result (Integer, a)))
-> (IBindEnv -> SolveM a (Sol QBind, Result (Integer, a)))
-> SolveM a (Sol QBind, Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt -> do
    -- let s3   = solveEbinds fi s2
    Sol QBind
s3       <- {- SCC "sol-refine" -} IBindEnv
-> BindEnv a -> Sol QBind -> Worklist a -> SolveM a (Sol QBind)
forall a.
Loc a =>
IBindEnv
-> BindEnv a -> Sol QBind -> Worklist a -> SolveM a (Sol QBind)
refine IBindEnv
bindingsInSmt (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi) Sol QBind
s2 Worklist a
wkl
    Result (Integer, a)
res0     <- {- SCC "sol-result" -} IBindEnv
-> Config
-> SInfo a
-> [SimpC a]
-> Sol QBind
-> SolveM a (Result (Integer, a))
forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> SInfo a
-> [SimpC a]
-> Sol QBind
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg SInfo a
fi (Worklist a -> [SimpC a]
forall a. Worklist a -> [SimpC a]
W.unsatCandidates Worklist a
wkl) Sol QBind
s3
    (Sol QBind, Result (Integer, a))
-> SolveM a (Sol QBind, Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sol QBind
s3, Result (Integer, a)
res0)

  (SInfo a
fi1, Result (Integer, a)
res1) <- case Result (Integer, a) -> FixResult (Integer, a)
forall a. Result a -> FixResult a
resStatus Result (Integer, a)
res0 of  {- first run the interpreter -}
    Unsafe Stats
_ [(Integer, a)]
bads | Config -> Bool
rewriteAxioms Config
cfg Bool -> Bool -> Bool
&& Config -> Bool
interpreter Config
cfg -> do
      SmtM () -> SolveM a ()
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM () -> SolveM a ()) -> SmtM () -> SolveM a ()
forall a b. (a -> b) -> a -> b
$ Text -> SmtM ()
smtComment Text
"solve: interpreter"
      BindEnv a
bs <- Config -> SInfo a -> [Integer] -> SolveM a (BindEnv a)
forall a.
Loc a =>
Config -> SInfo a -> [Integer] -> SolveM a (BindEnv a)
doInterpret Config
cfg SInfo a
fi (((Integer, a) -> Integer) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, a) -> Integer
forall a b. (a, b) -> a
fst ([(Integer, a)] -> [Integer]) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> a -> b
$ String -> [(Integer, a)] -> [(Integer, a)]
forall a. String -> a -> a
mytrace (String
"before the Interpreter " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([(Integer, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Integer, a)]
bads) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" constraints remain") [(Integer, a)]
bads)
      let fi1 :: SInfo a
fi1 = SInfo a
fi { F.bs = bs }
          badCs :: [SimpC a]
badCs = CMap (SimpC a) -> Integer -> SimpC a
forall a. HasCallStack => CMap a -> Integer -> a
lookupCMap (SInfo a -> CMap (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
F.cm SInfo a
fi) (Integer -> SimpC a) -> [Integer] -> [SimpC a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Integer, a) -> Integer) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, a) -> Integer
forall a b. (a, b) -> a
fst [(Integer, a)]
bads
      SmtM () -> SolveM a ()
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM () -> SolveM a ()) -> SmtM () -> SolveM a ()
forall a b. (a -> b) -> a -> b
$ Text -> SmtM ()
smtComment Text
"solve: pos-interpreter check"
      (Result (Integer, a) -> (SInfo a, Result (Integer, a)))
-> SolveM a (Result (Integer, a))
-> StateT (SolverState a) IO (SInfo a, Result (Integer, a))
forall a b.
(a -> b)
-> StateT (SolverState a) IO a -> StateT (SolverState a) IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SInfo a
fi1,) (SolveM a (Result (Integer, a))
 -> StateT (SolverState a) IO (SInfo a, Result (Integer, a)))
-> SolveM a (Result (Integer, a))
-> StateT (SolverState a) IO (SInfo a, Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ IBindEnv
-> BindEnv a
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall ann a.
IBindEnv
-> BindEnv ann -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv BindEnv a
bs ((IBindEnv -> SolveM a (Result (Integer, a)))
 -> SolveM a (Result (Integer, a)))
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt ->
        IBindEnv
-> Config
-> SInfo a
-> [SimpC a]
-> Sol QBind
-> SolveM a (Result (Integer, a))
forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> SInfo a
-> [SimpC a]
-> Sol QBind
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg SInfo a
fi1 [SimpC a]
badCs Sol QBind
s3
    FixResult (Integer, a)
_ -> (SInfo a, Result (Integer, a))
-> StateT (SolverState a) IO (SInfo a, Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return  (SInfo a
fi, String -> Result (Integer, a) -> Result (Integer, a)
forall a. String -> a -> a
mytrace String
"all checked before interpreter" Result (Integer, a)
res0)

  Result (Integer, a)
res2  <- case Result (Integer, a) -> FixResult (Integer, a)
forall a. Result a -> FixResult a
resStatus Result (Integer, a)
res1 of  {- then run normal PLE on remaining unsolved constraints -}
    Unsafe Stats
_ [(Integer, a)]
bads2 | Config -> Bool
rewriteAxioms Config
cfg -> do
      SmtM () -> SolveM a ()
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM () -> SolveM a ()) -> SmtM () -> SolveM a ()
forall a b. (a -> b) -> a -> b
$ Text -> SmtM ()
smtComment Text
"solve: ple"
      BindEnv a
bs <- SmtM (BindEnv a) -> SolveM a (BindEnv a)
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM (BindEnv a) -> SolveM a (BindEnv a))
-> SmtM (BindEnv a) -> SolveM a (BindEnv a)
forall a b. (a -> b) -> a -> b
$ Config
-> SInfo a
-> Maybe (Sol QBind)
-> Maybe [Integer]
-> SmtM (BindEnv a)
forall a.
Loc a =>
Config
-> SInfo a
-> Maybe (Sol QBind)
-> Maybe [Integer]
-> SmtM (BindEnv a)
PLE.instantiate Config
cfg SInfo a
fi1 (Sol QBind -> Maybe (Sol QBind)
forall a. a -> Maybe a
Just Sol QBind
s3) ([Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just ([Integer] -> Maybe [Integer]) -> [Integer] -> Maybe [Integer]
forall a b. (a -> b) -> a -> b
$ ((Integer, a) -> Integer) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, a) -> Integer
forall a b. (a, b) -> a
fst [(Integer, a)]
bads2)
      -- Check the constraints one last time after PLE
      let fi2 :: SInfo a
fi2 = SInfo a
fi { F.bs = bs }
          badsCs2 :: [SimpC a]
badsCs2 = CMap (SimpC a) -> Integer -> SimpC a
forall a. HasCallStack => CMap a -> Integer -> a
lookupCMap (SInfo a -> CMap (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
F.cm SInfo a
fi) (Integer -> SimpC a) -> [Integer] -> [SimpC a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Integer, a) -> Integer) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, a) -> Integer
forall a b. (a, b) -> a
fst [(Integer, a)]
bads2
      SmtM () -> SolveM a ()
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM () -> SolveM a ()) -> SmtM () -> SolveM a ()
forall a b. (a -> b) -> a -> b
$ Text -> SmtM ()
smtComment Text
"solve: pos-ple check"
      IBindEnv
-> BindEnv a
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall ann a.
IBindEnv
-> BindEnv ann -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv BindEnv a
bs ((IBindEnv -> SolveM a (Result (Integer, a)))
 -> SolveM a (Result (Integer, a)))
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt ->
        IBindEnv
-> Config
-> SInfo a
-> [SimpC a]
-> Sol QBind
-> SolveM a (Result (Integer, a))
forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> SInfo a
-> [SimpC a]
-> Sol QBind
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg SInfo a
fi2 [SimpC a]
badsCs2 Sol QBind
s3
    FixResult (Integer, a)
_ -> Result (Integer, a) -> SolveM a (Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Integer, a) -> SolveM a (Result (Integer, a)))
-> Result (Integer, a) -> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ String -> Result (Integer, a) -> Result (Integer, a)
forall a. String -> a -> a
mytrace String
"all checked with interpreter" Result (Integer, a)
res1

  SmtM () -> SolveM a ()
forall a ann. SmtM a -> SolveM ann a
liftSMT (SmtM () -> SolveM a ()) -> SmtM () -> SolveM a ()
forall a b. (a -> b) -> a -> b
$ Text -> SmtM ()
smtComment Text
"solve: finished"
  Stats
st      <- SolveM a Stats
forall ann. SolveM ann Stats
stats
  let res3 :: Result (Integer, a)
res3 = {- SCC "sol-tidy" -} Config -> Result (Integer, a) -> Result (Integer, a)
forall a. Config -> Result a -> Result a
tidyResult Config
cfg Result (Integer, a)
res2
  (Result (Integer, a), Stats)
-> SolveM a (Result (Integer, a), Stats)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Result (Integer, a), Stats)
 -> SolveM a (Result (Integer, a), Stats))
-> (Result (Integer, a), Stats)
-> SolveM a (Result (Integer, a), Stats)
forall a b. NFData a => (a -> b) -> a -> b
$!! (Result (Integer, a)
res3, Stats
st)


--------------------------------------------------------------------------------
-- | tidyResult ensures we replace the temporary kVarArg names introduced to
--   ensure uniqueness with the original names in the given WF constraints.
--------------------------------------------------------------------------------
tidyResult :: Config -> F.Result a -> F.Result a
tidyResult :: forall a. Config -> Result a -> Result a
tidyResult Config
_ Result a
r = Result a
r
  { F.resSolution = tidySolution (F.resSolution r)
  , F.resNonCutsSolution = M.map (fmap tidyPred) (F.resNonCutsSolution r)
  , F.resSorts = fmap tidyBind <$>  F.resSorts r
  }

tidySolution :: F.FixSolution -> F.FixSolution
tidySolution :: FixSolution -> FixSolution
tidySolution = (Pred -> Pred) -> FixSolution -> FixSolution
forall a b. (a -> b) -> HashMap KVar a -> HashMap KVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pred -> Pred
tidyPred

tidyBind :: (F.Symbol, F.Sort) -> (F.Symbol, F.Sort)
tidyBind :: (Symbol, Sort) -> (Symbol, Sort)
tidyBind (Symbol
x, Sort
t) = (Symbol -> Symbol
F.tidySymbol Symbol
x, Sort
t)

tidyPred :: F.Expr -> F.Expr
tidyPred :: Pred -> Pred
tidyPred =  Pred -> Pred
go
  where
    ts :: Symbol -> Symbol
ts = Symbol -> Symbol
F.tidySymbol
    tb :: (Symbol, Sort) -> (Symbol, Sort)
tb = (Symbol, Sort) -> (Symbol, Sort)
tidyBind
    go :: Pred -> Pred
go (F.EApp Pred
s Pred
e)      = Pred -> Pred -> Pred
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp (Pred -> Pred
go Pred
s) (Pred -> Pred
go Pred
e)
    go (F.ELam (Symbol
x,Sort
t) Pred
e)  = (Symbol, Sort) -> Pred -> Pred
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
F.ELam (Symbol -> Symbol
ts Symbol
x, Sort
t) (Pred -> Pred
go Pred
e)
    go (F.ECoerc Sort
a Sort
t Pred
e)  = Sort -> Sort -> Pred -> Pred
forall v. Sort -> Sort -> ExprV v -> ExprV v
F.ECoerc Sort
a Sort
t (Pred -> Pred
go Pred
e)
    go (F.ENeg Pred
e)        = Pred -> Pred
forall v. ExprV v -> ExprV v
F.ENeg (Pred -> Pred
go Pred
e)
    go (F.EBin Bop
op Pred
e1 Pred
e2) = Bop -> Pred -> Pred -> Pred
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
F.EBin Bop
op (Pred -> Pred
go Pred
e1) (Pred -> Pred
go Pred
e2)
    go (F.ELet Symbol
x Pred
e1 Pred
e2)  = Symbol -> Pred -> Pred -> Pred
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
F.ELet (Symbol -> Symbol
ts Symbol
x) (Pred -> Pred
go Pred
e1) (Pred -> Pred
go Pred
e2)
    go (F.EIte Pred
p Pred
e1 Pred
e2)  = Pred -> Pred -> Pred -> Pred
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
F.EIte (Pred -> Pred
go Pred
p) (Pred -> Pred
go Pred
e1) (Pred -> Pred
go Pred
e2)
    go (F.ECst Pred
e Sort
so)     = Pred -> Sort -> Pred
forall v. ExprV v -> Sort -> ExprV v
F.ECst (Pred -> Pred
go Pred
e) Sort
so
    go (F.EVar Symbol
x)        = Symbol -> Pred
forall v. v -> ExprV v
F.EVar (Symbol -> Symbol
ts Symbol
x)
    go (F.PAnd [Pred]
ps)       = [Pred] -> Pred
forall v. [ExprV v] -> ExprV v
F.PAnd ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
go [Pred]
ps
    go (F.POr  [Pred]
ps)       = [Pred] -> Pred
forall v. [ExprV v] -> ExprV v
F.POr  ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
go [Pred]
ps
    go (F.PNot Pred
p)        = Pred -> Pred
forall v. ExprV v -> ExprV v
F.PNot (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Pred -> Pred
go Pred
p
    go (F.PImp Pred
p1 Pred
p2)    = Pred -> Pred -> Pred
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp (Pred -> Pred
go Pred
p1) (Pred -> Pred
go Pred
p2)
    go (F.PIff Pred
p1 Pred
p2)    = Pred -> Pred -> Pred
forall v. ExprV v -> ExprV v -> ExprV v
F.PIff (Pred -> Pred
go Pred
p1) (Pred -> Pred
go Pred
p2)
    go (F.PAtom Brel
r Pred
e1 Pred
e2) = Brel -> Pred -> Pred -> Pred
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
r (Pred -> Pred
go Pred
e1) (Pred -> Pred
go Pred
e2)
    go (F.PExist [(Symbol, Sort)]
xts Pred
e)  = [(Symbol, Sort)] -> Pred -> Pred
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.PExist ((Symbol, Sort) -> (Symbol, Sort)
tb ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) (Pred -> Pred
go Pred
e)
    go (F.PAll [(Symbol, Sort)]
xts Pred
e)    = [(Symbol, Sort)] -> Pred -> Pred
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.PAll   ((Symbol, Sort) -> (Symbol, Sort)
tb ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) (Pred -> Pred
go Pred
e)
    go  Pred
p                = Pred
p

--------------------------------------------------------------------------------
{-# SCC refine #-}
-- | Implementation of the inference algorithm from:
--
-- "Liquid Types", PLDI 2008, https://ranjitjhala.github.io/static/liquid_types.pdf
--
refine
  :: forall a. F.Loc a
  => F.IBindEnv
  -> F.BindEnv a
  -> Sol.Solution
  -> W.Worklist a
  -> SolveM a Sol.Solution
--------------------------------------------------------------------------------
refine :: forall a.
Loc a =>
IBindEnv
-> BindEnv a -> Sol QBind -> Worklist a -> SolveM a (Sol QBind)
refine IBindEnv
bindingsInSmt BindEnv a
be0 Sol QBind
s0 Worklist a
w0 = BindEnv a -> Sol QBind -> Worklist a -> SolveM a (Sol QBind)
go BindEnv a
be0 Sol QBind
s0 Worklist a
w0
  where
    go :: F.BindEnv a -> Sol.Solution -> W.Worklist a -> SolveM a Sol.Solution
    go :: BindEnv a -> Sol QBind -> Worklist a -> SolveM a (Sol QBind)
go BindEnv a
be Sol QBind
s Worklist a
w
      | Just (SimpC a
c, Worklist a
w', Bool
newScc, Int
rnk) <- Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)
forall a. Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)
W.pop Worklist a
w = do
         Int
i       <- Bool -> SolveM a Int
forall ann. Bool -> SolveM ann Int
tickIter Bool
newScc
         (Bool
b, Sol QBind
s') <- IBindEnv
-> BindEnv a
-> Int
-> Sol QBind
-> SimpC a
-> SolveM a (Bool, Sol QBind)
forall a.
Loc a =>
IBindEnv
-> BindEnv a
-> Int
-> Sol QBind
-> SimpC a
-> SolveM a (Bool, Sol QBind)
refineC IBindEnv
bindingsInSmt BindEnv a
be Int
i Sol QBind
s SimpC a
c
         IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
writeLoud (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> SimpC a -> Bool -> Int -> String -> String
forall {t} {t} {t} {t} {c :: * -> *} {a} {a}.
(PrintfArg t, PrintfArg t, PrintfArg t, PrintfType t, TaggedC c a,
 Show a) =>
t -> c a -> a -> t -> t -> t
refineMsg Int
i SimpC a
c Bool
b Int
rnk (Sol QBind -> String
forall a. PPrint a => a -> String
showpp Sol QBind
s')
         let w'' :: Worklist a
w'' = if Bool
b then SimpC a -> Worklist a -> Worklist a
forall a. SimpC a -> Worklist a -> Worklist a
W.push SimpC a
c Worklist a
w' else Worklist a
w'
         BindEnv a -> Sol QBind -> Worklist a -> SolveM a (Sol QBind)
go BindEnv a
be Sol QBind
s' Worklist a
w''
      | Bool
otherwise = Sol QBind -> SolveM a (Sol QBind)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sol QBind
s
      where
        -- DEBUG
        refineMsg :: t -> c a -> a -> t -> t -> t
refineMsg t
i c a
c a
b t
rnk t
s = String -> t -> Integer -> String -> t -> t -> t
forall r. PrintfType r => String -> r
printf String
"\niter=%d id=%d change=%s rank=%d s=%s\n"
                                 t
i (c a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId c a
c) (a -> String
forall a. Show a => a -> String
show a
b) t
rnk t
s

---------------------------------------------------------------------------
-- | Single Step Refinement -----------------------------------------------
---------------------------------------------------------------------------
{-# SCC refineC #-}
refineC
  :: forall a. (F.Loc a)
  => F.IBindEnv
  -> F.BindEnv a
  -> Int
  -> Sol.Solution
  -> F.SimpC a
  -> SolveM a (Bool, Sol.Solution)
---------------------------------------------------------------------------
refineC :: forall a.
Loc a =>
IBindEnv
-> BindEnv a
-> Int
-> Sol QBind
-> SimpC a
-> SolveM a (Bool, Sol QBind)
refineC IBindEnv
bindingsInSmt BindEnv a
be Int
_i Sol QBind
s SimpC a
c =
  do let krhs :: [(KVar, Cand EQual)]
krhs = Sol QBind -> [(KVar, Cand EQual)]
rhsCands Sol QBind
s
     Config
cfg <- Context -> Config
T.config (Context -> Config)
-> StateT (SolverState a) IO Context
-> StateT (SolverState a) IO Config
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (SolverState a) IO Context
forall ann. SolveM ann Context
getContext
     if ((KVar, Cand EQual) -> Bool) -> [(KVar, Cand EQual)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Cand EQual -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Cand EQual -> Bool)
-> ((KVar, Cand EQual) -> Cand EQual) -> (KVar, Cand EQual) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar, Cand EQual) -> Cand EQual
forall a b. (a, b) -> b
snd) [(KVar, Cand EQual)]
krhs
        then (Bool, Sol QBind) -> SolveM a (Bool, Sol QBind)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Sol QBind
s)
        else do
          let lhs :: Pred
lhs = Config -> IBindEnv -> BindEnv a -> Sol QBind -> SimpC a -> Pred
forall a.
Loc a =>
Config -> IBindEnv -> BindEnv a -> Sol QBind -> SimpC a -> Pred
S.lhsPred Config
cfg IBindEnv
bindingsInSmt BindEnv a
be Sol QBind
s SimpC a
c
          [(KVar, QBind)]
kqs <- [(KVar, Cand EQual)]
-> ((KVar, Cand EQual) -> StateT (SolverState a) IO (KVar, QBind))
-> StateT (SolverState a) IO [(KVar, QBind)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(KVar, Cand EQual)]
krhs (((KVar, Cand EQual) -> StateT (SolverState a) IO (KVar, QBind))
 -> StateT (SolverState a) IO [(KVar, QBind)])
-> ((KVar, Cand EQual) -> StateT (SolverState a) IO (KVar, QBind))
-> StateT (SolverState a) IO [(KVar, QBind)]
forall a b. (a -> b) -> a -> b
$ \(KVar
k, Cand EQual
rhs) ->
            (,) KVar
k (QBind -> (KVar, QBind))
-> ([EQual] -> QBind) -> [EQual] -> (KVar, QBind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [EQual] -> QBind
Sol.QB ([EQual] -> (KVar, QBind))
-> StateT (SolverState a) IO [EQual]
-> StateT (SolverState a) IO (KVar, QBind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Pred -> Cand EQual -> StateT (SolverState a) IO [EQual]
forall a ann. SrcSpan -> Pred -> Cand a -> SolveM ann [a]
filterValid (SimpC a -> SrcSpan
forall a. Loc a => SimpC a -> SrcSpan
cstrSpan SimpC a
c) Pred
lhs Cand EQual
rhs
          (Bool, Sol QBind) -> SolveM a (Bool, Sol QBind)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool, Sol QBind) -> SolveM a (Bool, Sol QBind))
-> (Bool, Sol QBind) -> SolveM a (Bool, Sol QBind)
forall a b. (a -> b) -> a -> b
$ Sol QBind -> [(KVar, QBind)] -> (Bool, Sol QBind)
S.update Sol QBind
s [(KVar, QBind)]
kqs
  where
    rhsCands :: Sol.Solution -> [(F.KVar, Sol.Cand Sol.EQual)]
    rhsCands :: Sol QBind -> [(KVar, Cand EQual)]
rhsCands Sol QBind
s = HashMap KVar (Cand EQual) -> [(KVar, Cand EQual)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap KVar (Cand EQual) -> [(KVar, Cand EQual)])
-> HashMap KVar (Cand EQual) -> [(KVar, Cand EQual)]
forall a b. (a -> b) -> a -> b
$ [(KVar, Cand EQual)] -> HashMap KVar (Cand EQual)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([(KVar, Cand EQual)] -> HashMap KVar (Cand EQual))
-> [(KVar, Cand EQual)] -> HashMap KVar (Cand EQual)
forall a b. (a -> b) -> a -> b
$ ((KVar, Subst) -> (KVar, Cand EQual))
-> [(KVar, Subst)] -> [(KVar, Cand EQual)]
forall a b. (a -> b) -> [a] -> [b]
map (KVar, Subst) -> (KVar, Cand EQual)
cnd [(KVar, Subst)]
ks
      where
        ks :: [(KVar, Subst)]
ks          = Pred -> [(KVar, Subst)]
predKs (Pred -> [(KVar, Subst)])
-> (SimpC a -> Pred) -> SimpC a -> [(KVar, Subst)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> Pred
forall (c :: * -> *) a. TaggedC c a => c a -> Pred
F.crhs (SimpC a -> [(KVar, Subst)]) -> SimpC a -> [(KVar, Subst)]
forall a b. (a -> b) -> a -> b
$ SimpC a
c
        cnd :: (F.KVar, F.Subst) -> (F.KVar , Sol.Cand Sol.EQual)
        cnd :: (KVar, Subst) -> (KVar, Cand EQual)
cnd (KVar
k, Subst
su) = (KVar
k, Subst -> QBind -> Cand EQual
Sol.qbPreds Subst
su (Sol QBind -> KVar -> QBind
Sol.lookupQBind Sol QBind
s KVar
k))

predKs :: F.Expr -> [(F.KVar, F.Subst)]
predKs :: Pred -> [(KVar, Subst)]
predKs (F.PAnd [Pred]
ps)    = (Pred -> [(KVar, Subst)]) -> [Pred] -> [(KVar, Subst)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pred -> [(KVar, Subst)]
predKs [Pred]
ps
predKs (F.PKVar KVar
k Subst
su) = [(KVar
k, Subst
su)]
predKs Pred
_              = []

--------------------------------------------------------------------------------
-- | Convert Solution into Result ----------------------------------------------
--------------------------------------------------------------------------------
{-# SCC result #-}
result
  :: (F.Fixpoint a, F.Loc a, NFData a)
  => F.IBindEnv
  -> Config
  -> F.SInfo a
  -> [F.SimpC a]
  -> Sol.Solution
  -> SolveM a (F.Result (Integer, a))
--------------------------------------------------------------------------------
result :: forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> SInfo a
-> [SimpC a]
-> Sol QBind
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg SInfo a
fi [SimpC a]
cs Sol QBind
s =
  IBindEnv
-> BindEnv a
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall ann a.
IBindEnv
-> BindEnv ann -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
bindingsInSmt BindEnv a
be ((IBindEnv -> SolveM a (Result (Integer, a)))
 -> SolveM a (Result (Integer, a)))
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt2 -> do
    IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift       (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
writeLoud String
"Computing Result"
    FixResult (SimpC a)
stat      <- IBindEnv
-> BindEnv a
-> Config
-> [SimpC a]
-> Sol QBind
-> SolveM a (FixResult (SimpC a))
forall a.
(Loc a, NFData a) =>
IBindEnv
-> BindEnv a
-> Config
-> [SimpC a]
-> Sol QBind
-> SolveM a (FixResult (SimpC a))
result_ IBindEnv
bindingsInSmt2 BindEnv a
be Config
cfg [SimpC a]
cs Sol QBind
s
    IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift       (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"RESULT: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FixResult (Maybe Integer) -> String
forall a. Show a => a -> String
show (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
F.sid (SimpC a -> Maybe Integer)
-> FixResult (SimpC a) -> FixResult (Maybe Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (SimpC a)
stat)
    FixSolution
resCut    <- Config -> Sol QBind -> SolveM a FixSolution
forall ann. Config -> Sol QBind -> SolveM ann FixSolution
solResult Config
cfg Sol QBind
s
    let resNonCut :: HashMap KVar (Delayed Pred)
resNonCut = Config -> BindEnv a -> Sol QBind -> HashMap KVar (Delayed Pred)
forall ann.
Config -> BindEnv ann -> Sol QBind -> HashMap KVar (Delayed Pred)
S.nonCutsResult Config
cfg BindEnv a
be Sol QBind
s
        resSorts :: HashMap KVar [(Symbol, Sort)]
resSorts = SInfo a -> [KVar] -> BindEnv a -> HashMap KVar [(Symbol, Sort)]
forall a.
SInfo a -> [KVar] -> BindEnv a -> HashMap KVar [(Symbol, Sort)]
resultSorts SInfo a
fi (FixSolution -> [KVar]
forall k v. HashMap k v -> [k]
M.keys FixSolution
resCut [KVar] -> [KVar] -> [KVar]
forall a. [a] -> [a] -> [a]
++ HashMap KVar (Delayed Pred) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys HashMap KVar (Delayed Pred)
resNonCut) BindEnv a
be
    Result (Integer, a) -> SolveM a (Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return     (Result (Integer, a) -> SolveM a (Result (Integer, a)))
-> Result (Integer, a) -> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ FixResult (Integer, a)
-> FixSolution
-> HashMap KVar (Delayed Pred)
-> HashMap KVar [(Symbol, Sort)]
-> Result (Integer, a)
forall a.
FixResult a
-> FixSolution
-> HashMap KVar (Delayed Pred)
-> HashMap KVar [(Symbol, Sort)]
-> Result a
F.Result (SimpC a -> (Integer, a)
forall {c :: * -> *} {b}. TaggedC c b => c b -> (Integer, b)
ci (SimpC a -> (Integer, a))
-> FixResult (SimpC a) -> FixResult (Integer, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (SimpC a)
stat) FixSolution
resCut HashMap KVar (Delayed Pred)
resNonCut HashMap KVar [(Symbol, Sort)]
resSorts
  where
    ci :: c b -> (Integer, b)
ci c b
c = (c b -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId c b
c, c b -> b
forall (c :: * -> *) a. TaggedC c a => c a -> a
F.sinfo c b
c)
    be :: BindEnv a
be = SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi

resultSorts :: F.SInfo a -> [F.KVar] -> F.BindEnv a -> F.ResultSorts
resultSorts :: forall a.
SInfo a -> [KVar] -> BindEnv a -> HashMap KVar [(Symbol, Sort)]
resultSorts SInfo a
fi [KVar]
ks BindEnv a
be = [(KVar, [(Symbol, Sort)])] -> HashMap KVar [(Symbol, Sort)]
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList
  [(KVar
k, [(Symbol, Sort)]
xts)
    | KVar
k <- [KVar]
ks
    , [(Symbol, Sort)]
xts <- Maybe [(Symbol, Sort)] -> [[(Symbol, Sort)]]
forall a. Maybe a -> [a]
maybeToList (SInfo a -> BindEnv a -> KVar -> Maybe [(Symbol, Sort)]
forall a. SInfo a -> BindEnv a -> KVar -> Maybe [(Symbol, Sort)]
kvarScope SInfo a
fi BindEnv a
be KVar
k) ]

kvarScope :: F.SInfo a -> F.BindEnv a -> F.KVar -> Maybe [(F.Symbol, F.Sort)]
kvarScope :: forall a. SInfo a -> BindEnv a -> KVar -> Maybe [(Symbol, Sort)]
kvarScope SInfo a
fi BindEnv a
be KVar
k = do
  WfC a
w <- KVar -> HashMap KVar (WfC a) -> Maybe (WfC a)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup KVar
k (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
fi)
  let bs :: IBindEnv
bs = WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
F.wenv WfC a
w
  let (Symbol
v, Sort
t, KVar
_) = WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
F.wrft WfC a
w
  [(Symbol, Sort)] -> Maybe [(Symbol, Sort)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Symbol, Sort)] -> Maybe [(Symbol, Sort)])
-> [(Symbol, Sort)] -> Maybe [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ (Symbol
v, Sort
t) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
: [ BindEnv a -> Int -> (Symbol, Sort)
forall a. BindEnv a -> Int -> (Symbol, Sort)
bindInfo BindEnv a
be Int
i | Int
i <- [Int] -> [Int]
forall a. Ord a => [a] -> [a]
L.sort (IBindEnv -> [Int]
F.elemsIBindEnv IBindEnv
bs) ]

bindInfo :: F.BindEnv a -> F.BindId -> (F.Symbol, F.Sort)
bindInfo :: forall a. BindEnv a -> Int -> (Symbol, Sort)
bindInfo BindEnv a
be Int
i = (Symbol
x, SortedReft -> Sort
F.sr_sort SortedReft
sr)
  where
    (Symbol
x, SortedReft
sr, a
_) = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv Int
i BindEnv a
be

solResult :: Config -> Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr)
solResult :: forall ann. Config -> Sol QBind -> SolveM ann FixSolution
solResult Config
cfg = Config -> FixSolution -> SolveM ann FixSolution
forall ann. Config -> FixSolution -> SolveM ann FixSolution
minimizeResult Config
cfg (FixSolution -> SolveM ann FixSolution)
-> (Sol QBind -> FixSolution)
-> Sol QBind
-> SolveM ann FixSolution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sol QBind -> FixSolution
Sol.result

result_
  :: (F.Loc a, NFData a)
  => F.IBindEnv
  -> F.BindEnv a
  -> Config
  -> [F.SimpC a]
  -> Sol.Solution
  -> SolveM a (F.FixResult (F.SimpC a))
result_ :: forall a.
(Loc a, NFData a) =>
IBindEnv
-> BindEnv a
-> Config
-> [SimpC a]
-> Sol QBind
-> SolveM a (FixResult (SimpC a))
result_ IBindEnv
bindingsInSmt BindEnv a
be Config
cfg [SimpC a]
cs0 Sol QBind
s = do
  [SimpC a]
unsatisfiedConstraints <- (SimpC a -> StateT (SolverState a) IO Bool)
-> [SimpC a] -> StateT (SolverState a) IO [SimpC a]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IBindEnv
-> BindEnv a
-> Sol QBind
-> SimpC a
-> StateT (SolverState a) IO Bool
forall a.
(Loc a, NFData a) =>
IBindEnv -> BindEnv a -> Sol QBind -> SimpC a -> SolveM a Bool
isUnsat IBindEnv
bindingsInSmt BindEnv a
be Sol QBind
s) [SimpC a]
cs
  Stats
sts      <- SolveM a Stats
forall ann. SolveM ann Stats
stats
  FixResult (SimpC a) -> SolveM a (FixResult (SimpC a))
forall a. a -> StateT (SolverState a) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FixResult (SimpC a) -> SolveM a (FixResult (SimpC a)))
-> FixResult (SimpC a) -> SolveM a (FixResult (SimpC a))
forall a b. (a -> b) -> a -> b
$ Stats -> [SimpC a] -> FixResult (SimpC a)
forall {a}. Stats -> [a] -> FixResult a
res Stats
sts [SimpC a]
unsatisfiedConstraints
  where
    cs :: [SimpC a]
cs          = Config -> [SimpC a] -> [SimpC a]
forall a. Config -> [SimpC a] -> [SimpC a]
isChecked Config
cfg [SimpC a]
cs0
    res :: Stats -> [a] -> FixResult a
res Stats
sts []  = Stats -> FixResult a
forall a. Stats -> FixResult a
F.Safe Stats
sts
    res Stats
sts [a]
cs' = Stats -> [a] -> FixResult a
forall {a}. Stats -> [a] -> FixResult a
F.Unsafe Stats
sts [a]
cs'

isChecked :: Config -> [F.SimpC a] -> [F.SimpC a]
isChecked :: forall a. Config -> [SimpC a] -> [SimpC a]
isChecked Config
cfg [SimpC a]
cs = case Config -> [Integer]
checkCstr Config
cfg of
  []   -> [SimpC a]
cs
  [Integer]
ids  -> let s :: HashSet Integer
s = [Integer] -> HashSet Integer
forall a. Hashable a => [a] -> HashSet a
S.fromList [Integer]
ids in
          [SimpC a
c | SimpC a
c <- [SimpC a]
cs, Integer -> HashSet Integer -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member (SimpC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c) HashSet Integer
s ]

--------------------------------------------------------------------------------
-- | `minimizeResult` transforms each KVar's result by removing
--   conjuncts that are implied by others. That is,
--
--      minimizeConjuncts :: ps:[Pred] -> {qs:[Pred] | subset qs ps}
--
--   such that `minimizeConjuncts ps` is a minimal subset of ps where no
--   is implied by /\_{q' in qs \ qs}
--   see: tests/pos/min00.fq for an example.
--------------------------------------------------------------------------------
minimizeResult :: Config -> M.HashMap F.KVar F.Expr
               -> SolveM ann (M.HashMap F.KVar F.Expr)
--------------------------------------------------------------------------------
minimizeResult :: forall ann. Config -> FixSolution -> SolveM ann FixSolution
minimizeResult Config
cfg FixSolution
s
  | Config -> Bool
minimalSol Config
cfg = (Pred -> StateT (SolverState ann) IO Pred)
-> FixSolution -> StateT (SolverState ann) IO FixSolution
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HashMap KVar a -> m (HashMap KVar b)
mapM Pred -> StateT (SolverState ann) IO Pred
forall ann. Pred -> SolveM ann Pred
minimizeConjuncts FixSolution
s
  | Bool
otherwise      = FixSolution -> StateT (SolverState ann) IO FixSolution
forall a. a -> StateT (SolverState ann) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FixSolution
s

minimizeConjuncts :: F.Expr -> SolveM ann F.Expr
minimizeConjuncts :: forall ann. Pred -> SolveM ann Pred
minimizeConjuncts Pred
p = [Pred] -> Pred
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd ([Pred] -> Pred)
-> StateT (SolverState ann) IO [Pred]
-> StateT (SolverState ann) IO Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
forall {ann}.
[Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go (Pred -> [Pred]
forall v. Eq v => ExprV v -> [ExprV v]
F.conjuncts Pred
p) []
  where
    go :: [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go []     [Pred]
acc   = [Pred] -> StateT (SolverState ann) IO [Pred]
forall a. a -> StateT (SolverState ann) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Pred]
acc
    go (Pred
p:[Pred]
ps) [Pred]
acc   = do Bool
b <- SrcSpan -> Pred -> Pred -> SolveM ann Bool
forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid SrcSpan
F.dummySpan ([Pred] -> Pred
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd ([Pred]
acc [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred]
ps)) Pred
p
                         if Bool
b then [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go [Pred]
ps [Pred]
acc
                              else [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go [Pred]
ps (Pred
pPred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:[Pred]
acc)

--------------------------------------------------------------------------------
isUnsat
  :: (F.Loc a, NFData a) => F.IBindEnv -> F.BindEnv a -> Sol.Solution -> F.SimpC a -> SolveM a Bool
--------------------------------------------------------------------------------
isUnsat :: forall a.
(Loc a, NFData a) =>
IBindEnv -> BindEnv a -> Sol QBind -> SimpC a -> SolveM a Bool
isUnsat IBindEnv
bindingsInSmt BindEnv a
be Sol QBind
s SimpC a
c = do
  -- lift   $ printf "isUnsat %s" (show (F.subcId c))
  Int
_     <- Bool -> SolveM a Int
forall ann. Bool -> SolveM ann Int
tickIter Bool
True -- newScc
  Config
cfg <- Context -> Config
T.config (Context -> Config)
-> StateT (SolverState a) IO Context
-> StateT (SolverState a) IO Config
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (SolverState a) IO Context
forall ann. SolveM ann Context
getContext
  let lp :: Pred
lp = Config -> IBindEnv -> BindEnv a -> Sol QBind -> SimpC a -> Pred
forall a.
Loc a =>
Config -> IBindEnv -> BindEnv a -> Sol QBind -> SimpC a -> Pred
S.lhsPred Config
cfg IBindEnv
bindingsInSmt BindEnv a
be Sol QBind
s SimpC a
c
      rp :: Pred
rp = SimpC a -> Pred
forall a. SimpC a -> Pred
rhsPred SimpC a
c
  Bool
res   <- Bool -> Bool
not (Bool -> Bool) -> SolveM a Bool -> SolveM a Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Pred -> Pred -> SolveM a Bool
forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid (SimpC a -> SrcSpan
forall a. Loc a => SimpC a -> SrcSpan
cstrSpan SimpC a
c) Pred
lp Pred
rp
  IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift   (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Pred -> Pred -> IO ()
showUnsat Bool
res (SimpC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c) Pred
lp Pred
rp
  Bool -> SolveM a Bool
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
res

showUnsat :: Bool -> Integer -> F.Pred -> F.Pred -> IO ()
showUnsat :: Bool -> Integer -> Pred -> Pred -> IO ()
showUnsat Bool
u Integer
i Pred
lP Pred
rP = {- when u $ -} do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf   String
"UNSAT id %s %s" (Integer -> String
forall a. Show a => a -> String
show Integer
i) (Bool -> String
forall a. Show a => a -> String
show Bool
u)
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. PPrint a => a -> String
showpp (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Doc
"LHS:" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. PPrint a => a -> Doc
pprint Pred
lP
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. PPrint a => a -> String
showpp (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Doc
"RHS:" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. PPrint a => a -> Doc
pprint Pred
rP

--------------------------------------------------------------------------------
-- | Predicate corresponding to RHS of constraint in current solution
--------------------------------------------------------------------------------
rhsPred :: F.SimpC a -> F.Expr
--------------------------------------------------------------------------------
rhsPred :: forall a. SimpC a -> Pred
rhsPred SimpC a
c
  | SimpC a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c = SimpC a -> Pred
forall (c :: * -> *) a. TaggedC c a => c a -> Pred
F.crhs SimpC a
c
  | Bool
otherwise  = String -> Pred
forall a. HasCallStack => String -> a
errorstar (String -> Pred) -> String -> Pred
forall a b. (a -> b) -> a -> b
$ String
"rhsPred on non-target: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe Integer -> String
forall a. Show a => a -> String
show (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
F.sid SimpC a
c)

--------------------------------------------------------------------------------
isValid :: F.SrcSpan -> F.Expr -> F.Expr -> SolveM ann Bool
--------------------------------------------------------------------------------
isValid :: forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid SrcSpan
sp Pred
p Pred
q = Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([()] -> Bool)
-> StateT (SolverState ann) IO [()]
-> StateT (SolverState ann) IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Pred -> Cand () -> StateT (SolverState ann) IO [()]
forall a ann. SrcSpan -> Pred -> Cand a -> SolveM ann [a]
filterValid SrcSpan
sp Pred
p [(Pred
q, ())]

cstrSpan :: (F.Loc a) => F.SimpC a -> F.SrcSpan
cstrSpan :: forall a. Loc a => SimpC a -> SrcSpan
cstrSpan = a -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan (a -> SrcSpan) -> (SimpC a -> a) -> SimpC a -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
F.sinfo

{-
---------------------------------------------------------------------------
donePhase' :: String -> SolveM ()
---------------------------------------------------------------------------
donePhase' msg = lift $ do
  threadDelay 25000
  putBlankLn
  donePhase Loud msg
-}