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

98.67

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

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.PB.Internal.Adder
-- 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.Adder
  ( addPBLinAtLeastAdder
  , encodePBLinAtLeastWithPolarityAdder
  ) where

import Control.Monad
import Control.Monad.Primitive
import Data.Bits
import Data.Maybe
import Data.Primitive.MutVar
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import ToySolver.Data.Boolean
import qualified ToySolver.Internal.Data.SeqQueue as SQ
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))

addPBLinAtLeastAdder :: forall m. PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
addPBLinAtLeastAdder enc constr = do
  formula <- encodePBLinAtLeastAdder' enc constr
  Tseitin.addFormula enc formula

encodePBLinAtLeastWithPolarityAdder :: PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastWithPolarityAdder enc polarity constr = do
  formula <- encodePBLinAtLeastAdder' enc constr
  Tseitin.encodeFormulaWithPolarity enc polarity formula

encodePBLinAtLeastAdder' :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m Tseitin.Formula
encodePBLinAtLeastAdder' _ (_,rhs) | rhs <= 0 = return true
encodePBLinAtLeastAdder' enc (lhs,rhs) = do
  lhs1 <- encodePBLinSumAdder enc lhs
  let rhs1 = bits rhs
  if length lhs1 < length rhs1 then do
    return false
  else do
    let lhs2 = reverse lhs1
        rhs2 = replicate (length lhs1 - length rhs1) False ++ reverse rhs1
        f [] = true
        f ((x,False) : xs) = Atom x .||. f xs
        f ((x,True) : xs) = Atom x .&&. f xs
    return $ f (zip lhs2 rhs2)
  where
    bits :: Integer -> [Bool]
    bits n = f n 0
      where
        f 0 !_ = []
        f n i = testBit n i : f (clearBit n i) (i+1)

encodePBLinSumAdder :: forall m. PrimMonad m => Tseitin.Encoder m -> SAT.PBLinSum -> m [SAT.Lit]
encodePBLinSumAdder enc lhs = do
  (buckets :: MutVar (PrimState m) (Seq (SQ.SeqQueue m SAT.Lit))) <- newMutVar Seq.empty
  let insert :: Int -> Int -> m ()
      insert i x = do
        bs <- readMutVar buckets
        let n = Seq.length bs
        q <- if i < n then do
               return $ Seq.index bs i
             else do
               qs <- replicateM (i+1 - n) SQ.newFifo
               let bs' = bs Seq.>< Seq.fromList qs
               writeMutVar buckets bs'
               return $ Seq.index bs' i
        SQ.enqueue q x

      bits :: Integer -> [Int]
      bits n = f n 0
        where
          f 0 !_ = []
          f n i
            | testBit n i = i : f (clearBit n i) (i+1)
            | otherwise = f n (i+1)

  forM_ lhs $ \(c,x) -> do
    forM_ (bits c) $ \i -> insert i x

  let loop i ret = do
        bs <- readMutVar buckets
        let n = Seq.length bs
        if i >= n then do
          return $ reverse ret
        else do
          let q = Seq.index bs i
          m <- SQ.queueSize q
          case m of
            0 -> do
              b <- Tseitin.encodeDisj enc [] -- False
              loop (i+1) (b : ret)
            1 -> do
              b <- fromJust <$> SQ.dequeue q
              loop (i+1) (b : ret)
            2 -> do
              b1 <- fromJust <$> SQ.dequeue q
              b2 <- fromJust <$> SQ.dequeue q
              s <- encodeHASum enc b1 b2
              c <- encodeHACarry enc b1 b2
              insert (i+1) c
              loop (i+1) (s : ret)
            _ -> do
              b1 <- fromJust <$> SQ.dequeue q
              b2 <- fromJust <$> SQ.dequeue q
              b3 <- fromJust <$> SQ.dequeue q
              s <- Tseitin.encodeFASum enc b1 b2 b3
              c <- Tseitin.encodeFACarry enc b1 b2 b3
              insert i s
              insert (i+1) c
              loop i ret
  loop 0 []

encodeHASum :: PrimMonad m => Tseitin.Encoder m -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeHASum = Tseitin.encodeXOR

encodeHACarry :: PrimMonad m => Tseitin.Encoder m -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeHACarry enc a b = Tseitin.encodeConj enc [a,b]

1	{-# LANGUAGE BangPatterns #-}
2	{-# LANGUAGE FlexibleContexts #-}
3	{-# LANGUAGE ScopedTypeVariables #-}
4	{-# OPTIONS_GHC -Wall #-}
5	{-# OPTIONS_HADDOCK show-extensions #-}
6	-----------------------------------------------------------------------------
7	-- \|
8	-- Module : ToySolver.SAT.Encoder.PB.Internal.Adder
9	-- Copyright : (c) Masahiro Sakai 2016
10	-- License : BSD-style
11	--
12	-- Maintainer : masahiro.sakai@gmail.com
13	-- Stability : provisional
14	-- Portability : non-portable
15	--
16	-- References:
17	--
18	-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
19	-- Constraints into SAT. JSAT 2:1–26, 2006.
20	--
21	-----------------------------------------------------------------------------
22	module ToySolver.SAT.Encoder.PB.Internal.Adder
23	( addPBLinAtLeastAdder
24	, encodePBLinAtLeastWithPolarityAdder
25	) where
26
27	import Control.Monad
28	import Control.Monad.Primitive
29	import Data.Bits
30	import Data.Maybe
31	import Data.Primitive.MutVar
32	import Data.Sequence (Seq)
33	import qualified Data.Sequence as Seq
34	import ToySolver.Data.Boolean
35	import qualified ToySolver.Internal.Data.SeqQueue as SQ
36	import qualified ToySolver.SAT.Types as SAT
37	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
38	import ToySolver.SAT.Encoder.Tseitin (Formula (..))
39
40	addPBLinAtLeastAdder :: forall m. PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
41	addPBLinAtLeastAdder enc constr = do	1✔
42	formula <- encodePBLinAtLeastAdder' enc constr	1✔
43	Tseitin.addFormula enc formula	1✔
44
45	encodePBLinAtLeastWithPolarityAdder :: PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
46	encodePBLinAtLeastWithPolarityAdder enc polarity constr = do	1✔
47	formula <- encodePBLinAtLeastAdder' enc constr	1✔
48	Tseitin.encodeFormulaWithPolarity enc polarity formula	1✔
49
50	encodePBLinAtLeastAdder' :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m Tseitin.Formula
51	encodePBLinAtLeastAdder' _ (_,rhs) \| rhs <= 0 = return true	1✔
52	encodePBLinAtLeastAdder' enc (lhs,rhs) = do	1✔
53	lhs1 <- encodePBLinSumAdder enc lhs	1✔
54	let rhs1 = bits rhs	1✔
55	if length lhs1 < length rhs1 then do	1✔
56	return false	1✔
57	else do	1✔
58	let lhs2 = reverse lhs1	1✔
59	rhs2 = replicate (length lhs1 - length rhs1) False ++ reverse rhs1	1✔
60	f [] = true	1✔
61	f ((x,False) : xs) = Atom x .\|\|. f xs	1✔
62	f ((x,True) : xs) = Atom x .&&. f xs	1✔
63	return $ f (zip lhs2 rhs2)	1✔
64	where
65	bits :: Integer -> [Bool]
66	bits n = f n 0	1✔
67	where
68	f 0 !_ = []	1✔
69	f n i = testBit n i : f (clearBit n i) (i+1)	1✔
70
71	encodePBLinSumAdder :: forall m. PrimMonad m => Tseitin.Encoder m -> SAT.PBLinSum -> m [SAT.Lit]
72	encodePBLinSumAdder enc lhs = do	1✔
73	(buckets :: MutVar (PrimState m) (Seq (SQ.SeqQueue m SAT.Lit))) <- newMutVar Seq.empty	1✔
74	let insert :: Int -> Int -> m ()
75	insert i x = do	1✔
76	bs <- readMutVar buckets	1✔
77	let n = Seq.length bs	1✔
78	q <- if i < n then do	1✔
79	return $ Seq.index bs i	1✔
80	else do	1✔
81	qs <- replicateM (i+1 - n) SQ.newFifo	1✔
82	let bs' = bs Seq.>< Seq.fromList qs	1✔
83	writeMutVar buckets bs'	1✔
84	return $ Seq.index bs' i	1✔
85	SQ.enqueue q x	1✔
86
87	bits :: Integer -> [Int]
88	bits n = f n 0	1✔
89	where
90	f 0 !_ = []	1✔
91	f n i
92	\| testBit n i = i : f (clearBit n i) (i+1)	1✔
93	\| otherwise = f n (i+1)	×
94
95	forM_ lhs $ \(c,x) -> do	1✔
96	forM_ (bits c) $ \i -> insert i x	1✔
97
98	let loop i ret = do	1✔
99	bs <- readMutVar buckets	1✔
100	let n = Seq.length bs	1✔
101	if i >= n then do	1✔
102	return $ reverse ret	1✔
103	else do	1✔
104	let q = Seq.index bs i	1✔
105	m <- SQ.queueSize q	1✔
106	case m of	1✔
107	0 -> do	1✔
108	b <- Tseitin.encodeDisj enc [] -- False	1✔
109	loop (i+1) (b : ret)	1✔
110	1 -> do	1✔
111	b <- fromJust <$> SQ.dequeue q	1✔
112	loop (i+1) (b : ret)	1✔
113	2 -> do	1✔
114	b1 <- fromJust <$> SQ.dequeue q	1✔
115	b2 <- fromJust <$> SQ.dequeue q	1✔
116	s <- encodeHASum enc b1 b2	1✔
117	c <- encodeHACarry enc b1 b2	1✔
118	insert (i+1) c	1✔
119	loop (i+1) (s : ret)	1✔
120	_ -> do	1✔
121	b1 <- fromJust <$> SQ.dequeue q	1✔
122	b2 <- fromJust <$> SQ.dequeue q	1✔
123	b3 <- fromJust <$> SQ.dequeue q	1✔
124	s <- Tseitin.encodeFASum enc b1 b2 b3	1✔
125	c <- Tseitin.encodeFACarry enc b1 b2 b3	1✔
126	insert i s	1✔
127	insert (i+1) c	1✔
128	loop i ret	1✔
129	loop 0 []	1✔
130
131	encodeHASum :: PrimMonad m => Tseitin.Encoder m -> SAT.Lit -> SAT.Lit -> m SAT.Lit
132	encodeHASum = Tseitin.encodeXOR	1✔
133
134	encodeHACarry :: PrimMonad m => Tseitin.Encoder m -> SAT.Lit -> SAT.Lit -> m SAT.Lit
135	encodeHACarry enc a b = Tseitin.encodeConj enc [a,b]	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