twee-2.6.1: misc/BestTwee.hs
{-# LANGUAGE TemplateHaskell #-}
module Main where
import MaxCover
import System.FilePath
import System.FilePath.Glob
import System.Directory
import Control.Monad
import Data.Ord
import Data.List
import Data.Maybe
import Data.Time.Clock
import qualified Data.Map as Map
import Data.Map(Map)
import Data.FileEmbed
solvedInTime :: NominalDiffTime -> FilePath -> String -> IO Bool
solvedInTime timeLimit dir prob = do
let
stdout = dir </> prob ++ ".p.stdout"
stderr = dir </> prob ++ ".p.stderr"
outTime <- getModificationTime stdout
errTime <- getModificationTime stderr
return (diffUTCTime outTime errTime <= timeLimit)
notE :: [(String, Double)]
notE = filter (\(x, _) -> '+' `notElem` x) [
("GRP702+1", 0.06), ("GRP715+1", 0.06), ("GRP660+2", 0.12), ("GRP660+3", 0.12),
("GRP665+1", 0.12), ("GRP700+1", 0.12), ("GRP658+1", 0.18), ("GRP659+1", 0.18),
("GRP656+1", 0.24), ("GRP657+1", 0.24), ("GRP660+1", 0.24), ("GRP682+1", 0.24),
("GRP683+1", 0.24), ("GRP685+1", 0.24), ("GRP703+1", 0.24), ("GRP704+1", 0.24),
("GRP710+1", 0.24), ("GRP777+1", 0.24), ("LCL897+1", 0.29), ("LAT168-1", 0.30),
("LAT171-1", 0.43), ("ALG240-1", 0.48), ("GRP654+2", 0.53), ("GRP654+3", 0.53),
("GRP655+2", 0.53), ("GRP655+3", 0.53), ("LAT174-1", 0.65), ("LAT142-1", 0.70),
("GRP654+1", 0.71), ("GRP655+1", 0.71), ("GRP505-1", 0.74), ("LAT145-1", 0.74),
("LAT164-1", 0.74), ("GRP506-1", 0.78), ("GRP507-1", 0.78), ("LAT018-1", 0.78),
("LAT148-1", 0.78), ("LAT153-1", 0.78), ("LAT155-1", 0.78), ("GRP508-1", 0.83),
("KLE151-10", 0.83), ("LAT162-1", 0.83), ("LAT146-1", 0.87), ("LAT159-1", 0.87),
("LAT160-1", 0.87), ("LAT170-1", 0.87), ("LAT177-1", 0.87), ("GRP664+1", 0.88),
("ALG441-10", 0.91), ("COL042-10", 0.91), ("GRP196-1", 0.91), ("GRP666-3", 0.91),
("GRP666-4", 0.91), ("GRP666-5", 0.91), ("LAT156-1", 0.91), ("LAT169-1", 0.91),
("LCL148-10", 0.91), ("GRP164-2", 0.96), ("GRP666-2", 0.96), ("GRP678-1", 0.96),
("GRP725-1", 0.96), ("KLE110-10", 0.96), ("LAT072-1", 0.96), ("LAT076-1", 0.96),
("LAT140-1", 0.96), ("LAT141-1", 0.96), ("LAT144-1", 0.96), ("LAT147-1", 0.96),
("LAT149-1", 0.96), ("LAT151-1", 0.96), ("LAT158-1", 0.96), ("LAT163-1", 0.96),
("LAT167-1", 0.96), ("LAT172-1", 0.96), ("LAT173-1", 0.96), ("LAT175-1", 0.96),
("LAT176-1", 0.96), ("LCL927-10", 0.96), ("REL040-1", 0.96), ("REL040-3", 0.96),
("ALG212+1", 1.00), ("ALG213+1", 1.00), ("GRP724-1", 1.00), ("KLE122-10", 1.00),
("LAT074-1", 1.00), ("LAT075-1", 1.00), ("LAT077-1", 1.00), ("LAT078-1", 1.00),
("LAT079-1", 1.00), ("LAT139-1", 1.00), ("LAT161-1", 1.00), ("LCL220-10", 1.00),
("LCL330-10", 1.00), ("LCL348-10", 1.00), ("REL032-2", 1.00), ("REL038-1", 1.00),
("REL039-1", 1.00)]
ratings :: Map String Double
ratings =
Map.fromList
[ (name, read rating)
| [name, rating] <- map words (lines input)]
where
input = $(embedStringFile "ratings")
problemBonus :: (Int, Int, Int, Int, Int, Int) -> String -> Int
problemBonus (b0, b1, b2, b3, b4, b5) p =
ebonus *
case Map.lookup p ratings of
Nothing -> b0
Just x
| x < 0.7 -> b1
| x < 0.8 -> b2
| x < 0.9 -> b3
| x < 0.95 -> b4
| otherwise -> b5
where
ebonus =
case lookup p notE of
Nothing -> 1
Just _ -> 1
greatProblemsBonus :: (Int, Int, Int, Int, Int, Int) -> String -> [String]
greatProblemsBonus b p =
[p ++ "/" ++ show i | i <- [1..problemBonus b p]]
bonuses :: [(String, (Int, Int, Int, Int, Int, Int))]
bonuses =
[("no bonus", (1, 1, 1, 1, 1, 1)),
--("low bonus", (1, 1, 2, 3, 5, 10)),
("medium bonus", (1, 2, 4, 6, 8, 10)),
--("high bonus", (0, 1, 2, 3, 4, 5)),
--("big fish", (0, 0, 0, 0, 1, 1)),
("rating 1", (0, 0, 0, 0, 0, 1))]
readResults ok = do
filenames <- glob "/home/nick/twee-out/*/times"
fmap (filter (\(x, _) -> x `notElem` banned)) $ forM filenames $ \filename -> do
let name = takeFileName (takeDirectory filename)
let unpack xs = (takeBaseName name, read time :: Double) where [name, time] = words xs
solved <- filter (ok . fst) . map unpack . lines <$> readFile filename
let solvedInTime t = [name | (name, time) <- solved, time < t]
-- fast <- filterM (solvedInTime 120 directory) solved
-- med <- filterM (solvedInTime 240 directory) solved
-- slow <- filterM (solvedInTime 600 directory) solved
let fast = solvedInTime 120
let med = solvedInTime 210
let slow = solvedInTime (1/0)
return (name, (fast, med, slow))
score results cover =
length (usort (concat [probs | (name, probs) <- results, name `elem` cover]))
levels results name names =
[ (i, length xs)
| i <- [0..length names],
let xs = find name \\ concatMap find (take i names),
not (null xs) ]
where
find x = fromJust (lookup x results)
main = do
--probs <- lines <$> readFile "unsat"
results <- readResults (const True) -- `elem` probs)
let
options =
[("fast", \(fast, _, _) -> (fast, [], [])),
("med", \(_, med, _) -> ([], med, []))]
--("slow", \(_, _, slow) -> ([], [], slow))]
--("fast and med", \(fast, med, _) -> (fast, med, []))]
forM_ bonuses $ \(bonus, b) -> do
forM_ options $ \(option, f) -> do
let
results1 =
[ (name,
map (++ "/fast") (concatMap (greatProblemsBonus b) fast) ++
map (++ "/med") (concatMap (greatProblemsBonus b) med) ++
map (++ "/slow") (concatMap (greatProblemsBonus b) slow))
| (name, res) <- results,
let (fast, med, slow) = f res ]
best = greedy results1
putStrLn (option ++ "/" ++ bonus ++ ":")
forM_ (take 8 $ zip3 [1..] best (inits best)) $ \(i, name, names) -> do
putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (drop (length fixed) $ levels results1 name names))
putStrLn ""
{-
putStrLn "Best:"
forM_ [1..6] $ \i -> do
cover <- maxCover i results1
putStrLn (show i ++ ": " ++ show (score results1 cover))
forM_ cover $ \name -> putStrLn (" " ++ name)
-}
greedy [] = []
greedy results =
best:
greedy (map deleteResults (delete (best, probs) results))
where
(best, probs) = maximumBy (comparing f) results
deleteResults (name, probs') = (name, probs' \\ probs)
f (name, probs) =
case elemIndex name fixed of
Just i -> Right (-i)
Nothing -> Left (length probs)
fixed :: [String]
fixed = [
"twee-250707-casc---lhs-weight-1---flip-ordering---normalise-queue-percent-10---cp-renormalise-threshold-10---complete-subsets---ground-joining-incomplete-limit-15",
"twee-250707-casc---no-flatten-goal---ground-joining-incomplete-limit-15"
]
fixed_new = take 6 [
"twee-210619-twee-casc-extra-lhsnormal-flatten",
"twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",
"twee-210619-twee-casc-extra-depth-60",
"twee-210619-twee-casc-extra-no-dup",
"twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm-kbo0",
"twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0"]
fixed_old = take 2 [
"twee-210619-twee-casc-extra-no-dup",
"twee-210621-twee-casc-extra-depth-60-kbo0",
"twee-210619-twee-casc-extra-lhs5-flip-aggrnorm",
"twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm-kbo0",
"twee-210621-twee-casc-extra-complete-subsets-flatten",
"twee-210619-twee-casc-extra-lhs9-flip-nogoal",
"twee-210619-twee-casc-extra-no-dup-nogoal"]
{- attempt 2:
fixed = take 0 [
"twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0",
"twee-210621-twee-casc-extra-depth-60-kbo0",
"twee-210619-twee-casc-extra-complete-subsets",
"twee-210621-twee-casc-extra-flatten-lhs9-kbo0",
"twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm",
"twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0"]
-}
{- attempt 1:
"twee-210621-twee-casc-extra-flatten-lhs9-kbo0",
"twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm",
"twee-210621-twee-casc-extra-depth-60-kbo0",
"twee-210619-twee-casc-extra-complete-subsets",
"twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",
"twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0"]
-}
banned :: [String]
banned = []