-- | 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 #-}

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

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
import           Control.DeepSeq

---------------------------------------------------------------------------
-- polymorphic delta debugging implementation
---------------------------------------------------------------------------
deltaDebug :: Bool -> Oracle a c -> Config -> Solver a -> FInfo a -> [c] -> [c] -> IO [c]
deltaDebug :: 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) = Int -> [c] -> ([c], [c])
forall a. Int -> [a] -> ([a], [a])
splitAt ([c] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [c]
set Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [c]
set
  if [c] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [c]
set Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
    then Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
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 [c] -> [c] -> [c]
forall a. [a] -> [a] -> [a]
++ [c]
r)
      if Bool
test1
        then Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
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 [c] -> [c] -> [c]
forall a. [a] -> [a] -> [a]
++ [c]
r)
          if Bool
test2
            then Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
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 <- Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
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 [c] -> [c] -> [c]
forall a. [a] -> [a] -> [a]
++ [c]
r)
              [c]
d2 <- Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
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 [c] -> [c] -> [c]
forall a. [a] -> [a] -> [a]
++ [c]
r)
              [c] -> IO [c]
forall (m :: * -> *) a. Monad m => a -> m a
return ([c]
d1 [c] -> [c] -> [c]
forall a. [a] -> [a] -> [a]
++ [c]
d2)

deltaDebug1 :: Bool -> (a -> b -> c -> d -> IO Bool)
            -> a -> b -> c -> [e] -> d
            -> IO [e]
deltaDebug1 :: 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
_ = [e] -> IO [e]
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 [e] -> IO [e]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else [e] -> IO [e]
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 :: (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 = (FInfo a -> [c] -> FInfo a)
-> (Result (Integer, a) -> Bool) -> Oracle a c
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 <- Bool
-> Oracle a c
-> Config
-> Solver a
-> FInfo a
-> [c]
-> [c]
-> IO [c]
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
  Config -> FInfo a -> IO ()
forall a. Config -> FInfo a -> IO ()
saveQuery (Ext -> Config -> Config
addExt Ext
ext Config
cfg) FInfo a
minFi
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ FInfo a -> [c] -> String
formatter FInfo a
fi [c]
cs
  Result (Integer, a) -> IO (Result (Integer, a))
forall (m :: * -> *) a. Monad m => a -> m a
return Result (Integer, a)
forall a. Monoid a => a
mempty

---------------------------------------------------------------------------
minQuery :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a
         -> IO (Result (Integer, a))
---------------------------------------------------------------------------
minQuery :: 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   = Maybe MCInfo -> FInfo a -> [FInfo a]
forall (c :: * -> *) a.
TaggedC c a =>
Maybe MCInfo -> GInfo c a -> [GInfo c a]
partition' Maybe MCInfo
forall a. Maybe a
Nothing FInfo a
fi
  [FInfo a]
failFis  <- (FInfo a -> IO Bool) -> [FInfo a] -> IO [FInfo a]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Result (Integer, a) -> Bool)
-> IO (Result (Integer, a)) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool)
-> (Result (Integer, a) -> Bool) -> Result (Integer, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result (Integer, a) -> Bool
forall a. Result a -> Bool
isSafe) (IO (Result (Integer, a)) -> IO Bool)
-> (FInfo a -> IO (Result (Integer, a))) -> FInfo a -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solver a
solve Config
cfg') [FInfo a]
fis
  let failFi :: FInfo a
failFi = String -> [FInfo a] -> FInfo a
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f b -> String
forall a. Show a => a -> String
show ((b, b) -> b
forall a b. (a, b) -> a
fst ((b, b) -> b) -> f (b, b) -> f b
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 = [(Integer, c a)] -> HashMap Integer (c a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Integer, c a)]
cs }
  (FInfo a -> [(Integer, SubC a)])
-> (FInfo a -> [(Integer, SubC a)] -> FInfo a)
-> (Result (Integer, a) -> Bool)
-> Bool
-> Config
-> Solver a
-> FInfo a
-> Ext
-> (FInfo a -> [(Integer, SubC a)] -> String)
-> IO (Result (Integer, a))
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 (HashMap Integer (SubC a) -> [(Integer, SubC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Integer (SubC a) -> [(Integer, SubC a)])
-> (FInfo a -> HashMap Integer (SubC a))
-> FInfo a
-> [(Integer, SubC a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FInfo a -> HashMap Integer (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm) FInfo a -> [(Integer, SubC a)] -> FInfo a
forall (c :: * -> *) a (c :: * -> *).
GInfo c a -> [(Integer, c a)] -> GInfo c a
update (Bool -> Bool
not (Bool -> Bool)
-> (Result (Integer, a) -> Bool) -> Result (Integer, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result (Integer, a) -> Bool
forall a. Result a -> Bool
isSafe) Bool
True Config
cfg' Solver a
solve FInfo a
failFi Ext
Min FInfo a -> [(Integer, SubC a)] -> String
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 :: 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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
qs)
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"; Total Qualifiers: "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Qualifier] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Qualifier] -> Int) -> [Qualifier] -> Int
forall a b. (a -> b) -> a -> b
$ GInfo c a -> [Qualifier]
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 }
  (FInfo a -> [Qualifier])
-> (FInfo a -> [Qualifier] -> FInfo a)
-> (Result (Integer, a) -> Bool)
-> Bool
-> Config
-> Solver a
-> FInfo a
-> Ext
-> (FInfo a -> [Qualifier] -> String)
-> IO (Result (Integer, a))
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 -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals FInfo a -> [Qualifier] -> FInfo a
forall (c :: * -> *) a. GInfo c a -> [Qualifier] -> GInfo c a
update Result (Integer, a) -> Bool
forall a. Result a -> Bool
isSafe Bool
False Config
cfg' Solver a
solve FInfo a
fi Ext
MinQuals FInfo a -> [Qualifier] -> String
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 :: 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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ks)
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"; Total KVars: "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (HashMap KVar (WfC a) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (HashMap KVar (WfC a) -> Int) -> HashMap KVar (WfC a) -> Int
forall a b. (a -> b) -> a -> b
$ GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
fi)
  (FInfo a -> [KVar])
-> (FInfo a -> [KVar] -> FInfo a)
-> (Result (Integer, a) -> Bool)
-> Bool
-> Config
-> Solver a
-> FInfo a
-> Ext
-> (FInfo a -> [KVar] -> String)
-> IO (Result (Integer, a))
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 (HashMap KVar (WfC a) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys (HashMap KVar (WfC a) -> [KVar])
-> (FInfo a -> HashMap KVar (WfC a)) -> FInfo a -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws) FInfo a -> [KVar] -> FInfo a
forall a. FInfo a -> [KVar] -> FInfo a
removeOtherKs Result (Integer, a) -> Bool
forall a. Result a -> Bool
isSafe Bool
False Config
cfg' Solver a
solve FInfo a
fi Ext
MinKVars FInfo a -> [KVar] -> String
forall (t :: * -> *) (c :: * -> *) a a.
Foldable t =>
GInfo c a -> t a -> String
format

removeOtherKs :: FInfo a -> [KVar] -> FInfo a
removeOtherKs :: 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 = (KVar -> Maybe Expr) -> FInfo a -> FInfo a
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 KVar -> [KVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [KVar]
ks = Maybe Expr
forall a. Maybe a
Nothing
         | Bool
otherwise   = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
PTrue
    ws' :: HashMap KVar (WfC a)
ws' = (KVar -> WfC a -> Bool)
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\KVar
k WfC a
_ -> KVar
k KVar -> [KVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [KVar]
ks) (HashMap KVar (WfC a) -> HashMap KVar (WfC a))
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws FInfo a
fi1
    cm' :: HashMap Integer (SubC a)
cm' = (SubC a -> Bool)
-> HashMap Integer (SubC a) -> HashMap Integer (SubC a)
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter (SortedReft -> Bool
forall r. Reftable r => r -> Bool
isNonTrivial (SortedReft -> Bool) -> (SubC a -> SortedReft) -> SubC a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs) (HashMap Integer (SubC a) -> HashMap Integer (SubC a))
-> HashMap Integer (SubC a) -> HashMap Integer (SubC a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap Integer (SubC a)
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 :: (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'
  Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Result (Integer, a) -> Bool
checkRes Result (Integer, a)
res