Variables symboliques dans z3

Question

Existe-t-il un moyen de faire en sorte que le solveur z3 émette des solutions «symboliques»? Par exemple, pour l'équation:

1 + x = c

la solution est x = c-1, mais émet toujours z3 un modèle spécifique, comme [c = 0, x = -1]. Comment "définir" c comme une variable symbolique?

Answer 1

Malheureusement, Z3 n'expose pas ce type de fonctionnalité. Bien que nous utilisions des solveurs en interne, ils ne sont pas exposés dans l'API. Dans les versions futures, nous voulons exposer les composants internes tels que: solveur, procédures bases Grobner, etc. Dans la version actuelle, nous avons une tactique appelée solve-eqs (voir http://rise4fun.com/Z3Py/tutorial/strategies). Il élimine les variables en utilisant une généralisation de l'élimination gaussienne. Cependant, il s'agit d'une étape de prétraitement et vous n'avez aucun contrôle sur les variables éliminées.