SMT 中量化算术的推理限制是什么? [英] What are the limits of reasoning in quantified arithmetic in SMT?

问题描述

我在以下看似微不足道的基准测试中尝试了多种 SMT 求解器(CVC3、CVC4 和 Z3):

I have tried several SMT solvers (CVC3, CVC4 and Z3) on the following seemingly trivial benchmark:

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)

求解器都返回未知.我知道这是一个无法确定的片段(很好的非线性)，但我希望会有一些简单的实例化启发式方法可以解决它.我还尝试使用常量添加一些额外的断言，但没有帮助.

The solvers all return unknown. I understand that this is an undecidable fragment (well non-linear) but I was expecting there would be some simple instantiation heuristics that could solve it. I also tried adding some extra assertions with constants but it didn't help.

有没有办法解决这些问题?SMT 中量化算术推理的局限性是什么?

Is there a way to attack these problems and what are the limits of reasoning in quantified arithmetic in SMT?

推荐答案

Pad 是正确的，qe 预处理器可能相当昂贵.此外，它对来自软件验证工具的公式无效，例如 VCC、Poirot, Dafny、VeriFast、Why3 和 ESCJava2.它是无效的，因为这些应用程序生成的公式还包含未解释的函数、数组等.

Pad is correct, the qe preprocessor can be quite expensive. Moreover, it is not effective in formulas coming from software verification tools such as VCC, Poirot, Dafny, VeriFast, Why3, and ESCJava2. It is not effective because the formulas produced by these applications also contain uninterpreted functions, arrays, etc.

正如 Pad 的回答所暗示的那样，Z3 是引擎的集合.它提供 API 和命令，允许用户选择将使用哪个引擎(或引擎组合)来解决问题.当用户只是说 (check-sat) 是试图猜测解决输入公式的最佳引擎是什么.猜测是基于输入公式的结构和用户提供的注释(例如:set-logic 命令).我们不断扩展自动检测的片段集以及我们提供的引擎集.

As Pad's answer suggests, Z3 is a collection of engines. It provides APIs and commands that allow users to select which engine (or combination of engines) will be used to solve a problem. When the user just says (check-sat) is tries to guess what is the best engine for solving the input formula. The guess is based on the structure of input formula and annotations provided by the user (example: the set-logic command). We are continuously expanding the set of fragments that are automatically detected, and the set of engines we provide.

话虽如此，令人尴尬的是，Z3 错过了诸如 LIA 之类的片段，并且没有自动对其应用 qe 过程.对于LIA 公式，qe 通常是最好的选择.基于 E 匹配或 MBQI 的替代方案无效，因为它们适用于完全不同的片段.

That being said, it is embarrassing that Z3 missed a fragment such as LIA and did not automatically applied the qe procedure to it. For LIA formulas, qe is usually the best option. Alternatives based on E-matching or MBQI are not effective since they are meant for completely different fragments.

我只是提交的代码来检测LIA(甚至当不使用 set-logic 时).unstable (working-in-progress) 分支中已经有此更改.它将在明天的每晚构建和下一个正式版本中提供.

I just committed code that detects LIA (even when set-logic is not used). The change is already available in the unstable (working-in-progress) branch. It will be available tomorrow in the nightly builds, and in the next official release.

这篇关于SMT 中量化算术的推理限制是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！