Existe-t-il de bons mécanismes dans Z3 pour faire abstraction des assertions ? Je veux créer une "fonction" qui prend des paramètres et fait des assertions sur ces paramètres, éventuellement avec des définitions de "variables locales".
Imaginons que je dispose d'un String et je veux affirmer qu'il représente un nombre décimal compris entre 13 et 24. Je pourrais écrire une combinaison d'assertions d'expressions régulières sur la chaîne et la combiner avec une assertion de type str.to.int l'affirmation de la portée. Je peux le faire directement, mais si j'ai des dizaines de variables de ce type pour lesquelles je veux faire l'assertion, cela devient répétitif. Je peux utiliser une API de langage externe, ou peut-être définir une macro/fonction renvoyant un booléen dans Z3 et affirmer que c'est vrai, mais cela semble un peu indirect. Qu'est-ce qui est idiomatique ici ? Je veux que ce soit aussi facile à résoudre pour Z3 que d'écrire les assertions à la main.
