search

formalsec / smtml

A frontend for multiple SMT solvers in OCaml
https://formalsec.github.io/smtml/smtml/
MIT License
27 stars 8 forks source link

Caches consts #221

Closed filipeom closed 2 months ago

filipeom commented 2 months ago 
Adds `caches_consts` flag to mappings

Solvers can inform us that they cache constants by setting the flag
`caches_consts = true` in their mappings. This should avoid having a
`Map.find_opt` everytime we call `make_symbol`.

Currently the mappings that behave like this are only Z3
filipeom commented 2 months ago

@joaomhmpereira I've set cvc5's caches_const=true so this should solve some performance issues?

EDIT: I reverted it as it was not passing the CI.

filipeom commented 2 months ago

Queueing to merge. We can set cvc5's caches_const to true in another PR