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

--------------------------------------------------------------------------------