Я использую Ocaml API Z3 версии 4.0 в течение последнего года или около того, в основном теорию битового вектора. Теперь мне нужно извлечь неподтвержденные ядра после выполнения Z3.solver_check, и, к сожалению, в версии 4 такой возможности нет. Я могу переписать, чтобы использовать предположения для обозначения каждого уравнения битового вектора в формуле, а затем получить ядро unsat, но это критическая часть кода, это может повлиять на общую производительность.
Есть ли способ получить ядро unsat, не делая предположений для версии 4? Долгосрочным решением, конечно же, является переход на последнюю версию, но если есть менее разрушительное решение, это было бы неплохо. Например, есть ли способ извлечь ядро unsat из доказательства unsat (возвращенного Z3.solver_get_proof)?
Спасибо!
