C语言中的Z3数组而非python

Question

如果你不知道Z3求解器，请不要回答。我之前发布了这个问题，一些答案，比如如何用C实现up.There中的数组，是一些在这个forum.Its中开发Z3求解器的人，目的是为了them.If你不知道Z3求解器，请避免回答这个问题。

我早些时候发布了这个问题，并得到了解决方案，因为在Python.we中已经实现了以下问题已经在python.we中尝试移植Z3求解器来集成Z3求解器到内部工具作为我的thesis.Could的一部分，您帮我显示了解决方案的"C“语言，而不是在Python语言的以下要求。

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

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

2维数组的元素仅为0或1。每行的总和等于每列的1和(控制器内存)如果我<= 100我试图解决的问题是，我有两个数组，其中一个是asw={50,25,100,75}，它表示由每个具有内存(Kb)的控制器{100,100,100}产生的数据(50kb) capacity.we试图生成a4矩阵，显示满足上述约束的控制器的函数分配

上述problem.but的示例输出(这可以是众多配置中的一个)它是有效的配置

asw =

A、B、C

A 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++。但是，Python Python API使用起来要方便得多，而且Z3列表理解简化了编码。以下是在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";
    }
}