yices2 icon indicating copy to clipboard operation
yices2 copied to clipboard

Context cloning

Open degrigis opened this issue 2 years ago • 2 comments

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!

degrigis avatar Aug 16 '22 20:08 degrigis

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.

BrunoDutertre avatar Aug 17 '22 07:08 BrunoDutertre

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.

degrigis avatar Aug 17 '22 16:08 degrigis