msakai / toysolver / 496

Committed 10 Nov 2024 11:05AM UTC coverage: 69.994% (-1.1%) from 71.113%

Build # 496

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #117 from msakai/update-coveralls-and-haddock

GitHub Actions: Update coveralls and haddock configuration

Run Details

9872 of 14104 relevant lines covered (69.99%)

0.7 hits per line

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

92.86

/src/ToySolver/SAT/Encoder/PB/Internal/BDD.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.PB.Internal.BDD
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
--   Constraints into SAT. JSAT 2:1–26, 2006.
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.PB.Internal.BDD
  ( addPBLinAtLeastBDD
  , encodePBLinAtLeastWithPolarityBDD
  ) where

import Control.Monad.State.Strict
import Control.Monad.Primitive
import Data.Ord
import Data.List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

addPBLinAtLeastBDD :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
addPBLinAtLeastBDD enc constr = do
  l <- encodePBLinAtLeastWithPolarityBDD enc Tseitin.polarityPos constr
  SAT.addClause enc [l]

encodePBLinAtLeastWithPolarityBDD :: forall m. PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastWithPolarityBDD enc polarity (lhs,rhs) = do
  let lhs' = sortBy (flip (comparing fst)) lhs
  flip evalStateT Map.empty $ do
    let f :: SAT.PBLinSum -> Integer -> Integer -> StateT (Map (SAT.PBLinSum, Integer) SAT.Lit) m SAT.Lit
        f xs rhs slack
          | rhs <= 0  = lift $ Tseitin.encodeConjWithPolarity enc polarity [] -- true
          | slack < 0 = lift $ Tseitin.encodeDisjWithPolarity enc polarity [] -- false
          | otherwise = do
              m <- get
              case Map.lookup (xs,rhs) m of
                Just l -> return l
                Nothing -> do
                  case xs of
                    [] -> error "encodePBLinAtLeastBDD: should not happen"
                    [(_,l)] -> return l
                    (c,l) : xs' -> do
                      thenLit <- f xs' (rhs - c) slack
                      l2 <- lift $ Tseitin.encodeConjWithPolarity enc polarity [l, thenLit]
                      l3 <- if c > slack then
                              return l2
                            else do
                              elseLit <- f xs' rhs (slack - c)
                              lift $ Tseitin.encodeDisjWithPolarity enc polarity [l2, elseLit]
                      modify (Map.insert (xs,rhs) l3)
                      return l3
    f lhs' rhs (sum [c | (c,_) <- lhs'] - rhs)

1	{-# LANGUAGE FlexibleContexts #-}
2	{-# LANGUAGE ScopedTypeVariables #-}
3	{-# OPTIONS_GHC -Wall #-}
4	{-# OPTIONS_HADDOCK show-extensions #-}
5	-----------------------------------------------------------------------------
6	-- \|
7	-- Module : ToySolver.SAT.Encoder.PB.Internal.BDD
8	-- Copyright : (c) Masahiro Sakai 2016
9	-- License : BSD-style
10	--
11	-- Maintainer : masahiro.sakai@gmail.com
12	-- Stability : provisional
13	-- Portability : non-portable
14	--
15	-- References:
16	--
17	-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
18	-- Constraints into SAT. JSAT 2:1–26, 2006.
19	--
20	-----------------------------------------------------------------------------
21	module ToySolver.SAT.Encoder.PB.Internal.BDD
22	( addPBLinAtLeastBDD
23	, encodePBLinAtLeastWithPolarityBDD
24	) where
25
26	import Control.Monad.State.Strict
27	import Control.Monad.Primitive
28	import Data.Ord
29	import Data.List
30	import Data.Map.Strict (Map)
31	import qualified Data.Map.Strict as Map
32	import qualified ToySolver.SAT.Types as SAT
33	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
34
35	addPBLinAtLeastBDD :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
36	addPBLinAtLeastBDD enc constr = do	1✔
37	l <- encodePBLinAtLeastWithPolarityBDD enc Tseitin.polarityPos constr	1✔
38	SAT.addClause enc [l]	1✔
39
40	encodePBLinAtLeastWithPolarityBDD :: forall m. PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
41	encodePBLinAtLeastWithPolarityBDD enc polarity (lhs,rhs) = do	1✔
42	let lhs' = sortBy (flip (comparing fst)) lhs	1✔
43	flip evalStateT Map.empty $ do	1✔
44	let f :: SAT.PBLinSum -> Integer -> Integer -> StateT (Map (SAT.PBLinSum, Integer) SAT.Lit) m SAT.Lit
45	f xs rhs slack	1✔
46	\| rhs <= 0 = lift $ Tseitin.encodeConjWithPolarity enc polarity [] -- true	1✔
47	\| slack < 0 = lift $ Tseitin.encodeDisjWithPolarity enc polarity [] -- false	1✔
48	\| otherwise = do	×
49	m <- get	1✔
50	case Map.lookup (xs,rhs) m of	1✔
51	Just l -> return l	1✔
52	Nothing -> do	1✔
53	case xs of	1✔
54	[] -> error "encodePBLinAtLeastBDD: should not happen"	×
55	[(_,l)] -> return l	1✔
56	(c,l) : xs' -> do	1✔
57	thenLit <- f xs' (rhs - c) slack	1✔
58	l2 <- lift $ Tseitin.encodeConjWithPolarity enc polarity [l, thenLit]	1✔
59	l3 <- if c > slack then	1✔
60	return l2	1✔
61	else do	1✔
62	elseLit <- f xs' rhs (slack - c)	1✔
63	lift $ Tseitin.encodeDisjWithPolarity enc polarity [l2, elseLit]	1✔
64	modify (Map.insert (xs,rhs) l3)	1✔
65	return l3	1✔
66	f lhs' rhs (sum [c \| (c,_) <- lhs'] - rhs)	1✔

msakai / toysolver / 496

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