Skip to content

Commit

Permalink
Fix a wrong interpretation of DIMACS CNF format
Browse files Browse the repository at this point in the history
* 'c' after 'p' was ignored
  • Loading branch information
shnarazk committed Feb 2, 2016
1 parent 4ea35a3 commit 16addbd
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion SAT/Solver/Mios.hs
Original file line number Diff line number Diff line change
Expand Up @@ -92,10 +92,15 @@ injectClauses :: Solver -> Int -> Int -> B.ByteString -> IO ()
injectClauses solver n m str = do
let
initialSize = 3
-- | skip comment lines and whitespaces
-- CAVEAT: this code interpretes 'c' as a comment designator even if it is placed in the middle of a line
skipToInt :: B.ByteString -> B.ByteString
skipToInt str = if B.head bol == 'c' then skipToInt $ B.dropWhile ('\n' /=) bol else bol
where bol = B.dropWhile (`elem` " \t\n") str
-- | read an Int and store it to /j/-th literal of /i/-th clause
loop :: Int -> Int -> B.ByteString -> FixedVecInt -> IO ()
loop i j str vec = do
case B.readInt $ B.dropWhile (`elem` " \t\n") str of
case B.readInt (skipToInt str) of
Just (0, str') -> do
setAt 0 vec (j - 1)
solver `addClause` vec
Expand Down

0 comments on commit 16addbd

Please sign in to comment.