z3 (v4.3.1) を使用して、量指定子を持つ未解釈の関数を含む制約セットを解決しています。問題は、z3 のメモリ使用量が非常に高いことです。以下は私の制約です：
(solver
(v0 0)
(forall ((i Int))
(let ((a!1 (=> (v0 i)
(and (not (v1 i))
(not (v2 i))
(not (v3 i))
(not (v4 i))
(not (v5 i))))))
(=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v0 i) (v1 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v1 i)
(and (not (v0 i))
(not (v2 i))
(not (v3 i))
(not (v4 i))
(not (v5 i))))))
(=> (>= i 0) a!1)))
forall ((i Int))
(let ((a!1 (=> (v1 i) (or (v2 (+ i 1)) (v5 (+ i 1))))))
(=> (>= i 0) a!1)))
(forall ((i Int))
(let ((a!1 (=> (v2 i)
(and (not (v0 i))
(not (v1 i))
(not (v3 i))
(not (v4 i))
(not (v5 i))))))
(=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v2 i) (v3 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v3 i)
(and (not (v0 i))
(not (v1 i))
(not (v2 i))
(not (v4 i))
(not (v5 i))))))
(=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v3 i) (v4 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v4 i)
(and (not (v0 i))
(not (v1 i))
(not (v2 i))
(not (v3 i))
(not (v5 i))))))
(=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v4 i) (v1 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v5 i)
(and (not (v0 i))
(not (v1 i))
(not (v2 i))
(not (v3 i))
(not (v4 i))))))
(=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v5 i) (v5 (+ i 1)))))
(exists ((i Int)) (=> (>= i 0) (v5 i)))
(forall ((i Int))
(let ((a!1 (not (v5 (- (+ i 3) 1)))))
(let ((a!2 (=> (and (v0 i) (v1 (+ i 1))) a!1)))
(=> (>= i 0) a!2))))
(forall ((i Int))
(let ((a!1 (not (v5 (- (+ i 4) 1)))))
(let ((a!2 (=> (and (v3 i) (v4 (+ i 1)) (v1 (+ i 2))) a!1)))
制約セットを smt2 ファイルに書き込み、それを解決するために z3 を使用すると、すぐに「不明」という結果が得られます。以下はsmt2ファイルの内容です
(declare-fun v0 (Int) Bool)
(declare-fun v1 (Int) Bool)
(declare-fun v2 (Int) Bool)
(declare-fun v3 (Int) Bool)
(declare-fun v4 (Int) Bool)
(declare-fun v5 (Int) Bool)
(assert (v0 0))
(assert (forall ((i Int)) (=> (v0 i) (and (not (v1 i)) (not (v2 i)) (not (v3 i)) (not (v4 i)) (not (v5 i))))))
(assert (forall ((i Int)) (=> (v1 i) (and (not (v0 i)) (not (v2 i)) (not (v3 i)) (not (v4 i)) (not (v5 i))))))
assert (forall ((i Int)) (=> (v2 i) (and (not (v1 i)) (not (v0 i)) (not (v3 i)) (not (v4 i)) (not (v5 i))))))
(assert (forall ((i Int)) (=> (v3 i) (and (not (v1 i)) (not (v2 i)) (not (v0 i)) (not (v4 i)) (not (v5 i))))))
(assert (forall ((i Int)) (=> (v4 i) (and (not (v1 i)) (not (v2 i)) (not (v3 i)) (not (v0 i)) (not (v5 i))))))
(assert (forall ((i Int)) (=> (v5 i) (and (not (v1 i)) (not (v2 i)) (not (v3 i)) (not (v4 i)) (not (v0 i))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (v0 i) (v1 (+ i 1))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (v1 i) (or (v2 (+ i 1)) (v5 (+ i 1)))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (v2 i) (v3 (+ i 1))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (v3 i) (v4 (+ i 1))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (v4 i) (v1 (+ i 1))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (v5 i) (v5 (+ i 1))))))
(assert (exists ((i Int)) (=> (>= i 0) (v5 i))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (and (v0 i) (v1 (+ i 1))) (not (v5 (+ i 2)))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (and (v3 i) (v4 (+ i 1)) (v1 (+ i 2))) (not (v5 (+ i 3)))))))
(check-sat)
私が何か間違ったことを書いているのか、それともz3が解決するのが難しい問題なのか疑問に思っています。