CVC4 相当于 Z3 的 seq.unit

Question

我正在尝试运行以下同时使用 Z3 和 CVC4 的不饱和示例。如果我用 (seq.unit #x00) 替换 "\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/issues 的答案（为了完整性而带到这里）：

Thanks for the benchmark. Unfortunately there isn't anything that converts between bitvectors and strings at the moment.

We are planning to add support for sequences soon (issue #1122). Although of course there isn't an SMT standard for sequences yet. I will keep this issue in mind when we add support for sequences.

CVC4 相当于 Z3 的 seq.unit

CVC4 equivalent of Z3's seq.unit

smt

cvc4