2

APIを使用してSMTLIB式を読んだとします。

context ctx;
...
expr F = to_expr(ctx, Z3_parse_smtlib2_file(ctx,argv[1],0,0,0,0,0,0));

式Fは、次の形式のアサーションの接続詞です。

(and (< (+ x y) 3)
     (> (- x1 x2) 0)
     (< (- x1 x2) 4)
     (not (= (- x1 x2) 1))
     (not (= (- x1 x2) 2))
     (not (= (- x1 x2) 3)))

投稿から次のコードフラグメントを使用して、この接続詞から個々のアサーションを抽出したいと思います。unsatコアのz3 split句を使用して、unsatコアをもう一度見つけてみてください。

    F = F.simplify();
    for (unsigned i = 0; i < F.num_args(); i++) {
        expr Ai = F.arg(i);
        // ... Do something with Ai, just printing in this example.
        std::cout << Ai << "\n";
    }

を利用した後F.arg(i)、元の句(< (+ x y) 3)はに変更されました(not (<= 3 (+ x y)))。これが私の

(not (<= 3 (+ x y)))a）質問：条項をどのように配置でき(< (+ x y) 3)ますか？

b）質問：<=この場合、記号は以下を意味するのではなく、意味することを意味すると思います。私は正しいですか？

c）質問：句(not (<= 3 (+ x y)))モデルがtrueまたはfalseであるため、次のような算術値を取得するにはどうすればよいx = 1, y = -1ですか？

どんな提案にもとても感謝しています。どうもありがとうございます。

4

1 に答える 1

2

式はwhen に(< (+ x y) 3)変換されます。使用したコード フラグメントでは、ネストされた「and」を「フラット」にするためにメソッドが使用されています。つまり、数式は にフラット化されます。次に、for ループを使用して、すべての結合を簡単にトラバースできます。ただし、は入力式で他の変換も実行します。すべての変換が同等性を維持することに注意してください。つまり、入力式と出力式は論理的に等価です。によって適用される変換が望ましくない場合は、この方法を避けることをお勧めします。入れ子になった "and" をトラバースしたい場合は、補助ベクトルを使用できます。次に例を示します。(not (<= 3 (+ x y)))F = F.simplify()simplify()(and (and A B) (and C (and D E)))(and A B C D E)simplify()simplify()todo

expr_vector todo(c);
todo.push_back(F);
while (!todo.empty()) {
    expr current = todo.back();
    todo.pop_back();
    if (current.decl().decl_kind() == Z3_OP_AND) {
        // it is an AND, then put children into the todo list
        for (unsigned i = 0; i < current.num_args(); i++) {
            todo.push_back(current.arg(i));
        }
    }
    else {
        // do something with current
        std::cout << current << "\n";
    }
}
于 2012-11-29T06:57:55.463 に答える