ненасыщенные ядра из API

Question

Я знаю, что Java API parseSMTLIB2File игнорирует определенные команды в файле SMT2. Однако есть ли способ обойти это? Я генерирую файлы smt2 и использую parseSMTLIB2File и solver.check () для анализа и устранения ограничений.

Теперь я бы хотел использовать ядра unsat из решателя для некоторых вычислений. Я знаю, что, вероятно, могу сделать это, используя стандартный ввод и вывод ( здесь ). Однако это будет очень неэффективно для запуска алгоритмов. Кроме того, также не является идеальным изменение всей кодовой базы для переключения каждого поколения ограничений через API Java Z3.

Поскольку собственный интерфейс C ++ хорошо обрабатывает параметры и (отслеживаемые) утверждения. Следовательно, есть ли способ обойти это? Как я могу сделать это программно и эффективно?

Другие API C ++ / C / Python parseSMTLIB2File выполняют те же функции, что и Java, или они могут читать другие вещи.

Answer 1

есть ли способ обойти это?

Нет. parseSMTLIB2File не является полным интерфейсом для решателя и не предназначен для этого. Единственные варианты - перейти к полному интерфейсу API или к полнотекстовому интерфейсу, создав файлы .smt2 и передав их в Z3. Последнее может быть сделано через каналы вместо реальных файлов, и многие пользователи довольны производительностью этого.