（get

本文介绍了（get-unsat-core）在Z3中返回空的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述

我正在使用Z3提取不满意公式的不饱和核。我正在使用Z3 @ Rise界面（基于Web）编写以下代码，

I am using Z3 to extract the unsat-core of an unsatisfiable formula. I am using Z3@Rise interface (web based) to write the following code,

(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）返回空。我是否缺少某些配置/选项？还是我使示例变得复杂了？

check-sat correctly returns 'unsat' but (get-unsat-core) returns empty. Am I missing some configuration/option? Or have I made the example complicated?

推荐答案

您需要在断言中添加名称标签，以便get-unsat-core具有标签在unsat核心输出中使用。像这样写你的断言：

You need to add name labels to your assertions so get-unsat-core has labels to use in the unsat core output. Write your assertions like this:

(assert (! one :named a1)) (assert (! two :named a2)) (assert (! three :named a3)) (assert (! four :named a4)) (assert (! five :named a5)) (assert (! six :named a6)) (assert (! secondpartA :named spA)) (assert (! secondpartB :named spB))

和get-unsat-core将打印一个unsat核心。

and get-unsat-core will print an unsat core.

此语法的文档可以是在 SMTLIB教程（PDF文件）中找到。

Documentation for this syntax can be found in the SMTLIB tutorial (PDF file).