{-# OPTIONS_GHC -optc-DCTYPE_solver=minisat_solver* #-}
{-# OPTIONS_GHC -optc-DHTYPE_solver=Solver #-}
{-# OPTIONS_GHC -optc-DCTYPE_bool=minisat_bool #-}
{-# OPTIONS_GHC -optc-DHTYPE_bool=Bool #-}
{-# OPTIONS_GHC -optc-DCTYPE_lit=minisat_Lit #-}
{-# OPTIONS_GHC -optc-DHTYPE_lit=Lit #-}
{-# OPTIONS_GHC -optc-DCTYPE_int=int #-}
{-# OPTIONS_GHC -optc-DHTYPE_int=Int #-}
{-# OPTIONS_GHC -optc-DCTYPE_var=minisat_Var #-}
{-# OPTIONS_GHC -optc-DHTYPE_var=Var #-}
{-# OPTIONS_GHC -optc-DCTYPE_lbool=minisat_lbool #-}
{-# OPTIONS_GHC -optc-DHTYPE_lbool=LBool #-}
{-# LINE 1 "minisat-haskell-bindings/MiniSat.hsc" #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE ScopedTypeVariables #-}

module MiniSat where

import Foreign.Ptr     ( Ptr, nullPtr )
import Foreign.C.Types ( CInt(..) )
import Control.Exception (bracket, finally, mask_, onException )
import Control.Concurrent.Async




-- | Run a minisat instance in such a way that it is
-- interruptable (by sending killThread).
-- cf. https://github.com/niklasso/minisat-haskell-bindings/issues/1
withNewSolverAsync :: (Solver -> IO a) -> IO a
withNewSolverAsync :: (Solver -> IO a) -> IO a
withNewSolverAsync Solver -> IO a
h = 
  IO Solver -> (Solver -> IO ()) -> (Solver -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket IO Solver
newSolver Solver -> IO ()
deleteSolver ((Solver -> IO a) -> IO a) -> (Solver -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \  Solver
s -> do
    IO a -> IO a
forall a. IO a -> IO a
mask_ (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ IO a -> (Async a -> IO a) -> IO a
forall a b. IO a -> (Async a -> IO b) -> IO b
withAsync (Solver -> IO a
h Solver
s) ((Async a -> IO a) -> IO a) -> (Async a -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \ Async a
a -> do
      Async a -> IO a
forall a. Async a -> IO a
wait Async a
a IO a -> IO () -> IO a
forall a b. IO a -> IO b -> IO a
`onException` Solver -> IO ()
minisat_interrupt Solver
s

withNewSolver :: (Solver -> IO a) -> IO a
withNewSolver :: (Solver -> IO a) -> IO a
withNewSolver Solver -> IO a
h =
  do Solver
s <- IO Solver
newSolver
     Solver -> IO a
h Solver
s IO a -> IO () -> IO a
forall a b. IO a -> IO b -> IO a
`finally` Solver -> IO ()
deleteSolver Solver
s

newSolver :: IO Solver
newSolver :: IO Solver
newSolver =
  do Solver
s <- IO Solver
minisat_new
     Solver -> Bool -> IO Bool
eliminate Solver
s Bool
True -- make the default behave as a normal solver (avoiding common bugs)
     Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
s

deleteSolver :: Solver -> IO ()
deleteSolver :: Solver -> IO ()
deleteSolver = Solver -> IO ()
minisat_delete

newLit :: Solver -> IO Lit
newLit :: Solver -> IO Lit
newLit = Solver -> IO Lit
minisat_newLit

neg :: Lit -> Lit
neg :: Lit -> Lit
neg = Lit -> Lit
minisat_negate

addClause :: Solver -> [Lit] -> IO Bool
addClause :: Solver -> [Lit] -> IO Bool
addClause Solver
s [Lit]
xs =
  do Solver -> IO ()
minisat_addClause_begin Solver
s
     [IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Solver -> Lit -> IO ()
minisat_addClause_addLit Solver
s Lit
x | Lit
x <- [Lit]
xs ]
     Solver -> IO Bool
minisat_addClause_commit Solver
s

simplify :: Solver -> IO Bool
simplify :: Solver -> IO Bool
simplify = Solver -> IO Bool
minisat_simplify

eliminate :: Solver -> Bool -> IO Bool
eliminate :: Solver -> Bool -> IO Bool
eliminate = Solver -> Bool -> IO Bool
minisat_eliminate

setFrozen :: Solver -> Var -> Bool -> IO ()
setFrozen :: Solver -> Var -> Bool -> IO ()
setFrozen = Solver -> Var -> Bool -> IO ()
minisat_setFrozen

isEliminated :: Solver -> Var -> IO Bool
isEliminated :: Solver -> Var -> IO Bool
isEliminated = Solver -> Var -> IO Bool
minisat_isEliminated

{-
solve :: Solver -> [Lit] -> Model a -> IO (Either [Lit] a)
-}

solve :: Solver -> [Lit] -> IO Bool
solve :: Solver -> [Lit] -> IO Bool
solve Solver
s [Lit]
xs =
  do Solver -> IO ()
minisat_solve_begin Solver
s
     [IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Solver -> Lit -> IO ()
minisat_solve_addLit Solver
s Lit
x | Lit
x <- [Lit]
xs ]
     Solver -> IO Bool
minisat_solve_commit Solver
s

limited_solve :: Solver -> [Lit] -> IO LBool
limited_solve :: Solver -> [Lit] -> IO LBool
limited_solve Solver
s [Lit]
xs =
  do Solver -> IO ()
minisat_solve_begin Solver
s
     [IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Solver -> Lit -> IO ()
minisat_solve_addLit Solver
s Lit
x | Lit
x <- [Lit]
xs ]
     Solver -> IO LBool
minisat_limited_solve_commit Solver
s

value, modelValue :: Solver -> Lit -> IO (Maybe Bool)
(Solver -> Lit -> IO (Maybe Bool)
value,Solver -> Lit -> IO (Maybe Bool)
modelValue) = ((Solver -> Lit -> IO LBool) -> Solver -> Lit -> IO (Maybe Bool)
forall (f :: * -> *) t t.
Functor f =>
(t -> t -> f LBool) -> t -> t -> f (Maybe Bool)
get Solver -> Lit -> IO LBool
minisat_value_Lit, (Solver -> Lit -> IO LBool) -> Solver -> Lit -> IO (Maybe Bool)
forall (f :: * -> *) t t.
Functor f =>
(t -> t -> f LBool) -> t -> t -> f (Maybe Bool)
get Solver -> Lit -> IO LBool
minisat_modelValue_Lit)
 where
  get :: (t -> t -> f LBool) -> t -> t -> f (Maybe Bool)
get t -> t -> f LBool
f t
s t
x = LBool -> Maybe Bool
mbool (LBool -> Maybe Bool) -> f LBool -> f (Maybe Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` t -> t -> f LBool
f t
s t
x

  mbool :: LBool -> Maybe Bool
mbool LBool
b 
    | LBool
b LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
l_False = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    | LBool
b LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
l_True  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
    | Bool
otherwise    = Maybe Bool
forall a. Maybe a
Nothing

conflict :: Solver -> IO [Lit]
conflict :: Solver -> IO [Lit]
conflict Solver
s =
  do Int
n <- Solver -> IO Int
minisat_conflict_len Solver
s
     [IO Lit] -> IO [Lit]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Solver -> Int -> IO Lit
minisat_conflict_nthLit Solver
s Int
i | Int
i <- [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]

-- TODO: Is it possible to FFI C constants, instead of using a dummy function?
l_True, l_False, l_Undef :: LBool
l_True :: LBool
l_True  = LBool
minisat_get_l_True
l_False :: LBool
l_False = LBool
minisat_get_l_False
l_Undef :: LBool
l_Undef = LBool
minisat_get_l_Undef

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

newtype Solver = MkSolver (Ptr ())
newtype Var    = MkVar CInt  deriving ( Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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 :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq Var
Ord )
newtype Lit    = MkLit CInt  deriving ( Lit -> Lit -> Bool
(Lit -> Lit -> Bool) -> (Lit -> Lit -> Bool) -> Eq Lit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lit -> Lit -> Bool
$c/= :: Lit -> Lit -> Bool
== :: Lit -> Lit -> Bool
$c== :: Lit -> Lit -> Bool
Eq, Eq Lit
Eq Lit
-> (Lit -> Lit -> Ordering)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Lit)
-> (Lit -> Lit -> Lit)
-> Ord Lit
Lit -> Lit -> Bool
Lit -> Lit -> Ordering
Lit -> Lit -> Lit
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 :: Lit -> Lit -> Lit
$cmin :: Lit -> Lit -> Lit
max :: Lit -> Lit -> Lit
$cmax :: Lit -> Lit -> Lit
>= :: Lit -> Lit -> Bool
$c>= :: Lit -> Lit -> Bool
> :: Lit -> Lit -> Bool
$c> :: Lit -> Lit -> Bool
<= :: Lit -> Lit -> Bool
$c<= :: Lit -> Lit -> Bool
< :: Lit -> Lit -> Bool
$c< :: Lit -> Lit -> Bool
compare :: Lit -> Lit -> Ordering
$ccompare :: Lit -> Lit -> Ordering
$cp1Ord :: Eq Lit
Ord )
newtype LBool  = MkLBool CInt deriving ( LBool -> LBool -> Bool
(LBool -> LBool -> Bool) -> (LBool -> LBool -> Bool) -> Eq LBool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LBool -> LBool -> Bool
$c/= :: LBool -> LBool -> Bool
== :: LBool -> LBool -> Bool
$c== :: LBool -> LBool -> Bool
Eq, Eq LBool
Eq LBool
-> (LBool -> LBool -> Ordering)
-> (LBool -> LBool -> Bool)
-> (LBool -> LBool -> Bool)
-> (LBool -> LBool -> Bool)
-> (LBool -> LBool -> Bool)
-> (LBool -> LBool -> LBool)
-> (LBool -> LBool -> LBool)
-> Ord LBool
LBool -> LBool -> Bool
LBool -> LBool -> Ordering
LBool -> LBool -> LBool
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 :: LBool -> LBool -> LBool
$cmin :: LBool -> LBool -> LBool
max :: LBool -> LBool -> LBool
$cmax :: LBool -> LBool -> LBool
>= :: LBool -> LBool -> Bool
$c>= :: LBool -> LBool -> Bool
> :: LBool -> LBool -> Bool
$c> :: LBool -> LBool -> Bool
<= :: LBool -> LBool -> Bool
$c<= :: LBool -> LBool -> Bool
< :: LBool -> LBool -> Bool
$c< :: LBool -> LBool -> Bool
compare :: LBool -> LBool -> Ordering
$ccompare :: LBool -> LBool -> Ordering
$cp1Ord :: Eq LBool
Ord )

instance Show Var where
  show :: Var -> String
show (MkVar CInt
n) = Char
'v' Char -> ShowS
forall a. a -> [a] -> [a]
: CInt -> String
forall a. Show a => a -> String
show CInt
n

instance Show Lit where
  show :: Lit -> String
show Lit
x = (if Lit -> Bool
minisat_sign Lit
x then String
"~" else String
"") String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Show a => a -> String
show (Lit -> Var
minisat_var Lit
x) 

instance Show LBool where
  show :: LBool -> String
show LBool
b
    | LBool
b LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
l_False = String
"False"
    | LBool
b LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
l_True  = String
"True"
    | Bool
otherwise    = String
"Undef"














foreign import ccall unsafe minisat_new :: IO (Solver)

{-# LINE 131 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_delete :: Solver -> IO (())

{-# LINE 132 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_newVar :: Solver -> IO (Var)

{-# LINE 133 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_newLit :: Solver -> IO (Lit)

{-# LINE 134 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_mkLit :: Var -> Lit

{-# LINE 135 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_mkLit_args :: Var -> Int -> Lit

{-# LINE 136 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_negate :: Lit -> Lit

{-# LINE 137 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_var :: Lit -> Var

{-# LINE 138 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_sign :: Lit -> Bool

{-# LINE 139 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_addClause :: Solver -> Int -> Ptr (Lit) -> IO (Bool)

{-# LINE 140 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_addClause_begin :: Solver -> IO (())

{-# LINE 141 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_addClause_addLit :: Solver -> Lit -> IO (())

{-# LINE 142 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_addClause_commit :: Solver -> IO (Bool)

{-# LINE 143 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_simplify :: Solver -> IO (Bool)

{-# LINE 144 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall safe minisat_solve :: Solver -> Int -> Ptr (Lit) -> IO (Bool)

{-# LINE 145 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_solve_begin :: Solver -> IO (())

{-# LINE 146 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_solve_addLit :: Solver -> Lit -> IO (())

{-# LINE 147 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall safe minisat_solve_commit :: Solver -> IO (Bool)

{-# LINE 148 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall safe minisat_limited_solve_commit :: Solver -> IO (LBool)

{-# LINE 149 "minisat-haskell-bindings/MiniSat.hsc" #-}

foreign import ccall safe minisat_interrupt :: Solver -> IO (())

{-# LINE 151 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall safe minisat_clearInterrupt :: Solver -> IO (())

{-# LINE 152 "minisat-haskell-bindings/MiniSat.hsc" #-}

foreign import ccall unsafe minisat_okay :: Solver -> IO (Bool)

{-# LINE 154 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_setPolarity :: Solver -> Var -> Int -> IO (())

{-# LINE 155 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_setDecisionVar :: Solver -> Var -> Int -> IO (())

{-# LINE 156 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_value_Var :: Solver -> Var -> IO (LBool)

{-# LINE 157 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_value_Lit :: Solver -> Lit -> IO (LBool)

{-# LINE 158 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_modelValue_Var :: Solver -> Var -> IO (LBool)

{-# LINE 159 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_modelValue_Lit :: Solver -> Lit -> IO (LBool)

{-# LINE 160 "minisat-haskell-bindings/MiniSat.hsc" #-}

foreign import ccall unsafe minisat_get_l_True :: LBool

{-# LINE 162 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_get_l_False :: LBool

{-# LINE 163 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_get_l_Undef :: LBool

{-# LINE 164 "minisat-haskell-bindings/MiniSat.hsc" #-}

-- // Simpsolver methods:
foreign import ccall unsafe minisat_setFrozen :: Solver -> Var -> Bool -> IO (())

{-# LINE 167 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_isEliminated :: Solver -> Var -> IO (Bool)

{-# LINE 168 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_eliminate :: Solver -> Bool -> IO (Bool)

{-# LINE 169 "minisat-haskell-bindings/MiniSat.hsc" #-}

foreign import ccall unsafe minisat_num_assigns :: Solver -> IO (Int)

{-# LINE 171 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_num_clauses :: Solver -> IO (Int)

{-# LINE 172 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_num_learnts :: Solver -> IO (Int)

{-# LINE 173 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_num_vars :: Solver -> IO (Int)

{-# LINE 174 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_num_freeVars :: Solver -> IO (Int)

{-# LINE 175 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_num_conflicts :: Solver -> IO (Int)

{-# LINE 176 "minisat-haskell-bindings/MiniSat.hsc" #-}

foreign import ccall unsafe minisat_conflict_len :: Solver -> IO (Int)

{-# LINE 178 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_conflict_nthLit :: Solver -> Int -> IO (Lit)

{-# LINE 179 "minisat-haskell-bindings/MiniSat.hsc" #-}
foreign import ccall unsafe minisat_set_verbosity :: Solver -> Int -> IO (())

{-# LINE 180 "minisat-haskell-bindings/MiniSat.hsc" #-}