http://www.smtlib.org/ a défini un format de fichier pour décrire des formules de satisfiabilité modulo une théorie. Cela paraît compliqué, mais il s'agit tout bonnement de formules logiques dont les atomes sont pris dans une théorie, par exemple les inégalités linéaires, et dont il s'agit de savoir si elles sont satisfiables.

Question : pour écrire des formules sur les inégalités linéaires, ont-ils choisi un format lisible, comme l'on pourrait par exemple écrire dans Mathematica ? Par exemple, x <= 4 && x + y <= 7 && y >= 1...

Que non. Le format est compliqué, sa spécification inutilement biscornue, tellement qu'apparemment la plupart des outils ne mettent pas en œuvre un lecteur généraliste pour le format de fichier, mais un bricolage ad-hoc suffisant pour passer les exemples fournis...

Pourquoi faire simple quand on peut faire compliqué ?