diff --git a/dist/build/Jukebox/TPTP/Lexer.hs b/dist/build/Jukebox/TPTP/Lexer.hs --- a/dist/build/Jukebox/TPTP/Lexer.hs +++ b/dist/build/Jukebox/TPTP/Lexer.hs @@ -74,7 +74,7 @@ show x = case x of { Normal -> "normal"; - Thf -> "thf"; Tff -> "tff"; Fof -> "fof"; Cnf -> "cnf"; + Thf -> "thf"; Tff -> "tff"; Fof -> "fof"; Tcf -> "tcf"; Cnf -> "cnf"; Axiom -> "axiom"; Hypothesis -> "hypothesis"; Definition -> "definition"; Assumption -> "assumption"; Lemma -> "lemma"; Theorem -> "theorem"; Conjecture -> "conjecture"; NegatedConjecture -> "negated_conjecture"; diff --git a/executable/Main.hs b/executable/Main.hs --- a/executable/Main.hs +++ b/executable/Main.hs @@ -4,6 +4,7 @@ import Control.Monad import Jukebox.Options import Jukebox.Toolbox +import Jukebox.Form #if __GLASGOW_HASKELL__ < 710 import Control.Applicative import Data.Monoid @@ -47,8 +48,9 @@ description :: String, pipeline :: OptionParser (IO ()) } -tools = [fof, cnf, smt, monotonox, guessmodel, hornToUnit] -internal = [guessmodel] +tools = external ++ internal +external = [fof, cnf, smt, monotonox, hornToUnit] +internal = [guessmodel, parse] fof = Tool "fof" "Translate a problem from TFF (typed) to FOF (untyped)" $ @@ -94,4 +96,15 @@ clausifyBox =>>= oneConjectureBox =>>= hornToUnitBox =>>= - printClausesBox) + (printAnswerOr <$> printClausesBox)) + where + printAnswerOr _ (Left answer) = do + mapM_ putStrLn (answerSZS answer) + printAnswerOr printClauses (Right clauses) = + printClauses clauses + +parse = + Tool "parse" "Parse the problem and exit (internal use)" $ + forAllFilesBox <*> + (readProblemBox =>>= + pure (const (return ()))) diff --git a/gcc-static-libstdc++ b/gcc-static-libstdc++ new file mode 100644 --- /dev/null +++ b/gcc-static-libstdc++ @@ -0,0 +1,24 @@ +#!/bin/zsh +typeset -a args + +process() { + for arg in $*; do + case $arg in + \"*\") + process $(echo $arg | cut -c2- | rev | cut -c2- | rev) + ;; + @*) + process $(cat $(echo $arg | cut -c2-)) + ;; + -lstdc++ | -fuse-ld=gold) + ;; + *) + args+=$arg + ;; + esac + done +} + +process $* + +exec g++ -static-libgcc -static-libstdc++ $args diff --git a/jukebox.cabal b/jukebox.cabal --- a/jukebox.cabal +++ b/jukebox.cabal @@ -1,5 +1,5 @@ Name: jukebox -Version: 0.3 +Version: 0.3.1 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone @@ -17,12 +17,16 @@ encoding types) and clausify problems (both typed and untyped). License: BSD3 License-file: LICENSE -extra-source-files: src/errors.h +extra-source-files: src/errors.h gcc-static-libstdc++ flag minisat Description: Use minisat. Required for monotonicity inference. Default: True +flag static-cxx + description: Build a binary which statically links against libstdc++. + default: False + source-repository head type: git location: https://github.com/nick8325/jukebox @@ -72,3 +76,6 @@ Main-is: executable/Main.hs Build-depends: base >= 4 && < 5, jukebox ghc-options: -W -fno-warn-incomplete-patterns + + if flag(static-cxx) + ghc-options: -pgml ./gcc-static-libstdc++ diff --git a/src/Jukebox/ExternalProvers/E.hs b/src/Jukebox/ExternalProvers/E.hs --- a/src/Jukebox/ExternalProvers/E.hs +++ b/src/Jukebox/ExternalProvers/E.hs @@ -1,7 +1,7 @@ {-# LANGUAGE GADTs #-} module Jukebox.ExternalProvers.E where -import Jukebox.Form hiding (tag, Or) +import Jukebox.Form hiding (tag, Or, run_) import Jukebox.Name import Jukebox.Options import Control.Applicative hiding (Const) @@ -66,10 +66,10 @@ funMap = Map.fromList [(show (name x), x) | x <- functions prob] result = lines str status = head $ - [Sat Satisfiable | "# SZS status Satisfiable" <- result] ++ - [Sat CounterSatisfiable | "# SZS status CounterSatisfiable" <- result] ++ - [Unsat Unsatisfiable | "# SZS status Unsatisfiable" <- result] ++ - [Unsat Theorem | "# SZS status Theorem" <- result] ++ + [Sat Satisfiable Nothing | "# SZS status Satisfiable" <- result] ++ + [Sat CounterSatisfiable Nothing | "# SZS status CounterSatisfiable" <- result] ++ + [Unsat Unsatisfiable Nothing | "# SZS status Unsatisfiable" <- result] ++ + [Unsat Theorem Nothing | "# SZS status Theorem" <- result] ++ [NoAnswer Timeout | "# SZS status ResourceOut" <- result] ++ [NoAnswer Timeout | "# SZS status Timeout" <- result] ++ [NoAnswer Timeout | "# SZS status MemyOut" <- result] ++ diff --git a/src/Jukebox/ExternalProvers/SPASS.hs b/src/Jukebox/ExternalProvers/SPASS.hs --- a/src/Jukebox/ExternalProvers/SPASS.hs +++ b/src/Jukebox/ExternalProvers/SPASS.hs @@ -46,6 +46,6 @@ extractAnswer :: String -> Answer extractAnswer result = head $ - [ Unsat Unsatisfiable | "SPASS beiseite: Proof found." <- lines result ] ++ - [ Sat Satisfiable | "SPASS beiseite: Completion found." <- lines result ] ++ + [ Unsat Unsatisfiable Nothing | "SPASS beiseite: Proof found." <- lines result ] ++ + [ Sat Satisfiable Nothing | "SPASS beiseite: Completion found." <- lines result ] ++ [ NoAnswer Timeout ] diff --git a/src/Jukebox/Form.hs b/src/Jukebox/Form.hs --- a/src/Jukebox/Form.hs +++ b/src/Jukebox/Form.hs @@ -270,13 +270,13 @@ CNF { axioms :: [Input Clause], conjectures :: [[Input Clause]], - satisfiable :: Answer, - unsatisfiable :: Answer } + satisfiable :: Maybe Model -> Answer, + unsatisfiable :: Maybe CNFRefutation -> Answer } toCNF :: [Input Clause] -> [[Input Clause]] -> CNF toCNF axioms [] = CNF axioms [[]] (Sat Satisfiable) (Unsat Unsatisfiable) toCNF axioms [conjecture] = CNF axioms [conjecture] (Sat CounterSatisfiable) (Unsat Theorem) -toCNF axioms conjectures = CNF axioms conjectures (NoAnswer GaveUp) (Unsat Theorem) +toCNF axioms conjectures = CNF axioms conjectures (\_ -> NoAnswer GaveUp) (Unsat Theorem) newtype Clause = Clause (Bind [Literal]) @@ -311,26 +311,48 @@ NegatedConjecture deriving (Eq, Ord) data ConjKind = Conjecture | Question deriving (Eq, Ord) -data Answer = Sat SatReason | Unsat UnsatReason | NoAnswer NoAnswerReason +data Answer = Sat SatReason (Maybe Model) | Unsat UnsatReason (Maybe CNFRefutation) | NoAnswer NoAnswerReason deriving (Eq, Ord) data NoAnswerReason = GaveUp | Timeout deriving (Eq, Ord, Show) data SatReason = Satisfiable | CounterSatisfiable deriving (Eq, Ord, Show) data UnsatReason = Unsatisfiable | Theorem deriving (Eq, Ord, Show) +type Model = [String] +type CNFRefutation = [String] instance Show Answer where - show (Sat reason) = show reason - show (Unsat reason) = show reason + show (Sat reason _) = show reason + show (Unsat reason _) = show reason show (NoAnswer x) = show x explainAnswer :: Answer -> String -explainAnswer (Sat Satisfiable) = "the axioms are consistent" -explainAnswer (Sat CounterSatisfiable) = "the conjecture is false" -explainAnswer (Unsat Unsatisfiable) = "the axioms are contradictory" -explainAnswer (Unsat Theorem) = "the conjecture is true" +explainAnswer (Sat Satisfiable _) = "the axioms are consistent" +explainAnswer (Sat CounterSatisfiable _) = "the conjecture is false" +explainAnswer (Unsat Unsatisfiable _) = "the axioms are contradictory" +explainAnswer (Unsat Theorem _) = "the conjecture is true" explainAnswer (NoAnswer GaveUp) = "couldn't solve the problem" explainAnswer (NoAnswer Timeout) = "ran out of time while solving the problem" +answerSZS :: Answer -> [String] +answerSZS answer = + ["% SZS status " ++ show answer] ++ + case answerJustification answer of + Nothing -> [] + Just strs -> [""] ++ strs + +answerJustification :: Answer -> Maybe [String] +answerJustification (Sat _ (Just model)) = + Just $ + ["% SZS output start Model"] ++ + model ++ + ["% SZS output end Model"] +answerJustification (Unsat _ (Just refutation)) = + Just $ + ["% SZS output start CNFRefutation"] ++ + refutation ++ + ["% SZS output end CNFRefutation"] +answerJustification _ = Nothing + data Input a = Input { tag :: Tag, kind :: Kind, @@ -537,7 +559,7 @@ names :: Symbolic a => a -> [Name] names = usort . termsAndBinders term bind where - term t = return (name t) `mappend` return (name (typ t)) + term t = DList.fromList (allNames t) `mappend` DList.fromList (allNames (typ t)) bind :: Symbolic a => Bind a -> [Name] bind (Bind vs _) = map name (Set.toList vs) @@ -545,6 +567,9 @@ run :: Symbolic a => a -> (a -> NameM b) -> b run x f = runNameM (names x) (f x) +run_ :: Symbolic a => a -> NameM b -> b +run_ x mx = run x (const mx) + types :: Symbolic a => a -> [Type] types = usort . termsAndBinders term bind where term t = return (typ t) @@ -585,8 +610,21 @@ f == g = Sum 1 | otherwise = mempty +funsOcc :: Symbolic a => a -> Map Function Int +funsOcc = + Map.fromList . map f . group . sort . termsAndBinders term mempty + where + term (f :@: _) = return f + term _ = mempty + + f xs@(x:_) = (x, length xs) + isFof :: Symbolic a => a -> Bool isFof f = length (types' f) <= 1 + +eraseTypes :: Symbolic a => a -> a +eraseTypes x = + mapType (\ty -> if ty == O then ty else indType) x uniqueNames :: Symbolic a => a -> NameM a uniqueNames t = evalStateT (aux Map.empty t) (Map.fromList [(x, t) | x ::: t <- Set.toList (free t)]) diff --git a/src/Jukebox/Name.hs b/src/Jukebox/Name.hs --- a/src/Jukebox/Name.hs +++ b/src/Jukebox/Name.hs @@ -90,8 +90,25 @@ instance Named [Char] where name = Fixed . Basic . intern +instance Named Integer where + name n = name ("n" ++ show n) + +instance Named Int where + name = name . toInteger + instance Named Name where name = id + +-- Get all names, including those only used as part of a variant. +allNames :: Named a => a -> [Name] +allNames x = gather [name x] [] + where + gather [] xs = xs + gather (x:xs) ys = + sub x (x:gather xs ys) + sub (Variant x xs _) ys = + gather (x:xs) ys + sub _ ys = ys variant :: (Named a, Named b) => a -> [b] -> Name variant x xs = diff --git a/src/Jukebox/Options.hs b/src/Jukebox/Options.hs --- a/src/Jukebox/Options.hs +++ b/src/Jukebox/Options.hs @@ -100,15 +100,13 @@ nums (n:"..":m:",":ns) = ([read n .. read m] ++) `fmap` nums ns nums _ = Nothing -argOption :: [String] -> ArgParser String -argOption as = arg ("<" ++ concat (intersperse " | " as) ++ ">") "expected an argument" elts - where - elts x | x `elem` as = Just x - | otherwise = Nothing +argOption :: [(String, a)] -> ArgParser a +argOption as = + argOptionWith "one" "or" "" (map fst as) (`lookup` as) argList :: [String] -> ArgParser [String] -argList as = arg ("<" ++ concat (intersperse " | " as) ++ ">*") "expected an argument" $ \x -> - elts $ x ++ "," +argList as = + argOptionWith "several" "and" "*" as $ \x -> elts (x ++ ",") where elts [] = Just [] elts s | w `elem` as = (w:) `fmap` elts r @@ -117,6 +115,17 @@ r = tail (dropWhile (/= ',') s) elts _ = Nothing + +argOptionWith :: String -> String -> String -> [String] -> (String -> Maybe a) -> ArgParser a +argOptionWith one or suff opts p = + arg ("<" ++ intercalate " | " opts ++ ">" ++ suff) + ("expected " ++ one ++ " of " ++ list) p + where + list = + case opts of + [] -> "" -- ?? + _ -> + intercalate ", " (init opts) ++ " " ++ or ++ " " ++ last opts -- A parser that always fails but produces an error message (useful for --help etc.) argUsage :: ExitCode -> [String] -> ArgParser a diff --git a/src/Jukebox/SMTLIB.hs b/src/Jukebox/SMTLIB.hs --- a/src/Jukebox/SMTLIB.hs +++ b/src/Jukebox/SMTLIB.hs @@ -86,7 +86,7 @@ , "select" , "subset", "union", "intersect" -- CVC4: - , "concat", "member" + , "concat", "member", "singleton" ] ++ map snd renamings renamings :: [(String, String)] @@ -192,7 +192,9 @@ pPrintForm (Literal (Pos l)) = pPrintAtomic l pPrintForm (Literal (Neg l)) = sexp ["not", pPrintAtomic l] pPrintForm (Not f) = sexp ["not", pPrintForm f] +pPrintForm (And []) = text "true" pPrintForm (And ts) = sexp ("and":map pPrintForm ts) +pPrintForm (Or []) = text "false" pPrintForm (Or ts) = sexp ("or":map pPrintForm ts) pPrintForm (Equiv t u) = sexp ["=", pPrintForm t, pPrintForm u] pPrintForm (Connective Implies t u) = sexp ["=>", pPrintForm t, pPrintForm u] diff --git a/src/Jukebox/TPTP/Lexer.x b/src/Jukebox/TPTP/Lexer.x --- a/src/Jukebox/TPTP/Lexer.x +++ b/src/Jukebox/TPTP/Lexer.x @@ -119,7 +119,7 @@ show x = case x of { Normal -> "normal"; - Thf -> "thf"; Tff -> "tff"; Fof -> "fof"; Cnf -> "cnf"; + Thf -> "thf"; Tff -> "tff"; Fof -> "fof"; Tcf -> "tcf"; Cnf -> "cnf"; Axiom -> "axiom"; Hypothesis -> "hypothesis"; Definition -> "definition"; Assumption -> "assumption"; Lemma -> "lemma"; Theorem -> "theorem"; Conjecture -> "conjecture"; NegatedConjecture -> "negated_conjecture"; diff --git a/src/Jukebox/TPTP/ParseSnippet.hs b/src/Jukebox/TPTP/ParseSnippet.hs --- a/src/Jukebox/TPTP/ParseSnippet.hs +++ b/src/Jukebox/TPTP/ParseSnippet.hs @@ -7,7 +7,7 @@ import Jukebox.TPTP.Parsec as TPTP.Parsec import Jukebox.TPTP.Lexer import Jukebox.Name -import Jukebox.Form +import Jukebox.Form hiding (run_) import qualified Data.Map.Strict as Map import Data.List #if __GLASGOW_HASKELL__ < 710 diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs --- a/src/Jukebox/Toolbox.hs +++ b/src/Jukebox/Toolbox.hs @@ -205,10 +205,11 @@ forAllConjectures :: TSTPFlags -> Solver -> CNF -> IO () forAllConjectures (TSTPFlags tstp) solve CNF{..} = do todo <- newIORef (return ()) - loop 1 todo conjectures - where loop _ todo [] = - result todo unsatisfiable - loop i todo (c:cs) = do + loop 1 todo conjectures Nothing + -- XXX fix this to properly combine refutations from parts + where loop _ todo [] mref = + result todo (unsatisfiable mref) + loop i todo (c:cs) _ = do when multi $ do join (readIORef todo) writeIORef todo (return ()) @@ -217,14 +218,14 @@ putStrLn $ "Partial result (" ++ part i ++ "): " ++ show answer putStrLn "" case answer of - Sat _ -> result todo satisfiable - Unsat _ -> loop (i+1) todo cs + Sat _ mmodel -> result todo (satisfiable mmodel) + Unsat _ mref -> loop (i+1) todo cs mref NoAnswer x -> result todo (NoAnswer x) multi = length conjectures > 1 part i = show i ++ "/" ++ show (length conjectures) result todo x = do when tstp $ do - putStrLn ("% SZS status " ++ show x) + mapM_ putStrLn (answerSZS x) putStrLn "" join (readIORef todo) putStrLn ("RESULT: " ++ show x ++ " (" ++ explainAnswer x ++ ").") @@ -251,14 +252,13 @@ schemeBox :: OptionParser Scheme schemeBox = inGroup "Options for encoding types" $ - choose <$> flag "encoding" ["Which type encoding to use (guards by default)."] - "guards" - (argOption ["guards", "tags"]) + (const guards) + (argOption + [("guards", const guards), + ("tags", tags)]) <*> tagsFlags - where choose "guards" _flags = guards - choose "tags" flags = tags flags ---------------------------------------------------------------------- -- Analyse monotonicity. @@ -290,13 +290,10 @@ inGroup "Options for the model guesser:" $ (\expansive univ prob -> return (guessModel expansive univ prob)) <$> expansive <*> universe - where universe = choose <$> - flag "universe" + where universe = flag "universe" ["Which universe to find the model in (peano by default)."] - "peano" - (argOption ["peano", "trees"]) - choose "peano" = Peano - choose "trees" = Trees + Peano + (argOption [("peano", Peano), ("trees", Trees)]) expansive = manyFlags "expansive" ["Allow a function to construct 'new' terms in its base case."] (arg "" "expected a function name" Just) @@ -316,12 +313,13 @@ ---------------------------------------------------------------------- -- Translate Horn problems to unit equality. -hornToUnitBox :: OptionParser (Problem Clause -> IO (Problem Clause)) +hornToUnitBox :: OptionParser (Problem Clause -> IO (Either Answer (Problem Clause))) hornToUnitBox = hornToUnitIO <$> hornFlags -hornToUnitIO :: HornFlags -> Problem Clause -> IO (Problem Clause) -hornToUnitIO flags prob = - case hornToUnit flags prob of +hornToUnitIO :: HornFlags -> Problem Clause -> IO (Either Answer (Problem Clause)) +hornToUnitIO flags prob = do + res <- hornToUnit flags prob + case res of Left clause -> do mapM_ (hPutStrLn stderr) [ "Expected a Horn problem, but the input file contained", 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 @@ -27,17 +27,30 @@ import Jukebox.Name import Jukebox.Options 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 +import Control.Monad.Trans.RWS +import Control.Monad.Trans.List +import Control.Monad.Trans.Class data HornFlags = HornFlags { allowNonUnitConjectures :: Bool, allowNonGroundConjectures :: Bool, - asymmetricEncoding :: Bool } + allowCompoundConjectures :: Bool, + dropNonHorn :: Bool, + passivise :: Bool, + multi :: Bool, + extra :: Bool, + encoding :: Encoding } deriving Show +data Encoding = Symmetric | Asymmetric1 | Asymmetric2 | Asymmetric3 + deriving (Eq, Show) + hornFlags :: OptionParser HornFlags hornFlags = inGroup "Horn clause encoding options" $ @@ -46,18 +59,78 @@ ["Allow conjectures to be non-unit clauses (off by default)."] False <*> bool "non-ground-conjectures" - ["Allow conjectures to be non-ground clauses (off by default)."] + ["Allow conjectures to be non-ground clauses (on by default)."] + True <*> + bool "compound-conjectures" + ["Allow conjectures to be compound terms (on by default)."] + True <*> + bool "drop-non-horn" + ["Silently drop non-Horn clauses from input problem (off by default)."] False <*> - bool "asymmetric-encoding" - ["Use an alternative, asymmetric encoding (off by default)."] - False + bool "passivise" + ["Encode problem so as to get fewer critical pairs (off by default)."] + False <*> + bool "multi" + ["Encode multiple left-hand sides at once (off by default)."] + False <*> + bool "extra" + ["Encode Horn axioms (off by default)."] + False <*> + encoding + where + encoding = + flag "conditional-encoding" + ["Which method to use to encode conditionals (asymmetric1 by default)."] + Asymmetric1 + (argOption + [("symmetric", Symmetric), + ("asymmetric1", Asymmetric1), + ("asymmetric2", Asymmetric2), + ("asymmetric3", Asymmetric3)]) -hornToUnit :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause) -hornToUnit flags prob = - eliminateHornClauses $ - eliminateUnsuitableConjectures flags $ - eliminatePredicates prob +hornToUnit :: HornFlags -> Problem Clause -> IO (Either (Input Clause) (Either Answer (Problem Clause))) +hornToUnit flags prob = do + res <- encodeTypesSmartly prob + return $ + case res of + Left ans -> + Right (Left ans) + Right enc -> + fmap (Right . enc) $ + eliminateHornClauses flags $ + eliminateUnsuitableConjectures flags $ + eliminatePredicates $ + if passivise flags then passiviseClauses prob else prob +passiviseClauses :: Problem Clause -> Problem Clause +passiviseClauses prob = + [ c { what = clause ls' } + | (n, c@Input{what = Clause (Bind _ ls)}) <- zip [0..] prob, + ls' <- cls n ls ] + where + cls n ls = + case partition pos ls of + (ps, ns) | length ns >= 1 -> + let + ns' = zipWith (toPred ls n) [0..] ns + in + [(map Neg ns' ++ ps)] ++ + [[n, Pos n'] | (n, n') <- zip ns ns'] + _ -> + [ls] + + toPred :: [Literal] -> Int -> Int -> Literal -> Atomic + toPred ls m n l = + Tru (p :@: map Var vs) + where + p = + variant "$p" [fresh, name m, name n] + ::: FunType (map typ vs) O + vs = intersect (vars (delete l ls)) (vars l) + + fresh = run_ prob $ + newName "fresh" + eliminatePredicates :: Problem Clause -> Problem Clause eliminatePredicates prob = map (fmap elim) prob @@ -67,7 +140,7 @@ elim1 (Tru ((p ::: FunType tys _) :@: ts)) = ((p ::: FunType tys bool) :@: ts) :=: true - (bool, true) = run prob $ \_ -> do + (bool, true) = run_ prob $ do bool <- newType "bool" true <- newFunction "true" [] bool return (bool, true :@: []) @@ -84,65 +157,165 @@ unsuitable c = all (not . pos) ls && - ((not (allowNonUnitConjectures flags) && length ls /= 1) || + ((not (allowCompoundConjectures flags) && or [size t > 1 | t <- terms ls]) || + (not (allowNonUnitConjectures flags) && length ls /= 1) || (not (allowNonGroundConjectures flags) && not (ground ls))) where ls = toLiterals (what c) addConjecture c = clause (Pos (a :=: b):toLiterals c) - (a, b) = run prob $ \_ -> do + (a, b) = run_ prob $ do token <- newType "token" a <- newFunction "a" [] token b <- newFunction "b" [] token return (a :@: [], b :@: []) -eliminateHornClauses :: Problem Clause -> Either (Input Clause) (Problem Clause) -eliminateHornClauses prob = do - prob <- mapM elim1 prob - return (prob ++ map axiom (usort (filter isIfeq (functions prob)))) +eliminateHornClauses :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause) +eliminateHornClauses flags prob = do + (prob, funs) <- evalRWST (mapM elim1 prob) () 0 + return (map toInput (usort funs) ++ concat prob) where + fresh base = lift $ do + n <- get + put $! n+1 + return (variant base [name (show n)]) + + elim1 :: Input Clause -> RWST () [Atomic] Int (Either (Input Clause)) [Input Clause] elim1 c = case partition pos (toLiterals (what c)) of - ([], _) -> Right c - ([l], ls) -> - Right c { what = clause [Pos (encode ls l)] } - _ -> Left c + ([], _) -> return [c] + ([Pos l], ls) + | encoding flags == Asymmetric2 && multi flags -> runListT $ do + l <- encodeAsymm2 l ls + return c { what = clause [Pos l] } + ([Pos l], ls) -> runListT $ do + l <- foldM encode l ls + return c { what = clause [Pos l] } + _ -> + if dropNonHorn flags then + return [] + else + lift $ Left c - encode [] (Pos l) = l - encode (Neg (t :=: u):ls) l = - if size v < size w then - ifeq ty1 ty2 :@: [t, u, w, v] :=: v - else - ifeq ty1 ty2 :@: [t, u, v, w] :=: w - where - v :=: w = encode ls l - ty1 = typ t - ty2 = typ v - - axiom (ifeq@(_ ::: FunType [ty1, _, ty2, _] _)) = - Input { - tag = "ifeq_axiom", - kind = Ax Axiom, - source = Unknown, - what = clause [Pos (ifeq :@: [x, x, y, z] :=: y)] } - where + encodeAsymm2 :: Atomic -> [Literal] -> ListT (RWST () [Atomic] Int (Either (Input Clause))) Atomic + encodeAsymm2 l ls = do + ifeqName <- fresh ifeqName + let + vs = Set.toList (Set.unions (map free (l:map the ls))) + lhs (t :=: _) = t + rhs (_ :=: u) = u + ifeq = + ifeqName ::: + FunType (map (typ . lhs . the) ls ++ map typ vs) + (typ (lhs l)) + app ts = ifeq :@: (ts ++ map Var vs) + msum $ map return [ + app (map (lhs . the) ls) :=: lhs l, + app (map (rhs . the) ls) :=: rhs l] + + encode :: Atomic -> Literal -> ListT (RWST () [Atomic] Int (Either (Input Clause))) Atomic + encode (c :=: d) (Neg (a :=: b)) = + let + ty1 = typ a + ty2 = typ c x = Var (xvar ::: ty1) y = Var (yvar ::: ty2) z = Var (zvar ::: ty2) - - ifeq ty1 ty2 = - variant ifeqName [name ty1, name ty2] ::: - FunType [ty1, ty1, ty2, ty2] ty2 + in case encoding flags of + -- ifeq(x, x, y) = y + -- ifeq(a, b, c) = ifeq(a, b, d) + Symmetric -> do + let ifeq = variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2] ty2 + 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 + -- extra: ifeq(x, y, z, z) = z + Asymmetric1 -> do + let + ifeq = variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2, ty2] ty2 + (c :=: d) <- return (swap size (c :=: d)) + axiom (ifeq :@: [x, x, y, z] :=: y) + return (ifeq :@: [a, b, c, d] :=: d) `mplus` do + guard (extra flags) + return (ifeq :@: [x, y, z, z] :=: z) + -- f(a, sigma) = c + -- f(b, sigma) = d + -- where sigma = FV(a, b, c, d) + Asymmetric2 -> do + ifeqName <- fresh ifeqName + let + vs = Set.toList (Set.unions (map free [a, b, c, d])) + ifeq = ifeqName ::: FunType (ty1:map typ vs) ty2 + app t = ifeq :@: (t:map Var vs) + msum $ map return [app a :=: c, app b :=: d] + -- f(a, b, sigma) = c + -- f(x, x, sigma) = d + -- where sigma = FV(c, d) + Asymmetric3 -> do + ifeqName <- fresh ifeqName + let + vs = Set.toList (Set.unions (map free [c, d])) + ifeq = ifeqName ::: FunType (ty1:ty1:map typ vs) ty2 + app t u = ifeq :@: (t:u:map Var vs) + x = Var (xvar ::: ty1) + msum $ map return [app a b :=: c, app x x :=: d] - isIfeq f = - isJust $ do - (x, _) <- unvariant (name f) - guard (x == ifeqName) + swap f (t :=: u) = + if f t >= f u then (t :=: u) else (u :=: t) - (ifeqName, xvar, yvar, zvar) = run prob $ \_ -> do + axiom l = lift $ tell [l] + + toInput l = + Input { + tag = "ifeq_axiom", + kind = Ax Axiom, + source = Unknown, + what = clause [Pos l] } + + (ifeqName, xvar, yvar, zvar) = run_ prob $ do ifeqName <- newName "$ifeq" - xvar <- newName "X" - yvar <- newName "Y" - zvar <- newName "Z" + xvar <- newName "A" + yvar <- newName "B" + zvar <- newName "C" return (ifeqName, xvar, yvar, zvar) + +-- Soundly encode types, but try to erase them if possible. +-- Based on the observation that if the input problem is untyped, +-- erasure is sound unless: +-- * the problem is satisfiable +-- * but the only model is of size 1. +-- We therefore check if there is a model of size 1. This is easy +-- (the term structure collapses), and if so, we return the SZS +-- status directly instead. +encodeTypesSmartly :: Problem Clause -> IO (Either Answer (Problem Clause -> Problem Clause)) +encodeTypesSmartly prob + | isFof prob = do + sat <- hasSizeOneModel prob + if sat then + return $ Left $ + Sat Satisfiable $ Just + ["There is a model where all terms are equal, ![X,Y]:X=Y."] + else return (Right eraseTypes) + | otherwise = + return (Right id) + +-- Check if a problem has a model of size 1. +-- Done by erasing all terms from the problem. +hasSizeOneModel :: Problem Clause -> IO Bool +hasSizeOneModel p = do + s <- Sat.newSolver + let funs = functions p + lits <- replicateM (length funs) (Sat.newLit s) + let + funMap = Map.fromList (zip funs lits) + transClause (Clause (Bind _ ls)) = + map transLit ls + transLit (Pos a) = transAtom a + transLit (Neg a) = Sat.neg (transAtom a) + transAtom (Tru (p :@: _)) = + Map.findWithDefault undefined p funMap + transAtom (_ :=: _) = Sat.true + mapM_ (Sat.addClause s . transClause) (map what p) + Sat.solve s [] <* Sat.deleteSolver s