StringSort 类型的工作序列时未知

Question

我正在尝试使用序列（对 SQL 条件进行建模，并需要它与

"US" in ImportCountries

形式的 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()) # Gives unknown.

这是Z3的限制还是我理解的限制，或者两者兼而有之？

尝试使用 Int 序列进行相同的操作，效果符合预期：

s = Solver()

test = Const('test', SeqSort(IntSort()))

expr1 = Contains(test, Unit(IntVal(1)))
expr2 = Not(Contains(test, Unit(IntVal(2))))

s.add(And(expr1 == True, expr2 == True))

print(s.check())
print(s.model())

Answer 1

你没有做错任何事。看起来 z3 可能缺少一些内部“启发式”来决定字符串大小写。请注意，当您混合字符串和序列时，逻辑变得半可判定：因此这是某些内部规则无法应用的情况。但如果元素是整数，它们就可以很好地处理。

作为参考，我用 CVC5 尝试了你的问题，结果很好。 （即，CVC5 能够肯定地回答您的查询。）这是与您的问题等效的 SMTLib：

(set-option :produce-models true)
(set-logic ALL)
(define-fun s1 () (Seq String) (seq.unit "US"))
(define-fun s3 () (Seq String) (seq.unit "AE"))
(declare-fun s0 () (Seq String))
(define-fun s2 () Bool (seq.contains s0 s1))
(define-fun s4 () Bool (seq.contains s0 s3))
(define-fun s5 () Bool (not s4))
(define-fun s6 () Bool (and s2 s5))
(assert s6)
(check-sat)
(get-value (s0))

使用 z3 我得到：

$ z3 a.smt2
unknown
(error "line 12 column 15: model is not available")

通过 CVC5，我得到：

$ cvc5 a.smt2
sat
((s0 (seq.unit "US")))

您应该在 https://github.com/Z3Prover/z3/issues 报告此问题。虽然严格来说这并不是一个错误，但我确信开发人员很想了解它。 （别忘了提及 CVC5 很好地解决了这个问题！）