在处理字符串序列时未知
作者: manojlds创建于 2024年3月6日更新于 2026年7月13日
标签string
我正在尝试使用序列（模拟 SQL 条件，并需要它与 ImportCountries 中的"US"形式的 IN 子句一起工作，以查看两个条件是否同时为 True）：
s = Solver()
test = Const('test', SeqSort(StringSort()))
expr1 = Contains(test, Unit(StringVal("US")))
expr2 = Not(Contains(test, Unit(StringVal("AE"))))
s.add(And(expr1 == True, expr2 == True))
print(s.check()) # 返回未知值。内容来源: Z3Prover/z3