Soft/Hard constraints in Z3

Question

How do I express soft and hard constraints in Z3? I know from the API that it is possible to have assumptions (soft constraints), but I can't express this when using the command line tool. I am calling it using z3 /smt2 /si

Answer 1

Assumptions are available in the SMT 2.0 frontend. They are used to extract unsatisfiable cores. They may be also used to “retract” assumptions. Note that, assumptions are not really “soft constraints”, but they can be used to implement them. See the maxsat example (subdir maxsat) in the Z3 distribution. That being said, here is an example on how to use assumptions in the Z3 SMT 2.0 frontend.

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