我的上下文仅包含以下数据类型声明:
EnumSort signal = ctx.mkEnumSort("signal", "red", "yellow", "green");
我想要的是获得上述声明的等效 SMTLIB 表示，如下所示:
(declare-datatypes () ((signal red yellow green)))
如何转换它？我尝试为此上下文创建一个求解器，然后执行 solver.toString() 但它不会打印任何内容，除非我在断言中使用此声明。
最佳答案
您只能从Solver(或Optimize)对象转换为smtlib。将上下文视为某种“管理器”，它独立于 smt-lib 或任何特定的表示形式。你是对的，你必须断言这个对象的一些东西，这是相当烦人的。
话虽如此，您的 signal 值在内部将存储为 Sort 对象:https://z3prover.github.io/api/html/classz3_1_1sort.html 。 (在你的例子中，无论这个类的 Java 等价物是什么。)理论上，人们可以仔细检查这个对象以找出它是一种数据类型，获取构造函数等，以手动进行翻译；但这将非常依赖于表示，并且从长远来看可能容易出错。
关于java - Z3 Java API toString() 不打印未使用的声明，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/56515223/