Explore Sequences in SMT

[yangky11]

https://microsoft.github.io/z3guide/docs/theories/Sequences/

[JC-Chen1]

After reading the basic operations supported about sequence by smt, I tried to encode the summation in the format of (seq.fold_left fn b s).

Example,

theorem induction_sum2kp1npqsqm1 (n : ℕ) :
    ∑ k in Finset.range n, (2 * k + 3) = (n + 1) ^ 2 - 1 := by

After encoding,

(declare-const s (Seq Int))

(define-fun sum ((acc Int) (x Int)) Int (+ acc x))

(declare-const n Int)

(assert (= (seq.len s) n))

(assert (forall ((k Int))
  (=> (and (>= k 0) (< k n))
  (= (seq.nth s k) (+ 3 (* 2 k))))
))

(assert (not (= (- (^ (+ 1 n) 2) 1) (seq.fold_left sum 0 s))))

(check-sat)

Specifically, I represent sum as

(define-fun sum ((acc Int) (x Int)) Int (+ acc x))
(seq.fold_left sum 0 s)

But SMT-solvers stucked when searching the answer.

I wonder if it mainly comes from variable sequence length issue.

So I take another example where sequence is length-fixed.

Example2,

theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) :
    (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by

After encoding,

(declare-fun v ((Int)) Int)

(assert (forall ((n Int)) (= (v n) (- (* 2 n) 1))))

(declare-const s (Seq Int))
(assert (= (seq.len s) 100))

(define-fun sum ((acc Int) (x Int)) Int (+ acc x))

(assert (forall ((k Int))
    (=> (and (>= k 0) (< k 100))
    (= (seq.nth s k) (v (+ k 1))))
))

(assert (not (= (mod (seq.fold_left sum 0 s) 7) 4)))

(check-sat)

Z3 solver achieve to output unsat but take quite a long time.

[JC-Chen1]

It seems that under current encoding strategy, difficulty of searching process is highly related to length of sequence.

[yangky11]

The encoding looks good to me. Problems related to sequences are just inherently more challenging, and they sometimes require induction, which SMT solvers are not good at. I think we can just go with the current implementation.

[JC-Chen1]

Got it.