增量求解有什么好处? [英] What are the benefits of incremental solving?

问题描述

如果pop"完全破坏了上下文(即学习的引理)增量约束解决使用堆栈"的目的是什么模式"?

If "pop" completely destroys context (i.e., learned lemmas) in incremental constraint solving what is the purpose of using "stack mode"?

基本原理:我想如果我只有 1 个约束(几个conjuncts)最好进行单个查询而不是将单独框架中的连接堆叠到堆叠上.如果我有超过 1 个约束并决定使用增量求解堆栈，然后我需要(至少制作一个)在查询一个后弹出约束，这大概会破坏学习的引理".所以，使用增量求解(使用堆栈)的优势是什么?破坏流行的学过的引理"的真正含义是什么?

Rationale: I imagine that if I have just 1 constraint (several conjuncts) it would be preferable to make a single query as opposed to stacking the conjuncts in separate frames onto the stack. If I have more than 1 constraint and decide to use incremental solving with stack, then I would need to (make at least one) pop after querying one constraint and that would presumably "destroy learned lemmas". So, what is the advantage of using incremental solving (with stacks)? What "destroying learned lemmas in pop" really means?

观察:我的实验表明这确实有益，但我找到指示(参见 smt 公式，总共有 500查询，增量求解在 0.01 秒内完成，而 noninc. 求解在 16 秒内完成.)与这个观察.

Observation: My experiments indicate this is really beneficial but I find the indication (see smt formulas, there are in total of 500 queries, incremental solving finished in 0.01sec, while noninc. solving finished in 16sec. ) contradictory with this observation.

推荐答案

当出现 push/pop 命令时，Z3 本质上会切换到一个完全不同的求解器，因为它检测到它需要支持增量.增量求解器在非增量查询上通常(但不总是)较慢，但反过来可以利用增量.另请参见此处:在 UFBV 上对 Z3 的增量调用使用和不使用推送调用，Z3 中的软/硬约束.

When push/pop commands are present, Z3 essentially switches to a completely different solver, because it detects that it needs support for incrementality. The incremental solver is usually (but not always) slower on non-incremental queries, but in turn can take advantage of incrementality. See also here: Incremental calls to Z3 on UFBV with and without push calls, Soft/Hard constraints in Z3.

销毁学习到的引理意味着那些在 pop 之后无效的引理将被删除.它们变得无效是因为它们依赖于最内层范围内的一些约束，因此从它们而来的所有引理现在都是无效的.可能有一些例外，但通常 Z3 只会尝试销毁无效的引理.

Destroying learned lemmas means that those lemmas that are not valid after pop will be removed. They become invalid because they depend on some constraints within the innermost scope and therefore all the lemmas that follow from them are now invalid. There may be some exceptions, but usually Z3 will try to destroy only invalidated lemmas.

抱歉，如果之前的帖子(SMT 求解器中约束强化的效率).那个帖子并没有完全清楚哪些引理被删除并且已经更新.

Sorry if there was any confusion that may have arisen from a previous post (Efficiency of constraint strengthening in SMT solvers). That post was not completely clear about which lemmas are removed and has since been updated.

这篇关于增量求解有什么好处?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！