haskal
/
rosette
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Compare commits

base: haskal:733863da2fb99823ff33670bd4ef985f2c647fa6
Branches Tags
haskal:xenia/patches
haskal:dependabot/github_actions/actions/checkout-6
haskal:master
haskal:gh-pages
haskal:4.1
haskal:4.0
haskal:3.2
haskal:3.1
haskal:3.0
haskal:assume
haskal:2.2
haskal:v2.1
haskal:v2.0
haskal:v1.1
haskal:objectives
haskal:v1.0
..
compare: haskal:25b2b677cd4abad8a7b11166ae99d6026dfba09a
Branches Tags
haskal:xenia/patches
haskal:dependabot/github_actions/actions/checkout-6
haskal:master
haskal:gh-pages
haskal:4.1
haskal:4.0
haskal:3.2
haskal:3.1
haskal:3.0
haskal:assume
haskal:2.2
haskal:v2.1
haskal:v2.0
haskal:v1.1
haskal:objectives
haskal:v1.0

3 Commits
733863da2f ... 25b2b677cd

Author SHA1 Message Date
xenia 25b2b677cd wip: feat: add support for z3 bit rotate exts 2026-05-31 23:42:41 -04:00
xenia 92d4091567 fix: test regression on newer Z3 
z3 > 4.8.8 will return sign_extend and zero_extend operators in the
model, which were not handled by the smt-lib2 decoder, despite being
handled in the encoder. support for these operators has been added
 2026-05-31 23:41:26 -04:00
xenia 38d467618e fix: always use system Z3 by default 
rosette (for convenience) provides functionality to download and install
a z3 binary during raco installation. unfortunately this package is
currently very out of date, so this commit removes all install-time
functionality, causing rosette to fall back to searching for the z3
binary in the system PATH
 2026-05-31 23:41:19 -04:00
1 changed files with 5 additions and 1 deletions
Show Stats Expand all files Collapse all files

6
rosette/solver/smt/dec.rkt
View File

@ -15,7 +15,7 @@
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
@bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
@z3_ext_rotate_left @z3_ext_rotate_right @z3_ext_rotate_left @z3_ext_rotate_right
@concat @extract)) @concat @extract @sign-extend @zero-extend))
(provide decode-model) (provide decode-model)
@ -132,6 +132,10 @@
(bv n (bitvector len))] (bv n (bitvector len))]
[(list (list (== '_) (== 'extract) i j) s) [(list (list (== '_) (== 'extract) i j) s)
`(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))] `(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))]
[(list (list (== '_) (== 'sign_extend) i) s)
`(, @sign-extend ,(inline i sol ~env) ,(inline s sol ~env))]
[(list (list (== '_) (== 'zero_extend) i) s)
`(, @zero-extend ,(inline i sol ~env) ,(inline s sol ~env))]
[(list (== 'let) binds body) [(list (== 'let) binds body)
(substitute (inline body sol ~env) (substitute (inline body sol ~env)
(for/hash ([id:expr binds]) (for/hash ([id:expr binds])