diff --git a/executable/Main.hs b/executable/Main.hs --- a/executable/Main.hs +++ b/executable/Main.hs @@ -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 = diff --git a/jukebox.cabal b/jukebox.cabal --- a/jukebox.cabal +++ b/jukebox.cabal @@ -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: diff --git a/src/Jukebox/Name.hs b/src/Jukebox/Name.hs --- a/src/Jukebox/Name.hs +++ b/src/Jukebox/Name.hs @@ -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) diff --git a/src/Jukebox/SMTLIB.hs b/src/Jukebox/SMTLIB.hs --- a/src/Jukebox/SMTLIB.hs +++ b/src/Jukebox/SMTLIB.hs @@ -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 diff --git a/src/Jukebox/TPTP/Parse/Core.hs b/src/Jukebox/TPTP/Parse/Core.hs --- a/src/Jukebox/TPTP/Parse/Core.hs +++ b/src/Jukebox/TPTP/Parse/Core.hs @@ -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 diff --git a/src/Jukebox/TPTP/Print.hs b/src/Jukebox/TPTP/Print.hs --- a/src/Jukebox/TPTP/Print.hs +++ b/src/Jukebox/TPTP/Print.hs @@ -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 diff --git a/src/Jukebox/Tools/EncodeTypes.hs b/src/Jukebox/Tools/EncodeTypes.hs --- a/src/Jukebox/Tools/EncodeTypes.hs +++ b/src/Jukebox/Tools/EncodeTypes.hs @@ -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 diff --git a/src/Jukebox/Tools/HornToUnit.hs b/src/Jukebox/Tools/HornToUnit.hs --- a/src/Jukebox/Tools/HornToUnit.hs +++ b/src/Jukebox/Tools/HornToUnit.hs @@ -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, diff --git a/src/Jukebox/Tools/InferTypes.hs b/src/Jukebox/Tools/InferTypes.hs --- a/src/Jukebox/Tools/InferTypes.hs +++ b/src/Jukebox/Tools/InferTypes.hs @@ -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 ]