-- Copyright (C) 2016 Peter Selinger.
--
-- This file is free software and may be distributed under the terms
-- of the MIT license. Please see the file LICENSE for details.

{-# LANGUAGE ForeignFunctionInterface #-}

-- | A low-level Haskell wrapper around the MiniSat-All library.

module SAT.MiniSat.LowLevel where

import Foreign
import Foreign.C.Types

-- ----------------------------------------------------------------------
-- * Some types

-- | An abstract type for the solver.
data C_Solver = C_Solver

-- | The marshalled \"int\" type from C.
type C_Int = Int32

-- | The marshalled \"lit\" type from the MiniSat library.
type C_Lit = C_Int

-- | The marshalled \"bool\" type from the MiniSat library.
type C_Bool = C_Int

-- | The marshalled \"lbool\" type from the MiniSat library.
type C_LBool = CChar

-- ----------------------------------------------------------------------
-- * Conversions

-- | Low-level wrapper around the C function /lit_new/.
foreign import ccall unsafe "solver.h lit_new"
  c_lit_new :: C_Int -> C_Bool -> C_Lit

-- ----------------------------------------------------------------------
-- * C API functions

-- | Low-level wrapper around the C function /solver_new/.
foreign import ccall unsafe "solver.h solver_new"
  c_solver_new :: IO (Ptr C_Solver)

-- | Low-level wrapper around the C function /solver_delete/.
foreign import ccall unsafe "solver.h solver_delete"
  c_solver_delete :: Ptr C_Solver -> IO ()

-- | Free a solver, callable by the garbage collector.
foreign import ccall unsafe "solver.h &solver_delete"
  c_solver_delete_ptr :: FinalizerPtr C_Solver

-- | Low-level wrapper around the C function /solver_addclause/.
foreign import ccall unsafe "solver.h solver_addclause"
  c_solver_addclause :: Ptr C_Solver -> Ptr C_Lit -> C_Int -> IO C_Bool

-- | Low-level wrapper around the C function /solver_solve_start/.
foreign import ccall unsafe "solver.h solver_solve_start"
  c_solver_solve_start :: Ptr C_Solver -> IO ()

-- | Low-level wrapper around the C function /solver_solve_next/.
foreign import ccall unsafe "solver.h solver_solve_next"
  c_solver_solve_next :: Ptr C_Solver -> IO C_Bool

-- | Low-level wrapper around the C function /solver_solve_finish/.
foreign import ccall unsafe "solver.h solver_solve_finish"
  c_solver_solve_finish :: Ptr C_Solver -> IO ()

-- | Low-level wrapper around the C function /solver_nvars/.
foreign import ccall unsafe "solver.h solver_nvars"
  c_solver_nvars :: Ptr C_Solver -> IO C_Int

-- | Low-level wrapper around the C function /solver_solution/.
foreign import ccall unsafe "solver.h solver_solution"
  c_solver_solution :: Ptr C_Solver -> IO (Ptr C_LBool)