为什么 Z3 返回未知结果？答案

【问题标题】：Why does Z3 return unknown result?为什么 Z3 返回未知结果？
【发布时间】：2015-04-23 19:31:18
【问题描述】：

所有，我是使用 Z3 的新手。我写了这个 smt2 文件，但结果返回未知，我的文件有什么问题？

(set-option :fixedpoint.engine datalog)

(define-sort site () (_ BitVec 3))

(declare-rel pointsto (Int Int)) ;used to get all points-to relation
(declare-rel dcall (Int Int)) ;used to label all function call or assignment
(declare-rel derived (Int Int))  ;used to get h1->hk
(declare-rel assign (Int Int))

(declare-var vs Int)
(declare-var vd Int)
(declare-var ss Int)
(declare-var sd Int)
(declare-var sm Int)

;;;;; definition of derived ;;;
(rule (=> (dcall vs vd) (pointsto vs vd)))
(rule (=> (and (dcall vs vd) (pointsto vs ss) (pointsto vd sd) ) (derived ss sd)))          
(rule (=> (and (derived ss sm) (derived sm sd)) (derived ss sd)))

;facts 0-999 for var, 999** for addr
;(rule (dcall 3 6));src and sink
(rule (dcall 3 4))
(rule (dcall 4 6))

(rule (pointsto 0 9992))
(rule (pointsto 1 9991))
(rule (pointsto 2 9991))
(rule (pointsto 3 99948))
(rule (pointsto 4 99950))
(rule (pointsto 5 99928))
(rule (pointsto 6 9999))

(query (derived 99948 9999))

【问题讨论】：

标签： z3

【解决方案1】：

正如另一篇文章所解释的，数据记录引擎应该只使用有限排序。 Z3 的最新不稳定版本将拒绝上面的输入，并指示谓词的参数应该是有限域类型。这是重写的示例：

(set-option :fixedpoint.engine datalog)

(define-sort site () (_ BitVec 3))
(define-sort Loc () (_ BitVec 16))


(declare-rel pointsto (Loc Loc)) ;used to get all points-to relation
(declare-rel dcall (Loc Loc)) ;used to label all function call or assignment
(declare-rel derived (Loc Loc))  ;used to get h1->hk
(declare-rel assign (Loc Loc))

(declare-var vs Loc)
(declare-var vd Loc)
(declare-var ss Loc)
(declare-var sd Loc)
(declare-var sm Loc)

;;;;; definition of derived ;;;
(rule (=> (dcall vs vd) (pointsto vs vd)))
(rule (=> (and (dcall vs vd) (pointsto vs ss) (pointsto vd sd) ) (derived ss sd)))          
(rule (=> (and (derived ss sm) (derived sm sd)) (derived ss sd)))

;facts 0-999 for var, 999** for addr
;(rule (dcall (_ bv3 16) (_ bv6 16)));src and sink
(rule (dcall (_ bv3 16) (_ bv4 16)))
(rule (dcall (_ bv4 16) (_ bv6 16)))

(rule (pointsto (_ bv0 16) (_ bv9992 16)))
(rule (pointsto (_ bv1 16) (_ bv9991 16)))
(rule (pointsto (_ bv2 16) (_ bv9991 16)))
(rule (pointsto (_ bv3 16) (_ bv99948 16)))
(rule (pointsto (_ bv4 16) (_ bv99950 16)))
(rule (pointsto (_ bv5 16) (_ bv9992 16)))
(rule (pointsto (_ bv6 16) (_ bv9999 16)))

(query (derived (_ bv99948 16) (_ bv9999 16)))

Z3 报告“sat”，也就是说可以推导出查询

【讨论】：