msakai / toysolver / 547

Committed 07 Dec 2024 02:57PM UTC coverage: 69.322% (-0.2%) from 69.513%

Build # 547

Build Type

push

github

Committed by

web-flow

Commit Message

Merge e2f74f4de into b30fce672

Run Details

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

113 existing lines in 10 files now uncovered.

10060 of 14512 relevant lines covered (69.32%)

0.69 hits per line

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

72.73

/src/ToySolver/SAT/Store/PB.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Store.PB
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Store.PB
  ( PBStore
  , newPBStore
  , getPBFormula
  ) where

import Control.Monad.Primitive
import Data.Foldable (toList)
import Data.Primitive.MutVar
import Data.Sequence (Seq, (|>))
import qualified Data.Sequence as Seq
import qualified Data.PseudoBoolean as PBFile
import qualified ToySolver.SAT.Types as SAT

data PBStore m = PBStore (MutVar (PrimState m) Int) (MutVar (PrimState m) (Seq PBFile.Constraint))

instance PrimMonad m => SAT.NewVar m (PBStore m) where
  newVar (PBStore ref _) = do
    modifyMutVar' ref (+1)
    readMutVar ref

instance PrimMonad m => SAT.AddClause m (PBStore m) where
  addClause enc clause = SAT.addPBNLAtLeast enc [(1,[l]) | l <- clause] 1

instance PrimMonad m => SAT.AddCardinality m (PBStore m) where
  addAtLeast enc lhs rhs = SAT.addPBNLAtLeast enc [(1,[l]) | l <- lhs] (fromIntegral rhs)

instance PrimMonad m => SAT.AddPBLin m (PBStore m) where
  addPBAtLeast enc lhs rhs = SAT.addPBNLAtLeast enc [(c,[l]) | (c,l) <- lhs] rhs
  addPBAtMost enc lhs rhs  = SAT.addPBNLAtMost enc  [(c,[l]) | (c,l) <- lhs] rhs
  addPBExactly enc lhs rhs = SAT.addPBNLExactly enc [(c,[l]) | (c,l) <- lhs] rhs

instance PrimMonad m => SAT.AddPBNL m (PBStore m) where
  addPBNLAtLeast (PBStore _ ref) lhs rhs = do
    let lhs' = [(c,ls) | (c,ls@(_:_)) <- lhs]
        rhs' = rhs - sum [c | (c,[]) <- lhs]
    modifyMutVar' ref (|> (lhs', PBFile.Ge, rhs'))
  addPBNLExactly (PBStore _ ref) lhs rhs = do
    let lhs' = [(c,ls) | (c,ls@(_:_)) <- lhs]
        rhs' = rhs - sum [c | (c,[]) <- lhs]
    modifyMutVar' ref (|> (lhs', PBFile.Eq, rhs'))

newPBStore :: PrimMonad m => m (PBStore m)
newPBStore = do
  ref1 <- newMutVar 0
  ref2 <- newMutVar Seq.empty
  return (PBStore ref1 ref2)

getPBFormula :: PrimMonad m => PBStore m -> m (PBFile.Formula)
getPBFormula (PBStore ref1 ref2) = do
  nv <- readMutVar ref1
  cs <- readMutVar ref2
  return $
    PBFile.Formula
    { PBFile.pbObjectiveFunction = Nothing
    , PBFile.pbConstraints = toList cs
    , PBFile.pbNumVars = nv
    , PBFile.pbNumConstraints = Seq.length cs
    }

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE FlexibleContexts #-}
4	{-# LANGUAGE FlexibleInstances #-}
5	{-# LANGUAGE MultiParamTypeClasses #-}
6	-----------------------------------------------------------------------------
7	-- \|
8	-- Module : ToySolver.SAT.Store.PB
9	-- Copyright : (c) Masahiro Sakai 2016
10	-- License : BSD-style
11	--
12	-- Maintainer : masahiro.sakai@gmail.com
13	-- Stability : experimental
14	-- Portability : non-portable
15	--
16	-----------------------------------------------------------------------------
17	module ToySolver.SAT.Store.PB
18	( PBStore
19	, newPBStore
20	, getPBFormula
21	) where
22
23	import Control.Monad.Primitive
24	import Data.Foldable (toList)
25	import Data.Primitive.MutVar
26	import Data.Sequence (Seq, (\|>))
27	import qualified Data.Sequence as Seq
28	import qualified Data.PseudoBoolean as PBFile
29	import qualified ToySolver.SAT.Types as SAT
30
31	data PBStore m = PBStore (MutVar (PrimState m) Int) (MutVar (PrimState m) (Seq PBFile.Constraint))
32
33	instance PrimMonad m => SAT.NewVar m (PBStore m) where	1✔
34	newVar (PBStore ref _) = do	1✔
35	modifyMutVar' ref (+1)	1✔
36	readMutVar ref	1✔
37
38	instance PrimMonad m => SAT.AddClause m (PBStore m) where
UNCOV 39	addClause enc clause = SAT.addPBNLAtLeast enc [(1,[l]) \| l <- clause] 1	×
40
41	instance PrimMonad m => SAT.AddCardinality m (PBStore m) where	×
42	addAtLeast enc lhs rhs = SAT.addPBNLAtLeast enc [(1,[l]) \| l <- lhs] (fromIntegral rhs)	×
43
44	instance PrimMonad m => SAT.AddPBLin m (PBStore m) where	×
45	addPBAtLeast enc lhs rhs = SAT.addPBNLAtLeast enc [(c,[l]) \| (c,l) <- lhs] rhs	×
46	addPBAtMost enc lhs rhs = SAT.addPBNLAtMost enc [(c,[l]) \| (c,l) <- lhs] rhs	×
47	addPBExactly enc lhs rhs = SAT.addPBNLExactly enc [(c,[l]) \| (c,l) <- lhs] rhs	×
48
49	instance PrimMonad m => SAT.AddPBNL m (PBStore m) where	1✔
50	addPBNLAtLeast (PBStore _ ref) lhs rhs = do	1✔
51	let lhs' = [(c,ls) \| (c,ls@(_:_)) <- lhs]	1✔
52	rhs' = rhs - sum [c \| (c,[]) <- lhs]	×
53	modifyMutVar' ref (\|> (lhs', PBFile.Ge, rhs'))	1✔
54	addPBNLExactly (PBStore _ ref) lhs rhs = do	1✔
55	let lhs' = [(c,ls) \| (c,ls@(_:_)) <- lhs]	1✔
56	rhs' = rhs - sum [c \| (c,[]) <- lhs]	1✔
57	modifyMutVar' ref (\|> (lhs', PBFile.Eq, rhs'))	1✔
58
59	newPBStore :: PrimMonad m => m (PBStore m)
60	newPBStore = do	1✔
61	ref1 <- newMutVar 0	1✔
62	ref2 <- newMutVar Seq.empty	1✔
63	return (PBStore ref1 ref2)	1✔
64
65	getPBFormula :: PrimMonad m => PBStore m -> m (PBFile.Formula)
66	getPBFormula (PBStore ref1 ref2) = do	1✔
67	nv <- readMutVar ref1	1✔
68	cs <- readMutVar ref2	1✔
69	return $	1✔
70	PBFile.Formula	1✔
71	{ PBFile.pbObjectiveFunction = Nothing	×
72	, PBFile.pbConstraints = toList cs	1✔
73	, PBFile.pbNumVars = nv	1✔
74	, PBFile.pbNumConstraints = Seq.length cs	1✔
75	}

msakai / toysolver / 547

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