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

Question

我可以运行从命令行使用 z3 进行（字符串）查询，指定或不指定 smt.string_solver=z3str3:

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

Answer 1

z3str3 不是一个策略，而是一个参数（对于默认的 smt 策略）。您可以通过调用 Z3_global_param_set("smt.string_solver", "z3str3");

全局设置它（最好在构造任何 contexts/solvers 之前）

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

How to specify smt.string_solver=z3str3 through (Z3) API?

api

z3