Мягкие / жесткие ограничения в Z3

Question

Как выразить мягкие и жесткие ограничения в Z3? Я знаю из API, что возможно иметь предположения (мягкие ограничения), но я не могу выразить это при использовании инструмента командной строки. Я звоню, используя z3 /smt2 /si

Answer 1

Допущения доступны в интерфейсе SMT 2.0. Они используются для извлечения неудовлетворительных ядер. Они также могут быть использованы для "отвода" предположений. Обратите внимание, что предположения на самом деле не являются "мягкими ограничениями", но их можно использовать для их реализации. Смотрите пример maxsat (subdir maxsat) в дистрибутиве Z3. Тем не менее, вот пример того, как использовать предположения в интерфейсе 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)