我读过有关非线性算法和未解释函数的帖子 . 我对SMT世界还很陌生，如果我没有使用正确的词汇，那么道歉，或者这是一个糟糕的问题 .
对于以下代码，有一些断言放在堆栈上面一个不相关的顶级断言 (assert (> i 10)) . 但是，对于Reals的情况，Z3返回不满（第一次推送到第一个pop） . 我认为这与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 ...) ，具体取决于所声明的类型？
1 回答
由于您正在混合实数和整数排序，我认为您需要使用
check-sat-using. 来自How does Z3 handle non-linear integer arithmetic?：“对于非线性整数问题，默认情况下不使用非线性实数算术（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），非线性真实算术求解器策略并未完全与其他求解器集成然而 .