我正在使用 Z3 来提取无法满足的公式的 unsat-core。我正在使用 Z3@Rise 界面(基于 Web)编写以下代码,
(set-logic QF_LIA)
(set-option :produce-unsat-cores true)
(declare-fun ph1 () Int)
(declare-fun ph1p () Int)
(declare-fun ph3 () Int)
(declare-fun ph3p () Int)
(declare-fun ph4 () Int)
(declare-fun ph4p () Int)
(define-fun one () Bool (= ph3p (+ ph1 1)))
(define-fun two () Bool (= ph3 (+ ph1 1)))
(define-fun three () Bool (= ph1p (+ ph1 1)))
(define-fun four () Bool (= ph4p (+ ph1p 1)))
(define-fun five () Bool (>= ph1 0))
(define-fun six () Bool (>= ph4 0))
(define-fun secondpartA () Bool (or (= ph4 0) (<= ph3 ph4) ))
(define-fun secondpartB () Bool (or (= ph3p 0) (<= ph4p ph3p) ))
(assert one)
(assert two)
(assert three)
(assert four)
(assert five)
(assert six)
(assert secondpartA)
(assert secondpartB)
(check-sat)
(get-unsat-core)
check-sat 正确返回 'unsat' 但 (get-unsat-core) 返回空。我错过了一些配置/选项吗?还是我让这个例子变得复杂了?