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)