conversion int/real/float

real_repr.smt2

Bonjour !

COLIBRI répond avec une erreur de syntaxe sur le fichier en PJ:

$ colibri real_repr.smt2
(error "real_repr.smt2:syntax")
unknown
Steps : 41
Syntax error on real expression : fp_to_real(as(round(as(rna, rnd), float_from_real(as(rne, rnd), as(ColVar#2{rbox : (float_int, 0), mreal : [-9.22337203685478e+18 .. -1.0, 0.0, 1.0 .. 9.22337203685478e+18]}, real))), float_simple))

Or, cvc4 l'accepte. Quel est le problème ?

cvc4 prouve le fichier tel quel, mais il y a une variante dans le fichier (il faut juste ligne 288 et décommenter ligne 287) que cvc4 ne prouve pas. Est-ce que COLIBRI (après avoir corrigé ce que je suppose est juste un bug de parsing) peut prouver les deux ?

Merci d'avance

changed the description

Salut Johannes, après correction du pb de parsing et mise en commentaire des "(assert (forall ...", colibri dit sat pour la variante ou cvc4 dit unsat ! Si on ajoute la solution de colibri avec un assert de la valeur pour "i" alors cvc4 dit sat !! Ca ressemble à un bug de cvc4. Par contre pour la variante ou cvc4 ne répond pas, colibri dit unsat ! nreal_repr.smt2

Je commite et signale la correction à François !

Bruno, selon toi, la borne supérieure ne devrait pas être prouvée alors ? Colibri prouve la version avec la borne inférieure, mais pas la version avec le prédicat qui contient les deux bornes, logiquement le problème serait avec la borne supérieure ? Je regarderai plus en détail demain.

En tous cas, cvc4 donne des réponses contradictoires selon qu'on donne la valeur de "i" ou pas !

Et tu as raison, il faut aussi que je regarde de plus près pourquoi colibri dit unsat et non pas sat (bug !)

En fait le contre-exemple est sur la borne supérieure donc ça ne contredit pas le unsat pour la borne inférieure ?

Et cvc4 confirme le contre-exemple pour la borne supérieure quand on lui donne sa valeur !

merci pour ton analyse !

J'ai pu reproduire le problème avec cvc4, mais cela semble être corrigé dans des versions plus récentes (cvc5).

Tu as pu tester cvc5 sur la variante unsat de ton exemple ? Comment récupérer un binaire cvc5 ?

Je crois qu'il n'y a pas de nightly build pour l'instant. Je l'ai construit moi-même, j'ai testé sur la variante unsat, et il ne le prouve plus.

Donc pas mieux que colibri sur ton exemple :-)

En fait par "la version unsat" je voulais dire la version que cvc4 prouve incorrectement. Mais le résultat est le mếme, il me semble que cvc5 ne prouve plus rien sur cet exemple ...

Clairement pas mieux que colibri :-)

mentioned in commit 5a6a4987

closed with merge request !16 (merged)

mentioned in commit 810fdd4c

mentioned in merge request !16 (merged)

Je confirme que c'est corrigé dans la nouvelle version