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

Add consequences to solver #302

Open
VadeveSi opened this issue Jul 17, 2024 · 0 comments
Open

Add consequences to solver #302

VadeveSi opened this issue Jul 17, 2024 · 0 comments

Comments

@VadeveSi
Copy link
Contributor

Hi,

I wanted to work towards adding support for Z3's consequences to the Solver. I figure something like

pub fn get_consequence(self,
                       mut assumptions: &[ast::Bool<'ctx>],
                       mut variables: &[ast::Bool<'ctx>]
                       ) -> &[ast::Bool<'ctx>] {
...
}

should work as a high-level wrapper around z3_sys::Z3_solver_get_consequences, but this requires the data to be in a Z3_ast_vector and I'm struggling on how to do that. Do you have any suggestions on how to do this? Am I overlooking something obvious?

Thanks.

VadeveSi added a commit to VadeveSi/z3.rs that referenced this issue Aug 7, 2024
Add consequences, allowing you to derive implied propositions from a set of assumed propositions.
VadeveSi added a commit to VadeveSi/z3.rs that referenced this issue Aug 7, 2024
Add consequences, allowing you to derive implied propositions from a set of assumed propositions.
waywardmonkeys pushed a commit that referenced this issue Aug 11, 2024
Add consequences, allowing you to derive implied propositions from a set of assumed propositions.
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

1 participant