Why does Z3 return unknown result?

Question

all, I am a newer to use Z3. I wrote this smt2 file, but the result return unknown, what is wrong in my file?

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

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2015-05-20T22:38:45

As a different post explains, the datalog engine should only use finite sorts. THe newest unstable version of Z3 will reject the input above and indicate that arguments to predicates should be over a finite domain type. Here is the example rewritten:

(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 reports "sat", in other words, the query can be derived

Why does Z3 return unknown result?

1 Answers