Interplay between abs and div on integers

Would it be possible for COLIBRI to know about the fact that the absolute value and the division on integers can commute? that is, prove the code:

(set-logic ALL)
(set-info :smt-lib-version 2.6)
(declare-const x Int)
(declare-const y Int)
(assert
  (not (= (colibri_abs_int (colibri_cdiv x y))
          (colibri_cdiv (colibri_abs_int x) (colibri_abs_int y)))))
(check-sat)

C'est possible mais quelle est la généralité (intérêt) de ce propagateur ? (je suis en congé ce sera pour plus tard :-) )

Il me semble que ce but est sat, car on peut prendre 0 pour y. cdiv me semblerait indéfinie (ou pouvant prendre toute valeur) pour 0.

Mais l'utilisation de abs en lien avec / ou * m'a fait pensé à une extension de ce que Colibri2 fait pour les produits. C'était marrant comme exercice de vacances colibrics!17 (merged) et ça résoud le problème soumis avec / au lieu de cdiv et avec y < 0 colibrics!17 (diffs) mais il faut encore que j'étende un peu pour des exemples plus compliqué comme x^2 = y^2 => x * y > 0 => x = y.

François a raison, c'est sat pour y = 0 car cdiv est alors traité comme une fonction non-interprétée. Mais colibri part d'abord dans une branche (infinie) où y <> 0 et ne termine pas (sans info de commutation pour cdiv et abs).

D'autres corrections ont permis de trouver directement le sat pou y=0. je commite et ce sera dans la prochaine version.

mentioned in commit 696afbbc

mentioned in merge request !21 (merged)

Désolé Yannick, l'issue reste ouverte. Je vais regarder ça de plus près.

C'est enfin corrigé et sera intégré dans la prochaine version quand François aura le temps

mentioned in commit ef0c5838

mentioned in merge request !22 (merged)

mentioned in commit 6261a423

mentioned in commit 159140b5

closed with merge request !22 (merged)