Z3 找到的模型中的集合的值

Question

我有一个类似的问题：How to print a Z3 Set object? 从中我无法弄清楚如何在模型中打印一组值。我有一种枚举排序（Java 代码）：

• EnumSort rSort = ctx.mkEnumSort(ctx.mkSymbol("res"), ctx.mkSymbol("res1"));

我从中创建了一个集合排序：

• SetSort rSet = ctx.mkSetSort(rSort)

通过使用这个集合排序，我创建了一个 Z3 常量 rID 并定义了一个简单的成员表达式：

• BoolExpr c1 = (BoolExpr)ctx.mkSetMembership(rSort.getConsts()[0], rID);

当 c1 可以满足时，我希望看到模型中 rID 的一个可能值。如果我尝试使用 const 解释（即 m.getConstInterp(e)，其中 e 是模型中的 FuncDecl），我会得到：“非零元函数和数组将 FunctionInterpretations 作为模型。使用 FuncInterp。”。

当我尝试使用 func 解释（即 m.getFuncInterp(e)）时，我得到“参数不是数组常量”。我在这里做错了吗？不能打印设置对象的值吗？或者，是否有更好的方法来表示可能包含来自排序的多个值的变量？

Answer 1

集合在内部由数组表示，而数组又具有模型的功能。 getConstInterp 失败，因为rID 是集合类型（内部数组类型）并且它会引发相应的异常。从示例中不清楚e 是什么，但这里有一个示例说明如何获取 rID 的 FuncInterp：

Context ctx = new Context(cfg);

EnumSort rSort = ctx.mkEnumSort(ctx.mkSymbol("res"), ctx.mkSymbol("res1"));
SetSort rSet = ctx.mkSetSort(rSort);
Expr rID = ctx.mkConst("rID", rSet);
BoolExpr c1 = (BoolExpr)ctx.mkSetMembership(rSort.getConsts()[0], rID);

Solver s = ctx.mkSolver();
s.add(c1);
Status status = s.check();
Model m = s.getModel();

System.out.println(status);
System.out.println("Model = " + m);

FuncInterp fi = m.getFuncInterp(rID.getFuncDecl());
System.out.println("fi="+ fi);

请注意，对getFuncInterp 的调用会获取常量 rID 的 FuncDecl，这可能是造成混淆的原因。