search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Context cloning #405

Open degrigis opened 2 years ago

degrigis commented 2 years ago

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!

BrunoDutertre commented 2 years ago

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.

degrigis commented 2 years ago

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.