1

Z3ソルバーについて知らない場合は、親切なリクエストに答えないでください.iは以前にこの質問を投稿しました.Cで配列を実装する方法のようないくつかの回答がポップアップしました.このフォーラムでZ3ソルバーを開発した人が何人かいます.それは彼らを対象としています. Z3 ソルバーは、この質問への返信を避けてください。

以前にこの質問を投稿し、Python のように解決策を得ました。以下の問題は既に python で実装していました。論文の一部として、Z3 ソルバーを社内ツールに統合するために Z3 ソルバーを移植しようとしています。 Pythonではなく「C」言語で以下の要件の解決策を示します。

C APIを使用してz3ソルバーを使用して、次のように2次元配列を定義して作成したい

例: a[3][3] Z3 ソルバー C API を使用してこれを定義する方法

2 次元配列の要素は 0 または 1 のみです。各行の合計は各列 (コントローラー メモリ) の合計 1 に等しくなります。解決しようとしている問題は 100 以下である必要があります。 [sw]={50,25,100,75} は、各関数によって生成されたデータ (50kb) を表します。b[cont]={100,100,100} メモリ (kb) 容量のコントローラー。[4][3 を生成しようとしています。 ] の行列は、上記の制約を満たすコントローラーへの機能割り当てを示しています。

上記の問題のサンプル出力 (これは非常に多くの構成のうちの 1 つです)。ただし、有効な構成です。

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 リスト内包表記によってエンコードが簡素化されます。Python の例 ( Z3 ソルバーの 2 次元配列) を C++ でエンコードする方法の 1 つを次に示します。主な違いは次のとおりです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 に答える