-- | A monadic interface to the SAT (@minisat@) solver.
--
-- The interface is inspired by ST monad. 'SAT' and 'Lit' are indexed by a "state" token,
-- so you cannot mixup literals from different SAT computations.
module Control.Monad.SAT (
    -- * SAT Monad
    SAT,
    runSAT,
    runSATMaybe,
    UnsatException (..),
    -- * Literals
    Lit,
    newLit,
    -- ** Negation
    Neg (..),
    -- * Clauses
    addClause,
    assertAtLeastOne,
    assertAtMostOne,
    assertAtMostOnePairwise,
    assertAtMostOneSequential,
    assertEqual,
    assertAllEqual,
    -- ** Propositional formulas
    Prop,
    true, false,
    lit, (\/), (/\), (<->), (-->), xor, ite,
    addDefinition,
    addProp,
    -- ** Clause definitions
    trueLit,
    falseLit,
    addConjDefinition,
    addDisjDefinition,
    -- * Solving
    solve,
    solve_,
    -- * Simplification
    simplify,
    -- * Statistics
    numberOfVariables,
    numberOfClauses,
    numberOfLearnts,
    numberOfConflicts,
) where

import Control.Exception       (Exception, catch, throwIO)
import Control.Monad           (forM_, unless)
import Control.Monad.IO.Class  (MonadIO (..))
import Control.Monad.IO.Unlift (MonadUnliftIO (..))
import Data.Bits               (shiftR, testBit)
import Data.IORef              (IORef, newIORef, readIORef, writeIORef)
import Data.List               (tails)
import Data.Map.Strict         (Map)
import Data.Set                (Set)
import GHC.Exts                (oneShot)

import qualified Data.Map.Strict as Map
import qualified Data.Set        as Set
import qualified MiniSat

-------------------------------------------------------------------------------
-- SAT Monad
-------------------------------------------------------------------------------

-- | Satisfiability monad.
newtype SAT s a = SAT_ { forall s a.
SAT s a -> Solver -> Lit s -> IORef (Definitions s) -> IO a
unSAT :: MiniSat.Solver -> Lit s -> IORef (Definitions s) -> IO a }
  deriving forall a b. a -> SAT s b -> SAT s a
forall a b. (a -> b) -> SAT s a -> SAT s b
forall s a b. a -> SAT s b -> SAT s a
forall s a b. (a -> b) -> SAT s a -> SAT s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> SAT s b -> SAT s a
$c<$ :: forall s a b. a -> SAT s b -> SAT s a
fmap :: forall a b. (a -> b) -> SAT s a -> SAT s b
$cfmap :: forall s a b. (a -> b) -> SAT s a -> SAT s b
Functor

-- The SAT monad environment consists of
-- * A solver instance
-- * A literal constraint to be true.
-- * A map of asserted definitions, to dedup these for 'addDefinitions' and 'addProp' calls.
--   (we don't dedup clauses though - it's up to the solver).

type role SAT nominal representational

pattern SAT :: forall s a. (MiniSat.Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
pattern $bSAT :: forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
$mSAT :: forall {r} {s} {a}.
SAT s a
-> ((Solver -> Lit s -> IORef (Definitions s) -> IO a) -> r)
-> ((# #) -> r)
-> r
SAT m <- SAT_ m
  where SAT Solver -> Lit s -> IORef (Definitions s) -> IO a
m = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT_ (oneShot :: forall a b. (a -> b) -> a -> b
oneShot Solver -> Lit s -> IORef (Definitions s) -> IO a
m)
{-# COMPLETE SAT #-}

type Definitions s = Map (Set (Lit s)) (Lit s)

-- | Unsatisfiable exception.
--
-- It may be thrown by various functions: in particular 'solve' and 'solve_', but also 'addClause', 'simplify'.
--
-- The reason to use an exception is because after unsatisfiable state is reached the underlying solver instance is unusable.
-- You may use 'runSATMaybe' to catch it.
data UnsatException = UnsatException
  deriving (Int -> UnsatException -> ShowS
[UnsatException] -> ShowS
UnsatException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnsatException] -> ShowS
$cshowList :: [UnsatException] -> ShowS
show :: UnsatException -> String
$cshow :: UnsatException -> String
showsPrec :: Int -> UnsatException -> ShowS
$cshowsPrec :: Int -> UnsatException -> ShowS
Show)

instance Exception UnsatException

data SATPanic = SATPanic
  deriving (Int -> SATPanic -> ShowS
[SATPanic] -> ShowS
SATPanic -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SATPanic] -> ShowS
$cshowList :: [SATPanic] -> ShowS
show :: SATPanic -> String
$cshow :: SATPanic -> String
showsPrec :: Int -> SATPanic -> ShowS
$cshowsPrec :: Int -> SATPanic -> ShowS
Show)

instance Exception SATPanic

instance Applicative (SAT s) where
    pure :: forall a. a -> SAT s a
pure a
x = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT (\Solver
_ Lit s
_ IORef (Definitions s)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
    SAT Solver -> Lit s -> IORef (Definitions s) -> IO (a -> b)
f <*> :: forall a b. SAT s (a -> b) -> SAT s a -> SAT s b
<*> SAT Solver -> Lit s -> IORef (Definitions s) -> IO a
x = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT (\Solver
s Lit s
t IORef (Definitions s)
r -> Solver -> Lit s -> IORef (Definitions s) -> IO (a -> b)
f Solver
s Lit s
t IORef (Definitions s)
r forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solver -> Lit s -> IORef (Definitions s) -> IO a
x Solver
s Lit s
t IORef (Definitions s)
r)

instance Monad (SAT s) where
    SAT s a
m >>= :: forall a b. SAT s a -> (a -> SAT s b) -> SAT s b
>>= a -> SAT s b
k = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
t IORef (Definitions s)
r -> do
        a
x <- forall s a.
SAT s a -> Solver -> Lit s -> IORef (Definitions s) -> IO a
unSAT SAT s a
m Solver
s Lit s
t IORef (Definitions s)
r
        forall s a.
SAT s a -> Solver -> Lit s -> IORef (Definitions s) -> IO a
unSAT (a -> SAT s b
k a
x) Solver
s Lit s
t IORef (Definitions s)
r

instance MonadIO (SAT s) where
    liftIO :: forall a. IO a -> SAT s a
liftIO IO a
m = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT (\Solver
_ Lit s
_ IORef (Definitions s)
_ -> IO a
m)

instance MonadUnliftIO (SAT s) where
    withRunInIO :: forall b. ((forall a. SAT s a -> IO a) -> IO b) -> SAT s b
withRunInIO (forall a. SAT s a -> IO a) -> IO b
kont = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
t IORef (Definitions s)
r -> (forall a. SAT s a -> IO a) -> IO b
kont (\(SAT Solver -> Lit s -> IORef (Definitions s) -> IO a
m) -> Solver -> Lit s -> IORef (Definitions s) -> IO a
m Solver
s Lit s
t IORef (Definitions s)
r)

-- | Run 'SAT' computation.
runSAT :: (forall s. SAT s a) -> IO a
runSAT :: forall a. (forall s. SAT s a) -> IO a
runSAT (SAT Solver -> Lit Any -> IORef (Definitions Any) -> IO a
f) = forall a. (Solver -> IO a) -> IO a
MiniSat.withNewSolverAsync forall a b. (a -> b) -> a -> b
$ \Solver
s -> do
    Lit
t <- Solver -> IO Lit
MiniSat.newLit Solver
s
    forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [forall s. Lit -> Lit s
L Lit
t]
    IORef (Definitions Any)
r <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty
    Solver -> Lit Any -> IORef (Definitions Any) -> IO a
f Solver
s (forall s. Lit -> Lit s
L Lit
t) IORef (Definitions Any)
r

-- | Run 'SAT' computation. Return 'Nothing' if 'UnsatException' is thrown.
runSATMaybe :: (forall s. SAT s a) -> IO (Maybe a)
runSATMaybe :: forall a. (forall s. SAT s a) -> IO (Maybe a)
runSATMaybe forall s. SAT s a
m = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just (forall a. (forall s. SAT s a) -> IO a
runSAT forall s. SAT s a
m) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \UnsatException
UnsatException -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

-------------------------------------------------------------------------------
-- Literals
-------------------------------------------------------------------------------

-- | Literal.
--
-- To negate literate use 'neg'.
newtype Lit s = L { forall s. Lit s -> Lit
unL :: MiniSat.Lit }
  deriving (Lit s -> Lit s -> Bool
forall s. Lit s -> Lit s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lit s -> Lit s -> Bool
$c/= :: forall s. Lit s -> Lit s -> Bool
== :: Lit s -> Lit s -> Bool
$c== :: forall s. Lit s -> Lit s -> Bool
Eq, Lit s -> Lit s -> Bool
Lit s -> Lit s -> Ordering
Lit s -> Lit s -> Lit s
forall s. Eq (Lit s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. Lit s -> Lit s -> Bool
forall s. Lit s -> Lit s -> Ordering
forall s. Lit s -> Lit s -> Lit s
min :: Lit s -> Lit s -> Lit s
$cmin :: forall s. Lit s -> Lit s -> Lit s
max :: Lit s -> Lit s -> Lit s
$cmax :: forall s. Lit s -> Lit s -> Lit s
>= :: Lit s -> Lit s -> Bool
$c>= :: forall s. Lit s -> Lit s -> Bool
> :: Lit s -> Lit s -> Bool
$c> :: forall s. Lit s -> Lit s -> Bool
<= :: Lit s -> Lit s -> Bool
$c<= :: forall s. Lit s -> Lit s -> Bool
< :: Lit s -> Lit s -> Bool
$c< :: forall s. Lit s -> Lit s -> Bool
compare :: Lit s -> Lit s -> Ordering
$ccompare :: forall s. Lit s -> Lit s -> Ordering
Ord)

type role Lit nominal

instance Show (Lit s) where
    showsPrec :: Int -> Lit s -> ShowS
showsPrec Int
d (L (MiniSat.MkLit CInt
l))
        | Bool
p         = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
6) (Char -> ShowS
showChar Char
'-' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows Int
v)
        | Bool
otherwise = forall a. Show a => a -> ShowS
shows Int
v
      where
        i :: Int
        i :: Int
i = forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
l

        -- minisat encodes polarity of literal in 0th bit.
        -- (this way normal order groups same variable literals).
        p :: Bool
        p :: Bool
p = forall a. Bits a => a -> Int -> Bool
testBit Int
i Int
0

        v :: Int
        v :: Int
v = forall a. Bits a => a -> Int -> a
shiftR Int
i Int
1

class Neg a where
    neg :: a -> a

-- | Negate literal.
instance Neg (Lit s) where
   neg :: Lit s -> Lit s
neg (L Lit
l) = forall s. Lit -> Lit s
L (Lit -> Lit
MiniSat.neg Lit
l)

-- | Create fresh literal.
newLit :: SAT s (Lit s)
newLit :: forall s. SAT s (Lit s)
newLit = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
    Lit
l <- Solver -> IO Lit
MiniSat.newLit Solver
s
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall s. Lit -> Lit s
L Lit
l)

-------------------------------------------------------------------------------
-- Prop
-------------------------------------------------------------------------------

-- | Propositional formula.
data Prop s
    = PTrue
    | PFalse
    | P (Prop1 s)
  deriving (Prop s -> Prop s -> Bool
forall s. Prop s -> Prop s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prop s -> Prop s -> Bool
$c/= :: forall s. Prop s -> Prop s -> Bool
== :: Prop s -> Prop s -> Bool
$c== :: forall s. Prop s -> Prop s -> Bool
Eq, Prop s -> Prop s -> Bool
Prop s -> Prop s -> Ordering
forall s. Eq (Prop s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. Prop s -> Prop s -> Bool
forall s. Prop s -> Prop s -> Ordering
forall s. Prop s -> Prop s -> Prop s
min :: Prop s -> Prop s -> Prop s
$cmin :: forall s. Prop s -> Prop s -> Prop s
max :: Prop s -> Prop s -> Prop s
$cmax :: forall s. Prop s -> Prop s -> Prop s
>= :: Prop s -> Prop s -> Bool
$c>= :: forall s. Prop s -> Prop s -> Bool
> :: Prop s -> Prop s -> Bool
$c> :: forall s. Prop s -> Prop s -> Bool
<= :: Prop s -> Prop s -> Bool
$c<= :: forall s. Prop s -> Prop s -> Bool
< :: Prop s -> Prop s -> Bool
$c< :: forall s. Prop s -> Prop s -> Bool
compare :: Prop s -> Prop s -> Ordering
$ccompare :: forall s. Prop s -> Prop s -> Ordering
Ord)

infixr 5 \/
infixr 6 /\

instance Show (Prop s) where
    showsPrec :: Int -> Prop s -> ShowS
showsPrec Int
_ Prop s
PTrue  = String -> ShowS
showString String
"true"
    showsPrec Int
_ Prop s
PFalse = String -> ShowS
showString String
"false"
    showsPrec Int
d (P Prop1 s
p)  = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Prop1 s
p

-- | True 'Prop'.
true :: Prop s
true :: forall s. Prop s
true = forall s. Prop s
PTrue

-- | False 'Prop'.
false :: Prop s
false :: forall s. Prop s
false = forall s. Prop s
PFalse

-- | Make 'Prop' from a literal.
lit :: Lit s -> Prop s
lit :: forall s. Lit s -> Prop s
lit Lit s
l = forall s. Prop1 s -> Prop s
P (forall s. Lit s -> Prop1 s
P1Lit Lit s
l)

-- | Disjunction of propositional formulas, or.
(\/) :: Prop s -> Prop s -> Prop s
Prop s
x \/ :: forall s. Prop s -> Prop s -> Prop s
\/ Prop s
y = forall a. Neg a => a -> a
neg (forall a. Neg a => a -> a
neg Prop s
x forall s. Prop s -> Prop s -> Prop s
/\ forall a. Neg a => a -> a
neg Prop s
y)

-- | Conjunction of propositional formulas, and.
(/\) :: Prop s -> Prop s -> Prop s
Prop s
PFalse /\ :: forall s. Prop s -> Prop s -> Prop s
/\ Prop s
_      = forall s. Prop s
PFalse
Prop s
_      /\ Prop s
PFalse = forall s. Prop s
PFalse
Prop s
PTrue  /\ Prop s
y      = Prop s
y
Prop s
x      /\ Prop s
PTrue  = Prop s
x
P Prop1 s
x    /\ P Prop1 s
y    = forall s. Prop1 s -> Prop s
P (forall s. Prop1 s -> Prop1 s -> Prop1 s
p1and Prop1 s
x Prop1 s
y)

-- | Implication of propositional formulas.
(-->) :: Prop s -> Prop s -> Prop s
Prop s
x --> :: forall s. Prop s -> Prop s -> Prop s
--> Prop s
y = forall a. Neg a => a -> a
neg Prop s
x forall s. Prop s -> Prop s -> Prop s
\/ Prop s
y

-- | Equivalence of propositional formulas.
(<->) :: Prop s -> Prop s -> Prop s
Prop s
x <-> :: forall s. Prop s -> Prop s -> Prop s
<-> Prop s
y = (Prop s
x forall s. Prop s -> Prop s -> Prop s
--> Prop s
y) forall s. Prop s -> Prop s -> Prop s
/\ (Prop s
y forall s. Prop s -> Prop s -> Prop s
--> Prop s
x)

-- | Exclusive or, not equal of propositional formulas.
xor :: Prop s -> Prop s -> Prop s
xor :: forall s. Prop s -> Prop s -> Prop s
xor Prop s
x Prop s
y = Prop s
x forall s. Prop s -> Prop s -> Prop s
<-> forall a. Neg a => a -> a
neg Prop s
y

-- | If-then-else.
--
-- Semantics of @'ite' c t f@ are @ (c '/\' t) '\/' ('neg' c '/\' f)@.
--
ite :: Prop s -> Prop s -> Prop s -> Prop s
-- ite c t f = (c /\ t) \/ (neg c /\ f)
ite :: forall s. Prop s -> Prop s -> Prop s -> Prop s
ite Prop s
c Prop s
t Prop s
f = (Prop s
c forall s. Prop s -> Prop s -> Prop s
\/ Prop s
f) forall s. Prop s -> Prop s -> Prop s
/\ (forall a. Neg a => a -> a
neg Prop s
c forall s. Prop s -> Prop s -> Prop s
\/ Prop s
t) forall s. Prop s -> Prop s -> Prop s
/\ (Prop s
t forall s. Prop s -> Prop s -> Prop s
\/ Prop s
f) -- this encoding makes (t == f) case propagate even when c is yet undecided.

-- | Negation of propositional formulas.
instance Neg (Prop s) where
    neg :: Prop s -> Prop s
neg Prop s
PTrue  = forall s. Prop s
PFalse
    neg Prop s
PFalse = forall s. Prop s
PTrue
    neg (P Prop1 s
p)  = forall s. Prop1 s -> Prop s
P (forall s. Prop1 s -> Prop1 s
p1neg Prop1 s
p)

-------------------------------------------------------------------------------
-- Prop1
-------------------------------------------------------------------------------

data Prop1 s
    = P1Lit !(Lit s)
    | P1Nnd !(Set (PropA s))
    | P1And !(Set (PropA s))
  deriving (Prop1 s -> Prop1 s -> Bool
forall s. Prop1 s -> Prop1 s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prop1 s -> Prop1 s -> Bool
$c/= :: forall s. Prop1 s -> Prop1 s -> Bool
== :: Prop1 s -> Prop1 s -> Bool
$c== :: forall s. Prop1 s -> Prop1 s -> Bool
Eq, Prop1 s -> Prop1 s -> Bool
Prop1 s -> Prop1 s -> Ordering
forall s. Eq (Prop1 s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. Prop1 s -> Prop1 s -> Bool
forall s. Prop1 s -> Prop1 s -> Ordering
forall s. Prop1 s -> Prop1 s -> Prop1 s
min :: Prop1 s -> Prop1 s -> Prop1 s
$cmin :: forall s. Prop1 s -> Prop1 s -> Prop1 s
max :: Prop1 s -> Prop1 s -> Prop1 s
$cmax :: forall s. Prop1 s -> Prop1 s -> Prop1 s
>= :: Prop1 s -> Prop1 s -> Bool
$c>= :: forall s. Prop1 s -> Prop1 s -> Bool
> :: Prop1 s -> Prop1 s -> Bool
$c> :: forall s. Prop1 s -> Prop1 s -> Bool
<= :: Prop1 s -> Prop1 s -> Bool
$c<= :: forall s. Prop1 s -> Prop1 s -> Bool
< :: Prop1 s -> Prop1 s -> Bool
$c< :: forall s. Prop1 s -> Prop1 s -> Bool
compare :: Prop1 s -> Prop1 s -> Ordering
$ccompare :: forall s. Prop1 s -> Prop1 s -> Ordering
Ord)

data PropA s
    = PALit !(Lit s)
    | PANnd !(Set (PropA s))
  deriving (PropA s -> PropA s -> Bool
forall s. PropA s -> PropA s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropA s -> PropA s -> Bool
$c/= :: forall s. PropA s -> PropA s -> Bool
== :: PropA s -> PropA s -> Bool
$c== :: forall s. PropA s -> PropA s -> Bool
Eq, PropA s -> PropA s -> Bool
PropA s -> PropA s -> Ordering
forall s. Eq (PropA s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. PropA s -> PropA s -> Bool
forall s. PropA s -> PropA s -> Ordering
forall s. PropA s -> PropA s -> PropA s
min :: PropA s -> PropA s -> PropA s
$cmin :: forall s. PropA s -> PropA s -> PropA s
max :: PropA s -> PropA s -> PropA s
$cmax :: forall s. PropA s -> PropA s -> PropA s
>= :: PropA s -> PropA s -> Bool
$c>= :: forall s. PropA s -> PropA s -> Bool
> :: PropA s -> PropA s -> Bool
$c> :: forall s. PropA s -> PropA s -> Bool
<= :: PropA s -> PropA s -> Bool
$c<= :: forall s. PropA s -> PropA s -> Bool
< :: PropA s -> PropA s -> Bool
$c< :: forall s. PropA s -> PropA s -> Bool
compare :: PropA s -> PropA s -> Ordering
$ccompare :: forall s. PropA s -> PropA s -> Ordering
Ord)

instance Show (Prop1 s) where
    showsPrec :: Int -> Prop1 s -> ShowS
showsPrec Int
d (P1Lit Lit s
l)  = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Lit s
l
    showsPrec Int
_ (P1And Set (PropA s)
xs) = forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith forall a. Show a => a -> ShowS
shows (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    showsPrec Int
_ (P1Nnd Set (PropA s)
xs) = Char -> ShowS
showChar Char
'-' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith forall a. Show a => a -> ShowS
shows (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)

instance Show (PropA s) where
    showsPrec :: Int -> PropA s -> ShowS
showsPrec Int
d (PALit Lit s
l)  = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Lit s
l
    showsPrec Int
_ (PANnd Set (PropA s)
xs) = Char -> ShowS
showChar Char
'-' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith forall a. Show a => a -> ShowS
shows (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)

showNoCommaListWith :: (a -> ShowS) ->  [a] -> ShowS
showNoCommaListWith :: forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith a -> ShowS
_     []     String
s = String
"[]" forall a. [a] -> [a] -> [a]
++ String
s
showNoCommaListWith a -> ShowS
showx (a
x:[a]
xs) String
s = Char
'[' forall a. a -> [a] -> [a]
: a -> ShowS
showx a
x ([a] -> String
showl [a]
xs)
  where
    showl :: [a] -> String
showl []     = Char
']' forall a. a -> [a] -> [a]
: String
s
    showl (a
y:[a]
ys) = Char
' ' forall a. a -> [a] -> [a]
: a -> ShowS
showx a
y ([a] -> String
showl [a]
ys)

p1and :: Prop1 s -> Prop1 s -> Prop1 s
p1and :: forall s. Prop1 s -> Prop1 s -> Prop1 s
p1and p :: Prop1 s
p@(P1Lit Lit s
x) (P1Lit Lit s
y)
    | Lit s
x forall a. Eq a => a -> a -> Bool
== Lit s
y    = Prop1 s
p
    | Bool
otherwise = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Lit s -> PropA s
PALit Lit s
x) (forall s. Lit s -> PropA s
PALit Lit s
y))
p1and p :: Prop1 s
p@(P1Nnd Set (PropA s)
x) (P1Nnd Set (PropA s)
y)
    | Set (PropA s)
x forall a. Eq a => a -> a -> Bool
== Set (PropA s)
y    = Prop1 s
p
    | Bool
otherwise = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y))
p1and (P1Lit Lit s
x)  (P1Nnd Set (PropA s)
y)  = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Lit s -> PropA s
PALit Lit s
x) (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y))
p1and (P1Nnd Set (PropA s)
x)  (P1Lit Lit s
y)  = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) (forall s. Lit s -> PropA s
PALit Lit s
y))
p1and (P1Lit Lit s
x)  (P1And Set (PropA s)
ys) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Lit s -> PropA s
PALit Lit s
x) Set (PropA s)
ys)
p1and (P1Nnd Set (PropA s)
x)  (P1And Set (PropA s)
ys) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) Set (PropA s)
ys)
p1and (P1And Set (PropA s)
xs) (P1Lit Lit s
y)  = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Lit s -> PropA s
PALit Lit s
y) Set (PropA s)
xs)
p1and (P1And Set (PropA s)
xs) (P1Nnd Set (PropA s)
y)  = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y) Set (PropA s)
xs)
p1and (P1And Set (PropA s)
xs) (P1And Set (PropA s)
ys) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (PropA s)
xs Set (PropA s)
ys)

p1neg :: Prop1 s -> Prop1 s
p1neg :: forall s. Prop1 s -> Prop1 s
p1neg (P1Lit Lit s
l)  = forall s. Lit s -> Prop1 s
P1Lit (forall a. Neg a => a -> a
neg Lit s
l)
p1neg (P1Nnd Set (PropA s)
xs) = forall s. Set (PropA s) -> Prop1 s
P1And Set (PropA s)
xs
p1neg (P1And Set (PropA s)
xs) = forall s. Set (PropA s) -> Prop1 s
P1Nnd Set (PropA s)
xs

double :: Ord a => a -> a -> Set a
double :: forall a. Ord a => a -> a -> Set a
double a
x a
y = forall a. Ord a => a -> Set a -> Set a
Set.insert a
x (forall a. a -> Set a
Set.singleton a
y)

-------------------------------------------------------------------------------
-- Clause definitions
-------------------------------------------------------------------------------

-- | Add conjunction definition.
--
-- @addConjDefinition x ys@ asserts that @x ↔ ⋀ yᵢ@
addConjDefinition :: Lit s -> [Lit s] -> SAT s ()
addConjDefinition :: forall s. Lit s -> [Lit s] -> SAT s ()
addConjDefinition Lit s
x [Lit s]
zs = do
    Lit s
y <- forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
zs)
    if Lit s
x forall a. Eq a => a -> a -> Bool
== Lit s
y
    then forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else forall s. Lit s -> Lit s -> SAT s ()
assertEqual Lit s
x Lit s
y

-- | Add disjunction definition.
--
-- @addDisjDefinition x ys@ asserts that @x ↔ ⋁ yᵢ@
--
addDisjDefinition :: Lit s -> [Lit s] -> SAT s ()
addDisjDefinition :: forall s. Lit s -> [Lit s] -> SAT s ()
addDisjDefinition Lit s
x [Lit s]
ys = forall s. Lit s -> [Lit s] -> SAT s ()
addConjDefinition (forall a. Neg a => a -> a
neg Lit s
x) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Neg a => a -> a
neg [Lit s]
ys)
-- Implementation: @(x ↔ ⋁ yᵢ) ↔ (¬x ↔ ⋀ ¬xyᵢ)@

-------------------------------------------------------------------------------
-- Methods
-------------------------------------------------------------------------------

-- | Assert that given 'Prop' is true.
--
-- This is equivalent to
--
-- @
-- addProp p = do
--     l <- addDefinition p
--     addClause l
-- @
--
-- but avoid creating the definition, asserting less clauses.
--
addProp :: Prop s -> SAT s ()
addProp :: forall s. Prop s -> SAT s ()
addProp Prop s
PTrue  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
addProp Prop s
PFalse = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
t IORef (Definitions s)
_ -> forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [forall a. Neg a => a -> a
neg Lit s
t]
addProp (P Prop1 s
p)  = forall s. Prop1 s -> SAT s ()
add_prop Prop1 s
p

-- | Add definition of 'Prop'. The resulting literal is equivalent to the argument 'Prop'.
--
addDefinition :: Prop s -> SAT s (Lit s)
addDefinition :: forall s. Prop s -> SAT s (Lit s)
addDefinition Prop s
PTrue  = forall s. SAT s (Lit s)
trueLit
addDefinition Prop s
PFalse = forall s. SAT s (Lit s)
falseLit
addDefinition (P Prop1 s
p)  = forall s. Prop1 s -> SAT s (Lit s)
addDefinition1 Prop1 s
p

-- | True literal.
trueLit :: SAT s (Lit s)
trueLit :: forall s. SAT s (Lit s)
trueLit = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
_s Lit s
t IORef (Definitions s)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
t

-- | False literal
falseLit :: SAT s (Lit s)
falseLit :: forall s. SAT s (Lit s)
falseLit = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
_s Lit s
t IORef (Definitions s)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Neg a => a -> a
neg Lit s
t)

addDefinition1 :: Prop1 s -> SAT s (Lit s)
addDefinition1 :: forall s. Prop1 s -> SAT s (Lit s)
addDefinition1 = forall s. Prop1 s -> SAT s (Lit s)
tseitin1

-- | Add conjuctive definition.
add_definition :: Set (Lit s) -> SAT s (Lit s)
add_definition :: forall s. Set (Lit s) -> SAT s (Lit s)
add_definition Set (Lit s)
ps
    | forall a. Set a -> Bool
Set.null Set (Lit s)
ps
    = forall s. SAT s (Lit s)
trueLit

add_definition Set (Lit s)
ps = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_ IORef (Definitions s)
defsRef -> do
    Definitions s
defs <- forall a. IORef a -> IO a
readIORef IORef (Definitions s)
defsRef
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Set (Lit s)
ps Definitions s
defs of
        Just Lit s
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
d
        Maybe (Lit s)
Nothing -> do
            Lit
d' <- Solver -> IO Lit
MiniSat.newLit Solver
s
            let d :: Lit s
d = forall s. Lit -> Lit s
L Lit
d'

            -- putStrLn $ "add_definition " ++ show (Set.toList ps) ++ " = " ++ show d

            -- d ∨ ¬x₁ ∨ ¬x₂ ∨ ... ∨ ¬xₙ
            forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s forall a b. (a -> b) -> a -> b
$ Lit s
d forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Neg a => a -> a
neg (forall a. Set a -> [a]
Set.toList Set (Lit s)
ps)

            -- ¬d ∨ x₁
            -- ¬d ∨ x₂
            --  ...
            -- ¬d ∨ xₙ
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set (Lit s)
ps forall a b. (a -> b) -> a -> b
$ \Lit s
p -> do
                forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [forall a. Neg a => a -> a
neg Lit s
d, Lit s
p]

            -- save the definition.
            forall a. IORef a -> a -> IO ()
writeIORef IORef (Definitions s)
defsRef forall a b. (a -> b) -> a -> b
$! forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Set (Lit s)
ps Lit s
d Definitions s
defs

            forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
d

-- top-level add prop: CNF
add_prop :: Prop1 s  -> SAT s ()
add_prop :: forall s. Prop1 s -> SAT s ()
add_prop (P1Lit Lit s
l) = forall s. [Lit s] -> SAT s ()
addClause [Lit s
l]
add_prop (P1And Set (PropA s)
xs) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set (PropA s)
xs forall s. PropA s -> SAT s ()
add_prop'
add_prop (P1Nnd Set (PropA s)
xs) = do
    [Lit s]
ls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    forall s. [Lit s] -> SAT s ()
addClause (forall a b. (a -> b) -> [a] -> [b]
map forall a. Neg a => a -> a
neg [Lit s]
ls)

-- first-level: Clauses
add_prop' :: PropA s -> SAT s ()
add_prop' :: forall s. PropA s -> SAT s ()
add_prop' (PALit Lit s
l) = forall s. [Lit s] -> SAT s ()
addClause [Lit s
l]
add_prop' (PANnd Set (PropA s)
xs) = do
    [Lit s]
ls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    forall s. [Lit s] -> SAT s ()
addClause (forall a b. (a -> b) -> [a] -> [b]
map forall a. Neg a => a -> a
neg [Lit s]
ls)

tseitin1 :: Prop1 s -> SAT s (Lit s)
tseitin1 :: forall s. Prop1 s -> SAT s (Lit s)
tseitin1 (P1Lit Lit s
l) = forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
l
tseitin1 (P1And Set (PropA s)
xs) = do
    [Lit s]
xs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
xs')
tseitin1 (P1Nnd Set (PropA s)
xs) = do
    [Lit s]
xs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    forall a. Neg a => a -> a
neg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
xs')

tseitinA :: PropA s -> SAT s (Lit s)
tseitinA :: forall s. PropA s -> SAT s (Lit s)
tseitinA (PALit Lit s
l) = forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
l
tseitinA (PANnd Set (PropA s)
xs) = do
    [Lit s]
xs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    forall a. Neg a => a -> a
neg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
xs')

-------------------------------------------------------------------------------
-- Constraints
-------------------------------------------------------------------------------

-- | Add a clause to the solver.
addClause :: [Lit s] -> SAT s ()
addClause :: forall s. [Lit s] -> SAT s ()
addClause [Lit s]
ls = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [Lit s]
ls

add_clause :: MiniSat.Solver -> [Lit s] -> IO ()
add_clause :: forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [Lit s]
ls = do
    -- putStrLn $ "add_clause " ++ show ls
    Bool
ok <- Solver -> [Lit] -> IO Bool
MiniSat.addClause Solver
s (forall a b. (a -> b) -> [a] -> [b]
map forall s. Lit s -> Lit
unL [Lit s]
ls)
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException

-- | At least one -constraint.
--
-- Alias to 'addClause'.
assertAtLeastOne :: [Lit s] -> SAT s ()
assertAtLeastOne :: forall s. [Lit s] -> SAT s ()
assertAtLeastOne = forall s. [Lit s] -> SAT s ()
addClause

-- | At most one -constraint.
--
-- Uses 'atMostOnePairwise' for lists of length 2 to 5
-- and 'atMostOneSequential' for longer lists.
--
-- The cutoff is chosen by picking encoding with least clauses:
-- For 5 literals, 'atMostOnePairwise' needs 10 clauses and 'assertAtMostOneSequential' needs 11 (and 4 new variables).
-- For 6 literals, 'atMostOnePairwise' needs 15 clauses and 'assertAtMostOneSequential' needs 14.
--
assertAtMostOne :: [Lit s] -> SAT s ()
assertAtMostOne :: forall s. [Lit s] -> SAT s ()
assertAtMostOne [Lit s]
ls = case [Lit s]
ls of
    []          -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [Lit s
_]         -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [Lit s
_,Lit s
_]       -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s
_,Lit s
_,Lit s
_]     -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s
_,Lit s
_,Lit s
_,Lit s
_]   -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s
_,Lit s
_,Lit s
_,Lit s
_,Lit s
_] -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s]
_           -> forall s. [Lit s] -> SAT s ()
assertAtMostOneSequential [Lit s]
ls

-- | At most one -constraint using pairwise encoding.
--
-- \[
-- \mathrm{AMO}(x_1, \ldots, x_n) = \bigwedge_{1 \le i < j \le n} \neg x_i \lor \neg x_j
-- \]
--
-- \(n(n-1)/2\) clauses, zero auxiliary variables.
--
assertAtMostOnePairwise :: [Lit s] -> SAT s ()
assertAtMostOnePairwise :: forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
literals = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall s. [Lit s] -> SAT s ()
f (forall a. [a] -> [[a]]
tails [Lit s]
literals) where
    f :: [Lit s] -> SAT s ()
    f :: forall s. [Lit s] -> SAT s ()
f [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    f (Lit s
l:[Lit s]
ls) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall s. Lit s -> Lit s -> SAT s ()
g Lit s
l) [Lit s]
ls

    g :: Lit s -> Lit s -> SAT s ()
    g :: forall s. Lit s -> Lit s -> SAT s ()
g Lit s
l1 Lit s
l2 = forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
l1, forall a. Neg a => a -> a
neg Lit s
l2]

-- | At most one -constraint using sequential counter encoding.
--
-- \[
-- \mathrm{AMO}(x_1, \ldots, x_n) =
--  (\neg x_1 \lor s_1) \land
--  (\neg x_n \lor \neg s_{n-1}) \land
--  \bigwedge_{1 < i < n} (\neg x_i \lor a_i) \land (\neg a_{i-1} \lor a_i) \land (\neg x_i \lor \neg a_{i-1})
-- \]
--
-- Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints, Proceedings of Principles and Practice of Constraint Programming (CP), 827–831 (2005)
--
-- \(3n-4\) clauses, \(n-1\) auxiliary variables.
--
-- We optimize the two literal case immediately ([resolution](https://en.wikipedia.org/wiki/Resolution_(logic)) on \(s_1\).
--
-- \[
-- (\neg x_1 \lor s_1) \land (\neg x_2 \lor \neg s_1) \Longrightarrow \neg x_1 \lor \neg x_2
-- \]
--
assertAtMostOneSequential :: [Lit s] -> SAT s ()
assertAtMostOneSequential :: forall s. [Lit s] -> SAT s ()
assertAtMostOneSequential []         = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAtMostOneSequential [Lit s
_]        = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAtMostOneSequential [Lit s
x1,Lit s
x2]    = forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
x1, forall a. Neg a => a -> a
neg Lit s
x2]
assertAtMostOneSequential (Lit s
xn:Lit s
x1:[Lit s]
xs) = do
    Lit s
a1 <- forall s. SAT s (Lit s)
newLit
    forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
x1, Lit s
a1]
    Lit s -> [Lit s] -> SAT s ()
go Lit s
a1 [Lit s]
xs
  where
     go :: Lit s -> [Lit s] -> SAT s ()
go Lit s
an1 [] = forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
xn, forall a. Neg a => a -> a
neg Lit s
an1]
     go Lit s
ai1 (Lit s
xi:[Lit s]
xis) = do
        Lit s
ai <- forall s. SAT s (Lit s)
newLit
        forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
xi, Lit s
ai]
        forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
ai1, Lit s
ai]
        forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
xi, forall a. Neg a => a -> a
neg Lit s
ai1]
        Lit s -> [Lit s] -> SAT s ()
go Lit s
ai [Lit s]
xis

-- | Assert that two literals are equal.
assertEqual :: Lit s -> Lit s -> SAT s ()
assertEqual :: forall s. Lit s -> Lit s -> SAT s ()
assertEqual Lit s
l Lit s
l'
    | Lit s
l forall a. Eq a => a -> a -> Bool
== Lit s
l'   = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise = do
        forall s. [Lit s] -> SAT s ()
addClause [Lit s
l, forall a. Neg a => a -> a
neg Lit s
l']
        forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
l, Lit s
l']

-- | Assert that all literals in the list are equal.
assertAllEqual :: [Lit s] -> SAT s ()
assertAllEqual :: forall s. [Lit s] -> SAT s ()
assertAllEqual []     = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAllEqual (Lit s
l:[Lit s]
ls) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
ls) forall a b. (a -> b) -> a -> b
$ \Lit s
l' -> forall s. Lit s -> Lit s -> SAT s ()
assertEqual Lit s
l Lit s
l'

-------------------------------------------------------------------------------
-- Solving
-------------------------------------------------------------------------------

-- | Search without returning a model.
solve_ :: SAT s ()
solve_ :: forall s. SAT s ()
solve_ = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
    Bool
ok <- Solver -> [Lit] -> IO Bool
MiniSat.solve Solver
s []
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException

-- | Search and return a model.
solve :: Traversable model => model (Lit s) -> SAT s (model Bool)
solve :: forall (model :: * -> *) s.
Traversable model =>
model (Lit s) -> SAT s (model Bool)
solve model (Lit s)
model = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
    Bool
ok <- Solver -> [Lit] -> IO Bool
MiniSat.solve Solver
s []
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException

    forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall s. Solver -> Lit s -> IO Bool
getSym Solver
s) model (Lit s)
model
  where
    getSym :: MiniSat.Solver -> Lit s -> IO Bool
    getSym :: forall s. Solver -> Lit s -> IO Bool
getSym Solver
s (L Lit
l) = do
        Maybe Bool
b <- Solver -> Lit -> IO (Maybe Bool)
MiniSat.modelValue Solver
s Lit
l
        case Maybe Bool
b of
            Maybe Bool
Nothing -> forall e a. Exception e => e -> IO a
throwIO SATPanic
SATPanic
            Just Bool
b' -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b'

-------------------------------------------------------------------------------
-- Simplification
-------------------------------------------------------------------------------

-- | Removes already satisfied clauses.
simplify :: SAT s ()
simplify :: forall s. SAT s ()
simplify = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
    Bool
ok <- Solver -> IO Bool
MiniSat.simplify Solver
s
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException

-------------------------------------------------------------------------------
-- Statistics
-------------------------------------------------------------------------------

-- | The current number of variables.
numberOfVariables :: SAT s Int
numberOfVariables :: forall s. SAT s Int
numberOfVariables = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_vars Solver
s

-- | The current number of original clauses.
numberOfClauses :: SAT s Int
numberOfClauses :: forall s. SAT s Int
numberOfClauses = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_clauses Solver
s

-- | The current number of learnt clauses.
numberOfLearnts :: SAT s Int
numberOfLearnts :: forall s. SAT s Int
numberOfLearnts = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_learnts Solver
s

-- | The current number of conflicts.
numberOfConflicts :: SAT s Int
numberOfConflicts :: forall s. SAT s Int
numberOfConflicts = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_conflicts Solver
s