Z3 Java API 定义一个函数 [英] Z3 Java API defining a function

问题描述

我需要你的帮助，用 Z3 Java API 定义一个函数.我尝试解决这样的问题(在 z3.exe 进程中工作正常):

I need your help defining a function with the Z3 Java API. I try to solve something like this (which is working fine with the z3.exe process):

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Bool)

(define-fun max2 ((x Real) (y Real)) Real (ite (<= x y) y x))

(assert (and (>= a 0.0) (<= a 100.0)))
(assert (or (= (max2 (+ 100.0 (* (- 1.0) a)) (/ 1.0 1000.0)) 0.0) c (not (= b 0.0))))

(check-sat-using (then simplify bit-blast qfnra))
(get-model)

这个 smt 文件的结果是:

The result of this smt-file is:

sat
(model
  (define-fun a () Real
    1.0)
  (define-fun c () Bool
    false)
  (define-fun b () Real
    1.0)
)

现在的问题是:没有选择，用java API定义一个函数.在另一篇文章中(相当于 Z3 API 中的define-fun)，我注意到在 java API 中使用了以下语句:

The problem now is: There is no option, to define a function with the java API. In another post (Equivalent of define-fun in Z3 API), i noticed to use the following statement in the java API:

(declare-fun max2 (Real Real) Real)
(assert (forall ((y Real) (x Real)) (= (max2 y x) (ite (<= x y) y x))))

所以我在我的 smt 文件中替换了 (define-fun max2 ((x Real) (y Real)) Real (ite (<= xy) yx)) 并启动了 z3.exe进程再次.结果如下:

So i replaced (define-fun max2 ((x Real) (y Real)) Real (ite (<= x y) y x)) in my smt-file and started the z3.exe process again. The result was the following:

unknown
(model
  (define-fun b () Real
    0.0)
)

所以，如你所见，不再有可满足的结果.用 java 翻译，将得到相同的结果 UNKNOWN.

So, as you can see, there is no satisfiable result any more. Translating this in java, will get the same result UNKNOWN.

任何想法，我能做什么?

Any ideas, what i can do?

推荐答案

没有等效的函数定义，因为它们不是必需的，就像define-fun 宏一样.在 API 中要做的等效的事情是为函数构建一个表达式，然后对于函数的每个应用程序，只需将参数值替换为输入值，例如，使用 Expr.Substitute.

There is no equivalent to function definitions because they aren't necessary, just like the define-fun macro. The equivalent thing to do in the API is to build an expression for the function and then for every application of the function, just substitute the argument values for the input values, e.g., by using Expr.Substitute.

就像您引用的帖子中提到的 Leo 一样，可以为此目的使用量词，但是求解器通常会放弃并返回 unknown，因为它认为公式太难求解.我们可以通过使用宏查找器(参见引用的帖子)来解决这个问题，它可以准确识别这种宏.

Like Leo mentioned in the post you cited, the use of quantifiers is possible for this purpose, but the solver will often just give up and return unknown because it thinks the formula is too hard to solve. We can get around that by using the macro finder (see cited post), which will recognize exactly this kind of macro.

这篇关于Z3 Java API 定义一个函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！