CVC4 最小化/最大化模型优化 [英] CVC4 minimize/maximize model optimization

问题描述

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

Does CVC4 an option to maximize or minimize the result model for bitvectors as Z3 does?

谢谢.

推荐答案

遗憾的是，CVC4(尚)不支持优化.对于位向量，您始终可以使用多个查询和二进制搜索自行完成，但它不是内置的.

Unfortunately, CVC4 does not (yet) support optimization. For bitvectors, you can always do it yourself using multiple queries and binary search, but it's not built-in.

这篇关于CVC4 最小化/最大化模型优化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！