在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相矛盾。给出的模型是假的。但你不能为责怪z3，因为它已经告诉你unknown。它超越了Z3的能力来解决你的查询。