{-# OPTIONS_GHC -Wall #-}
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
+ nv
+ nc
+ 1
+ nv
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