Я нахожусь в ситуации, когда у меня есть куча запросов Z3 (bitvector) уже в формате txt. Есть ли способ создать решатель и контекст через некоторый API, читая в этих запросах? Я больше программист на Java, поэтому я бы предпочел какой-то Java API, но с и python тоже должно быть все в порядке.
Очень ценится! Спасибо!