Est-il possible de détecter des équations incohérentes dans Z3, ou avant de passer à Z3?

Question

Je travaillais avec z3 avec l'exemple suivant.

f=Function('f',IntSort(),IntSort()) 
n=Int('n') 
c=Int('c') 
s=Solver() 
s.add(c>=0) 
s.add(f(0)==0) 
s.add(ForAll([n],Implies(n>=0, f(n+1)==f(n)+10/(n-c)))) 

La dernière équation est incompatible (depuis n=c rendrait indéterminée). Mais, Z3 ne peut pas détecter ce genre d'incohérences. Y a-t-il un moyen de détecter Z3 ou tout autre outil capable de le détecter?

Answer 1

Z3 ne vérifie pas la division par zéro car, comme l'a mentionné Patrick Trentin, la sémantique de division par zéro selon SMT-LIB est qu'elle renvoie une valeur inconnue.

Vous pouvez demander manuellement à Z3 de vérifier la division par zéro, pour vous assurer que vous ne dépendez jamais de la division par zéro. (. Ceci est important, par exemple, si vous modélisez une langue où la division par zéro a une sémantique différente de SMT-LIB)

Pour exemple, cela se présentera comme suit:

(declare-fun f (Int) Int) 

(declare-const c Int) 

(assert (>= c 0)) 

(assert (= (f 0) 0)) 

; check for division by zero 
(push) 
(declare-const n Int) 
(assert (>= n 0)) 

(assert (= (- n c) 0)) 
(check-sat) ; reports sat, meaning division by zero is possible 
(get-model) ; an example model where division by zero would occur 
(pop) 

;; Supposing the check had passed (returned unsat) instead, we could 
;; continue, safely knowing that division by zero could not happen in 
;; the following. 
(assert (forall ((n Int)) 
       (=> (>= n 0) 
        (= (f (+ n 1)) 
         (+ (f n) (/ 10 (- n c))))))) 

Answer 2

Pour autant que je peux dire, votre affirmation selon laquelle la dernière équation est incompatible ne correspond pas à la documentation de la norme SMT-LIB. La page Theories: Reals dit:

Depuis la logique SMT-LIB tous les symboles de fonction sont interprétées comme des fonctions au total, les termes de la forme (/ t 0)sont significatives dans tous les cas de reals. Cependant, la déclaration n'impose aucune contrainte sur leur valeur. Cela signifie en particulier que

• pour toute théorie de l'instance T et
• pour chaque valeur v (tel que défini dans: les valeurs d'attributs) et terme fermé t de type réel,

il y a un modèle de T qui satisfait (= v (/ t 0)).

De même, la page Theories: Ints dit:

Voir note dans la déclaration de la théorie reals sur les termes de la forme (/ t 0). La même observation s'applique ici aux termes de la forme (div t 0) et (mod t 0).

Par conséquent, il va de soi de croire qu'aucun SMT-LIB outil compatible ne jamais imprimer unsat pour la formule donnée.