content: {- |
  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
      { initialAxioms :: [AS_Anno.Named AS.FORMULA]
      , initialSignature :: Sign
      , freeDefs :: [LP.FreeDefMorphism AS.FORMULA QMorphism.Morphism]
      } deriving (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 aSens freedefs =
      let
          axioms = prepareSenNames transSenName $ filter AS_Anno.isAxiom aSens
      in
          foldl insertSentence
          QBFProverState
          {
            initialAxioms = []
          , initialSignature = sign
          , freeDefs = freedefs
          } axioms
  
  transSenName :: String -> String
  transSenName = 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 pst f = pst { initialAxioms = initialAxioms pst ++ [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 thName pst nGoal _ =
      let
          fList :: AS.FORMULA -> [[AS.FORMULA]]
          fList (AS.Conjunction fs _) = map (\ f ->
            case f of
               (AS.Disjunction xs _) -> xs
               a@(AS.TrueAtom _) -> [a]
               a@(AS.FalseAtom _) -> [a]
               p@(AS.Predication _) -> [p]
               x -> error ("Unexpected " ++ show x)
             ) fs
          fList (AS.Disjunction xs _) = [xs]
          fList a@(AS.TrueAtom _) = [[a]]
          fList a@(AS.FalseAtom _) = [[a]]
          fList p@(AS.Predication _) = [[p]]
          fList n@(AS.Negation _ _) = [[n]]
          fList f = error ("Unexpected " ++ show f)
          atomToNum :: AS.FORMULA -> Int
          atomToNum f = case f of
                             AS.TrueAtom _ -> trueAtom
                             AS.FalseAtom _ -> falseAtom
                             AS.Negation x _ -> -(atomToNum x)
                             AS.Predication t ->
                               case (elemIndex t qf, elemIndex t qe) of
                                    (Just i, Nothing) -> 1 + i
                                    (Nothing, Just i) -> lqf + 1 + i
                                    _ -> error ("Unknown variable " ++ show f)
                             t -> error ("Unexpected " ++ show t)
  
          axioms = map (AS_Anno.senAttr Control.Arrow.&&& AS_Anno.sentence)
                       (initialAxioms pst)
          goal = AS_Anno.sentence 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 = maximum (map (length . tokStr)
                                (concatMap getVars (goal : (snd . unzip) axioms)))
          prefix = replicate maxVarLen '_'
          (c, goal1) = uniqueQuantifiedVars 1 prefix goal
          axioms1 = snd (foldr (\ (s, f) (c', a') -> let
              (c1, f') = uniqueQuantifiedVars c' prefix f
            in
              (c1, (s, f') : a')) (c, []) axioms)
          -- next we transform everything into cnf form
          axioms2 = map (Control.Arrow.second (fList . cnf . removeQuantifiers))
                      axioms1
          goal2 = (fList . cnf . removeQuantifiers) 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 = foldr joinQuantifiedVars quantifiedVars
            (getQuantifiedVars goal1 : map (getQuantifiedVars . snd) axioms1)
          qf = universallyQ qv
          qe = existentiallyQ qv ++ notQ qv
          lqf = length qf
          lqe = length qe
          (cTrueAtom, cFalseAtom) = foldl
            (\ (r1, r2) (r3, r4) -> (r1 || r3, r2 || r4))
            (False, False) ((containsAtoms . AS_Anno.sentence) nGoal :
              map (containsAtoms . AS_Anno.sentence) (initialAxioms pst))
          goalN = AS_Anno.senAttr nGoal
          trueAtom = lqf + lqe + (if cTrueAtom then 1 else 0)
          falseAtom = -(trueAtom + (if cFalseAtom then 1 else 0))
          base = 3 + (if lqf > 0 then 1 else 0)
            + (if lqe > 0 then 1 else 0) + length axioms2
          axiomsL = sum (map (length . snd) axioms2)
      in
          return (unlines ([
            "c Problem" ++ thName,
            "c The goal " ++ goalN ++ " is on the lines "
            ++ show (base + axiomsL + 1) ++ "-"
            ++ show (base + axiomsL + length goal2)
            ] ++ snd (foldl
                        (\ (cnt, lst) (name, fs) ->
                          ( cnt + length fs,
                            lst ++
                            ["c The axiom " ++ name ++ " is on the lines "
                              ++ show (base + cnt)
                              ++ "-"
                              ++ show (base + cnt + length fs - 1)
                            ]
                          )
                        ) (1, []) axioms2)
            ++ ["p cnf "
                 ++ show (-falseAtom)
                 ++ " "
                 ++ show (length goal2 + axiomsL)
               ]
            ++ (if null qf then []
                else ["a " ++ unwords (map show ([1 .. lqf] ++ [0]))])
            ++ (if null qe then []
                else ["e " ++ unwords (map show
                       ([(lqf + 1) .. (lqf + lqe)] ++ [0]))])
            ++ concatMap
                   (\ (_, f) -> map
                                  (\ fs -> unwords
                                            (map (show . atomToNum) fs ++ ["0"])
                                  ) f
                   ) (axioms2 ++ [("", goal2)])
            ++ (if cTrueAtom then [show trueAtom, " 0"] else [])
            ++ (if cFalseAtom then [show falseAtom, " 0"] else [])))
  