1

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

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

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

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

二维数组的元素只有 0 或 1。每行的总和等于 1 每列的总和（控制器内存）如果我 <= 100 我要解决的问题是，我有两个数组，其中一个是[sw]={50,25,100,75} 表示每个函数产生的数据（50kb）。b[cont]={100,100,100} 具有内存（kb）容量的控制器。我们正在尝试生成 a[4][3 ] 矩阵显示了对满足上述约束的控制器的功能分配

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

a[sw][续] =

ABC
A 1 0 0 B 1 0 0
C 0 1 0
D 0 0 1

4

1 回答 1

3

Z3 Python API 在 C API 之上实现。任何用 Python 编写的 Z3 示例都可以转换为 C/C++。然而，Z3 Python API 使用起来更方便，而且 Python 列表推导简化了编码。这是在 C++中编码 Python 示例（ Z3 求解器中的二维数组）的一种方法。主要区别是：我使用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";
    }
}
于 2013-04-22T14:53:04.503 回答