{- |
Module      :  ./QBF/ProverState.hs
Description :  Help functions for all automatic theorem provers.
Copyright   :  (c) Jonatzhan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

Data structures and initialising functions for Prover state and configurations.

-}

module QBF.ProverState where

import Logic.Prover as LP

import Propositional.Sign
import qualified QBF.Morphism as QMorphism
import qualified QBF.AS_BASIC_QBF as AS
import QBF.Tools

import Data.List (elemIndex)
import qualified Control.Arrow

import qualified Common.AS_Annotation as AS_Anno
import Common.ProofUtils
import Common.Id

-- * Data structures

data QBFProverState = QBFProverState
    { QBFProverState -> [Named FORMULA]
initialAxioms :: [AS_Anno.Named AS.FORMULA]
    , QBFProverState -> Sign
initialSignature :: Sign
    , QBFProverState -> [FreeDefMorphism FORMULA Morphism]
freeDefs :: [LP.FreeDefMorphism AS.FORMULA QMorphism.Morphism]
    } deriving (Int -> QBFProverState -> ShowS
[QBFProverState] -> ShowS
QBFProverState -> String
(Int -> QBFProverState -> ShowS)
-> (QBFProverState -> String)
-> ([QBFProverState] -> ShowS)
-> Show QBFProverState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QBFProverState] -> ShowS
$cshowList :: [QBFProverState] -> ShowS
show :: QBFProverState -> String
$cshow :: QBFProverState -> String
showsPrec :: Int -> QBFProverState -> ShowS
$cshowsPrec :: Int -> QBFProverState -> ShowS
Show)

{- |
  Creates an initial qbf prover state
-}
qbfProverState :: Sign -- ^ QBF signature
                 -> [AS_Anno.Named AS.FORMULA] -- ^ list of named QBF formulas
                 -> [LP.FreeDefMorphism AS.FORMULA QMorphism.Morphism]
                 -- ^ freeness constraints
                 -> QBFProverState
qbfProverState :: Sign
-> [Named FORMULA]
-> [FreeDefMorphism FORMULA Morphism]
-> QBFProverState
qbfProverState sign :: Sign
sign aSens :: [Named FORMULA]
aSens freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
    let
        axioms :: [Named FORMULA]
axioms = ShowS -> [Named FORMULA] -> [Named FORMULA]
forall a. ShowS -> [Named a] -> [Named a]
prepareSenNames ShowS
transSenName ([Named FORMULA] -> [Named FORMULA])
-> [Named FORMULA] -> [Named FORMULA]
forall a b. (a -> b) -> a -> b
$ (Named FORMULA -> Bool) -> [Named FORMULA] -> [Named FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter Named FORMULA -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom [Named FORMULA]
aSens
    in
        (QBFProverState -> Named FORMULA -> QBFProverState)
-> QBFProverState -> [Named FORMULA] -> QBFProverState
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl QBFProverState -> Named FORMULA -> QBFProverState
insertSentence
        QBFProverState :: [Named FORMULA]
-> Sign -> [FreeDefMorphism FORMULA Morphism] -> QBFProverState
QBFProverState
        {
          initialAxioms :: [Named FORMULA]
initialAxioms = []
        , initialSignature :: Sign
initialSignature = Sign
sign
        , freeDefs :: [FreeDefMorphism FORMULA Morphism]
freeDefs = [FreeDefMorphism FORMULA Morphism]
freedefs
        } [Named FORMULA]
axioms

transSenName :: String -> String
transSenName :: ShowS
transSenName = ShowS
forall a. a -> a
id

{- |
  Inserts a named SoftFOL term into SoftFOL prover state.
-}
insertSentence :: QBFProverState -- ^ prover state containing the axioms
                  -> AS_Anno.Named AS.FORMULA -- ^ formula to add
                  -> QBFProverState
insertSentence :: QBFProverState -> Named FORMULA -> QBFProverState
insertSentence pst :: QBFProverState
pst f :: Named FORMULA
f = QBFProverState
pst { initialAxioms :: [Named FORMULA]
initialAxioms = QBFProverState -> [Named FORMULA]
initialAxioms QBFProverState
pst [Named FORMULA] -> [Named FORMULA] -> [Named FORMULA]
forall a. [a] -> [a] -> [a]
++ [Named FORMULA
f] }

{- |
  Pretty printing QBF goal in QDIMACS format.
-}
showQDIMACSProblem :: String -- ^ theory name
                -> QBFProverState -- ^ prover state
                -> AS_Anno.Named AS.FORMULA -- ^ goal
                -> [String] -- ^ extra options
                -> IO String -- ^ formatted output of the goal
showQDIMACSProblem :: String -> QBFProverState -> Named FORMULA -> [String] -> IO String
showQDIMACSProblem thName :: String
thName pst :: QBFProverState
pst nGoal :: Named FORMULA
nGoal _ =
    let
        fList :: AS.FORMULA -> [[AS.FORMULA]]
        fList :: FORMULA -> [[FORMULA]]
fList (AS.Conjunction fs :: [FORMULA]
fs _) = (FORMULA -> [FORMULA]) -> [FORMULA] -> [[FORMULA]]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: FORMULA
f ->
          case FORMULA
f of
             (AS.Disjunction xs :: [FORMULA]
xs _) -> [FORMULA]
xs
             a :: FORMULA
a@(AS.TrueAtom _) -> [FORMULA
a]
             a :: FORMULA
a@(AS.FalseAtom _) -> [FORMULA
a]
             p :: FORMULA
p@(AS.Predication _) -> [FORMULA
p]
             x :: FORMULA
x -> String -> [FORMULA]
forall a. HasCallStack => String -> a
error ("Unexpected " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FORMULA -> String
forall a. Show a => a -> String
show FORMULA
x)
           ) [FORMULA]
fs
        fList (AS.Disjunction xs :: [FORMULA]
xs _) = [[FORMULA]
xs]
        fList a :: FORMULA
a@(AS.TrueAtom _) = [[FORMULA
a]]
        fList a :: FORMULA
a@(AS.FalseAtom _) = [[FORMULA
a]]
        fList p :: FORMULA
p@(AS.Predication _) = [[FORMULA
p]]
        fList n :: FORMULA
n@(AS.Negation _ _) = [[FORMULA
n]]
        fList f :: FORMULA
f = String -> [[FORMULA]]
forall a. HasCallStack => String -> a
error ("Unexpected " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FORMULA -> String
forall a. Show a => a -> String
show FORMULA
f)
        atomToNum :: AS.FORMULA -> Int
        atomToNum :: FORMULA -> Int
atomToNum f :: FORMULA
f = case FORMULA
f of
                           AS.TrueAtom _ -> Int
trueAtom
                           AS.FalseAtom _ -> Int
falseAtom
                           AS.Negation x :: FORMULA
x _ -> -(FORMULA -> Int
atomToNum FORMULA
x)
                           AS.Predication t :: Token
t ->
                             case (Token -> [Token] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Token
t [Token]
qf, Token -> [Token] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Token
t [Token]
qe) of
                                  (Just i :: Int
i, Nothing) -> 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
                                  (Nothing, Just i :: Int
i) -> Int
lqf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
                                  _ -> String -> Int
forall a. HasCallStack => String -> a
error ("Unknown variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FORMULA -> String
forall a. Show a => a -> String
show FORMULA
f)
                           t :: FORMULA
t -> String -> Int
forall a. HasCallStack => String -> a
error ("Unexpected " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FORMULA -> String
forall a. Show a => a -> String
show FORMULA
t)

        axioms :: [(String, FORMULA)]
axioms = (Named FORMULA -> (String, FORMULA))
-> [Named FORMULA] -> [(String, FORMULA)]
forall a b. (a -> b) -> [a] -> [b]
map (Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr (Named FORMULA -> String)
-> (Named FORMULA -> FORMULA) -> Named FORMULA -> (String, FORMULA)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
Control.Arrow.&&& Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence)
                     (QBFProverState -> [Named FORMULA]
initialAxioms QBFProverState
pst)
        goal :: FORMULA
goal = Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence Named FORMULA
nGoal
        {- first we need to make sure that we simply can move out all
        quantifiers by making sure that every quantified variable is unique -}
        maxVarLen :: Int
maxVarLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Token -> Int) -> [Token] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> (Token -> String) -> Token -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
tokStr)
                              ((FORMULA -> [Token]) -> [FORMULA] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [Token]
getVars (FORMULA
goal FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: (([String], [FORMULA]) -> [FORMULA]
forall a b. (a, b) -> b
snd (([String], [FORMULA]) -> [FORMULA])
-> ([(String, FORMULA)] -> ([String], [FORMULA]))
-> [(String, FORMULA)]
-> [FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, FORMULA)] -> ([String], [FORMULA])
forall a b. [(a, b)] -> ([a], [b])
unzip) [(String, FORMULA)]
axioms)))
        prefix :: String
prefix = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
maxVarLen '_'
        (c :: Int
c, goal1 :: FORMULA
goal1) = Int -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars 1 String
prefix FORMULA
goal
        axioms1 :: [(String, FORMULA)]
axioms1 = (Int, [(String, FORMULA)]) -> [(String, FORMULA)]
forall a b. (a, b) -> b
snd (((String, FORMULA)
 -> (Int, [(String, FORMULA)]) -> (Int, [(String, FORMULA)]))
-> (Int, [(String, FORMULA)])
-> [(String, FORMULA)]
-> (Int, [(String, FORMULA)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (s :: String
s, f :: FORMULA
f) (c' :: Int
c', a' :: [(String, FORMULA)]
a') -> let
            (c1 :: Int
c1, f' :: FORMULA
f') = Int -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars Int
c' String
prefix FORMULA
f
          in
            (Int
c1, (String
s, FORMULA
f') (String, FORMULA) -> [(String, FORMULA)] -> [(String, FORMULA)]
forall a. a -> [a] -> [a]
: [(String, FORMULA)]
a')) (Int
c, []) [(String, FORMULA)]
axioms)
        -- next we transform everything into cnf form
        axioms2 :: [(String, [[FORMULA]])]
axioms2 = ((String, FORMULA) -> (String, [[FORMULA]]))
-> [(String, FORMULA)] -> [(String, [[FORMULA]])]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA -> [[FORMULA]])
-> (String, FORMULA) -> (String, [[FORMULA]])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
Control.Arrow.second (FORMULA -> [[FORMULA]]
fList (FORMULA -> [[FORMULA]])
-> (FORMULA -> FORMULA) -> FORMULA -> [[FORMULA]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
cnf (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
removeQuantifiers))
                    [(String, FORMULA)]
axioms1
        goal2 :: [[FORMULA]]
goal2 = (FORMULA -> [[FORMULA]]
fList (FORMULA -> [[FORMULA]])
-> (FORMULA -> FORMULA) -> FORMULA -> [[FORMULA]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
cnf (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
removeQuantifiers) FORMULA
goal1
        {- find out how the variables are quantified - variables that
        are not explictly quantified are treated to be existentially
        quantified since a theory holds iff it has a model -}
        qv :: QuantifiedVars
qv = (QuantifiedVars -> QuantifiedVars -> QuantifiedVars)
-> QuantifiedVars -> [QuantifiedVars] -> QuantifiedVars
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars QuantifiedVars
quantifiedVars
          (FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
goal1 QuantifiedVars -> [QuantifiedVars] -> [QuantifiedVars]
forall a. a -> [a] -> [a]
: ((String, FORMULA) -> QuantifiedVars)
-> [(String, FORMULA)] -> [QuantifiedVars]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA -> QuantifiedVars
getQuantifiedVars (FORMULA -> QuantifiedVars)
-> ((String, FORMULA) -> FORMULA)
-> (String, FORMULA)
-> QuantifiedVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, FORMULA) -> FORMULA
forall a b. (a, b) -> b
snd) [(String, FORMULA)]
axioms1)
        qf :: [Token]
qf = QuantifiedVars -> [Token]
universallyQ QuantifiedVars
qv
        qe :: [Token]
qe = QuantifiedVars -> [Token]
existentiallyQ QuantifiedVars
qv [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ QuantifiedVars -> [Token]
notQ QuantifiedVars
qv
        lqf :: Int
lqf = [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
qf
        lqe :: Int
lqe = [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
qe
        (cTrueAtom :: Bool
cTrueAtom, cFalseAtom :: Bool
cFalseAtom) = ((Bool, Bool) -> (Bool, Bool) -> (Bool, Bool))
-> (Bool, Bool) -> [(Bool, Bool)] -> (Bool, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
          (\ (r1 :: Bool
r1, r2 :: Bool
r2) (r3 :: Bool
r3, r4 :: Bool
r4) -> (Bool
r1 Bool -> Bool -> Bool
|| Bool
r3, Bool
r2 Bool -> Bool -> Bool
|| Bool
r4))
          (Bool
False, Bool
False) ((FORMULA -> (Bool, Bool)
containsAtoms (FORMULA -> (Bool, Bool))
-> (Named FORMULA -> FORMULA) -> Named FORMULA -> (Bool, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence) Named FORMULA
nGoal (Bool, Bool) -> [(Bool, Bool)] -> [(Bool, Bool)]
forall a. a -> [a] -> [a]
:
            (Named FORMULA -> (Bool, Bool))
-> [Named FORMULA] -> [(Bool, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA -> (Bool, Bool)
containsAtoms (FORMULA -> (Bool, Bool))
-> (Named FORMULA -> FORMULA) -> Named FORMULA -> (Bool, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence) (QBFProverState -> [Named FORMULA]
initialAxioms QBFProverState
pst))
        goalN :: String
goalN = Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal
        trueAtom :: Int
trueAtom = Int
lqf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lqe Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (if Bool
cTrueAtom then 1 else 0)
        falseAtom :: Int
falseAtom = -(Int
trueAtom Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (if Bool
cFalseAtom then 1 else 0))
        base :: Int
base = 3 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (if Int
lqf Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then 1 else 0)
          Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (if Int
lqe Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then 1 else 0) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(String, [[FORMULA]])] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, [[FORMULA]])]
axioms2
        axiomsL :: Int
axiomsL = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((String, [[FORMULA]]) -> Int) -> [(String, [[FORMULA]])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([[FORMULA]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[FORMULA]] -> Int)
-> ((String, [[FORMULA]]) -> [[FORMULA]])
-> (String, [[FORMULA]])
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, [[FORMULA]]) -> [[FORMULA]]
forall a b. (a, b) -> b
snd) [(String, [[FORMULA]])]
axioms2)
    in
        String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> String
unlines ([
          "c Problem" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thName,
          "c The goal " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
goalN String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is on the lines "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
base Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
axiomsL Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "-"
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
base Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
axiomsL Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[FORMULA]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[FORMULA]]
goal2)
          ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int, [String]) -> [String]
forall a b. (a, b) -> b
snd (((Int, [String]) -> (String, [[FORMULA]]) -> (Int, [String]))
-> (Int, [String]) -> [(String, [[FORMULA]])] -> (Int, [String])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
                      (\ (cnt :: Int
cnt, lst :: [String]
lst) (name :: String
name, fs :: [[FORMULA]]
fs) ->
                        ( Int
cnt Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[FORMULA]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[FORMULA]]
fs,
                          [String]
lst [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                          ["c The axiom " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is on the lines "
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
base Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
cnt)
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ "-"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
base Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
cnt Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[FORMULA]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[FORMULA]]
fs Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)
                          ]
                        )
                      ) (1, []) [(String, [[FORMULA]])]
axioms2)
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["p cnf "
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (-Int
falseAtom)
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ " "
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([[FORMULA]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[FORMULA]]
goal2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
axiomsL)
             ]
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
qf then []
              else ["a " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show ([1 .. Int
lqf] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [0]))])
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
qe then []
              else ["e " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show
                     ([(Int
lqf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) .. (Int
lqf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lqe)] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [0]))])
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, [[FORMULA]]) -> [String])
-> [(String, [[FORMULA]])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                 (\ (_, f :: [[FORMULA]]
f) -> ([FORMULA] -> String) -> [[FORMULA]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
                                (\ fs :: [FORMULA]
fs -> [String] -> String
unwords
                                          ((FORMULA -> String) -> [FORMULA] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (FORMULA -> Int) -> FORMULA -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> Int
atomToNum) [FORMULA]
fs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["0"])
                                ) [[FORMULA]]
f
                 ) ([(String, [[FORMULA]])]
axioms2 [(String, [[FORMULA]])]
-> [(String, [[FORMULA]])] -> [(String, [[FORMULA]])]
forall a. [a] -> [a] -> [a]
++ [("", [[FORMULA]]
goal2)])
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Bool
cTrueAtom then [Int -> String
forall a. Show a => a -> String
show Int
trueAtom, " 0"] else [])
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Bool
cFalseAtom then [Int -> String
forall a. Show a => a -> String
show Int
falseAtom, " 0"] else [])))