特定のテキスト内の部分文字列を見つけるために、Z3 で配列と量指定子を使用しようとしています。
私のコードは次のとおりです。
(declare-const a (Array Int Int))
(declare-const x Int)
;; a|A
(assert (or (= (select a 0) 61) (= (select a 0) 41)))
;; b|B
(assert (or (= (select a 1) 62) (= (select a 1) 42)))
;; c|C
(assert (or (= (select a 2) 63) (= (select a 2) 43)))
(assert (>= x 0))
(assert (< x 3))
(assert (exists ((i Int)) (= (select a i) 72) ))
(check-sat)
Z3 は、それが SAT であってはならないときに、SAT であると言います。私は Z3 と SMT 理論にかなり慣れていないので、自分のコードの何が問題なのかわかりません。
あなたの例では、i を 0、1、2 の範囲外の任意の自然数にすることで実際に満足できます。したがって、たとえば i = 3 とすると、インデックス 3 の配列を何らかの方法で制約していないため、 a[3] が 72 である可能性があります。
Z3@Rise インターフェースでの例への満足のいく割り当て (モデル) を示すリンクと、次に説明する修正を次に示します: http://rise4fun.com/Z3/E6YI
これが起こらないようにするための 1 つの方法は、i の範囲を、既に割り当てた配列インデックスの 1 つに制限することです。つまり、i を 0 から 2 の間に制限します。
(declare-const a (Array Int Int))
(declare-const x Int)
;; a|A
(assert (or (= (select a 0) 61) (= (select a 0) 41)))
;; b|B
(assert (or (= (select a 1) 62) (= (select a 1) 42)))
;; c|C
(assert (or (= (select a 2) 63) (= (select a 2) 43)))
(assert (>= x 0))
(assert (< x 3))
(assert (exists ((i Int)) (= (select a i) 72)))
(check-sat)
(get-model) ; model gives i == 3 with a[i] == 72
(assert (exists ((i Int)) (and (>= i 0) (<= i 2) (= (select a i) 72) )))
(check-sat)