From 546328f8773abd09a2405773df51c35daf388144 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 13 Sep 2023 11:59:29 -0700 Subject: [PATCH] Cut out extra stuff from bitwuzla.rkt --- rosette/solver/smt/bitwuzla.rkt | 123 +------------------------------- 1 file changed, 2 insertions(+), 121 deletions(-) diff --git a/rosette/solver/smt/bitwuzla.rkt b/rosette/solver/smt/bitwuzla.rkt index b7cdb8be..63aff6dd 100644 --- a/rosette/solver/smt/bitwuzla.rkt +++ b/rosette/solver/smt/bitwuzla.rkt @@ -65,8 +65,8 @@ (define (solver-pop self [k 1]) (base/solver-pop self k)) - (define (solver-check self) - (base/solver-check self bitwuzla-read-solution)) + (define (solver-check self [read-solution base/read-solution]) + (base/solver-check self read-solution)) (define (solver-debug self) (base/solver-debug self))]) @@ -104,122 +104,3 @@ [else (unless (or (boolean? v) (bv? v)) (error 'bitwuzla "bitwuzla does not support value (expected boolean? or bv?): ~v" v))]))) - - -; Reads the SMT solution from the server. -; This is the same as `base/read-solution` except that it applies some fixups -; for quirks in how various versions of bitwuzla have emitted models. -(define (bitwuzla-read-solution server env) - (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 - (define m (decode stripped-raw-model (fake-env-types env))) - ; Finally, fix up the decoded model with the right types - (fixup-model m)) - - -; bitwuzla adds a prefix to constant names in incremental mode, -; and repeats bindings for the same constant at different levels. -; For example: -; (model -; (define-fun BTOR@5c10 () (_ BitVec 1) #b1) -; (define-fun BTOR@5c11 () (_ BitVec 1) #b0) -; (define-fun BTOR@5c13 () (_ BitVec 1) #b1) -; (define-fun BTOR@6c10 () (_ BitVec 1) #b0) -; (define-fun BTOR@7c12 () (_ BitVec 1) #b1) -; (define-fun BTOR@8c13 () (_ BitVec 1) #b0)) -; For each constant, we need to choose the binding with the highest such level, -; and then strip the prefix so the names match their actual definitions. -; There are two different styles of prefix, "BTOR@0x" or "BTOR_0@x", depending -; on the version of bitwuzla (where 0 is the level and x the original name). -(define (strip-BTOR@-prefix-from-define-fun v) - (match v - [(list (== 'define-fun) id params ret body) - `(define-fun ,(regexp-replace #rx"^BTOR((@[0-9]+)|(_[0-9]+@))c" (symbol->string id) "c") ,params ,ret ,body)] - [_ v])) -(define (BTOR@-level k) - (let ([match (regexp-match #rx"^BTOR@([0-9]+)(c.*)$" (symbol->string k))]) - (if match - (values (string->number (second match)) (string->symbol (third match))) - (let ([match (regexp-match #rx"^BTOR_([0-9]+)@(c.*)$" (symbol->string k))]) - (if match - (values (string->number (second match)) (string->symbol (third match))) - (values 0 k)))))) -(define (fixup-incremental-names raw-model) - (define leveled - (for/fold ([ret (hash)]) ([(k v) raw-model]) - (define-values (l id) (BTOR@-level k)) - (if (> l (car (hash-ref ret id '(-1 -1)))) - (hash-set ret id (cons l (strip-BTOR@-prefix-from-define-fun v))) - ret))) - (for/hash ([(k l/v) leveled]) - (values k (cdr l/v)))) - - -; bitwuzla sometimes interprets booleans as 1-bit bitvectors. -; We need to temporarily make this same transformation in the types -; in an environment before passing it to `decode`, so that decoded -; uninterpreted functions perform the right type casts and checks -; (i.e., they check their inputs are 1-bit BVs instead of booleans). -; Then, once the model has been decoded, we need to undo this transformation, -; so that the final model matches its expected Rosette types. -; More recent versions of bitwuzla removed this transformation for arity-0 -; booleans, but kept it for higher arities (i.e., uninterpreted functions). - -; A fake-function? proxies an original function?, -; but with all booleans in the original function's type -; replaced with 1-bit bitvectors. -(struct fake-function function (original) #:transparent) - -; Rewrite an env to replace all constant declarations of type function? -; to equivalent fake-function?s that replace booleans with 1-bit bitvectors. -(define (fake-env-types env) - (with-terms ; don't pollute the cache with fake constants - (for/hash ([(decl id) (in-dict env)]) - (values - (match decl - [(constant val (function domain range)) - (if (or (member @boolean? domain) (eq? @boolean? range)) - (constant (gensym) - (fake-function (for/list ([a (in-list domain)]) - (if (eq? @boolean? a) (bitvector 1) a)) - (if (eq? @boolean? range) (bitvector 1) range) - decl)) - decl)] - [_ decl]) - id)))) - -; Replace all values with type fake-function? in a model with their -; original types, wrapping their procedures in a cast from booleans to -; 1-bit bitvectors where necessary. -(define bv1 (bitvector 1)) -(define (fixup-model m) - (match m - [(model dict) - (sat (for/hash ([(var val) (in-dict dict)]) - (match (type-of var) - [(== @boolean?) - (values var (if (bv? val) - (not (= (bv-value val) 0)) - val))] - [(fake-function fake-domain fake-range original) - (match-define (function orig-domain orig-range) (type-of original)) - (match val - [(fv type) - (define inner - (lambda args - (apply val - (for/list ([a (in-list args)] - [ot (in-list orig-domain)] - [ft (in-list fake-domain)]) - (if (and (eq? ot @boolean?) (eq? ft bv1)) - (@if a (bv 1 1) (bv 0 1)) - a))))) - (define outer - (if (and (eq? orig-range @boolean?) (eq? fake-range bv1)) - (lambda args (@bveq (apply inner args) (bv 1 1))) - inner)) - (values original (fv (type-of original) outer))])] - [_ (values var val)])))] - [_ m]))