{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnboxedTuples #-}
module Control.Monad.SAT (
SAT,
runSATMaybe,
Lit,
newLit,
boostScore,
Neg (..),
addClause,
assertAtLeastOne,
assertAtMostOne,
assertAtMostOnePairwise,
assertAtMostOneSequential,
assertEqual,
assertAllEqual,
Prop,
true, false,
lit, (\/), (/\), (<->), (-->), xor, ite,
addDefinition,
addProp,
trueLit,
falseLit,
addConjDefinition,
addDisjDefinition,
solve,
solve_,
simplify,
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
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
type role SAT nominal representational
type Definitions s = Map (Set (Lit s)) (Lit s)
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
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
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
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
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)
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)
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)
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 s
true :: forall s. Prop s
true = Prop s
forall s. Prop s
PTrue
false :: Prop s
false :: forall s. Prop s
false = Prop s
forall s. Prop s
PFalse
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)
(\/) :: 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)
(/\) :: 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)
(-->) :: 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
(<->) :: 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)
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
ite :: Prop s -> Prop s -> Prop s -> Prop s
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)
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)
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)
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
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)
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
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
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
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_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'
add_clause s (d : map neg (Set.toList ps))
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]
liftST (writeSTRef defsRef $! Map.insert ps d defs)
return d
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)
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')
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
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
assertAtLeastOne :: [Lit s] -> SAT s ()
assertAtLeastOne :: forall s. [Lit s] -> SAT s ()
assertAtLeastOne = [Lit s] -> SAT s ()
forall s. [Lit s] -> SAT s ()
addClause
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
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]
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
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']
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'
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
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)
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
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
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
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
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
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
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