content: -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.SAT.TheorySolver
  -- Copyright   :  (c) Masahiro Sakai 2012
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  portable
  --
  -----------------------------------------------------------------------------
  module ToySolver.SAT.TheorySolver
    ( TheorySolver (..)
    , emptyTheory
    ) where
  
  import ToySolver.SAT.Types
  
  data TheorySolver =
    TheorySolver
    { thAssertLit :: (Lit -> IO Bool) -> Lit -> IO Bool
    , thCheck     :: (Lit -> IO Bool) -> IO Bool
    , thExplain   :: Maybe Lit -> IO [Lit]
    , thPushBacktrackPoint :: IO ()
    , thPopBacktrackPoint  :: IO ()
    , thConstructModel :: IO ()
    }
  
  emptyTheory :: TheorySolver
  emptyTheory =
    TheorySolver
    { thAssertLit = \propagate lit -> return True
    , thCheck = \propagate -> return True
    , thExplain = \_ -> error "should not happen"
    , thPushBacktrackPoint = return ()
    , thPopBacktrackPoint  = return ()
    , thConstructModel = return ()
    }
  