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

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

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

import           Control.Monad (when, filterM)
import           Control.Monad.State.Strict (lift)
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 qualified Language.Fixpoint.Solver.Solution  as S
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

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

solve :: Config -> SInfo a -> IO (Result (Integer, a))
solve Config
cfg 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 Bool -> Bool -> Bool
|| Config -> Bool
gradual Config
cfg) then IO (Result (Integer, a), Stats) -> IO (Result (Integer, a), Stats)
forall a. a -> a
id else SolverInfo a (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall a b. SolverInfo a b -> IO b -> IO b
withProgressFI SolverInfo a (Result (Integer, a), Stats)
forall b. SolverInfo a b
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 Any
-> SolveM (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall b c a. Config -> SolverInfo b c -> SolveM a -> IO a
runSolverM Config
cfg SolverInfo a Any
forall b. SolverInfo a b
sI SolveM (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 (m :: * -> *) a. Monad m => a -> m a
return Result (Integer, a)
res
  where
    act :: SolveM (Result (Integer, a), Stats)
act  = Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM (Result (Integer, a), Stats)
forall a.
(NFData a, Fixpoint a, Loc a) =>
Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM (Result (Integer, a), Stats)
solve_ Config
cfg SInfo a
fi Solution
forall b. Sol b QBind
s0 HashSet KVar
ks  Worklist a
wkl
    sI :: SolverInfo a b
sI   = Config -> SInfo a -> SolverInfo a b
forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg SInfo a
fi
    wkl :: Worklist a
wkl  = SolverInfo a Any -> Worklist a
forall a b. SolverInfo a b -> Worklist a
W.init SolverInfo a Any
forall b. SolverInfo a b
sI
    s0 :: Sol b QBind
s0   = SolverInfo a b -> Sol b QBind
forall a b. SolverInfo a b -> Sol b QBind
siSol  SolverInfo a b
forall b. SolverInfo a b
sI
    ks :: HashSet KVar
ks   = SolverInfo a Any -> HashSet KVar
forall a b. SolverInfo a b -> HashSet KVar
siVars SolverInfo a Any
forall b. SolverInfo a b
sI


--------------------------------------------------------------------------------
-- | Progress Bar
--------------------------------------------------------------------------------
withProgressFI :: SolverInfo a b -> IO b -> IO b
withProgressFI :: SolverInfo a b -> 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 b -> Int) -> SolverInfo a b -> 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 b -> Int) -> SolverInfo a b -> 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 b -> Int) -> SolverInfo a b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CDeps -> Int
cNumScc (CDeps -> Int)
-> (SolverInfo a b -> CDeps) -> SolverInfo a b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverInfo a b -> CDeps
forall a b. SolverInfo a b -> CDeps
siDeps  
--------------------------------------------------------------------------------

printStats :: F.SInfo a ->  W.Worklist a -> Stats -> IO ()
printStats :: SInfo a -> Worklist a -> Stats -> IO ()
printStats SInfo a
fi Worklist a
w Stats
s = String -> IO ()
putStrLn String
"\n" IO () -> IO () -> IO ()
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 b
--------------------------------------------------------------------------------
solverInfo :: Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg SInfo a
fI
  | Config -> Bool
useElim Config
cfg = Config -> SInfo a -> SolverInfo a b
forall a b. Config -> SInfo a -> SolverInfo a b
E.solverInfo Config
cfg SInfo a
fI
  | Bool
otherwise   = Sol b QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a b
forall a b.
Sol b QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a b
SI Sol b 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 -> HashSet Symbol -> CDeps
forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> HashSet KVar -> HashSet Symbol -> 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 HashSet Symbol
forall a. Monoid a => a
mempty

siKvars :: F.SInfo a -> S.HashSet F.KVar
siKvars :: SInfo a -> HashSet KVar
siKvars = [KVar] -> HashSet KVar
forall a. (Eq 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

--------------------------------------------------------------------------------
solve_ :: (NFData a, F.Fixpoint a, F.Loc a)
       => Config
       -> F.SInfo a
       -> Sol.Solution
       -> S.HashSet F.KVar
       -> W.Worklist a
       -> SolveM (F.Result (Integer, a), Stats)
--------------------------------------------------------------------------------
solve_ :: Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM (Result (Integer, a), Stats)
solve_ Config
cfg SInfo a
fi Solution
s0 HashSet KVar
ks Worklist a
wkl = do
  let s1 :: Solution
s1   = {-# SCC "sol-init" #-} Config -> SInfo a -> HashSet KVar -> Solution
forall a.
Fixpoint a =>
Config -> SInfo a -> HashSet KVar -> Solution
S.init Config
cfg SInfo a
fi HashSet KVar
ks
  let s2 :: Solution
s2   = Solution -> Solution -> Solution
forall a. Monoid a => a -> a -> a
mappend Solution
s0 Solution
s1 
  -- let s3   = solveEbinds fi s2 
  Solution
s       <- {-# SCC "sol-refine" #-} Solution -> Worklist a -> SolveM Solution
forall a. Loc a => Solution -> Worklist a -> SolveM Solution
refine Solution
s2 Worklist a
wkl
  Result (Integer, a)
res     <- {-# SCC "sol-result" #-} Config -> Worklist a -> Solution -> SolveM (Result (Integer, a))
forall a.
(Fixpoint a, Loc a, NFData a) =>
Config -> Worklist a -> Solution -> SolveM (Result (Integer, a))
result Config
cfg Worklist a
wkl Solution
s
  Stats
st      <- SolveM Stats
stats
  let res' :: Result (Integer, a)
res' = {-# SCC "sol-tidy"   #-} Result (Integer, a) -> Result (Integer, a)
forall a. Result a -> Result a
tidyResult Result (Integer, a)
res
  (Result (Integer, a), Stats) -> SolveM (Result (Integer, a), Stats)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Result (Integer, a), Stats)
 -> SolveM (Result (Integer, a), Stats))
-> (Result (Integer, a), Stats)
-> SolveM (Result (Integer, a), Stats)
forall a b. NFData a => (a -> b) -> a -> b
$!! (Result (Integer, a)
res', Stats
st)

--------------------------------------------------------------------------------
-- | tidyResult ensures we replace the temporary kVarArg names introduced to
--   ensure uniqueness with the original names in the given WF constraints.
--------------------------------------------------------------------------------
tidyResult :: F.Result a -> F.Result a
tidyResult :: Result a -> Result a
tidyResult Result a
r = Result a
r { resSolution :: FixSolution
F.resSolution = FixSolution -> FixSolution
tidySolution (Result a -> FixSolution
forall a. Result a -> FixSolution
F.resSolution Result a
r) }

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

tidyPred :: F.Expr -> F.Expr
tidyPred :: Expr -> Expr
tidyPred = (Symbol -> Expr) -> Expr -> Expr
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Symbol -> Expr) -> (Symbol -> Symbol) -> Symbol -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
F.tidySymbol)

--------------------------------------------------------------------------------
refine :: (F.Loc a) => Sol.Solution -> W.Worklist a -> SolveM Sol.Solution
--------------------------------------------------------------------------------
refine :: Solution -> Worklist a -> SolveM Solution
refine Solution
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 Int
tickIter Bool
newScc
     (Bool
b, Solution
s') <- Int -> Solution -> SimpC a -> SolveM (Bool, Solution)
forall a.
Loc a =>
Int -> Solution -> SimpC a -> SolveM (Bool, Solution)
refineC Int
i Solution
s SimpC a
c
     IO () -> StateT SolverState IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT SolverState IO ())
-> IO () -> StateT SolverState 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
forall t t t (c :: * -> *) a a.
(PrintfArg t, PrintfArg t, PrintfType t, TaggedC c a, Show a) =>
t -> c a -> a -> t -> t
refineMsg Int
i SimpC a
c Bool
b Int
rnk
     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'
     Solution -> Worklist a -> SolveM Solution
forall a. Loc a => Solution -> Worklist a -> SolveM Solution
refine Solution
s' Worklist a
w''
  | Bool
otherwise = Solution -> SolveM Solution
forall (m :: * -> *) a. Monad m => a -> m a
return Solution
s
  where
    -- DEBUG
    refineMsg :: t -> c a -> a -> t -> t
refineMsg t
i c a
c a
b t
rnk = String -> t -> Integer -> String -> t -> t
forall r. PrintfType r => String -> r
printf String
"\niter=%d id=%d change=%s rank=%d\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

---------------------------------------------------------------------------
-- | Single Step Refinement -----------------------------------------------
---------------------------------------------------------------------------
refineC :: (F.Loc a) => Int -> Sol.Solution -> F.SimpC a
        -> SolveM (Bool, Sol.Solution)
---------------------------------------------------------------------------
refineC :: Int -> Solution -> SimpC a -> SolveM (Bool, Solution)
refineC Int
_i Solution
s SimpC a
c
  | [(Expr, (KVar, EQual))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Expr, (KVar, EQual))]
rhs  = (Bool, Solution) -> SolveM (Bool, Solution)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Solution
s)
  | Bool
otherwise = do BindEnv
be     <- SolveM BindEnv
getBinds
                   let lhs :: Expr
lhs = BindEnv -> Solution -> SimpC a -> Expr
forall a. Loc a => BindEnv -> Solution -> SimpC a -> Expr
S.lhsPred BindEnv
be Solution
s SimpC a
c
                   [(KVar, EQual)]
kqs    <- SrcSpan
-> Expr -> [(Expr, (KVar, EQual))] -> SolveM [(KVar, EQual)]
forall a. SrcSpan -> Expr -> Cand a -> SolveM [a]
filterValid (SimpC a -> SrcSpan
forall a. Loc a => SimpC a -> SrcSpan
cstrSpan SimpC a
c) Expr
lhs [(Expr, (KVar, EQual))]
rhs
                   (Bool, Solution) -> SolveM (Bool, Solution)
forall (m :: * -> *) a. Monad m => a -> m a
return  ((Bool, Solution) -> SolveM (Bool, Solution))
-> (Bool, Solution) -> SolveM (Bool, Solution)
forall a b. (a -> b) -> a -> b
$ Solution -> [KVar] -> [(KVar, EQual)] -> (Bool, Solution)
forall a.
Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
S.update Solution
s [KVar]
ks [(KVar, EQual)]
kqs
  where
    _ci :: Integer
_ci       = SimpC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c
    ([KVar]
ks, [(Expr, (KVar, EQual))]
rhs) = Solution -> SimpC a -> ([KVar], [(Expr, (KVar, EQual))])
forall a. Solution -> SimpC a -> ([KVar], [(Expr, (KVar, EQual))])
rhsCands Solution
s SimpC a
c
    -- msg       = printf "refineC: iter = %d, sid = %s, soln = \n%s\n"
    --               _i (show (F.sid c)) (showpp s)
    _msg :: a -> t a -> t a -> t
_msg a
ks t a
xs t a
ys = String -> Int -> String -> String -> Int -> Int -> t
forall r. PrintfType r => String -> r
printf String
"refineC: iter = %d, sid = %s, s = %s, rhs = %d, rhs' = %d \n"
                     Int
_i (Integer -> String
forall a. Show a => a -> String
show Integer
_ci) (a -> String
forall a. PPrint a => a -> String
showpp a
ks) (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
xs) (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ys)

rhsCands :: Sol.Solution -> F.SimpC a -> ([F.KVar], Sol.Cand (F.KVar, Sol.EQual))
rhsCands :: Solution -> SimpC a -> ([KVar], [(Expr, (KVar, EQual))])
rhsCands Solution
s SimpC a
c    = ((KVar, Subst) -> KVar
forall a b. (a, b) -> a
fst ((KVar, Subst) -> KVar) -> [(KVar, Subst)] -> [KVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, Subst)]
ks, [(Expr, (KVar, EQual))]
kqs)
  where
    kqs :: [(Expr, (KVar, EQual))]
kqs         = [ (Expr
p, (KVar
k, EQual
q)) | (KVar
k, Subst
su) <- [(KVar, Subst)]
ks, (Expr
p, EQual
q)  <- KVar -> Subst -> [(Expr, EQual)]
cnd KVar
k Subst
su ]
    ks :: [(KVar, Subst)]
ks          = Expr -> [(KVar, Subst)]
predKs (Expr -> [(KVar, Subst)])
-> (SimpC a -> Expr) -> SimpC a -> [(KVar, Subst)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs (SimpC a -> [(KVar, Subst)]) -> SimpC a -> [(KVar, Subst)]
forall a b. (a -> b) -> a -> b
$ SimpC a
c
    cnd :: KVar -> Subst -> [(Expr, EQual)]
cnd KVar
k Subst
su    = String -> Solution -> Subst -> QBind -> [(Expr, EQual)]
forall a.
String -> Sol a QBind -> Subst -> QBind -> [(Expr, EQual)]
Sol.qbPreds String
msg Solution
s Subst
su (Solution -> KVar -> QBind
forall a. Sol a QBind -> KVar -> QBind
Sol.lookupQBind Solution
s KVar
k)
    msg :: String
msg         = String
"rhsCands: " 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)

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

--------------------------------------------------------------------------------
-- | Convert Solution into Result ----------------------------------------------
--------------------------------------------------------------------------------
result :: (F.Fixpoint a, F.Loc a, NFData a) => Config -> W.Worklist a -> Sol.Solution
       -> SolveM (F.Result (Integer, a))
--------------------------------------------------------------------------------
result :: Config -> Worklist a -> Solution -> SolveM (Result (Integer, a))
result Config
cfg Worklist a
wkl Solution
s = do
  IO () -> StateT SolverState IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT SolverState IO ())
-> IO () -> StateT SolverState IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
writeLoud String
"Computing Result"
  FixResult (SimpC a)
stat    <- Config -> Worklist a -> Solution -> SolveM (FixResult (SimpC a))
forall a.
(Loc a, NFData a) =>
Config -> Worklist a -> Solution -> SolveM (FixResult (SimpC a))
result_ Config
cfg Worklist a
wkl Solution
s
  IO () -> StateT SolverState IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT SolverState IO ())
-> IO () -> StateT SolverState 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)

  FixResult (Integer, a)
-> FixSolution -> GFixSolution -> Result (Integer, a)
forall a. FixResult a -> FixSolution -> GFixSolution -> 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 -> GFixSolution -> Result (Integer, a))
-> StateT SolverState IO FixSolution
-> StateT SolverState IO (GFixSolution -> Result (Integer, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config -> Solution -> StateT SolverState IO FixSolution
solResult Config
cfg Solution
s StateT SolverState IO (GFixSolution -> Result (Integer, a))
-> StateT SolverState IO GFixSolution
-> SolveM (Result (Integer, a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GFixSolution -> StateT SolverState IO GFixSolution
forall (m :: * -> *) a. Monad m => a -> m a
return GFixSolution
forall a. Monoid a => a
mempty
  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)

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

result_ :: (F.Loc a, NFData a) => Config -> W.Worklist a -> Sol.Solution -> SolveM (F.FixResult (F.SimpC a))
result_ :: Config -> Worklist a -> Solution -> SolveM (FixResult (SimpC a))
result_  Config
cfg Worklist a
w Solution
s = do
  [SimpC a]
filtered <- (SimpC a -> StateT SolverState IO Bool)
-> [SimpC a] -> StateT SolverState IO [SimpC a]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Solution -> SimpC a -> StateT SolverState IO Bool
forall a.
(Loc a, NFData a) =>
Solution -> SimpC a -> StateT SolverState IO Bool
isUnsat Solution
s) [SimpC a]
cs
  Stats
sts      <- SolveM Stats
stats
  FixResult (SimpC a) -> SolveM (FixResult (SimpC a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FixResult (SimpC a) -> SolveM (FixResult (SimpC a)))
-> FixResult (SimpC a) -> SolveM (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]
filtered
  where
    cs :: [SimpC a]
cs          = Config -> [SimpC a] -> [SimpC a]
forall a. Config -> [SimpC a] -> [SimpC a]
isChecked Config
cfg (Worklist a -> [SimpC a]
forall a. Worklist a -> [SimpC a]
W.unsatCandidates Worklist a
w)
    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 :: 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. (Eq 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. (Eq 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 (M.HashMap F.KVar F.Expr)
--------------------------------------------------------------------------------
minimizeResult :: Config -> FixSolution -> StateT SolverState IO FixSolution
minimizeResult Config
cfg FixSolution
s
  | Config -> Bool
minimalSol Config
cfg = (Expr -> StateT SolverState IO Expr)
-> FixSolution -> StateT SolverState IO FixSolution
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr -> StateT SolverState IO Expr
minimizeConjuncts FixSolution
s
  | Bool
otherwise      = FixSolution -> StateT SolverState IO FixSolution
forall (m :: * -> *) a. Monad m => a -> m a
return FixSolution
s

minimizeConjuncts :: F.Expr -> SolveM F.Expr
minimizeConjuncts :: Expr -> StateT SolverState IO Expr
minimizeConjuncts Expr
p = [Expr] -> Expr
F.pAnd ([Expr] -> Expr)
-> StateT SolverState IO [Expr] -> StateT SolverState IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr] -> [Expr] -> StateT SolverState IO [Expr]
go (Expr -> [Expr]
F.conjuncts Expr
p) []
  where
    go :: [Expr] -> [Expr] -> StateT SolverState IO [Expr]
go []     [Expr]
acc   = [Expr] -> StateT SolverState IO [Expr]
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
acc
    go (Expr
p:[Expr]
ps) [Expr]
acc   = do Bool
b <- SrcSpan -> Expr -> Expr -> StateT SolverState IO Bool
isValid SrcSpan
F.dummySpan ([Expr] -> Expr
F.pAnd ([Expr]
acc [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
ps)) Expr
p
                         if Bool
b then [Expr] -> [Expr] -> StateT SolverState IO [Expr]
go [Expr]
ps [Expr]
acc
                              else [Expr] -> [Expr] -> StateT SolverState IO [Expr]
go [Expr]
ps (Expr
pExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
acc)

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

showUnsat :: Bool -> Integer -> F.Pred -> F.Pred -> IO ()
showUnsat :: Bool -> Integer -> Expr -> Expr -> IO ()
showUnsat Bool
u Integer
i Expr
lP Expr
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
<+> Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
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
<+> Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
rP

--------------------------------------------------------------------------------
-- | Predicate corresponding to RHS of constraint in current solution
--------------------------------------------------------------------------------
rhsPred :: F.SimpC a -> F.Expr
--------------------------------------------------------------------------------
rhsPred :: SimpC a -> Expr
rhsPred SimpC a
c
  | SimpC a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c = SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC a
c
  | Bool
otherwise  = String -> Expr
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> Expr) -> String -> Expr
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 Bool
--------------------------------------------------------------------------------
isValid :: SrcSpan -> Expr -> Expr -> StateT SolverState IO Bool
isValid SrcSpan
sp Expr
p Expr
q = (Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([()] -> Bool)
-> StateT SolverState IO [()] -> StateT SolverState IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Expr -> Cand () -> StateT SolverState IO [()]
forall a. SrcSpan -> Expr -> Cand a -> SolveM [a]
filterValid SrcSpan
sp Expr
p [(Expr
q, ())]

cstrSpan :: (F.Loc a) => F.SimpC a -> F.SrcSpan
cstrSpan :: 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
-}


-- NV TODO Move to a new file
-------------------------------------------------------------------------------
-- | Interaction with the user when Solving -----------------------------------
-------------------------------------------------------------------------------

_iMergePartitions :: [(Int, F.SInfo a)] -> IO [(Int, F.SInfo a)]
_iMergePartitions :: [(Int, SInfo a)] -> IO [(Int, SInfo a)]
_iMergePartitions [(Int, SInfo a)]
ifis = do
  String -> IO ()
putStrLn String
"Current Partitions are: "
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ((Int, SInfo a) -> String
forall a. (Int, SInfo a) -> String
partitionInfo ((Int, SInfo a) -> String) -> [(Int, SInfo a)] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, SInfo a)]
ifis)
  String -> IO ()
putStrLn String
"Merge Partitions? Y/N"
  Char
c <- IO Char
getChar
  if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'N'
    then do String -> IO ()
putStrLn String
"Solving Partitions"
            [(Int, SInfo a)] -> IO [(Int, SInfo a)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, SInfo a)]
ifis
    else do
      (Int
i, Int
j) <- Int -> IO (Int, Int)
getMergePartition ([(Int, SInfo a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, SInfo a)]
ifis)
      [(Int, SInfo a)] -> IO [(Int, SInfo a)]
forall a. [(Int, SInfo a)] -> IO [(Int, SInfo a)]
_iMergePartitions (Int -> Int -> [(Int, SInfo a)] -> [(Int, SInfo a)]
forall a. Int -> Int -> [(Int, SInfo a)] -> [(Int, SInfo a)]
mergePartitions Int
i Int
j [(Int, SInfo a)]
ifis)

getMergePartition :: Int -> IO (Int, Int)
getMergePartition :: Int -> IO (Int, Int)
getMergePartition Int
n = do
  String -> IO ()
putStrLn String
"Which two partition to merge? (i, j)"
  String
ic <- IO String
getLine
  let (Int
i,Int
j) = String -> (Int, Int)
forall a. Read a => String -> a
read String
ic :: (Int, Int)
  if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j
    then do String -> IO ()
putStrLn (String
"Invalid Partition numbers, write (i,j) with 1 <= i <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
            Int -> IO (Int, Int)
getMergePartition Int
n
    else (Int, Int) -> IO (Int, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i,Int
j)

mergePartitions :: Int -> Int -> [(Int, F.SInfo a)] -> [(Int, F.SInfo a)]
mergePartitions :: Int -> Int -> [(Int, SInfo a)] -> [(Int, SInfo a)]
mergePartitions Int
i Int
j [(Int, SInfo a)]
fis
  = [Int] -> [SInfo a] -> [(Int, SInfo a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] ((Int -> SInfo a
takei Int
i SInfo a -> SInfo a -> SInfo a
forall a. Monoid a => a -> a -> a
`mappend` (Int -> SInfo a
takei Int
j){bs :: BindEnv
F.bs = BindEnv
forall a. Monoid a => a
mempty})SInfo a -> [SInfo a] -> [SInfo a]
forall a. a -> [a] -> [a]
:[SInfo a]
rest)
  where
    takei :: Int -> SInfo a
takei Int
i = (Int, SInfo a) -> SInfo a
forall a b. (a, b) -> b
snd ([(Int, SInfo a)]
fis [(Int, SInfo a)] -> Int -> (Int, SInfo a)
forall a. [a] -> Int -> a
L.!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    rest :: [SInfo a]
rest = (Int, SInfo a) -> SInfo a
forall a b. (a, b) -> b
snd ((Int, SInfo a) -> SInfo a) -> [(Int, SInfo a)] -> [SInfo a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, SInfo a) -> Bool) -> [(Int, SInfo a)] -> [(Int, SInfo a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
k,SInfo a
_) -> (Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i Bool -> Bool -> Bool
&& Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j)) [(Int, SInfo a)]
fis

partitionInfo :: (Int, F.SInfo a) -> String
partitionInfo :: (Int, SInfo a) -> String
partitionInfo (Int
i, SInfo a
fi)
  = String
"Partition number " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
    String
"Defined ?? " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SrcSpan] -> String
forall a. Show a => a -> String
show [SrcSpan]
defs    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
    String
"Used ?? "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Maybe SrcSpan] -> String
forall a. Show a => a -> String
show [Maybe SrcSpan]
uses
  where
    gs :: [GradInfo]
gs   = WfC a -> GradInfo
forall a. WfC a -> GradInfo
F.wloc (WfC a -> GradInfo)
-> ((KVar, WfC a) -> WfC a) -> (KVar, WfC a) -> GradInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar, WfC a) -> WfC a
forall a b. (a, b) -> b
snd ((KVar, WfC a) -> GradInfo) -> [(KVar, WfC a)] -> [GradInfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((KVar, WfC a) -> Bool) -> [(KVar, WfC a)] -> [(KVar, WfC a)]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (WfC a -> Bool
forall a. WfC a -> Bool
F.isGWfc (WfC a -> Bool)
-> ((KVar, WfC a) -> WfC a) -> (KVar, WfC a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar, WfC a) -> WfC a
forall a b. (a, b) -> b
snd) (HashMap KVar (WfC a) -> [(KVar, WfC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
fi))
    defs :: [SrcSpan]
defs = [SrcSpan] -> [SrcSpan]
forall a. Eq a => [a] -> [a]
L.nub (GradInfo -> SrcSpan
F.gsrc (GradInfo -> SrcSpan) -> [GradInfo] -> [SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GradInfo]
gs)
    uses :: [Maybe SrcSpan]
uses = [Maybe SrcSpan] -> [Maybe SrcSpan]
forall a. Eq a => [a] -> [a]
L.nub (GradInfo -> Maybe SrcSpan
F.gused (GradInfo -> Maybe SrcSpan) -> [GradInfo] -> [Maybe SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GradInfo]
gs)