Fortress

Предлагается добавить в мэпперы возможность обработки операций, не являющихся базовыми для соотвествующего солвера. Для этого предлагается ввести дескрипторы операций, хранящие (1) текстовое представление кода операции и (2) определение функции на соответствующем языке (пустой для встроенных операций).

Для каждой использованной пользовательской операции в начало результирующего кода должно быть добавлено определение соответствующей функции.

P.S. Поскольку библиотека должна быть достаточно универсальной, должен быть предусмотрен мэппинг не только в текст (например, в формат smtlib), но и последовательность вызовов API. То есть есть мысль, что дескрипторы операций хранят не строки, а объекты (интерпретируемые каждым мэппером по своему).