module Language.Fixpoint.Minimize ( minQuery ) where
import qualified Data.HashMap.Strict as M
import Control.Monad (filterM)
import Language.Fixpoint.Types.Config (Config (..))
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Utils.Files hiding (Result)
import Language.Fixpoint.Partition
import Language.Fixpoint.Types
import Control.DeepSeq
concatMapM :: (Monad m) => (a -> m [b]) -> [a] -> m [b]
concatMapM f = fmap concat . mapM f
minQuery :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a
-> IO (Result (Integer, a))
minQuery cfg solve fi = do
let cfg' = cfg { minimize = False }
let (_, fis) = partition' Nothing fi
failFis <- filterM (fmap isUnsafe . solve cfg') fis
failCs <- concatMapM (getMinFailingCons cfg' solve) failFis
let minFi = fi { cm = M.fromList failCs, fileName = minFileName fi }
saveQuery cfg' minFi
putStrLn $ "Minimized Constraints: " ++ show (fst <$> failCs)
return mempty
minFileName :: FInfo a -> FilePath
minFileName = extFileName Min . fileName
isUnsafe :: Result a -> Bool
isUnsafe (Result Safe _) = False
isUnsafe _ = True
type ConsList a = [(Integer, SubC a)]
type Oracle a c = (Config -> Solver a -> FInfo a -> [c] -> IO Bool)
deltaDebug :: Oracle a c -> Config -> Solver a -> FInfo a -> [c] -> [c] -> IO [c]
deltaDebug testSet cfg solve finfo set r = do
let (s1, s2) = splitAt (length set `div` 2) set
if length set == 1
then return set
else do
test1 <- testSet cfg solve finfo (s1 ++ r)
if test1
then deltaDebug testSet cfg solve finfo s1 r
else do
test2 <- testSet cfg solve finfo (s2 ++ r)
if test2
then deltaDebug testSet cfg solve finfo s2 r
else do
d1 <- deltaDebug testSet cfg solve finfo s1 (s2 ++ r)
d2 <- deltaDebug testSet cfg solve finfo s2 (s1 ++ r)
return (d1 ++ d2)
testConstraints :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a -> ConsList a -> IO Bool
testConstraints cfg solve fi cons = do
let fi' = fi { cm = M.fromList cons }
res <- solve cfg fi'
return $ isUnsafe res
getMinFailingCons :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a -> IO (ConsList a)
getMinFailingCons cfg solve fi = do
let cons = M.toList $ cm fi
deltaDebug testConstraints cfg solve fi cons []