-----------------------------------------------------------------------------
-- |
-- 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
  { TheorySolver -> (Lit -> IO Bool) -> Lit -> IO Bool
thAssertLit :: (Lit -> IO Bool) -> Lit -> IO Bool
  , TheorySolver -> (Lit -> IO Bool) -> IO Bool
thCheck     :: (Lit -> IO Bool) -> IO Bool
  , TheorySolver -> Maybe Lit -> IO [Lit]
thExplain   :: Maybe Lit -> IO [Lit]
  , TheorySolver -> IO ()
thPushBacktrackPoint :: IO ()
  , TheorySolver -> IO ()
thPopBacktrackPoint  :: IO ()
  , TheorySolver -> IO ()
thConstructModel :: IO ()
  }

emptyTheory :: TheorySolver
emptyTheory :: TheorySolver
emptyTheory =
  TheorySolver
  { thAssertLit :: (Lit -> IO Bool) -> Lit -> IO Bool
thAssertLit = \Lit -> IO Bool
propagate Lit
lit -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  , thCheck :: (Lit -> IO Bool) -> IO Bool
thCheck = \Lit -> IO Bool
propagate -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  , thExplain :: Maybe Lit -> IO [Lit]
thExplain = \Maybe Lit
_ -> [Char] -> IO [Lit]
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
  , thPushBacktrackPoint :: IO ()
thPushBacktrackPoint = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , thPopBacktrackPoint :: IO ()
thPopBacktrackPoint  = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , thConstructModel :: IO ()
thConstructModel = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  }