-- | This module implements a "delta-debugging" based query minimizer.
--   Exported clients of that minimizer include one that attempts to
--   shrink UNSAT queries down to a minimal subset of constraints,
--   one that shrinks SAT queries down to a minimal subset of qualifiers,
--   and one that shrinks SAT queries down to a minimal subset of KVars
--   (replacing all others by True).

{-# LANGUAGE ScopedTypeVariables #-}

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

module Language.Fixpoint.Minimize ( minQuery, minQuals, minKvars ) where

import Prelude hiding (min, init)
import qualified Data.HashMap.Strict                as M
import           Control.Monad                      (filterM)
import           Language.Fixpoint.Types.Visitor    (mapKVars)
import           Language.Fixpoint.Types.Config     (Config (..), queryFile)
import           Language.Fixpoint.Misc             (safeHead)
import           Language.Fixpoint.Utils.Files      hiding (Result)
import           Language.Fixpoint.Graph
import           Language.Fixpoint.Types            hiding (fi)
import           Control.DeepSeq

---------------------------------------------------------------------------
-- polymorphic delta debugging implementation
---------------------------------------------------------------------------
deltaDebug :: Bool -> Oracle a c -> Config -> Solver a -> FInfo a -> [c] -> [c] -> IO [c]
deltaDebug :: forall a c.
Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
deltaDebug Bool
min Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo [c]
set [c]
r = do
  let ([c]
s1, [c]
s2) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length [c]
set forall a. Integral a => a -> a -> a
`div` Int
2) [c]
set
  if forall (t :: * -> *) a. Foldable t => t a -> Int
length [c]
set forall a. Eq a => a -> a -> Bool
== Int
1
    then forall a b c d e.
Bool
-> (a -> b -> c -> d -> IO Bool)
-> a
-> b
-> c
-> [e]
-> d
-> IO [e]
deltaDebug1 Bool
min Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo [c]
set [c]
r
    else do
      Bool
test1 <- Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo ([c]
s1 forall a. [a] -> [a] -> [a]
++ [c]
r)
      if Bool
test1
        then forall a c.
Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
deltaDebug Bool
min Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo [c]
s1 [c]
r
        else do
          Bool
test2 <- Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo ([c]
s2 forall a. [a] -> [a] -> [a]
++ [c]
r)
          if Bool
test2
            then forall a c.
Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
deltaDebug Bool
min Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo [c]
s2 [c]
r
            else do
              [c]
d1 <- forall a c.
Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
deltaDebug Bool
min Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo [c]
s1 ([c]
s2 forall a. [a] -> [a] -> [a]
++ [c]
r)
              [c]
d2 <- forall a c.
Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
deltaDebug Bool
min Oracle a c
testSet Config
cfg Solver a
solve FInfo a
finfo [c]
s2 ([c]
d1 forall a. [a] -> [a] -> [a]
++ [c]
r)
              forall (m :: * -> *) a. Monad m => a -> m a
return ([c]
d1 forall a. [a] -> [a] -> [a]
++ [c]
d2)

deltaDebug1 :: Bool -> (a -> b -> c -> d -> IO Bool)
            -> a -> b -> c -> [e] -> d
            -> IO [e]
deltaDebug1 :: forall a b c d e.
Bool
-> (a -> b -> c -> d -> IO Bool)
-> a
-> b
-> c
-> [e]
-> d
-> IO [e]
deltaDebug1 Bool
True  a -> b -> c -> d -> IO Bool
_       a
_   b
_     c
_     [e]
set d
_ = forall (m :: * -> *) a. Monad m => a -> m a
return [e]
set
deltaDebug1 Bool
False a -> b -> c -> d -> IO Bool
testSet a
cfg b
solve c
finfo [e]
set d
r = do
  Bool
test <- a -> b -> c -> d -> IO Bool
testSet a
cfg b
solve c
finfo d
r
  if Bool
test then forall (m :: * -> *) a. Monad m => a -> m a
return [] else forall (m :: * -> *) a. Monad m => a -> m a
return [e]
set

type Oracle a c = (Config -> Solver a -> FInfo a -> [c] -> IO Bool)

commonDebug :: (NFData a, Fixpoint a) => (FInfo a -> [c])
                                      -> (FInfo a -> [c] -> FInfo a)
                                      -> (Result (Integer, a) -> Bool)
                                      -> Bool
                                      -> Config
                                      -> Solver a
                                      -> FInfo a
                                      -> Ext
                                      -> (FInfo a -> [c] -> String)
                                      -> IO (Result (Integer, a))
commonDebug :: forall a c.
(NFData a, Fixpoint a) =>
(FInfo a -> [c])
-> (FInfo a -> [c] -> FInfo a)
-> (Result (Integer, a) -> Bool)
-> Bool
-> Config
-> Solver a
-> FInfo a
-> Ext
-> (FInfo a -> [c] -> String)
-> IO (Result (Integer, a))
commonDebug FInfo a -> [c]
init FInfo a -> [c] -> FInfo a
updateFi Result (Integer, a) -> Bool
checkRes Bool
min Config
cfg Solver a
solve FInfo a
fi Ext
ext FInfo a -> [c] -> String
formatter = do
  let cs0 :: [c]
cs0 = FInfo a -> [c]
init FInfo a
fi
  let oracle :: Oracle a c
oracle = forall a c.
(NFData a, Fixpoint a) =>
(FInfo a -> [c] -> FInfo a)
-> (Result (Integer, a) -> Bool) -> Oracle a c
mkOracle FInfo a -> [c] -> FInfo a
updateFi Result (Integer, a) -> Bool
checkRes
  [c]
cs <- forall a c.
Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
deltaDebug Bool
min Oracle a c
oracle Config
cfg Solver a
solve FInfo a
fi [c]
cs0 []
  let minFi :: FInfo a
minFi = FInfo a -> [c] -> FInfo a
updateFi FInfo a
fi [c]
cs
  forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveQuery (Ext -> Config -> Config
addExt Ext
ext Config
cfg) FInfo a
minFi
  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ FInfo a -> [c] -> String
formatter FInfo a
fi [c]
cs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty

---------------------------------------------------------------------------
minQuery :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a
         -> IO (Result (Integer, a))
---------------------------------------------------------------------------
minQuery :: forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minQuery Config
cfg Solver a
solve FInfo a
fi = do
  let cfg' :: Config
cfg'  = Config
cfg { minimize :: Bool
minimize = Bool
False }
  let fis :: [FInfo a]
fis   = forall (c :: * -> *) a.
TaggedC c a =>
Maybe MCInfo -> GInfo c a -> [GInfo c a]
partition' forall a. Maybe a
Nothing FInfo a
fi
  [FInfo a]
failFis  <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Result a -> Bool
isSafe) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solver a
solve Config
cfg') [FInfo a]
fis
  let failFi :: FInfo a
failFi = forall a. (?callStack::CallStack) => String -> ListNE a -> a
safeHead String
"--minimize can only be called on UNSAT fq" [FInfo a]
failFis
  let format :: p -> f (b, b) -> String
format p
_ f (b, b)
cs = String
"Minimized Constraints: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (b, b)
cs)
  let update :: GInfo c a -> [(Integer, c a)] -> GInfo c a
update GInfo c a
fi' [(Integer, c a)]
cs = GInfo c a
fi' { cm :: HashMap Integer (c a)
cm = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Integer, c a)]
cs }
  forall a c.
(NFData a, Fixpoint a) =>
(FInfo a -> [c])
-> (FInfo a -> [c] -> FInfo a)
-> (Result (Integer, a) -> Bool)
-> Bool
-> Config
-> Solver a
-> FInfo a
-> Ext
-> (FInfo a -> [c] -> String)
-> IO (Result (Integer, a))
commonDebug (forall k v. HashMap k v -> [(k, v)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm) forall {c :: * -> *} {a} {c :: * -> *}.
GInfo c a -> [(Integer, c a)] -> GInfo c a
update (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Result a -> Bool
isSafe) Bool
True Config
cfg' Solver a
solve FInfo a
failFi Ext
Min forall {f :: * -> *} {b} {p} {b}.
(Show (f b), Functor f) =>
p -> f (b, b) -> String
format

---------------------------------------------------------------------------
minQuals :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a
         -> IO (Result (Integer, a))
---------------------------------------------------------------------------
minQuals :: forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minQuals Config
cfg Solver a
solve FInfo a
fi = do
  let cfg' :: Config
cfg'  = Config
cfg { minimizeQs :: Bool
minimizeQs = Bool
False }
  let format :: GInfo c a -> t a -> String
format GInfo c a
fi' t a
qs = String
"Required Qualifiers: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
qs)
                  forall a. [a] -> [a] -> [a]
++ String
"; Total Qualifiers: "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
fi')
  let update :: GInfo c a -> [Qualifier] -> GInfo c a
update GInfo c a
fi' [Qualifier]
qs = GInfo c a
fi' { quals :: [Qualifier]
quals = [Qualifier]
qs }
  forall a c.
(NFData a, Fixpoint a) =>
(FInfo a -> [c])
-> (FInfo a -> [c] -> FInfo a)
-> (Result (Integer, a) -> Bool)
-> Bool
-> Config
-> Solver a
-> FInfo a
-> Ext
-> (FInfo a -> [c] -> String)
-> IO (Result (Integer, a))
commonDebug forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals forall {c :: * -> *} {a}. GInfo c a -> [Qualifier] -> GInfo c a
update forall a. Result a -> Bool
isSafe Bool
False Config
cfg' Solver a
solve FInfo a
fi Ext
MinQuals forall {t :: * -> *} {c :: * -> *} {a} {a}.
Foldable t =>
GInfo c a -> t a -> String
format

---------------------------------------------------------------------------
minKvars :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a
         -> IO (Result (Integer, a))
---------------------------------------------------------------------------
minKvars :: forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minKvars Config
cfg Solver a
solve FInfo a
fi = do
  let cfg' :: Config
cfg'  = Config
cfg { minimizeKs :: Bool
minimizeKs = Bool
False }
  let format :: GInfo c a -> t a -> String
format GInfo c a
fi' t a
ks = String
"Required KVars: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ks)
                  forall a. [a] -> [a] -> [a]
++ String
"; Total KVars: "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
fi')
  forall a c.
(NFData a, Fixpoint a) =>
(FInfo a -> [c])
-> (FInfo a -> [c] -> FInfo a)
-> (Result (Integer, a) -> Bool)
-> Bool
-> Config
-> Solver a
-> FInfo a
-> Ext
-> (FInfo a -> [c] -> String)
-> IO (Result (Integer, a))
commonDebug (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)
ws) forall a. FInfo a -> [KVar] -> FInfo a
removeOtherKs forall a. Result a -> Bool
isSafe Bool
False Config
cfg' Solver a
solve FInfo a
fi Ext
MinKVars forall {t :: * -> *} {c :: * -> *} {a} {a}.
Foldable t =>
GInfo c a -> t a -> String
format

removeOtherKs :: FInfo a -> [KVar] -> FInfo a
removeOtherKs :: forall a. FInfo a -> [KVar] -> FInfo a
removeOtherKs FInfo a
fi0 [KVar]
ks = FInfo a
fi1 { ws :: HashMap KVar (WfC a)
ws = HashMap KVar (WfC a)
ws', cm :: HashMap Integer (SubC a)
cm = HashMap Integer (SubC a)
cm' }
  where
    fi1 :: FInfo a
fi1 = forall t. Visitable t => (KVar -> Maybe Expr) -> t -> t
mapKVars KVar -> Maybe Expr
go FInfo a
fi0
    go :: KVar -> Maybe Expr
go KVar
k | KVar
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [KVar]
ks = forall a. Maybe a
Nothing
         | Bool
otherwise   = forall a. a -> Maybe a
Just Expr
PTrue
    ws' :: HashMap KVar (WfC a)
ws' = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\KVar
k WfC a
_ -> KVar
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [KVar]
ks) forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws FInfo a
fi1
    cm' :: HashMap Integer (SubC a)
cm' = forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter (forall r. Reftable r => r -> Bool
isNonTrivial forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SubC a -> SortedReft
srhs) forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm FInfo a
fi1

---------------------------------------------------------------------------
-- Helper functions
---------------------------------------------------------------------------
addExt :: Ext -> Config -> Config
addExt :: Ext -> Config -> Config
addExt Ext
ext Config
cfg = Config
cfg { srcFile :: String
srcFile = Ext -> Config -> String
queryFile Ext
ext Config
cfg }

mkOracle :: (NFData a, Fixpoint a) => (FInfo a -> [c] -> FInfo a)
                                   -> (Result (Integer, a) -> Bool)
                                   -> Oracle a c
mkOracle :: forall a c.
(NFData a, Fixpoint a) =>
(FInfo a -> [c] -> FInfo a)
-> (Result (Integer, a) -> Bool) -> Oracle a c
mkOracle FInfo a -> [c] -> FInfo a
updateFi Result (Integer, a) -> Bool
checkRes Config
cfg Solver a
solve FInfo a
fi [c]
qs = do
  let fi' :: FInfo a
fi' = FInfo a -> [c] -> FInfo a
updateFi FInfo a
fi [c]
qs
  Result (Integer, a)
res <- Solver a
solve Config
cfg FInfo a
fi'
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Result (Integer, a) -> Bool
checkRes Result (Integer, a)
res