Z3 v1 does not directly expose functionality for unsatisfiable cores.
It is possible to extract unsat cores by using indirect means. The system CAMUS for instance, wraps around Yices to obtain multiple unsat cores withtout requiring direct interface.
We are currently preparing Z3 v2, which does have an interface that allows you to retrieve unsatisfiable subset of assumptions directly.It will be ready in the "near future". In the meanwhile, I suggest to take a look at CAMUS and determine whether this approach is right for you.It should be possible to also use this in conjunction with Z3 v1 and v2.
Hmmm... i'll think about it. i'm running z3 from boogie and i don't know how hard it'll be change it to smt/yices... thanks.
You are interposing a few layers here (your front-end, Boogie, Z3). Boogie interacts with Z3 using the Simplify textual format.Possibly the easiest will be to dump these formulas in the simplify format (using the /proverLog option) and then tranform them into a format such that Z3 v2 can give you cores.
Ok, now I've got a machine with Z3 v2 and a unsat formula but when setting the DISPLAY_UNSAT_CORE flag nothing happens. How do I use this feature?
Best,
Martin
In Z3, the unsat core is generated for assumptions tagged for core extraction. So, if you use the standard SMT format as input, nothing will be displayed in the unsat core because nothing is tagged in the standard format. We have created an extension of the standard SMT format that allows extracting unsatisfiable subsets of assumptions. The format uses the keyword ":assumption*" (instead of ":assumption" to track which assumptions should be tracked.
Example:
(benchmark unsat_core_example :logic QF_AUFLIA :extrapreds ((lt U U)) :extrafuns ((f U U) (g U U) (h U U U) (a U) (b U) (c U) (d U) (e U) (x U) (y U) (f1 bool U U)) :extrapreds ((p U U) (p1) (p2) (p3) (p4) (p5) (p6) (p7) (p8)) :assumption* (or p1 (= a b)) :assumption* (or (not p1) (= a b)) :assumption* (= x b) :assumption* (= y a) :assumption* (or false (= c d)) :assumption* (and (= b c) (= d e)) :assumption* (or p1 p2) :assumption* (or p2 p3) :formula (not (= (f a) (f e))))
z3.exe unsat_core_example.smt DISPLAY_UNSAT_CORE=true
(or p1 (= a b))(or (not p1) (= a b))(= c d)(= b c)(= d e)unsat
The way to get unsat cores over the API is to use the Z3_check_assumptions (in C), Z3.check_assumptions (in OCaml) or CheckAssumptions (in .NET).this function takes as additional arguments an array of assumptions. It returns another array, which is a subset of the input array. The subset are the set of assumptions that are used in the unsat core.