optimization - CVC4 最小化/最大化模型优化

Question

CVC4 是否可以像 Z3 那样最大化或最小化位向量的结果模型？

谢谢。

Answer 1

不幸的是，CVC4（还）不支持优化。对于位向量，您始终可以使用多个查询和二进制搜索自己完成，但它不是内置的。