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

在此页，我发现了以下引语：

命令 eval计算Z3生成的上一个模型中的表达式。它本质上是在执行Z3生成的“函数程序”。

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

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