История изменений
Исправление hateyoufeel, (текущая версия) :
Оно для доказательства теорем, но основано на лиспе. Локально можно запустить как-то так
z3 -smt2 -in, но(+ 2 2)там не вычисляется, мне некогда разбираться.
Оно не основано на лишпе. Оно использует s-expr как формат данных, но в основном потому что никто в здравом уме это всё руками не пишет. Код для Z3 генерится другим кодом почти всегда, и тут s-expr как нельзя кстати.
Хотя если у тебя лишп – это всё что использует s-expr, то тогда может быть.
Исправление hateyoufeel, :
Оно для доказательства теорем, но основано на лиспе. Локально можно запустить как-то так
z3 -smt2 -in, но(+ 2 2)там не вычисляется, мне некогда разбираться.
Оно не основано на лишпе. Оно использует s-expr как синтаксис, но в основном потому что никто в здравом уме это всё руками не пишет. Код для Z3 генерится другим кодом почти всегда, и тут s-expr как нельзя кстати.
Хотя если у тебя лишп – это всё что использует s-expr, то тогда может быть.
Исходная версия hateyoufeel, :
Оно для доказательства теорем, но основано на лиспе. Локально можно запустить как-то так
z3 -smt2 -in, но(+ 2 2)там не вычисляется, мне некогда разбираться.
Оно не основано на лишпе. Оно использует s-expr как синтаксис, но в основном потому что никто в здравом уме это всё руками не пишет. Код для Z3 генерится другим кодом почти всегда, и тут s-expr как нельзя кстати.