{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE ConstraintKinds #-}
{-# OPTIONS_HADDOCK not-home #-}
module Ersatz.Problem
(
SAT(SAT)
, HasSAT(..)
, MonadSAT
, runSAT, runSAT', dimacsSAT
, literalExists
, assertFormula
, generateLiteral
, QSAT(QSAT)
, HasQSAT(..)
, MonadQSAT
, runQSAT, runQSAT', qdimacsQSAT
, literalForall
, 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
type MonadSAT s m = (HasSAT s, MonadState s m)
type MonadQSAT s m = (HasQSAT s, MonadState s m)
data SAT = SAT
{ SAT -> Int
_lastAtom :: {-# UNPACK #-} !Int
, SAT -> Formula
_formula :: !Formula
, SAT -> HashMap (StableName ()) Literal
_stableMap :: !(HashMap (StableName ()) Literal)
}
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
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
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
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
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 #-}
data QSAT = QSAT
{ QSAT -> IntSet
_universals :: !IntSet
, QSAT -> SAT
_qsatSat :: 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
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
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
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 #-}
class DIMACS t where
:: t -> [ByteString]
dimacsNumVariables :: t -> Int
dimacsClauses :: t -> Seq IntSet
class QDIMACS t where
:: t -> [ByteString]
qdimacsNumVariables :: t -> Int
qdimacsQuantified :: t -> [Quant]
qdimacsClauses :: t -> Seq IntSet
class WDIMACS t where
:: t -> [ByteString]
wdimacsNumVariables :: t -> Int
wdimacsTopWeight :: t -> Int64
wdimacsClauses :: t -> Seq (Int64, IntSet)
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
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
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
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'
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
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
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
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))