如果"pop"在增量约束中完全破坏上下文(即学习的lemmas),那么解决使用"堆栈模式"的目的是什么？
理由:我想如果我只有一个约束(几个合取),那么最好只进行一次查询,而不是将合并堆叠在不同的框架中.如果我有超过1个约束并且决定使用堆栈的增量求解,那么在查询一个约束之后我需要(至少有一个)pop,这可能会"破坏学习的lemmas".那么,使用增量求解(使用堆栈)的优点是什么.什么"摧毁流行音乐中学习的引理"真的意味着什么？
观察:我的实验表明这是非常有益的,但我找到了指示(参见smt公式,总共有500个查询,增量求解在0.01秒内完成,而noninc.求解在16秒完成.)与此观察结果相矛盾.
当存在push/pop命令时,Z3实际上切换到完全不同的解算器,因为它检测到它需要支持增量.增量求解器通常(但不总是)在非增量查询上较慢,但反过来可以利用递增性.另请参见此处:UFBV上的Z3增量调用,带或不带推送调用,Z3中的软/硬约束.
摧毁学习的引理意味着那些在pop之后无效的引理将被删除.它们变得无效,因为它们依赖于最内层范围内的某些约束,因此它们后面的所有引理现在都是无效的.可能有一些例外,但通常Z3会尝试仅销毁无效的引理.
很抱歉,如果前一篇文章中出现任何混淆(SMT求解器中的约束强化效率).这篇文章并不完全清楚哪些lemmas被删除,并且已经更新.
| 归档时间： |
|
| 查看次数： |
676 次 |
| 最近记录： |