Я использую Z3 и расширенный синтаксис SMT-LIB2 для решения моих клаксонов. Глава рога должна быть неинтерпретируемым предикатом;но мне интересно, как я могу переписать следующее предложение как предложение рога.
(declare-rel p(Int))
(declare-val x Int)
(rule (=> p(0) false)
Невозможно переписать его как (rule ((not p(0)))), поскольку отрицание неинтерпретированных предикатов не допускается.