jukebox 0.2.1 → 0.2.2

raw patch · 3 files changed

+8/−4 lines, 3 files

Files

jukebox.cabal +1/−1
src/Jukebox/TPTP/Parse/Core.hs +3/−1
src/Jukebox/Toolbox.hs +4/−2

jukebox.cabal view

@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.2.1+Version: 0.2.2 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone

src/Jukebox/TPTP/Parse/Core.hs view

@@ -306,7 +306,9 @@ cnf = do   MkState p t f _ n <- getState   putState (MkState p t f Map.empty n)-  formula NoQuantification __+  form <- formula NoQuantification __+  MkState _ _ _ vs _ <- getState+  return (ForAll (Bind (Set.fromList (Map.elems vs)) form)) tff = formula Typed Map.empty fof = formula Untyped Map.empty

src/Jukebox/Toolbox.hs view

@@ -89,9 +89,11 @@  toFofIO :: GlobalFlags -> (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form) toFofIO globals clausify scheme f = do-  cs <- clausify f >>= oneConjecture+  CNF{..} <- clausify f   unless (quiet globals) $ hPutStrLn stderr "Monotonicity analysis..."-  m <- monotone (map what cs)+  -- In some cases we might get better results by considering each+  -- problem (axioms + conjecture) separately, but no big deal.+  m <- monotone (map what (axioms ++ concat conjectures))   let isMonotone ty =         case Map.lookup ty m of           Just Nothing -> False