Z3 Java API - get unsat core

Question

I am trying to figure out how to get the unsat core using the Java API for Z3. Our scenario is as follows (code is underneath, which works in rise4fun):

1. We create the SMT2 input programtically
2. The input contains function definitions, datatype declarations, and assertions
3. We parse this using the parseSMTLIB2String API
4. We ensure that the context and the solver have unsat_core -> true
5. Z3 returns UNSAT for the provided input, which is correct
6. The UNSAT core is always empty though.
7. The same input produces an UNSAT core correctly on rise4fun (x1 x3)

I am guessing I am misusing the API somehow... but not quite sure how/why.

I have noticed that I cannot set the unsat core option in the SMT string that I pass to parseSMTLIB2String, because that is not allowed. I am guessing that is expected.

Can someone point me in the right direction please?

Thanks!!

(set-option :smt.macro-finder true)

;; The following is only for rise4fun, i cannot get it 
;; to work with the parse SMT Java API
(set-option :produce-unsat-cores true)

(define-sort Ref () Int)

(declare-datatypes (T1 T2) ((Tuple2 (mk-Tuple2 (_1 T1)(_2 T2)))))
(declare-datatypes (T1 T2 T3) ((Tuple3 (mk-Tuple3 (_1 T1)(_2 T2)(_3 T3)))))

(define-sort Set (T) (Array T Bool))
(define-sort Bag (T) (Array T Int))

(declare-const emptySetOf_Int (Set Int))
(assert (!(forall ((x Int)) (= (select emptySetOf_Int x) false)) :named AXIOM1))

(declare-sort TopLevelDeclarations) (declare-const mk-TopLevelDeclarations TopLevelDeclarations)
(declare-datatypes () ((A (mk-A (x Int)(y Int)))))

(declare-datatypes () ((Any
  (lift-TopLevelDeclarations (sel-TopLevelDeclarations TopLevelDeclarations))
  (lift-A (sel-A A))
  null))
)

(declare-const heap (Array Ref Any))

(define-fun deref ((ref Ref)) Any
  (select heap ref)
)

(define-fun deref-is-TopLevelDeclarations ((this Ref)) Bool
  (is-lift-TopLevelDeclarations (deref this))
)

(define-fun deref-TopLevelDeclarations ((this Ref)) TopLevelDeclarations
  (sel-TopLevelDeclarations (deref this))
)

(define-fun deref-is-A ((this Ref)) Bool
  (is-lift-A (deref this))
)

(define-fun deref-A ((this Ref)) A
  (sel-A (deref this))
)

(define-fun deref-isa-TopLevelDeclarations ((this Ref)) Bool
  (deref-is-TopLevelDeclarations this)
)

(define-fun deref-isa-A ((this Ref)) Bool
  (deref-is-A this)
)

(define-fun A!x ((this Ref)) Int
  (x (deref-A this))
)

(define-fun A!y ((this Ref)) Int
  (y (deref-A this))
)

(define-fun TopLevelDeclarations.inv ((this Ref)) Bool
  true
)

(assert (! (forall ((this Ref))
  (=> (deref-is-TopLevelDeclarations this) (TopLevelDeclarations.inv this))
) :named x0))

(define-fun A.inv ((this Ref)) Bool
  (and
    (> (A!x this)  0)
    (> (A!y this)  0)
    (< (A!x this)  0)
  )
)

(assert (! (forall ((this Ref))
  (=> (deref-is-A this) (A.inv this))
) :named x1))

(assert (!(deref-is-TopLevelDeclarations 0) :named TOP))
(assert (!(exists ((instanceOfA Ref)) (deref-is-A instanceOfA)) :named x3))

(check-sat)
(get-unsat-core)

Answer 1

You're not using the Java API, except for the call to parseSMTLIB2String. This function does not execute any SMT commands and there is no function that would do that for you. parseSMTLIB2String exists exclusively to parse assertions, it will ignore everything else. For this particular problem, I recommend to simply pass the problem file to z3.exe either as a command line argument or via stdin (use -in option). This produces

unsat
(x1 x3)

If the intent is to use the Java API for other things at a later point, see the Java API unsat core example.

Answer 2

I just had the same problem and found that it depends on how you pass the parsed input to the solver.

While the following approach produces an empty unsat-core...:

BoolExpr[] program = context.parseSMTLIB2File(input_file, null, null, null, null);
solver.add(program);
solver.check();
solver.getUnsatCore();

... the unsat-core is produced correctly if you give the parsed input file to the solver as follows:

BoolExpr[] program = context.parseSMTLIB2File(input_file, null, null, null, null);
solver.check(program);
solver.getUnsatCore();

I therefore assume that everything that is passed via solver.add() belongs to the assumptions and therefore presumably does not belong to the unsat-core according to Z3.