z3 - z3_astが句に対応するかどうかを確認するにはどうすればよいですか？

Question

私はcapiでZ3を使用しています。Z3_ast与えられた変数が以下のような節に対応するかどうかを知ることは可能or_b1_b2ですか？

Z3_ast or_b1_b2 = mk_binary_or(c,mk_bool_var(c,"b1"),mk_bool_var(c,"b2"));

ありがとうございました

Answer 1

はい、Z3 API は、AST を検査/トラバースするためのいくつかの関数を提供します。is_propositional_variableZ3 API は最小限ですが、 、is_literal、などの関数を記述するために必要な要素がすべて含まれていますis_clause。次に例を示します。

// Return true if the given ast is an application of the given kind
int is_app_of(Z3_context c, Z3_ast a, Z3_decl_kind k) {
   if (Z3_get_ast_kind(c, a) != Z3_APP_AST) 
       return 0;
   return Z3_get_decl_kind(c, Z3_get_app_decl(c, Z3_to_app(c, a))) == k;
}

// Return true if the given ast is an OR.
int is_or(Z3_context c, Z3_ast a) {
    return is_app_of(c, a, Z3_OP_OR);
}

// Return true if the given ast is a NOT.
int is_not(Z3_context c, Z3_ast a) {
    return is_app_of(c, a, Z3_OP_NOT);
}

// Return true if the given ast is an application of an unintepreted symbol.
int is_uninterp(Z3_context c, Z3_ast a) {
    return is_app_of(c, a, Z3_OP_UNINTERPRETED);
}

// Return true if the given ast is a uninterpreted constant.
// That is, it is application (with zero arguments) of an uninterpreted symbol.
int is_uninterp_const(Z3_context c, Z3_ast a) {
    return is_uninterp(c, a) && Z3_get_app_num_args(c, Z3_to_app(c, a)) == 0;
}

// Return true if the given ast has Boolean sort (aka type).
int has_bool_sort(Z3_context c, Z3_ast a) {
    return Z3_get_sort_kind(c, Z3_get_sort(c, a)) == Z3_BOOL_SORT;
}

// Return true if the given ast is a "propositional variable".
// That is, it has Boolean sort and it is uninterpreted.
int is_propositional_var(Z3_context c, Z3_ast a) {
    return is_uninterp_const(c, a) && has_bool_sort(c, a);
}

// Return true if the given ast is a "literal".
// That is, it is a "propositional variable" or the negation of a propositional variable.
int is_literal(Z3_context c, Z3_ast a) {
    if (is_propositional_var(c, a))
        return 1;
    if (is_not(c, a))
        return is_propositional_var(c, Z3_get_app_arg(c, Z3_to_app(c, a), 0));
    return 0;
}

// Return true if the given ast is a "clause".
// That is, it is a literal, or a disjuction (OR) of literals.
int is_clause(Z3_context c, Z3_ast a) {
    if (is_literal(c, a)) {
        return 1; // unit clause
    }
    else if (is_or(c, a)) {
        unsigned num;
        unsigned i;
        num = Z3_get_app_num_args(c, Z3_to_app(c, a));
        for (i = 0; i < num; i++) {
            if (!is_literal(c, Z3_get_app_arg(c, Z3_to_app(c, a), i)))
                return 0;
        }
        return 1;
    }
    else {
        return 0;
    }
}