PS
как экспоненты, разумеется
Вы формулу для решателя покажите.
Size: a a a
2020 February 26
M
Это означает, что сама по себе задача, с которой имеет дело решатель — NP-полная. А алгоритмы для таких задач не масштабируются в общем случае. И еще отдельный вопрос — как представить в SMT-решателе тригонометрию :)
FO
Вы формулу для решателя покажите.
не обладаю такими знаниями.
PS
MaxGraey
Ну там в реальности эффективно поддерживается LIA. Для reals есть LRA, но кто-нибудь пробовал вообще ее использовать для супероптимизаторов? :)
PS
Вот здесь подробнее можно прочесть: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-solving-arithmetical-fragments
M
Да, там не просто это, но не невозможно
PS
Ну вот трансцендентные функции не поддерживаются. И даже не видно, как вызвать из того же Питона для Z3 sin/cos :)
PS
Конечно, работу с floats всегда можно организовать через битовые вектора. А функции — задать табличкой через If :)
M
PS
Да, это то, что не работает.
M
Насколько я знаю работают но ограниченно
PS
Ну что, пойду кодировать теорему Ферма для Z3. Я полон оптимизма! :)
M
Ну что, пойду кодировать теорему Ферма для Z3. Я полон оптимизма! :)
Или проблему дискретного логарифмирования в кольце вычетов для сверх больших модулей =)
PS
Если вернуться к исходному вопросу, то супероптимизаторы, повторюсь, не помогают, в общем случае, писать предметно-ориентированные правила (хотя в библиотеке правил в духе Mathematica нашлось бы многое и было бы хорошо это многое переиспользовать). Вообще, радоваться надо, что синтезом программ вообще что-то удается сделать! Но совсем залениться, увы, не получится :)
is
прочитал это полотно и не понял сути вопроса
Это про преобразование выражений чтобы написать что-то типо Mathematica, Matlab, WolframAlpha. Или автоматизировать то что мы делали на математике на бумажке в школе и универе. Меня интересовало какие теоретические выкладки по этому существуют. Всё-же тема близкая к синтаксическому анализу, поэтому спросил здесь.
is
в общем виде, это просто система переписывания? но они канонически недетерминистичны, что вряд ли на практике встречается. Пригодилась бы информация о том по какому правилу такие преобразования происходят
Спасибо за термин. "Система переписывания"
E
задаешь правила преобразований и запускаешь брудфорс
is
Тут действительно напрашиваются системы переписывания. И еще вопрос — какую из них считать за канон ;)
Короче говоря, гуглить полезно по "term rewriting" и "equational language".
Короче говоря, гуглить полезно по "term rewriting" и "equational language".
Ого, спасибо!