(get-unsat-core) Z3: unsat core is not available

1
votes

Here is my program which return SAT when there exists a cycle in the graph and UNSAT when there is no cycle:

(set-option :fixedpoint.engine datalog) 

(define-sort s () Int) 

(declare-rel edge (s s)) 
(declare-rel path (s s)) 

(declare-var a s) 
(declare-var b s) 
(declare-var c s) 

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge 1 2))
(rule (edge 2 3))


(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)

I want to get the model when there is no cycle ( UNSAT ). I realised that i should use the command (get-unsat-core) and set the option to (set-option :produce-unsat-cores true) :

(set-option :fixedpoint.engine datalog) 
(set-option :produce-unsat-cores true)
(define-sort s () Int) 

(declare-rel edge (s s)) 
(declare-rel path (s s)) 

(declare-var a s) 
(declare-var b s) 
(declare-var c s) 

(rule (=> (edge a b) (path a b)) P-1)
(rule (=> (and (path a b) (path b c)) (path a c)) P-2)

(rule (edge 1 2) E-1)
(rule (edge 2 3) E-2)
(rule (edge 3 1) E-3)

(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)


(get-unsat-core)

I get this error:

unsat
(error "line 24 column 15: unsat core is not available")
2
z3proofz3pysatsat-solvers
Try moving the set-option command to the top of the file. Z3 needs to know about this right away; otherwise it will not set up all the datastructures required to track unsat cores, which can be expensive. – Christoph Wintersteiger
I modified the question with your proposal but i still get an error : unsat (error "line 24 column 15: unsat core is not available") – Inzo. Geo

2 Answers

3
votes

Getting a model in the unsat case doesn't make sense. Unsatisfiable literally means there's no model that satisfies your constraints. Please post a more clear question of precisely what you're trying to achieve.

An unsat core is a subset of the assertions that are conflicting. This set is by definition not satisfiable, and does not constitute model as you are seeking. Furthermore, I very much doubt the fixed-point engine supports unsat-cores, so the error message you're getting simply means they are not computed.

2
votes

If I may intrude, AFAIK one needs to name the constraints when one wants to retrieve the unsat core.

The smtlib website provides the following example:

; Getting unsatisfiable cores
(set-option :produce-unsat-cores true)
(set-logic QF_UF)
(declare-const p Bool) (declare-const q Bool) (declare-const r Bool)
(declare-const s Bool) (declare-const t Bool)
(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (=> r s) :named RS))
(assert (! (=> s t) :named ST))
(assert (! (not (=> q s)) :named NQS))
(check-sat)
; unsat
(get-unsat-core)
; (QR RS NQS)
(exit)

As @LeventErkok points out, a model is only available when the formula is sat and the unsat core is only available when the formula is unsat.