{-# 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
        Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nv -- negative literal
        Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc -- clause
        Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1  -- conjunction
        Int -> Int -> Int
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
x
    alpha_l :: Int -> BoolExpr Int
alpha_l Int
l  = Int -> BoolExpr Int
forall a. a -> BoolExpr a
BoolExpr.Atom (Int -> BoolExpr Int) -> Int -> BoolExpr Int
forall a b. (a -> b) -> a -> b
$ if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Int -> Int
forall {p}. p -> p
alpha_xp Int
l else Int -> Int
alpha_xn (- Int
l)
    alpha_c :: Int -> BoolExpr Int
alpha_c Int
i  = Int -> BoolExpr Int
forall a. a -> BoolExpr a
BoolExpr.Atom (Int -> BoolExpr Int) -> Int -> BoolExpr Int
forall a b. (a -> b) -> a -> b
$ Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)
    alpha_mat :: BoolExpr Int
alpha_mat  = Int -> BoolExpr Int
forall a. a -> BoolExpr a
BoolExpr.Atom (Int -> BoolExpr Int) -> Int -> BoolExpr Int
forall a b. (a -> b) -> a -> b
$ Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    alpha_qf :: Int -> BoolExpr Int
alpha_qf Int
i = Int -> BoolExpr Int
forall a. a -> BoolExpr a
BoolExpr.Atom (Int -> BoolExpr Int) -> Int -> BoolExpr Int
forall a b. (a -> b) -> a -> b
$ Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)

    lhs :: [BoolExpr Int]
lhs =
      (BoolExpr Int, [BoolExpr Int]) -> [BoolExpr Int]
forall a b. (a, b) -> b
snd ([(Int, (Quantifier, Int))] -> (BoolExpr Int, [BoolExpr Int])
f ([Int] -> [(Quantifier, Int)] -> [(Int, (Quantifier, Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(Quantifier, Int)]
prefix)) [BoolExpr Int] -> [BoolExpr Int] -> [BoolExpr Int]
forall a. [a] -> [a] -> [a]
++
      [(BoolExpr Int -> BoolExpr Int -> BoolExpr Int)
-> BoolExpr Int -> [BoolExpr Int] -> BoolExpr Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
(.=>.) BoolExpr Int
alpha_mat [Int -> BoolExpr Int
alpha_c Int
i | (Int
i,PackedClause
_) <- [Int] -> [PackedClause] -> [(Int, PackedClause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (QDimacs -> [PackedClause]
CNF.qdimacsMatrix QDimacs
qdimacs)]] [BoolExpr Int] -> [BoolExpr Int] -> [BoolExpr Int]
forall a. [a] -> [a] -> [a]
++
      [[BoolExpr Int]] -> [BoolExpr Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Int -> BoolExpr Int
alpha_l Int
l BoolExpr Int -> BoolExpr Int -> BoolExpr Int
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) <- [Int] -> [PackedClause] -> [(Int, PackedClause)]
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 BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. Int -> BoolExpr Int
alpha_qf Int
i, (Int -> BoolExpr Int
alpha_l (- Int
x) BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. Int -> BoolExpr Int
alpha_qf Int
i] [BoolExpr Int] -> [BoolExpr Int] -> [BoolExpr Int]
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 BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. (Int -> BoolExpr Int
alpha_l (- Int
x) BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. BoolExpr Int
alpha_body) BoolExpr Int -> BoolExpr Int -> BoolExpr Int
forall a. Boolean a => a -> a -> a
.=>. Int -> BoolExpr Int
alpha_qf Int
i] [BoolExpr Int] -> [BoolExpr Int] -> [BoolExpr Int]
forall a. [a] -> [a] -> [a]
++ [BoolExpr Int]
ret)

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