From c2975b940036dc380929daafc24ee76b66f64edd Mon Sep 17 00:00:00 2001 From: James Bornholt Date: Tue, 22 Mar 2022 21:30:00 -0500 Subject: [PATCH] Fix parsing of SMT-LIB-compliant models SMT-LIB says that models should not start with a 'model symbol, but most SMT solvers have been doing so anyway until recently. So let's just support both variants for the widest compatibility. We had already fixed this specifically for Boolector, but we need to do it everywhere, so this change makes a small refactoring to allow all SMT solvers to share the same model parsing code, while still preserving Boolector-specific fixups to the model after parsing. --- rosette/solver/smt/base-solver.rkt | 61 ++++++++++++++++-------------- rosette/solver/smt/boolector.rkt | 23 ++--------- 2 files changed, 36 insertions(+), 48 deletions(-) diff --git a/rosette/solver/smt/base-solver.rkt b/rosette/solver/smt/base-solver.rkt index ec4947bf..d3a1bd8c 100644 --- a/rosette/solver/smt/base-solver.rkt +++ b/rosette/solver/smt/base-solver.rkt @@ -122,35 +122,40 @@ ; Reads the SMT solution from the server. -; The solution consists of 'sat or 'unsat, followed by -; followed by a suitably formatted s-expression. The -; output of this procedure is a hashtable from constant +; The solution consists of 'sat or 'unsat, followed by +; followed by a suitably formatted s-expression. The +; output of this procedure is a hashtable from constant ; identifiers to their SMTLib values (if the solution is 'sat); ; a non-empty list of assertion identifiers that form an -; unsatisfiable core (if the solution is 'unsat and a -; core was extracted); #f (if the solution is +; unsatisfiable core (if the solution is 'unsat and a +; core was extracted); #f (if the solution is ; 'unsat and no core was extracted); or 'unknown otherwise. (define (read-solution server env #:unsat-core? [unsat-core? #f]) - (decode - (parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols - (match (server-read server (read)) - [(== 'sat) - (server-write server (get-model)) - (let loop () - (match (server-read server (read)) - [(list (== 'objectives) _ ...) (loop)] - [(list (== 'model) def ...) - (for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun))) - (values (cadr d) d))] - [other (error 'read-solution "expected model, given ~a" other)]))] - [(== 'unsat) - (if unsat-core? - (begin - (server-write server (get-unsat-core)) - (match (server-read server (read)) - [(list (? symbol? name) ...) name] - [other (error 'read-solution "expected unsat core, given ~a" other)])) - 'unsat)] - [(== 'unknown) 'unknown] - [other (error 'read-solution "unrecognized solver output: ~a" other)])) - env)) + (decode (parse-solution server #:unsat-core? unsat-core?) env)) + +(define (parse-solution server #:unsat-core? [unsat-core? #f]) + (parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols + (match (server-read server (read)) + [(== 'sat) + (server-write server (get-model)) + (let loop () + (match (server-read server (read)) + [(list (== 'objectives) _ ...) (loop)] + ; The SMT-LIB spec says that a model should be just a list of + ; `define-fun`s, but many SMT solvers used to prefix that list + ; with `model`, so let's support both versions. + ; https://groups.google.com/g/smt-lib/c/5xpcIxdQ8-A/m/X4uQ7dIgAwAJ + [(or (list (== 'model) def ...) (list def ...)) + (for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun))) + (values (cadr d) d))] + [other (error 'read-solution "expected model, given ~a" other)]))] + [(== 'unsat) + (if unsat-core? + (begin + (server-write server (get-unsat-core)) + (match (server-read server (read)) + [(list (? symbol? name) ...) name] + [other (error 'read-solution "expected unsat core, given ~a" other)])) + 'unsat)] + [(== 'unknown) 'unknown] + [other (error 'read-solution "unrecognized solver output: ~a" other)]))) \ No newline at end of file diff --git a/rosette/solver/smt/boolector.rkt b/rosette/solver/smt/boolector.rkt index 064b55dd..566dd37e 100644 --- a/rosette/solver/smt/boolector.rkt +++ b/rosette/solver/smt/boolector.rkt @@ -107,27 +107,10 @@ ; Reads the SMT solution from the server. -; The solution consists of 'sat or 'unsat, followed by -; followed by a suitably formatted s-expression. The -; output of this procedure is a hashtable from constant -; identifiers to their SMTLib values (if the solution is 'sat); -; a non-empty list of assertion identifiers that form an -; unsatisfiable core (if the solution is 'unsat and a -; core was extracted); #f (if the solution is -; 'unsat and no core was extracted); or 'unknown otherwise. +; This is the same as `base/read-solution` except that it applies some fixups +; for quirks in how various versions of Boolector have emitted models. (define (boolector-read-solution server env) - (define raw-model - (parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols - (match (server-read server (read)) - [(== 'sat) - (server-write server (get-model)) - (match (server-read server (read)) - [(list (== 'model) ... (and def (list (== 'define-fun) _ ...)) ...) - (for/hash ([d def]) (values (cadr d) d))] - [other (error 'read-solution "expected model, given ~a" other)])] - [(== 'unsat) 'unsat] - [(== 'unknown) 'unknown] - [other (error 'read-solution "unrecognized solver output: ~a" other)]))) + (define raw-model (base/parse-solution server)) ; First, we need to fix up the model's shadowing of incremental variables (define stripped-raw-model (if (hash? raw-model) (fixup-incremental-names raw-model) raw-model)) ; Now decode in an environment with fake types for UFs