Z3 Java API toString () не печатает неиспользуемые объявления

Question

У меня есть контекст только со следующим объявлением типа данных:

EnumSort signal = ctx.mkEnumSort("signal", "red", "yellow", "green");

Я хочу получить эквивалентное представление SMTLIB вышеупомянутой декларации, что-то вроде следующего:

(declare-datatypes () ((signal red yellow green)))

Как мне конвертировать это? Я попытался создать решатель для этого контекста и затем выполнить solver.toString(), но он ничего не печатает, если я не использую это объявление в утверждении.

Answer 1

Вы можете конвертировать в smtlib только из объекта Solver (или Optimize). Думайте о контексте как о "менеджере", который не зависит от smt-lib или какого-либо конкретного представления. И вы правы, что вам придется что-то утверждать об этом объекте, что довольно раздражает.

Сказав это, внутренне ваше signal значение будет сохранено как Sort объект: https://z3prover.github.io/api/html/classz3_1_1sort.html. (В вашем случае, каким бы ни был Java-эквивалент этого класса.) Теоретически, тогда можно изучить этот объект, чтобы выяснить его тип данных, получить конструкторы и т. д., чтобы выполнить перевод вручную; но это будет в значительной степени зависеть от представления и, вероятно, будет подвержено ошибкам в долгосрочной перспективе.