z3 4.3.2未能找到Why3生成（可满足）目标的模型

我试图使用Why3的Z3后端为了检索模型，然后可以用于派生测试案例展示程序中的错误。但是，对于任何Why3目标而言，Z3 4.3.2版似乎无法回答sat。它看起来像Why3使用的某些公理化定义混淆了Z3。例如，下面的例子（其是什么Why3产生一小部分）z3 4.3.2未能找到Why3生成（可满足）目标的模型

(declare-fun abs1 (Int) Int) 

;; abs_def 
    (assert 
    (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x))))) 

(check-sat)

导致timeout使用下面的命令行：

z3 -smt2 model.partial=true file.smt2 -T:10

在另一方面，改变定义

(declare-fun abs1 (Int) Int) 

;; abs_def 
    (assert 
    (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x)))) 

    (assert 
    (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))

会得到我的模型（这看起来很合理）

(model 
    (define-fun abs1 ((x!1 Int)) Int 
    (ite (>= x!1 0) x!1 (* (- 1) x!1))) 
)

但如果我尝试添加下一个公理存在于原始的Why3文件，即

;; Abs_pos 
(assert (forall ((x Int)) (<= 0 (abs1 x))))

再次Z3回答timeout。

在Z3的配置中是否存在缺少的东西？此外，在以前的Why3版本中，有一个选项MODEL_ON_TIMEOUT，允许在这种情况下检索模型。尽管无法保证这是真正的模型，因为Z3无法完成检查，实际上，这些模型通常包含我需要的所有信息。但是，我在4.3.2中没有找到类似的选项。它还存在吗？

更新最后公理Abs_pos是错的（我玩弄了一下与Why3的输出在这里发帖之前，结束了粘贴问题的版本不正确）。这现在已经修复。

来源

2015-02-23 Virgile

附加公理

（断言（未（forall的（（X智力））（< = 0（ABS1 X）））））

使得问题不可满足，因为ABS1总是返回一个非负整数，并且在附加公理中，对于某个x，您需要存在abs1的负结果。网络版Z3返回的结果不如预期，请参阅here。

来源

2015-02-24 09:43:20

糟糕，我意识到我粘贴了我试图玩弄Why3的输出的错误部分。 Why3提供的真正公理当然是（assert（forall（（x Int））（<= 0（abs1 x））））'。我会相应地编辑我的问题，对于噪音感到抱歉。 – Virgile 2015-02-24 09:51:44

z3 4.3.2未能找到Why3生成（可满足）目标的模型

回答

相关问题