Z3またはZ3に渡す前に一貫性のない方程式を検出できますか？

Question

私は次の例でz3で作業していました。

f=Function('f',IntSort(),IntSort()) 
n=Int('n') 
c=Int('c') 
s=Solver() 
s.add(c>=0) 
s.add(f(0)==0) 
s.add(ForAll([n],Implies(n>=0, f(n+1)==f(n)+10/(n-c)))) 

最後の式には一貫性がありません（n=cは不確定になります）。しかし、Z3はこの種の矛盾を検出できません。それを検出するためにZ3を作る方法やそれを検出できる他のツールはありますか？

Answer 1

Z3は、Patrick Trentinが述べたように、SMT-LIBによるゼロ除算の意味は未知の値を返すため、0で除算をチェックしません。

Z3にゼロで除算するかどうかを手動で確認して、0で除算することがないようにすることができます。

をご例えば以下のように、これはなります（これは、あなたがゼロによる除算は、SMT-LIBは異なる意味を持っている言語をモデル化している場合など、重要です）：

(declare-fun f (Int) Int) 

(declare-const c Int) 

(assert (>= c 0)) 

(assert (= (f 0) 0)) 

; check for division by zero 
(push) 
(declare-const n Int) 
(assert (>= n 0)) 

(assert (= (- n c) 0)) 
(check-sat) ; reports sat, meaning division by zero is possible 
(get-model) ; an example model where division by zero would occur 
(pop) 

;; Supposing the check had passed (returned unsat) instead, we could 
;; continue, safely knowing that division by zero could not happen in 
;; the following. 
(assert (forall ((n Int)) 
       (=> (>= n 0) 
        (= (f (+ n 1)) 
         (+ (f n) (/ 10 (- n c))))))) 

Answer 2

私の知る限り、最後の式は、矛盾がSMT-LIB標準のドキュメントと一致していないですあなたの主張ということ。ページTheories: Realsは言う：

SMT-LIBロジックですべての関数記号は合計関数として 解釈されるので、フォーム(/ t 0)の用語は に有意義実数のすべてのインスタンスです。しかし、この宣言は、その値に制限を課すものではない（ ）。

、および 閉じ用語実ソートのtがあります：これは

• すべてのインスタンスの理論Tと
• すべての値v用（値は属性で定義されている）のためにすることを特に意味します(= v (/ t 0))を満たすTのモデル。

同様に、ページTheories: Intsは言う：

をフォーム (/ t 0)の条件についてレアル理論宣言でノートを参照してください。

(div t 0)と (mod t 0)という形式の用語についても同じことが言えます。

したがって、それはSMT-LIB準拠したツールは、これまでに与えられた式のためunsatを印刷しないだろうと信じるように理にかなっています。