Z3はこのプログラムを検証できるはずですか？

Question

私はZ3の初心者です。最近、いくつかの問題を確認するためにz3を使用しています。ここに私が試した一つの問題である：（X & Y < 0）は含意X/Y> = 0、以下、私が書いたプログラムは、次のとおり

(declare-const x Int) 
(declare-const y Int) 
(define-fun assumption() Bool 
    (and (< x 0) (< y 0)) 
) 

(define-fun predicate() Bool 
    (<= 0 (div x y)) 
) 

(assert (not (=> assumption predicate))) 

(check-sat) 

私は確認する 'Z3 -smt2ファイル名' を使用このプログラムは、動作し、unsatを返します。 （ - 1 *のy）と何らかの形で私は追加する必要があり、私は（-1 * X）/に 'X/Y' に変更するときにタイムアウトするこの原因Z3

(declare-const x Int) 
(declare-const y Int) 
(define-fun assumption() Bool 
    (and (< x 0) (< y 0)) 
) 

(define-fun predicate() Bool 
    (<= 0 (div (* -1 x) (* -1 y))) 
) 

(assert (not (=> assumption predicate))) 

(check-sat) 

：しかし、ときに私は後にプログラムを修正しますそこに-1。私はなぜこれが起こったのか、なぜ定数を乗じたのがこの問題をより複雑にするのか混乱しています。

誰かがこれがなぜ起こったのか理解するのに役立つことができますか？

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

Answer 1

除数が変数である除算など、非線形演算のサポートは非​​常に限られています。 Z3は最善を尽くしますが、決してすべての数式について非線形算術演算で決定することは決してできません。たとえば、ディオファンタス方程式をZ3に入力することはできますが、座っている/しゃべらない答えを提供するとは思いません。 Z3は無限の検索を試みるのではなく、あきらめて不明を返すことを好みます。

Answer 2

（注：これはちょうどコメントの代わりに、答えは私がそうしなければならない、私はコメントを追加するのに十分な評判を持っていないため）

ここでは、整数の除算についてZ3 guideからの引用ですモジュロおよびリマインダー演算子：

Z3には、除算、整数除算、モジュロおよび剰余演算子もサポートされています。内部的には、すべて乗算にマップされます。 Z3で

(declare-const a Int) 
(declare-const r1 Int) 
(declare-const r2 Int) 
(declare-const r3 Int) 
(declare-const r4 Int) 
(declare-const r5 Int) 
(declare-const r6 Int) 
(assert (= a 10)) 
(assert (= r1 (div a 4))) ; integer division 
(assert (= r2 (mod a 4))) ; mod 
(assert (= r3 (rem a 4))) ; remainder 
(assert (= r4 (div a (- 4)))) ; integer division 
(assert (= r5 (mod a (- 4)))) ; mod 
(assert (= r6 (rem a (- 4)))) ; remainder 
(declare-const b Real) 
(declare-const c Real) 
(assert (>= b (/ c 3.0))) 
(assert (>= c 20.0)) 
(check-sat) 
(get-model) 

、ゼロによる除算は許可されるが、結果が指定されていません。除算は部分的な関数ではありません。実際には、Z3ではすべての関数が合計ですが、ゼロによる除算のような場合には結果が不明瞭になることがあります。

引数が負の場合の動作は不明です。換言すれば、これらの演算に対する乗算へのマッピングは明確ではない。