module Control.Monad.SAT (
SAT,
runSAT,
runSATMaybe,
UnsatException (..),
Lit,
newLit,
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,
numberOfConflicts,
) where
import Control.Exception (Exception, catch, throwIO)
import Control.Monad (forM_, unless)
import Control.Monad.IO.Class (MonadIO (..))
import Control.Monad.IO.Unlift (MonadUnliftIO (..))
import Data.Bits (shiftR, testBit)
import Data.IORef (IORef, newIORef, readIORef, writeIORef)
import Data.List (tails)
import Data.Map.Strict (Map)
import Data.Set (Set)
import GHC.Exts (oneShot)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import qualified MiniSat
newtype SAT s a = SAT_ { forall s a.
SAT s a -> Solver -> Lit s -> IORef (Definitions s) -> IO a
unSAT :: MiniSat.Solver -> Lit s -> IORef (Definitions s) -> IO a }
deriving forall a b. a -> SAT s b -> SAT s a
forall a b. (a -> b) -> SAT s a -> SAT s b
forall s a b. a -> SAT s b -> SAT s a
forall s a b. (a -> b) -> SAT s a -> SAT s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> SAT s b -> SAT s a
$c<$ :: forall s a b. a -> SAT s b -> SAT s a
fmap :: forall a b. (a -> b) -> SAT s a -> SAT s b
$cfmap :: forall s a b. (a -> b) -> SAT s a -> SAT s b
Functor
type role SAT nominal representational
pattern SAT :: forall s a. (MiniSat.Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
pattern $bSAT :: forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
$mSAT :: forall {r} {s} {a}.
SAT s a
-> ((Solver -> Lit s -> IORef (Definitions s) -> IO a) -> r)
-> ((# #) -> r)
-> r
SAT m <- SAT_ m
where SAT Solver -> Lit s -> IORef (Definitions s) -> IO a
m = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT_ (oneShot :: forall a b. (a -> b) -> a -> b
oneShot Solver -> Lit s -> IORef (Definitions s) -> IO a
m)
{-# COMPLETE SAT #-}
type Definitions s = Map (Set (Lit s)) (Lit s)
data UnsatException = UnsatException
deriving (Int -> UnsatException -> ShowS
[UnsatException] -> ShowS
UnsatException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnsatException] -> ShowS
$cshowList :: [UnsatException] -> ShowS
show :: UnsatException -> String
$cshow :: UnsatException -> String
showsPrec :: Int -> UnsatException -> ShowS
$cshowsPrec :: Int -> UnsatException -> ShowS
Show)
instance Exception UnsatException
data SATPanic = SATPanic
deriving (Int -> SATPanic -> ShowS
[SATPanic] -> ShowS
SATPanic -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SATPanic] -> ShowS
$cshowList :: [SATPanic] -> ShowS
show :: SATPanic -> String
$cshow :: SATPanic -> String
showsPrec :: Int -> SATPanic -> ShowS
$cshowsPrec :: Int -> SATPanic -> ShowS
Show)
instance Exception SATPanic
instance Applicative (SAT s) where
pure :: forall a. a -> SAT s a
pure a
x = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT (\Solver
_ Lit s
_ IORef (Definitions s)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
SAT Solver -> Lit s -> IORef (Definitions s) -> IO (a -> b)
f <*> :: forall a b. SAT s (a -> b) -> SAT s a -> SAT s b
<*> SAT Solver -> Lit s -> IORef (Definitions s) -> IO a
x = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT (\Solver
s Lit s
t IORef (Definitions s)
r -> Solver -> Lit s -> IORef (Definitions s) -> IO (a -> b)
f Solver
s Lit s
t IORef (Definitions s)
r forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solver -> Lit s -> IORef (Definitions s) -> IO a
x Solver
s Lit s
t IORef (Definitions s)
r)
instance Monad (SAT s) where
SAT s a
m >>= :: forall a b. SAT s a -> (a -> SAT s b) -> SAT s b
>>= a -> SAT s b
k = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
t IORef (Definitions s)
r -> do
a
x <- forall s a.
SAT s a -> Solver -> Lit s -> IORef (Definitions s) -> IO a
unSAT SAT s a
m Solver
s Lit s
t IORef (Definitions s)
r
forall s a.
SAT s a -> Solver -> Lit s -> IORef (Definitions s) -> IO a
unSAT (a -> SAT s b
k a
x) Solver
s Lit s
t IORef (Definitions s)
r
instance MonadIO (SAT s) where
liftIO :: forall a. IO a -> SAT s a
liftIO IO a
m = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT (\Solver
_ Lit s
_ IORef (Definitions s)
_ -> IO a
m)
instance MonadUnliftIO (SAT s) where
withRunInIO :: forall b. ((forall a. SAT s a -> IO a) -> IO b) -> SAT s b
withRunInIO (forall a. SAT s a -> IO a) -> IO b
kont = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
t IORef (Definitions s)
r -> (forall a. SAT s a -> IO a) -> IO b
kont (\(SAT Solver -> Lit s -> IORef (Definitions s) -> IO a
m) -> Solver -> Lit s -> IORef (Definitions s) -> IO a
m Solver
s Lit s
t IORef (Definitions s)
r)
runSAT :: (forall s. SAT s a) -> IO a
runSAT :: forall a. (forall s. SAT s a) -> IO a
runSAT (SAT Solver -> Lit Any -> IORef (Definitions Any) -> IO a
f) = forall a. (Solver -> IO a) -> IO a
MiniSat.withNewSolverAsync forall a b. (a -> b) -> a -> b
$ \Solver
s -> do
Lit
t <- Solver -> IO Lit
MiniSat.newLit Solver
s
forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [forall s. Lit -> Lit s
L Lit
t]
IORef (Definitions Any)
r <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty
Solver -> Lit Any -> IORef (Definitions Any) -> IO a
f Solver
s (forall s. Lit -> Lit s
L Lit
t) IORef (Definitions Any)
r
runSATMaybe :: (forall s. SAT s a) -> IO (Maybe a)
runSATMaybe :: forall a. (forall s. SAT s a) -> IO (Maybe a)
runSATMaybe forall s. SAT s a
m = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just (forall a. (forall s. SAT s a) -> IO a
runSAT forall s. SAT s a
m) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \UnsatException
UnsatException -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
newtype Lit s = L { forall s. Lit s -> Lit
unL :: MiniSat.Lit }
deriving (Lit s -> Lit s -> Bool
forall s. Lit s -> Lit s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lit s -> Lit s -> Bool
$c/= :: forall s. Lit s -> Lit s -> Bool
== :: Lit s -> Lit s -> Bool
$c== :: forall s. Lit s -> Lit s -> Bool
Eq, Lit s -> Lit s -> Bool
Lit s -> Lit s -> Ordering
Lit s -> Lit s -> Lit s
forall s. Eq (Lit s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. Lit s -> Lit s -> Bool
forall s. Lit s -> Lit s -> Ordering
forall s. Lit s -> Lit s -> Lit s
min :: Lit s -> Lit s -> Lit s
$cmin :: forall s. Lit s -> Lit s -> Lit s
max :: Lit s -> Lit s -> Lit s
$cmax :: forall s. Lit s -> Lit s -> Lit s
>= :: Lit s -> Lit s -> Bool
$c>= :: forall s. Lit s -> Lit s -> Bool
> :: Lit s -> Lit s -> Bool
$c> :: forall s. Lit s -> Lit s -> Bool
<= :: Lit s -> Lit s -> Bool
$c<= :: forall s. Lit s -> Lit s -> Bool
< :: Lit s -> Lit s -> Bool
$c< :: forall s. Lit s -> Lit s -> Bool
compare :: Lit s -> Lit s -> Ordering
$ccompare :: forall s. Lit s -> Lit s -> Ordering
Ord)
type role Lit nominal
instance Show (Lit s) where
showsPrec :: Int -> Lit s -> ShowS
showsPrec Int
d (L (MiniSat.MkLit CInt
l))
| Bool
p = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
6) (Char -> ShowS
showChar Char
'-' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows Int
v)
| Bool
otherwise = forall a. Show a => a -> ShowS
shows Int
v
where
i :: Int
i :: Int
i = forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
l
p :: Bool
p :: Bool
p = forall a. Bits a => a -> Int -> Bool
testBit Int
i Int
0
v :: Int
v :: Int
v = forall a. Bits a => a -> Int -> a
shiftR Int
i Int
1
class Neg a where
neg :: a -> a
instance Neg (Lit s) where
neg :: Lit s -> Lit s
neg (L Lit
l) = forall s. Lit -> Lit s
L (Lit -> Lit
MiniSat.neg Lit
l)
newLit :: SAT s (Lit s)
newLit :: forall s. SAT s (Lit s)
newLit = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
Lit
l <- Solver -> IO Lit
MiniSat.newLit Solver
s
forall (m :: * -> *) a. Monad m => a -> m a
return (forall s. Lit -> Lit s
L Lit
l)
data Prop s
= PTrue
| PFalse
| P (Prop1 s)
deriving (Prop s -> Prop s -> Bool
forall s. Prop s -> Prop s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prop s -> Prop s -> Bool
$c/= :: forall s. Prop s -> Prop s -> Bool
== :: Prop s -> Prop s -> Bool
$c== :: forall s. Prop s -> Prop s -> Bool
Eq, Prop s -> Prop s -> Bool
Prop s -> Prop s -> Ordering
forall s. Eq (Prop s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. Prop s -> Prop s -> Bool
forall s. Prop s -> Prop s -> Ordering
forall s. Prop s -> Prop s -> Prop s
min :: Prop s -> Prop s -> Prop s
$cmin :: forall s. Prop s -> Prop s -> Prop s
max :: Prop s -> Prop s -> Prop s
$cmax :: forall s. Prop s -> Prop s -> Prop s
>= :: Prop s -> Prop s -> Bool
$c>= :: forall s. Prop s -> Prop s -> Bool
> :: Prop s -> Prop s -> Bool
$c> :: forall s. Prop s -> Prop s -> Bool
<= :: Prop s -> Prop s -> Bool
$c<= :: forall s. Prop s -> Prop s -> Bool
< :: Prop s -> Prop s -> Bool
$c< :: forall s. Prop s -> Prop s -> Bool
compare :: Prop s -> Prop s -> Ordering
$ccompare :: forall s. Prop s -> Prop s -> Ordering
Ord)
infixr 5 \/
infixr 6 /\
instance Show (Prop s) where
showsPrec :: Int -> Prop s -> ShowS
showsPrec Int
_ Prop s
PTrue = String -> ShowS
showString String
"true"
showsPrec Int
_ Prop s
PFalse = String -> ShowS
showString String
"false"
showsPrec Int
d (P Prop1 s
p) = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Prop1 s
p
true :: Prop s
true :: forall s. Prop s
true = forall s. Prop s
PTrue
false :: Prop s
false :: forall s. Prop s
false = forall s. Prop s
PFalse
lit :: Lit s -> Prop s
lit :: forall s. Lit s -> Prop s
lit Lit s
l = forall s. Prop1 s -> Prop s
P (forall s. Lit s -> Prop1 s
P1Lit Lit s
l)
(\/) :: Prop s -> Prop s -> Prop s
Prop s
x \/ :: forall s. Prop s -> Prop s -> Prop s
\/ Prop s
y = forall a. Neg a => a -> a
neg (forall a. Neg a => a -> a
neg Prop s
x forall s. Prop s -> Prop s -> Prop s
/\ forall a. Neg a => a -> a
neg Prop s
y)
(/\) :: Prop s -> Prop s -> Prop s
Prop s
PFalse /\ :: forall s. Prop s -> Prop s -> Prop s
/\ Prop s
_ = forall s. Prop s
PFalse
Prop s
_ /\ Prop s
PFalse = forall s. Prop s
PFalse
Prop s
PTrue /\ Prop s
y = Prop s
y
Prop s
x /\ Prop s
PTrue = Prop s
x
P Prop1 s
x /\ P Prop1 s
y = forall s. Prop1 s -> Prop s
P (forall s. Prop1 s -> Prop1 s -> Prop1 s
p1and Prop1 s
x Prop1 s
y)
(-->) :: Prop s -> Prop s -> Prop s
Prop s
x --> :: forall s. Prop s -> Prop s -> Prop s
--> Prop s
y = forall a. Neg a => a -> a
neg Prop s
x forall s. Prop s -> Prop s -> Prop s
\/ Prop s
y
(<->) :: Prop s -> Prop s -> Prop s
Prop s
x <-> :: forall s. Prop s -> Prop s -> Prop s
<-> Prop s
y = (Prop s
x forall s. Prop s -> Prop s -> Prop s
--> Prop s
y) forall s. Prop s -> Prop s -> Prop s
/\ (Prop s
y forall s. Prop s -> Prop s -> Prop s
--> Prop s
x)
xor :: Prop s -> Prop s -> Prop s
xor :: forall s. Prop s -> Prop s -> Prop s
xor Prop s
x Prop s
y = Prop s
x forall s. Prop s -> Prop s -> Prop s
<-> forall a. Neg a => a -> a
neg Prop s
y
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 forall s. Prop s -> Prop s -> Prop s
\/ Prop s
f) forall s. Prop s -> Prop s -> Prop s
/\ (forall a. Neg a => a -> a
neg Prop s
c forall s. Prop s -> Prop s -> Prop s
\/ Prop s
t) forall s. Prop s -> Prop s -> Prop s
/\ (Prop s
t forall s. Prop s -> Prop s -> Prop s
\/ Prop s
f)
instance Neg (Prop s) where
neg :: Prop s -> Prop s
neg Prop s
PTrue = forall s. Prop s
PFalse
neg Prop s
PFalse = forall s. Prop s
PTrue
neg (P Prop1 s
p) = forall s. Prop1 s -> Prop s
P (forall s. Prop1 s -> Prop1 s
p1neg Prop1 s
p)
data Prop1 s
= P1Lit !(Lit s)
| P1Nnd !(Set (PropA s))
| P1And !(Set (PropA s))
deriving (Prop1 s -> Prop1 s -> Bool
forall s. Prop1 s -> Prop1 s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prop1 s -> Prop1 s -> Bool
$c/= :: forall s. Prop1 s -> Prop1 s -> Bool
== :: Prop1 s -> Prop1 s -> Bool
$c== :: forall s. Prop1 s -> Prop1 s -> Bool
Eq, Prop1 s -> Prop1 s -> Bool
Prop1 s -> Prop1 s -> Ordering
forall s. Eq (Prop1 s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. Prop1 s -> Prop1 s -> Bool
forall s. Prop1 s -> Prop1 s -> Ordering
forall s. Prop1 s -> Prop1 s -> Prop1 s
min :: Prop1 s -> Prop1 s -> Prop1 s
$cmin :: forall s. Prop1 s -> Prop1 s -> Prop1 s
max :: Prop1 s -> Prop1 s -> Prop1 s
$cmax :: forall s. Prop1 s -> Prop1 s -> Prop1 s
>= :: Prop1 s -> Prop1 s -> Bool
$c>= :: forall s. Prop1 s -> Prop1 s -> Bool
> :: Prop1 s -> Prop1 s -> Bool
$c> :: forall s. Prop1 s -> Prop1 s -> Bool
<= :: Prop1 s -> Prop1 s -> Bool
$c<= :: forall s. Prop1 s -> Prop1 s -> Bool
< :: Prop1 s -> Prop1 s -> Bool
$c< :: forall s. Prop1 s -> Prop1 s -> Bool
compare :: Prop1 s -> Prop1 s -> Ordering
$ccompare :: forall s. Prop1 s -> Prop1 s -> Ordering
Ord)
data PropA s
= PALit !(Lit s)
| PANnd !(Set (PropA s))
deriving (PropA s -> PropA s -> Bool
forall s. PropA s -> PropA s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropA s -> PropA s -> Bool
$c/= :: forall s. PropA s -> PropA s -> Bool
== :: PropA s -> PropA s -> Bool
$c== :: forall s. PropA s -> PropA s -> Bool
Eq, PropA s -> PropA s -> Bool
PropA s -> PropA s -> Ordering
forall s. Eq (PropA s)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s. PropA s -> PropA s -> Bool
forall s. PropA s -> PropA s -> Ordering
forall s. PropA s -> PropA s -> PropA s
min :: PropA s -> PropA s -> PropA s
$cmin :: forall s. PropA s -> PropA s -> PropA s
max :: PropA s -> PropA s -> PropA s
$cmax :: forall s. PropA s -> PropA s -> PropA s
>= :: PropA s -> PropA s -> Bool
$c>= :: forall s. PropA s -> PropA s -> Bool
> :: PropA s -> PropA s -> Bool
$c> :: forall s. PropA s -> PropA s -> Bool
<= :: PropA s -> PropA s -> Bool
$c<= :: forall s. PropA s -> PropA s -> Bool
< :: PropA s -> PropA s -> Bool
$c< :: forall s. PropA s -> PropA s -> Bool
compare :: PropA s -> PropA s -> Ordering
$ccompare :: forall s. PropA s -> PropA s -> Ordering
Ord)
instance Show (Prop1 s) where
showsPrec :: Int -> Prop1 s -> ShowS
showsPrec Int
d (P1Lit Lit s
l) = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Lit s
l
showsPrec Int
_ (P1And Set (PropA s)
xs) = forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith forall a. Show a => a -> ShowS
shows (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
showsPrec Int
_ (P1Nnd Set (PropA s)
xs) = Char -> ShowS
showChar Char
'-' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith forall a. Show a => a -> ShowS
shows (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
instance Show (PropA s) where
showsPrec :: Int -> PropA s -> ShowS
showsPrec Int
d (PALit Lit s
l) = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Lit s
l
showsPrec Int
_ (PANnd Set (PropA s)
xs) = Char -> ShowS
showChar Char
'-' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith forall a. Show a => a -> ShowS
shows (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
showNoCommaListWith :: (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith :: forall a. (a -> ShowS) -> [a] -> ShowS
showNoCommaListWith a -> ShowS
_ [] String
s = String
"[]" forall a. [a] -> [a] -> [a]
++ String
s
showNoCommaListWith a -> ShowS
showx (a
x:[a]
xs) String
s = Char
'[' forall a. a -> [a] -> [a]
: a -> ShowS
showx a
x ([a] -> String
showl [a]
xs)
where
showl :: [a] -> String
showl [] = Char
']' forall a. a -> [a] -> [a]
: String
s
showl (a
y:[a]
ys) = Char
' ' forall a. a -> [a] -> [a]
: a -> ShowS
showx a
y ([a] -> String
showl [a]
ys)
p1and :: Prop1 s -> Prop1 s -> Prop1 s
p1and :: forall s. Prop1 s -> Prop1 s -> Prop1 s
p1and p :: Prop1 s
p@(P1Lit Lit s
x) (P1Lit Lit s
y)
| Lit s
x forall a. Eq a => a -> a -> Bool
== Lit s
y = Prop1 s
p
| Bool
otherwise = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Lit s -> PropA s
PALit Lit s
x) (forall s. Lit s -> PropA s
PALit Lit s
y))
p1and p :: Prop1 s
p@(P1Nnd Set (PropA s)
x) (P1Nnd Set (PropA s)
y)
| Set (PropA s)
x forall a. Eq a => a -> a -> Bool
== Set (PropA s)
y = Prop1 s
p
| Bool
otherwise = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y))
p1and (P1Lit Lit s
x) (P1Nnd Set (PropA s)
y) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Lit s -> PropA s
PALit Lit s
x) (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y))
p1and (P1Nnd Set (PropA s)
x) (P1Lit Lit s
y) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> a -> Set a
double (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) (forall s. Lit s -> PropA s
PALit Lit s
y))
p1and (P1Lit Lit s
x) (P1And Set (PropA s)
ys) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Lit s -> PropA s
PALit Lit s
x) Set (PropA s)
ys)
p1and (P1Nnd Set (PropA s)
x) (P1And Set (PropA s)
ys) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
x) Set (PropA s)
ys)
p1and (P1And Set (PropA s)
xs) (P1Lit Lit s
y) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Lit s -> PropA s
PALit Lit s
y) Set (PropA s)
xs)
p1and (P1And Set (PropA s)
xs) (P1Nnd Set (PropA s)
y) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall s. Set (PropA s) -> PropA s
PANnd Set (PropA s)
y) Set (PropA s)
xs)
p1and (P1And Set (PropA s)
xs) (P1And Set (PropA s)
ys) = forall s. Set (PropA s) -> Prop1 s
P1And (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (PropA s)
xs Set (PropA s)
ys)
p1neg :: Prop1 s -> Prop1 s
p1neg :: forall s. Prop1 s -> Prop1 s
p1neg (P1Lit Lit s
l) = forall s. Lit s -> Prop1 s
P1Lit (forall a. Neg a => a -> a
neg Lit s
l)
p1neg (P1Nnd Set (PropA s)
xs) = forall s. Set (PropA s) -> Prop1 s
P1And Set (PropA s)
xs
p1neg (P1And Set (PropA s)
xs) = forall s. Set (PropA s) -> Prop1 s
P1Nnd Set (PropA s)
xs
double :: Ord a => a -> a -> Set a
double :: forall a. Ord a => a -> a -> Set a
double a
x a
y = forall a. Ord a => a -> Set a -> Set a
Set.insert a
x (forall a. a -> Set a
Set.singleton a
y)
addConjDefinition :: Lit s -> [Lit s] -> SAT s ()
addConjDefinition :: forall s. Lit s -> [Lit s] -> SAT s ()
addConjDefinition Lit s
x [Lit s]
zs = do
Lit s
y <- forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
zs)
if Lit s
x forall a. Eq a => a -> a -> Bool
== Lit s
y
then forall (m :: * -> *) a. Monad m => a -> m a
return ()
else forall s. Lit s -> Lit s -> SAT s ()
assertEqual Lit s
x Lit s
y
addDisjDefinition :: Lit s -> [Lit s] -> SAT s ()
addDisjDefinition :: forall s. Lit s -> [Lit s] -> SAT s ()
addDisjDefinition Lit s
x [Lit s]
ys = forall s. Lit s -> [Lit s] -> SAT s ()
addConjDefinition (forall a. Neg a => a -> a
neg Lit s
x) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Neg a => a -> a
neg [Lit s]
ys)
addProp :: Prop s -> SAT s ()
addProp :: forall s. Prop s -> SAT s ()
addProp Prop s
PTrue = forall (m :: * -> *) a. Monad m => a -> m a
return ()
addProp Prop s
PFalse = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
t IORef (Definitions s)
_ -> forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [forall a. Neg a => a -> a
neg Lit s
t]
addProp (P Prop1 s
p) = forall s. Prop1 s -> SAT s ()
add_prop Prop1 s
p
addDefinition :: Prop s -> SAT s (Lit s)
addDefinition :: forall s. Prop s -> SAT s (Lit s)
addDefinition Prop s
PTrue = forall s. SAT s (Lit s)
trueLit
addDefinition Prop s
PFalse = forall s. SAT s (Lit s)
falseLit
addDefinition (P Prop1 s
p) = forall s. Prop1 s -> SAT s (Lit s)
addDefinition1 Prop1 s
p
trueLit :: SAT s (Lit s)
trueLit :: forall s. SAT s (Lit s)
trueLit = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
_s Lit s
t IORef (Definitions s)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
t
falseLit :: SAT s (Lit s)
falseLit :: forall s. SAT s (Lit s)
falseLit = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
_s Lit s
t IORef (Definitions s)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Neg a => a -> a
neg Lit s
t)
addDefinition1 :: Prop1 s -> SAT s (Lit s)
addDefinition1 :: forall s. Prop1 s -> SAT s (Lit s)
addDefinition1 = forall s. Prop1 s -> SAT s (Lit s)
tseitin1
add_definition :: Set (Lit s) -> SAT s (Lit s)
add_definition :: forall s. Set (Lit s) -> SAT s (Lit s)
add_definition Set (Lit s)
ps
| forall a. Set a -> Bool
Set.null Set (Lit s)
ps
= forall s. SAT s (Lit s)
trueLit
add_definition Set (Lit s)
ps = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_ IORef (Definitions s)
defsRef -> do
Definitions s
defs <- forall a. IORef a -> IO a
readIORef IORef (Definitions s)
defsRef
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Set (Lit s)
ps Definitions s
defs of
Just Lit s
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
d
Maybe (Lit s)
Nothing -> do
Lit
d' <- Solver -> IO Lit
MiniSat.newLit Solver
s
let d :: Lit s
d = forall s. Lit -> Lit s
L Lit
d'
forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s forall a b. (a -> b) -> a -> b
$ Lit s
d forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Neg a => a -> a
neg (forall a. Set a -> [a]
Set.toList Set (Lit s)
ps)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set (Lit s)
ps forall a b. (a -> b) -> a -> b
$ \Lit s
p -> do
forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [forall a. Neg a => a -> a
neg Lit s
d, Lit s
p]
forall a. IORef a -> a -> IO ()
writeIORef IORef (Definitions s)
defsRef forall a b. (a -> b) -> a -> b
$! forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Set (Lit s)
ps Lit s
d Definitions s
defs
forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
d
add_prop :: Prop1 s -> SAT s ()
add_prop :: forall s. Prop1 s -> SAT s ()
add_prop (P1Lit Lit s
l) = forall s. [Lit s] -> SAT s ()
addClause [Lit s
l]
add_prop (P1And Set (PropA s)
xs) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set (PropA s)
xs forall s. PropA s -> SAT s ()
add_prop'
add_prop (P1Nnd Set (PropA s)
xs) = do
[Lit s]
ls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
forall s. [Lit s] -> SAT s ()
addClause (forall a b. (a -> b) -> [a] -> [b]
map forall a. Neg a => a -> a
neg [Lit s]
ls)
add_prop' :: PropA s -> SAT s ()
add_prop' :: forall s. PropA s -> SAT s ()
add_prop' (PALit Lit s
l) = forall s. [Lit s] -> SAT s ()
addClause [Lit s
l]
add_prop' (PANnd Set (PropA s)
xs) = do
[Lit s]
ls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
forall s. [Lit s] -> SAT s ()
addClause (forall a b. (a -> b) -> [a] -> [b]
map forall a. Neg a => a -> a
neg [Lit s]
ls)
tseitin1 :: Prop1 s -> SAT s (Lit s)
tseitin1 :: forall s. Prop1 s -> SAT s (Lit s)
tseitin1 (P1Lit Lit s
l) = forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
l
tseitin1 (P1And Set (PropA s)
xs) = do
[Lit s]
xs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
xs')
tseitin1 (P1Nnd Set (PropA s)
xs) = do
[Lit s]
xs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
forall a. Neg a => a -> a
neg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
xs')
tseitinA :: PropA s -> SAT s (Lit s)
tseitinA :: forall s. PropA s -> SAT s (Lit s)
tseitinA (PALit Lit s
l) = forall (m :: * -> *) a. Monad m => a -> m a
return Lit s
l
tseitinA (PANnd Set (PropA s)
xs) = do
[Lit s]
xs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. PropA s -> SAT s (Lit s)
tseitinA (forall a. Set a -> [a]
Set.toList Set (PropA s)
xs)
forall a. Neg a => a -> a
neg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. Set (Lit s) -> SAT s (Lit s)
add_definition (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
xs')
addClause :: [Lit s] -> SAT s ()
addClause :: forall s. [Lit s] -> SAT s ()
addClause [Lit s]
ls = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [Lit s]
ls
add_clause :: MiniSat.Solver -> [Lit s] -> IO ()
add_clause :: forall s. Solver -> [Lit s] -> IO ()
add_clause Solver
s [Lit s]
ls = do
Bool
ok <- Solver -> [Lit] -> IO Bool
MiniSat.addClause Solver
s (forall a b. (a -> b) -> [a] -> [b]
map forall s. Lit s -> Lit
unL [Lit s]
ls)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException
assertAtLeastOne :: [Lit s] -> SAT s ()
assertAtLeastOne :: forall s. [Lit s] -> SAT s ()
assertAtLeastOne = 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
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Lit s
_] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Lit s
_,Lit s
_] -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
[Lit s
_,Lit s
_,Lit s
_] -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
[Lit s
_,Lit s
_,Lit s
_,Lit s
_] -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
[Lit s
_,Lit s
_,Lit s
_,Lit s
_,Lit s
_] -> forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
ls
[Lit s]
_ -> forall s. [Lit s] -> SAT s ()
assertAtMostOneSequential [Lit s]
ls
assertAtMostOnePairwise :: [Lit s] -> SAT s ()
assertAtMostOnePairwise :: forall s. [Lit s] -> SAT s ()
assertAtMostOnePairwise [Lit s]
literals = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall s. [Lit s] -> SAT s ()
f (forall a. [a] -> [[a]]
tails [Lit s]
literals) where
f :: [Lit s] -> SAT s ()
f :: forall s. [Lit s] -> SAT s ()
f [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
f (Lit s
l:[Lit s]
ls) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall s. Lit s -> Lit s -> SAT s ()
g Lit s
l) [Lit s]
ls
g :: Lit s -> Lit s -> SAT s ()
g :: forall s. Lit s -> Lit s -> SAT s ()
g Lit s
l1 Lit s
l2 = forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
l1, forall a. Neg a => a -> a
neg Lit s
l2]
assertAtMostOneSequential :: [Lit s] -> SAT s ()
assertAtMostOneSequential :: forall s. [Lit s] -> SAT s ()
assertAtMostOneSequential [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAtMostOneSequential [Lit s
_] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAtMostOneSequential [Lit s
x1,Lit s
x2] = forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
x1, forall a. Neg a => a -> a
neg Lit s
x2]
assertAtMostOneSequential (Lit s
xn:Lit s
x1:[Lit s]
xs) = do
Lit s
a1 <- forall s. SAT s (Lit s)
newLit
forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
x1, Lit s
a1]
Lit s -> [Lit s] -> SAT s ()
go Lit s
a1 [Lit s]
xs
where
go :: Lit s -> [Lit s] -> SAT s ()
go Lit s
an1 [] = forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
xn, forall a. Neg a => a -> a
neg Lit s
an1]
go Lit s
ai1 (Lit s
xi:[Lit s]
xis) = do
Lit s
ai <- forall s. SAT s (Lit s)
newLit
forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
xi, Lit s
ai]
forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
ai1, Lit s
ai]
forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
xi, forall a. Neg a => a -> a
neg Lit s
ai1]
Lit s -> [Lit s] -> SAT s ()
go Lit s
ai [Lit s]
xis
assertEqual :: Lit s -> Lit s -> SAT s ()
assertEqual :: forall s. Lit s -> Lit s -> SAT s ()
assertEqual Lit s
l Lit s
l'
| Lit s
l forall a. Eq a => a -> a -> Bool
== Lit s
l' = forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do
forall s. [Lit s] -> SAT s ()
addClause [Lit s
l, forall a. Neg a => a -> a
neg Lit s
l']
forall s. [Lit s] -> SAT s ()
addClause [forall a. Neg a => a -> a
neg Lit s
l, Lit s
l']
assertAllEqual :: [Lit s] -> SAT s ()
assertAllEqual :: forall s. [Lit s] -> SAT s ()
assertAllEqual [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertAllEqual (Lit s
l:[Lit s]
ls) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Ord a => [a] -> Set a
Set.fromList [Lit s]
ls) forall a b. (a -> b) -> a -> b
$ \Lit s
l' -> forall s. Lit s -> Lit s -> SAT s ()
assertEqual Lit s
l Lit s
l'
solve_ :: SAT s ()
solve_ :: forall s. SAT s ()
solve_ = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
Bool
ok <- Solver -> [Lit] -> IO Bool
MiniSat.solve Solver
s []
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException
solve :: Traversable model => model (Lit s) -> SAT s (model Bool)
solve :: forall (model :: * -> *) s.
Traversable model =>
model (Lit s) -> SAT s (model Bool)
solve model (Lit s)
model = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
Bool
ok <- Solver -> [Lit] -> IO Bool
MiniSat.solve Solver
s []
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall s. Solver -> Lit s -> IO Bool
getSym Solver
s) model (Lit s)
model
where
getSym :: MiniSat.Solver -> Lit s -> IO Bool
getSym :: forall s. Solver -> Lit s -> IO Bool
getSym Solver
s (L Lit
l) = do
Maybe Bool
b <- Solver -> Lit -> IO (Maybe Bool)
MiniSat.modelValue Solver
s Lit
l
case Maybe Bool
b of
Maybe Bool
Nothing -> forall e a. Exception e => e -> IO a
throwIO SATPanic
SATPanic
Just Bool
b' -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b'
simplify :: SAT s ()
simplify :: forall s. SAT s ()
simplify = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> do
Bool
ok <- Solver -> IO Bool
MiniSat.simplify Solver
s
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO UnsatException
UnsatException
numberOfVariables :: SAT s Int
numberOfVariables :: forall s. SAT s Int
numberOfVariables = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_vars Solver
s
numberOfClauses :: SAT s Int
numberOfClauses :: forall s. SAT s Int
numberOfClauses = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_clauses Solver
s
numberOfLearnts :: SAT s Int
numberOfLearnts :: forall s. SAT s Int
numberOfLearnts = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_learnts Solver
s
numberOfConflicts :: SAT s Int
numberOfConflicts :: forall s. SAT s Int
numberOfConflicts = forall s a.
(Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a
SAT forall a b. (a -> b) -> a -> b
$ \Solver
s Lit s
_t IORef (Definitions s)
_r -> Solver -> IO Int
MiniSat.minisat_num_conflicts Solver
s