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

Abstract domain concepts #7

Open
ptal opened this issue Feb 25, 2020 · 0 comments
Open

Abstract domain concepts #7

ptal opened this issue Feb 25, 2020 · 0 comments

Comments

@ptal
Copy link
Owner

ptal commented Feb 25, 2020

Abstract domains have various additional operators depending on their capabilities. For instance, they can be Schedulable or be equipped with projection over vardom. We should find a design in which we do not force an abstract domain to have projection or events, and let Abstract_domain being the minimal interface for satisfiability testing. Abstract transformers could require additional concepts.

I don't really know how to achieve such a design in OCaml with modules and functors. In C++, template and concepts would be used, in Rust it would be traits. Perhaps it requires more advanced functionalities of OCaml such as GADT.

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

No branches or pull requests

1 participant