通过 Java 实现在 Z3 中定义一个函数？答案

【问题标题】：Defining a function in Z3 by its Java implementation?通过 Java 实现在 Z3 中定义一个函数？
【发布时间】：2016-05-22 13:38:03
【问题描述】：

这就是我想要做的。

假设我想在类似于下面的表达式中使用 Z3（及其 Java 绑定）查找 op 的值：

((exists (op Int)) (= (foo op) 2)

所以我想在 op 变量上调用函数 foo 并检查函数将返回 2 的 op 值。我想在 Java 中定义一个函数 foo 并认为 Z3 存在一种方法访问这些函数定义。我想这样做是因为这些函数实际上是在 HashMap 中查找，这在 Java 中很容易实现。

由于我通常是 SMT 求解器的初学者，因此我可能想做一些无法完成的事情。因此，我愿意接受有关该主题的所有建议。

提前感谢您的时间和回答！

【问题讨论】：

标签： z3 smt

【解决方案1】：

这将是非常好的，但目前 Z3 不能使用来自其他语言/API 的函数定义。但是对于查找表来说应该很容易，因为它们可以很容易地编码为 if-then-else 级联，例如如下：

;; define foo
(define-fun foo ((x Int)) Int
    (ite (= x 1) 42
    (ite (= x 2) 43
    ;; ...
                 78)))

;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply skip)

生产

(goal
  (exists ((op Int)) (= (ite (= op 1) 42 (ite (= op 2) 43 78)) 43))
  :precision precise :depth 0)
)

（也很快解决了。）

通过 API 执行此操作的最简单方法是使用函数声明设置问题，然后通过 macro-finder 策略识别的通用量词提供宏定义：

;; declare foo
(declare-fun foo ((Int)) Int)

;; define foo
(assert (forall ((x Int)) (= (foo x)
    (ite (= x 1) 42
    (ite (= x 2) 43
    ;; ...
                 78)))))

;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply macro-finder) ;; replaces foo with it's definition

为了让宏查找器获取函数定义，量词必须具有格式

(forall ((x ...)) (= (foo x) (... definition ...))

【讨论】：

感谢您抽出宝贵时间回答问题。我也想到了这个解决方案，但我认为它的开销太大了......无论如何我必须这样做。
嘿，我已经开始使用 Java 绑定来实现它，但遇到了一个问题。我想使用您指定的示例中的宏，但是我似乎无法找到一种方法来定义一个函数（宏），其主体使用 API 将参数映射到返回值，因为 mkFuncDecl 提供了一个声明函数但不定义其主体的方法。
好点！我认为最简单的方法是应用宏查找器策略。我会将其添加到示例中。