search

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
638 stars 74 forks source link

The result of a get-model command should be compatible with SMT-LIB standard #222

Closed chansey97 closed 2 years ago

chansey97 commented 2 years ago

According to SMT-LIB standard, the answer to (get-model) should just be a list of (define-fun...) commands, e.g.

(get-model)
((define-fun x () Int 0) 
 (define-fun y () Int 1))

However, currently many solvers (e.g. z3-4.8.7) adds additional model keyword in the answer:

(get-model)
(model 
 (define-fun x () Int 0)
 (define-fun y () Int 1))

This issue has been fixed in the latest version of z3 (e.g. z3-4.8.12). but rosette code has not be updated (so cannot run normally in z3-4.8.12).

This patch supports both two formats.

More details see https://groups.google.com/g/smt-lib/c/5xpcIxdQ8-A/m/X4uQ7dIgAwAJ

jamesbornholt commented 2 years ago

Thanks! It turns out we had already fixed this for Boolector in #206, but we needed to do it for all solvers. So I'm going to fix this a slightly different way with #223, which refactors our model parsing a little so that all solvers share the same parsing code.

However, I suggest not using the latest Z3 with Rosette just yet. There is a performance issue (https://github.com/Z3Prover/z3/issues/5917) that makes model parsing either not work at all or be prohibitively expensive for larger problems. Hopefully we can either get that fixed or work around it soon, but in the meantime, I suggest sticking with the version Rosette ships with.