Z3 c++api替换数组

Z3 c++ api substitution array

本文关键字：数组 替换 c++api Z3      更新时间：2023-10-16

我正在尝试对包含数组和整数的表达式使用替换。替换后出现分段错误。

这是代码：

    context cxt;
    vector<Z3_ast> vars_ast,primed_vars_ast;
    sort Int = cxt.int_sort();
    sort Array = cxt.array_sort(Int,Int);
    expr arr =cxt.constant("arr",Array); 
    vars_ast.push_back(arr); 

    expr i =cxt.int_const("i"); 
    vars_ast.push_back(i); 

    expr test_expr = select(arr,i)==0 ;
    primed_vars_ast.push_back(cxt.constant("arr_primed",Array));
    primed_vars_ast.push_back(cxt.int_const("i_primed"));
    expr cstr_expr (cxt,
                 ast(cxt,
                  Z3_substitute(cxt,
                        ast(test_expr),
                        vars_ast.size(),
                        vars_ast.data(),
                        primed_vars_ast.data())));

但是，如果我从ast数组中删除变量i，而是对表达式test_expr = select(arr,1)==0进行替换测试，那么它就成功了。我是不是错过了什么？

这里的问题是您混合了C和C++代码（z3.h和z3++.h）。z3 C-API不会为您进行引用计数，因此每次创建Z3_ast和Z3_dec_ref时，每次Z3_ast超出范围/使用时，您都必须调用Z3_inc_ref。

C++API（z3++.h）的主要目的是将引用计数代码抽象出来，但这只适用于不混合使用C代码的情况。经验法则是：如果一个函数被称为"Z3_*"，那么它是一个C函数，如果它返回Z3_ast，则立即将其放入expr中，例如：

expr q(cxt, Z3_mk_select(cxt, arr, i));

在这个特定的示例中，我们可以将vector<Z3_ast>更改为expr_vector（附带z3+++.h）。然后可以将该示例修改为

context cxt;
expr_vector vars_ast(cxt), primed_vars_ast(cxt);
sort Int = cxt.int_sort();
sort Array = cxt.array_sort(Int,Int);
expr arr = cxt.constant("arr",Array); 
vars_ast.push_back(arr);
expr i = cxt.int_const("i"); 
vars_ast.push_back(i); 
expr test_expr = select(arr,i)==0;
primed_vars_ast.push_back(cxt.constant("arr_primed",Array));
primed_vars_ast.push_back(cxt.int_const("i_primed"));
test_expr.substitute(vars_ast, primed_vars_ast);
相关文章：