使用 Z3 从 .smt2 文件获取 UNSAT Core
Get UNSAT Core using Z3 from .smt2 file
我需要从 z3 获取 unsat 核心。 .smt2 文件的内容是：
(set-option :produce-unsat-cores true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
; Constraints
(! (assert (bvslt (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32) ) (concat (select a (_ bv1 32) ) (select a (_ bv0 32) ) ) ) ) (_ bv10 32) ) )
:named ?U0)
(! (assert (bvslt (_ bv10 32) (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32) ) (concat (select a (_ bv1 32) ) (select a (_ bv0 32) ) ) ) ) ) )
:named ?U1)
(check-sat)
(get-unsat-core)
(exit)
当 运行 z3:
unsupported
; !
unsupported
; !
sat
(error "line 11 column 15: unsat core is not available") 时，我得到以下输出
我是 z3 的新手，不明白这里发生了什么（我确定表达式不正确）。
谢谢
您使用 ! 不正确。感叹号用于命名公式（而非断言）。请参阅 Tutorial.
中的第 3.9.8 节
这应该可以修复它：(assert (! (bvslt ...) :named ?U0))。
我需要从 z3 获取 unsat 核心。 .smt2 文件的内容是：
(set-option :produce-unsat-cores true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
; Constraints
(! (assert (bvslt (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32) ) (concat (select a (_ bv1 32) ) (select a (_ bv0 32) ) ) ) ) (_ bv10 32) ) )
:named ?U0)
(! (assert (bvslt (_ bv10 32) (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32) ) (concat (select a (_ bv1 32) ) (select a (_ bv0 32) ) ) ) ) ) )
:named ?U1)
(check-sat)
(get-unsat-core)
(exit)
当 运行 z3:unsupported
; !
unsupported
; !
sat
(error "line 11 column 15: unsat core is not available") 时，我得到以下输出
我是 z3 的新手，不明白这里发生了什么（我确定表达式不正确）。
谢谢
您使用 ! 不正确。感叹号用于命名公式（而非断言）。请参阅 Tutorial.
这应该可以修复它：(assert (! (bvslt ...) :named ?U0))。