История изменений

Оно для доказательства теорем, но основано на лиспе. Локально можно запустить как-то такz3 -smt2 -in, но(+ 2 2)там не вычисляется, мне некогда разбираться.

Оно не основано на лишпе. Оно использует s-expr как формат данных, но в основном потому что никто в здравом уме это всё руками не пишет. Код для Z3 генерится другим кодом почти всегда, и тут s-expr как нельзя кстати.

Хотя если у тебя лишп – это всё что использует s-expr, то тогда может быть.

Оно для доказательства теорем, но основано на лиспе. Локально можно запустить как-то такz3 -smt2 -in, но(+ 2 2)там не вычисляется, мне некогда разбираться.

Оно не основано на лишпе. Оно использует s-expr как синтаксис, но в основном потому что никто в здравом уме это всё руками не пишет. Код для Z3 генерится другим кодом почти всегда, и тут s-expr как нельзя кстати.

Хотя если у тебя лишп – это всё что использует s-expr, то тогда может быть.

Оно для доказательства теорем, но основано на лиспе. Локально можно запустить как-то такz3 -smt2 -in, но(+ 2 2)там не вычисляется, мне некогда разбираться.

Оно не основано на лишпе. Оно использует s-expr как синтаксис, но в основном потому что никто в здравом уме это всё руками не пишет. Код для Z3 генерится другим кодом почти всегда, и тут s-expr как нельзя кстати.