如果注释中间 `(check-sat)` 调用，为什么查询结果会发生变化？

【问题标题】：Why does a query result changes if comment an intermediate `(check-sat)` call?如果注释中间 `(check-sat)` 调用，为什么查询结果会发生变化？
【发布时间】：2012-04-30 14:54:27
【问题描述】：

在调试 UNSAT 查询时，我注意到查询状态有一个有趣的差异。查询结构为：

assert(...)
(push)      ; commenting any of these two calls
(check-sat) ; makes the whole query UNSAT, otherwise it is SAT

assert(...)
(check-sat) ; SAT or UNSAT depending on existence of previous call
(exit)

查询中没有pop 调用。触发此行为的查询是here。

想法为什么？

注意：我实际上并不需要增量，它仅用于调试目的。 Z3版本是3.2。

【问题讨论】：

标签： z3 smt

【解决方案1】：

这是量词推理引擎之一中的错误。这个错误将被修复。同时，您可以通过使用数据类型而不是未解释的排序 + 基数约束来避免该错误。也就是说，您将Q 和T 声明为：

(declare-datatypes () ((Q q_accept_S13 q_T0_init q_accept_S7 q_accept_S6 q_accept_S5 q_accept_S4 q_T0_S3 q_accept_S12 q_accept_S10 q_accept_S9 q_accept_all)))

（声明数据类型（）（（T t_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7）））

上面的声明本质上定义了两种“枚举”类型。通过这些声明，您将获得第二个查询的一致答案。

【讨论】：