packages feed

jukebox 0.3 → 0.3.1

raw patch · 14 files changed

+389/−108 lines, 14 files

Files

dist/build/Jukebox/TPTP/Lexer.hs view
@@ -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";
executable/Main.hs view
@@ -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 ())))
+ gcc-static-libstdc++ view
@@ -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
jukebox.cabal view
@@ -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++
src/Jukebox/ExternalProvers/E.hs view
@@ -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] ++
src/Jukebox/ExternalProvers/SPASS.hs view
@@ -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 ]
src/Jukebox/Form.hs view
@@ -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)])
src/Jukebox/Name.hs view
@@ -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 =
src/Jukebox/Options.hs view
@@ -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+        [] -> "<empty list>" -- ??+        _ ->+          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
src/Jukebox/SMTLIB.hs view
@@ -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]
src/Jukebox/TPTP/Lexer.x view
@@ -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";
src/Jukebox/TPTP/ParseSnippet.hs view
@@ -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
src/Jukebox/Toolbox.hs view
@@ -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 "<function>" "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",
src/Jukebox/Tools/HornToUnit.hs view
@@ -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