Z3 Java API - 获得 unsat 核心 [英] Z3 Java API - get unsat core

问题描述

我想弄清楚如何使用 Z3 的 Java API 获取 unsat 核心.我们的场景如下(代码在下面，在rise4fun中有效):

I am trying to figure out how to get the unsat core using the Java API for Z3. Our scenario is as follows (code is underneath, which works in rise4fun):

1. 我们以编程方式创建 SMT2 输入
2. 输入包含函数定义、数据类型声明和断言
3. 我们使用 parseSMTLIB2String API 解析它
4. 我们确保上下文和求解器具有 unsat_core -> true
5. Z3 为提供的输入返回 UNSAT，这是正确的
6. 不过，UNSAT 核心始终是空的.
7. 相同的输入在rise4fun (x1 x3) 上正确生成 UNSAT 核心

我猜我以某种方式滥用了 API...但不太确定如何/为什么.

I am guessing I am misusing the API somehow... but not quite sure how/why.

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

I have noticed that I cannot set the unsat core option in the SMT string that I pass to parseSMTLIB2String, because that is not allowed. I am guessing that is expected.

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

Can someone point me in the right direction please?

谢谢！！

(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)

推荐答案

您没有使用 Java API，除了对 parseSMTLIB2String 的调用.此函数不执行任何 SMT 命令，并且没有任何函数可以为您执行此操作.parseSMTLIB2String 专门用于解析断言，它将忽略其他所有内容.对于这个特定问题，我建议将问题文件作为命令行参数或通过标准输入(使用 -in 选项)简单地传递给 z3.exe.这会产生

You're not using the Java API, except for the call to parseSMTLIB2String. This function does not execute any SMT commands and there is no function that would do that for you. parseSMTLIB2String exists exclusively to parse assertions, it will ignore everything else. For this particular problem, I recommend to simply pass the problem file to z3.exe either as a command line argument or via stdin (use -in option). This produces

unsat
(x1 x3)

如果以后打算将 Java API 用于其他用途，请参阅 Java API unsat 核心示例.

If the intent is to use the Java API for other things at a later point, see the Java API unsat core example.

这篇关于Z3 Java API - 获得 unsat 核心的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！