将非线性实数与线性实数相结合

我读过关于非线性算术和未解释函数的文章。我对SMT世界还很陌生，所以如果我没有使用正确的词汇或者这是一个糟糕的问题，我很抱歉。将非线性实数与线性实数相结合

对于下面的代码，在无关顶层断言(assert (> i 10))上面存在置于堆栈上的断言。但是，Z3对于Reals（第一次推到第一次弹出）的情况返回不起作用。我认为这与Z3尝试使用Int求解器有关，因为第一个断言是在Int上的，而Z3将e1分配给(/ 1.0 2.0)，这是一个没有Int表示的数字，因为约束条件为(assert (< e3 1))（如果我删除了这个约束，它的工作原理）。使用(check-sat-using qfnra-nlsat)解决了Reals的问题，但对于Ints的情况返回unknown，但是仍然可以获得满足约束条件的Int案例的模型。

(set-option :global-decls false) 

(declare-const i Int) 
(assert (> i 10)) 

(push) 
    (declare-const e1 Real) 
    (declare-const e2 Real) 

    (define-fun e3() Real (/ e1 e2)) 
    (assert (> e1 0)) 
    (assert (> e2 0)) 
    (assert (< e3 1)) 

    ;(check-sat-using qfnra-nlsat) 
    (check-sat) 
(pop) 
(push) 
    (declare-const e1 Int) 
    (declare-const e2 Int) 

    (define-fun e3() Int (div e1 e2)) 
    (assert (> e2 0)) 
    (assert (> e3 0)) 

    ;(check-sat-using qfnra-nlsat) 
    (check-sat) 
(pop)

有一个调用来检查，我可以在任何情况下使用，否则我将需要使用(check-sat-using ...)取决于被断言的类型？

来源

2013-10-29 corbin

既然你是混合真正的和整数的种类，我想你需要使用check-sat-using。 “对于非线性整数问题，非线性实数算术（NLSat）求解器默认不使用，它对整数问题通常是无效的，但是我们可以迫使Z3甚至在整数问题中使用NLSat。”

您正迫使Z3使用非线性实数算术求解器对整数约束与(check-sat-using qfnra-nlsat)。这也是如何与z3py做在Python：z3 fails with this system of equations

我在将来的某个时候想象（虽然开发者可以证实），你就不必这样做，但我最后听到的（参见例如mixing reals and bit-vectors和Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5 ），非线性实数算术求解器策略还没有与其他求解器完全整合。

来源

2013-10-29 15:19:28 Taylor

谢谢，泰勒。我不幸没有代表upvote你:( – corbin

将非线性实数与线性实数相结合

回答

相关问题