SMT solver Yices

Résolu/Fermé
yices - 10 déc. 2012 à 00:35
 yices - 11 déc. 2012 à 17:49
Bonjour,

Je commence a me mordre les doigts, j'essaie d'apprendre à utiliser Yices, seulement je ne trouve aucune documentation réellement utile et clair c'est quand même dingue !!!

impossible de trouver un tuto ou autre qui explique par exemple se que la commande "assert" fait ! Incroyable je trouve ... bref pour cette commande j'ai compris.

mais pour tout le reste je galère un maximum...

par exemple pour faire un truc simple j'essaie de réaliser le programme qui va faire une suite tel que : f0 = 0 , f1 = f0 + 1 , f2 = f1 + 1 etc etc ...
qui serait un truc du style : (assert (= update f (x) (+ fx 1)))
enfin je sais pas trop ...

quelqu'un connait ce langage ? et par hasard avez vous un tuto bien fait que explique comment on programme et a quoi servent les différentes fonctions... pke jouer à deviner ça va bien pendant 1 semaine mais la j'en ai marre.


Merci d'avance

cordialement,

5 réponses

KX
Messages postés
16544
Date d'inscription
samedi 31 mai 2008
Statut
Modérateur
Dernière intervention
28 mai 2022
2 958
10 déc. 2012 à 17:38
Google connaît !
https://www.google.com/search?q=yices&gws_rd=ssl

Tu prends le premier lien et tu tombes sur le site officiel !
https://yices.csl.sri.com/

Et là, qu'est-ce qu'on a ? Documentation, exemples, wiki, FAQ, etc.

Après, c'est vrai, il fallait connaître Google...
1
KX
Messages postés
16544
Date d'inscription
samedi 31 mai 2008
Statut
Modérateur
Dernière intervention
28 mai 2022
2 958
Modifié par KX le 10/12/2012 à 20:02
Déjà je t'ai déplacé dans le forum Lisp, parce qu'au niveau de la syntaxe on en est très proche, et tu trouveras beaucoup plus de documentation là dessus pour construire tes fonctions.

Après, je ne connaissais pas Yices, et je me demande bien qui peut en avoir besoin, et par exemple pourquoi tu es arrivé à t'intéresser à ce "langage"...

C'est un assistant de preuve, tu définis des règles (les assert) et il se débrouille pour déterminer tout seul si ce que tu lui proposes est vrai ou faux.

Tu parlais de faire une suite f0 = 0 , f1 = f0 + 1 , f2 = f1 + 1 etc.
Cela s'écrit comme ceci :

(define f::(-> int int) ; f prend un entier et renvoie un entier
	(lambda (x::int); soit x le paramètre de la fonction
	(if	(= x 0) ; si x=0 
		0	; alors le résultat f0=0
		(+ 1 (f (- x 1))) ; sinon c'est f(x-1)+1
	)
	)
)

Après on pourrait lui demander par exemple de prouver que f(5)=5
(assert (= 5 (f 5)))
(check)

Dans ce cas il va répondre "sat" (satisfait). Tu peux tester d'autres valeurs, et on te répondras "unsat" si ce que tu affirmes est faux.

On pourrait également vouloir prouver que c'est vrai pour tout x :
(define x::int)
(assert (= x (f x)))
(check)

Malheureusement, sur un simple exemple, on voit déjà les limites de Yices, puisque l'on nous donne une erreur "feature not supported: recursive functions."
Le domaine d'application de ce programme doit donc être assez limité...
1
KX
Messages postés
16544
Date d'inscription
samedi 31 mai 2008
Statut
Modérateur
Dernière intervention
28 mai 2022
2 958
10 déc. 2012 à 20:39
Remarque : en trichant un peu, je peux définir f sans récursivité et utiliser Yices pour prouver que f(x)=x

(define f::(-> int int)
	(lambda (x::int)
		x
	)
)

(define x::int)
(assert (= x (f x)))
(check)
0
Heuuu , Merci lol

tu as trouvé ça par toi même ?

Je dois donc définitivement avoir un problème de compréhension en informatique.

Pour répondre à ta question je suis "intéressé" par Yices car je suis une formation dans une université aux Pays Bas qui s'intitule "Automated Reasonning" le but de ce cours est de résoudre des problèmes complexes grâce a des programmes en gros. et je dois utiliser Yices et Bddsolve selon le problème.

En tout cas merci beaucoup, je vais déjà partir sur ce que tu m'as dit pour faire dans un premier temps des petites résolutions simples.

cordialement,
0
KX
Messages postés
16544
Date d'inscription
samedi 31 mai 2008
Statut
Modérateur
Dernière intervention
28 mai 2022
2 958
11 déc. 2012 à 13:52
"tu as trouvé ça par toi même ?"
J'ai lu la documentation dont je t'ai donné les liens hier...

Ta fonction f est une adaptation de la fonction fact dans Limit on Recursive Function Expansion, ce passage est d'ailleurs intéressant pour comprendre les limites de la récursivité.
Mais en fait c'est une syntaxe proche de Lisp, excepté le typage fort qui ressemble à du Caml (deux langages que je connaissais déjà), la documentation est facile à suivre lorsqu'on a ces "pré-requis"

En ce qui concerne les tests assert/check, il y en avait partout dans les exemples, tu avais d'ailleurs dis avoir compris à quoi ils servaient.

Remarque : dans ces exemples, on voit qu'ils ne définissent pas vraiment la fonction comme je l'ai fait hier (à la Lisp). Ils préfèrent faire des déclarations de faits comme on pourrait en avoir dans des langages de programmation logique comme Prolog (un autre langage que j'ai déjà manipulé).

La manière la plus correcte de manipuler Yices serait donc de définir f en deux temps :

(define f::(-> int int))
(assert (= f (lambda (x::int) (if (= x 0) 0 (+ 1 (f (- x 1)))))))

Evidemment, cela ne réglera pas le problème de récursivité que ne supporte pas Yices...
0
Ok merci beaucoup pour ton aide,
Je n'ai aucun prérequis en langages de programmation (a part des notions en C), là est peut être le problème.
J'avais déjà lu cette documentation (fournit par le prof) mais c'est un peu du chinois pour moi.

ce matin j'ai eu un entretien avec le professeur qui m'a expliqué comment utiliser le "logiciel".

en fait il ne veut pas que je gère la récursivité via Yices mais plutôt que je créé un programme en C ou autre pour générer le code SMT.

Je lui ai demandé un exemple (le même que celui indiqué au dessus) et il m'a dit de faire quelque chose comme ca :
printf("
(benchmark test.smt
:extrafuns (
(A Int Int)
)
:formula (and
(= (A 0) 0)
");

for(i=0; i < 100 ; i++)
{
printf("(= (A i) (+ (A (i - 1)) 1);
}
))


Je ne suis pas sur de la syntaxe mais dans le principe c'est ca. Car il trouve comme toi que Yices c'est pas pratique pour ce genre de chose.

Un grand merci a toi de m'avoir aidé, et dsl pour mon manque de savoir ;)

Je peux clôturer le sujet
0
personne ne connait ?
0
quelqun en a t'il au moins deja entendu parlé ?
0

Vous n’avez pas trouvé la réponse que vous recherchez ?

Posez votre question
Mdr merci pour cette information et cette recherche ^^

seulement c'est cette documentation que j'estime comme : "qui sert a rien"

voila comment par exemple cette documentation va t'expliquer ce que fait la fonction update :

" Functions can be functionally updated using the update constructor. The syntax is:

(update f (pos_1 ... pos_n) new-val)
"
Si toi tu as compris comment ca fonctionne et ce que ca fait je t'en pris explique moi ^^

si tu en sais plus sur le langage SMT dis moi comment tu as appris stp

merci d'avoir pris du temps pour me répondre en tout cas
0