Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Context cloning #405

Open
degrigis opened this issue Aug 16, 2022 · 2 comments
Open

Context cloning #405

degrigis opened this issue Aug 16, 2022 · 2 comments

Comments

@degrigis
Copy link

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
Copy link
Member

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
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants