Wrong order in models

[Halbaroth]

It seems we do not print definitions in models in the same order of the corresponding declarations in the input file. For instance, the following input:

(set-option :produce-models true)
(set-logic ALL)
(declare-const r (_ BitVec 8))
(declare-const l (_ BitVec 8))
(declare-const m (_ BitVec 8))
(assert (bvule l r))
(assert (= m (bvudiv (bvadd l r) (_ bv2 8))))
(assert (not (and (bvule l m) (bvule m r))))
(check-sat)
(get-model)

gives

unknown
(
  (define-fun m () (_ BitVec 8) #x00)
  (define-fun r () (_ BitVec 8) #xff)
  (define-fun l () (_ BitVec 8) #x01)
) 

I believe that the appropriate fix consists in using term_cst of Dolmen instead of Id.t to store profiles. I tried to write the fix but it requires a lot of annoying workarounds because of the legacy frontend. I postpone the fix for the next release after getting rid of the legacy frontend.

[Gbury]

There has been some discussions about order of definitions in models, and it is still ongoing (see https://github.com/SMT-LIB/SMT-LIB-2/issues/26).

For what it's worth, even though keeping the same order as the original problem is optimal in my opinion (basically, it helps with performance of checking the model), as long as the model is at least in topological order (i.e. constants are defined before being used), dolmen will be happy.

[Halbaroth]

Thanks for the clarification. I thought it was unspecified by the SMT-LIB standard (and it seems it is unclear according to your issue) but I believe that it is better for readability too.

[bclement-ocp]

as long as the model is at least in topological order (i.e. constants are defined before being used), dolmen will be happy.

That is not the case currently (see embedded-array), but I'd say this is a bug, probably related to #1213.

Edit: to clarify, when I say "this is a bug" I mean that we should refer to the abstract constant (as @a2 S) in the definition of x, not to s.