SMTLib output has missing bindings

[gergoerdi]

I am getting the following output from SBV:

*** Data.SBV: Unexpected response from the solver, context: define-fun:
***
***    Sent      : (define-fun table1_initializer_0 () Bool (= (table1 #x0000) s57))
***    Expected  : success
***    Received  : (error "line 78 column 60: unknown constant s57")
***
***    Executable: z3
***    Options   : -nw -in -smt2

Looking at the SMTLib output with verbose = True, I see that indeed s57 is not part of the output:

** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; external query, using all logics.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (declare-fun s0 () (_ BitVec 16))
[GOOD] (define-fun s1 () (_ BitVec 16) #x0000)
[GOOD] (define-fun s3 () (_ BitVec 16) #x0001)
[GOOD] (define-fun s2 () Bool (bvsle s1 s0))
[GOOD] (define-fun s4 () Bool (bvslt s0 s3))
[GOOD] (define-fun s5 () Bool (and s2 s4))
[GOOD] (assert s5)
[GOOD] (declare-fun s6 () (_ BitVec 16))
[GOOD] (define-fun s7 () Bool (bvsle s1 s6))
[GOOD] (define-fun s8 () Bool (bvslt s6 s3))
[GOOD] (define-fun s9 () Bool (and s7 s8))
[GOOD] (assert s9)
[GOOD] (push 1)
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
                                           ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
                                                         (proj_2_SBVTuple2 T2))))))
[GOOD] (declare-datatypes ((SBVMaybe 1)) ((par (T)
                                           ((nothing_SBVMaybe)
                                            (just_SBVMaybe (get_just_SBVMaybe T))))))
[GOOD] (define-fun s13 () (_ BitVec 16) #x000a)
[GOOD] (define-fun s15 () (_ BitVec 16) (bvneg #x0001))
[GOOD] (define-fun s17 () (_ BitVec 16) #x0007)
[GOOD] (define-fun s19 () (SBVMaybe (_ BitVec 16)) ((as just_SBVMaybe (SBVMaybe (_ BitVec 16))) #x0000))
[GOOD] (define-fun s20 () (SBVMaybe (_ BitVec 16)) (as nothing_SBVMaybe (SBVMaybe (_ BitVec 16))))
[GOOD] (define-fun s28 () (_ BitVec 16) #x00ff)
[GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 16))
[GOOD] (define-fun table0_initializer_0 () Bool (= (table0 #x0000) s3))
[GOOD] (define-fun table0_initializer () Bool table0_initializer_0)
[GOOD] (assert table0_initializer)
[GOOD] (define-fun s10 () (SBVTuple2 (_ BitVec 16) (_ BitVec 16)) (mkSBVTuple2 s0 s6))
[GOOD] (define-fun s11 () (_ BitVec 16) (proj_1_SBVTuple2 s10))
[GOOD] (define-fun s12 () Bool (= s3 s11))
[GOOD] (define-fun s14 () Bool (= s11 s13))
[GOOD] (define-fun s16 () (_ BitVec 16) (proj_2_SBVTuple2 s10))
[GOOD] (define-fun s18 () Bool (= s16 s17))
[GOOD] (define-fun s21 () (SBVMaybe (_ BitVec 16)) (ite s18 s19 s20))
[GOOD] (define-fun s22 () (_ BitVec 16) (get_just_SBVMaybe s21))
[GOOD] (define-fun s23 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 16)))) s21))
[GOOD] (define-fun s24 () (_ BitVec 16) (ite s23 s15 s22))
[GOOD] (define-fun s25 () (_ BitVec 16) (ite (or (bvslt s24 #x0000) (bvsle #x0001 s24)) s15 (table0 s24)))
[GOOD] (define-fun s26 () Bool (= s1 s25))
[GOOD] (define-fun s27 () Bool (= s1 s24))
[GOOD] (define-fun s29 () (_ BitVec 16) (ite s27 s28 s3))
[GOOD] (define-fun s30 () (_ BitVec 16) (ite s26 s29 s3))
[GOOD] (define-fun s31 () (_ BitVec 16) (ite s14 s30 s3))
[GOOD] (define-fun s32 () (_ BitVec 16) (ite s12 s3 s31))
[GOOD] (define-fun s33 () Bool (= s3 s32))
[GOOD] (define-fun s34 () Bool ((_ pbeq 1 1) s33))
[GOOD] (assert s34)
[SEND] (check-sat)
[RECV] sat
[GOOD] (pop 1)
[GOOD] (assert table0_initializer)
[GOOD] (declare-fun s35 () (_ BitVec 16))
[GOOD] (define-fun s36 () Bool (bvsle s1 s35))
[GOOD] (define-fun s37 () Bool (bvslt s35 s3))
[GOOD] (define-fun s38 () Bool (and s36 s37))
[GOOD] (assert s38)
[GOOD] (declare-fun s39 () (_ BitVec 16))
[GOOD] (define-fun s40 () Bool (bvsle s1 s39))
[GOOD] (define-fun s41 () Bool (bvslt s39 s3))
[GOOD] (define-fun s42 () Bool (and s40 s41))
[GOOD] (assert s42)
[GOOD] (push 1)
[GOOD] (define-fun s48 () (_ BitVec 16) #x0006)
[GOOD] (define-fun s56 () (_ BitVec 16) #x0002)
[GOOD] (declare-fun table1 ((_ BitVec 16)) (_ BitVec 16))
[FAIL] (define-fun table1_initializer_0 () Bool (= (table1 #x0000) s57))

Unfortunately, the only way I have of reproducing it at the moment is a 150-line module; bear in mind that this is already the result of a significant reduction effort, as the original code was much more complicated. Here is the minimised version with no external dependencies other than MTL/Transformers:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
module Main (main) where

import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State

import Data.Int

import GHC.Generics (Generic)
import Data.SBV
import Data.SBV.Control
import qualified Data.SBV.Maybe as SBV
import qualified Data.SBV.Tuple as SBV

data S = S
    { currentRoom :: SInt16
    , itemLocations :: [SInt16]
    } deriving (Show, Generic, Mergeable)

main :: IO ()
main = do
    let theGame = Game
            { gameDictSize = 1
            , gameItems = [7]
            , gameRooms = [[0],[2]]
            }


    let genWord = do
            word <- freshVar_
            constrain $ 0 .<= word .&& word .< literal (gameDictSize theGame)
            return word
        genCmd = do
            verb <- genWord
            noun <- genWord
            return $ SBV.tuple (verb, noun)

    cmds <- runSMTWith z3{ verbose = True} $ do
        query $ do
            s <- return $ initState theGame

            let step cmd = do
                    let (verb, noun) = SBV.untuple cmd
                    runGame theGame $ stepPlayer (verb, noun)

            cmd1 <- genCmd
            push 1
            (finished, s) <- return $ runState (step cmd1) s
            constrain finished
            _cs <- checkSat
            pop 1

            cmd2 <- genCmd
            push 1
            (finished, s) <- return $ runState (step cmd2) s
            constrain finished
            cs <- checkSat

            mapM getValue [cmd1, cmd2]

    mapM_ print cmds

instance forall a. Mergeable a => Mergeable (Identity a) where
    symbolicMerge force cond thn els = Identity $ symbolicMerge force cond (runIdentity thn) (runIdentity els)

instance (Mergeable a, forall a. Mergeable a => Mergeable (m a)) => Mergeable (ReaderT r m a) where
    symbolicMerge force cond thn els = ReaderT $ symbolicMerge force cond (runReaderT thn) (runReaderT els)

instance (Mergeable s, Mergeable a, forall a. Mergeable a => Mergeable (m a)) => Mergeable (StateT s m a) where
    symbolicMerge force cond thn els = StateT $ symbolicMerge force cond (runStateT thn) (runStateT els)

data Game = Game
    { gameDictSize :: Int16
    , gameItems :: [Int16]
    , gameRooms :: [[Int16]]
    }
    deriving (Show)

type SInput = (SInt16, SInt16)

type Engine = ReaderT Game (State S)

carried :: Int16
carried = 255

initState :: Game -> S
initState game = S
    { currentRoom = 0
    , itemLocations = [1]
    }

runGame :: Game -> Engine a -> State S a
runGame game act = runReaderT act game

stepPlayer :: SInput -> Engine SBool
stepPlayer (v, n) = do
    perform (v, n)
    finished

finished :: Engine SBool
finished = do
    locs <- gets itemLocations
    return $ map (.== 1) locs `pbExactly` 1

perform :: SInput -> Engine ()
perform (verb, noun) = sCase verb (return ())
    [ (1, builtin_go)
    , (10, builtin_get)
    ]
  where
    builtin_go = sWhen (1 .<= noun .&& noun .<= 6) $ do
        let dir = noun - 1
        here <- gets currentRoom
        exits <- asks $ (.!! here) . map (map literal) . gameRooms
        let newRoom = select exits 0 dir
        sUnless (newRoom .== 0) $ modify $ \s ->
          s{ currentRoom = newRoom }

    builtin_get = do
        locs <- gets itemLocations
        here <- gets currentRoom
        items <- asks gameItems
        let item = SBV.fromMaybe (-1) $ sFindIndex (\name -> noun .== literal name) $ items
        sWhen (select locs (-1) item .== here) $ modify $ \s ->
          s{ itemLocations = replaceAt item (literal carried) (itemLocations s) }

(.!!) :: (Mergeable a) => [a] -> SInt16 -> a
xs .!! i = case xs of
    [] -> error "(.!) : empty array"
    xs@(x:_) -> select xs x i

replaceAt :: (Mergeable a) => SInt16 -> a -> [a] -> [a]
replaceAt i x' = map (\(j, x) -> ite (i .== literal j) x' x) . zip [0..]

sCase :: (Mergeable a) => SInt16 -> a -> [(Int16, a)] -> a
sCase x def = go
  where
    go [] = def
    go ((k,v):kvs) = ite (x .== literal k) v (go kvs)

sUnless :: (Monad m, Mergeable (m ())) => SBool -> m () -> m ()
sUnless b act = ite b (return ()) act

sWhen :: (Monad m, Mergeable (m ())) => SBool -> m () -> m ()
sWhen b act = ite b act (return ())

sFindIndex :: (a -> SBool) -> [a] -> SMaybe Int16
sFindIndex p = go 0
  where
    go i [] = SBV.sNothing
    go i (x:xs) = ite (p x) (SBV.sJust i) (go (i + 1) xs)

Tested with SBV 8.8 running on GHC 8.8.3.

[gergoerdi]

Managed to make it just a tiny bit smaller at 62 lines now:

{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Main (main) where

import Control.Monad.State

import Data.Int

import Data.SBV
import Data.SBV.Control

data Game = Game
    { gameItems :: [Int16]
    , gameRooms :: [[Int16]]
    }
    deriving (Show)

main :: IO ()
main = do
    let theGame = Game
            { gameItems = [1]
            , gameRooms = [[0],[1]]
            }

    runSMTWith z3{ verbose = True} $ query $ do
        let round s = do
                word <- freshVar_
                return $ runState (stepPlayer theGame word) s

        s <- return [0]
        (finished, s) <- round s
        (finished, s) <- round s
        constrain finished
        checkSat
        return ()

instance (Mergeable s, Mergeable a) => Mergeable (State s a) where
    symbolicMerge force cond thn els = state $ symbolicMerge force cond (runState thn) (runState els)

type Engine = State [SInt16]

stepPlayer :: Game -> SInt16 -> Engine SBool
stepPlayer Game{..} word = do
    ite (word .== 1) builtin_go builtin_get
    locs <- get
    return $ map (.== 1) locs `pbExactly` 1
  where
    builtin_go = do
        ~[here] <- get
        let rooms@(room:_) = map (map literal) gameRooms
        let exits = select rooms room here
        let newRoom = select exits 0 word
        ite (newRoom .== 0) (return ()) $ put [1]

    builtin_get = do
        locs <- get
        let item = literal . head $ gameItems
        ite (select locs (-1) item ./= 0) (return ()) $ put [255]

The SMTLib output is also considerably smaller:

** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; external query, using all logics.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (declare-fun s0 () (_ BitVec 16))
[GOOD] (declare-fun s1 () (_ BitVec 16))
[GOOD] (define-fun s2 () (_ BitVec 16) #x0001)
[GOOD] (define-fun s5 () (_ BitVec 16) #x0000)
[GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 16))
[FAIL] (define-fun table0_initializer_0 () Bool (= (table0 #x0000) s8))

[SYNC] Attempting to synchronize with tag: "terminating upon unexpected response (at: 2020-07-06 11:52:17.00269423 +08)"
[FIRE] (echo "terminating upon unexpected response (at: 2020-07-06 11:52:17.00269423 +08)")
[SYNC] Synchronization achieved using tag: "terminating upon unexpected response (at: 2020-07-06 11:52:17.00269423 +08)"
*** Exception: 
*** Data.SBV: Unexpected response from the solver, context: define-fun:
***
***    Sent      : (define-fun table0_initializer_0 () Bool (= (table0 #x0000) s8))
***    Expected  : success
***    Received  : (error "line 12 column 60: unknown constant s8")
***
***    Executable: z3
***    Options   : -nw -in -smt2

[LeventErkok]

Thanks for the report. This seems to be a bug in SBV; some unexpected interaction. I'll investigate.

[LeventErkok]

@gergoerdi

I pushed in a fix that should address this issue. But it's rather finicky, so please do some testing and let me know if it solves the problem.

Note that I ran into a z3 bug while working on this, and reported here: Z3Prover/z3#4565

If you run into that, I recommend downloading a version of z3 that's pre-Jun-24th of this year; this bug seems to have crept after that date into z3.

[LeventErkok]

@gergoerdi

Looking at the code again, this isn't quite fixed yet. Please delay testing. It'll need some more work.

[LeventErkok]

@gergoerdi

I pushed in changes that should address this issue. (And the z3 bug is fixed as well.)

Can you give it a try and let me know if it all works fine?

[gergoerdi]

Holy moly, the code assembles SMTLib output as a string?!

I was hoping it has an AST representation which gets coparsed into a string at the edges only...

[LeventErkok]

That rendering is precisely what I'd call the "edges." Is this causing you problems?

[gergoerdi]

No, it's just surprising.

[gergoerdi]

I can confirm that both my cut-down test case and my original program works with the fix in
036ce4e.

[LeventErkok]

Thanks for the report.

[LeventErkok]

Sure, please file a new issue. There could always be bugs/performance issues.