java - Z3 Java API - 忽略像最大函数这样的表达式

Question

上次我问如何在 Z3 Java API 中定义函数。原因是在 Java API 中没有定义函数的命令。答案是用函数的参数值替换输入值 ( Z3 Java API defining a function )。

示例(我需要的):

<强>1。没有 API(普通 smt 文件)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(define-fun max2 ((x Int) (y Int)) Int (ite (<= x y) y x))

(assert (< (max2 a b) c))
(assert (>= (max2 a b) c))

(check-sat)

我现在做的是这样的:

<强>2。使用 Java API

Context ctx = new Context();

ArithExpr a = (ArithExpr) ctx.mkConst(ctx.mkSymbol("a"), ctx.getIntSort());
ArithExpr b = (ArithExpr) ctx.mkConst(ctx.mkSymbol("b"), ctx.getIntSort());
ArithExpr c = (ArithExpr) ctx.mkConst(ctx.mkSymbol("c"), ctx.getIntSort());

ArithExpr max2 = (ArithExpr) ctx.mkITE(ctx.mkLe(a, b), b, a);
BoolExpr one = (BoolExpr) ctx.mkLt(max2, c);
BoolExpr two = (BoolExpr) ctx.mkGe(max2, c);

我想知道，这是否有所作为？

我假设 smt-file (1) 中的 max2-function 是正确的，不必重新求解。但是如果我按照上面的java代码(2)那样做，求解器必须求解max2函数的表达式ctx.mkITE(ctx.mkLe(a, b), b, a) 每一次。还是我完全错了，不可能忽略 max2 函数的表达式？

有没有人有想法？

Answer 1

define-fun 构造的行为类似于宏，因此所有出现的 max2 都将替换为函数定义。或者，我们可以使用量词和宏查找器(参见例如 Equivalent of define-fun in Z3 API )，或者我们可以自己替换所有出现的函数。

一般来说，不可能“忽略”任何东西，Z3 也不会尝试在另一个函数之前“解决”一个函数；它只知道同一个子表达式可以出现多次的问题(并且它具有散列运算，所以它知道相等的子表达式)。如果您知道可以在不了解函数语义的情况下解决问题，那么您可以用一个新变量替换它来表示某些特定参数的返回值，这可能会大大解决问题更快。