Soft / hard restrictions in Z3

Question

How to express soft and hard restrictions in Z3? I know from the API that assumptions are possible (soft restrictions), but I cannot express this when using the command line tool. I call it with z3 / smt2 / si

Answer 1

Assumptions are available in the SMT 2.0 interface. They are used to extract unsatisfactory nuclei. They can also be used to “reverse” assumptions. Note that assumptions are not really “soft constraints”, but they can be used to implement them. See the example maxsat (subdir maxsat) in the Z3 distribution. Here is an example of how to use assumptions in the Z3 SMT 2.0 interface.

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