Z3/SMT-LIB 评估功能和收集结果

Question

我正在尝试以一种自动查询所有可用值的方式从 Z3 中获取一些值：

(define-fun-rec out ((p Pkg) (t Time)) (List Bool)
  (ite (< t 0) (as nil (List Bool)) (insert (eval (installed p t)) (out p (- t 1)))))

(eval (out a t-final))

不幸的是，这给了我错误unknown function/constant eval

我还尝试在函数中执行 eval 副作用而不是构建列表，但这也不起作用，因为我无法对语句进行排序（eval 和递归调用）。

有人有什么想法吗？

Answer 1

在this page，我找到了以下引用：

命令 eval 计算最后一个模型中的表达式 Z3。它本质上是在执行Z3产生的“功能程序”。

由于 eval 是 <command>，因此它不能在 <term> 表达式中使用。

---

我相信模型枚举应该使用一些 API 接口而不是 SmtLibv2 format 更容易，因为人们可以轻松地编写一个循环，将可满足性检查与学习阻塞子句交替进行，该阻塞子句从搜索空间中删除以前找到的解决方案。