在 Z3 中使用量词消除时的 SegFault答案

【问题标题】：SegFault when using quantifier elimination in Z3在 Z3 中使用量词消除时的 SegFault
【发布时间】：2013-02-18 11:50:46
【问题描述】：

我在 MacOS X 10.8 下使用 Z3 4.3.1（来自 master 分支）。我在以下示例中遇到分段错误：

(declare-const a Int)
(declare-const b Int)

(assert
  (exists ((k Int))
    (and 
     (= (- (* 2 k) a) 0)
     (= (- (* 2 k) b) 0)
    )
  )
)


(check-sat-using qe)

任何想法，关于如何解决这个问题？

【问题讨论】：

标签： z3

【解决方案1】：

我设法使用 OSX 和 Z3 4.3.1 重现了您描述的错误。此错误已修复，将在下一个正式版本中提供。同时，您可以使用夜间构建 OSX 或使用 unstable (working-in-progress) 分支构建 Z3。

可以在以下位置下载每晚构建版本：http://z3.codeplex.com/releases。我们必须点击“计划中的”链接。我写了一些说明here。

顺便说一句，如果我们想检查可满足性，我们应该在 qe 之后使用最终游戏策略（例如 smt），就像 Axel 发布的示例一样。如果我们想检查qe产生的结果，我们应该使用(apply qe)来代替。

【讨论】：

谢谢莱昂纳多。我通过在 src/muz_qe/qe_arith_plugin.cpp （第 527 行）的 expr 上添加缺少的 ref 来修复该错误： // as + bt + (a-1)(b-1)
即使使用“（然后 qe smt）”策略我也遇到了错误。

【解决方案2】：

在 Windows XP + Z3 4.3.0 下可以正常运行

(declare-const a Int)
(declare-const b Int)

(assert
  (exists ((k Int))
    (and 
     (= (- (* 2 k) a) 0)
     (= (- (* 2 k) b) 0)
    )
  )
)
(check-sat-using (then qe smt))
(get-model)

【讨论】：

谢谢，但我最初的策略是（然后是 simpligy solve-eqs qe smt）。我隔离了实际产生分段错误的那个（即“qe”）。
'(check-sat-using qe)' 也可以，但在我的安装中产生“未知”。
qe 是一个预处理步骤。如果我们想检查可满足性，我们应该在qe 之后使用结束游戏策略（例如smt），就像Axel 发布的示例一样。如果我们想检查qe产生的结果，我们应该使用(apply qe)来代替。