代码之家  ›  专栏  ›  技术社区  ›  jmite

Z3中的全面评估结果?

  •  2
  • jmite  · 技术社区  · 7 年前

    Z3通常返回根据一系列中间函数定义的模型。例如,常见的情况如下(请原谅我的语法错误):

    (define-const myArray (Array Bool Int) (_ as-array f))
    (define-fun f (x Bool) Int (f!10 (k!26 x)))
    

    ... 等等

    我希望能够得到一个结果,我可以在我的程序(调用Z3使用库绑定)和打印结果,并解析成一个我可以实际运行的函数。如果我可以将模型函数作为可以运行的单个直线程序,而不是根据彼此定义的多个函数,那么这会容易得多。

    这可能吗?如果有帮助的话,我只处理有限域函数。

    1 回复  |  直到 7 年前
        1
  •  1
  •   Nikolaj Bjorner    7 年前

    我们将在未来的版本中更新模型结构,尽可能压缩中间函数。然而,在某些情况下,这可能会导致指数开销,因为相同的辅助函数可以在多个上下文中重用。对于这些模型,扩展辅助功能没有意义。因此,如果用户想要对模型进行后期处理,他们仍将被迫处理此类功能。