msakai / toysolver / 517

Committed 24 Nov 2024 02:02PM UTC coverage: 69.746% (-0.7%) from 70.447%

Build # 517

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #123 from msakai/feature/reduce-transformers-2

Change SimplifyMaxSAT2Info and SAT3ToMaxSAT2Info to be synonyms of TseitinInfo

Run Details

5 of 5 new or added lines in 1 file covered. (100.0%)

127 existing lines in 13 files now uncovered.

9816 of 14074 relevant lines covered (69.75%)

0.7 hits per line

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

86.0

/src/ToySolver/SAT/Encoder/Cardinality/Internal/ParallelCounter.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
-- Copyright   :  (c) Masahiro Sakai 2019
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
  ( addAtLeastParallelCounter
  , encodeAtLeastWithPolarityParallelCounter
  ) where

import Control.Monad.Primitive
import Control.Monad.State.Strict
import Data.Bits
import Data.Vector (Vector)
import qualified Data.Vector as V
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

addAtLeastParallelCounter :: PrimMonad m => Tseitin.Encoder m -> SAT.AtLeast -> m ()
addAtLeastParallelCounter enc constr = do
  l <- encodeAtLeastWithPolarityParallelCounter enc Tseitin.polarityPos constr
  SAT.addClause enc [l]

encodeAtLeastWithPolarityParallelCounter :: forall m. PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> SAT.AtLeast -> m SAT.Lit
encodeAtLeastWithPolarityParallelCounter enc polarity (lhs,rhs) = do
  if rhs <= 0 then
    Tseitin.encodeConjWithPolarity enc polarity []
  else if length lhs < rhs then
    Tseitin.encodeDisjWithPolarity enc polarity []
  else do
    let rhs_bits = bits (fromIntegral rhs)
    (cnt, overflowBits) <- encodeSumParallelCounter enc (length rhs_bits) lhs
    isGE <- encodeGE enc polarity cnt rhs_bits
    Tseitin.encodeDisjWithPolarity enc polarity $ isGE : overflowBits
  where
    bits :: Integer -> [Bool]
    bits n = f n 0
      where
        f 0 !_ = []
        f n i = testBit n i : f (clearBit n i) (i+1)

encodeSumParallelCounter :: forall m. PrimMonad m => Tseitin.Encoder m -> Int -> [SAT.Lit] -> m ([SAT.Lit], [SAT.Lit])
encodeSumParallelCounter enc w lits = do
  let add :: [SAT.Lit] -> [SAT.Lit] -> SAT.Lit -> StateT [SAT.Lit] m [SAT.Lit]
      add = go 0 []
        where
          go :: Int -> [SAT.Lit] -> [SAT.Lit] -> [SAT.Lit] -> SAT.Lit -> StateT [SAT.Lit] m [SAT.Lit]
          go i ret _xs _ys c | i == w = do
            modify (c:)
            return $ reverse ret
          go _i ret [] [] c = return $ reverse (c : ret)
          go i ret (x : xs) (y : ys) c = do
            z <- lift $ Tseitin.encodeFASum enc x y c
            c' <- lift $ Tseitin.encodeFACarry enc x y c
            go (i+1) (z : ret) xs ys c'
          go _ _ _ _ _ = error "encodeSumParallelCounter: should not happen"

      f :: Vector SAT.Lit -> StateT [SAT.Lit] m [SAT.Lit]
      f xs
        | V.null xs = return []
        | otherwise = do
            let len2 = V.length xs `div` 2
            cnt1 <- f (V.slice 0 len2 xs)
            cnt2 <- f (V.slice len2 len2 xs)
            c <- if V.length xs `mod` 2 == 0 then
                   lift $ Tseitin.encodeDisj enc []
                 else
                   lift $ return $ xs V.! (V.length xs - 1)
            add cnt1 cnt2 c

  runStateT (f (V.fromList lits)) []

encodeGE :: forall m. PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> [SAT.Lit] -> [Bool] -> m SAT.Lit
encodeGE enc polarity lhs rhs = do
  let f :: [SAT.Lit] -> [Bool] -> SAT.Lit -> m SAT.Lit
      f [] [] r = return r
      f [] (True  : _) _ = Tseitin.encodeDisjWithPolarity enc polarity [] -- false
      f [] (False : bs) r = f [] bs r
      f (l : ls) (True  : bs) r = do
        f ls bs =<< Tseitin.encodeConjWithPolarity enc polarity [l, r]
      f (l : ls) (False : bs) r = do
        f ls bs =<< Tseitin.encodeDisjWithPolarity enc polarity [l, r]
      f (l : ls) [] r = do
        f ls [] =<< Tseitin.encodeDisjWithPolarity enc polarity [l, r]
  t <- Tseitin.encodeConjWithPolarity enc polarity [] -- true
  f lhs rhs t

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE BangPatterns #-}
4	{-# LANGUAGE ScopedTypeVariables #-}
5	-----------------------------------------------------------------------------
6	-- \|
7	-- Module : ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
8	-- Copyright : (c) Masahiro Sakai 2019
9	-- License : BSD-style
10	--
11	-- Maintainer : masahiro.sakai@gmail.com
12	-- Stability : provisional
13	-- Portability : non-portable
14	--
15	-----------------------------------------------------------------------------
16	module ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
17	( addAtLeastParallelCounter
18	, encodeAtLeastWithPolarityParallelCounter
19	) where
20
21	import Control.Monad.Primitive
22	import Control.Monad.State.Strict
23	import Data.Bits
24	import Data.Vector (Vector)
25	import qualified Data.Vector as V
26	import qualified ToySolver.SAT.Types as SAT
27	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
28
29	addAtLeastParallelCounter :: PrimMonad m => Tseitin.Encoder m -> SAT.AtLeast -> m ()
30	addAtLeastParallelCounter enc constr = do	1✔
31	l <- encodeAtLeastWithPolarityParallelCounter enc Tseitin.polarityPos constr	1✔
32	SAT.addClause enc [l]	1✔
33
34	encodeAtLeastWithPolarityParallelCounter :: forall m. PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> SAT.AtLeast -> m SAT.Lit
35	encodeAtLeastWithPolarityParallelCounter enc polarity (lhs,rhs) = do	1✔
36	if rhs <= 0 then	1✔
37	Tseitin.encodeConjWithPolarity enc polarity []	1✔
38	else if length lhs < rhs then	1✔
39	Tseitin.encodeDisjWithPolarity enc polarity []	1✔
40	else do	1✔
41	let rhs_bits = bits (fromIntegral rhs)	1✔
42	(cnt, overflowBits) <- encodeSumParallelCounter enc (length rhs_bits) lhs	1✔
43	isGE <- encodeGE enc polarity cnt rhs_bits	1✔
44	Tseitin.encodeDisjWithPolarity enc polarity $ isGE : overflowBits	1✔
45	where
46	bits :: Integer -> [Bool]
47	bits n = f n 0	1✔
48	where
49	f 0 !_ = []	1✔
50	f n i = testBit n i : f (clearBit n i) (i+1)	1✔
51
52	encodeSumParallelCounter :: forall m. PrimMonad m => Tseitin.Encoder m -> Int -> [SAT.Lit] -> m ([SAT.Lit], [SAT.Lit])
53	encodeSumParallelCounter enc w lits = do	1✔
54	let add :: [SAT.Lit] -> [SAT.Lit] -> SAT.Lit -> StateT [SAT.Lit] m [SAT.Lit]
55	add = go 0 []	1✔
56	where
57	go :: Int -> [SAT.Lit] -> [SAT.Lit] -> [SAT.Lit] -> SAT.Lit -> StateT [SAT.Lit] m [SAT.Lit]
58	go i ret _xs _ys c \| i == w = do	1✔
59	modify (c:)	1✔
60	return $ reverse ret	1✔
61	go _i ret [] [] c = return $ reverse (c : ret)	1✔
62	go i ret (x : xs) (y : ys) c = do	1✔
63	z <- lift $ Tseitin.encodeFASum enc x y c	1✔
64	c' <- lift $ Tseitin.encodeFACarry enc x y c	1✔
65	go (i+1) (z : ret) xs ys c'	1✔
66	go _ _ _ _ _ = error "encodeSumParallelCounter: should not happen"	×
67
68	f :: Vector SAT.Lit -> StateT [SAT.Lit] m [SAT.Lit]
69	f xs	1✔
70	\| V.null xs = return []	1✔
71	\| otherwise = do	×
72	let len2 = V.length xs `div` 2	1✔
73	cnt1 <- f (V.slice 0 len2 xs)	1✔
74	cnt2 <- f (V.slice len2 len2 xs)	1✔
75	c <- if V.length xs `mod` 2 == 0 then	1✔
76	lift $ Tseitin.encodeDisj enc []	1✔
77	else
78	lift $ return $ xs V.! (V.length xs - 1)	1✔
79	add cnt1 cnt2 c	1✔
80
81	runStateT (f (V.fromList lits)) []	1✔
82
83	encodeGE :: forall m. PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> [SAT.Lit] -> [Bool] -> m SAT.Lit
84	encodeGE enc polarity lhs rhs = do	1✔
85	let f :: [SAT.Lit] -> [Bool] -> SAT.Lit -> m SAT.Lit
86	f [] [] r = return r	1✔
87	f [] (True : _) _ = Tseitin.encodeDisjWithPolarity enc polarity [] -- false	×
88	f [] (False : bs) r = f [] bs r	×
89	f (l : ls) (True : bs) r = do	1✔
90	f ls bs =<< Tseitin.encodeConjWithPolarity enc polarity [l, r]	1✔
91	f (l : ls) (False : bs) r = do	1✔
UNCOV 92	f ls bs =<< Tseitin.encodeDisjWithPolarity enc polarity [l, r]	×
93	f (l : ls) [] r = do	×
94	f ls [] =<< Tseitin.encodeDisjWithPolarity enc polarity [l, r]	×
95	t <- Tseitin.encodeConjWithPolarity enc polarity [] -- true	1✔
96	f lhs rhs t	1✔

msakai / toysolver / 517

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