Z3 Java API - 获得不满的核心

我试图弄清楚如何使用Java API for Z3获得不饱和核心 . 我们的场景如下（代码在下面，在rise4fun中工作）：

• 我们以编程方式创建SMT2输入

• 输入包含函数定义，数据类型声明和断言

• 我们使用parseSMTLIB2String API解析它

• 我们确保上下文和解算器具有unsat_core - > true

• Z3为提供的输入返回UNSAT，这是正确的

• UNSAT核心总是空着的 .

• 相同的输入在rise4fun（x1 x3）上正确生成UNSAT核心

我猜我错误地使用了API ...但不太确定如何/为什么 .

我注意到我无法在传递给parseSMTLIB2String的SMT字符串中设置不满核心选项，因为这是不允许的 . 我猜这是预料之中的 .

有人能指出我正确的方向吗？

谢谢！！

(set-option :smt.macro-finder true)

;; The following is only for rise4fun, i cannot get it 
;; to work with the parse SMT Java API
(set-option :produce-unsat-cores true)

(define-sort Ref () Int)

(declare-datatypes (T1 T2) ((Tuple2 (mk-Tuple2 (_1 T1)(_2 T2)))))
(declare-datatypes (T1 T2 T3) ((Tuple3 (mk-Tuple3 (_1 T1)(_2 T2)(_3 T3)))))

(define-sort Set (T) (Array T Bool))
(define-sort Bag (T) (Array T Int))

(declare-const emptySetOf_Int (Set Int))
(assert (!(forall ((x Int)) (= (select emptySetOf_Int x) false)) :named AXIOM1))

(declare-sort TopLevelDeclarations) (declare-const mk-TopLevelDeclarations TopLevelDeclarations)
(declare-datatypes () ((A (mk-A (x Int)(y Int)))))

(declare-datatypes () ((Any
  (lift-TopLevelDeclarations (sel-TopLevelDeclarations TopLevelDeclarations))
  (lift-A (sel-A A))
  null))
)

(declare-const heap (Array Ref Any))

(define-fun deref ((ref Ref)) Any
  (select heap ref)
)

(define-fun deref-is-TopLevelDeclarations ((this Ref)) Bool
  (is-lift-TopLevelDeclarations (deref this))
)

(define-fun deref-TopLevelDeclarations ((this Ref)) TopLevelDeclarations
  (sel-TopLevelDeclarations (deref this))
)

(define-fun deref-is-A ((this Ref)) Bool
  (is-lift-A (deref this))
)

(define-fun deref-A ((this Ref)) A
  (sel-A (deref this))
)

(define-fun deref-isa-TopLevelDeclarations ((this Ref)) Bool
  (deref-is-TopLevelDeclarations this)
)

(define-fun deref-isa-A ((this Ref)) Bool
  (deref-is-A this)
)

(define-fun A!x ((this Ref)) Int
  (x (deref-A this))
)

(define-fun A!y ((this Ref)) Int
  (y (deref-A this))
)

(define-fun TopLevelDeclarations.inv ((this Ref)) Bool
  true
)

(assert (! (forall ((this Ref))
  (=> (deref-is-TopLevelDeclarations this) (TopLevelDeclarations.inv this))
) :named x0))

(define-fun A.inv ((this Ref)) Bool
  (and
    (> (A!x this)  0)
    (> (A!y this)  0)
    (< (A!x this)  0)
  )
)

(assert (! (forall ((this Ref))
  (=> (deref-is-A this) (A.inv this))
) :named x1))

(assert (!(deref-is-TopLevelDeclarations 0) :named TOP))
(assert (!(exists ((instanceOfA Ref)) (deref-is-A instanceOfA)) :named x3))

(check-sat)
(get-unsat-core)