Z3发现的模型中集合的java值

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的一个可能值。如果我尝试使用常量解释（例如，m.GetContinterp（e），其中e是模型中的FuncDecl），我会得到：“非零算术函数和数组的函数解释是一个模型。使用FuncInterp。”

当我尝试func解释（即m.getFuncInterp（e））时，我得到“参数不是数组常量”。我做错什么了吗？难道不能打印set object的值吗？或者，有没有更好的方法来表示可能包含排序中多个值的变量

Answer 1

集合在内部由数组表示，数组又具有作为模型的功能。GetContinterp失败，因为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，这可能是造成混淆的原因