{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE MagicHash           #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RoleAnnotations     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnboxedTuples       #-}
-- | A monadic interface to the SAT (@PureSAT@) 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,
    runSATMaybe,
    -- * Literals
    Lit,
    newLit,
    boostScore,
    -- ** 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,
    numberOfLearntLiterals,
    numberOfConflicts,
    numberOfRestarts,
) where

import Control.Monad   (forM_, unless)
import Data.Bits       (shiftR, testBit)
import Data.List       (tails)
import Data.Map.Strict (Map)
import Data.Set        (Set)
import Data.STRef      (STRef, newSTRef, readSTRef, writeSTRef)

import EST

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

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

-- | Satisfiability monad.
newtype SAT s a = SAT { forall s a.
SAT s a
-> Solver s
-> Lit s
-> STRef s (Definitions s)
-> EST UnsatException s a
unSAT :: PureSAT.Solver s -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a }
  deriving (forall a b. (a -> b) -> SAT s a -> SAT s b)
-> (forall a b. a -> SAT s b -> SAT s a) -> Functor (SAT s)
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
$cfmap :: forall s a b. (a -> b) -> SAT s a -> SAT s b
fmap :: forall a b. (a -> b) -> SAT s a -> SAT s b
$c<$ :: forall s a b. a -> SAT s b -> SAT s a
<$ :: forall a b. a -> SAT s b -> SAT s a
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

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
(Int -> UnsatException -> ShowS)
-> (UnsatException -> String)
-> ([UnsatException] -> ShowS)
-> Show UnsatException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnsatException -> ShowS
showsPrec :: Int -> UnsatException -> ShowS
$cshow :: UnsatException -> String
show :: UnsatException -> String
$cshowList :: [UnsatException] -> ShowS
showList :: [UnsatException] -> ShowS
Show)

throwUnsatException :: EST UnsatException s a
throwUnsatException :: forall s a. EST UnsatException s a
throwUnsatException = UnsatException -> EST UnsatException s a
forall e s any. e -> EST e s any
earlyExitEST UnsatException
UnsatException

instance Applicative (SAT s) where
    pure :: forall a. a -> SAT s a
pure a
x = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT (\Solver s
_ Lit s
_ STRef s (Definitions s)
_ -> a -> EST UnsatException s a
forall a. a -> EST UnsatException s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
    SAT Solver s
-> Lit s
-> STRef s (Definitions s)
-> EST UnsatException s (a -> b)
f <*> :: forall a b. SAT s (a -> b) -> SAT s a -> SAT s b
<*> SAT Solver s
-> Lit s -> STRef s (Definitions s) -> EST UnsatException s a
x = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s b)
-> SAT s b
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT (\Solver s
s Lit s
t STRef s (Definitions s)
r -> Solver s
-> Lit s
-> STRef s (Definitions s)
-> EST UnsatException s (a -> b)
f Solver s
s Lit s
t STRef s (Definitions s)
r EST UnsatException s (a -> b)
-> EST UnsatException s a -> EST UnsatException s b
forall a b.
EST UnsatException s (a -> b)
-> EST UnsatException s a -> EST UnsatException s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solver s
-> Lit s -> STRef s (Definitions s) -> EST UnsatException s a
x Solver s
s Lit s
t STRef s (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 = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s b)
-> SAT s b
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s b)
 -> SAT s b)
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s b)
-> SAT s b
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
t STRef s (Definitions s)
r -> do
        x <- SAT s a
-> Solver s
-> Lit s
-> STRef s (Definitions s)
-> EST UnsatException s a
forall s a.
SAT s a
-> Solver s
-> Lit s
-> STRef s (Definitions s)
-> EST UnsatException s a
unSAT SAT s a
m Solver s
s Lit s
t STRef s (Definitions s)
r
        unSAT (k x) s t r

-- | Run 'SAT' computation.
runSATMaybe :: forall a. (forall s. SAT s a) -> Maybe a
runSATMaybe :: forall a. (forall s. SAT s a) -> Maybe a
runSATMaybe forall s. SAT s a
f = (UnsatException -> Maybe a)
-> (a -> Maybe a) -> Either UnsatException a -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe a -> UnsatException -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) a -> Maybe a
forall a. a -> Maybe a
Just (Either UnsatException a -> Maybe a)
-> Either UnsatException a -> Maybe a
forall a b. (a -> b) -> a -> b
$ (forall s. EST UnsatException s a) -> Either UnsatException a
forall e a. (forall s. EST e s a) -> Either e a
runEST ((forall s. EST UnsatException s a) -> Either UnsatException a)
-> (forall s. EST UnsatException s a) -> Either UnsatException a
forall a b. (a -> b) -> a -> b
$ do
    s <- ST s (Solver s) -> EST UnsatException s (Solver s)
forall s a e. ST s a -> EST e s a
liftST ST s (Solver s)
forall s. ST s (Solver s)
PureSAT.newSolver
    t <- liftST (PureSAT.newLit s)
    add_clause s [L t]
    r <- liftST (newSTRef Map.empty)
    unSAT f s (L t) r

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

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

type role Lit nominal

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

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

        v :: Int
        v :: Int
v = Int -> Int -> Int
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) = Lit -> Lit s
forall s. Lit -> Lit s
L (Lit -> Lit
PureSAT.neg Lit
l)

-- | Create fresh literal.
newLit :: SAT s (Lit s)
newLit :: forall s. SAT s (Lit s)
newLit = (Solver s
 -> Lit s
 -> STRef s (Definitions s)
 -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s
  -> STRef s (Definitions s)
  -> EST UnsatException s (Lit s))
 -> SAT s (Lit s))
-> (Solver s
    -> Lit s
    -> STRef s (Definitions s)
    -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> do
    l <- ST s Lit -> EST UnsatException s Lit
forall s a e. ST s a -> EST e s a
liftST (Solver s -> ST s Lit
forall s. Solver s -> ST s Lit
PureSAT.newLit Solver s
s)
    return (L l)

-- | Boost score of the literal
boostScore :: Lit s -> SAT s ()
boostScore :: forall s. Lit s -> SAT s ()
boostScore (L Lit
l) = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
 -> SAT s ())
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> ST s () -> EST UnsatException s ()
forall s a e. ST s a -> EST e s a
liftST (Solver s -> Lit -> ST s ()
forall s. Solver s -> Lit -> ST s ()
PureSAT.boostScore Solver s
s Lit
l)

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

-- | Propositional formula.
data Prop s
    = PTrue
    | PFalse
    | P (Prop1 s)
  deriving (Prop s -> Prop s -> Bool
(Prop s -> Prop s -> Bool)
-> (Prop s -> Prop s -> Bool) -> Eq (Prop s)
forall s. Prop s -> Prop s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
Eq, Eq (Prop s)
Eq (Prop s) =>
(Prop s -> Prop s -> Ordering)
-> (Prop s -> Prop s -> Bool)
-> (Prop s -> Prop s -> Bool)
-> (Prop s -> Prop s -> Bool)
-> (Prop s -> Prop s -> Bool)
-> (Prop s -> Prop s -> Prop s)
-> (Prop s -> Prop s -> Prop s)
-> Ord (Prop s)
Prop s -> Prop s -> Bool
Prop s -> Prop s -> Ordering
Prop s -> Prop s -> Prop s
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
$ccompare :: forall s. Prop s -> Prop s -> Ordering
compare :: Prop s -> Prop s -> Ordering
$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
>= :: Prop s -> Prop s -> Bool
$cmax :: forall s. Prop s -> Prop s -> Prop s
max :: Prop s -> Prop s -> Prop s
$cmin :: forall s. Prop s -> Prop s -> Prop s
min :: Prop s -> Prop s -> Prop s
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)  = Int -> Prop1 s -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Prop1 s
p

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

-- | False 'Prop'.
false :: Prop s
false :: forall s. Prop s
false = Prop s
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 = Prop1 s -> Prop s
forall s. Prop1 s -> Prop s
P (Lit s -> Prop1 s
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 = Prop s -> Prop s
forall a. Neg a => a -> a
neg (Prop s -> Prop s
forall a. Neg a => a -> a
neg Prop s
x Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop 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
_      = Prop s
forall s. Prop s
PFalse
Prop s
_      /\ Prop s
PFalse = Prop s
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    = Prop1 s -> Prop s
forall s. Prop1 s -> Prop s
P (Prop1 s -> Prop1 s -> Prop1 s
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 = Prop s -> Prop s
forall a. Neg a => a -> a
neg Prop s
x Prop s -> Prop s -> Prop s
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 Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
--> Prop s
y) Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
/\ (Prop s
y Prop s -> Prop s -> Prop s
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 Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop 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 Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
\/ Prop s
f) Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
/\ (Prop s -> Prop s
forall a. Neg a => a -> a
neg Prop s
c Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
\/ Prop s
t) Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
/\ (Prop s
t Prop s -> Prop s -> Prop s
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  = Prop s
forall s. Prop s
PFalse
    neg Prop s
PFalse = Prop s
forall s. Prop s
PTrue
    neg (P Prop1 s
p)  = Prop1 s -> Prop s
forall s. Prop1 s -> Prop s
P (Prop1 s -> Prop1 s
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
(Prop1 s -> Prop1 s -> Bool)
-> (Prop1 s -> Prop1 s -> Bool) -> Eq (Prop1 s)
forall s. Prop1 s -> Prop1 s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
Eq, Eq (Prop1 s)
Eq (Prop1 s) =>
(Prop1 s -> Prop1 s -> Ordering)
-> (Prop1 s -> Prop1 s -> Bool)
-> (Prop1 s -> Prop1 s -> Bool)
-> (Prop1 s -> Prop1 s -> Bool)
-> (Prop1 s -> Prop1 s -> Bool)
-> (Prop1 s -> Prop1 s -> Prop1 s)
-> (Prop1 s -> Prop1 s -> Prop1 s)
-> Ord (Prop1 s)
Prop1 s -> Prop1 s -> Bool
Prop1 s -> Prop1 s -> Ordering
Prop1 s -> Prop1 s -> Prop1 s
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
$ccompare :: forall s. Prop1 s -> Prop1 s -> Ordering
compare :: Prop1 s -> Prop1 s -> Ordering
$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
>= :: Prop1 s -> Prop1 s -> Bool
$cmax :: forall s. Prop1 s -> Prop1 s -> Prop1 s
max :: Prop1 s -> Prop1 s -> Prop1 s
$cmin :: forall s. Prop1 s -> Prop1 s -> Prop1 s
min :: Prop1 s -> Prop1 s -> Prop1 s
Ord)

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

instance Show (Prop1 s) where
    showsPrec :: Int -> Prop1 s -> ShowS
showsPrec Int
d (P1Lit Lit s
l)  = Int -> Lit s -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Lit s
l
    showsPrec Int
_ (P1And Set (PropA s)
xs) = (PropA s -> ShowS) -> [PropA s] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith PropA s -> ShowS
forall a. Show a => a -> ShowS
shows (Set (PropA s) -> [PropA s]
forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    showsPrec Int
_ (P1Nnd Set (PropA s)
xs) = Char -> ShowS
showChar Char
'-' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PropA s -> ShowS) -> [PropA s] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith PropA s -> ShowS
forall a. Show a => a -> ShowS
shows (Set (PropA s) -> [PropA s]
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)  = Int -> Lit s -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Lit s
l
    showsPrec Int
_ (PANnd Set (PropA s)
xs) = Char -> ShowS
showChar Char
'-' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PropA s -> ShowS) -> [PropA s] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith PropA s -> ShowS
forall a. Show a => a -> ShowS
shows (Set (PropA s) -> [PropA s]
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
"[]" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
showNoCommaListWith a -> ShowS
showx (a
x:[a]
xs) String
s = Char
'[' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> ShowS
showx a
x ([a] -> String
showl [a]
xs)
  where
    showl :: [a] -> String
showl []     = Char
']' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s
    showl (a
y:[a]
ys) = Char
' ' Char -> ShowS
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 Lit s -> Lit s -> Bool
forall a. Eq a => a -> a -> Bool
== Lit s
y    = Prop1 s
p
    | Bool
otherwise = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> PropA s -> Set (PropA s)
forall a. Ord a => a -> a -> Set a
double (Lit s -> PropA s
forall s. Lit s -> PropA s
PALit Lit s
x) (Lit s -> PropA s
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 Set (PropA s) -> Set (PropA s) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (PropA s)
y    = Prop1 s
p
    | Bool
otherwise = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> PropA s -> Set (PropA s)
forall a. Ord a => a -> a -> Set a
double (Set (PropA s) -> PropA s
forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) (Set (PropA s) -> PropA s
forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y))
p1and (P1Lit Lit s
x)  (P1Nnd Set (PropA s)
y)  = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> PropA s -> Set (PropA s)
forall a. Ord a => a -> a -> Set a
double (Lit s -> PropA s
forall s. Lit s -> PropA s
PALit Lit s
x) (Set (PropA s) -> PropA s
forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y))
p1and (P1Nnd Set (PropA s)
x)  (P1Lit Lit s
y)  = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> PropA s -> Set (PropA s)
forall a. Ord a => a -> a -> Set a
double (Set (PropA s) -> PropA s
forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) (Lit s -> PropA s
forall s. Lit s -> PropA s
PALit Lit s
y))
p1and (P1Lit Lit s
x)  (P1And Set (PropA s)
ys) = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> Set (PropA s) -> Set (PropA s)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Lit s -> PropA s
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) = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> Set (PropA s) -> Set (PropA s)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Set (PropA s) -> PropA s
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)  = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> Set (PropA s) -> Set (PropA s)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Lit s -> PropA s
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)  = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (PropA s -> Set (PropA s) -> Set (PropA s)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Set (PropA s) -> PropA s
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) = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And (Set (PropA s) -> Set (PropA s) -> Set (PropA s)
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)  = Lit s -> Prop1 s
forall s. Lit s -> Prop1 s
P1Lit (Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
l)
p1neg (P1Nnd Set (PropA s)
xs) = Set (PropA s) -> Prop1 s
forall s. Set (PropA s) -> Prop1 s
P1And Set (PropA s)
xs
p1neg (P1And Set (PropA s)
xs) = Set (PropA s) -> Prop1 s
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 = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x (a -> Set a
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
    y <- Set (Lit s) -> SAT s (Lit s)
forall s. Set (Lit s) -> SAT s (Lit s)
add_definition ([Lit s] -> Set (Lit s)
forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
zs)
    if x == y
    then return ()
    else assertEqual x 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 = Lit s -> [Lit s] -> SAT s ()
forall s. Lit s -> [Lit s] -> SAT s ()
addConjDefinition (Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
x) ((Lit s -> Lit s) -> [Lit s] -> [Lit s]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Lit s -> Lit s
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  = () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
addProp Prop s
PFalse = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
 -> SAT s ())
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
t STRef s (Definitions s)
_-> Solver s -> [Lit s] -> EST UnsatException s ()
forall s. Solver s -> [Lit s] -> EST UnsatException s ()
add_clause Solver s
s [Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
t]
addProp (P Prop1 s
p)  = Prop1 s -> SAT s ()
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  = SAT s (Lit s)
forall s. SAT s (Lit s)
trueLit
addDefinition Prop s
PFalse = SAT s (Lit s)
forall s. SAT s (Lit s)
falseLit
addDefinition (P Prop1 s
p)  = Prop1 s -> SAT s (Lit s)
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 = (Solver s
 -> Lit s
 -> STRef s (Definitions s)
 -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s
  -> STRef s (Definitions s)
  -> EST UnsatException s (Lit s))
 -> SAT s (Lit s))
-> (Solver s
    -> Lit s
    -> STRef s (Definitions s)
    -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall a b. (a -> b) -> a -> b
$ \Solver s
_s Lit s
t STRef s (Definitions s)
_ -> Lit s -> EST UnsatException s (Lit s)
forall a. a -> EST UnsatException s a
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 = (Solver s
 -> Lit s
 -> STRef s (Definitions s)
 -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s
  -> STRef s (Definitions s)
  -> EST UnsatException s (Lit s))
 -> SAT s (Lit s))
-> (Solver s
    -> Lit s
    -> STRef s (Definitions s)
    -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall a b. (a -> b) -> a -> b
$ \Solver s
_s Lit s
t STRef s (Definitions s)
_ -> Lit s -> EST UnsatException s (Lit s)
forall a. a -> EST UnsatException s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit s -> Lit s
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 = Prop1 s -> SAT s (Lit s)
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
    | Set (Lit s) -> Bool
forall a. Set a -> Bool
Set.null Set (Lit s)
ps
    = SAT s (Lit s)
forall s. SAT s (Lit s)
trueLit

add_definition Set (Lit s)
ps = (Solver s
 -> Lit s
 -> STRef s (Definitions s)
 -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s
  -> STRef s (Definitions s)
  -> EST UnsatException s (Lit s))
 -> SAT s (Lit s))
-> (Solver s
    -> Lit s
    -> STRef s (Definitions s)
    -> EST UnsatException s (Lit s))
-> SAT s (Lit s)
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_ STRef s (Definitions s)
defsRef -> do
    defs <- ST s (Definitions s) -> EST UnsatException s (Definitions s)
forall s a e. ST s a -> EST e s a
liftST (STRef s (Definitions s) -> ST s (Definitions s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Definitions s)
defsRef)
    case Map.lookup ps defs of
        Just Lit s
d -> Lit s -> EST UnsatException s (Lit s)
forall a. a -> EST UnsatException s a
forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
d
        Maybe (Lit s)
Nothing -> do
            d' <- ST s Lit -> EST UnsatException s Lit
forall s a e. ST s a -> EST e s a
liftST (Solver s -> ST s Lit
forall s. Solver s -> ST s Lit
PureSAT.newLit Solver s
s)
            let d = Lit -> Lit s
forall s. Lit -> Lit s
L Lit
d'

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

            -- d ∨ ¬x₁ ∨ ¬x₂ ∨ ... ∨ ¬xₙ
            add_clause s (d : map neg (Set.toList ps))

            -- ¬d ∨ x₁
            -- ¬d ∨ x₂
            --  ...
            -- ¬d ∨ xₙ
            forM_ ps $ \Lit s
p -> do
                Solver s -> [Lit s] -> EST UnsatException s ()
forall s. Solver s -> [Lit s] -> EST UnsatException s ()
add_clause Solver s
s [Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
d, Lit s
p]

            -- save the definition.
            liftST (writeSTRef defsRef $! Map.insert ps d defs)

            return 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) = [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
addClause [Lit s
l]
add_prop (P1And Set (PropA s)
xs) = Set (PropA s) -> (PropA s -> SAT s ()) -> SAT s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set (PropA s)
xs PropA s -> SAT s ()
forall s. PropA s -> SAT s ()
add_prop'
add_prop (P1Nnd Set (PropA s)
xs) = do
    ls <- (PropA s -> SAT s (Lit s)) -> [PropA s] -> SAT s [Lit s]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse PropA s -> SAT s (Lit s)
forall s. PropA s -> SAT s (Lit s)
tseitinA (Set (PropA s) -> [PropA s]
forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
    addClause (map neg ls)

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

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

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

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

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

add_clause :: PureSAT.Solver s -> [Lit s] -> EST UnsatException s ()
add_clause :: forall s. Solver s -> [Lit s] -> EST UnsatException s ()
add_clause Solver s
s [Lit s]
ls = do
    -- putStrLn $ "add_clause " ++ show ls
    ok <- ST s Bool -> EST UnsatException s Bool
forall s a e. ST s a -> EST e s a
liftST (Solver s -> [Lit] -> ST s Bool
forall s. Solver s -> [Lit] -> ST s Bool
PureSAT.addClause Solver s
s ((Lit s -> Lit) -> [Lit s] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map Lit s -> Lit
forall s. Lit s -> Lit
unL [Lit s]
ls))
    unless ok throwUnsatException

-- | At least one -constraint.
--
-- Alias to 'addClause'.
assertAtLeastOne :: [Lit s] -> SAT s ()
assertAtLeastOne :: forall s. [Lit s] -> SAT s ()
assertAtLeastOne = [Lit s] -> SAT s ()
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
    []          -> () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [Lit s
_]         -> () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [Lit s
_,Lit s
_]       -> [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s
_,Lit s
_,Lit s
_]     -> [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s
_,Lit s
_,Lit s
_,Lit s
_]   -> [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s
_,Lit s
_,Lit s
_,Lit s
_,Lit s
_] -> [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
    [Lit s]
_           -> [Lit s] -> SAT 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 = ([Lit s] -> SAT s ()) -> [[Lit s]] -> SAT s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
f ([Lit s] -> [[Lit s]]
forall a. [a] -> [[a]]
tails [Lit s]
literals) where
    f :: [Lit s] -> SAT s ()
    f :: forall s. [Lit s] -> SAT s ()
f [] = () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    f (Lit s
l:[Lit s]
ls) = (Lit s -> SAT s ()) -> [Lit s] -> SAT s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Lit s -> Lit s -> SAT s ()
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 = [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
addClause [Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
l1, Lit s -> Lit s
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 []         = () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAtMostOneSequential [Lit s
_]        = () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAtMostOneSequential [Lit s
x1,Lit s
x2]    = [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
addClause [Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
x1, Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
x2]
assertAtMostOneSequential (Lit s
xn:Lit s
x1:[Lit s]
xs) = do
    a1 <- SAT s (Lit s)
forall s. SAT s (Lit s)
newLit
    addClause [neg x1, a1]
    go a1 xs
  where
     go :: Lit s -> [Lit s] -> SAT s ()
go Lit s
an1 [] = [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
addClause [Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
xn, Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
an1]
     go Lit s
ai1 (Lit s
xi:[Lit s]
xis) = do
        ai <- SAT s (Lit s)
forall s. SAT s (Lit s)
newLit
        addClause [neg xi, ai]
        addClause [neg ai1, ai]
        addClause [neg xi, neg ai1]
        go ai 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 Lit s -> Lit s -> Bool
forall a. Eq a => a -> a -> Bool
== Lit s
l'   = () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise = do
        [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
addClause [Lit s
l, Lit s -> Lit s
forall a. Neg a => a -> a
neg Lit s
l']
        [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
addClause [Lit s -> Lit s
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 []     = () -> SAT s ()
forall a. a -> SAT s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAllEqual (Lit s
l:[Lit s]
ls) = Set (Lit s) -> (Lit s -> SAT s ()) -> SAT s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Lit s] -> Set (Lit s)
forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
ls) ((Lit s -> SAT s ()) -> SAT s ())
-> (Lit s -> SAT s ()) -> SAT s ()
forall a b. (a -> b) -> a -> b
$ \Lit s
l' -> Lit s -> Lit s -> SAT s ()
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_ = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
 -> SAT s ())
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> do
    ok <- ST s Bool -> EST UnsatException s Bool
forall s a e. ST s a -> EST e s a
liftST (Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
PureSAT.solve Solver s
s)
    unless ok throwUnsatException

-- | 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 = (Solver s
 -> Lit s
 -> STRef s (Definitions s)
 -> EST UnsatException s (model Bool))
-> SAT s (model Bool)
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s
  -> STRef s (Definitions s)
  -> EST UnsatException s (model Bool))
 -> SAT s (model Bool))
-> (Solver s
    -> Lit s
    -> STRef s (Definitions s)
    -> EST UnsatException s (model Bool))
-> SAT s (model Bool)
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> do
    ok <- ST s Bool -> EST UnsatException s Bool
forall s a e. ST s a -> EST e s a
liftST (Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
PureSAT.solve Solver s
s)
    unless ok throwUnsatException

    traverse (getSym s) model
  where
    getSym :: PureSAT.Solver s -> Lit s -> EST UnsatException s Bool
    getSym :: forall s. Solver s -> Lit s -> EST UnsatException s Bool
getSym Solver s
s (L Lit
l) = ST s Bool -> EST UnsatException s Bool
forall s a e. ST s a -> EST e s a
liftST (Solver s -> Lit -> ST s Bool
forall s. Solver s -> Lit -> ST s Bool
PureSAT.modelValue Solver s
s Lit
l)

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

-- | Removes already satisfied clauses.
simplify :: SAT s ()
simplify :: forall s. SAT s ()
simplify = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
 -> SAT s ())
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s ())
-> SAT s ()
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> do
    ok <- ST s Bool -> EST UnsatException s Bool
forall s a e. ST s a -> EST e s a
liftST (Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
PureSAT.simplify Solver s
s)
    unless ok throwUnsatException

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

-- | The current number of variables.
numberOfVariables :: SAT s Int
numberOfVariables :: forall s. SAT s Int
numberOfVariables = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
 -> SAT s Int)
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> ST s Int -> EST UnsatException s Int
forall s a e. ST s a -> EST e s a
liftST (ST s Int -> EST UnsatException s Int)
-> ST s Int -> EST UnsatException s Int
forall a b. (a -> b) -> a -> b
$ Solver s -> ST s Int
forall s. Solver s -> ST s Int
PureSAT.num_vars Solver s
s

-- | The current number of original clauses.
numberOfClauses :: SAT s Int
numberOfClauses :: forall s. SAT s Int
numberOfClauses = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
 -> SAT s Int)
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> ST s Int -> EST UnsatException s Int
forall s a e. ST s a -> EST e s a
liftST (ST s Int -> EST UnsatException s Int)
-> ST s Int -> EST UnsatException s Int
forall a b. (a -> b) -> a -> b
$ Solver s -> ST s Int
forall s. Solver s -> ST s Int
PureSAT.num_clauses Solver s
s

-- | The current number of learnt clauses.
numberOfLearnts :: SAT s Int
numberOfLearnts :: forall s. SAT s Int
numberOfLearnts = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
 -> SAT s Int)
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> ST s Int -> EST UnsatException s Int
forall s a e. ST s a -> EST e s a
liftST (ST s Int -> EST UnsatException s Int)
-> ST s Int -> EST UnsatException s Int
forall a b. (a -> b) -> a -> b
$ Solver s -> ST s Int
forall s. Solver s -> ST s Int
PureSAT.num_learnts Solver s
s

-- | The current number of learnt literals.
numberOfLearntLiterals :: SAT s Int
numberOfLearntLiterals :: forall s. SAT s Int
numberOfLearntLiterals = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
 -> SAT s Int)
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> ST s Int -> EST UnsatException s Int
forall s a e. ST s a -> EST e s a
liftST (ST s Int -> EST UnsatException s Int)
-> ST s Int -> EST UnsatException s Int
forall a b. (a -> b) -> a -> b
$ Solver s -> ST s Int
forall s. Solver s -> ST s Int
PureSAT.num_learnt_literals Solver s
s

-- | The current number of conflicts.
numberOfConflicts :: SAT s Int
numberOfConflicts :: forall s. SAT s Int
numberOfConflicts = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
 -> SAT s Int)
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> ST s Int -> EST UnsatException s Int
forall s a e. ST s a -> EST e s a
liftST (ST s Int -> EST UnsatException s Int)
-> ST s Int -> EST UnsatException s Int
forall a b. (a -> b) -> a -> b
$ Solver s -> ST s Int
forall s. Solver s -> ST s Int
PureSAT.num_conflicts Solver s
s

-- | The current number of conflicts.
numberOfRestarts :: SAT s Int
numberOfRestarts :: forall s. SAT s Int
numberOfRestarts = (Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall s a.
(Solver s
 -> Lit s -> STRef s (Definitions s) -> EST UnsatException s a)
-> SAT s a
SAT ((Solver s
  -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
 -> SAT s Int)
-> (Solver s
    -> Lit s -> STRef s (Definitions s) -> EST UnsatException s Int)
-> SAT s Int
forall a b. (a -> b) -> a -> b
$ \Solver s
s Lit s
_t STRef s (Definitions s)
_r -> ST s Int -> EST UnsatException s Int
forall s a e. ST s a -> EST e s a
liftST (ST s Int -> EST UnsatException s Int)
-> ST s Int -> EST UnsatException s Int
forall a b. (a -> b) -> a -> b
$ Solver s -> ST s Int
forall s. Solver s -> ST s Int
PureSAT.num_restarts Solver s
s