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

QE: Self-substitution #460

Merged
merged 3 commits into from Nov 24, 2017
Merged

QE: Self-substitution #460

merged 3 commits into from Nov 24, 2017

Conversation

marcogario
Copy link
Contributor

Implementation of Self-Substitution as described in
Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi,, "BDD-Based Boolean Functional Synthesis", CAV 2016

@marcogario marcogario added this to the 0.7.5 milestone Nov 19, 2017
Copy link
Contributor

@mikand mikand left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like this a lot!

I was not aware of this paper and it seems a very interesting way of performing Boolean QE! Also, we might consider adding this also in the BDDSolver as an option.

(Not sure why the tests fail on travis, it seems related to the PR of strings, but I do not know why, since this changes have nothing in common to that PR)

@marcogario marcogario self-assigned this Nov 22, 2017
@marcogario
Copy link
Contributor Author

Tests are failing due to mathsat qe. It seems that this additional QE method is triggering the execution of some tests that were typically not executed. Need to investigate further to understand if it is a bug or feature :)

@marcogario marcogario assigned mikand and unassigned marcogario Nov 23, 2017
@mikand mikand merged commit ce526e4 into master Nov 24, 2017
@mikand mikand deleted the self_substitution branch November 24, 2017 08:47
nbailluet pushed a commit to nbailluet/pysmt that referenced this pull request Mar 14, 2024
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

Successfully merging this pull request may close these issues.

None yet

2 participants