Z3 Java API toString() 不打印未使用的声明

Question

我有一个只有以下数据类型声明的上下文：

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

我想要的是获得上述声明的等效 SMTLIB 表示，如下所示：

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

如何转换？我尝试为此上下文创建一个求解器，然后执行solver.toString()，但除非我在断言中使用此声明，否则它不会打印任何内容。

Answer 1

您只能从Solver（或Optimize）对象转换为smtlib。将上下文视为某种“管理器”，它独立于 smt-lib 或任何特定表示。你是对的，你必须对这个对象进行断言，这很烦人。

话虽如此，在内部您的signal 值将存储为Sort 对象：https://z3prover.github.io/api/html/classz3_1_1sort.html。 （在你的情况下，无论这个类的 Java 等价物是什么。）理论上，可以仔细检查这个对象以确定它是一种数据类型，获取构造函数等，然后手动进行翻译；但从长远来看，这将非常依赖于表示，并且可能容易出错。