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.
vcanumalla · Mar 23, 2022 · c2975b9 · c2975b9
1 parent 1017855
commit c2975b9
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 48 deletions.
diff --git 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)])))
diff --git 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