小编use*_*755的帖子

我想使用 z3 求解器使用 C API 定义一个二维数组如下

a[3][3] = { {0,0,0},{0,0,0},{0,0,0}}

如何使用 Z3 求解器 C API 定义它，其中我需要添加约束，例如每行的总和等于 1，并且每个颜色的总和应该 <= 100。