我试图以一种自动查询所有可用值的方式从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和递归调用)。
有人有什么想法吗?
在this page,我发现了以下引用:
命令
eval
计算Z3生成的最后一个模型中的表达式。它本质上是执行Z3生成的“功能程序”。
由于eval是<command>
,因此它不能在<term>
表达式中使用。
我相信模型枚举应该更容易使用一些API接口而不是SmtLibv2 format,因为人们可以轻松地编写一个循环,交替可满足性检查与学习阻塞子句,从而从搜索空间中删除以前找到的解决方案。