如何在Z3中表达软约束和硬约束？我从API中了解到可能有假设(软约束),但在使用命令行工具时我无法表达这一点.我用z3/smt2/si来调用它
如果"pop"在增量约束中完全破坏上下文(即学习的lemmas),那么解决使用"堆栈模式"的目的是什么？
理由:我想如果我只有一个约束(几个合取),那么最好只进行一次查询,而不是将合并堆叠在不同的框架中.如果我有超过1个约束并且决定使用堆栈的增量求解,那么在查询一个约束之后我需要(至少有一个)pop,这可能会"破坏学习的lemmas".那么,使用增量求解(使用堆栈)的优点是什么.什么"摧毁流行音乐中学习的引理"真的意味着什么？
观察:我的实验表明这是非常有益的,但我找到了指示(参见smt公式,总共有500个查询,增量求解在0.01秒内完成,而noninc.求解在16秒完成.)与此观察结果相矛盾.
z3 ×2