{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE ConstraintKinds #-}

{-# OPTIONS_HADDOCK not-home #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Problem
  (
  -- * SAT
    SAT(SAT)
  , HasSAT(..)
  , MonadSAT
  , runSAT, runSAT', dimacsSAT
  , literalExists
  , assertFormula
  , generateLiteral
  -- * QSAT
  , QSAT(QSAT)
  , HasQSAT(..)
  , MonadQSAT
  , runQSAT, runQSAT', qdimacsQSAT
  , literalForall
  -- * DIMACS pretty printing
  , DIMACS(..)
  , QDIMACS(..)
  , WDIMACS(..)
  , dimacs, qdimacs, wdimacs
  ) where

import Data.ByteString.Builder
import Control.Lens
import Control.Monad.State
import Data.ByteString (ByteString)
import qualified Data.ByteString.Lazy as Lazy
import Data.Default
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as HashMap
import Data.Int
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Ersatz.Internal.Formula
import Ersatz.Internal.Literal
import Ersatz.Internal.StableName
import System.IO.Unsafe
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq

#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup (Semigroup(..))
#endif

-- | Constraint synonym for types that carry a SAT state.
type MonadSAT  s m = (HasSAT  s, MonadState s m)

-- | Constraint synonym for types that carry a QSAT state.
type MonadQSAT s m = (HasQSAT s, MonadState s m)

------------------------------------------------------------------------------
-- SAT Problems
------------------------------------------------------------------------------

data SAT = SAT
  { SAT -> Int
_lastAtom  :: {-# UNPACK #-} !Int      -- ^ The id of the last atom allocated
  , SAT -> Formula
_formula   :: !Formula                 -- ^ a set of clauses to assert
  , SAT -> HashMap (StableName ()) Literal
_stableMap :: !(HashMap (StableName ()) Literal)  -- ^ a mapping used during 'Bit' expansion
  }

class HasSAT s where
  sat :: Lens' s SAT

  lastAtom :: Lens' s Int
  lastAtom Int -> f Int
f = (SAT -> f SAT) -> s -> f s
forall s. HasSAT s => Lens' s SAT
sat ((SAT -> f SAT) -> s -> f s) -> (SAT -> f SAT) -> s -> f s
forall a b. (a -> b) -> a -> b
$ \ (SAT Int
a Formula
b HashMap (StableName ()) Literal
c) -> (Int -> SAT) -> f Int -> f SAT
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Int
a' -> Int -> Formula -> HashMap (StableName ()) Literal -> SAT
SAT Int
a' Formula
b HashMap (StableName ()) Literal
c) (Int -> f Int
f Int
a)

  formula :: Lens' s Formula
  formula Formula -> f Formula
f = (SAT -> f SAT) -> s -> f s
forall s. HasSAT s => Lens' s SAT
sat ((SAT -> f SAT) -> s -> f s) -> (SAT -> f SAT) -> s -> f s
forall a b. (a -> b) -> a -> b
$ \ (SAT Int
a Formula
b HashMap (StableName ()) Literal
c) -> (Formula -> SAT) -> f Formula -> f SAT
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Formula
b' -> Int -> Formula -> HashMap (StableName ()) Literal -> SAT
SAT Int
a Formula
b' HashMap (StableName ()) Literal
c) (Formula -> f Formula
f Formula
b)

  stableMap :: Lens' s (HashMap (StableName ()) Literal)
  stableMap HashMap (StableName ()) Literal
-> f (HashMap (StableName ()) Literal)
f = (SAT -> f SAT) -> s -> f s
forall s. HasSAT s => Lens' s SAT
sat ((SAT -> f SAT) -> s -> f s) -> (SAT -> f SAT) -> s -> f s
forall a b. (a -> b) -> a -> b
$ \ (SAT Int
a Formula
b HashMap (StableName ()) Literal
c) -> Int -> Formula -> HashMap (StableName ()) Literal -> SAT
SAT Int
a Formula
b (HashMap (StableName ()) Literal -> SAT)
-> f (HashMap (StableName ()) Literal) -> f SAT
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (StableName ()) Literal
-> f (HashMap (StableName ()) Literal)
f HashMap (StableName ()) Literal
c

instance HasSAT SAT where
  sat :: (SAT -> f SAT) -> SAT -> f SAT
sat = (SAT -> f SAT) -> SAT -> f SAT
forall a. a -> a
id

instance Show SAT where
  showsPrec :: Int -> SAT -> ShowS
showsPrec Int
p SAT
bf = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
                 (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"SAT " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (SAT
bfSAT -> Getting Int SAT Int -> Int
forall s a. s -> Getting a s a -> a
^.Getting Int SAT Int
forall s. HasSAT s => Lens' s Int
lastAtom)
                 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (SAT
bfSAT -> Getting Formula SAT Formula -> Formula
forall s a. s -> Getting a s a -> a
^.Getting Formula SAT Formula
forall s. HasSAT s => Lens' s Formula
formula)
                 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" mempty"


instance Default SAT where
  -- The literal 1 is dedicated for the True constant.
  def :: SAT
def = Int -> Formula -> HashMap (StableName ()) Literal -> SAT
SAT Int
1 (Literal -> Formula
formulaLiteral Literal
literalTrue) HashMap (StableName ()) Literal
forall k v. HashMap k v
HashMap.empty

-- | Run a 'SAT'-generating state computation. Useful e.g. in ghci for
-- disambiguating the type of a 'MonadSAT' value.
runSAT :: StateT SAT m a -> m (a, SAT)
runSAT :: StateT SAT m a -> m (a, SAT)
runSAT StateT SAT m a
s = StateT SAT m a -> SAT -> m (a, SAT)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT SAT m a
s SAT
forall a. Default a => a
def

-- | Run a 'SAT'-generating state computation in the 'Identity' monad. Useful
-- e.g. in ghci for disambiguating the type of a 'MonadSAT' value.
runSAT' :: StateT SAT Identity a -> (a, SAT)
runSAT' :: StateT SAT Identity a -> (a, SAT)
runSAT' = Identity (a, SAT) -> (a, SAT)
forall a. Identity a -> a
runIdentity (Identity (a, SAT) -> (a, SAT))
-> (StateT SAT Identity a -> Identity (a, SAT))
-> StateT SAT Identity a
-> (a, SAT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT SAT Identity a -> Identity (a, SAT)
forall (m :: * -> *) a. StateT SAT m a -> m (a, SAT)
runSAT

-- | Run a 'SAT'-generating state computation and return the respective
-- 'DIMACS' output. Useful for testing and debugging.
dimacsSAT :: StateT SAT Identity a -> Lazy.ByteString
dimacsSAT :: StateT SAT Identity a -> ByteString
dimacsSAT = Builder -> ByteString
toLazyByteString (Builder -> ByteString)
-> (StateT SAT Identity a -> Builder)
-> StateT SAT Identity a
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SAT -> Builder
forall t. DIMACS t => t -> Builder
dimacs (SAT -> Builder)
-> (StateT SAT Identity a -> SAT)
-> StateT SAT Identity a
-> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, SAT) -> SAT
forall a b. (a, b) -> b
snd ((a, SAT) -> SAT)
-> (StateT SAT Identity a -> (a, SAT))
-> StateT SAT Identity a
-> SAT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT SAT Identity a -> (a, SAT)
forall a. StateT SAT Identity a -> (a, SAT)
runSAT'

literalExists :: MonadSAT s m => m Literal
literalExists :: m Literal
literalExists = (Int -> Literal) -> m Int -> m Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Literal
Literal (m Int -> m Literal) -> m Int -> m Literal
forall a b. (a -> b) -> a -> b
$ (Int -> (Int, Int)) -> s -> (Int, s)
forall s. HasSAT s => Lens' s Int
lastAtom ((Int -> (Int, Int)) -> s -> (Int, s)) -> Int -> m Int
forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
<+= Int
1
{-# INLINE literalExists #-}

assertFormula :: MonadSAT s m => Formula -> m ()
assertFormula :: Formula -> m ()
assertFormula Formula
xs = (Formula -> Identity Formula) -> s -> Identity s
forall s. HasSAT s => Lens' s Formula
formula ((Formula -> Identity Formula) -> s -> Identity s)
-> Formula -> m ()
forall s (m :: * -> *) a.
(MonadState s m, Semigroup a) =>
ASetter' s a -> a -> m ()
<>= Formula
xs
{-# INLINE assertFormula #-}

generateLiteral :: MonadSAT s m => a -> (Literal -> m ()) -> m Literal
generateLiteral :: a -> (Literal -> m ()) -> m Literal
generateLiteral a
a Literal -> m ()
f = do
  let sn :: StableName ()
sn = IO (StableName ()) -> StableName ()
forall a. IO a -> a
unsafePerformIO (a -> IO (StableName ())
forall a. a -> IO (StableName ())
makeStableName' a
a)
  Getting (Maybe Literal) s (Maybe Literal) -> m (Maybe Literal)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((HashMap (StableName ()) Literal
 -> Const (Maybe Literal) (HashMap (StableName ()) Literal))
-> s -> Const (Maybe Literal) s
forall s. HasSAT s => Lens' s (HashMap (StableName ()) Literal)
stableMap((HashMap (StableName ()) Literal
  -> Const (Maybe Literal) (HashMap (StableName ()) Literal))
 -> s -> Const (Maybe Literal) s)
-> ((Maybe Literal -> Const (Maybe Literal) (Maybe Literal))
    -> HashMap (StableName ()) Literal
    -> Const (Maybe Literal) (HashMap (StableName ()) Literal))
-> Getting (Maybe Literal) s (Maybe Literal)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (HashMap (StableName ()) Literal)
-> Lens'
     (HashMap (StableName ()) Literal)
     (Maybe (IxValue (HashMap (StableName ()) Literal)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at StableName ()
Index (HashMap (StableName ()) Literal)
sn) m (Maybe Literal) -> (Maybe Literal -> m Literal) -> m Literal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Maybe Literal
ml -> case Maybe Literal
ml of
    Just Literal
l -> Literal -> m Literal
forall (m :: * -> *) a. Monad m => a -> m a
return Literal
l
    Maybe Literal
Nothing -> do
      Literal
l <- m Literal
forall s (m :: * -> *). MonadSAT s m => m Literal
literalExists
      (HashMap (StableName ()) Literal
 -> Identity (HashMap (StableName ()) Literal))
-> s -> Identity s
forall s. HasSAT s => Lens' s (HashMap (StableName ()) Literal)
stableMap((HashMap (StableName ()) Literal
  -> Identity (HashMap (StableName ()) Literal))
 -> s -> Identity s)
-> ((Maybe Literal -> Identity (Maybe Literal))
    -> HashMap (StableName ()) Literal
    -> Identity (HashMap (StableName ()) Literal))
-> (Maybe Literal -> Identity (Maybe Literal))
-> s
-> Identity s
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (HashMap (StableName ()) Literal)
-> Lens'
     (HashMap (StableName ()) Literal)
     (Maybe (IxValue (HashMap (StableName ()) Literal)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at StableName ()
Index (HashMap (StableName ()) Literal)
sn ((Maybe Literal -> Identity (Maybe Literal)) -> s -> Identity s)
-> Literal -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= Literal
l
      Literal -> m ()
f Literal
l
      Literal -> m Literal
forall (m :: * -> *) a. Monad m => a -> m a
return Literal
l
{-# INLINE generateLiteral #-}

------------------------------------------------------------------------------
-- QSAT Problems
------------------------------------------------------------------------------

-- | A (quantified) boolean formula.
data QSAT = QSAT
  { QSAT -> IntSet
_universals :: !IntSet -- ^ a set indicating which literals are universally quantified
  , QSAT -> SAT
_qsatSat    :: SAT     -- ^ The rest of the information, in 'SAT'
  } deriving Int -> QSAT -> ShowS
[QSAT] -> ShowS
QSAT -> String
(Int -> QSAT -> ShowS)
-> (QSAT -> String) -> ([QSAT] -> ShowS) -> Show QSAT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QSAT] -> ShowS
$cshowList :: [QSAT] -> ShowS
show :: QSAT -> String
$cshow :: QSAT -> String
showsPrec :: Int -> QSAT -> ShowS
$cshowsPrec :: Int -> QSAT -> ShowS
Show

class HasSAT t => HasQSAT t where
  qsat       :: Lens' t QSAT
  universals :: Lens' t IntSet
  universals IntSet -> f IntSet
f = (QSAT -> f QSAT) -> t -> f t
forall t. HasQSAT t => Lens' t QSAT
qsat QSAT -> f QSAT
ago where
    ago :: QSAT -> f QSAT
ago (QSAT IntSet
u SAT
s) = IntSet -> f IntSet
f IntSet
u f IntSet -> (IntSet -> QSAT) -> f QSAT
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \IntSet
u' -> IntSet -> SAT -> QSAT
QSAT IntSet
u' SAT
s

instance HasSAT QSAT where
  sat :: (SAT -> f SAT) -> QSAT -> f QSAT
sat SAT -> f SAT
f (QSAT IntSet
u SAT
s) = IntSet -> SAT -> QSAT
QSAT IntSet
u (SAT -> QSAT) -> f SAT -> f QSAT
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SAT -> f SAT
f SAT
s

instance HasQSAT QSAT where
  qsat :: (QSAT -> f QSAT) -> QSAT -> f QSAT
qsat = (QSAT -> f QSAT) -> QSAT -> f QSAT
forall a. a -> a
id

instance Default QSAT where
  def :: QSAT
def = IntSet -> SAT -> QSAT
QSAT IntSet
IntSet.empty SAT
forall a. Default a => a
def

-- | Run a 'QSAT'-generating state computation. Useful e.g. in ghci for
-- disambiguating the type of a 'MonadState', 'HasQSAT' value.
runQSAT :: StateT QSAT m a -> m (a, QSAT)
runQSAT :: StateT QSAT m a -> m (a, QSAT)
runQSAT StateT QSAT m a
s = StateT QSAT m a -> QSAT -> m (a, QSAT)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT QSAT m a
s QSAT
forall a. Default a => a
def

-- | Run a 'QSAT'-generating state computation in the 'Identity' monad. Useful
-- e.g. in ghci for disambiguating the type of a 'MonadState', 'HasQSAT' value.
runQSAT' :: StateT QSAT Identity a -> (a, QSAT)
runQSAT' :: StateT QSAT Identity a -> (a, QSAT)
runQSAT' = Identity (a, QSAT) -> (a, QSAT)
forall a. Identity a -> a
runIdentity (Identity (a, QSAT) -> (a, QSAT))
-> (StateT QSAT Identity a -> Identity (a, QSAT))
-> StateT QSAT Identity a
-> (a, QSAT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT QSAT Identity a -> Identity (a, QSAT)
forall (m :: * -> *) a. StateT QSAT m a -> m (a, QSAT)
runQSAT

-- | Run a 'QSAT'-generating state computation and return the respective
-- 'QDIMACS' output. Useful for testing and debugging.
qdimacsQSAT :: StateT QSAT Identity a -> Lazy.ByteString
qdimacsQSAT :: StateT QSAT Identity a -> ByteString
qdimacsQSAT = Builder -> ByteString
toLazyByteString (Builder -> ByteString)
-> (StateT QSAT Identity a -> Builder)
-> StateT QSAT Identity a
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QSAT -> Builder
forall t. QDIMACS t => t -> Builder
qdimacs (QSAT -> Builder)
-> (StateT QSAT Identity a -> QSAT)
-> StateT QSAT Identity a
-> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, QSAT) -> QSAT
forall a b. (a, b) -> b
snd ((a, QSAT) -> QSAT)
-> (StateT QSAT Identity a -> (a, QSAT))
-> StateT QSAT Identity a
-> QSAT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT QSAT Identity a -> (a, QSAT)
forall a. StateT QSAT Identity a -> (a, QSAT)
runQSAT'

literalForall :: MonadQSAT s m => m Literal
literalForall :: m Literal
literalForall = do
   Int
l <- (Int -> (Int, Int)) -> s -> (Int, s)
forall s. HasSAT s => Lens' s Int
lastAtom ((Int -> (Int, Int)) -> s -> (Int, s)) -> Int -> m Int
forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
<+= Int
1
   (IntSet -> Identity IntSet) -> s -> Identity s
forall t. HasQSAT t => Lens' t IntSet
universals((IntSet -> Identity IntSet) -> s -> Identity s)
-> ((Bool -> Identity Bool) -> IntSet -> Identity IntSet)
-> (Bool -> Identity Bool)
-> s
-> Identity s
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index IntSet -> Lens' IntSet Bool
forall m. Contains m => Index m -> Lens' m Bool
contains Int
Index IntSet
l ((Bool -> Identity Bool) -> s -> Identity s) -> Bool -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Bool
True
   Literal -> m Literal
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> m Literal) -> Literal -> m Literal
forall a b. (a -> b) -> a -> b
$ Int -> Literal
Literal Int
l
{-# INLINE literalForall #-}

------------------------------------------------------------------------------
-- Printing SATs
------------------------------------------------------------------------------

-- | DIMACS file format pretty printer
--
-- This is used to generate the problem statement for a given 'SAT' 'Ersatz.Solver.Solver'.

-- http://www.cfdvs.iitb.ac.in/download/Docs/verification/papers/BMC/JT.ps
class DIMACS t where
  dimacsComments :: t -> [ByteString]
  dimacsNumVariables :: t -> Int
  dimacsClauses :: t -> Seq IntSet

-- | QDIMACS file format pretty printer
--
-- This is used to generate the problem statement for a given 'QSAT' 'Ersatz.Solver.Solver'.

-- http://www.qbflib.org/qdimacs.html
class QDIMACS t where
  qdimacsComments :: t -> [ByteString]
  qdimacsNumVariables :: t -> Int
  qdimacsQuantified :: t -> [Quant]
  qdimacsClauses :: t -> Seq IntSet

-- | WDIMACS file format pretty printer
--
-- This is used to generate the problem statement for a given 'MaxSAT' 'Ersatz.Solver.Solver' (TODO).

-- http://maxsat.ia.udl.cat/requirements/
class WDIMACS t where
  wdimacsComments :: t -> [ByteString]
  wdimacsNumVariables :: t -> Int
  wdimacsTopWeight :: t -> Int64  -- ^ Specified to be 1 ≤ n < 2^63
  wdimacsClauses :: t -> Seq (Int64, IntSet)

-- | Generate a 'Builder' out of a 'DIMACS' problem.
dimacs :: DIMACS t => t -> Builder
dimacs :: t -> Builder
dimacs t
t = Builder
comments Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
problem Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
clauses
  where
    comments :: Builder
comments = (ByteString -> Builder) -> [ByteString] -> Builder
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ByteString -> Builder
bComment (t -> [ByteString]
forall t. DIMACS t => t -> [ByteString]
dimacsComments t
t)
    problem :: Builder
problem = [Builder] -> Builder
bLine [ String -> Builder
string7 String
"p cnf"
                    , Int -> Builder
intDec (t -> Int
forall t. DIMACS t => t -> Int
dimacsNumVariables t
t)
                    , Int -> Builder
intDec (Seq IntSet -> Int
forall a. Seq a -> Int
Seq.length Seq IntSet
tClauses)
                    ]
    clauses :: Builder
clauses = (IntSet -> Builder) -> Seq IntSet -> Builder
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap IntSet -> Builder
bClause Seq IntSet
tClauses

    tClauses :: Seq IntSet
tClauses = t -> Seq IntSet
forall t. DIMACS t => t -> Seq IntSet
dimacsClauses t
t

-- | Generate a 'Builder' out of a 'QDIMACS' problem.
qdimacs :: QDIMACS t => t -> Builder
qdimacs :: t -> Builder
qdimacs t
t = Builder
comments Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
problem Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
quantified Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
clauses
  where
    comments :: Builder
comments = (ByteString -> Builder) -> [ByteString] -> Builder
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ByteString -> Builder
bComment (t -> [ByteString]
forall t. QDIMACS t => t -> [ByteString]
qdimacsComments t
t)
    problem :: Builder
problem = [Builder] -> Builder
bLine [ String -> Builder
string7 String
"p cnf"
                    , Int -> Builder
intDec (t -> Int
forall t. QDIMACS t => t -> Int
qdimacsNumVariables t
t)
                    , Int -> Builder
intDec (Seq IntSet -> Int
forall a. Seq a -> Int
Seq.length Seq IntSet
tClauses)
                    ]
    quantified :: Builder
quantified = ([Quant] -> Builder) -> [[Quant]] -> Builder
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap [Quant] -> Builder
go [[Quant]]
tQuantGroups
      where go :: [Quant] -> Builder
go [Quant]
ls = [Builder] -> Builder
bLine0 (Quant -> Builder
q ([Quant] -> Quant
forall a. [a] -> a
head [Quant]
ls) Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
: (Quant -> Builder) -> [Quant] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Builder
intDec (Int -> Builder) -> (Quant -> Int) -> Quant -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quant -> Int
getQuant) [Quant]
ls)
            q :: Quant -> Builder
q Exists{} = Char -> Builder
char7 Char
'e'
            q Forall{} = Char -> Builder
char7 Char
'a'
    clauses :: Builder
clauses = (IntSet -> Builder) -> Seq IntSet -> Builder
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap IntSet -> Builder
bClause Seq IntSet
tClauses

    tQuantGroups :: [[Quant]]
tQuantGroups = (Quant -> Quant -> Bool) -> [Quant] -> [[Quant]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy Quant -> Quant -> Bool
eqQuant (t -> [Quant]
forall t. QDIMACS t => t -> [Quant]
qdimacsQuantified t
t)
      where
        eqQuant :: Quant -> Quant -> Bool
        eqQuant :: Quant -> Quant -> Bool
eqQuant Exists{} Exists{} = Bool
True
        eqQuant Forall{} Forall{} = Bool
True
        eqQuant Quant
_ Quant
_ = Bool
False
    tClauses :: Seq IntSet
tClauses = t -> Seq IntSet
forall t. QDIMACS t => t -> Seq IntSet
qdimacsClauses t
t

-- | Generate a 'Builder' out of a 'WDIMACS' problem.
wdimacs :: WDIMACS t => t -> Builder
wdimacs :: t -> Builder
wdimacs t
t = Builder
comments Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
problem Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
clauses
  where
    comments :: Builder
comments = (ByteString -> Builder) -> [ByteString] -> Builder
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ByteString -> Builder
bComment (t -> [ByteString]
forall t. WDIMACS t => t -> [ByteString]
wdimacsComments t
t)
    problem :: Builder
problem = [Builder] -> Builder
bLine [ String -> Builder
string7 String
"p wcnf"
                    , Int -> Builder
intDec (t -> Int
forall t. WDIMACS t => t -> Int
wdimacsNumVariables t
t)
                    , Int -> Builder
intDec (Seq (Int64, IntSet) -> Int
forall a. Seq a -> Int
Seq.length Seq (Int64, IntSet)
tClauses)
                    , Int64 -> Builder
int64Dec (t -> Int64
forall t. WDIMACS t => t -> Int64
wdimacsTopWeight t
t)
                    ]
    clauses :: Builder
clauses = ((Int64, IntSet) -> Builder) -> Seq (Int64, IntSet) -> Builder
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Int64 -> IntSet -> Builder) -> (Int64, IntSet) -> Builder
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int64 -> IntSet -> Builder
bWClause) Seq (Int64, IntSet)
tClauses

    tClauses :: Seq (Int64, IntSet)
tClauses = t -> Seq (Int64, IntSet)
forall t. WDIMACS t => t -> Seq (Int64, IntSet)
wdimacsClauses t
t

bComment :: ByteString -> Builder
bComment :: ByteString -> Builder
bComment ByteString
bs = [Builder] -> Builder
bLine [ Char -> Builder
char7 Char
'c', ByteString -> Builder
byteString ByteString
bs ]

bClause :: IntSet -> Builder
bClause :: IntSet -> Builder
bClause = (Builder -> Int -> Builder) -> Builder -> IntSet -> Builder
forall a. (a -> Int -> a) -> a -> IntSet -> a
IntSet.foldl' ( \ Builder
e Int
i -> Int -> Builder
intDec Int
i Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
e ) ( Char -> Builder
char7 Char
'0' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
'\n' )

bWClause :: Int64 -> IntSet -> Builder
bWClause :: Int64 -> IntSet -> Builder
bWClause Int64
w IntSet
ls = [Builder] -> Builder
bLine0 (Int64 -> Builder
int64Dec Int64
w Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
: (Int -> Builder) -> [Int] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Builder
intDec (IntSet -> [Int]
IntSet.toList IntSet
ls))

bLine0 :: [Builder] -> Builder
bLine0 :: [Builder] -> Builder
bLine0 = [Builder] -> Builder
bLine ([Builder] -> Builder)
-> ([Builder] -> [Builder]) -> [Builder] -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ [Char -> Builder
char7 Char
'0'])

bLine :: [Builder] -> Builder
bLine :: [Builder] -> Builder
bLine [Builder]
bs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat (Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
List.intersperse (Char -> Builder
char7 Char
' ') [Builder]
bs) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
'\n'

-- | An explicit prenex quantifier
data Quant
  = Exists { Quant -> Int
getQuant :: {-# UNPACK #-} !Int }
  | Forall { getQuant :: {-# UNPACK #-} !Int }

instance DIMACS SAT where
  dimacsComments :: SAT -> [ByteString]
dimacsComments SAT
_ = []
  dimacsNumVariables :: SAT -> Int
dimacsNumVariables SAT
s = SAT
sSAT -> Getting Int SAT Int -> Int
forall s a. s -> Getting a s a -> a
^.Getting Int SAT Int
forall s. HasSAT s => Lens' s Int
lastAtom
  dimacsClauses :: SAT -> Seq IntSet
dimacsClauses = SAT -> Seq IntSet
forall s. HasSAT s => s -> Seq IntSet
satClauses

instance QDIMACS QSAT where
  qdimacsComments :: QSAT -> [ByteString]
qdimacsComments QSAT
_ = []
  qdimacsNumVariables :: QSAT -> Int
qdimacsNumVariables QSAT
q = QSAT
qQSAT -> Getting Int QSAT Int -> Int
forall s a. s -> Getting a s a -> a
^.Getting Int QSAT Int
forall s. HasSAT s => Lens' s Int
lastAtom Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
padding
    where
      -- "The innermost quantified set is always of type 'e'" per QDIMACS
      -- standard. Add an existential atom if the last one is universal.
      padding :: Int
padding
        | Just (Int
i, IntSet
_) <- IntSet -> Maybe (Int, IntSet)
IntSet.maxView (QSAT
qQSAT -> Getting IntSet QSAT IntSet -> IntSet
forall s a. s -> Getting a s a -> a
^.Getting IntSet QSAT IntSet
forall t. HasQSAT t => Lens' t IntSet
universals), Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== QSAT
qQSAT -> Getting Int QSAT Int -> Int
forall s a. s -> Getting a s a -> a
^.Getting Int QSAT Int
forall s. HasSAT s => Lens' s Int
lastAtom = Int
1
        | Bool
otherwise = Int
0
  -- "Unbound atoms are to be considered as being existentially quantified in
  -- the first (i.e., the outermost) quantified set." per QDIMACS standard.
  -- Skip the implicit first existentials.
  qdimacsQuantified :: QSAT -> [Quant]
qdimacsQuantified QSAT
q
    | IntSet -> Bool
IntSet.null (QSAT
qQSAT -> Getting IntSet QSAT IntSet -> IntSet
forall s a. s -> Getting a s a -> a
^.Getting IntSet QSAT IntSet
forall t. HasQSAT t => Lens' t IntSet
universals) = []
    | Bool
otherwise = [Int] -> [Int] -> [Quant]
quants [[Int] -> Int
forall a. [a] -> a
head [Int]
qUniversals..Int
lastAtom'] [Int]
qUniversals
    where
      lastAtom' :: Int
lastAtom'   = QSAT -> Int
forall t. QDIMACS t => t -> Int
qdimacsNumVariables QSAT
q
      qUniversals :: [Int]
qUniversals = IntSet -> [Int]
IntSet.toAscList (QSAT
qQSAT -> Getting IntSet QSAT IntSet -> IntSet
forall s a. s -> Getting a s a -> a
^.Getting IntSet QSAT IntSet
forall t. HasQSAT t => Lens' t IntSet
universals)

      quants :: [Int] -> [Int] -> [Quant]
      quants :: [Int] -> [Int] -> [Quant]
quants []     [Int]
_  = []
      quants (Int
i:[Int]
is) [] = Int -> Quant
Exists Int
i Quant -> [Quant] -> [Quant]
forall a. a -> [a] -> [a]
: [Int] -> [Int] -> [Quant]
quants [Int]
is []
      quants (Int
i:[Int]
is) jjs :: [Int]
jjs@(Int
j:[Int]
js)
        | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j    = Int -> Quant
Forall Int
i Quant -> [Quant] -> [Quant]
forall a. a -> [a] -> [a]
: [Int] -> [Int] -> [Quant]
quants [Int]
is [Int]
js
        | Bool
otherwise = Int -> Quant
Exists Int
i Quant -> [Quant] -> [Quant]
forall a. a -> [a] -> [a]
: [Int] -> [Int] -> [Quant]
quants [Int]
is [Int]
jjs
  qdimacsClauses :: QSAT -> Seq IntSet
qdimacsClauses = QSAT -> Seq IntSet
forall s. HasSAT s => s -> Seq IntSet
satClauses

-- | the name is wrong (Does it return Clauses? No - it returns IntSets.)
-- and it means extra work (traversing, and re-building, the full collection).
-- Or is this fused away (because of Coercible)?
satClauses :: HasSAT s => s -> Seq IntSet
satClauses :: s -> Seq IntSet
satClauses s
s = (Clause -> IntSet) -> Seq Clause -> Seq IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> IntSet
clauseSet (Formula -> Seq Clause
formulaSet (s
ss -> Getting Formula s Formula -> Formula
forall s a. s -> Getting a s a -> a
^.Getting Formula s Formula
forall s. HasSAT s => Lens' s Formula
formula))