Z3数组在C语言，不是python

Question

如果你不知道Z3求解器，请不要回答。我张贴了这个问题早些时候的一些答案，如如何在C中实现数组弹出。在这个论坛里有一些开发Z3求解器的人。这是给他们的。如果你不知道Z3求解器，请避免回答这个问题。

我早些时候发布了这个问题，并在Python中得到了解决方案。我们已经在python中实现了下面的问题。我们正在尝试移植Z3求解器，将Z3求解器集成到内部工具中作为我论文的一部分。你能帮我展示一个解决以下要求的"C"语言，而不是python吗?

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

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

元素只能为0或1。每一行的和等于1每列(控制器内存)的总和应该是= 100我试图解决的问题是，我有两个数组，其中一个是a[sw]={50,25,100,75}，它表示每个函数产生的数据(50kb)。B [cont]={100,100,100}个内存(kb)容量的控制器。我们试图生成一个[4][3]矩阵，其中显示了满足上述约束的控制器的功能分配

对于上述问题，

示例输出(这可能是众多配置中的一个)。但它是一个有效的配置

(sw)[继续]=

A B C
A 1 0 0B 1 00 00
C 0 0 0
D 0 0 1

Answer 1

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";
    }
}