summaryrefslogtreecommitdiff
path: root/src/parser.mly
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-10-06 16:53:15 +0100
committerAlasdair Armstrong2017-10-06 16:53:15 +0100
commit6e4573f9a1ace7cba38d0cecb95b4dfe95c73c71 (patch)
tree3284c9c20c1c6357894cc950362eec895df4ee36 /src/parser.mly
parent59d7781403f9f92cda4954b75d5116157f98ba84 (diff)
Various improvements to menhir parser, and performance improvments for Z3 calls
New option -memo_z3 memoizes calls to the Z3 solver, and saves these results between calls to sail. This greatly increases the performance of sail when re-checking large specifications by about an order of magnitude. For example: time sail -no_effects prelude.sail aarch64_no_vector.sail real 0m4.391s user 0m0.856s sys 0m0.464s After running with -memo_z3 once, running again gives: time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail real 0m0.457s user 0m0.448s sys 0m0.008s Both the old and the new parser should now have better error messages where the location of the parse error is displayed visually in the error message and highlighted.
Diffstat (limited to 'src/parser.mly')
0 files changed, 0 insertions, 0 deletions