java - 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))时，我得到“Argument was not an array constant”。我在这里做错了什么吗？是否可以打印 set 对象的值？或者，是否有更好的方法来表示可能包含排序中的多个值的变量？

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，这可能是混淆的根源。