0

我正在尝试实现 String.Containts 函数。我写了一些简单的测试用例，但是下面的一个（应该返回 UNSAT）返回 SAT。

该测试尝试通过将所有可能的子字符串与想要的字符串（取自 Z3 输出的文本）进行比较来匹配字符串 'abcd' 中的子字符串 'bd'：

{(exists ((i Int))
  (let ((a!1 (forall ((k Int))
               (and (>= k i)
                    (<= k (+ i 1))
                    (= (select stringToScan k) (select substring (- k i)))
                    (= (select stringToScan 0) #x0061)
                    (= (select stringToScan 1) #x0062)
                    (= (select stringToScan 2) #x0063)
                    (= (select stringToScan 3) #x0064)
                    (= (select stringToSearch 0) #x0062)
                    (= (select stringToSearch 1) #x0064)))))
    (and (>= i 0)
         (< i 2)
         a!1
         (= (select substring 0) (select stringToSearch 0))
         (= (select substring 1) (select stringToSearch 1)))))}

我尝试了各种实现，但没有任何成功。

4

1 回答 1

1

如果您断言公式，它将返回 UNSAT。

http://rise4fun.com/Z3/szN

那个部分：

(forall ((k Int))
           (and (>= k i)
                (<= k (+ i 1)) ...)))

是错误的，因为您可以将 k 设置为 i + 2 或 i - 1。您可能的意思是写一个暗示而不是连词。有时对字符串使用数组并不是执行编码的最佳方式。自动机工具包（参见：http ://rise4fun.com/Rex ）使用序列。

于 2012-09-06T16:41:40.957 回答