有人可以指出为什么最终查询没有输出吗?
基本上我告诉Z3如果vs-)vd和vs->ss和vd->sd,那么sd是从ss派生的。
(set-option :fixedpoint.engine datalog)
(define-sort site () (_ BitVec 3))
(declare-rel pointsto (Int site))
(declare-rel dcall (Int Int))
(declare-rel derived (site site))
(declare-var vs Int)
(declare-var vd Int)
(declare-var ss site)
(declare-var sd site)
;;;;; definition of derived ;;
(rule (=> (and (dcall vs vd) (pointsto vs ss) (pointsto vd sd)) (derived ss sd)))
(rule (dcall 11 12))
(rule (pointsto 11 #b001))
(rule (pointsto 12 #b010))
(query (derived #b001 #b010))
最佳答案
这个例子揭示了一些事情。我会尝试完成这些。
- 查询返回“sat”或“unsat”。在“sat”情况下,存在与查询中的自由变量相对应的一组元组,使得查询是可导出的。要打印这些元组,您可以指定“:print-answer true”作为选项。
- 您的特定查询不包含任何自由变量,因此没有要打印的元组。
- 我添加了另一个包含自由变量的示例,Z3 打印了一个解决方案。
- 数据记录引擎并不真正支持无限域。您应该使用 bool 值、位向量或有限域值的关系(一种用于以数据记录格式输入的程序的特殊排序)。我已更改您的示例以使用位向量。
(set-option :fixedpoint.engine datalog)
(define-sort site () (_ BitVec 3))
(define-sort Loc () (_ BitVec 8))
(declare-rel pointsto (Loc site))
(declare-rel dcall (Loc Loc))
(declare-rel derived (site site))
(declare-var vs Loc)
(declare-var vd Loc)
(declare-var ss site)
(declare-var sd site)
;;;;; definition of derived ;;
(rule (=> (and (dcall vs vd) (pointsto vs ss) (pointsto vd sd)) (derived ss sd)))
(rule (dcall (_ bv11 8) (_ bv12 8)))
(rule (pointsto (_ bv11 8) #b001))
(rule (pointsto (_ bv12 8) #b010))
(query (derived #b001 #b010)
:print-answer true)
(query (derived #b001 ss)
:print-answer true)
关于z3 - Z3 中的固定点,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/29725654/