基于这个非常有用的答案，我重写了我的solver-for-a-stateful-program 以使用Querymonad 和一个不断增加的SMT 变量列表来代表输入。我期望由此产生的两个结果之一：第一部分（生成 SMTLib 输出）被加速并变得可用，或者它仍然很慢以至于它可能无法工作。
但是，相反，我从 SMT 求解器（在我的情况下为 Z3）收到一条错误消息，抱怨 SMTLib 输出中缺少 SMT 变量。看看输出verbose = True，你看，确实有一个变量只被引用，但没有定义：
** 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
（ Github 上的完整代码）。我该如何调试？这甚至可能是我程序中的错误，还是 SBV 本身的错误？
编辑：我设法用一个独立的模块重现了这个，除了 MTL/Transformers，当然还有 SBV 本身，没有外部依赖项：
{-# 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]
完整的 SMTLib 输出：
** 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