如果“pop”完全破坏了上下文（即学到的引理）
增量约束求解使用“堆栈”的目的是什么
模式”？
理由：我想如果我只有 1 个约束（几个
合词）最好进行单个查询，而不是
将单独帧中的合取词堆叠到堆栈上。如果我
有超过 1 个约束并决定使用增量求解
堆栈，那么我需要在查询一个后（至少制作一个）弹出
约束，这可能会“破坏习得的引理”。所以，
使用增量求解（使用堆栈）的优点是什么？
“摧毁流行音乐中的习得引理”到底意味着什么？
观察：我的实验表明这确实有益，但我
找到指示（参见，总共有 500 个查询，增量求解在 0.01 秒内完成，而非增量求解。 16秒内解决完毕。 ）与矛盾
这一观察。
当存在推送/弹出命令时，Z3 本质上会切换到完全不同的求解器，因为它检测到需要增量支持。增量求解器在非增量查询上通常（但并非总是）较慢，但反过来可以利用增量性。另请参阅此处：在使用和不使用推送调用的情况下对 UFBV 上的 Z3 进行增量调用 https://stackoverflow.com/questions/9131078/incremental-calls-to-z3-on-ufbv-with-and-without-push-calls, Z3 中的软/硬约束 https://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3.
销毁学习引理意味着那些在弹出后无效的引理将被删除。它们变得无效，因为它们依赖于最内部范围内的某些约束，因此它们后面的所有引理现在都无效。可能有一些例外，但通常 Z3 会尝试仅销毁无效的引理。
抱歉，如果之前的帖子可能引起任何混乱（SMT 求解器中约束强化的效率 https://stackoverflow.com/questions/11245992/efficiency-of-constraint-strengthening-in-smt-solvers）。该帖子并不完全清楚哪些引理被删除，并且已经更新。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
