Based on this very helpful answer I rewrote my solver-for-a-stateful-program to use the Query monad and an ever-increasing list of SMT variables standing for the inputs. I expected one of two outcomes from this: either the first part (generating the SMTLib output) is sped up a lot and becomes usable, or it still remains so slow that it might as well not work.
However, instead I get an error message from the SMT solver (Z3 in my case) complaining about a missing SMT variable in the SMTLib output. And looking at the output with verbose = True, lo and behold there really is a variable that is only referred to, but not defined:
** 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 ---
Searching at depth: 1
[GOOD] (declare-fun s0 () (_ BitVec 16))
[GOOD] (define-fun s1 () (_ BitVec 16) #x0000)
[GOOD] (define-fun s3 () (_ BitVec 16) #x0013)
[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 s12 () (_ BitVec 16) #x0001)
[GOOD] (define-fun s14 () (_ BitVec 16) #x0003)
[GOOD] (define-fun s15 () (_ BitVec 16) #x000a)
[GOOD] (define-fun s17 () (_ BitVec 16) #x0002)
[GOOD] (define-fun s18 () (_ BitVec 16) (bvneg #x0001))
[GOOD] (define-fun s20 () (_ BitVec 16) #x0007)
[GOOD] (define-fun s22 () (SBVMaybe (_ BitVec 16)) ((as just_SBVMaybe (SBVMaybe (_ BitVec 16))) #x0001))
[GOOD] (define-fun s23 () (SBVMaybe (_ BitVec 16)) (as nothing_SBVMaybe (SBVMaybe (_ BitVec 16))))
[GOOD] (define-fun s31 () (_ BitVec 16) #x00ff)
[GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 16))
[GOOD] (define-fun table0_initializer_0 () Bool (= (table0 #x0000) s17))
[GOOD] (define-fun table0_initializer_1 () Bool (= (table0 #x0001) s14))
[GOOD] (define-fun table0_initializer () Bool (and table0_initializer_0 table0_initializer_1))
[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 s13 () Bool (= s11 s12))
[GOOD] (define-fun s16 () Bool (= s11 s15))
[GOOD] (define-fun s19 () (_ BitVec 16) (proj_2_SBVTuple2 s10))
[GOOD] (define-fun s21 () Bool (= s19 s20))
[GOOD] (define-fun s24 () (SBVMaybe (_ BitVec 16)) (ite s21 s22 s23))
[GOOD] (define-fun s25 () (_ BitVec 16) (get_just_SBVMaybe s24))
[GOOD] (define-fun s26 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 16)))) s24))
[GOOD] (define-fun s27 () (_ BitVec 16) (ite s26 s18 s25))
[GOOD] (define-fun s28 () (_ BitVec 16) (ite (or (bvslt s27 #x0000) (bvsle #x0002 s27)) s18 (table0 s27)))
[GOOD] (define-fun s29 () Bool (distinct s12 s28))
[GOOD] (define-fun s30 () Bool (= s12 s27))
[GOOD] (define-fun s32 () (_ BitVec 16) (ite s30 s31 s14))
[GOOD] (define-fun s33 () (_ BitVec 16) (ite s29 s14 s32))
[GOOD] (define-fun s34 () (_ BitVec 16) (ite s16 s33 s14))
[GOOD] (define-fun s35 () (_ BitVec 16) (ite s13 s14 s34))
[GOOD] (define-fun s36 () Bool (= s12 s35))
[GOOD] (define-fun s37 () Bool ((_ pbeq 1 1) s36))
[GOOD] (assert s37)
[SEND] (check-sat)
[RECV] unsat
[GOOD] (pop 1)
[GOOD] (assert table0_initializer)
Searching at depth: 2
[GOOD] (declare-fun s38 () (_ BitVec 16))
[GOOD] (define-fun s39 () Bool (bvsle s1 s38))
[GOOD] (define-fun s40 () Bool (bvslt s38 s3))
[GOOD] (define-fun s41 () Bool (and s39 s40))
[GOOD] (assert s41)
[GOOD] (declare-fun s42 () (_ BitVec 16))
[GOOD] (define-fun s43 () Bool (bvsle s1 s42))
[GOOD] (define-fun s44 () Bool (bvslt s42 s3))
[GOOD] (define-fun s45 () Bool (and s43 s44))
[GOOD] (assert s45)
[GOOD] (push 1)
[GOOD] (define-fun s51 () (_ BitVec 16) #x0006)
[GOOD] (declare-fun table1 ((_ BitVec 16)) (_ BitVec 16))
[GOOD] (define-fun table1_initializer_0 () Bool (= (table1 #x0000) s1))
[GOOD] (define-fun table1_initializer_1 () Bool (= (table1 #x0001) s17))
[GOOD] (define-fun table1_initializer_2 () Bool (= (table1 #x0002) s1))
[GOOD] (define-fun table1_initializer_3 () Bool (= (table1 #x0003) s1))
[GOOD] (define-fun table1_initializer_4 () Bool (= (table1 #x0004) s1))
[GOOD] (define-fun table1_initializer_5 () Bool (= (table1 #x0005) s1))
[GOOD] (define-fun table1_initializer () Bool (and table1_initializer_0 table1_initializer_1 table1_initializer_2 table1_initializer_3 table1_initializer_4 table1_initializer_5))
[GOOD] (assert table1_initializer)
[GOOD] (declare-fun table2 ((_ BitVec 16)) (_ BitVec 16))
[FAIL] (define-fun table2_initializer_0 () Bool (= (table2 #x0000) s73))
[SYNC] Attempting to synchronize with tag: "terminating upon unexpected response (at: 2020-07-04 12:44:46.557353117 +08)"
[FIRE] (echo "terminating upon unexpected response (at: 2020-07-04 12:44:46.557353117 +08)")
[SYNC] Synchronization achieved using tag: "terminating upon unexpected response (at: 2020-07-04 12:44:46.557353117 +08)"
*** Exception:
*** Data.SBV: Unexpected response from the solver, context: define-fun:
***
*** Sent : (define-fun table2_initializer_0 () Bool (= (table2 #x0000) s73))
*** Expected : success
*** Received : (error "line 90 column 60: unknown constant s73")
***
*** Executable: z3
*** Options : -nw -in -smt2
(full code on Github). How do I debug this? Is this even possibly a bug in my program, or is this a bug in SBV itself?
EDIT: I managed to reproduce this with a single self-contained module with no outside dependencies other than MTL/Transformers and of course SBV itself:
{-# 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]
Full SMTLib 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] (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))
Error message:
[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
This seems to be a bug in SBV. Reporting it at the github repo is the right thing to do.
Note: Should be fixed as of this commit. Please give it a try!