C语言中的Z3数组不是python

Question

如果您不了解 Z3 求解器，请不要回答。我之前发布了这个问题，弹出了一些答案，例如如何在 C 中实现数组。有一些人在这个论坛上开发了 Z3 求解器。它是针对他们的。如果不懂Z3求解器的请不要回答这个问题。

我之前已经发布了这个问题并得到了 Python 中的解决方案。我们已经在 python 中实现了以下问题。我们正在尝试移植 Z3 求解器以将 Z3 求解器集成到内部工具中，作为我论文的一部分。你能帮助我用“C”语言而不是 python 显示以下要求的解决方案。

我想使用 C API 使用 z3 求解器定义和创建一个二维数组，如下所示

示例：a[3][3] 如何使用 Z3 求解器 C API 来定义它，我需要在其中添加约束，例如

二维数组的元素只有0或1。 每行之和等于 1 每列的总和（控制器内存）应该

上述问题的示例输出（这可以是众多配置中的一种）。但它是一个有效的配置

a[sw][继续] =

A B C
一个 1 0 0 B 1 0 0
C 0 1 0
D 0 0 1

Answer 1

Z3 Python API 是在 C API 之上实现的。任何用 Python 编写的 Z3 示例都可以转换为 C/C++。然而，Z3 Python API 使用起来更方便，而且 Python 列表推导简化了编码。这是在 C++ 中编码 Python 示例 (Two dimensional Array in Z3 solver) 的一种方法。 主要区别是：我使用 std::vector 代替列表，使用 for 循环代替列表推导。

void cpp_vector_example() {
    context c;
    unsigned n = 3;
    std::vector<std::vector<expr> > A;
    // Create a nxn matrix of Z3 integer constants
    for (unsigned i = 0; i < n; i++) {
        A.push_back(std::vector<expr>());
        for (unsigned j = 0; j < n; j++) {
            char name[100];
            sprintf(name, "a_%d_%d", i, j);
            A[i].push_back(c.int_const(name));
        }
    }

    solver s(c);

    // Add constraint: the sum of each row is one
    for (unsigned i = 0; i < n; i++) {
        expr sum(c);
        sum = A[i][0];
        for (unsigned j = 1; j < n; j++) {
            sum = sum + A[i][j];
        }
        s.add(sum == 1);
    }

    // Add constraint: the sum of each column is less than 100
    for (unsigned j = 0; j < n; j++) {
        expr sum(c);
        sum = A[0][j];
        for (unsigned i = 1; i < n; i++) {
            sum = sum + A[i][j];
        }
        s.add(sum <= 100);
    }

    // Add constraint: for each a_i_j in the matrix, 0 <= a_i_j <= 10
    for (unsigned j = 0; j < n; j++) {
        for (unsigned i = 1; i < n; i++) {
            s.add(0 <= A[i][j]);
            s.add(A[i][j] <= 100);
        }
    }

    // Display constraints added to solver s.
    std::cout << s << "\n";

    // Solve constraints
    std::cout << s.check() << "\n";

    // Print solution (aka model)
    model m = s.get_model();
    std::cout << m << "\n";

    // Print result as a matrix
    for (unsigned i = 0; i < n; i++) {
        for (unsigned j = 0; j < n; j++) {
            std::cout << m.eval(A[i][j]) << " ";
        }
        std::cout << "\n";
    }
}