twee-2.7.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
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
[ (strip ".p" name, read rating)
| [name, rating] <- map words (lines input)]
where
input = $(embedStringFile "ratings")
strip suf str
| suf `isSuffixOf` str = take (length str - length suf) str
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 "results/*/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]
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 = []