如果评论中间的`(check-sat)`调用，为什么查询结果会改变? [英] Why does a query result changes if comment an intermediate `(check-sat)` call?

问题描述

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

While debugging UNSAT query I noticed an interesting difference in the query status. The query structure is:

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 调用.触发此行为的查询是此处.

There are no pop calls in the query. The query that triggers this behaviour is here.

想法为什么?

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

Note: I don't actually need incrementality, it is for debugging purposes only. Z3 version is 3.2.

推荐答案

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

This is a bug in one of the quantifier reasoning engines. This bug will be fixed. In the meantime, you can avoid the bug by using datatypes instead of uninterpreted sorts + cardinality constraints. That is, you declare Q and T as:

(declare-datatypes() ((Q q_accept_S13 q_T0_init q_accept_S7q_accept_S6 q_accept_S5 q_accept_S4 q_T0_S3 q_accept_S12 q_accept_S10q_accept_S9 q_accept_all)))

(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)))

(declare-datatypes () ((T t_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7)))

(declare-datatypes () ((T t_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7)))

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

The declarations above are essentially defining two "enumeration" types. With these declarations, you will get a consistent answer for the second query.

这篇关于如果评论中间的`(check-sat)`调用，为什么查询结果会改变?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！