Difference in behavior between declare-const + assert and define-fun

[meditans]

Consider this z3 model written in the smt2-lib format (use the latest master to run it because of #2120):

(set-option :produce-models true)

; --------------- Basic Definitions -------------------

(declare-datatype Dummy (A B))

(declare-datatype Formula
  ((Base (forB Dummy))
   (And  (andB1 Formula) (andB2 Formula))
   (Or   (orB1 Formula) (orB2 Formula))
   (Not  (notB Formula))))

(declare-const dummyFormula1 Formula)
(assert (= dummyFormula1 (Base A)))

(declare-const dummyFormula2 Formula)
(assert (= dummyFormula2 (And (Base A) (Base A))))

; --------------- Some functions -----------------------

(define-fun
  in_list ((o Dummy) (l (Seq Dummy))) Bool
  (seq.contains l (seq.unit o)))

(define-fun
  permutation ((l1 (Seq Dummy)) (l2 (Seq Dummy))) Bool
  (forall ((o Dummy)) (= (in_list o l1) (in_list o l2))))

(define-fun-rec unroll ((f Formula)) (Seq Dummy)
  (match f
    (((Base j)    (seq.unit j))
     ((And f1 f2) (seq.++ (unroll f1) (unroll f2)))
     ((Or  f1 f2) (seq.++ (unroll f1) (unroll f2)))
     ((Not f1)    (unroll f1)))))

; -------------- The question -------------------------

;; Here are two versions that should express the same idea, but try commenting
;; the first one and uncommenting the second one!

;; A)

(declare-const flat1 (Seq Dummy))
(assert (= flat1 (unroll dummyFormula1)))

;; B)

; (define-fun flat1 () (Seq Dummy) (unroll dummyFormula1))
; -----------------------------------------------------

(declare-const flat2 (Seq Dummy))
(assert (= flat2 (unroll dummyFormula2)))

(assert (permutation flat1 flat2))

; --------------- Verify -------------------
(check-sat)
(get-model)

I noticed that when I use:

(declare-const flat1 (Seq Dummy))
(assert (= flat1 (unroll dummyFormula1)))

The model is sat, while when I use:

(define-fun flat1 () (Seq Dummy) (unroll dummyFormula1))

the model is reported as unknown. Why is the difference important?

[NikolajBjorner]

Ideally, it shouldn't be different, but the seq solver is not a decision procedure and sometimes has to give up based on how it does proof search.

[meditans]

Do you have any tip on how to avoid getting unknown as the solution? Should I always choose declare-const? More generally, how could I debug how proof search is done?

…

On Thu, 14 Feb 2019, 23:56 Nikolaj Bjorner ***@***.*** wrote: Ideally, it shouldn't be different, but the seq solver is not a decision procedure and sometimes has to give up based on how it does proof search. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#2139 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEbSpfaLE1mO24MkCqIx4wBDC8AVeZE1ks5vNemLgaJpZM4a7vns> .