packages feed

jukebox 0.3.7 → 0.4

raw patch · 9 files changed

+127/−127 lines, 9 filesdep +semigroups

Dependencies added: semigroups

Files

executable/Main.hs view
@@ -49,7 +49,7 @@     pipeline :: OptionParser (IO ()) }  tools = external ++ internal-external = [fof, cnf, smt, monotonox, hornToUnit]+external = [fof, cnf, uncnf, smt, monotonox, hornToUnit, inferTypes] internal = [guessmodel, parse]  fof =@@ -80,6 +80,22 @@       (readProblemBox =>>=        clausifyBox =>>=        oneConjectureBox =>>=+       printClausesBox)++uncnf =+  Tool "uncnf" "Introduce explicit quantification into a problem" $+    forAllFilesBox <*>+      (readProblemBox =>>=+       printProblemBox)++inferTypes =+  Tool "infer-types" "Infer types" $+    forAllFilesBox <*>+      (readProblemBox =>>=+       clausifyBox =>>=+       oneConjectureBox =>>=+       inferBox =>>=+       printInferredBox =>>=        printClausesBox)  guessmodel =
jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.3.7+Version: 0.4 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone@@ -34,6 +34,8 @@ Library   Build-depends: base >= 4 && < 5, array, transformers >= 0.4.0.0, directory,     filepath, pretty >= 1.1.2.0, symbol, dlist, process, containers, uglymemo+  if !impl(ghc >= 8.0)+    Build-depends: semigroups   if flag(minisat)     Build-depends: minisat     Exposed-modules:
src/Jukebox/Name.hs view
@@ -13,8 +13,8 @@ #endif  data Name =-    Fixed !FixedName-  | Unique {-# UNPACK #-} !Int64 String Renamer+    Fixed !FixedName (Maybe String)+  | Unique {-# UNPACK #-} !Int64 String (Maybe String) Renamer   | Variant !Name ![Name] Renamer  data FixedName =@@ -31,10 +31,28 @@ base :: Named a => a -> String base x =   case name x of-    Fixed x -> show x-    Unique _ xs _ -> xs+    Fixed x _ -> show x+    Unique _ xs _ _ -> xs     Variant x _ _ -> base x +label :: Named a => a -> Maybe String+label x =+  case name x of+    Fixed _ x -> x+    Unique _ _ x _ -> x+    Variant x _ _ -> label x++hasLabel :: Named a => String -> a -> Bool+hasLabel l x = label x == Just l++withMaybeLabel :: Maybe String -> Name -> Name+withMaybeLabel l (Fixed x _) = Fixed x l+withMaybeLabel l (Unique x xs _ f) = Unique x xs l f+withMaybeLabel l (Variant x xs r) = Variant (withMaybeLabel l x) xs r++withLabel :: String -> Name -> Name+withLabel l x = withMaybeLabel (Just l) x+ instance Show FixedName where   show (Basic xs) = unintern xs   show (Overloaded xs _) = unintern xs@@ -45,8 +63,8 @@ renamer :: Named a => a -> Renamer renamer x =   case name x of-    Fixed _ -> defaultRenamer-    Unique _ _ f -> f+    Fixed _ _ -> defaultRenamer+    Unique _ _ _ f -> f     Variant _ _ f -> f  defaultRenamer :: Renamer@@ -58,8 +76,8 @@       | otherwise = ""  withRenamer :: Name -> Renamer -> Name-Fixed x `withRenamer` _ = Fixed x-Unique n xs _ `withRenamer` f = Unique n xs f+Fixed x l `withRenamer` _ = Fixed x l+Unique n xs l _ `withRenamer` f = Unique n xs l f Variant x xs _ `withRenamer` f = Variant x xs f  instance Eq Name where@@ -71,13 +89,21 @@ -- It's important that FixedNames come first so that they get added -- first to the used names list in Jukebox.TPTP.Print.prettyRename. compareName :: Name -> Either FixedName (Either Int64 (Name, [Name]))-compareName (Fixed xs) = Left xs-compareName (Unique n _ _) = Right (Left n)+compareName (Fixed xs _) = Left xs+compareName (Unique n _ _ _) = Right (Left n) compareName (Variant x xs _) = Right (Right (x, xs))  instance Show Name where-  show (Fixed x) = show x-  show (Unique n xs f) = ys ++ "@" ++ show n+  show (Fixed x ml) =+    show x +++    case ml of+      Nothing -> ""+      Just l -> "[" ++ l ++ "]"+  show (Unique n xs ml f) =+    ys ++ "@" ++ show n +++    case ml of+      Nothing -> ""+      Just l -> "[" ++ l ++ "]"     where       Renaming _ ys = f xs 0   show (Variant x xs _) =@@ -88,7 +114,7 @@   name :: a -> Name  instance Named [Char] where-  name = Fixed . Basic . intern+  name x = Fixed (Basic (intern x)) Nothing  instance Named Integer where   name n = name ("n" ++ show n)@@ -138,7 +164,7 @@  runNameM :: [Name] -> NameM a -> a runNameM xs m =-  evalState (unNameM m) (maximum (0:[ succ n | Unique n _ _ <- xs ]))+  evalState (unNameM m) (maximum (0:[ succ n | Unique n _ _ _ <- xs ]))  newName :: Named a => a -> NameM Name newName x = NameM $ do@@ -146,4 +172,4 @@   let idx' = idx+1   when (idx' < 0) $ error "Name.newName: too many names"   put $! idx'-  return $! Unique idx' (base x) (renamer x)+  return $! Unique idx' (base x) (label x) (renamer x)
src/Jukebox/SMTLIB.hs view
@@ -141,9 +141,9 @@     builtIn x =       (show (name x) /= "individual" && show (name x) `elem` map snd renamings) ||       case name x of-        Fixed Integer{} -> True-        Fixed Rational{} -> True-        Fixed Real{} -> True+        Fixed Integer{} _ -> True+        Fixed Rational{} _ -> True+        Fixed Real{} _ -> True         _ -> False      typeDecl O = empty@@ -158,10 +158,10 @@ sexp = parens . fsep  pPrintName :: Name -> Doc-pPrintName (Fixed (Integer n)) = pPrint n-pPrintName (Fixed (Rational n)) =+pPrintName (Fixed (Integer n) _) = pPrint n+pPrintName (Fixed (Rational n) _) =   sexp ["/", pPrint (numerator n), pPrint (denominator n)]-pPrintName (Fixed (Real n)) =+pPrintName (Fixed (Real n) _) =   sexp ["/", pPrint (numerator n), pPrint (denominator n)] pPrintName x = text . escape . show $ x   where
src/Jukebox/TPTP/Parse/Core.hs view
@@ -52,7 +52,7 @@     (Map.fromList [(show (name ty), ty) | ty <- [intType, ratType, realType]])     (Map.fromList        [ (fun,-          [Fixed (Overloaded (intern fun) (intern (show (name kind)))) ::: ty+          [Fixed (Overloaded (intern fun) (intern (show (name kind)))) Nothing ::: ty           | (kind, ty) <- tys ])        | (fun, tys) <- funs ])    where@@ -79,7 +79,7 @@ initialStateFrom :: Maybe String -> [Name] -> Map String Type -> Map String [Function] -> ParseState initialStateFrom mfile xs tys fs = MkState mfile [] tys fs Map.empty n   where-    n = maximum (0:[succ m | Unique m _ _ <- xs])+    n = maximum (0:[succ m | Unique m _ _ _ <- xs])  instance Stream TokenStream Token where   primToken (At _ (Cons Eof _)) _ok err _fatal = err@@ -436,7 +436,7 @@     case Map.lookup x ctx of       Just v -> return (Var v)       Nothing -> do-        let v = Unique (n+1) x defaultRenamer ::: indType+        let v = Unique (n+1) x Nothing defaultRenamer ::: indType         putState (MkState mfile p t f (Map.insert x v ctx) (n+1))         return (Var v)   var _ ctx = do@@ -489,7 +489,7 @@      {-# INLINE constant #-}     constant x ty =-      fromThing (Term ((Fixed x ::: FunType [] ty) :@: []))+      fromThing (Term ((Fixed x Nothing ::: FunType [] ty) :@: []))  literal, unitary, quantified, formula ::   FormulaLike a => Mode -> Map String Variable -> Parser a@@ -567,7 +567,7 @@              type_ } <|> return indType   MkState mfile p t f v n <- getState   putState (MkState mfile p t f v (n+1))-  return (Unique n x defaultRenamer ::: ty)+  return (Unique n x Nothing defaultRenamer ::: ty)  -- Parse a type type_ :: Parser Type
src/Jukebox/TPTP/Print.hs view
@@ -43,8 +43,8 @@   pPrintAnnotProof (evalState (concat <$> mapM annot prob) (1, Map.empty))   where     fun f [] = text f-    fun f xs = text f <> parens (fsep (punctuate comma xs))-    list = brackets . fsep . punctuate comma+    fun f xs = text f <> parens (hsep (punctuate comma xs))+    list = brackets . hsep . punctuate comma      clause n = "c" ++ show n @@ -170,7 +170,7 @@  pPrintClause :: String -> String -> String -> [Doc] -> Doc pPrintClause family name kind rest =-  text family <> parens (fsep (punctuate comma ([text (escapeAtom name), text kind] ++ rest))) <> text "."+  text family <> parens (hsep (punctuate comma ([text (escapeAtom name), text kind] ++ rest))) <> text "."  instance Pretty Clause where   pPrint (Clause (Bind _ ts)) =@@ -230,13 +230,13 @@     pPrint v   pPrint ((f ::: _) :@: []) =     case f of-      Fixed Integer{} -> text (show f)-      Fixed Rational{} -> text (show f)-      Fixed Real{} -> text (show f)+      Fixed Integer{} _ -> text (show f)+      Fixed Rational{} _ -> text (show f)+      Fixed Real{} _ -> text (show f)       _ -> text (escapeAtom (show f))   pPrint ((f ::: _) :@: ts) =     text (escapeAtom (show f)) <>-    parens (fsep (punctuate comma (map pPrint ts)))+    parens (hsep (punctuate comma (map pPrint ts)))  instance Show Term where   show = prettyShow@@ -286,15 +286,15 @@ pPrintConnective bind p _ident _op [x] = pPrintForm bind p x pPrintConnective bind p _ident op (x:xs) =   maybeParens (p > 0) $-    fsep (ppr x:[ nest 2 (text op <+> ppr x) | x <- xs ])+    hsep (ppr x:[ nest 2 (text op <+> ppr x) | x <- xs ])       where ppr = pPrintForm bind 1              pPrintQuant :: (Variable -> Doc) -> String -> Set.Set Variable -> Form -> Doc pPrintQuant bind q vs f   | Set.null vs = pPrintForm bind 1 f   | otherwise =-    fsep [-      text q <> brackets (fsep (punctuate comma (map bind (Set.toList vs)))) <> colon,+    hsep [+      text q <> brackets (hsep (punctuate comma (map bind (Set.toList vs)))) <> colon,       nest 2 (pPrintForm bind 1 f)]  instance Show Kind where@@ -337,15 +337,15 @@     add used names =       foldr add1 (Map.empty, used) names -    add1 (Fixed xs) (scope, used) =+    add1 (Fixed xs _) (scope, used) =       (scope, Set.insert (show xs) used)-    add1 x@(Unique _ base f) (scope, used) =+    add1 x@(Unique _ base _ f) (scope, used) =       addWith base f x (scope, used)     add1 x@(Variant y _ f) (scope, used) =       addWith (base y) f x (scope, used)      addWith base f x (scope, used) =-      (Map.insert x (name winner) scope,+      (Map.insert x (withMaybeLabel (label x) (name winner)) scope,        Set.insert winner (Set.fromList taken `Set.union` used))       where         cands = [f base n | n <- [0..]]@@ -359,6 +359,6 @@         [ ty | Type ty <- types x ]     (globalsScope, globalsUsed) = add fixed globals -    fixed = Set.fromList [ show xs | Fixed xs <- names x ]+    fixed = Set.fromList [ show xs | Fixed xs _ <- names x ]      x = run x0 uniqueNames
src/Jukebox/Tools/EncodeTypes.hs view
@@ -99,7 +99,7 @@ tags :: Bool -> Scheme tags moreAxioms = Scheme   { makeFunction = \ty ->-      newFunction ("to_" ++ base ty) [ty] ty,+      newFunction (withLabel "type_tag" (name ("to_" ++ base ty))) [ty] ty,     scheme1 = tags1 moreAxioms }  tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1@@ -147,7 +147,7 @@ guards :: Scheme guards = Scheme   { makeFunction = \ty ->-      newFunction ("is_" ++ base ty) [ty] O,+      newFunction (withLabel "type_pred" (name ("is_" ++ base ty))) [ty] O,     scheme1 = guards1 }  guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
src/Jukebox/Tools/HornToUnit.hs view
@@ -29,7 +29,6 @@ import Jukebox.Utils import qualified Jukebox.Sat as Sat import Data.List-import Data.Maybe import Control.Monad import qualified Data.Set as Set import qualified Data.Map.Strict as Map@@ -44,7 +43,6 @@     allowNonGroundConjectures :: Bool,     allowCompoundConjectures :: Bool,     dropNonHorn :: Bool,-    nonHornToOr :: Bool,     passivise :: Bool,     multi :: Bool,     smaller :: Bool,@@ -73,9 +71,6 @@     bool "drop-non-horn"       ["Silently drop non-Horn clauses from input problem (off by default)."]       False <*>-    bool "non-horn-to-or"-      ["Partially encode non-Horn clauses using 'or' (off by default)."]-      False <*>     bool "passivise"       ["Encode problem so as to get fewer critical pairs (off by default)."]       False <*>@@ -105,60 +100,14 @@       Left ans ->         Right (Left ans)       Right enc ->-        let-          (x, bool, true, false, or, equals) = run_ prob $ do-            x <- newName "X"-            bool <- newType "bool"-            true <- newFunction "true" [] bool-            false <- newFunction "false" [] bool-            or <- newFunction "or" [bool, bool] bool-            equals <- newName "equals"-            return (x, bool, true :@: [], false :@: [], \t u -> or :@: [t, u],-                    \t u -> (variant equals [typ t] ::: FunType [typ t, typ u] bool) :@: [t, u])-        in-          fmap (Right . enc) $-          eliminateHornClauses flags $-          eliminateUnsuitableConjectures flags $-          eliminateMultiplePreconditions flags $-          eliminatePredicates bool true $-          encodeNonHorn flags x bool equals true false or prob--encodeNonHorn :: HornFlags -> Name -> Type -> (Term -> Term -> Term) -> Term -> Term -> (Term -> Term -> Term) -> Problem Clause -> Problem Clause-encodeNonHorn flags xname bool equals true false or prob-  | not (nonHornToOr flags) = prob-  | otherwise =-    let (prob', axioms) = evalRWS (mapM encode prob) () () in-    map toInput axioms ++ prob'-  where-    toInput ls =-      Input "non_horn_axiom" (Ax Axiom) Unknown (clause ls)-    encode inp =-      case partition pos (toLiterals (what inp)) of-        ([], _) -> return inp-        ([_], _) -> return inp-        (ps, ns) -> do-          let-            toTerm (Tru p) = p-            toTerm (t :=: u) = equals t u-            p = foldr1 or (map (toTerm . the) ps)-            x ty = Var (variant xname [0 :: Int] ::: ty)-            y ty = Var (variant xname [1 :: Int] ::: ty)-            z ty = Var (variant xname [2 :: Int] ::: ty)-          tell [[Pos $ or (x bool) (y bool) :=: or (y bool) (x bool)],-                [Pos $ or (x bool) (or (y bool) (z bool)) :=: or (or (x bool) (y bool)) (z bool)],-                [Pos $ or false (x bool) :=: x bool],-                [Pos $ or true (x bool) :=: true]]-          forM_ ps $ \l ->-            case l of-              Pos (t :=: _) ->-                let ty = typ t in-                tell [[Pos $ Tru $ equals (x ty) (x ty)],-                      [Neg $ Tru $ equals (x ty) (y ty), Pos $ x ty :=: y ty]]-              _ -> return ()-          return inp { what = clause (Pos (Tru p):ns) }+        fmap (Right . enc) $+        eliminateHornClauses flags $+        eliminateUnsuitableConjectures flags $+        eliminateMultiplePreconditions flags $+        eliminatePredicates prob -eliminatePredicates :: Type -> Term -> Problem Clause -> Problem Clause-eliminatePredicates bool true prob =+eliminatePredicates :: Problem Clause -> Problem Clause+eliminatePredicates prob =   map (fmap elim) prob   where     elim = clause . map (fmap elim1) . toLiterals@@ -166,6 +115,11 @@     elim1 (Tru ((p ::: FunType tys _) :@: ts)) =       ((p ::: FunType tys bool) :@: ts) :=: true +    (bool, true) = run_ prob $ do+      bool <- newType (withLabel "bool" (name "bool"))+      true <- newFunction (withLabel "true" (name "true")) [] bool+      return (bool, true :@: [])+ eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause eliminateMultiplePreconditions flags prob   | otherwise =@@ -183,8 +137,8 @@       elim inp = inp        tuple = run_ prob $ do-        tupleType <- newName "tuple"-        tuple <- newName "tuple"+        tupleType <- newName (withLabel "tuple" (name "tuple"))+        tuple <- newName (withLabel "tuple" (name "tuple"))         return $ \args ->           variant tuple args :::           FunType args (Type (variant tupleType args))@@ -212,9 +166,9 @@     addConjecture c = clause (Pos (a :=: b):toLiterals c)      (a, b) = run_ prob $ do-      token <- newType "token"-      a <- newFunction "a" [] token-      b <- newFunction "b" [] token+      token <- newType (withLabel "token" (name "token"))+      a <- newFunction (withLabel "token_a" (name "a")) [] token+      b <- newFunction (withLabel "token_b" (name "b")) [] token       return (a :@: [], b :@: [])  eliminateHornClauses :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause)@@ -235,12 +189,12 @@     passive ((f ::: ty) :@: ts) =       (variant f [passiveName] ::: ty) :@: map passive ts -    elim1 :: Input Clause -> RWST () [Atomic] Int (Either (Input Clause)) [Input Clause]+    elim1 :: Input Clause -> RWST () [(String, Atomic)] Int (Either (Input Clause)) [Input Clause]     elim1 c =       case partition pos (toLiterals (what c)) of         ([], _) -> return [c]         ([Pos l], ls) -> runListT $ do-          l <- foldM encode l ls+          l <- foldM (encode (tag c)) l ls           return c { what = clause [Pos l] }         _ ->           if dropNonHorn flags then@@ -248,8 +202,8 @@           else             lift $ Left c -    encode :: Atomic -> Literal -> ListT (RWST () [Atomic] Int (Either (Input Clause))) Atomic-    encode (c :=: d) (Neg (a :=: b)) =+    encode :: String -> Atomic -> Literal -> ListT (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic+    encode tag (c :=: d) (Neg (a :=: b)) =       let         ty1 = typ a         ty2 = typ c@@ -262,11 +216,11 @@         Symmetric -> do           ifeq <- passiveFresh (variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2] ty2)           if passivise flags then do-            axiom (ifeq :@: [x, x, passive c] :=: c)-            axiom (ifeq :@: [x, x, passive d] :=: d)+            axiom (tag, ifeq :@: [x, x, passive c] :=: c)+            axiom (tag, ifeq :@: [x, x, passive d] :=: d)             return (ifeq :@: [a, b, passive c] :=: ifeq :@: [a, b, passive d])            else do-            axiom (ifeq :@: [x, x, y] :=: y)+            axiom ("ifeq_axiom", ifeq :@: [x, x, y] :=: y)             return (ifeq :@: [a, b, c] :=: ifeq :@: [a, b, d])         -- ifeq(x, x, y, z) = y         -- ifeq(a, b, c, d) = d@@ -274,16 +228,16 @@           ifeq <- passiveFresh (variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2, ty2] ty2)           (c :=: d) <- return (swap size (c :=: d))           if passivise flags then do-            axiom (ifeq :@: [x, x, passive c, y] :=: c)+            axiom ("ifeq_axiom", ifeq :@: [x, x, passive c, y] :=: c)             return (ifeq :@: [a, b, passive c, passive d] :=: d)            else do-            axiom (ifeq :@: [x, x, y, z] :=: y)+            axiom ("ifeq_axiom", ifeq :@: [x, x, y, z] :=: y)             return (ifeq :@: [a, b, c, d] :=: d)         -- f(a, sigma) = c         -- f(b, sigma) = d         -- where sigma = FV(a, b, c, d)         Asymmetric2 -> do-          ifeqName <- fresh ifeqName+          ifeqName <- fresh freshName           (a :=: b) <- return (swap size (a :=: b))           (c :=: d) <- return (swap size (c :=: d))           let@@ -295,16 +249,16 @@             ifeq = ifeqName ::: FunType (ty1:map typ vs) ty2             app t = ifeq :@: (t:vs)           if smaller flags then do-            axiom (app b :=: d)+            axiom (tag, app b :=: d)             return (app a :=: c)            else do-            axiom (app a :=: c)+            axiom (tag, app a :=: c)             return (app b :=: d)         -- f(a, b, sigma) = c         -- f(x, x, sigma) = d         -- where sigma = FV(c, d)         Asymmetric3 -> do-          ifeqName <- fresh ifeqName+          ifeqName <- fresh freshName           (c :=: d) <- return (swap size (c :=: d))           let             vs =@@ -315,7 +269,7 @@             ifeq = ifeqName ::: FunType (ty1:ty1:map typ vs) ty2             app t u = ifeq :@: (t:u:vs)             x = Var (xvar ::: ty1)-          axiom (app x x :=: c)+          axiom (tag, app x x :=: c)           return (app a b :=: d)      swap f (t :=: u) =@@ -324,20 +278,21 @@      axiom l = lift $ tell [l] -    toInput l =+    toInput (tag, l) =       Input {-        tag = "ifeq_axiom",+        tag = tag,         kind = Ax Axiom,         source = Unknown,         what = clause [Pos l] } -    (ifeqName, passiveName, xvar, yvar, zvar) = run_ prob $ do-      ifeqName <- newName "ifeq"-      passiveName <- newName "passive"+    (ifeqName, freshName, passiveName, xvar, yvar, zvar) = run_ prob $ do+      ifeqName <- newName (withLabel "ifeq" (name "ifeq"))+      freshName <- newName (withLabel "fresh" (name "fresh"))+      passiveName <- newName (withLabel "passive" (name "passive"))       xvar <- newName "A"       yvar <- newName "B"       zvar <- newName "C"-      return (ifeqName, passiveName, xvar, yvar, zvar)+      return (ifeqName, freshName, passiveName, xvar, yvar, zvar)  -- Soundly encode types, but try to erase them if possible. -- Based on the observation that if the input problem is untyped,
src/Jukebox/Tools/InferTypes.hs view
@@ -30,6 +30,7 @@       | v <- vars prob ]      let tyMap = Map.fromList $+              [(name O, O)] ++               concat [ res:args | (args, res) <- Map.elems funMap ] ++               [ ty | ty <- Map.elems varMap ]