CVC4 相当于 Z3 的 seq.unit答案

【问题标题】：CVC4 equivalent of Z3's seq.unitCVC4 相当于 Z3 的 seq.unit
【发布时间】：2018-06-16 05:29:58
【问题描述】：

我正在尝试使用 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

当我改用 seq.unit 行时，cvc4 抱怨的是：

(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)))
                                        ^
")

【问题讨论】：

您可以尝试询问：github.com/CVC4/CVC4/issues
谢谢，也发在那里：github.com/CVC4/CVC4/issues/2075

标签： smt cvc4

【解决方案1】：

这是来自CVC4/issues 的答案（为了完整起见，这里提供）：

感谢基准测试。不幸的是，没有任何东西目前在位向量和字符串之间进行转换。

我们计划很快添加对序列的支持（问题 #1122）。虽然当然还没有序列的 SMT 标准。我当我们添加对序列的支持时会记住这个问题。

【讨论】：