{-# 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 = forall s. HasSAT s => Lens' s SAT
sat forall a b. (a -> b) -> a -> b
$ \ (SAT Int
a Formula
b HashMap (StableName ()) Literal
c) -> 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 = forall s. HasSAT s => Lens' s SAT
sat forall a b. (a -> b) -> a -> b
$ \ (SAT Int
a Formula
b HashMap (StableName ()) Literal
c) -> 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 = forall s. HasSAT s => Lens' s SAT
sat 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 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 :: Lens' SAT SAT
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 forall a. Ord a => a -> a -> Bool
> Int
10)
                 forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"SAT " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (SAT
bfforall s a. s -> Getting a s a -> a
^.forall s. HasSAT s => Lens' s Int
lastAtom)
                 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (SAT
bfforall s a. s -> Getting a s a -> a
^.forall s. HasSAT s => Lens' s Formula
formula)
                 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) 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 :: forall (m :: * -> *) a. StateT SAT m a -> m (a, SAT)
runSAT StateT SAT m a
s = forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT SAT m a
s 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' :: forall a. StateT SAT Identity a -> (a, SAT)
runSAT' = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. StateT SAT Identity a -> ByteString
dimacsSAT = Builder -> ByteString
toLazyByteString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. DIMACS t => t -> Builder
dimacs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StateT SAT Identity a -> (a, SAT)
runSAT'

literalExists :: MonadSAT s m => m Literal
literalExists :: forall s (m :: * -> *). MonadSAT s m => m Literal
literalExists = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Literal
Literal forall a b. (a -> b) -> a -> b
$ forall s. HasSAT s => Lens' s Int
lastAtom 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 :: forall s (m :: * -> *). MonadSAT s m => Formula -> m ()
assertFormula Formula
xs = forall s. HasSAT s => Lens' s Formula
formula 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 :: forall s (m :: * -> *) a.
MonadSAT s m =>
a -> (Literal -> m ()) -> m Literal
generateLiteral a
a Literal -> m ()
f = do
  let sn :: StableName ()
sn = forall a. IO a -> a
unsafePerformIO (forall a. a -> IO (StableName ())
makeStableName' a
a)
  forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use (forall s. HasSAT s => Lens' s (HashMap (StableName ()) Literal)
stableMapforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at StableName ()
sn) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Maybe Literal
ml -> case Maybe Literal
ml of
    Just Literal
l -> forall (m :: * -> *) a. Monad m => a -> m a
return Literal
l
    Maybe Literal
Nothing -> do
      Literal
l <- forall s (m :: * -> *). MonadSAT s m => m Literal
literalExists
      forall s. HasSAT s => Lens' s (HashMap (StableName ()) Literal)
stableMapforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at StableName ()
sn forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= Literal
l
      Literal -> m ()
f Literal
l
      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
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 = 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 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 :: Lens' QSAT SAT
sat SAT -> f SAT
f (QSAT IntSet
u SAT
s) = IntSet -> SAT -> QSAT
QSAT IntSet
u forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SAT -> f SAT
f SAT
s

instance HasQSAT QSAT where
  qsat :: Lens' QSAT QSAT
qsat = forall a. a -> a
id

instance Default QSAT where
  def :: QSAT
def = IntSet -> SAT -> QSAT
QSAT IntSet
IntSet.empty 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 :: forall (m :: * -> *) a. StateT QSAT m a -> m (a, QSAT)
runQSAT StateT QSAT m a
s = forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT QSAT m a
s 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' :: forall a. StateT QSAT Identity a -> (a, QSAT)
runQSAT' = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. StateT QSAT Identity a -> ByteString
qdimacsQSAT = Builder -> ByteString
toLazyByteString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. QDIMACS t => t -> Builder
qdimacs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StateT QSAT Identity a -> (a, QSAT)
runQSAT'

literalForall :: MonadQSAT s m => m Literal
literalForall :: forall s (m :: * -> *). MonadQSAT s m => m Literal
literalForall = do
   Int
l <- forall s. HasSAT s => Lens' s Int
lastAtom forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
<+= Int
1
   forall t. HasQSAT t => Lens' t IntSet
universalsforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall m. Contains m => Index m -> Lens' m Bool
contains Int
l forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Bool
True
   forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: forall t. DIMACS t => t -> Builder
dimacs t
t = Builder
comments forall a. Semigroup a => a -> a -> a
<> Builder
problem forall a. Semigroup a => a -> a -> a
<> Builder
clauses
  where
    comments :: Builder
comments = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ByteString -> Builder
bComment (forall t. DIMACS t => t -> [ByteString]
dimacsComments t
t)
    problem :: Builder
problem = [Builder] -> Builder
bLine [ String -> Builder
string7 String
"p cnf"
                    , Int -> Builder
intDec (forall t. DIMACS t => t -> Int
dimacsNumVariables t
t)
                    , Int -> Builder
intDec (forall a. Seq a -> Int
Seq.length Seq IntSet
tClauses)
                    ]
    clauses :: Builder
clauses = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap IntSet -> Builder
bClause Seq IntSet
tClauses

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

-- | Generate a 'Builder' out of a 'QDIMACS' problem.
qdimacs :: QDIMACS t => t -> Builder
qdimacs :: forall t. QDIMACS t => t -> Builder
qdimacs t
t = Builder
comments forall a. Semigroup a => a -> a -> a
<> Builder
problem forall a. Semigroup a => a -> a -> a
<> Builder
quantified forall a. Semigroup a => a -> a -> a
<> Builder
clauses
  where
    comments :: Builder
comments = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ByteString -> Builder
bComment (forall t. QDIMACS t => t -> [ByteString]
qdimacsComments t
t)
    problem :: Builder
problem = [Builder] -> Builder
bLine [ String -> Builder
string7 String
"p cnf"
                    , Int -> Builder
intDec (forall t. QDIMACS t => t -> Int
qdimacsNumVariables t
t)
                    , Int -> Builder
intDec (forall a. Seq a -> Int
Seq.length Seq IntSet
tClauses)
                    ]
    quantified :: Builder
quantified = 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 (forall a. [a] -> a
head [Quant]
ls) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Int -> Builder
intDec 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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap IntSet -> Builder
bClause Seq IntSet
tClauses

    tQuantGroups :: [[Quant]]
tQuantGroups = forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy Quant -> Quant -> Bool
eqQuant (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 = forall t. QDIMACS t => t -> Seq IntSet
qdimacsClauses t
t

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

    tClauses :: Seq (Int64, IntSet)
tClauses = 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 = forall a. (a -> Int -> a) -> a -> IntSet -> a
IntSet.foldl' ( \ Builder
e Int
i -> Int -> Builder
intDec Int
i forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Builder
e ) ( Char -> Builder
char7 Char
'0' 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 forall a. a -> [a] -> [a]
: 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ [Char -> Builder
char7 Char
'0'])

bLine :: [Builder] -> Builder
bLine :: [Builder] -> Builder
bLine [Builder]
bs = forall a. Monoid a => [a] -> a
mconcat (forall a. a -> [a] -> [a]
List.intersperse (Char -> Builder
char7 Char
' ') [Builder]
bs) 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
sforall s a. s -> Getting a s a -> a
^.forall s. HasSAT s => Lens' s Int
lastAtom
  dimacsClauses :: SAT -> Seq IntSet
dimacsClauses = forall s. HasSAT s => s -> Seq IntSet
satClauses

instance QDIMACS QSAT where
  qdimacsComments :: QSAT -> [ByteString]
qdimacsComments QSAT
_ = []
  qdimacsNumVariables :: QSAT -> Int
qdimacsNumVariables QSAT
q = QSAT
qforall s a. s -> Getting a s a -> a
^.forall s. HasSAT s => Lens' s Int
lastAtom 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
qforall s a. s -> Getting a s a -> a
^.forall t. HasQSAT t => Lens' t IntSet
universals), Int
i forall a. Eq a => a -> a -> Bool
== QSAT
qforall s a. s -> Getting a s a -> a
^.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
qforall s a. s -> Getting a s a -> a
^.forall t. HasQSAT t => Lens' t IntSet
universals) = []
    | Bool
otherwise = [Int] -> [Int] -> [Quant]
quants [forall a. [a] -> a
head [Int]
qUniversals..Int
lastAtom'] [Int]
qUniversals
    where
      lastAtom' :: Int
lastAtom'   = forall t. QDIMACS t => t -> Int
qdimacsNumVariables QSAT
q
      qUniversals :: [Int]
qUniversals = IntSet -> [Int]
IntSet.toAscList (QSAT
qforall s a. s -> Getting a s a -> a
^.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 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 forall a. Eq a => a -> a -> Bool
== Int
j    = Int -> Quant
Forall Int
i forall a. a -> [a] -> [a]
: [Int] -> [Int] -> [Quant]
quants [Int]
is [Int]
js
        | Bool
otherwise = Int -> Quant
Exists Int
i forall a. a -> [a] -> [a]
: [Int] -> [Int] -> [Quant]
quants [Int]
is [Int]
jjs
  qdimacsClauses :: QSAT -> Seq IntSet
qdimacsClauses = 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 :: forall s. HasSAT s => s -> Seq IntSet
satClauses s
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> IntSet
clauseSet (Formula -> Seq Clause
formulaSet (s
sforall s a. s -> Getting a s a -> a
^.forall s. HasSAT s => Lens' s Formula
formula))