msakai / toysolver / 668

Committed 14 Apr 2025 03:29PM UTC coverage: 71.354% (+0.5%) from 70.812%

Build # 668

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #167 from msakai/feature/refactor-sat-encoder-integer

Refactor ToySolver.SAT.Encoder.Integer

Run Details

8 of 13 new or added lines in 2 files covered. (61.54%)

33 existing lines in 11 files now uncovered.

10733 of 15042 relevant lines covered (71.35%)

0.71 hits per line

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

46.88

/src/ToySolver/SAT/Encoder/Integer.hs

{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.Integer
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.Integer
  ( Expr (..)
  , newVar
  , newVarPBLinSum
  , linearize
  , addConstraint
  , addConstraintSoft
  , eval
  ) where

import Control.Monad
import Control.Monad.Primitive
import Data.Array.IArray
import Data.VectorSpace
import Math.NumberTheory.Logarithms (integerLog2)
import Text.Printf

import ToySolver.Data.OrdRel
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC

newtype Expr = Expr SAT.PBSum
  deriving (Eq, Show, Read)

newVar
  :: SAT.AddPBNL m enc
  => enc
  -> Integer -- ^ lower bound
  -> Integer -- ^ upper bound
  -> m Expr
newVar enc lo hi
  | lo > hi = do
      SAT.addClause enc [] -- assert inconsistency
      return 0
  | otherwise = do
      s <- newVarPBLinSum enc (hi - lo)
      return $ Expr $ [(lo,[]) | lo /= 0] ++ [(c, [l]) | (c,l) <- s]

-- | Lower-level version of 'newVar'
--
-- * It takes only upper bound. Lower bound is always 0.
--
-- * Return type is 'SAT.PBLinSum'. It is inconvenient for performing operations,
--   but it is sometimes useful to be guaranteed to be in a linear form.
newVarPBLinSum
  :: SAT.AddPBNL m enc
  => enc
  -> Integer -- ^ upper bound
  -> m SAT.PBLinSum
newVarPBLinSum enc hi
  | hi < 0 = do
      SAT.addClause enc [] -- assert inconsistency
      return []
  | hi == 0 = return []
  | otherwise = do
      let bitWidth = integerLog2 hi + 1
      vs <- SAT.newVars enc (bitWidth - 1)
      v <- SAT.newVar enc
      return $ [(c,x) | (c,x) <- zip (iterate (2*) 1) vs] ++ [(hi - (2 ^ (bitWidth - 1) - 1), v)]

instance AdditiveGroup Expr where
  Expr xs1 ^+^ Expr xs2 = Expr (xs1++xs2)
  zeroV = Expr []
  negateV = ((-1) *^)

instance VectorSpace Expr where
  type Scalar Expr = Integer
  n *^ Expr xs = Expr [(n*m,lits) | (m,lits) <- xs]

instance Num Expr where
  Expr xs1 + Expr xs2 = Expr (xs1++xs2)
  Expr xs1 * Expr xs2 = Expr [(c1*c2, lits1++lits2) | (c1,lits1) <- xs1, (c2,lits2) <- xs2]
  negate (Expr xs) = Expr [(-c,lits) | (c,lits) <- xs]
  abs      = id
  signum _ = 1
  fromInteger c = Expr [(c,[])]

linearize :: PrimMonad m => PBNLC.Encoder m -> Expr -> m (SAT.PBLinSum, Integer)
linearize enc (Expr xs) = do
  let ys = [(c,lits) | (c,lits@(_:_)) <- xs]
      c  = sum [c | (c,[]) <- xs]
  zs <- PBNLC.linearizePBSum enc ys
  return (zs, c)

addConstraint :: SAT.AddPBNL m enc => enc -> OrdRel Expr -> m ()
addConstraint enc (OrdRel lhs op rhs) = do
  let Expr e = lhs - rhs
  case op of
    Le  -> SAT.addPBNLAtMost  enc e 0
    Lt  -> SAT.addPBNLAtMost  enc e (-1)
    Ge  -> SAT.addPBNLAtLeast enc e 0
    Gt  -> SAT.addPBNLAtLeast enc e 1
    Eql -> SAT.addPBNLExactly enc e 0
    NEq -> do
      sel <- SAT.newVar enc
      SAT.addPBNLAtLeastSoft enc sel e 1
      SAT.addPBNLAtMostSoft  enc (-sel) e (-1)

addConstraintSoft :: SAT.AddPBNL m enc => enc -> SAT.Lit -> OrdRel Expr -> m ()
addConstraintSoft enc sel (OrdRel lhs op rhs) = do
  let Expr e = lhs - rhs
  case op of
    Le  -> SAT.addPBNLAtMostSoft  enc sel e 0
    Lt  -> SAT.addPBNLAtMostSoft  enc sel e (-1)
    Ge  -> SAT.addPBNLAtLeastSoft enc sel e 0
    Gt  -> SAT.addPBNLAtLeastSoft enc sel e 1
    Eql -> SAT.addPBNLExactlySoft enc sel e 0
    NEq -> do
      sel2 <- SAT.newVar enc
      sel3 <- SAT.newVar enc
      sel4 <- SAT.newVar enc
      SAT.addClause enc [-sel, -sel2, sel3] -- sel ∧  sel2 → sel3
      SAT.addClause enc [-sel,  sel2, sel4] -- sel ∧ ¬sel2 → sel4
      SAT.addPBNLAtLeastSoft enc sel3 e 1
      SAT.addPBNLAtMostSoft  enc sel4 e (-1)

eval :: SAT.IModel m => m -> Expr -> Integer
eval m (Expr ts) = sum [if and [SAT.evalLit m lit | lit <- lits] then n else 0 | (n,lits) <- ts]

1	{-# OPTIONS_HADDOCK show-extensions #-}
2	{-# LANGUAGE TypeFamilies #-}
3	-----------------------------------------------------------------------------
4	-- \|
5	-- Module : ToySolver.SAT.Encoder.Integer
6	-- Copyright : (c) Masahiro Sakai 2012
7	-- License : BSD-style
8	--
9	-- Maintainer : masahiro.sakai@gmail.com
10	-- Stability : provisional
11	-- Portability : non-portable
12	--
13	-----------------------------------------------------------------------------
14	module ToySolver.SAT.Encoder.Integer
15	( Expr (..)
16	, newVar
17	, newVarPBLinSum
18	, linearize
19	, addConstraint
20	, addConstraintSoft
21	, eval
22	) where
23
24	import Control.Monad
25	import Control.Monad.Primitive
26	import Data.Array.IArray
27	import Data.VectorSpace
28	import Math.NumberTheory.Logarithms (integerLog2)
29	import Text.Printf
30
31	import ToySolver.Data.OrdRel
32	import qualified ToySolver.SAT.Types as SAT
33	import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
34
35	newtype Expr = Expr SAT.PBSum
36	deriving (Eq, Show, Read)	×
37
38	newVar
39	:: SAT.AddPBNL m enc
40	=> enc
41	-> Integer -- ^ lower bound
42	-> Integer -- ^ upper bound
43	-> m Expr
44	newVar enc lo hi	1✔
45	\| lo > hi = do	×
46	SAT.addClause enc [] -- assert inconsistency	×
47	return 0	×
UNCOV 48	\| otherwise = do	×
49	s <- newVarPBLinSum enc (hi - lo)	1✔
50	return $ Expr $ [(lo,[]) \| lo /= 0] ++ [(c, [l]) \| (c,l) <- s]	1✔
51
52	-- \| Lower-level version of 'newVar'
53	--
54	-- * It takes only upper bound. Lower bound is always 0.
55	--
56	-- * Return type is 'SAT.PBLinSum'. It is inconvenient for performing operations,
57	-- but it is sometimes useful to be guaranteed to be in a linear form.
58	newVarPBLinSum
59	:: SAT.AddPBNL m enc
60	=> enc
61	-> Integer -- ^ upper bound
62	-> m SAT.PBLinSum
63	newVarPBLinSum enc hi	1✔
NEW 64	\| hi < 0 = do	×
NEW 65	SAT.addClause enc [] -- assert inconsistency	×
NEW 66	return []	×
67	\| hi == 0 = return []	1✔
NEW 68	\| otherwise = do	×
69	let bitWidth = integerLog2 hi + 1	1✔
70	vs <- SAT.newVars enc (bitWidth - 1)	1✔
71	v <- SAT.newVar enc	1✔
72	return $ [(c,x) \| (c,x) <- zip (iterate (2*) 1) vs] ++ [(hi - (2 ^ (bitWidth - 1) - 1), v)]	1✔
73
74	instance AdditiveGroup Expr where	×
75	Expr xs1 ^+^ Expr xs2 = Expr (xs1++xs2)	1✔
76	zeroV = Expr []	1✔
77	negateV = ((-1) *^)	×
78
79	instance VectorSpace Expr where
80	type Scalar Expr = Integer
81	n ^ Expr xs = Expr [(nm,lits) \| (m,lits) <- xs]	1✔
82
83	instance Num Expr where	1✔
84	Expr xs1 + Expr xs2 = Expr (xs1++xs2)	1✔
85	Expr xs1 * Expr xs2 = Expr [(c1*c2, lits1++lits2) \| (c1,lits1) <- xs1, (c2,lits2) <- xs2]	1✔
86	negate (Expr xs) = Expr [(-c,lits) \| (c,lits) <- xs]	1✔
87	abs = id	×
88	signum _ = 1	×
89	fromInteger c = Expr [(c,[])]	1✔
90
91	linearize :: PrimMonad m => PBNLC.Encoder m -> Expr -> m (SAT.PBLinSum, Integer)
92	linearize enc (Expr xs) = do	×
93	let ys = [(c,lits) \| (c,lits@(_:_)) <- xs]	×
94	c = sum [c \| (c,[]) <- xs]	×
95	zs <- PBNLC.linearizePBSum enc ys	×
96	return (zs, c)	×
97
98	addConstraint :: SAT.AddPBNL m enc => enc -> OrdRel Expr -> m ()
99	addConstraint enc (OrdRel lhs op rhs) = do	1✔
100	let Expr e = lhs - rhs	1✔
101	case op of	1✔
102	Le -> SAT.addPBNLAtMost enc e 0	1✔
103	Lt -> SAT.addPBNLAtMost enc e (-1)	×
104	Ge -> SAT.addPBNLAtLeast enc e 0	1✔
105	Gt -> SAT.addPBNLAtLeast enc e 1	×
106	Eql -> SAT.addPBNLExactly enc e 0	1✔
107	NEq -> do	×
108	sel <- SAT.newVar enc	×
109	SAT.addPBNLAtLeastSoft enc sel e 1	×
110	SAT.addPBNLAtMostSoft enc (-sel) e (-1)	×
111
112	addConstraintSoft :: SAT.AddPBNL m enc => enc -> SAT.Lit -> OrdRel Expr -> m ()
113	addConstraintSoft enc sel (OrdRel lhs op rhs) = do	1✔
114	let Expr e = lhs - rhs	1✔
115	case op of	1✔
116	Le -> SAT.addPBNLAtMostSoft enc sel e 0	1✔
117	Lt -> SAT.addPBNLAtMostSoft enc sel e (-1)	×
118	Ge -> SAT.addPBNLAtLeastSoft enc sel e 0	1✔
119	Gt -> SAT.addPBNLAtLeastSoft enc sel e 1	×
120	Eql -> SAT.addPBNLExactlySoft enc sel e 0	1✔
121	NEq -> do	×
122	sel2 <- SAT.newVar enc	×
123	sel3 <- SAT.newVar enc	×
124	sel4 <- SAT.newVar enc	×
125	SAT.addClause enc [-sel, -sel2, sel3] -- sel ∧ sel2 → sel3	×
126	SAT.addClause enc [-sel, sel2, sel4] -- sel ∧ ¬sel2 → sel4	×
127	SAT.addPBNLAtLeastSoft enc sel3 e 1	×
128	SAT.addPBNLAtMostSoft enc sel4 e (-1)	×
129
130	eval :: SAT.IModel m => m -> Expr -> Integer
131	eval m (Expr ts) = sum [if and [SAT.evalLit m lit \| lit <- lits] then n else 0 \| (n,lits) <- ts]	1✔

msakai / toysolver / 668

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