0

我有一个用 Java 实现的工具。我们已经使用Java JNI. 我正在使用 Z3 4.1 版

鉴于这种情况，我做了以下实验 -

实验 1 -

  1. 我在求解器中断言了一些约束。
  2. 我检查结果是坐还是不坐。

实验 2 -

  1. 我在求解器中断言相同约束的子集。
  2. Z3_solver_push()我使用API推送求解器的上下文。
  3. 我断言剩余的约束。
  4. 我检查结果是坐还是不坐。

我做实验2的原因是需要回溯。

现在在实验 1 中，我得到查询所需的时间始终小于 5 秒。到目前为止，我已经检查了大约 20-30 次。有时甚至不到2秒。

现在通过实验 2，注意到约束完全相同的事实，我得到的查询时间有时是 5 秒，有时是 10 秒，有时是 50 秒。我还看到查询是“超时”，超时为 60 秒。

为了消除一些疑虑，我从命令行执行了相同的实验。通过实验一，我发现查询时间总是在 2.3 - 2.7 秒之间。然而，对于实验 2，（我push手动放置了一条语句），时间变得可变，如前所述。它在 10-60 秒之间变化。

我想知道pushing上下文是否会导致查询出现这种变化？理想情况下不应该。但是有机会吗？

我们如何才能避免这种随机性并获得类似于没有push声明的稳定行为？

更新

我添加了示例约束，我想找出使用​​哪种策略。请注意，它无法重现实验中提到的问题。但是，我们使用多个此类约束，如下所示，可以重现问题 -

(set-option :produce-models true) ; enable model generation
(set-option :print-success false)
(declare-const goal1 Int)
(declare-const goal2 Int)
(declare-const goal3 Int)
(declare-const kmax Int)
(declare-const ordA0_A0 Bool)
(declare-const ordA0_B0 Bool)
(declare-const ordB0_B0 Bool)
(declare-const ordB0_A0 Bool)
(declare-const stA0 Int)
(declare-const stB0 Int)
(declare-const stPA_0 Int)
(declare-const enPA_0 Int)
(declare-const stPB_0 Int)
(declare-const enPB_0 Int)
(declare-const kstA0 Int)
(declare-const kyA_0 Int)
(declare-const kstB0 Int)
(declare-const kyB_0 Int)
(declare-const resA_0 Int)
(declare-const resB_0 Int)

(assert (if (>= stPA_0 enPA_0) (= ordA0_A0 true) (= ordA0_A0 false)))
(assert (if (>= stPB_0 enPB_0) (= ordB0_B0 true) (= ordB0_B0 false)))
(assert (if (>= stPA_0 enPB_0) (= ordB0_A0 true) (= ordB0_A0 false)))
(assert (if (>= stPB_0 enPA_0) (= ordA0_B0 true) (= ordA0_B0 false)))

(assert (and (>= stA0 0) (<= stA0 goal2)))
(assert (and (>= stB0 0) (<= stB0 goal2)))
(assert (or (= stA0 0) (= stB0 0)))
(assert (>= stB0 (+ stA0 1)))
(assert (=> (and (= resA_0 resB_0) (= ordA0_A0 false) (= ordB0_B0 false)) (or (= ordA0_B0 true) (= ordB0_A0 true))))
(assert (=> (and (= resA_0 resB_0) (or (= ordA0_A0 true) (= ordB0_B0 true))) (and (= ordA0_B0 true) (= ordB0_A0 true))))

(assert (and (>= resA_0 0) (< resA_0 goal3)))
(assert (and (>= resB_0 0) (< resB_0 goal3)))

(assert (=> (= resA_0 resB_0) (or (= ordA0_A0 false) (= ordB0_B0 false))))

(assert (= stPA_0 (- stA0 (* goal1 kstA0))))
(assert (= enPA_0 (- (+ stA0 1) (* goal1 kyA_0))))
(assert (= stPB_0 (- stB0 (* goal1 kstB0))))
(assert (= enPB_0 (- (+ stB0 2) (* goal1 kyB_0))))
(assert (= kstA0 (div stA0 goal1)))
(assert (= kyA_0 (div (+ stA0 1) goal1)))
(assert (= kstB0 (div stB0 goal1)))
(assert (= kyB_0 (div (+ stB0 2) goal1)))
(assert (= goal2 (+ stB0 1)))
(assert (>= goal1 1))
(assert (<= goal2 6))
(assert (= kmax (div 6 goal1)))
(assert (<= goal2 6))
(assert (<= goal3 5))
(assert (= goal1 3))

(check-sat)
(get-model)
4

1 回答 1

3

Z3 是求解器的集合。默认求解器对象是求解器组合。并非投资组合中的每个求解器都是增量的。一旦我们使用Z3_solver_push()，它将使用通用增量求解器。这种通用求解器的效率可能远低于非增量求解器。即使在使用时，您也可以强制 Z3 使用非增量求解器 Z3_solver_push()。但是，Z3 将对每个 查询从头开始check，并且不会重用以前check查询的任何工作。

创建非增量求解器的主要 API 是Z3_mk_solver_from_tactic.

于 2013-05-01T00:16:41.587 回答