-
Notifications
You must be signed in to change notification settings - Fork 179
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
Recursive solver #372
Recursive solver #372
Conversation
cbd30a8
to
248b05c
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK, did a first pass. I didn't read the recursive solver yet, will try to do that next, but I did a sweep over all the other code, which largely seems reasonable.
I added back the commented-out tests and added a few comments as suggested. |
@flodiebold can you rename |
The actual order of the constraints doesn't matter, I think; and the recursive solver puts them into a HashSet, so the order may vary.
… AGAIN)" This reverts commit 66332f8.
…umption ... in the fulfill loop.
The `program_clauses_for_env` function only added elaborated clauses, not the actual clauses from the environment. Instead, both solvers added the clauses afterwards. It seems easier to just add the direct clauses as well.
So if we had some implication A => B, if the solution for A had low priority, we also made B low priority. After some testing, I don't think this is right.
- bring back tests I commented out - add a few comments - add an is_var helper
b3223ff
to
77f262f
Compare
This is getting close to a state where I think it could be merged. Tests are run for both solvers unless otherwise specified.
To do:
Generalize
folder somewhere elseprogram_clauses
instead of usingOption