Z3中的固定点数

有人可以指出为什么最终查询没有输出吗？Z3中的固定点数

基本上我告诉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))

来源

2015-04-19 Tim

的语法似乎是错误的。为什么你写 pointsto（VS SS）代替（pointsto VS SS）？ –

对不起。一个错字。现在纠正。但仍然没有结果显示。 – Tim

通过运行本地Z3而不是rise4fun，我发现“libC++ abi.dylib：以std :: bad_cast：std :: bad_cast类型的未捕获异常终止” – Tim

这个例子暴露了一些东西。我会尝试通过这些。

查询返回“sat”或“unsat”。在“sat”情况下，有一组元组对应于查询中的自由变量，以便查询是可导出的。要打印这些元组，您可以指定“：print-answer true”作为选项。
您的特定查询不包含任何自由变量，因此没有要打印的元组。
我添加了另一个包含自由变量和Z3打印解决方案的示例。
数据记录引擎并不真正支持无限域。您应该使用布尔关系，位向量或有限域值（用于以数据记录格式输入的程序的特殊排序）的关系。我改变了你的例子使用位向量。

(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)

来源

2015-05-20 18:51:40

Z3中的固定点数

回答

相关问题