фиксированные точки в Z3

Question

Может ли кто-то любезно указать, почему окончательный запрос не имеет выхода?

В основном я говорю 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)) 

Answer 1

Этот пример раскрывает несколько вещей. Я попытаюсь пройти через них.

1. Запрос возвращает «sat» или «unsat». В случае «sat» имеется набор кортежей, соответствующих свободным переменным в запросе, так что запрос выводится. Чтобы напечатать эти кортежи, вы можете указать «: print-answer true» в качестве опции.
2. В вашем конкретном запросе не содержится свободных переменных, поэтому нет кортежей для печати.
3. Я добавил еще один пример, содержащий свободные переменные, и Z3 печатает решение.
4. Механизм datalog действительно не поддерживает бесконечные домены. Вы должны использовать отношения над булевыми, битовыми векторами или конечными значениями домена (специальный вид, используемый для программ, введенных в формат datalog). Я изменил ваш пример на использование битовых векторов.

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