Постоянным читателям хорошо известно, что я недолюбливаю java. Как только я начал чуть забывать, почему, она решила мне преподнести очередной сюрприз. Возьмем простенький класс

public class TestClass {
  public void foo(){ System.out.println(getBar()); }

  String getBar(){ return "bar"; }
}

И создадим от него наследника, переопределяя метод (довольно частый прием в тестах):

new TestClass(){
  String getBar() { return "baz"; }
}.foo();

Как думаете, что выведет foo?

В процессе поиска ответов на свои вопросы про cvc5 наткнулся на конспект по солверам. Это большой сборник примеров. Очень легко читается (и он на рунглише), местами написана чушь, но он неплох для погружения в область, если кому интересна эта тема. От души разбавлено байками.

Среди интересного можно увидеть ломание генератора случайных чисел, решение задачки из комикса xkcd, доказательство корректности всяких битовых хаков, факторизацию числа, решение задачи расцветки графа, чтобы занимать меньше регистров памяти, поиск коллизий в CRC32, минимизацию количества тестов.

Когда-то я в качестве калькулятора использовал bc. Но потом мне открыли глаза на очевидную истину: лучший калькулятор для командной строки — это питон.

Только недавно я узнал (а может вспомнил, просто уже давно забыл), что в интерпретаторе можно использовать _ для использования предыдущего результата:

>>> 9 + 10
19
>>> _ * 12
228
>>>

По совету Петра Георгиевича после z3 решил попробовать солвер cvc5.

У него есть API, который почти полностью повторяет синтаксис z3 — надо просто заменить импорт на from cvc5.pythonic import * и убрать z3.. (Ну или в стиле злодеев сделать import cvc5.pythonic as z3). Однако данные из модели выковыриваются немного по-другому: вместо

model.eval(el).as_long()

надо писать

model[el].ast.getIntegerValue()

С получением результатов еще связан один очень дебильный баг (и это не только у меня руки кривые).

Несмотря на то, что cvc5 побеждает на конкурсах, на моей машине работал он ощутимо медленнее. Если z3 решил судоку за 100мс примерно (и это с учетом запуска интерпретатора), то cvc5 пыхтел аж 9,5 секунд. Решение для магического квадрата 5x5 он не нашел. А для рюкзака нет аналога Optimization из z3.

За разумное время последние две проблемы я решить не смог. Вообще cvc5 показался существенно менее дружелюбным к пользователю с точки зрения документации и настройки по сравнению с z3. С учетом ниши, которую я описывал ранее, z3 выглядит более адекватно.

Оказывается, в баше есть встроенная команда command, которая изначально предназначена для запуска исполняемого файла, имя которого совпадает со какой-нибудь встроенной командой баша. Однако command -v можно использовать для проверки, существует ли исполняемый файл в принципе.

Более очевидный способ — использовать which, который еще и путь покажет, но внезапно, это не самый лучший вариант:

• which может отсутствовать в некоторых системах (особенно если система урезана под контейнер);
• which на некоторых системах может не устанавливать код ошибки;
• which может вызывать под капотом пакетный менеджер.

Чтобы отредактировать и выполнить длинную команду-колбасу с помощью редактора, можно воспользоваться Ctrl+X+E. Мне это пригодилось для длинных curl.

В редакторе может не быть включен мягкий перенос строк, тогда пользы будет немного. В nano это решается Esc+$ или добавлением set softwrap в ~/.nanorc.

Солвер — это инструмент, который позволяет задать систему неравенств и прочих условий, и на выходе дать решение, которое удовлетворяет этой системе. По сути, это декларативное программирование, когда нам вообще не важно, как это будет работать, главное — результат.

Я еще несколько месяцев назад наискосок просмотрел немного документации (раз и два), но к практике на основе репозитория в итоге перешёл только в поезде без интернета, поэтому первые два задания я подглядел. В остальном все решалось достаточно просто, для решения задач нужно совсем немного конструкций.

В целом сама парадигма довольно прикольная: надушить четкое ТЗ и дело в шляпе (а недостаточно душнишь — держи тривиальное решение с нулями). Какое-нибудь судоку решать с помощью него — самое то, фигачится минут за 10. Да и задача о рюкзаке была реализована мной за примерно такое же время — это не динпрог вертеть.

Однако чудес солвер тоже не открыл. Магический квадрат для 4x4 он находит мгновенно, а вот 5x5 уже не смог (я не стал ждать больше 10 минут). При этом проц и память были вообще не нагружены, т.е. по умолчанию параллелизации нет. И рюкзак для «плохих» входных данных (где стоит приближенно решать) тоже быстро не отработал.

В общем, для чего-то простого, когда может человек решить с ручкой и бумагой за обозримое время или программист тупым перебором — вполне достойный вариант. Но если известен хороший алгоритм и задача не одноразовая, то стоит посмотреть альтернативы.

Redis можно запустить как кластер для горизонтального масштабирования. И API вроде остается почти такое же — создал клиент чуть по-другому, и используй те же самые команды. Но есть нюанс — не все команды можно просто так взять и выполнить на кластере.

Пример — scan, которая позволяет искать ключи по паттерну. В документации ничего подозрительного не написано, в клиенте используем метод scan, тестируем локально, все зашибись. На стейдже будет ждать сюрприз — приложение упадает с ошибкой. Выясняется, что из-за шардинга нормально ключи не переберешь, и надо вместо scan писать метод, чтобы найти все ноды кластера, и для каждой из них уже выполнить scan.

Как мне кажется, это хороший пример нарушения принципа наименьшего удивления в API. Когда есть два клиента, отличающиеся только техническими деталями, ожидаешь, что их методы с одинаковыми названиями будут работать одинаково с точки зрения основной логики. А если нельзя сделать одинаковое поведение, то методы должны называться по-разному. Увы, реальность полна разочарований.

Забавный пост-сравнение степени подробности ошибок в разных языках. В целом совпадает с моими впечатлениями (на всем этом мне довелось что-нибудь написать). Elm тут немного перехвалили, хотя когда писал на нем, подсказка про возможные опечатки была весьма полезна. Про Rust тоже писал, что ошибки классные, когда компилятор угадал в чем ты ошибся, если нет, то все грустно.

Очень жалко, что автор не добавил в сравнение C++, но мой мем про это вы уже видели.

Занятная статья про проблемы производительности. В основном это выжимка из доклада одного из создателей BLAS и LAPACK (на которые полагается любимый многими numpy, если кто не в курсе). Сам доклад довольно неспешный, первые минут 15 там вообще идут биографические заметки, все основное в статье изложено неплохо.

TLDR: По CPU уже намасштабировались от души, сейчас основная проблема — передача данных. Лучшие компы работают на 5% мощности из-за того, что долго ждут на передаче данных. Раньше можно было сделать 1 вычисление с плавающей точкой на 1 перемещение, сейчас — уже 10-100. При этом очень мало внимания уделяется проектированию ПО так, чтобы оно учитывало особенности железа. Сейчас вполне нормально ситуация, когда асимптотически неэффективый алгоритм будет работать в разы быстрее оптимального просто за счет того, что ему нужно меньше перемещений данных.