push/pop and arrays are interacting badly

[LeventErkok]

This is a consequence of how we define arrays under certain circumstances: By putting in assertions to say which entries should equal to what. The problem is that these definitional asserts are interacting badly with push/pop, since we want to preserve them! To wit, consider:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import Data.SBV.Control

bad = runSMT $ do (a :: SArray Integer Integer) <- newArray "a"
                  query $ loop (writeArray a 1 1) []
  where loop a sofar = do push 1
                          constrain $ readArray a 1 .== 5
                          cs <- checkSat
                          case cs of
                            Unk   -> error "Unknown"
                            Unsat -> do pop 1
                                        d <- freshVar $ "d" ++ show (length sofar)
                                        constrain $ d .>= 1 &&& d .< 4
                                        loop (writeArray a 1 (readArray a 1 + d)) (sofar ++ [d])
                            Sat   -> do ds <- mapM getValue sofar
                                        io $ print ds

good = runSMT $ do setLogic Logic_ALL
                   query $ loop 1 []
  where loop a sofar = do push 1
                          constrain $ a .== (5 :: SInteger)
                          cs <- checkSat
                          case cs of
                            Unk   -> error "Unknown"
                            Unsat -> do pop 1
                                        d <- freshVar $ "d" ++ show (length sofar)
                                        constrain $ d .>= 1 &&& d .< 4
                                        loop (a + d) (sofar ++ [d])
                            Sat   -> do ds <- mapM getValue sofar
                                        io $ print ds

We get:

*Main> good
[1,3]
*Main> bad
[1]

This is rather unfortunate, and very confusing till you figure out what's going on.

Here's a lengthier and more interesting example:

-- https://www5.cadence.com/2018ClubVQuiz_LP.html

import Data.SBV
import Data.SBV.Control

type Color  = SWord8
type Button = SWord8
type Grid   = SArray Word8 Word8

black, blue, green, red :: Color
[black, blue, green, red] = [0, 1, 2, 3]

next :: Button -> Grid -> Grid
next b g = ite (readArray g b .== black) g
         $ ite (b .==  5)                (rot [ 1,  2,  6, 10,  9,  4])
         $ ite (b .==  6)                (rot [ 2,  3,  7, 11, 10,  5])
         $ ite (b .==  9)                (rot [ 4,  5, 10, 14, 13,  8])
         $ ite (b .== 10)                (rot [ 5,  6, 11, 15, 14,  9])
         $ ite (b .== 11)                (rot [ 6,  7, 12, 16, 15, 10])
         $ ite (b .== 14)                (rot [ 9, 10, 15, 18, 17, 13])
         $ ite (b .== 15)                (rot [10, 11, 16, 19, 18, 14]) g
  where rot xs = foldr (\(i, c) a -> writeArray a (literal i) c) g (zip new cur)
          where cur = map (readArray g . literal) xs
                new = tail xs ++ [head xs]

cover :: IO ()
cover = runSMT $ do newGrid <- newArray "grid"

                    let initGrid = foldr (\(i, c) a -> writeArray a (literal i) c) newGrid (zip [1..] initBoard)

                    query $ loop (0 :: Int) initGrid []

  where loop i g sofar = do io $ putStrLn $ "Searching at depth: " ++ show i

                            push 1
                            constrain $ map (readArray g . literal) [1..19] .== finalBoard
                            cs <- checkSat
                            case cs of
                              Unk   -> error $ "Solver said Unknown, depth: " ++ show i
                              Unsat -> do pop 1
                                          b <- freshVar ("press_" ++ show i)
                                          constrain $ b `sElem` map literal [5, 6, 9, 10, 11, 14, 15]
                                          loop (i+1) (next b g) (sofar ++ [b])
                              Sat   -> do vs <- mapM getValue sofar
                                          io $ putStrLn $ "Covered: " ++ show vs
                                          findOthers sofar vs

        findOthers vs cs = go cs
                where go curVals = do constrain $ bOr $ zipWith (\v c -> v ./= literal c) vs curVals
                                      cs <- checkSat
                                      case cs of
                                       Unk   -> error $ "Unknown!"
                                       Unsat -> io $ putStrLn $ "There are no more solutions."
                                       Sat   -> do newVals <- mapM getValue vs
                                                   io $ putStrLn $ "Covered: " ++ show newVals
                                                   go newVals

initBoard, finalBoard :: [Color]
initBoard  = [black, black, black, red, blue, green, red, black, green, green, green, black, red, green, green, red, black, black, black]
finalBoard = [black, red, black, black, green, green, black, red, green, blue, green, red, black, green, green, black, black, red, black]

main :: IO ()
main = cover

This currently returns:

*Main> main
Searching at depth: 0
Searching at depth: 1
Covered: [15]

which is completely bogus.

The correct answer must be one of:

[10, 10, 11, 9, 14, 6]

OR

[10, 10, 9, 11, 14, 6]

The code we need to fix seems to be located in:

• constTable
• declArray

Though it's not clear how to fix this right away. Also, would be good to audit all uses of assert to make sure they don't come from a "definitional" context that we want to preserve them; as otherwise a pop would kill them.

[LeventErkok]

NB. There's a workaround in this particular scenario: Instead of push/pop, use checkSatAssuming at each iterative loop with the assumption we're asserting. This avoids the issue since there are no more push/pop calls.

But of course, this doesn't address the bug itself: We need to at least catch it and flag it!

[LeventErkok]

Suggestion from Martin on the SMTLib mailing list:

*. I guess you could ...

(define-fun A_0_0 () Bool (= (select A 0) 0))
(define-fun A_1_1 () Bool (= (select A 1) 1))
(define-fun A_2_2 () Bool (= (select A 2) 2))

(define-fun A_assign () Bool (and A_0_0 A_1_1 A_2_2 ...))

We should either implement this; or at least recognize and reject such scenarios. (Otherwise we're unsound!)