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

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

--------------------------------------------------------------------------------
-- | 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 (liftIO, modify, 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
import Language.Fixpoint.Types (resStatus, FixResult(Unsafe))
import qualified Language.Fixpoint.Types.Config as C
import Language.Fixpoint.Solver.Interpreter (instInterpreter)
import Language.Fixpoint.Solver.Instantiate (instantiate)
--import Debug.Trace                      (trace)

mytrace :: String -> a -> a
mytrace :: forall a. [Char] -> a -> a
mytrace [Char]
_ a
x = {- trace -} a
x

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

solve :: forall a.
(NFData a, Fixpoint a, Show a, Loc a) =>
Config -> SInfo a -> IO (Result (Integer, a))
solve Config
cfg SInfo a
fi = do
    IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ Moods -> [Char] -> IO ()
donePhase Moods
Misc.Loud [Char]
"Worklist Initialize"
    Verbosity
vb <- IO Verbosity
getVerbosity
    (Result (Integer, a)
res, Stats
stat) <- (if Verbosity
Quiet forall a. Eq a => a -> a -> Bool
== Verbosity
vb Bool -> Bool -> Bool
|| Config -> Bool
gradual Config
cfg then forall a. a -> a
id else forall a b. SolverInfo a b -> IO b -> IO b
withProgressFI forall {b}. SolverInfo a b
sI) forall a b. (a -> b) -> a -> b
$ forall ann c a. Config -> SolverInfo ann c -> SolveM ann a -> IO a
runSolverM Config
cfg forall {b}. SolverInfo a b
sI SolveM a (Result (Integer, a), Stats)
act
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
solverStats Config
cfg) forall a b. (a -> b) -> a -> b
$ forall a. SInfo a -> Worklist a -> Stats -> IO ()
printStats SInfo a
fi Worklist a
wkl Stats
stat
    -- print (numIter stat)
    forall (m :: * -> *) a. Monad m => a -> m a
return Result (Integer, a)
res
  where
    act :: SolveM a (Result (Integer, a), Stats)
act  = forall a.
(NFData a, Fixpoint a, Loc a) =>
Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM a (Result (Integer, a), Stats)
solve_ Config
cfg SInfo a
fi forall {b}. Sol b QBind
s0 HashSet KVar
ks  Worklist a
wkl
    sI :: SolverInfo a b
sI   = forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg SInfo a
fi
    wkl :: Worklist a
wkl  = forall a b. SolverInfo a b -> Worklist a
W.init forall {b}. SolverInfo a b
sI
    s0 :: Sol b QBind
s0   = forall a b. SolverInfo a b -> Sol b QBind
siSol  forall {b}. SolverInfo a b
sI
    ks :: HashSet KVar
ks   = forall a b. SolverInfo a b -> HashSet KVar
siVars forall {b}. SolverInfo a b
sI


--------------------------------------------------------------------------------
-- | Progress Bar
--------------------------------------------------------------------------------
withProgressFI :: SolverInfo a b -> IO b -> IO b
withProgressFI :: forall a b. SolverInfo a b -> IO b -> IO b
withProgressFI = forall a. Int -> IO a -> IO a
withProgress forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Num a => a -> a -> a
+ Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. CDeps -> Int
cNumScc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. SolverInfo a b -> 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 = [Char] -> IO ()
putStrLn [Char]
"\n" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [DocTable] -> IO ()
ppTs [ forall a. PTable a => a -> DocTable
ptable SInfo a
fi, forall a. PTable a => a -> DocTable
ptable Stats
s, forall a. PTable a => a -> DocTable
ptable Worklist a
w ]
  where
    ppTs :: [DocTable] -> IO ()
ppTs          = [Char] -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => a -> [Char]
showpp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => [a] -> a
mconcat

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

siKvars :: F.SInfo a -> S.HashSet F.KVar
siKvars :: forall a. SInfo a -> HashSet KVar
siKvars = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [k]
M.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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.SInfo a)
doInterpret :: forall a.
Loc a =>
Config -> SInfo a -> [Integer] -> SolveM a (SInfo a)
doInterpret Config
cfg SInfo a
fi0 [Integer]
subcIds = do
  SInfo a
fi <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a.
Loc a =>
Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
instInterpreter Config
cfg SInfo a
fi0 (forall a. a -> Maybe a
Just [Integer]
subcIds)
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall {ann} {ann}. SInfo ann -> SolverState ann -> SolverState ann
update' SInfo a
fi
  forall (m :: * -> *) a. Monad m => a -> m a
return SInfo a
fi
  where
    update' :: SInfo ann -> SolverState ann -> SolverState ann
update' SInfo ann
fi SolverState ann
ss = SolverState ann
ss{ssBinds :: BindEnv ann
ssBinds = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo ann
fi'}
      where
        fi' :: SInfo ann
fi' = (forall a b. SolverInfo a b -> SInfo a
siQuery forall {b}. SolverInfo ann b
sI) {hoInfo :: HOInfo
F.hoInfo = Bool -> Bool -> HOInfo
F.HOI (Config -> Bool
C.allowHO Config
cfg) (Config -> Bool
C.allowHOqs Config
cfg)}
        sI :: SolverInfo ann b
sI  = forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg SInfo ann
fi

{-# SCC doPLE #-}
doPLE :: (F.Loc a) =>  Config -> F.SInfo a -> [F.SubcId] -> SolveM a ()
doPLE :: forall a. Loc a => Config -> SInfo a -> [Integer] -> SolveM a ()
doPLE Config
cfg SInfo a
fi0 [Integer]
subcIds = do
  SInfo a
fi <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a.
Loc a =>
Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
instantiate Config
cfg SInfo a
fi0 (forall a. a -> Maybe a
Just [Integer]
subcIds)
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall {ann} {ann}. SInfo ann -> SolverState ann -> SolverState ann
update' SInfo a
fi
  where
    update' :: SInfo ann -> SolverState ann -> SolverState ann
update' SInfo ann
fi SolverState ann
ss = SolverState ann
ss{ssBinds :: BindEnv ann
ssBinds = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo ann
fi'}
      where
        fi' :: SInfo ann
fi' = (forall a b. SolverInfo a b -> SInfo a
siQuery forall {b}. SolverInfo ann b
sI) {hoInfo :: HOInfo
F.hoInfo = Bool -> Bool -> HOInfo
F.HOI (Config -> Bool
C.allowHO Config
cfg) (Config -> Bool
C.allowHOqs Config
cfg)}
        sI :: SolverInfo ann b
sI  = forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg SInfo ann
fi

--------------------------------------------------------------------------------
{-# SCC solve_ #-}
solve_ :: (NFData a, F.Fixpoint a, F.Loc a)
       => Config
       -> F.SInfo a
       -> Sol.Solution
       -> S.HashSet F.KVar
       -> W.Worklist a
       -> SolveM a (F.Result (Integer, a), Stats)
--------------------------------------------------------------------------------
solve_ :: forall a.
(NFData a, Fixpoint a, Loc a) =>
Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM a (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" #-} forall a.
Fixpoint a =>
Config -> SInfo a -> HashSet KVar -> Solution
S.init Config
cfg SInfo a
fi HashSet KVar
ks
  let s2 :: Solution
s2   = forall a. Monoid a => a -> a -> a
mappend Solution
s0 Solution
s1
  (Solution
s3, Result (Integer, a)
res0) <- forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt -> do
    -- let s3   = solveEbinds fi s2
    Solution
s3       <- {- SCC "sol-refine" -} forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s2 Worklist a
wkl
    Result (Integer, a)
res0     <- {- SCC "sol-result" -} forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s3
    forall (m :: * -> *) a. Monad m => a -> m a
return (Solution
s3, Result (Integer, a)
res0)

  (SInfo a
fi1, Solution
s4, Result (Integer, a)
res1) <- case forall a. Result a -> FixResult a
resStatus Result (Integer, a)
res0 of  {- first run the interpreter -}
    Unsafe Stats
_ [(Integer, a)]
bads | Bool -> Bool
not (Config -> Bool
noLazyPLE Config
cfg) Bool -> Bool -> Bool
&& Config -> Bool
rewriteAxioms Config
cfg Bool -> Bool -> Bool
&& Config -> Bool
interpreter Config
cfg -> do
      SInfo a
fi1 <- forall a.
Loc a =>
Config -> SInfo a -> [Integer] -> SolveM a (SInfo a)
doInterpret Config
cfg SInfo a
fi (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> a
mytrace ([Char]
"before the Interpreter " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Integer, a)]
bads) forall a. [a] -> [a] -> [a]
++ [Char]
" constraints remain") [(Integer, a)]
bads)
      (Solution
s4, Result (Integer, a)
res1) <-  forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt -> do
        Solution
s4    <- {- SCC "sol-refine" -} forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s3 Worklist a
wkl
        Result (Integer, a)
res1  <- {- SCC "sol-result" -} forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s4
        forall (m :: * -> *) a. Monad m => a -> m a
return (Solution
s4, Result (Integer, a)
res1)
      forall (m :: * -> *) a. Monad m => a -> m a
return (SInfo a
fi1, Solution
s4, Result (Integer, a)
res1)
    FixResult (Integer, a)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return  (SInfo a
fi, Solution
s3, forall a. [Char] -> a -> a
mytrace [Char]
"all checked before interpreter" Result (Integer, a)
res0)

  Result (Integer, a)
res2  <- case 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 | Bool -> Bool
not (Config -> Bool
noLazyPLE Config
cfg) Bool -> Bool -> Bool
&& Config -> Bool
rewriteAxioms Config
cfg -> do
      forall a. Loc a => Config -> SInfo a -> [Integer] -> SolveM a ()
doPLE Config
cfg SInfo a
fi1 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> a
mytrace ([Char]
"before z3 PLE " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Integer, a)]
bads2) forall a. [a] -> [a] -> [a]
++ [Char]
" constraints remain") [(Integer, a)]
bads2)
      forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt -> do
        Solution
s5    <- {- SCC "sol-refine" -} forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s4 Worklist a
wkl
        forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s5
    FixResult (Integer, a)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> a
mytrace [Char]
"all checked with interpreter" Result (Integer, a)
res1

  Stats
st      <- forall ann. SolveM ann Stats
stats
  let res3 :: Result (Integer, a)
res3 = {- SCC "sol-tidy" -} forall a. Result a -> Result a
tidyResult Result (Integer, a)
res2
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: F.Result a -> F.Result a
tidyResult :: forall a. Result a -> Result a
tidyResult Result a
r = Result a
r
  { resSolution :: FixSolution
F.resSolution = FixSolution -> FixSolution
tidySolution (forall a. Result a -> FixSolution
F.resSolution Result a
r)
  , resNonCutsSolution :: FixSolution
F.resNonCutsSolution = FixSolution -> FixSolution
tidySolution (forall a. Result a -> FixSolution
F.resNonCutsSolution Result a
r)
  }

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

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

--------------------------------------------------------------------------------
{-# SCC refine #-}
refine
  :: (F.Loc a)
  => F.IBindEnv
  -> Sol.Solution
  -> W.Worklist a
  -> SolveM a Sol.Solution
--------------------------------------------------------------------------------
refine :: forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s Worklist a
w
  | Just (SimpC a
c, Worklist a
w', Bool
newScc, Int
rnk) <- forall a. Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)
W.pop Worklist a
w = do
     Int
i       <- forall ann. Bool -> SolveM ann Int
tickIter Bool
newScc
     (Bool
b, Solution
s') <- forall a.
Loc a =>
IBindEnv -> Int -> Solution -> SimpC a -> SolveM a (Bool, Solution)
refineC IBindEnv
bindingsInSmt Int
i Solution
s SimpC a
c
     forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
writeLoud forall a b. (a -> b) -> a -> b
$ 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 forall a. SimpC a -> Worklist a -> Worklist a
W.push SimpC a
c Worklist a
w' else Worklist a
w'
     forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s' Worklist a
w''
  | Bool
otherwise = 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 = forall r. PrintfType r => [Char] -> r
printf [Char]
"\niter=%d id=%d change=%s rank=%d\n"
                            t
i (forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId c a
c) (forall a. Show a => a -> [Char]
show a
b) t
rnk

---------------------------------------------------------------------------
-- | Single Step Refinement -----------------------------------------------
---------------------------------------------------------------------------
{-# SCC refineC #-}
refineC
  :: (F.Loc a)
  => F.IBindEnv
  -> Int
  -> Sol.Solution
  -> F.SimpC a
  -> SolveM a (Bool, Sol.Solution)
---------------------------------------------------------------------------
refineC :: forall a.
Loc a =>
IBindEnv -> Int -> Solution -> SimpC a -> SolveM a (Bool, Solution)
refineC IBindEnv
bindingsInSmt Int
_i Solution
s SimpC a
c
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Cand (KVar, EQual)
rhs  = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Solution
s)
  | Bool
otherwise = do BindEnv a
be     <- forall ann. SolveM ann (BindEnv ann)
getBinds
                   let lhs :: Pred
lhs = forall a.
Loc a =>
IBindEnv -> BindEnv a -> Solution -> SimpC a -> Pred
S.lhsPred IBindEnv
bindingsInSmt BindEnv a
be Solution
s SimpC a
c
                   [(KVar, EQual)]
kqs    <- forall a ann. SrcSpan -> Pred -> Cand a -> SolveM ann [a]
filterValid (forall a. Loc a => SimpC a -> SrcSpan
cstrSpan SimpC a
c) Pred
lhs Cand (KVar, EQual)
rhs
                   forall (m :: * -> *) a. Monad m => a -> m a
return  forall a b. (a -> b) -> a -> b
$ 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       = forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c
    ([KVar]
ks, Cand (KVar, EQual)
rhs) = forall a. Solution -> SimpC a -> ([KVar], Cand (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 = forall r. PrintfType r => [Char] -> r
printf [Char]
"refineC: iter = %d, sid = %s, s = %s, rhs = %d, rhs' = %d \n"
                     Int
_i (forall a. Show a => a -> [Char]
show Integer
_ci) (forall a. PPrint a => a -> [Char]
showpp a
ks) (forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
xs) (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 :: forall a. Solution -> SimpC a -> ([KVar], Cand (KVar, EQual))
rhsCands Solution
s SimpC a
c    = (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, Subst)]
ks, Cand (KVar, EQual)
kqs)
  where
    kqs :: Cand (KVar, EQual)
kqs         = [ (Pred
p, (KVar
k, EQual
q)) | (KVar
k, Subst
su) <- [(KVar, Subst)]
ks, (Pred
p, EQual
q)  <- KVar -> Subst -> [(Pred, EQual)]
cnd KVar
k Subst
su ]
    ks :: [(KVar, Subst)]
ks          = Pred -> [(KVar, Subst)]
predKs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> Pred
F.crhs forall a b. (a -> b) -> a -> b
$ SimpC a
c
    cnd :: KVar -> Subst -> [(Pred, EQual)]
cnd KVar
k Subst
su    = forall a.
[Char] -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]
Sol.qbPreds [Char]
msg Solution
s Subst
su (forall a. Sol a QBind -> KVar -> QBind
Sol.lookupQBind Solution
s KVar
k)
    msg :: [Char]
msg         = [Char]
"rhsCands: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
F.sid SimpC a
c)

predKs :: F.Expr -> [(F.KVar, F.Subst)]
predKs :: Pred -> [(KVar, Subst)]
predKs (F.PAnd [Pred]
ps)    = 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
  -> W.Worklist a
  -> Sol.Solution
  -> SolveM a (F.Result (Integer, a))
--------------------------------------------------------------------------------
result :: forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s =
  forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
bindingsInSmt forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt2 -> do
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
writeLoud [Char]
"Computing Result"
    FixResult (SimpC a)
stat    <- forall a.
(Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (FixResult (SimpC a))
result_ IBindEnv
bindingsInSmt2 Config
cfg Worklist a
wkl Solution
s
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"RESULT: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
F.sid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (SimpC a)
stat)

    forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
F.Result (forall {c :: * -> *} {b}. TaggedC c b => c b -> (Integer, b)
ci forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (SimpC a)
stat) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann. Config -> Solution -> SolveM ann FixSolution
solResult Config
cfg Solution
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ann. Solution -> SolveM ann FixSolution
solNonCutsResult Solution
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
  where
    ci :: c b -> (Integer, b)
ci c b
c = (forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId c b
c, forall (c :: * -> *) a. TaggedC c a => c a -> a
F.sinfo c b
c)

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

solNonCutsResult :: Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr)
solNonCutsResult :: forall ann. Solution -> SolveM ann FixSolution
solNonCutsResult Solution
s = do
  BindEnv ann
be <- forall ann. SolveM ann (BindEnv ann)
getBinds
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ann a. BindEnv ann -> Sol a QBind -> FixSolution
S.nonCutsResult BindEnv ann
be Solution
s

result_
  :: (F.Loc a, NFData a)
  => F.IBindEnv
  -> Config
  -> W.Worklist a
  -> Sol.Solution
  -> SolveM a (F.FixResult (F.SimpC a))
result_ :: forall a.
(Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (FixResult (SimpC a))
result_ IBindEnv
bindingsInSmt Config
cfg Worklist a
w Solution
s = do
  [SimpC a]
filtered <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall a.
(Loc a, NFData a) =>
IBindEnv -> Solution -> SimpC a -> SolveM a Bool
isUnsat IBindEnv
bindingsInSmt Solution
s) [SimpC a]
cs
  Stats
sts      <- forall ann. SolveM ann Stats
stats
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {a}. Stats -> [a] -> FixResult a
res Stats
sts [SimpC a]
filtered
  where
    cs :: [SimpC a]
cs          = forall a. Config -> [SimpC a] -> [SimpC a]
isChecked Config
cfg (forall a. Worklist a -> [SimpC a]
W.unsatCandidates Worklist a
w)
    res :: Stats -> [a] -> FixResult a
res Stats
sts []  = forall a. Stats -> FixResult a
F.Safe Stats
sts
    res Stats
sts [a]
cs' = 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 = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Integer]
ids in
          [SimpC a
c | SimpC a
c <- [SimpC a]
cs, forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall ann. Pred -> SolveM ann Pred
minimizeConjuncts FixSolution
s
  | Bool
otherwise      = 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
F.pAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {ann}.
[Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go (Pred -> [Pred]
F.conjuncts Pred
p) []
  where
    go :: [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go []     [Pred]
acc   = forall (m :: * -> *) a. Monad m => a -> m a
return [Pred]
acc
    go (Pred
p:[Pred]
ps) [Pred]
acc   = do Bool
b <- forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid SrcSpan
F.dummySpan ([Pred] -> Pred
F.pAnd ([Pred]
acc 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
pforall a. a -> [a] -> [a]
:[Pred]
acc)

--------------------------------------------------------------------------------
isUnsat
  :: (F.Loc a, NFData a) => F.IBindEnv -> Sol.Solution -> F.SimpC a -> SolveM a Bool
--------------------------------------------------------------------------------
isUnsat :: forall a.
(Loc a, NFData a) =>
IBindEnv -> Solution -> SimpC a -> SolveM a Bool
isUnsat IBindEnv
bindingsInSmt Solution
s SimpC a
c = do
  -- lift   $ printf "isUnsat %s" (show (F.subcId c))
  Int
_     <- forall ann. Bool -> SolveM ann Int
tickIter Bool
True -- newScc
  BindEnv a
be    <- forall ann. SolveM ann (BindEnv ann)
getBinds
  let lp :: Pred
lp = forall a.
Loc a =>
IBindEnv -> BindEnv a -> Solution -> SimpC a -> Pred
S.lhsPred IBindEnv
bindingsInSmt BindEnv a
be Solution
s SimpC a
c
  let rp :: Pred
rp = forall a. SimpC a -> Pred
rhsPred        SimpC a
c
  Bool
res   <- Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid (forall a. Loc a => SimpC a -> SrcSpan
cstrSpan SimpC a
c) Pred
lp Pred
rp
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift   forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Pred -> Pred -> IO ()
showUnsat Bool
res (forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c) Pred
lp Pred
rp
  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
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => [Char] -> r
printf   [Char]
"UNSAT id %s %s" (forall a. Show a => a -> [Char]
show Integer
i) (forall a. Show a => a -> [Char]
show Bool
u)
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> [Char]
showpp forall a b. (a -> b) -> a -> b
$ Doc
"LHS:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Pred
lP
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> [Char]
showpp forall a b. (a -> b) -> a -> b
$ Doc
"RHS:" Doc -> Doc -> 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
  | forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c = forall (c :: * -> *) a. TaggedC c a => c a -> Pred
F.crhs SimpC a
c
  | Bool
otherwise  = forall a. (?callStack::CallStack) => [Char] -> a
errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"rhsPred on non-target: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall a. Loc a => a -> SrcSpan
F.srcSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. [(Int, SInfo a)] -> IO [(Int, SInfo a)]
_iMergePartitions [(Int, SInfo a)]
ifis = do
  [Char] -> IO ()
putStrLn [Char]
"Current Partitions are: "
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines (forall a. (Int, SInfo a) -> [Char]
partitionInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, SInfo a)]
ifis)
  [Char] -> IO ()
putStrLn [Char]
"Merge Partitions? Y/N"
  Char
c <- IO Char
getChar
  if Char
c forall a. Eq a => a -> a -> Bool
== Char
'N'
    then do [Char] -> IO ()
putStrLn [Char]
"Solving Partitions"
            forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, SInfo a)]
ifis
    else do
      (Int
i, Int
j) <- Int -> IO (Int, Int)
getMergePartition (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, SInfo a)]
ifis)
      forall a. [(Int, SInfo a)] -> IO [(Int, SInfo a)]
_iMergePartitions (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
  [Char] -> IO ()
putStrLn [Char]
"Which two partition to merge? (i, j)"
  [Char]
ic <- IO [Char]
getLine
  let (Int
i,Int
j) = forall a. Read a => [Char] -> a
read [Char]
ic :: (Int, Int)
  if Int
i forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
n forall a. Ord a => a -> a -> Bool
< Int
i Bool -> Bool -> Bool
|| Int
j forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
n forall a. Ord a => a -> a -> Bool
< Int
j
    then do [Char] -> IO ()
putStrLn ([Char]
"Invalid Partition numbers, write (i,j) with 1 <= i <= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
            Int -> IO (Int, Int)
getMergePartition Int
n
    else 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 :: forall a. Int -> Int -> [(Int, SInfo a)] -> [(Int, SInfo a)]
mergePartitions Int
i Int
j [(Int, SInfo a)]
fis
  = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] ((Int -> SInfo a
takei Int
i forall a. Monoid a => a -> a -> a
`mappend` (Int -> SInfo a
takei Int
j){bs :: BindEnv a
F.bs = forall a. Monoid a => a
mempty})forall a. a -> [a] -> [a]
:[SInfo a]
rest)
  where
    takei :: Int -> SInfo a
takei Int
i = forall a b. (a, b) -> b
snd ([(Int, SInfo a)]
fis forall a. [a] -> Int -> a
L.!! (Int
i forall a. Num a => a -> a -> a
- Int
1))
    rest :: [SInfo a]
rest = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
k,SInfo a
_) -> Int
k forall a. Eq a => a -> a -> Bool
/= Int
i Bool -> Bool -> Bool
&& Int
k forall a. Eq a => a -> a -> Bool
/= Int
j) [(Int, SInfo a)]
fis

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