Z3 - try-for 导致分段错误
Z3 - try-for causes segmentation faults
我正在使用 Java-API 在 Ubuntu Linux 14.04 上与 Z3 通信。关于Z3，我使用在github（今天编译）上找到的master-branch的当前版本。
我要检查可满足性的公式的基本结构如下：
(and (exists ((x1 S1) ... (xn Sn)) p(x1,...,xn))
(not (exists ((x1 S1) ... (xm Sm)) q(x1,...,xm))))
其中 Si 可以是 Bool、枚举 Sort、Real 或 Integer
p 和 q 是包含以下内容的公式：
- 数值和常数之和之间的不等式
- 枚举值和常量之间的等式
- 布尔值和常量。
- 它们的组合（连词、析取、否定）
但是，公式可以包含整数或实数，但不能同时包含两者。
为了检查可满足性，我使用策略创建了一个求解器：
(or-else (try-for smt x) (then qe smt))
原因是有些公式很简单，因此可以快速检查并且不需要量词消除，但是普通的 smt 求解器对于一些没有量词消除的公式会失败。由于 smt 求解器失败可能需要很长时间，因此我使用超时 x 的 try-for。
现在的问题是，根据 x 的值，此策略会在数百次可满足性检查（实际数量不同）后产生分段错误。我还观察到较大的值往往更安全，但这取决于公式 p 和 q 的复杂性。目前，我使用的值介于 70 到 200 之间。
由于重现问题所需的可满足性检查的实际数量各不相同，因此我无法给出触发问题的具体最小示例。
我的问题是：通常应该避免低超时值还是有办法解决这个问题？ IE。是否可以使用 70 毫秒的超时并在之后尝试量词消除？
另一个问题：考虑到我在大多数情况下不需要模型，是否有更有效的策略来解决我描述的那种问题？
或者是否有必要提供更多细节？
编辑：
我刚刚意识到，与 try-for 的组合在某些情况下实际上会产生错误的结果，但只有在一定数量的可满足性检查之后，无论 x 的实际值如何（Z3 @ rise4fun 产生正确的结果）。使用此策略的求解器将不可满足的公式视为可满足的，而策略 (then qe smt) 产生了正确的结果。
Link to check of formula producing the correct result
如评论中所述，由于 Z3 团队 (closed bug report) 的错误修复，该问题现已解决。此错误修复已集成到下一个发布版本 4.4.1 中，该版本在撰写本文时是最新的。
我正在使用 Java-API 在 Ubuntu Linux 14.04 上与 Z3 通信。关于Z3，我使用在github（今天编译）上找到的master-branch的当前版本。
我要检查可满足性的公式的基本结构如下：
(and (exists ((x1 S1) ... (xn Sn)) p(x1,...,xn))
(not (exists ((x1 S1) ... (xm Sm)) q(x1,...,xm))))
其中 Si 可以是 Bool、枚举 Sort、Real 或 Integer p 和 q 是包含以下内容的公式：
- 数值和常数之和之间的不等式
- 枚举值和常量之间的等式
- 布尔值和常量。
- 它们的组合（连词、析取、否定）
但是，公式可以包含整数或实数，但不能同时包含两者。
为了检查可满足性，我使用策略创建了一个求解器：
(or-else (try-for smt x) (then qe smt))
原因是有些公式很简单，因此可以快速检查并且不需要量词消除，但是普通的 smt 求解器对于一些没有量词消除的公式会失败。由于 smt 求解器失败可能需要很长时间，因此我使用超时 x 的 try-for。
现在的问题是，根据 x 的值，此策略会在数百次可满足性检查（实际数量不同）后产生分段错误。我还观察到较大的值往往更安全，但这取决于公式 p 和 q 的复杂性。目前，我使用的值介于 70 到 200 之间。
由于重现问题所需的可满足性检查的实际数量各不相同，因此我无法给出触发问题的具体最小示例。
我的问题是：通常应该避免低超时值还是有办法解决这个问题？ IE。是否可以使用 70 毫秒的超时并在之后尝试量词消除？
另一个问题：考虑到我在大多数情况下不需要模型，是否有更有效的策略来解决我描述的那种问题？ 或者是否有必要提供更多细节？
编辑：
我刚刚意识到，与 try-for 的组合在某些情况下实际上会产生错误的结果，但只有在一定数量的可满足性检查之后，无论 x 的实际值如何（Z3 @ rise4fun 产生正确的结果）。使用此策略的求解器将不可满足的公式视为可满足的，而策略 (then qe smt) 产生了正确的结果。
Link to check of formula producing the correct result
如评论中所述，由于 Z3 团队 (closed bug report) 的错误修复，该问题现已解决。此错误修复已集成到下一个发布版本 4.4.1 中，该版本在撰写本文时是最新的。