Z3's seq.unit的CVC4等价

Question

我试图使用Z3和CVC4运行下面的unsat示例。如果我将"\x00"替换为(seq.unit #x00)，那么对于Z3来说这不是问题，但是CVC4抱怨说它不知道seq.unit。

(declare-fun AB_serial_1_version_0 () String)
(declare-fun AB_serial_1_version_1 () String)

(assert (= (str.len AB_serial_1_version_0) 16))
(assert (= (str.len AB_serial_1_version_1) (str.len AB_serial_1_version_0)))
(assert (= (str.at AB_serial_1_version_1 15) "\x00"))
;;; (assert (= (str.at AB_serial_1_version_1 15) (seq.unit #x00)))

(assert (= (str.indexof (str.substr AB_serial_1_version_1 0 (- 16 0)) "\x00" 0) (- 0 1)))
(check-sat)

下面是命令行调用：

cvc4 --strings-exp --quiet --produce-models --lang=smt2 ./example.txt

下面是cvc4在使用seq.unit行时抱怨的地方：

(error "Parse Error: ./example.txt:7.54: Symbol 'seq.unit' not declared as a variable

...= (str.at AB_serial_1_version_1 15) (seq.unit #x00)))
                                        ^
")

Answer 1

这是CVC4 4/问题给出的答案(这里是为了完整性而提出的)：

谢谢你的基准。不幸的是，目前没有任何东西可以在位向量和字符串之间进行转换。 我们计划很快增加对序列的支持(第1122期)。当然，对于序列还没有SMT标准。当我们添加对序列的支持时，我将记住这个问题。