toysolver-0.7.0: src/ToySolver/SAT/TheorySolver.hs

-----------------------------------------------------------------------------
-- |
-- 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 ()
  }