api - 如何通过 (Z3) API 指定 smt.string_solver=z3str3？

Question

无论是否指定 smt.string_solver=z3str3，我都可以从命令行使用 z3 运行（字符串）查询：

z3 [smt.string_solver=z3str3] input.smt

如何通过 API 指定相同的内容？我尝试使用以下方法打印战术名称：

/***************/
/* [0] Context */
/***************/
Z3_context ctx = mk_context();

/**************/
/* [1] Solver */
/**************/
Z3_solver solver = mk_solver(ctx);

/*******************************/
/* [2] Print the tactics names */
/*******************************/
for (i=0;i<Z3_get_num_tactics(ctx);i++)
{
    printf("tactic %d is %s\n",i,Z3_get_tactic_name(ctx,i));
}

我得到了105 个战术名称的列表，但没有 z3str3（叹气）......我一定是做错了什么，这是怎么回事？谢谢！

标签： apiz3

Answer 1

z3str3不是一个策略，而是一个参数（对于默认smt策略）。您可以通过调用全局设置它（最好在构造任何上下文/求解器之前）Z3_global_param_set("smt.string_solver", "z3str3");