module Ersatz.Problem
(
Problem(qbfLastAtom, qbfFormula, qbfUniversals, qbfSNMap)
, QDIMACS(..)
) where
import Data.Default
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as HashMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List (groupBy)
import qualified Data.Set as Set
import Data.Typeable
import Ersatz.Internal.Formula
import Ersatz.Internal.Literal
import Ersatz.Internal.StableName
data Problem = Problem
{ qbfLastAtom :: !Int
, qbfFormula :: !Formula
, qbfUniversals :: !IntSet
, qbfSNMap :: !(HashMap (StableName ()) Literal)
} deriving Typeable
instance Default Problem where
def = Problem 0 (Formula Set.empty) IntSet.empty HashMap.empty
instance Show Problem where
showsPrec p qbf = showParen (p > 10)
$ showString "Problem .. " . showsPrec 11 (qbfFormula qbf) . showString " .."
class QDIMACS t where
qdimacs :: t -> String
instance QDIMACS Literal where
qdimacs (Literal n) = show n
instance QDIMACS Formula where
qdimacs (Formula cs) = unlines $ map qdimacs (Set.toList cs)
instance QDIMACS Clause where
qdimacs (Clause xs) = unwords $ map show (IntSet.toList xs) ++ ["0"]
instance QDIMACS Problem where
qdimacs (Problem vars formula@(Formula cs) qs _) =
unlines (header : map showGroup quantGroups) ++ qdimacs formula
where
header = unwords ["p", "cnf", show (vars + padding), show (Set.size cs) ]
padding | Just (n, _) <- IntSet.maxView qs, n == vars = 1
| otherwise = 0
quantGroups | IntSet.null qs = []
| otherwise = List.groupBy eqQuant $ quants [head qlist..vars] qlist
where qlist = IntSet.toAscList qs
showGroup :: [Quant] -> String
showGroup xs = unwords $ q (head xs) : map (show . getQuant) xs
eqQuant :: Quant -> Quant -> Bool
eqQuant Exists{} Exists{} = True
eqQuant Forall{} Forall{} = True
eqQuant _ _ = False
q :: Quant -> String
q Exists{} = "e"
q Forall{} = "a"
quants :: [Int] -> [Int] -> [Quant]
quants [] _ = []
quants (i:is) [] = Exists i : quants is []
quants (i:is) jjs@(j:js)
| i == j = Forall i : quants is js
| otherwise = Exists i : quants is jjs
data Quant
= Exists { getQuant :: !Int }
| Forall { getQuant :: !Int }
deriving Typeable