points fixes dans Z3

Question

Quelqu'un peut-il préciser pourquoi la requête finale n'a pas de sortie? Fondamentalement, je dis à Z3 si vs-) vd et vs-> ss et vd-> sd, alors sd est dérivé de 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

Cet exemple expose quelques éléments. Je vais essayer de passer par ceux-ci.

1. La requête renvoie "sat" ou "unsat". Dans le cas "sat", il existe un ensemble de tuples correspondant aux variables libres dans la requête, de sorte que la requête est dérivable. Pour imprimer ces tuples, vous pouvez spécifier ": print-answer true" en option.
2. Votre requête particulière ne contient aucune variable libre, donc il n'y a pas de tuples à imprimer.
3. J'ai ajouté un autre exemple qui contient des variables libres et Z3 imprime une solution.
4. Le moteur de génération de données ne prend pas réellement en charge les domaines infinis. Vous devez utiliser des relations sur des booléens, des vecteurs de bits ou des valeurs de domaine finis (un tri spécial utilisé pour les programmes entrés au format datalog). J'ai changé votre exemple pour utiliser des vecteurs binaires.

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