msakai / toysolver / 707

Committed 28 Apr 2025 05:58AM UTC coverage: 71.855% (+0.7%) from 71.16%

Build # 707

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #174 from msakai/feature/checker

Add toysolver-check command

Run Details

211 of 259 new or added lines in 2 files covered. (81.47%)

35 existing lines in 6 files now uncovered.

11034 of 15356 relevant lines covered (71.85%)

0.72 hits per line

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

82.23

/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 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])
NEW 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✔
NEW 65	"UNKNOWN" -> return ()	×
66	_ -> do	1✔
67	addError $ "unknown status: " ++ BS.unpack status	1✔
68
69	case m of	1✔
NEW 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✔
NEW 88	"UNKNOWN" -> return ()	×
89	_ -> do	1✔
90	addError $ "unknown status: " ++ BS.unpack status	1✔
91
92	case m of	1✔
NEW 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✔
NEW 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✔
NEW 122	"UNSUPPORTED" -> return ()	×
NEW 123	"UNKNOWN" -> return ()	×
124	_ -> do	1✔
125	addError $ "unknown status: " ++ BS.unpack status	1✔
126
127	case m of	1✔
NEW 128	Nothing -> return ()	×
129	Just model -> do	1✔
130	case PBFile.pbObjectiveFunction opb of	1✔
NEW 131	Nothing -> return ()	×
132	Just objFunc -> do	1✔
133	let val = SAT.evalPBSum model objFunc	1✔
134	addInfo $ "objective function value = " ++ show val	1✔
135	case o of	1✔
136	Just oVal \| val /= oVal -> do	1✔
137	addError $ printf "o-line value (%d) is inconsistent" oVal	1✔
NEW 138	_ -> return ()	×
139
140	forM_ (PBFile.pbConstraints opb) $ \constr -> do	1✔
141	unless (SAT.evalPBConstraint model constr) $ do	1✔
142	addError $ printf "violated: %s" (showPBConstraint constr :: String)	1✔
143
144	checkWBOResult :: PBFile.SoftFormula -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])
145	checkWBOResult wbo (status, o, m) = execM $ do	1✔
146	case status of	1✔
147	"SATISFIABLE" -> do	1✔
148	when (isNothing m) $ do	1✔
149	addError "SATISFIABLE, but a model is missing"	1✔
150	"OPTIMUM FOUND" -> do	1✔
151	when (isNothing m) $ do	1✔
152	addError "OPTIMUM FOUND, but a model is missing"	1✔
153	"UNSATISFIABLE" -> do	1✔
154	when (isJust m) $ do	1✔
155	addError "UNSATISFIABLE, but a model is provided"	1✔
NEW 156	"UNSUPPORTED" -> return ()	×
NEW 157	"UNKNOWN" -> return ()	×
158	_ -> do	1✔
159	addError $ "unknown status: " ++ BS.unpack status	1✔
160
161	case m of	1✔
NEW 162	Nothing -> return ()	×
163	Just model -> do	1✔
164	cost <- fmap sum $ forM (PBFile.wboConstraints wbo) $ \(w, constr) -> do	1✔
165	if SAT.evalPBConstraint model constr then	1✔
166	return 0	1✔
167	else do	1✔
168	case w of	1✔
169	Nothing -> do	1✔
170	addError $ printf "violated hard constraint: %s" (showPBConstraint constr :: String)	1✔
171	return 0	1✔
172	Just w' -> do	1✔
173	return w'	1✔
174	addInfo $ "total cost = " ++ show cost	1✔
175
176	case PBFile.wboTopCost wbo of	1✔
177	Just top \| top <= cost -> do	1✔
178	addError $ printf "total cost (%d) is greater than or equal to top cost (%d)" cost top	1✔
NEW 179	_ -> return ()	×
180
181	case o of	1✔
182	Just oVal \| oVal /= cost -> do	1✔
183	addError $ printf "o-line value (%d) is inconsistent" oVal	1✔
NEW 184	_ -> return ()	×
185
186	checkMIPResult :: MIP.Tol Scientific -> MIP.Problem Scientific -> MIP.Solution Scientific -> (Bool, [String])
187	checkMIPResult tol mip sol = execM $ do	1✔
188	let m = MIP.solVariables sol	1✔
189
NEW 190	let objVal = MIP.eval tol m (MIP.objExpr (MIP.objectiveFunction mip))	×
191	addInfo $ "objective value = " ++ show objVal	1✔
192	case MIP.solObjectiveValue sol of	1✔
NEW 193	Nothing -> return ()	×
194	Just declaredObjVal -> do	1✔
195	unless (abs (objVal - declaredObjVal) <= MIP.feasibilityTol tol) $ do	1✔
196	addError $ printf "declared objective value (%s) does not match to the computed value (%s)"	1✔
197	(show declaredObjVal) (show objVal)	1✔
198
199	forM_ (Map.toList (MIP.varDomains mip)) $ \(v, (vt, bounds@(lb,ub))) -> do	1✔
NEW 200	let val = MIP.eval tol m v	×
201	flag1 =	1✔
202	case vt of	1✔
203	MIP.ContinuousVariable -> True	1✔
204	MIP.SemiContinuousVariable -> True	1✔
205	MIP.IntegerVariable -> isIntegral tol val	1✔
206	MIP.SemiIntegerVariable -> isIntegral tol val	1✔
207	flag2 =	1✔
208	case vt of	1✔
209	MIP.ContinuousVariable -> isInBounds tol bounds val	1✔
210	MIP.IntegerVariable -> isInBounds tol bounds val	1✔
211	MIP.SemiIntegerVariable -> isInBounds tol (0,0) val \|\| isInBounds tol bounds val	1✔
212	MIP.SemiContinuousVariable -> isInBounds tol (0,0) val \|\| isInBounds tol bounds val	1✔
213	unless flag1 $ do	1✔
214	addError $ printf "variable %s is not integral" (T.unpack (MIP.varName v))	1✔
215	unless flag2 $ do	1✔
NEW 216	let f MIP.NegInf = "-inf"	×
NEW 217	f MIP.PosInf = "+inf"	×
218	f (MIP.Finite x) = show x	1✔
219	addError $ printf "variable %s is out of bounds lb=%s ub=%s" (T.unpack (MIP.varName v)) (f lb) (f ub)	1✔
220
221	forM_ (MIP.constraints mip) $ \constr -> do	1✔
222	unless (MIP.eval tol m constr) $ do	1✔
223	addError $ case MIP.constrLabel constr of	1✔
NEW 224	Just name -> printf "violated: %s" (T.unpack name)	×
225	Nothing -> printf "violated: %s" (showMIPConstraint constr)	1✔
226
227	forM_ (MIP.sosConstraints mip) $ \constr -> do	1✔
228	unless (MIP.eval tol m constr) $ do	1✔
229	addError $ case MIP.sosLabel constr of	1✔
NEW 230	Just name -> printf "violated: %s" (T.unpack name)	×
231	Nothing -> printf "violated: %s" (showMIPSOSConstraint constr)	1✔
232
233	-- ------------------------------------------------------------------------
234
235	showClause :: (Monoid a, IsString a) => SAT.PackedClause -> a
236	showClause = foldr (\f g -> f <> fromString " " <> g) mempty . map (fromString . show) . SAT.unpackClause	1✔
237
238	showPBSum :: (Monoid a, IsString a) => PBFile.Sum -> a
239	showPBSum = mconcat . map showWeightedTerm	1✔
240	where
241	showWeightedTerm :: (Monoid a, IsString a) => PBFile.WeightedTerm -> a
242	showWeightedTerm (c, lits) = foldr (\f g -> f <> fromString " " <> g) mempty (x:xs)	1✔
243	where
NEW 244	x = if c >= 0 then fromString "+" <> fromString (show c) else fromString (show c)	×
NEW 245	xs = map showLit $ sortBy (comparing abs) lits	×
246
247	showLit :: (Monoid a, IsString a) => PBFile.Lit -> a
248	showLit lit = if lit > 0 then v else fromString "~" <> v	1✔
249	where
250	v = fromString "x" <> fromString (show (abs lit))	1✔
251
252	showPBConstraint :: (Monoid a, IsString a) => PBFile.Constraint -> a
253	showPBConstraint (lhs, op, rhs) =	1✔
254	showPBSum lhs <> f op <> fromString " " <> fromString (show rhs)	1✔
255	where
NEW 256	f PBFile.Eq = fromString "="	×
257	f PBFile.Ge = fromString ">="	1✔
258
259	showMIPConstraint :: MIP.Constraint Scientific -> String
260	showMIPConstraint constr = concat	1✔
261	[ case MIP.constrIndicator constr of	1✔
262	Nothing -> ""	1✔
263	Just (MIP.Var var, val) ->
NEW 264	let rhs =	×
NEW 265	case floatingOrInteger val of	×
NEW 266	Right (i :: Integer) -> show i	×
NEW 267	Left (_ :: Double) -> show val -- should be error?	×
NEW 268	in T.unpack var ++ " = " ++ rhs ++ " -> "	×
269	, case MIP.constrLB constr of	1✔
270	MIP.NegInf -> ""	1✔
NEW 271	MIP.PosInf -> "+inf <= "	×
NEW 272	MIP.Finite x -> show x ++ " <= "	×
273	, showMIPExpr (MIP.constrExpr constr)	1✔
274	, case MIP.constrUB constr of	1✔
NEW 275	MIP.NegInf -> "<= -inf"	×
NEW 276	MIP.PosInf -> ""	×
277	MIP.Finite x -> " <= " ++ show x	1✔
278	]
279
280	showMIPSOSConstraint :: MIP.SOSConstraint Scientific -> String
281	showMIPSOSConstraint constr = concat $	1✔
282	[show (MIP.sosType constr), " ::"] ++ [	1✔
283	" " ++ T.unpack (MIP.varName v) ++ " : " ++ show r	1✔
284	\| (v, r) <- MIP.sosBody constr	1✔
285	]
286
287	showMIPExpr :: MIP.Expr Scientific -> String
288	showMIPExpr e = intercalate " "	1✔
289	[ intercalate "*" (((if c >= 0 then "+" ++ show c else show c) : map (T.unpack . MIP.varName) vs))	1✔
290	\| MIP.Term c vs <- MIP.terms e	1✔
291	]
292
293	isIntegral :: RealFrac r => MIP.Tol r -> r -> Bool
294	isIntegral tol x = abs (x - fromIntegral (floor (x + 0.5) :: Integer)) <= MIP.integralityTol tol	1✔
295
296	isInBounds :: (Num r, Ord r) => MIP.Tol r -> MIP.Bounds r -> r -> Bool
297	isInBounds tol (lb, ub) x =	1✔
298	lb - MIP.Finite (MIP.feasibilityTol tol) <= MIP.Finite x &&	1✔
299	MIP.Finite x <= ub + MIP.Finite (MIP.feasibilityTol tol)	1✔
300
301	-- ------------------------------------------------------------------------

msakai / toysolver / 707

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