はZ3で解けません。どうして？

Question

Z3には対応していません。どうして？

私のプログラム：

;x = 2x + 2 (This on Underlaying DB is always increasing as X > Y in DB) 
(declare-const x0 Real) 
(declare-const xn Real) 
(declare-const n Real) 
(push) 
(assert (= x0 42)) 
(assert (= xn (+ (* x0 (^ 2 n)) (* 2 (- (^ 2 n) 1))))) ; recurrence relation 
(assert (> xn 700)) 
(check-sat-using qfnra-nlsat) 
(get-model); to find a satisfiable valuation 
(pop); removes any assertion 


----------------------------- 
Z3 Answer: 
----------------------------- 


unknown 
    (model 
    (define-fun n() Real 0.0) 
    (define-fun xn() Real 42.0) 
    (define-fun x0() Real 42.0) 
    ) 

---

私はまた、整数で試してみました： は、データベース内の値によると 'n' を4として来るべきではないが、それは0

として来てくださいそれを見て誰でも私を助けてください。

Answer 1

unknownは、モデルが「主張されている」、つまり正しいかもしれないし、そうでないかもしれないことを意味する。あなたの問題は非線形項（べき乗）を含んでいるので、これは予想されます。

実際、このモデルでは、xn = 42が示唆されています。これは、プログラム内で仮定xn > 700と矛盾しています。与えられたモデルは偽です。しかし、は、unknownを既に話しているので、それを責めることはできません。クエリを解決するのはZ3の機能を超えています。