yices2
yices2 copied to clipboard
Context cloning
In reference to the issue opened here, would it be feasible to implement an API to FULLY clone a Context
? (e.g., no need to re-assert formulas from scratch, etc...)
Ideally, there would be a function init_context_from(ctx, ctx_source,...)
that would return a new independent ctx
using ctx_source
. This would be enormously helpful to build scalable symbolic executors on top of Yices2.
(Sorry for the re-posting, after a discussion with @ianamason I thought this issue belonged here more than in the python bindings repo)
Thanks!
That sounds like a reasonable feature but that may take a while to implement. We'd have to go through all our data structures and implement a clone method for them.
We would be willing to help in the quest tho if you think this can be implemented in a reasonable time. If nothing, I really think this would definitely push the adoption of Yices2 among other communities.