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

【问题标题】：How to specify smt.string_solver=z3str3 through (Z3) API?如何通过 (Z3) API 指定 smt.string_solver=z3str3？
【发布时间】：2018-06-12 08:48:00
【问题描述】：

无论是否指定 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（叹气）......我一定是做错了什么，这是怎么回事？谢谢！

【问题讨论】：

标签： api z3

【解决方案1】：

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

【讨论】：

谢谢，这行得通——顺便问一下，将来只有一个字符串求解器吗？而 z3str3 会完全被 z3 吸收吗？还是不行？