msakai / toysolver / 797

Committed 09 May 2026 11:18AM UTC coverage: 71.463% (-0.4%) from 71.864%

Build # 797

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 2564c0a1a into 36153c78c

Coverage Stats

11046 of 15457 relevant lines covered (71.46%)

0.71 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

83.93

/src/ToySolver/SAT/PBO/Context.hs

{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.Context
-- Copyright   :  (c) Masahiro Sakai 2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.PBO.Context
  ( Context (..)
  , getBestValue
  , getBestModel
  , isOptimum
  , isFinished
  , getSearchUpperBound
  , setFinished

  , SimpleContext
  , newSimpleContext
  , newSimpleContext2
  , setOnUpdateBestSolution
  , setOnUpdateLowerBound
  , setLogger

  , Normalized
  , normalize
  ) where

import Control.Monad
import Control.Concurrent.STM
import Data.IORef
import Data.Maybe
import qualified ToySolver.SAT.Types as SAT

{--------------------------------------------------------------------
  Context class
--------------------------------------------------------------------}

class Context a where
  getObjectiveFunction :: a -> SAT.PBLinSum
  evalObjectiveFunction :: a -> SAT.Model -> Integer

  isUnsat         :: a -> STM Bool
  getBestSolution :: a -> STM (Maybe (SAT.Model, Integer))
  getLowerBound   :: a -> STM Integer

  setUnsat      :: a -> IO ()
  addSolution   :: a -> SAT.Model -> IO ()
  addLowerBound :: a -> Integer -> IO ()
  logMessage    :: a -> String -> IO ()

  evalObjectiveFunction c m = SAT.evalPBLinSum m (getObjectiveFunction c)

getBestValue :: Context a => a -> STM (Maybe Integer)
getBestValue cxt = liftM (fmap snd) $ getBestSolution cxt

getBestModel :: Context a => a -> STM (Maybe SAT.Model)
getBestModel cxt = liftM (fmap fst) $ getBestSolution cxt

isOptimum :: Context a => a -> STM Bool
isOptimum cxt = do
  ub <- getBestValue cxt
  lb <- getLowerBound cxt
  case ub of
    Nothing -> return False
    Just val -> return $ val <= lb
    -- Note that solving with the assumption 'obj < val' can yield
    -- a lower bound that is higher than val!

isFinished :: Context a => a -> STM Bool
isFinished cxt = do
  b1 <- isUnsat cxt
  b2 <- isOptimum cxt
  return $ b1 || b2

getSearchUpperBound :: Context a => a -> STM Integer
getSearchUpperBound ctx = do
  ret <- getBestValue ctx
  case ret of
    Just val -> return $ val - 1
    Nothing -> return $ SAT.pbLinUpperBound $ getObjectiveFunction ctx

setFinished :: Context a => a -> IO ()
setFinished cxt = do
  join $ atomically $ do
    ret <- getBestValue cxt
    case ret of
      Just val -> return $ addLowerBound cxt val
      Nothing -> return $ setUnsat cxt

{--------------------------------------------------------------------
  Simple Context
--------------------------------------------------------------------}

data SimpleContext
  = SimpleContext
  { scGetObjectiveFunction :: SAT.PBLinSum
  , scEvalObjectiveFunction :: SAT.Model -> Integer

  , scUnsatRef        :: TVar Bool
  , scBestSolutionRef :: TVar (Maybe (SAT.Model, Integer))
  , scLowerBoundRef   :: TVar Integer

  , scOnUpdateBestSolutionRef :: IORef (SAT.Model -> Integer -> IO ())
  , scOnUpdateLowerBoundRef   :: IORef (Integer -> IO ())
  , scLoggerRef               :: IORef (String -> IO ())
  }

instance Context SimpleContext where
  getObjectiveFunction = scGetObjectiveFunction
  evalObjectiveFunction = scEvalObjectiveFunction

  isUnsat sc = readTVar (scUnsatRef sc)
  getBestSolution sc = readTVar (scBestSolutionRef sc)
  getLowerBound sc = readTVar (scLowerBoundRef sc)

  setUnsat sc = do
    atomically $ do
      sol <- getBestSolution sc
      unless (isNothing sol) $ error "setUnsat: already has a solution" -- FIXME: use throwSTM?
      writeTVar (scUnsatRef sc) True

  addSolution sc m = do
    let !val = evalObjectiveFunction sc m
    join $ atomically $ do
      unsat <- isUnsat sc
      when unsat $ error "addSolution: already marked as unsatisfiable" -- FIXME: use throwSTM?

      sol0 <- getBestValue sc
      case sol0 of
        Just val0 | val0 <= val -> return $ return ()
        _ -> do
          writeTVar (scBestSolutionRef sc) (Just (m, val))
          return $ do
            h <- readIORef (scOnUpdateBestSolutionRef sc)
            h m val

  addLowerBound sc lb = do
    join $ atomically $ do
      lb0 <- getLowerBound sc
      if lb <= lb0 then
        return $ return ()
      else do
        writeTVar (scLowerBoundRef sc) lb
        return $ do
          h <- readIORef (scOnUpdateLowerBoundRef sc)
          h lb

  logMessage sc msg = do
    h <- readIORef (scLoggerRef sc)
    h msg

newSimpleContext :: SAT.PBLinSum -> IO SimpleContext
newSimpleContext obj = newSimpleContext2 obj (\m -> SAT.evalPBLinSum m obj)

newSimpleContext2 :: SAT.PBLinSum -> (SAT.Model -> Integer) -> IO SimpleContext
newSimpleContext2 obj obj2 = do
  unsatRef <- newTVarIO False
  bestsolRef <- newTVarIO Nothing
  lbRef <- newTVarIO $! SAT.pbLinLowerBound obj

  onUpdateBestSolRef <- newIORef $ \_ _ -> return ()
  onUpdateLBRef <- newIORef $ \_ -> return ()
  loggerRef <- newIORef $ \_ -> return ()

  return $
    SimpleContext
    { scGetObjectiveFunction = obj
    , scEvalObjectiveFunction = obj2

    , scUnsatRef        = unsatRef
    , scBestSolutionRef = bestsolRef
    , scLowerBoundRef   = lbRef

    , scOnUpdateBestSolutionRef = onUpdateBestSolRef
    , scOnUpdateLowerBoundRef   = onUpdateLBRef
    , scLoggerRef               = loggerRef
    }

setOnUpdateBestSolution :: SimpleContext -> (SAT.Model -> Integer -> IO ()) -> IO ()
setOnUpdateBestSolution sc h = writeIORef (scOnUpdateBestSolutionRef sc) h

setOnUpdateLowerBound :: SimpleContext -> (Integer -> IO ()) -> IO ()
setOnUpdateLowerBound sc h = writeIORef (scOnUpdateLowerBoundRef sc) h

setLogger :: SimpleContext -> (String -> IO ()) -> IO ()
setLogger sc h = writeIORef (scLoggerRef sc) h

{--------------------------------------------------------------------
  Normalization
--------------------------------------------------------------------}

data Normalized a
  = Normalized
  { nBase :: a
  , nObjectiveFunction :: SAT.PBLinSum
  , nOffset :: Integer
  }

instance Context a => Context (Normalized a) where
  getObjectiveFunction = nObjectiveFunction

  evalObjectiveFunction cxt m = evalObjectiveFunction (nBase cxt) m - nOffset cxt

  isUnsat cxt = isUnsat (nBase cxt)

  getBestSolution cxt = do
    sol <- getBestSolution (nBase cxt)
    case sol of
      Nothing -> return Nothing
      Just (m, val) -> return $ Just (m, val - nOffset cxt)

  getLowerBound cxt = do
    lb <- getLowerBound (nBase cxt)
    return $ lb - nOffset cxt

  setUnsat cxt = setUnsat $ nBase cxt

  addSolution cxt m = do
    addSolution (nBase cxt) m

  addLowerBound cxt lb = do
    addLowerBound (nBase cxt) (lb + nOffset cxt)

  logMessage cxt msg = logMessage (nBase cxt) msg

normalize :: Context a => a -> Normalized a
normalize cxt = Normalized cxt obj' offset
  where
    obj = getObjectiveFunction cxt
    (obj',offset) = SAT.normalizePBLinSum (obj, 0)


1	{-# LANGUAGE BangPatterns #-}
2	{-# OPTIONS_GHC -Wall #-}
3	{-# OPTIONS_HADDOCK show-extensions #-}
4	-----------------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.SAT.PBO.Context
7	-- Copyright : (c) Masahiro Sakai 2014
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : provisional
12	-- Portability : non-portable
13	--
14	-----------------------------------------------------------------------------
15	module ToySolver.SAT.PBO.Context
16	( Context (..)
17	, getBestValue
18	, getBestModel
19	, isOptimum
20	, isFinished
21	, getSearchUpperBound
22	, setFinished
23
24	, SimpleContext
25	, newSimpleContext
26	, newSimpleContext2
27	, setOnUpdateBestSolution
28	, setOnUpdateLowerBound
29	, setLogger
30
31	, Normalized
32	, normalize
33	) where
34
35	import Control.Monad
36	import Control.Concurrent.STM
37	import Data.IORef
38	import Data.Maybe
39	import qualified ToySolver.SAT.Types as SAT
40
41	{--------------------------------------------------------------------
42	Context class
43	--------------------------------------------------------------------}
44
45	class Context a where
46	getObjectiveFunction :: a -> SAT.PBLinSum
47	evalObjectiveFunction :: a -> SAT.Model -> Integer
48
49	isUnsat :: a -> STM Bool
50	getBestSolution :: a -> STM (Maybe (SAT.Model, Integer))
51	getLowerBound :: a -> STM Integer
52
53	setUnsat :: a -> IO ()
54	addSolution :: a -> SAT.Model -> IO ()
55	addLowerBound :: a -> Integer -> IO ()
56	logMessage :: a -> String -> IO ()
57
58	evalObjectiveFunction c m = SAT.evalPBLinSum m (getObjectiveFunction c)	×
59
60	getBestValue :: Context a => a -> STM (Maybe Integer)
61	getBestValue cxt = liftM (fmap snd) $ getBestSolution cxt	1✔
62
63	getBestModel :: Context a => a -> STM (Maybe SAT.Model)
64	getBestModel cxt = liftM (fmap fst) $ getBestSolution cxt	×
65
66	isOptimum :: Context a => a -> STM Bool
67	isOptimum cxt = do	1✔
68	ub <- getBestValue cxt	1✔
69	lb <- getLowerBound cxt	1✔
70	case ub of	1✔
71	Nothing -> return False	1✔
72	Just val -> return $ val <= lb	1✔
73	-- Note that solving with the assumption 'obj < val' can yield
74	-- a lower bound that is higher than val!
75
76	isFinished :: Context a => a -> STM Bool
77	isFinished cxt = do	1✔
78	b1 <- isUnsat cxt	1✔
79	b2 <- isOptimum cxt	1✔
80	return $ b1 \|\| b2	1✔
81
82	getSearchUpperBound :: Context a => a -> STM Integer
83	getSearchUpperBound ctx = do	1✔
84	ret <- getBestValue ctx	1✔
85	case ret of	1✔
86	Just val -> return $ val - 1	1✔
87	Nothing -> return $ SAT.pbLinUpperBound $ getObjectiveFunction ctx	1✔
88
89	setFinished :: Context a => a -> IO ()
90	setFinished cxt = do	1✔
91	join $ atomically $ do	1✔
92	ret <- getBestValue cxt	1✔
93	case ret of	1✔
94	Just val -> return $ addLowerBound cxt val	1✔
95	Nothing -> return $ setUnsat cxt	1✔
96
97	{--------------------------------------------------------------------
98	Simple Context
99	--------------------------------------------------------------------}
100
101	data SimpleContext
102	= SimpleContext
103	{ scGetObjectiveFunction :: SAT.PBLinSum	1✔
104	, scEvalObjectiveFunction :: SAT.Model -> Integer	1✔
105
106	, scUnsatRef :: TVar Bool	1✔
107	, scBestSolutionRef :: TVar (Maybe (SAT.Model, Integer))	1✔
108	, scLowerBoundRef :: TVar Integer	1✔
109
110	, scOnUpdateBestSolutionRef :: IORef (SAT.Model -> Integer -> IO ())	1✔
111	, scOnUpdateLowerBoundRef :: IORef (Integer -> IO ())	1✔
112	, scLoggerRef :: IORef (String -> IO ())	1✔
113	}
114
115	instance Context SimpleContext where
116	getObjectiveFunction = scGetObjectiveFunction	1✔
117	evalObjectiveFunction = scEvalObjectiveFunction	1✔
118
119	isUnsat sc = readTVar (scUnsatRef sc)	1✔
120	getBestSolution sc = readTVar (scBestSolutionRef sc)	1✔
121	getLowerBound sc = readTVar (scLowerBoundRef sc)	1✔
122
123	setUnsat sc = do	1✔
124	atomically $ do	1✔
125	sol <- getBestSolution sc	1✔
126	unless (isNothing sol) $ error "setUnsat: already has a solution" -- FIXME: use throwSTM?	×
127	writeTVar (scUnsatRef sc) True	1✔
128
129	addSolution sc m = do	1✔
130	let !val = evalObjectiveFunction sc m	1✔
131	join $ atomically $ do	1✔
132	unsat <- isUnsat sc	1✔
133	when unsat $ error "addSolution: already marked as unsatisfiable" -- FIXME: use throwSTM?	×
134
135	sol0 <- getBestValue sc	1✔
136	case sol0 of	1✔
137	Just val0 \| val0 <= val -> return $ return ()	×
138	_ -> do	1✔
139	writeTVar (scBestSolutionRef sc) (Just (m, val))	1✔
140	return $ do	1✔
141	h <- readIORef (scOnUpdateBestSolutionRef sc)	1✔
142	h m val	×
143
144	addLowerBound sc lb = do	1✔
145	join $ atomically $ do	1✔
146	lb0 <- getLowerBound sc	1✔
147	if lb <= lb0 then	1✔
148	return $ return ()	×
149	else do	1✔
150	writeTVar (scLowerBoundRef sc) lb	1✔
151	return $ do	1✔
152	h <- readIORef (scOnUpdateLowerBoundRef sc)	1✔
153	h lb	×
154
155	logMessage sc msg = do	1✔
156	h <- readIORef (scLoggerRef sc)	1✔
157	h msg	×
158
159	newSimpleContext :: SAT.PBLinSum -> IO SimpleContext
160	newSimpleContext obj = newSimpleContext2 obj (\m -> SAT.evalPBLinSum m obj)	×
161
162	newSimpleContext2 :: SAT.PBLinSum -> (SAT.Model -> Integer) -> IO SimpleContext
163	newSimpleContext2 obj obj2 = do	1✔
164	unsatRef <- newTVarIO False	1✔
165	bestsolRef <- newTVarIO Nothing	1✔
166	lbRef <- newTVarIO $! SAT.pbLinLowerBound obj	1✔
167
168	onUpdateBestSolRef <- newIORef $ \_ _ -> return ()	×
169	onUpdateLBRef <- newIORef $ \_ -> return ()	×
170	loggerRef <- newIORef $ \_ -> return ()	×
171
172	return $	1✔
173	SimpleContext	1✔
174	{ scGetObjectiveFunction = obj	1✔
175	, scEvalObjectiveFunction = obj2	1✔
176
177	, scUnsatRef = unsatRef	1✔
178	, scBestSolutionRef = bestsolRef	1✔
179	, scLowerBoundRef = lbRef	1✔
180
181	, scOnUpdateBestSolutionRef = onUpdateBestSolRef	1✔
182	, scOnUpdateLowerBoundRef = onUpdateLBRef	1✔
183	, scLoggerRef = loggerRef	1✔
184	}
185
186	setOnUpdateBestSolution :: SimpleContext -> (SAT.Model -> Integer -> IO ()) -> IO ()
187	setOnUpdateBestSolution sc h = writeIORef (scOnUpdateBestSolutionRef sc) h	×
188
189	setOnUpdateLowerBound :: SimpleContext -> (Integer -> IO ()) -> IO ()
190	setOnUpdateLowerBound sc h = writeIORef (scOnUpdateLowerBoundRef sc) h	×
191
192	setLogger :: SimpleContext -> (String -> IO ()) -> IO ()
193	setLogger sc h = writeIORef (scLoggerRef sc) h	×
194
195	{--------------------------------------------------------------------
196	Normalization
197	--------------------------------------------------------------------}
198
199	data Normalized a
200	= Normalized
201	{ nBase :: a	1✔
202	, nObjectiveFunction :: SAT.PBLinSum	1✔
203	, nOffset :: Integer	1✔
204	}
205
206	instance Context a => Context (Normalized a) where
207	getObjectiveFunction = nObjectiveFunction	1✔
208
209	evalObjectiveFunction cxt m = evalObjectiveFunction (nBase cxt) m - nOffset cxt	1✔
210
211	isUnsat cxt = isUnsat (nBase cxt)	1✔
212
213	getBestSolution cxt = do	1✔
214	sol <- getBestSolution (nBase cxt)	1✔
215	case sol of	1✔
216	Nothing -> return Nothing	1✔
217	Just (m, val) -> return $ Just (m, val - nOffset cxt)	×
218
219	getLowerBound cxt = do	1✔
220	lb <- getLowerBound (nBase cxt)	1✔
221	return $ lb - nOffset cxt	1✔
222
223	setUnsat cxt = setUnsat $ nBase cxt	1✔
224
225	addSolution cxt m = do	1✔
226	addSolution (nBase cxt) m	1✔
227
228	addLowerBound cxt lb = do	1✔
229	addLowerBound (nBase cxt) (lb + nOffset cxt)	1✔
230
231	logMessage cxt msg = logMessage (nBase cxt) msg	×
232
233	normalize :: Context a => a -> Normalized a
234	normalize cxt = Normalized cxt obj' offset	1✔
235	where
236	obj = getObjectiveFunction cxt	1✔
237	(obj',offset) = SAT.normalizePBLinSum (obj, 0)	1✔
238

msakai / toysolver / 797

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous