z3中`str.indexof`与`seq.indexof`之间的差异

Question

在z3中，tutorial中分别提到str.indexof和seq.indexof。但是，在Z3 C API中，只有一个相关函数Z3_mk_seq_index。对于8位BitVecs的序列，该函数是否进行特殊情况处理？意思是，如果我的序列都是字符串，Z3_mk_seq_index仍会使用z3str3代码库吗？还是会退回到z3的序列求解器上？

Answer 1

8位值的序列与z3中的字符串之间没有区别。实际上，所有字符串都被视为8位值的序列。

seq.indexof和str.indexof之间的唯一区别是它们的类型。后者只是前者的专业化。

要在常规字符串求解器和z3str3之间切换，只需使用适当的命令行开关smt.string_solver。有效选项为seq，z3str3和auto。