msakai / toysolver / 769

Committed 22 May 2025 11:08PM UTC coverage: 71.745% (-0.2%) from 71.906%

Build # 769

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #196 from msakai/feature/warn-o-lines-for-pbs

Warn if o-line(s) exist in a log for a PBS problem

Run Details

0 of 4 new or added lines in 1 file covered. (0.0%)

63 existing lines in 12 files now uncovered.

11091 of 15459 relevant lines covered (71.74%)

0.72 hits per line

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

80.6

/src/ToySolver/Internal/SolutionChecker.hs

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Internal.SolutionChecker
-- Copyright   :  (c) Masahiro Sakai 2025
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  unstable
-- Portability :  non-portable
--
-----------------------------------------------------------------------------

module ToySolver.Internal.SolutionChecker
  ( checkSATResult
  , checkMaxSATResult
  , checkPBResult
  , checkWBOResult
  , checkMIPResult
  ) where

import Control.Monad
import Control.Monad.RWS.Lazy
import qualified Data.ByteString.Char8 as BS
import Data.List (intercalate, sortBy)
import qualified Data.Map.Lazy as Map
import Data.Maybe
import Data.Ord
import qualified Data.PseudoBoolean as PBFile
import Data.Scientific
import Data.String
import qualified Data.Text as T
import qualified Numeric.Optimization.MIP as MIP
import Text.Printf

import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

-- ------------------------------------------------------------------------

type M = RWS () [String] Bool

execM :: M () -> (Bool, [String])
execM m = execRWS m () True

addInfo :: String -> M ()
addInfo s = tell [s]

addError :: String -> M ()
addError s = tell [s] >> put False

-- ------------------------------------------------------------------------

checkSATResult :: CNF.CNF -> (BS.ByteString, Maybe SAT.Model) -> (Bool, [String])
checkSATResult cnf (status, m) = execM $ do
  case status of
    "SATISFIABLE" -> do
      when (isNothing m) $ do
        addError "SATISFIABLE, but a model is missing"
    "UNSATISFIABLE" -> do
      when (isJust m) $ do
        addError "UNSATISFIABLE, but a model is provided"
    "UNKNOWN" -> return ()
    _ -> do
      addError $ "unknown status: " ++ BS.unpack status

  case m of
    Nothing -> return ()
    Just model -> do
      forM_ (CNF.cnfClauses cnf) $ \constr ->
        unless (SAT.evalClause model (SAT.unpackClause constr)) $ do
          addError $ printf "violated: %s" (showClause constr :: String)

checkMaxSATResult :: CNF.WCNF -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])
checkMaxSATResult wcnf (status, o, m) = execM $ do
  case status of
    "OPTIMUM FOUND" -> do
      when (isNothing m) $ do
        addError "OPTIMUM FOUND, but a model is missing"
    "SATISFIABLE" -> do
      when (isNothing m) $ do
        addError "SATISFIABLE, but a model is missing"
    "UNSATISFIABLE" -> do
      when (isJust m) $ do
        addError "UNSATISFIABLE, but a model is provided"
    "UNKNOWN" -> return ()
    _ -> do
      addError $ "unknown status: " ++ BS.unpack status

  case m of
    Nothing -> return ()
    Just model -> do
      cost <- fmap sum $ forM (CNF.wcnfClauses wcnf) $ \(w, constr) ->
        if SAT.evalClause model (SAT.unpackClause constr) then do
          return 0
        else if w == CNF.wcnfTopCost wcnf then do
          addError $ printf "violated hard constraint: %s" (showClause constr :: String)
          return 0
        else do
          return w
      addInfo $ "total cost = " ++ show cost

      case o of
        Just oVal | oVal /= cost -> do
          addError $ printf "o-line value (%d) is inconsistent" oVal
        _ -> return ()

checkPBResult :: PBFile.Formula -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])
checkPBResult opb (status, o, m) = execM $ do
  case status of
    "SATISFIABLE" -> do
      when (isNothing m) $ do
        addError "SATISFIABLE, but a model is missing"
    "OPTIMUM FOUND" -> do
      when (isNothing m) $ do
        addError "OPTIMUM FOUND, but a model is missing"
    "UNSATISFIABLE" -> do
      when (isJust m) $ do
        addError "UNSATISFIABLE, but a model is provided"
    "UNSUPPORTED" -> return ()
    "UNKNOWN" -> return ()
    _ -> do
      addError $ "unknown status: " ++ BS.unpack status


  case (PBFile.pbObjectiveFunction opb, o) of
    (Nothing, Just _) -> do
      addInfo $ "o-line(s) exist even though it is a PBS problem. (will be ignored)"
    _ -> pure ()

  case m of
    Nothing -> return ()
    Just model -> do
      case PBFile.pbObjectiveFunction opb of
        Nothing -> return ()
        Just objFunc -> do
          let val = SAT.evalPBSum model objFunc
          addInfo $ "objective function value = " ++ show val
          case o of
            Just oVal | val /= oVal -> do
              addError $ printf "o-line value (%d) is inconsistent" oVal
            _ -> return ()

      forM_ (PBFile.pbConstraints opb) $ \constr -> do
        unless (SAT.evalPBConstraint model constr) $ do
          addError $ printf "violated: %s" (showPBConstraint constr :: String)

checkWBOResult :: PBFile.SoftFormula -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])
checkWBOResult wbo (status, o, m) = execM $ do
  case status of
    "SATISFIABLE" -> do
      when (isNothing m) $ do
        addError "SATISFIABLE, but a model is missing"
    "OPTIMUM FOUND" -> do
      when (isNothing m) $ do
        addError "OPTIMUM FOUND, but a model is missing"
    "UNSATISFIABLE" -> do
      when (isJust m) $ do
        addError "UNSATISFIABLE, but a model is provided"
    "UNSUPPORTED" -> return ()
    "UNKNOWN" -> return ()
    _ -> do
      addError $ "unknown status: " ++ BS.unpack status

  case m of
    Nothing -> return ()
    Just model -> do
      cost <- fmap sum $ forM (PBFile.wboConstraints wbo) $ \(w, constr) -> do
        if SAT.evalPBConstraint model constr then
          return 0
        else do
          case w of
            Nothing -> do
              addError $ printf "violated hard constraint: %s" (showPBConstraint constr :: String)
              return 0
            Just w' -> do
              return w'
      addInfo $ "total cost = " ++ show cost

      case PBFile.wboTopCost wbo of
        Just top | top <= cost -> do
          addError $ printf "total cost (%d) is greater than or equal to top cost (%d)" cost top
        _ -> return ()

      case o of
        Just oVal | oVal /= cost -> do
          addError $ printf "o-line value (%d) is inconsistent" oVal
        _ -> return ()

checkMIPResult :: MIP.Tol Scientific -> MIP.Problem Scientific -> MIP.Solution Scientific -> (Bool, [String])
checkMIPResult tol mip sol = execM $ do
  let m = MIP.solVariables sol

  let objVal = MIP.eval tol m (MIP.objExpr (MIP.objectiveFunction mip))
  addInfo $ "objective value = " ++ show objVal
  case MIP.solObjectiveValue sol of
    Nothing -> return ()
    Just declaredObjVal -> do
      unless (abs (objVal - declaredObjVal) <= MIP.feasibilityTol tol) $ do
        addError $ printf "declared objective value (%s) does not match to the computed value (%s)"
          (show declaredObjVal) (show objVal)

  forM_ (Map.toList (MIP.varDomains mip)) $ \(v, (vt, bounds@(lb,ub))) -> do
    let val = MIP.eval tol m v
        flag1 =
          case vt of
            MIP.ContinuousVariable -> True
            MIP.SemiContinuousVariable -> True
            MIP.IntegerVariable -> isIntegral tol val
            MIP.SemiIntegerVariable -> isIntegral tol val
        flag2 =
          case vt of
            MIP.ContinuousVariable -> isInBounds tol bounds val
            MIP.IntegerVariable -> isInBounds tol bounds val
            MIP.SemiIntegerVariable -> isInBounds tol (0,0) val || isInBounds tol bounds val
            MIP.SemiContinuousVariable -> isInBounds tol (0,0) val || isInBounds tol bounds val
    unless flag1 $ do
      addError $ printf "variable %s is not integral" (T.unpack (MIP.varName v))
    unless flag2 $ do
      let f MIP.NegInf = "-inf"
          f MIP.PosInf = "+inf"
          f (MIP.Finite x) = show x
      addError $ printf "variable %s is out of bounds lb=%s ub=%s" (T.unpack (MIP.varName v)) (f lb) (f ub)

  forM_ (MIP.constraints mip) $ \constr -> do
    unless (MIP.eval tol m constr) $ do
      addError $ case MIP.constrLabel constr of
        Just name -> printf "violated: %s" (T.unpack name)
        Nothing -> printf "violated: %s" (showMIPConstraint constr)

  forM_ (MIP.sosConstraints mip) $ \constr -> do
    unless (MIP.eval tol m constr) $ do
      addError $ case MIP.sosLabel constr of
        Just name -> printf "violated: %s" (T.unpack name)
        Nothing -> printf "violated: %s" (showMIPSOSConstraint constr)

-- ------------------------------------------------------------------------

showClause :: (Monoid a, IsString a) => SAT.PackedClause -> a
showClause = foldr (\f g -> f <> fromString " " <> g) mempty . map (fromString . show) . SAT.unpackClause

showPBSum :: (Monoid a, IsString a) => PBFile.Sum -> a
showPBSum = mconcat . map showWeightedTerm
  where
    showWeightedTerm :: (Monoid a, IsString a) => PBFile.WeightedTerm -> a
    showWeightedTerm (c, lits) = foldr (\f g -> f <> fromString " " <> g) mempty (x:xs)
      where
        x = if c >= 0 then fromString "+" <> fromString (show c) else fromString (show c)
        xs = map showLit $ sortBy (comparing abs) lits

    showLit :: (Monoid a, IsString a) => PBFile.Lit -> a
    showLit lit = if lit > 0 then v else fromString "~" <> v
      where
        v = fromString "x" <> fromString (show (abs lit))

showPBConstraint :: (Monoid a, IsString a) => PBFile.Constraint -> a
showPBConstraint (lhs, op, rhs) =
  showPBSum lhs <> f op <>  fromString " " <> fromString (show rhs)
  where
    f PBFile.Eq = fromString "="
    f PBFile.Ge = fromString ">="

showMIPConstraint :: MIP.Constraint Scientific -> String
showMIPConstraint constr = concat
  [ case MIP.constrIndicator constr of
      Nothing -> ""
      Just (MIP.Var var, val) ->
        let rhs =
              case floatingOrInteger val of
                Right (i :: Integer) -> show i
                Left (_ :: Double) -> show val  -- should be error?
         in T.unpack var ++ " = " ++ rhs ++ " -> "
  , case MIP.constrLB constr of
      MIP.NegInf -> ""
      MIP.PosInf -> "+inf <= "
      MIP.Finite x -> show x ++ " <= "
  , showMIPExpr (MIP.constrExpr constr)
  , case MIP.constrUB constr of
      MIP.NegInf -> "<= -inf"
      MIP.PosInf -> ""
      MIP.Finite x -> " <= " ++ show x
  ]

showMIPSOSConstraint :: MIP.SOSConstraint Scientific -> String
showMIPSOSConstraint constr = concat $
  [show (MIP.sosType constr), " ::"] ++ [
    " " ++ T.unpack (MIP.varName v) ++ " : " ++ show r
  | (v, r) <- MIP.sosBody constr
  ]

showMIPExpr :: MIP.Expr Scientific -> String
showMIPExpr e = intercalate " "
  [ intercalate "*" (((if c >= 0 then "+" ++ show c else show c) : map (T.unpack . MIP.varName) vs))
  | MIP.Term c vs <- MIP.terms e
  ]

isIntegral :: RealFrac r => MIP.Tol r -> r -> Bool
isIntegral tol x = abs (x - fromIntegral (floor (x + 0.5) :: Integer)) <= MIP.integralityTol tol

isInBounds :: (Num r, Ord r) => MIP.Tol r -> MIP.Bounds r -> r -> Bool
isInBounds tol (lb, ub) x =
  lb - MIP.Finite (MIP.feasibilityTol tol) <= MIP.Finite x &&
  MIP.Finite x <= ub + MIP.Finite (MIP.feasibilityTol tol)

-- ------------------------------------------------------------------------

1	{-# OPTIONS_GHC -Wall #-}
2	{-# LANGUAGE OverloadedStrings #-}
3	{-# LANGUAGE ScopedTypeVariables #-}
4	-----------------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.Internal.SolutionChecker
7	-- Copyright : (c) Masahiro Sakai 2025
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : unstable
12	-- Portability : non-portable
13	--
14	-----------------------------------------------------------------------------
15
16	module ToySolver.Internal.SolutionChecker
17	( checkSATResult
18	, checkMaxSATResult
19	, checkPBResult
20	, checkWBOResult
21	, checkMIPResult
22	) where
23
24	import Control.Monad
25	import Control.Monad.RWS.Lazy
26	import qualified Data.ByteString.Char8 as BS
27	import Data.List (intercalate, sortBy)
28	import qualified Data.Map.Lazy as Map
29	import Data.Maybe
30	import Data.Ord
31	import qualified Data.PseudoBoolean as PBFile
32	import Data.Scientific
33	import Data.String
34	import qualified Data.Text as T
35	import qualified Numeric.Optimization.MIP as MIP
36	import Text.Printf
37
38	import qualified ToySolver.FileFormat.CNF as CNF
39	import qualified ToySolver.SAT.Types as SAT
40
41	-- ------------------------------------------------------------------------
42
43	type M = RWS () [String] Bool
44
45	execM :: M () -> (Bool, [String])
46	execM m = execRWS m () True	×
47
48	addInfo :: String -> M ()
49	addInfo s = tell [s]	1✔
50
51	addError :: String -> M ()
52	addError s = tell [s] >> put False	1✔
53
54	-- ------------------------------------------------------------------------
55
56	checkSATResult :: CNF.CNF -> (BS.ByteString, Maybe SAT.Model) -> (Bool, [String])
57	checkSATResult cnf (status, m) = execM $ do	1✔
58	case status of	1✔
59	"SATISFIABLE" -> do	1✔
60	when (isNothing m) $ do	1✔
61	addError "SATISFIABLE, but a model is missing"	1✔
62	"UNSATISFIABLE" -> do	1✔
63	when (isJust m) $ do	1✔
64	addError "UNSATISFIABLE, but a model is provided"	1✔
65	"UNKNOWN" -> return ()	×
66	_ -> do	1✔
67	addError $ "unknown status: " ++ BS.unpack status	1✔
68
69	case m of	1✔
70	Nothing -> return ()	×
71	Just model -> do	1✔
72	forM_ (CNF.cnfClauses cnf) $ \constr ->	1✔
73	unless (SAT.evalClause model (SAT.unpackClause constr)) $ do	1✔
74	addError $ printf "violated: %s" (showClause constr :: String)	1✔
75
76	checkMaxSATResult :: CNF.WCNF -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])
77	checkMaxSATResult wcnf (status, o, m) = execM $ do	1✔
78	case status of	1✔
79	"OPTIMUM FOUND" -> do	1✔
80	when (isNothing m) $ do	1✔
81	addError "OPTIMUM FOUND, but a model is missing"	1✔
82	"SATISFIABLE" -> do	1✔
83	when (isNothing m) $ do	1✔
84	addError "SATISFIABLE, but a model is missing"	1✔
85	"UNSATISFIABLE" -> do	1✔
86	when (isJust m) $ do	1✔
87	addError "UNSATISFIABLE, but a model is provided"	1✔
88	"UNKNOWN" -> return ()	×
89	_ -> do	1✔
90	addError $ "unknown status: " ++ BS.unpack status	1✔
91
92	case m of	1✔
93	Nothing -> return ()	×
94	Just model -> do	1✔
95	cost <- fmap sum $ forM (CNF.wcnfClauses wcnf) $ \(w, constr) ->	1✔
96	if SAT.evalClause model (SAT.unpackClause constr) then do	1✔
97	return 0	1✔
98	else if w == CNF.wcnfTopCost wcnf then do	1✔
99	addError $ printf "violated hard constraint: %s" (showClause constr :: String)	1✔
100	return 0	1✔
101	else do	1✔
102	return w	1✔
103	addInfo $ "total cost = " ++ show cost	1✔
104
105	case o of	1✔
106	Just oVal \| oVal /= cost -> do	1✔
107	addError $ printf "o-line value (%d) is inconsistent" oVal	1✔
108	_ -> return ()	×
109
110	checkPBResult :: PBFile.Formula -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])
111	checkPBResult opb (status, o, m) = execM $ do	1✔
112	case status of	1✔
113	"SATISFIABLE" -> do	1✔
114	when (isNothing m) $ do	1✔
115	addError "SATISFIABLE, but a model is missing"	1✔
116	"OPTIMUM FOUND" -> do	1✔
117	when (isNothing m) $ do	1✔
118	addError "OPTIMUM FOUND, but a model is missing"	1✔
119	"UNSATISFIABLE" -> do	1✔
120	when (isJust m) $ do	1✔
121	addError "UNSATISFIABLE, but a model is provided"	1✔
122	"UNSUPPORTED" -> return ()	×
123	"UNKNOWN" -> return ()	×
124	_ -> do	1✔
125	addError $ "unknown status: " ++ BS.unpack status	1✔
126
127
NEW 128	case (PBFile.pbObjectiveFunction opb, o) of	×
NEW 129	(Nothing, Just _) -> do	×
NEW 130	addInfo $ "o-line(s) exist even though it is a PBS problem. (will be ignored)"	×
NEW 131	_ -> pure ()	×
132
133	case m of	1✔
134	Nothing -> return ()	×
135	Just model -> do	1✔
136	case PBFile.pbObjectiveFunction opb of	1✔
137	Nothing -> return ()	×
138	Just objFunc -> do	1✔
139	let val = SAT.evalPBSum model objFunc	1✔
140	addInfo $ "objective function value = " ++ show val	1✔
141	case o of	1✔
142	Just oVal \| val /= oVal -> do	1✔
143	addError $ printf "o-line value (%d) is inconsistent" oVal	1✔
144	_ -> return ()	×
145
146	forM_ (PBFile.pbConstraints opb) $ \constr -> do	1✔
147	unless (SAT.evalPBConstraint model constr) $ do	1✔
148	addError $ printf "violated: %s" (showPBConstraint constr :: String)	1✔
149
150	checkWBOResult :: PBFile.SoftFormula -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])
151	checkWBOResult wbo (status, o, m) = execM $ do	1✔
152	case status of	1✔
153	"SATISFIABLE" -> do	1✔
154	when (isNothing m) $ do	1✔
155	addError "SATISFIABLE, but a model is missing"	1✔
156	"OPTIMUM FOUND" -> do	1✔
157	when (isNothing m) $ do	1✔
158	addError "OPTIMUM FOUND, but a model is missing"	1✔
159	"UNSATISFIABLE" -> do	1✔
160	when (isJust m) $ do	1✔
161	addError "UNSATISFIABLE, but a model is provided"	1✔
162	"UNSUPPORTED" -> return ()	×
163	"UNKNOWN" -> return ()	×
164	_ -> do	1✔
165	addError $ "unknown status: " ++ BS.unpack status	1✔
166
167	case m of	1✔
168	Nothing -> return ()	×
169	Just model -> do	1✔
170	cost <- fmap sum $ forM (PBFile.wboConstraints wbo) $ \(w, constr) -> do	1✔
171	if SAT.evalPBConstraint model constr then	1✔
172	return 0	1✔
173	else do	1✔
174	case w of	1✔
175	Nothing -> do	1✔
176	addError $ printf "violated hard constraint: %s" (showPBConstraint constr :: String)	1✔
177	return 0	1✔
178	Just w' -> do	1✔
179	return w'	1✔
180	addInfo $ "total cost = " ++ show cost	1✔
181
182	case PBFile.wboTopCost wbo of	1✔
183	Just top \| top <= cost -> do	1✔
184	addError $ printf "total cost (%d) is greater than or equal to top cost (%d)" cost top	1✔
185	_ -> return ()	×
186
187	case o of	1✔
188	Just oVal \| oVal /= cost -> do	1✔
189	addError $ printf "o-line value (%d) is inconsistent" oVal	1✔
190	_ -> return ()	×
191
192	checkMIPResult :: MIP.Tol Scientific -> MIP.Problem Scientific -> MIP.Solution Scientific -> (Bool, [String])
193	checkMIPResult tol mip sol = execM $ do	1✔
194	let m = MIP.solVariables sol	1✔
195
196	let objVal = MIP.eval tol m (MIP.objExpr (MIP.objectiveFunction mip))	×
197	addInfo $ "objective value = " ++ show objVal	1✔
198	case MIP.solObjectiveValue sol of	1✔
199	Nothing -> return ()	×
200	Just declaredObjVal -> do	1✔
201	unless (abs (objVal - declaredObjVal) <= MIP.feasibilityTol tol) $ do	1✔
202	addError $ printf "declared objective value (%s) does not match to the computed value (%s)"	1✔
203	(show declaredObjVal) (show objVal)	1✔
204
205	forM_ (Map.toList (MIP.varDomains mip)) $ \(v, (vt, bounds@(lb,ub))) -> do	1✔
206	let val = MIP.eval tol m v	×
207	flag1 =	1✔
208	case vt of	1✔
209	MIP.ContinuousVariable -> True	1✔
210	MIP.SemiContinuousVariable -> True	1✔
211	MIP.IntegerVariable -> isIntegral tol val	1✔
212	MIP.SemiIntegerVariable -> isIntegral tol val	1✔
213	flag2 =	1✔
214	case vt of	1✔
215	MIP.ContinuousVariable -> isInBounds tol bounds val	1✔
216	MIP.IntegerVariable -> isInBounds tol bounds val	1✔
217	MIP.SemiIntegerVariable -> isInBounds tol (0,0) val \|\| isInBounds tol bounds val	1✔
218	MIP.SemiContinuousVariable -> isInBounds tol (0,0) val \|\| isInBounds tol bounds val	1✔
219	unless flag1 $ do	1✔
220	addError $ printf "variable %s is not integral" (T.unpack (MIP.varName v))	1✔
221	unless flag2 $ do	1✔
222	let f MIP.NegInf = "-inf"	×
223	f MIP.PosInf = "+inf"	×
224	f (MIP.Finite x) = show x	1✔
225	addError $ printf "variable %s is out of bounds lb=%s ub=%s" (T.unpack (MIP.varName v)) (f lb) (f ub)	1✔
226
227	forM_ (MIP.constraints mip) $ \constr -> do	1✔
228	unless (MIP.eval tol m constr) $ do	1✔
229	addError $ case MIP.constrLabel constr of	1✔
230	Just name -> printf "violated: %s" (T.unpack name)	×
231	Nothing -> printf "violated: %s" (showMIPConstraint constr)	1✔
232
233	forM_ (MIP.sosConstraints mip) $ \constr -> do	1✔
234	unless (MIP.eval tol m constr) $ do	1✔
235	addError $ case MIP.sosLabel constr of	1✔
236	Just name -> printf "violated: %s" (T.unpack name)	×
237	Nothing -> printf "violated: %s" (showMIPSOSConstraint constr)	1✔
238
239	-- ------------------------------------------------------------------------
240
241	showClause :: (Monoid a, IsString a) => SAT.PackedClause -> a
242	showClause = foldr (\f g -> f <> fromString " " <> g) mempty . map (fromString . show) . SAT.unpackClause	1✔
243
244	showPBSum :: (Monoid a, IsString a) => PBFile.Sum -> a
245	showPBSum = mconcat . map showWeightedTerm	1✔
246	where
247	showWeightedTerm :: (Monoid a, IsString a) => PBFile.WeightedTerm -> a
248	showWeightedTerm (c, lits) = foldr (\f g -> f <> fromString " " <> g) mempty (x:xs)	1✔
249	where
250	x = if c >= 0 then fromString "+" <> fromString (show c) else fromString (show c)	×
251	xs = map showLit $ sortBy (comparing abs) lits	×
252
253	showLit :: (Monoid a, IsString a) => PBFile.Lit -> a
254	showLit lit = if lit > 0 then v else fromString "~" <> v	1✔
255	where
256	v = fromString "x" <> fromString (show (abs lit))	1✔
257
258	showPBConstraint :: (Monoid a, IsString a) => PBFile.Constraint -> a
259	showPBConstraint (lhs, op, rhs) =	1✔
260	showPBSum lhs <> f op <> fromString " " <> fromString (show rhs)	1✔
261	where
262	f PBFile.Eq = fromString "="	×
263	f PBFile.Ge = fromString ">="	1✔
264
265	showMIPConstraint :: MIP.Constraint Scientific -> String
266	showMIPConstraint constr = concat	1✔
267	[ case MIP.constrIndicator constr of	1✔
268	Nothing -> ""	1✔
269	Just (MIP.Var var, val) ->
270	let rhs =	×
271	case floatingOrInteger val of	×
272	Right (i :: Integer) -> show i	×
273	Left (_ :: Double) -> show val -- should be error?	×
274	in T.unpack var ++ " = " ++ rhs ++ " -> "	×
275	, case MIP.constrLB constr of	1✔
276	MIP.NegInf -> ""	1✔
277	MIP.PosInf -> "+inf <= "	×
278	MIP.Finite x -> show x ++ " <= "	×
279	, showMIPExpr (MIP.constrExpr constr)	1✔
280	, case MIP.constrUB constr of	1✔
281	MIP.NegInf -> "<= -inf"	×
282	MIP.PosInf -> ""	×
283	MIP.Finite x -> " <= " ++ show x	1✔
284	]
285
286	showMIPSOSConstraint :: MIP.SOSConstraint Scientific -> String
287	showMIPSOSConstraint constr = concat $	1✔
288	[show (MIP.sosType constr), " ::"] ++ [	1✔
289	" " ++ T.unpack (MIP.varName v) ++ " : " ++ show r	1✔
290	\| (v, r) <- MIP.sosBody constr	1✔
291	]
292
293	showMIPExpr :: MIP.Expr Scientific -> String
294	showMIPExpr e = intercalate " "	1✔
295	[ intercalate "*" (((if c >= 0 then "+" ++ show c else show c) : map (T.unpack . MIP.varName) vs))	1✔
296	\| MIP.Term c vs <- MIP.terms e	1✔
297	]
298
299	isIntegral :: RealFrac r => MIP.Tol r -> r -> Bool
300	isIntegral tol x = abs (x - fromIntegral (floor (x + 0.5) :: Integer)) <= MIP.integralityTol tol	1✔
301
302	isInBounds :: (Num r, Ord r) => MIP.Tol r -> MIP.Bounds r -> r -> Bool
303	isInBounds tol (lb, ub) x =	1✔
304	lb - MIP.Finite (MIP.feasibilityTol tol) <= MIP.Finite x &&	1✔
305	MIP.Finite x <= ub + MIP.Finite (MIP.feasibilityTol tol)	1✔
306
307	-- ------------------------------------------------------------------------

msakai / toysolver / 769

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