Z3の量子付き関数

Question

私は量子に問題があります。

a（0）= 0とし、a（n + 1）はx（n）の値に基づいてa（n）+1またはa（n）+2のいずれかになります。任意のx（。）とすべてのnについて、a（n）< = n * 2と期待できます。ここで

はZ3のためのコードです：

(declare-fun a (Int) Int) 
(declare-fun x (Int) Int) 
(declare-fun N() Int) 
(assert (forall 
    ((n Int)) 
    (=> (>= n 0) 
     (= (a (+ n 1)) 
      (ite (> (x n) 0) 
      (+ (a n) 1) 
      (+ (a n) 2) 
      ) 
     ) 
    ) 
)) 
(assert (= (a 0) 0)) 
(assert (> (a N) (+ N N))) 

(check-sat) 
(get-model) 

私はそれは常に "タイムアウト" しながら、Z3は、 "UNSAT" を返すことを願っています。 Z3がこの種の量指定子を扱うことができるかどうか、誰かが助言を与えることができるのだろうかと思います。

ありがとうございました。

Answer 1

ありがとう、MalteとNikolaj。 変数Nは境界されるべきである：

(assert (> N 0)) 
(assert (< N 10000)) 

Iは

(assert (and 
(not (> (a N) (+ N N))) 
(> (a (+ N 1)) (+ (+ N 1) (+ N 1))) 
)) 

と

(assert (> (a N) (+ N N))) 

を交換し、それは、（N）の両方の定義のために働きます。 これはあなたが言及した誘導的証拠の一種ですか？ここで

は、2つのコードブロックであり、両者は「UNSAT」を返す：

(declare-fun a (Int) Int) 
(declare-fun x (Int) Int) 
(declare-fun N() Int) 
(assert (forall 
    ((n Int)) 
    (=> (>= n 0) 
     (= (a (+ n 1)) 
     (ite (> (x n) 0) 
     (+ (a n) 1) 
     (+ (a n) 2) 
     ) 
    )) 
)) 
(assert (= (a 0) 0)) 

(assert (> N 0)) 
(assert (< N 10000)) 
;(assert (> (a N) (+ N N))) 
(assert (and 
    (not (> (a N) (+ N N))) 
    (> (a (+ N 1)) (+ (+ N 1) (+ N 1))) 
)) 
(check-sat) 
;(get-model) 

と

(declare-fun x (Int) Int) 
(declare-fun y (Int) Int) 
(declare-fun N() Int) 

(define-fun-rec a ((n Int)) Int 
    (if (> n 0) 
    (if (> (x (- n 1)) 0) (+ (a (- n 1)) 1) (+ (a (- n 1)) 2)) (y n))) 
(assert (= (a 0) 0)) 

(assert (> N 0)) 
(assert (< N 10000)) 
;(assert (> (a N) (+ N N))) 
(assert (and 
    (not (> (a N) (+ N N))) 
    (> (a (+ N 1)) (+ (+ N 1) (+ N 1))) 
)) 
(check-sat) 
;(get-model) 

Answer 2

式はSATであり、N <の場合、aのグラフは指定されていません。 しかし、デフォルトの定量化インスタンス化エンジンはこれを判別できません。あなたは、異なるエンジンを強制するための再帰関数を定義していることを利用できます。

;(declare-fun a (Int) Int) 
(declare-fun x (Int) Int) 
(declare-fun y (Int) Int) 
(declare-fun N() Int) 
(define-fun-rec a ((n Int)) Int 
    (if (> n 0) (if (> (x (- n 1)) 0) (+ (a (- n 1)) 1) (+ (a (- n 1)) 2)) (y n))) 
(assert (= (a 0) 0)) 
(assert (> (a N) (+ N N))) 

(check-sat) 
(get-model) 

Malteが書いているように、このような公式の誘導はサポートされていないため、Z3が誘導プルーフを生成するとは思わない。ホーン節式のクラスで誘導不変量を見つけることはできますが、任意の数式をこの形式に変換する変換が必要です。