时间戳

首页 > 解决方案 > CVC4 相当于 Z3 的 seq.unit

smt - CVC4 相当于 Z3 的 seq.unit

问题描述

我正在尝试使用 Z3 和 CVC4 运行以下 unsat 示例。如果我用(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

以下是我使用 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)))
                                        ^
")

标签： smtcvc4

解决方案

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

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

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

推荐阅读