本文介绍了如何找出 z3_ast 是否对应于子句?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
限时送ChatGPT账号..我正在使用带有 c api 的 Z3.是否可以找出给定的 Z3_ast
变量是否对应于下面的 or_b1_b2
子句?
I am using Z3 with c api. Is it possible to find out if a given Z3_ast
variable corresponds to a clause like or_b1_b2
bellow?
Z3_ast or_b1_b2 = mk_binary_or(c,mk_bool_var(c,"b1"),mk_bool_var(c,"b2"));
谢谢
推荐答案
是的,Z3 API 提供了几个用于检查/遍历 AST 的函数.Z3 API 是简约的,但它具有编写函数的所有必要成分,例如:is_propositional_variable
、is_literal
和 is_clause
.下面是一个例子:
Yes, The Z3 API provides several functions for inspecting/traversing ASTs.
The Z3 API is minimalist, but it has all necessary ingredients for writing function such as: is_propositional_variable
, is_literal
, and is_clause
. Here is an example:
// 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;
}
}
这篇关于如何找出 z3_ast 是否对应于子句?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
更多推荐
[db:关键词]
发布评论