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，並設計一些機制來識別軟約束。