division par zero

div_zero.smt2

Bonjour,

J'ai mis en PJ une VC qui tente de prouver des bornes sur une division x / y. COLIBRI prouve la VC, mais cvc4 et z3 n'y arrivent pas (il faut décommenter 3 lignes au début du fichier pour que le fichier passe avec ces autres prouveurs). z3 et cvc4 prouvent le but immédiatement si on exclut la valeur zéro de y (décommenter ligne 199).

Pourquoi COLIBRI prouve le but ? Il me semble en effet qu'on ne pourra dire quoi que ce soit sur la valeur de la division si y est zéro, et si on tente de prouver que y est différent de zéro, COLIBRI n'y arrive pas (et je ne vois pas comment il pourrait).

Est-ce un bug ?

C'est possible, Gatel utilise une sémantique différente pour les fonctions partielles. Donc il y a un wrapper au dessus de la division (/ ) qui test si le dénominateur est 0 dans l'interface SMTLIB de COLIBRI. colibri_cdiv est computeur division. J'ai peut-être oublié le wrapper pour celui là.

NB: div de la smtlib est euclidean division, pas computer division.

Salut, tu as raison, la définition pour les symboles pour cvc4/z3 n'est pas correcte, je l'avais choisie parce qu'il n'y a pas de computer division en smtlib (je crois).

@marre pourra tu regarder ces différentes fonctions que j'avais ajouté?

En fait il y a bien un bug sur le wrapper de colibri_cdiv et une fois corrigé, et en commentant les "(assert (forall ..." pour ne pas faire unknown, il trouve une solution pour y = 0 en considérant ce cas comme une fonction non interprétée. Si par contre on impose y <> 0, ça devient unsat! Je commite la correction et François pourra rappatrier cette version

Bonne nouvelle, merci !

Bonjour @bobot , est-ce que nous pourrions avoir accès à cette nouvelle version?

mentioned in commit d679bb2f

Thanks for the heads up.

mentioned in merge request !16 (merged)

mentioned in commit 810fdd4c

closed with merge request !16 (merged)

Je confirme que le problème est corrigé, merci !

added unsoundness label