我正在使用Z3来提取不可满足的配方的不饱和核心.我正在使用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 …