Z3 将 FuncInterp 设为 Null

Question

我正在使用 Z3 Java API 来解析 SMT 文件；当我调用 s.getModel() 时，其中 s 是求解器，我能够按如下方式正确打印模型：

(define-fun O_STUDENT () (Array Int STUDENT_TupleType)
  ((as const (Array Int STUDENT_TupleType))
  (STUDENT_TupleType _ID__12345 _NAME__Bourikas _DEPT_uNAME__Music 29)))
(define-fun O_DEPARTMENT () (Array Int DEPARTMENT_TupleType)
  ((as const (Array Int DEPARTMENT_TupleType))
  (DEPARTMENT_TupleType _DEPT_uNAME__Music _BUILDING__BUILDING_u5 50000.0)))

但是，当我尝试为 O_STUDENT 数组获取 FuncInterp 时，我得到了 null。我正在使用以下方法提取该值：

if (s.check() == Status.SATISFIABLE) {
            Model m = s.getModel();
            FuncDecl arrayDep = m.getConstDecls()[0];
            System.out.println(m.getFuncInterp(arrayDep));
        }

Answer 1

以防万一：数组有点特殊，因为有常量，但它们的模型是函数（参见 https://github.com/Z3Prover/z3/blob/master/src/api/java/Model.java#L88）。

模型可能不会包含所有变量的赋值 - 如果缺少一个变量，则意味着您可以自由选择您喜欢的任何值。如果您不喜欢，可以启用模型补全，Z3 会为您选择。

Z3 将 FuncInterp 设为 Null

Z3 Getting FuncInterp as Null

java

smt

z3