Z3 API中str.suffix未识别求助：是否函数名称有误？

你碰到的坑其实是Z3的C API和SMT-LIB脚本里的函数命名不对应导致的：

• 在z3_api.h里看到的后缀检查函数是Z3_mk_str_suffix，但这是C API层面的命名
• 而在SMT-LIB脚本中，对应的正确函数名是str.suffixof，不是你一开始尝试的str.suffix

你后来修正的脚本已经换成了正确的str.suffixof，所以Z3能正常处理，还给你返回了sat的结果。

修正后的完整脚本 #

(declare-const s String)
(declare-const s00 String)
(declare-const s1 String)
(declare-const s2 String)
(declare-const i Int)
(assert (= s "X2a2@@aDD\x00444ppa800"))
(assert (= s00 (str.substr s 0 (str.indexof s "\x00" 0))))
(assert (str.suffixof s1 s00))
(assert (str.suffixof s2 s1))
(assert (= (str.len s1) (+ (str.len s2) 1)))
(assert (or (and (str.contains s00 "a") (str.contains s1 "a")) (not (str.contains s00 "a"))))
(assert (not (str.contains s2 "a")))
(assert (= i (ite (not (str.contains s00 "a")) -1 (- (str.len s00) (str.len s1)))))
(check-sat)
(get-value (s s00 s1 s2 i))

Z3运行后的输出结果 #

sat
((s "X2a2@@aDD\x00444ppa800")
 (s00 "X2a2@@aDD")
 (s1 "aDD")
 (s2 "DD")
 (i 6))

简单总结下：Z3的C API和SMT-LIB脚本的函数命名规则有差异，写SMT-LIB脚本时要遵循SMT-LIB标准的字符串函数命名（比如str.suffixof、str.prefixof、str.contains等），不能直接照搬C API里的函数名哦。

内容的提问来源于stack exchange，提问作者OrenIshShalom