Как мне кажется, они немного ортогональны.
Классический Prolog/Datalog — это решение системы символьных рекурсивных уравнений путём нахождения наименьшей неподвижной точки. SAT/SMT — решение задачи SAT для (нерекурсивной) формулы алгоритмом DPLL + решателей конкретных теорий, типа арифметики.
Вот в Z3 эти две вещи пытаются скрестить, чтобы получить решатель рекурсивных символьных уравнений с поддержкой разных теорий.

Ну... да. А что и чему ортогонально?

нахождение lfp ортогонально решателям теорий )

но под датологом обычно понимают вполне конкретный метод нахождения lfp с magic-sets, bottom-up evaluation и вот этим вот всем

Так у них там в Z3 уже давно комбайн из разных полезностей :) Например, куда отнести их модуль оптимизации? Там используется maxSAT, ILP... :)

Вроде бы, классика это как раз использование BDD: https://people.csail.mit.edu/mcarbin/papers/aplas05.pdf

И это ещё и от данных для программы зависит... Думаю, без ML тут не обойтись! 😃

хз, конкретно про bdd в контексте даталога не слышал, но я не эксперт )

Я думаю, там и без ML есть чем заняться. Например, многие привычные ограничения в духе AllDifferent (Distinct) достаточно сложно выражаются на языке уравнений ILP.
Сейчас, как мне представляется, у SMT-решателей уровень, соответствующий оптимизирующим компиляторам 70-х. То есть шаг влево-вправо — и все перестает работать за разумное время. Единственное, что в старых компиляторах было похуже — там вообще при включении "мощной оптимизации", если помните, не гарантировалась работоспособность программы пользователя :)

интересно🧐

Неприлично длинное и безумно захватывающее для олдфагов интервью с Jonathan Blow: https://oxide.computer/blog/on-the-metal-9-jonathan-blow/

Эх, процессор Cell... Вот это был настоящий вызов для компиляторщиков!

Это не тот, который ставили в Playstation 3?

это он

Вот неплохое описание процесса разработки (именно 3 часть): http://www.blachford.info/computer/articles/CellProgramming3.html

Было множество исследовательских проектов на тему того, как всю эту возню с SPE автоматизировать.

If you’ve developed SSE and / or Altivec code in C and understand multithreading you’ll probably recognise almost everything here and be wondering what all the fuss is about.

правда выше написано что если ты перловод или питоновод - то ни хрена не поймешь

https://www.youtube.com/watch?v=ev28UgfoRR4 вот это интересней )

есть еще пдф пейпер но за пейволом