Z3中的软/硬约束

Question

如何在Z3中表达软约束和硬约束？我从API中了解到可能有假设(软约束),但在使用命令行工具时我无法表达这一点.我用z3/smt2/si来调用它

Answer 1

SMT 2.0前端提供了一些假设.它们用于提取不可满足的核心.它们也可能用于"收回"假设.请注意,假设并非真正的"软约束",但它们可用于实现它们.请参阅Z3分发中的maxsat示例(subdir maxsat).话虽如此,这里是一个如何在Z3 SMT 2.0前端使用假设的例子.

;; Must enable unsat core generation
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
;; Declare three Boolean constants to "assumptions"
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
;; We assert (=> p C) to track C using p
(declare-const x Int)
(declare-const y Int)
(assert (=> p1 (> x 10)))
;; An Boolean constant may track more than one formula
(assert (=> p1 (> y x)))

(assert (=> p2 (< y 5)))
(assert (=> p3 (> y 0)))

(check-sat p1 p2 p3)
(get-unsat-core) ;; produce core (p1 p2)

(check-sat p1 p3) ;; "retrack" p2
(get-model)