IPASIR.hs

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IPASIR () where

import Control.Exception
import Control.Monad
import Data.Int
import qualified Data.IntSet as IntSet
import Data.IORef
import Foreign
import Foreign.C

import qualified ToySolver.SAT as SAT


type Solver = Ptr ()

type SolverRep = (SAT.Solver, IORef [Int32], IORef [Int32])

withSolverRep :: Solver -> (SolverRep -> IO a) -> IO a
withSolverRep ptr k = do
  let sptr :: StablePtr SolverRep
      sptr = castPtrToStablePtr ptr
  solver <- deRefStablePtr sptr
  k solver

ensureVars :: SAT.Solver -> [Int32] -> IO ()
ensureVars _solver [] = return ()
ensureVars solver lits = do
  let maxVar = maximum $ map (abs . fromIntegral) lits
  nv <- SAT.getNVars solver
  when (nv < maxVar) $ SAT.newVars_ solver (maxVar - nv)


foreign export ccall "toysat_ipasir_init" ipasir_init :: IO Solver

-- | Construct a new solver and return a pointer to it.
--
-- Use the returned pointer as the first parameter in each
-- of the following functions.
--
-- Required state: N/A
--
-- State after: @INPUT@
ipasir_init :: IO Solver
ipasir_init = do
  solver <- SAT.newSolver
  addBuf <- newIORef []
  assumptionRef <- newIORef []
  sptr <- newStablePtr (solver, addBuf, assumptionRef)
  return (castStablePtrToPtr sptr)


foreign export ccall "toysat_ipasir_release" ipasir_release :: Solver -> IO ()

-- | Release the solver, i.e., all its resoruces and
-- allocated memory (destructor). The solver pointer
-- cannot be used for any purposes after this call.
--
-- Required state: @INPUT@ or @SAT@ or @UNSAT@
--
-- State after: undefined
ipasir_release :: Solver -> IO ()
ipasir_release ptr = do
  let sptr :: StablePtr SolverRep
      sptr = castPtrToStablePtr ptr
  freeStablePtr sptr


foreign export ccall ipasir_add :: Solver -> Int32 -> IO ()

-- | Add the given literal into the currently added clause
-- or finalize the clause with a 0.
--
-- Clauses added this way cannot be removed. The addition of
-- removable clauses can be simulated using activation literals
-- and assumptions.
--
-- Required state: @INPUT@ or @SAT@ or @UNSAT@
--
-- State after: @INPUT@
--
-- Literals are encoded as (non-zero) integers as in the
-- DIMACS formats.  They have to be smaller or equal to
-- @INT_MAX@ and strictly larger than @INT_MIN@ (to avoid
-- negation overflow).  This applies to all the literal
-- arguments in API functions.
ipasir_add :: Solver -> Int32 -> IO ()
ipasir_add ptr lit = withSolverRep ptr $ \(solver, addBuf, _assumptionRef) -> do
  if lit == 0 then do
    lits <- readIORef addBuf
    ensureVars solver lits
    SAT.addClause solver (map fromIntegral (reverse lits))
  else do
    modifyIORef addBuf (lit :)


foreign export ccall ipasir_assume :: Solver -> Int32 -> IO ()

-- | Add an assumption for the next SAT search (the next call
-- of ipasir_solve).
--
-- After calling 'ipasir_solve' all the previously added assumptions
-- are cleared.
--
-- Required state: @INPUT@ or @SAT@ or @UNSAT@
--
-- State after: @INPUT@
ipasir_assume :: Solver -> Int32 -> IO ()
ipasir_assume ptr lit = withSolverRep ptr $ \(_solver, _addBuf, assumptionRef) -> do
  modifyIORef assumptionRef (lit :)


foreign export ccall ipasir_solve :: Solver -> IO CInt

-- | Solve the formula with specified clauses under the specified assumptions.
--
-- * If the formula is satisfiable the function returns 10 and the state of the solver is changed to @SAT@.
-- * If the formula is unsatisfiable the function returns 20 and the state of the solver is changed to @UNSAT@.
-- * If the search is interrupted (see 'ipasir_set_terminate') the function returns 0 and the state of the solver is changed to @INPUT@.
--
-- This function can be called in any defined state of the solver.
-- Note that the state of the solver _during_ execution of @ipasir_solve@ is undefined.
--
-- Required state: @INPUT@ or @SAT@ or @UNSAT@
--
-- State after: @INPUT@ or @SAT@ or @UNSAT@
ipasir_solve :: Solver -> IO CInt
ipasir_solve ptr = withSolverRep ptr $ \(solver, _addBuf, assumptionRef) -> do
  assumptions <- readIORef assumptionRef
  writeIORef assumptionRef []
  ensureVars solver (assumptions)
  handle (\(_ :: SAT.Canceled) -> return 0) $ do
    ret <- SAT.solveWith solver (map fromIntegral assumptions)
    if ret then do
      return 10
    else do
      return 20

foreign export ccall ipasir_val :: Solver -> Int32 -> IO CInt

-- | Get the truth value of the given literal in the found satisfying
-- assignment.
--
-- Return @lit@ if True, @-lit@ if False;
-- @ipasir_val(lit)@ may return 0 if the found assignment is satisfying for both valuations of lit.
-- Each solution that agrees with all non-zero values of @ipasir_val@ is a model of the formula.
--
-- This function can only be used if 'ipasir_solve' has returned @10@
-- and no 'ipasir_add' nor 'ipasir_assume' has been called
-- since then, i.e., the state of the solver is SAT.
--
-- Required state: @SAT@
--
-- State after: @SAT@
ipasir_val :: Solver -> Int32 -> IO CInt
ipasir_val ptr lit = withSolverRep ptr $ \(solver, _addBuf, _assumptionRef) -> do
  nv <- SAT.getNVars solver
  if nv < abs (fromIntegral lit) then do
    return 0
  else do
    m <- SAT.getModel solver
    if SAT.evalLit m (fromIntegral lit) then
      return (fromIntegral lit)
    else
      return (- fromIntegral lit)


foreign export ccall ipasir_failed :: Solver -> Int32 -> IO CInt

-- | Check if the given assumption literal was used to prove the
-- unsatisfiability of the formula under the assumptions
-- used for the last SAT search. Return 1 if so, 0 otherwise.
--
-- The formula remains unsatisfiable even just under assumption literals for which @ipasir_failed@ returns 1.
-- Note that for literals @lit@ which are not assumption literals, the behavior of @ipasir_failed(lit)@ is not specified.
--
-- This function can only be used if 'ipasir_solve' has returned 20 and
-- no 'ipasir_add' or 'ipasir_assume' has been called since then, i.e.,
-- the state of the solver is @UNSAT@.
--
-- Required state: @UNSAT@
--
-- State after: @UNSAT@
ipasir_failed :: Solver -> Int32 -> IO CInt
ipasir_failed ptr lit = withSolverRep ptr $ \(solver, _addBuf, _assumptionRef) -> do
  failedLits <- SAT.getFailedAssumptions solver
  return $ if IntSet.member (fromIntegral lit) failedLits then 1 else 0


foreign export ccall ipasir_set_terminate :: Solver -> Ptr a -> FunPtr (Ptr a -> IO CInt) -> IO ()

-- | Set a callback function used to indicate a termination requirement to the
-- solver.
--
-- The solver will periodically call this function and check its return
-- value during the search. The @ipasir_set_terminate@ function can be called in any
-- state of the solver, the state remains unchanged after the call.
-- The callback function is of the form "@int terminate(void * data)@x"
--
-- * it returns a non-zero value if the solver should terminate.
-- * the solver calls the callback function with the parameter "data"
--   having the value passed in the @ipasir_set_terminate@ function (2nd parameter).
--
-- Required state: @INPUT@ or @SAT@ or @UNSAT@
--
-- State after: @INPUT@ or @SAT@ or @UNSAT@
ipasir_set_terminate :: Solver -> Ptr a -> FunPtr (Ptr a -> IO CInt) -> IO ()
ipasir_set_terminate ptr info funptr = withSolverRep ptr $ \(solver, _addBuf, _assumptionRef) -> do
  if funptr == nullFunPtr then do
    SAT.clearTerminateCallback solver
  else do
    let callback = mkTerminateCallback funptr
    SAT.setTerminateCallback solver $ do
      ret <- callback info
      return (ret /= 0)


foreign export ccall ipasir_set_learn :: Solver -> Ptr a -> CInt -> FunPtr (Ptr a -> Ptr Int32 -> IO ()) -> IO ()

-- | Set a callback function used to extract learned clauses up to a given length from the
-- solver.
--
-- The solver will call this function for each learned clause that satisfies
-- the maximum length (literal count) condition. The @ipasir_set_learn@ function can be called in any
-- state of the solver, the state remains unchanged after the call.
-- The callback function is of the form "@void learn(void * data, int * clause)@"
--
-- * the solver calls the callback function with the parameter "data"
--   having the value passed in the @ipasir_set_learn@ function (2nd parameter).
-- * the argument "clause" is a pointer to a null terminated integer array containing the learned clause.
--   the solver can change the data at the memory location that "clause" points to after the function call.
--
-- Required state: @INPUT@ or @SAT@ or @UNSAT@
--
-- State after: @INPUT@ or @SAT@ or @UNSAT@
ipasir_set_learn :: Solver -> Ptr a -> CInt -> FunPtr (Ptr a -> Ptr Int32 -> IO ()) -> IO ()
ipasir_set_learn ptr info max_length funptr = withSolverRep ptr $ \(solver, _addBuf, _assumptionRef) -> do
  if funptr == nullFunPtr then do
    SAT.clearLearnCallback solver
  else do
    let callback = mkLearnCallback funptr
    SAT.setLearnCallback solver $ \clause -> do
      when (length clause <= fromIntegral max_length) $ do
        withArray0 0 (map fromIntegral clause) (callback info)

foreign import ccall "dynamic" mkTerminateCallback :: FunPtr (Ptr a -> IO CInt) -> (Ptr a -> IO CInt)

foreign import ccall "dynamic" mkLearnCallback :: FunPtr (Ptr a -> Ptr Int32 -> IO ()) -> (Ptr a -> Ptr Int32 -> IO ())