问opt分支中的Z3 opt上下文
EN

Stack Overflow用户

提问于 2014-07-20 12:51:32

回答 1查看 117关注 0票数 1

关于如何使用Z3选择分支的优化特性，我有一个相当具体的问题。

也就是说，我可以使用z3_optimize_assert将断言添加到"opt“上下文中，而这些约束确实有效。但是，添加到原始z3_context中的所有约束(用于创建优化上下文)都将被忽略。它是一个bug还是一个特性？有两个语境的目的是什么？

回答已采纳

发布于 2014-07-20 13:30:30

向上下文添加约束的唯一函数称为Z3_assert_cnstr。这是一个不受欢迎的函数。应该对要使用的引擎断言约束。现在有下列引擎：

 Z3_solver_assert
 Z3_fixedpoint_assert
 Z3_optimzie_assert
 Z3_goal_assert

断言对于求解者、定点上下文、优化上下文或目标分别是本地的.

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/24850673

复制

相似问题

问opt分支中的Z3 opt上下文EN