z3 - Z3 maxsat smtlib 2.0

Question

有没有办法使用 smtlib2.0 实例对 c++ api 进行 maxsat。即，如何使函数 get_soft_constraints 与 smtlib2.0 实例一起工作？

Answer 1

不，该maxsat示例是在引入 SMT 2.0 之前实施的。可以修改该示例以读取 SMT 2.0 文件。基本思想是使用 SMT 2.0 解析器而不是 SMT 1.0，并设计一些机制来识别软约束。