У меня есть процесс с отслеживанием состояния, который моделируется как i -> RWS r w s a. Я хочу передать ему вход cmds :: [i]; в настоящее время я делаю это оптом:
let play = runGame theGame . go
where
go [] = finished
go ((v, n):cmds) = do
end1 <- stepWorld
end2 <- ite (SBV.isJust end1) (return end1) $ stepPlayer (v, n)
ite (SBV.isJust end2) (return end2) $ go cmds
Я могу попробовать найти ввод заданного размера следующим образом:
result <- satWith z3{ verbose = True } $ do
cmds <- mapM sCmd [1..inputLength]
return $ SBV.fromMaybe sFalse $ fst $ play cmds
Однако это дает мне ужасную производительность в самом SBV, то есть до вызова Z3 (я вижу, что это так, потому что вывод verbose показывает мне, что все время тратится до вызова (check-sat)). Это даже если inputLength установлено на что-то маленькое, например 4.
Однако если для inputLength установлено значение 1 или 2, весь процесс выполняется очень быстро. Поэтому я надеюсь, что есть способ запустить SBV, чтобы получить модель поведения одного шага i -> s -> (s, a), а затем указать SMT-решателю продолжать повторять эту модель для n разных is.
Итак, вот мой вопрос: в вычислении с отслеживанием состояния, подобном этому, когда я хочу подавать переменные SMT в качестве входных данных для вычисления с отслеживанием состояния, есть ли способ позволить решателю SMT повернуть свою рукоятку на избежать плохой работы SBV?
Я предполагаю, что упрощенный типовой вопрос будет таким: если у меня есть функция f :: St -> St и предикат p :: St -> SBool, и я хочу решить для n :: SInt такое, что p (iterateN n f x0), каков рекомендуемый способ сделать это с SBV, предположим Mergeable St?
EDIT: я загрузил весь код на Github но имейте в виду, что это не минималистичный пример; на самом деле это даже не очень хороший код на Haskell.
