z3_astが節に対応するかどうかを調べるにはどうすればよいですか？

Question

私はcp apiで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のを横断/検査するためのいくつかの機能を提供します。 Z3 APIは最小限ですが、is_propositional_variable,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; 
    } 
}