SMT solver Yices

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)

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,

"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...

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