module Jukebox.Sat.Equality where
import Jukebox.Sat
import Jukebox.Sat.ThreeValued
import Data.IORef
import Data.Map as M
data SolverEq =
SolverEq
{ SolverEq -> Solver
satSolver :: Solver
, SolverEq -> IORef Int
counter :: IORef Int
, SolverEq -> IORef (Map (Elt, Elt) Lit3)
table :: IORef (Map (Elt,Elt) Lit3)
, SolverEq -> IORef (Maybe (Map Elt Elt))
model :: IORef (Maybe (Map Elt Elt))
}
newSolverEq :: Solver -> IO SolverEq
newSolverEq :: Solver -> IO SolverEq
newSolverEq Solver
s =
do IORef Int
ctr <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
IORef (Map (Elt, Elt) Lit3)
tab <- Map (Elt, Elt) Lit3 -> IO (IORef (Map (Elt, Elt) Lit3))
forall a. a -> IO (IORef a)
newIORef Map (Elt, Elt) Lit3
forall k a. Map k a
M.empty
IORef (Maybe (Map Elt Elt))
mod <- Maybe (Map Elt Elt) -> IO (IORef (Maybe (Map Elt Elt)))
forall a. a -> IO (IORef a)
newIORef Maybe (Map Elt Elt)
forall a. Maybe a
Nothing
SolverEq -> IO SolverEq
forall (m :: * -> *) a. Monad m => a -> m a
return SolverEq :: Solver
-> IORef Int
-> IORef (Map (Elt, Elt) Lit3)
-> IORef (Maybe (Map Elt Elt))
-> SolverEq
SolverEq
{ satSolver :: Solver
satSolver = Solver
s
, counter :: IORef Int
counter = IORef Int
ctr
, table :: IORef (Map (Elt, Elt) Lit3)
table = IORef (Map (Elt, Elt) Lit3)
tab
, model :: IORef (Maybe (Map Elt Elt))
model = IORef (Maybe (Map Elt Elt))
mod
}
instance SatSolver SolverEq where
getSolver :: SolverEq -> Solver
getSolver = SolverEq -> Solver
satSolver
class SatSolver s => EqSolver s where
getSolverEq :: s -> SolverEq
instance EqSolver SolverEq where
getSolverEq :: SolverEq -> SolverEq
getSolverEq SolverEq
s = SolverEq
s
newtype Elt = Elt Int
deriving ( Elt -> Elt -> Bool
(Elt -> Elt -> Bool) -> (Elt -> Elt -> Bool) -> Eq Elt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Elt -> Elt -> Bool
$c/= :: Elt -> Elt -> Bool
== :: Elt -> Elt -> Bool
$c== :: Elt -> Elt -> Bool
Eq, Eq Elt
Eq Elt
-> (Elt -> Elt -> Ordering)
-> (Elt -> Elt -> Bool)
-> (Elt -> Elt -> Bool)
-> (Elt -> Elt -> Bool)
-> (Elt -> Elt -> Bool)
-> (Elt -> Elt -> Elt)
-> (Elt -> Elt -> Elt)
-> Ord Elt
Elt -> Elt -> Bool
Elt -> Elt -> Ordering
Elt -> Elt -> Elt
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
min :: Elt -> Elt -> Elt
$cmin :: Elt -> Elt -> Elt
max :: Elt -> Elt -> Elt
$cmax :: Elt -> Elt -> Elt
>= :: Elt -> Elt -> Bool
$c>= :: Elt -> Elt -> Bool
> :: Elt -> Elt -> Bool
$c> :: Elt -> Elt -> Bool
<= :: Elt -> Elt -> Bool
$c<= :: Elt -> Elt -> Bool
< :: Elt -> Elt -> Bool
$c< :: Elt -> Elt -> Bool
compare :: Elt -> Elt -> Ordering
$ccompare :: Elt -> Elt -> Ordering
$cp1Ord :: Eq Elt
Ord )
instance Show Elt where
show :: Elt -> String
show (Elt Int
k) = String
"#" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
newElt :: EqSolver s => s -> IO Elt
newElt :: s -> IO Elt
newElt s
s =
do Int
k <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef (SolverEq -> IORef Int
counter (s -> SolverEq
forall s. EqSolver s => s -> SolverEq
getSolverEq s
s))
IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverEq -> IORef Int
counter (s -> SolverEq
forall s. EqSolver s => s -> SolverEq
getSolverEq s
s)) (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$! Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
Elt -> IO Elt
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Elt
Elt Int
k)
equal :: EqSolver s => s -> Elt -> Elt -> IO Lit3
equal :: s -> Elt -> Elt -> IO Lit3
equal s
s Elt
x Elt
y =
case Elt
x Elt -> Elt -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Elt
y of
Ordering
GT -> s -> Elt -> Elt -> IO Lit3
forall s. EqSolver s => s -> Elt -> Elt -> IO Lit3
equal s
s Elt
y Elt
x
Ordering
EQ -> Lit3 -> IO Lit3
forall (m :: * -> *) a. Monad m => a -> m a
return Lit3
true3
Ordering
LT -> do Map (Elt, Elt) Lit3
tab <- IORef (Map (Elt, Elt) Lit3) -> IO (Map (Elt, Elt) Lit3)
forall a. IORef a -> IO a
readIORef (SolverEq -> IORef (Map (Elt, Elt) Lit3)
table (s -> SolverEq
forall s. EqSolver s => s -> SolverEq
getSolverEq s
s))
case (Elt, Elt) -> Map (Elt, Elt) Lit3 -> Maybe Lit3
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Elt
x,Elt
y) Map (Elt, Elt) Lit3
tab of
Just Lit3
q ->
do Lit3 -> IO Lit3
forall (m :: * -> *) a. Monad m => a -> m a
return Lit3
q
Maybe Lit3
Nothing ->
do Lit3
q <- s -> IO Lit3
forall s. SatSolver s => s -> IO Lit3
newLit3 s
s
IORef (Map (Elt, Elt) Lit3) -> Map (Elt, Elt) Lit3 -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverEq -> IORef (Map (Elt, Elt) Lit3)
table (s -> SolverEq
forall s. EqSolver s => s -> SolverEq
getSolverEq s
s)) ((Elt, Elt) -> Lit3 -> Map (Elt, Elt) Lit3 -> Map (Elt, Elt) Lit3
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Elt
x,Elt
y) Lit3
q Map (Elt, Elt) Lit3
tab)
Lit3 -> IO Lit3
forall (m :: * -> *) a. Monad m => a -> m a
return Lit3
q
solveEq :: EqSolver s => s -> [Lit] -> IO Bool
solveEq :: s -> [Lit] -> IO Bool
solveEq = s -> [Lit] -> IO Bool
forall a. HasCallStack => a
undefined
modelRep :: EqSolver s => s -> Elt -> IO (Maybe Elt)
modelRep :: s -> Elt -> IO (Maybe Elt)
modelRep s
s Elt
x =
do Maybe (Map Elt Elt)
mmod <- IORef (Maybe (Map Elt Elt)) -> IO (Maybe (Map Elt Elt))
forall a. IORef a -> IO a
readIORef (SolverEq -> IORef (Maybe (Map Elt Elt))
model (s -> SolverEq
forall s. EqSolver s => s -> SolverEq
getSolverEq s
s))
Maybe Elt -> IO (Maybe Elt)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Elt -> IO (Maybe Elt)) -> Maybe Elt -> IO (Maybe Elt)
forall a b. (a -> b) -> a -> b
$
case Maybe (Map Elt Elt)
mmod of
Just Map Elt Elt
mp -> Elt -> Map Elt Elt -> Maybe Elt
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Elt
x Map Elt Elt
mp
Maybe (Map Elt Elt)
Nothing -> Maybe Elt
forall a. Maybe a
Nothing