prédicat non-inliné

ada__model.mlw

ada__model_th.why

fl.mlw

_gnatprove_standard.mlw

_gnatprove_standard_th.why

Bonjour,

Ce problème est probablement similaire au précédent, il y a encore un prédicat non-inliné et on se retrouve dans la VC colibri juste avec la déclaration, sans définition. Le fichier principal est "fl.mlw", si on fait tourner why3, la VC généré pour colibri fait référence au prédicat "dynamic_property", mais ne contient pas sa définition.

Est-ce que vous auriez une solution pour ce prédicat aussi ? Pourquoi la solution du ticket #16 (closed) ne marche pas ici ?

Est-ce que vous avez une suggestion sur ce ticket ?

Je vais essayer d'enlever le maximum de transformation. J'ai l'impression que les autres solutions ne font que repousser à des problèmes futurs. Je le ferais jeudi. Sinon vendredi je reviendrais à des solutions plus simple.

Merci François.

Ok it works well, colibri now receive:

(define-fun dynamic_invariant ((temp___expr_67 Float32)
  (temp___is_init_63 Bool) (temp___skip_constant_64 Bool)
  (temp___do_toplevel_65 Bool)
  (temp___do_typ_inv_66 Bool)) Bool (=>
                                    (or (= temp___is_init_63 true)
                                    (fp.leq (fp.neg (fp #b0 #b11111110 #b11111111111111111111111)) (fp #b0 #b11111110 #b11111111111111111111111)))
                                    (fp.isFinite32 temp___expr_67)))

It was not hard to add the (par construct of smtlib v3 to dolmen. Just a problem with patterns but which was solved in dolmen master. Ça ma juste pris du temps de le voir et de backporter le master de dolmen dans colibri.

Je dois maintenant voir avec @marre à quelle moment on filtre les assertions polymorphes et qui gère les symboles polymorphesfl-with-par.smt2.

On gagne aussi l'accès aux datatypes, type énuméré, structure et type algébrique.

Au final les transformations faite en why3 ce limite à:

transformation "inline_trivial"
transformation "simplify_trivial_quantification"
transformation "simplify_formula"
transformation "eliminate_builtin"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "instantiate_predicate"

TODO: vérifier avec les functions recursive ce qui se passe, ou les éliminer.

NB: J'ai du cherry-pické f9c4697666aa77ed1c72dff215c91f4cb7a59b05

Ça a l'air de bien avancer, merci ! J'ai vu les changements dans la branche colibri de why3. D'après ce que j'ai compris, pour en profiter, je dois attendre des changements dans colibri lui-même, c'est bien ça ? Dans ce cas, tenez moi au courant !

En fait on peut pas utiliser tes derniers changements dans la branche colibri de why3 car tu utilises la function kdprintf qui est disponible depuis ocaml 4.08.0, mais nous sommes toujours sur 4.07.1 ... est-ce que tu peux éviter cet appel ?

Bien sûr. Merci d'avoir testé.

C'est corrigé.

Super, ça compile maintenant.

J'attends avec impatience les changements dans colibri (j'ai testé au cas où, mais avec le colibri actuel les résultats sont pires ... c'est attendu je pense)

Hello François,

do you have a time frame for the changes in colibri? Is this a big work that might take months?

Johannes

Non, Bruno était sur la finalisation et test. Ensuite je test depuis why3, mais tu pourra tester en parallèle de moi.

mentioned in merge request !8 (merged)

Fixed by !8 (merged)

closed