content: {-# OPTIONS_GHC -Wall #-}
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.Converter.QBF2IPC
  -- Copyright   :  (c) Masahiro Sakai 2018
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  experimental
  -- Portability :  portable
  --
  -- References:
  --
  -- * Morten Heine B. Sørensen, and Pawel Urzyczyn. Lectures on the Curry-Howard
  --   Isomorphism. http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
  --
  -----------------------------------------------------------------------------
  module ToySolver.Converter.QBF2IPC
    ( qbf2ipc
    ) where
  
  import qualified Data.IntSet as IntSet
  
  import ToySolver.Data.Boolean
  import ToySolver.Data.BoolExpr (BoolExpr)
  import qualified ToySolver.Data.BoolExpr as BoolExpr
  import qualified ToySolver.FileFormat.CNF as CNF
  import qualified ToySolver.QBF as QBF
  import qualified ToySolver.SAT.Types as SAT
  
  
  qbf2ipc :: CNF.QDimacs -> (Int, [BoolExpr SAT.Var], BoolExpr SAT.Var)
  qbf2ipc qdimacs = (nv2, lhs, rhs)
    where
      nv = CNF.qdimacsNumVars qdimacs
      nc = CNF.qdimacsNumClauses qdimacs
  
      prefix = [(q,a) | (q,as) <- qs, a <- IntSet.toList as]
        where
          qs = QBF.quantifyFreeVariables nv [(q, IntSet.fromList as) | (q,as) <- CNF.qdimacsPrefix qdimacs]
  
      nv2 = nv -- positive literal
          + nv -- negative literal
          + nc -- clause
          + 1  -- conjunction
          + nv -- quantified formula
      alpha_xp x = x
      alpha_xn x = nv + x
      alpha_l l  = BoolExpr.Atom $ if l > 0 then alpha_xp l else alpha_xn (- l)
      alpha_c i  = BoolExpr.Atom $ nv + nv + (1 + i)
      alpha_mat  = BoolExpr.Atom $ nv + nv + nc + 1
      alpha_qf i = BoolExpr.Atom $ nv + nv + nc + 1 + (1 + i)
  
      lhs =
        snd (f (zip [0..] prefix)) ++
        [foldr (.=>.) alpha_mat [alpha_c i | (i,_) <- zip [0..] (CNF.qdimacsMatrix qdimacs)]] ++
        concat [[alpha_l l .=>. alpha_c i | l <- SAT.unpackClause c] | (i, c) <- zip [0..] (CNF.qdimacsMatrix qdimacs)]
        where
          f [] = (alpha_mat, [])
          f ((i,(QBF.E,x)) : qs) =
           case f qs of
             (alpha_body, ret) -> (alpha_qf i, [(alpha_l x .=>. alpha_body) .=>. alpha_qf i, (alpha_l (- x) .=>. alpha_body) .=>. alpha_qf i] ++ ret)
          f ((i,(QBF.A,x)) : qs) =
           case f qs of
             (alpha_body, ret) -> (alpha_qf i, [(alpha_l x .=>. alpha_body) .=>. (alpha_l (- x) .=>. alpha_body) .=>. alpha_qf i] ++ ret)
  
      rhs = alpha_qf 0
  