首页 文章

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

提问于
浏览
1

我试图以一种自动查询所有可用值的方式从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 副作用而不是构建列表,但是没有't work either, because I can't序列语句(eval和递归调用) .

有人有什么想法吗?

1 回答

  • 1

    this page,我发现了以下引用:

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

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


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

相关问题