（get-unsat-core）Z3：不可用核心

Question

这是我的程序，当图中存在循环时返回SAT，当没有循环时返回UNSAT：

(set-option :fixedpoint.engine datalog) 

(define-sort s () Int) 

(declare-rel edge (s s)) 
(declare-rel path (s s)) 

(declare-var a s) 
(declare-var b s) 
(declare-var c s) 

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge 1 2))
(rule (edge 2 3))


(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)

我希望在没有循环时获得模型（UNSAT）。我意识到我应该使用命令（get-unsat-core）并将选项设置为（set-option：produce-unsat-cores true）：

(set-option :fixedpoint.engine datalog) 
(set-option :produce-unsat-cores true)
(define-sort s () Int) 

(declare-rel edge (s s)) 
(declare-rel path (s s)) 

(declare-var a s) 
(declare-var b s) 
(declare-var c s) 

(rule (=> (edge a b) (path a b)) P-1)
(rule (=> (and (path a b) (path b c)) (path a c)) P-2)

(rule (edge 1 2) E-1)
(rule (edge 2 3) E-2)
(rule (edge 3 1) E-3)

(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)


(get-unsat-core)

我收到此错误：

unsat
(error "line 24 column 15: unsat core is not available")

Answer 1

在unsat案例中获取模型没有意义。不满意的字面意思是没有满足你的约束的模型。请发一个更清楚的问题，确切地说是你想要实现的目标。

不饱和核心是冲突的断言的子集。根据定义，这个集合是不可满足的，并不构成您所寻求的模型。此外，我非常怀疑定点引擎支持不满核心，所以你得到的错误信息只是意味着它们没有计算。

Answer 2

如果我可能会介入，AFAIK需要在想要检索unsat core时命名约束。

smtlib网站提供以下示例：

; Getting unsatisfiable cores
(set-option :produce-unsat-cores true)
(set-logic QF_UF)
(declare-const p Bool) (declare-const q Bool) (declare-const r Bool)
(declare-const s Bool) (declare-const t Bool)
(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (=> r s) :named RS))
(assert (! (=> s t) :named ST))
(assert (! (not (=> q s)) :named NQS))
(check-sat)
; unsat
(get-unsat-core)
; (QR RS NQS)
(exit)

正如@LeventErkok指出的那样，只有当公式为sat时才能使用模型，而当公式为unsat core时，unsat才可用。