{-# 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 -> (Int, [BoolExpr Int], BoolExpr Int)
qbf2ipc QDimacs
qdimacs = (Int
nv2, [BoolExpr Int]
lhs, BoolExpr Int
rhs)
  where
    nv :: Int
nv = QDimacs -> Int
CNF.qdimacsNumVars QDimacs
qdimacs
    nc :: Int
nc = QDimacs -> Int
CNF.qdimacsNumClauses QDimacs
qdimacs

    prefix :: [(Quantifier, Int)]
prefix = [(Quantifier
q,Int
a) | (Quantifier
q,VarSet
as) <- Prefix
qs, Int
a <- VarSet -> [Int]
IntSet.toList VarSet
as]
      where
        qs :: Prefix
qs = Int -> Prefix -> Prefix
QBF.quantifyFreeVariables Int
nv [(Quantifier
q, [Int] -> VarSet
IntSet.fromList [Int]
as) | (Quantifier
q,[Int]
as) <- QDimacs -> [(Quantifier, [Int])]
CNF.qdimacsPrefix QDimacs
qdimacs]

    nv2 :: Int
nv2 = Int
nv -- positive literal
        forall a. Num a => a -> a -> a
+ Int
nv -- negative literal
        forall a. Num a => a -> a -> a
+ Int
nc -- clause
        forall a. Num a => a -> a -> a
+ Int
1  -- conjunction
        forall a. Num a => a -> a -> a
+ Int
nv -- quantified formula
    alpha_xp :: p -> p
alpha_xp p
x = p
x
    alpha_xn :: Int -> Int
alpha_xn Int
x = Int
nv forall a. Num a => a -> a -> a
+ Int
x
    alpha_l :: Int -> BoolExpr Int
alpha_l Int
l  = forall a. a -> BoolExpr a
BoolExpr.Atom forall a b. (a -> b) -> a -> b
$ if Int
l forall a. Ord a => a -> a -> Bool
> Int
0 then forall {p}. p -> p
alpha_xp Int
l else Int -> Int
alpha_xn (- Int
l)
    alpha_c :: Int -> BoolExpr Int
alpha_c Int
i  = forall a. a -> BoolExpr a
BoolExpr.Atom forall a b. (a -> b) -> a -> b
$ Int
nv forall a. Num a => a -> a -> a
+ Int
nv forall a. Num a => a -> a -> a
+ (Int
1 forall a. Num a => a -> a -> a
+ Int
i)
    alpha_mat :: BoolExpr Int
alpha_mat  = forall a. a -> BoolExpr a
BoolExpr.Atom forall a b. (a -> b) -> a -> b
$ Int
nv forall a. Num a => a -> a -> a
+ Int
nv forall a. Num a => a -> a -> a
+ Int
nc forall a. Num a => a -> a -> a
+ Int
1
    alpha_qf :: Int -> BoolExpr Int
alpha_qf Int
i = forall a. a -> BoolExpr a
BoolExpr.Atom forall a b. (a -> b) -> a -> b
$ Int
nv forall a. Num a => a -> a -> a
+ Int
nv forall a. Num a => a -> a -> a
+ Int
nc forall a. Num a => a -> a -> a
+ Int
1 forall a. Num a => a -> a -> a
+ (Int
1 forall a. Num a => a -> a -> a
+ Int
i)

    lhs :: [BoolExpr Int]
lhs =
      forall a b. (a, b) -> b
snd ([(Int, (Quantifier, Int))] -> (BoolExpr Int, [BoolExpr Int])
f (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(Quantifier, Int)]
prefix)) forall a. [a] -> [a] -> [a]
++
      [forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Boolean a => a -> a -> a
(.=>.) BoolExpr Int
alpha_mat [Int -> BoolExpr Int
alpha_c Int
i | (Int
i,PackedClause
_) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (QDimacs -> [PackedClause]
CNF.qdimacsMatrix QDimacs
qdimacs)]] forall a. [a] -> [a] -> [a]
++
      forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Int -> BoolExpr Int
alpha_l Int
l forall a. Boolean a => a -> a -> a
.=>. Int -> BoolExpr Int
alpha_c Int
i | Int
l <- PackedClause -> [Int]
SAT.unpackClause PackedClause
c] | (Int
i, PackedClause
c) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (QDimacs -> [PackedClause]
CNF.qdimacsMatrix QDimacs
qdimacs)]
      where
        f :: [(Int, (Quantifier, Int))] -> (BoolExpr Int, [BoolExpr Int])
f [] = (BoolExpr Int
alpha_mat, [])
        f ((Int
i,(Quantifier
QBF.E,Int
x)) : [(Int, (Quantifier, Int))]
qs) =
         case [(Int, (Quantifier, Int))] -> (BoolExpr Int, [BoolExpr Int])
f [(Int, (Quantifier, Int))]
qs of
           (BoolExpr Int
alpha_body, [BoolExpr Int]
ret) -> (Int -> BoolExpr Int
alpha_qf Int
i, [(Int -> BoolExpr Int
alpha_l Int
x forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) forall a. Boolean a => a -> a -> a
.=>. Int -> BoolExpr Int
alpha_qf Int
i, (Int -> BoolExpr Int
alpha_l (- Int
x) forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) forall a. Boolean a => a -> a -> a
.=>. Int -> BoolExpr Int
alpha_qf Int
i] forall a. [a] -> [a] -> [a]
++ [BoolExpr Int]
ret)
        f ((Int
i,(Quantifier
QBF.A,Int
x)) : [(Int, (Quantifier, Int))]
qs) =
         case [(Int, (Quantifier, Int))] -> (BoolExpr Int, [BoolExpr Int])
f [(Int, (Quantifier, Int))]
qs of
           (BoolExpr Int
alpha_body, [BoolExpr Int]
ret) -> (Int -> BoolExpr Int
alpha_qf Int
i, [(Int -> BoolExpr Int
alpha_l Int
x forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) forall a. Boolean a => a -> a -> a
.=>. (Int -> BoolExpr Int
alpha_l (- Int
x) forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) forall a. Boolean a => a -> a -> a
.=>. Int -> BoolExpr Int
alpha_qf Int
i] forall a. [a] -> [a] -> [a]
++ [BoolExpr Int]
ret)

    rhs :: BoolExpr Int
rhs = Int -> BoolExpr Int
alpha_qf Int
0