decoding of literals of unconstrained variables

[jwaldmann]

This looks super wrong (both b and not b are False)

print @(Result, Maybe _)  =<< (solveWith minisat $ do b <- exists @Bit; return [b, not b])  
(Satisfied,Just [False,False])

The bug seems to appear for unconstrained variables. Adding a useless constraint helps:

print @(Result, Maybe _)  =<< (solveWith minisat $ do b <- exists @Bit; assert $ b === b; return [b, not b])     
(Satisfied,Just [False,True])

Still I don't quite understand the behaviour, and don't know where to fix it.

[jwaldmann]

Ah, I see now: https://github.com/ekmett/ersatz/blob/master/src/Ersatz/Bit.hs#L126

instance Codec Bit where
  decode sol b
      = maybe (pure False <|> pure True) pure $
        solutionStableName sol (unsafePerformIO (makeStableName' b))
    <|> case b of
          Not c'  -> not <$> decode sol c'
          Var l   -> decode sol l

In the example, b = Var 2, and not b = Var (-2), so the case Not c' is never used. Instead, both literals go through solutionStableName, which returns Nothing, so the fallback (pure False <|> pure True) is used, giving value False in both cases.

[jwaldmann]

So, one solution is

-          Var l   -> decode sol l
+          Var l -> if literalId l >= 0
+                   then decode sol l
+                   else not <$> decode sol l

[jwaldmann]

The above explanation is right (using pure False <|> pure True) , but also wrong. The given source location is for decoding Var l :: Bit, while decoding l :: Literal is at https://github.com/ekmett/ersatz/blob/master/src/Ersatz/Codec.hs#L39 So the fix should probably be applied there.

[glguy]

This seems to be fixed in master.

[RyanGlScott]

I don't think that this was actually fixed, as this:

print @(Result, Maybe _)  =<< (solveWith minisat $ do b <- exists @Bit; return [b, not b])

Still returns an incorrect result:

(Satisfied,Just [False,False])

See also #76.