Closed symphorien closed 3 years ago
Pity we need to resort to the more complex recursive approach, but don't really see any way around it...
There any risk of the choiceVar
being unsigned
when the keys to the translation are int
?
There any risk of the choiceVar being unsigned when the keys to the translation are int?
All assignments to choiceVar are visible in the diff, and all of correct type unless I'm mistaken.
Looks much better now, thanks!
I've never introspected what was being stored on the decision nodes. You happy with half of em coming back with 0
as an entry?
That's what's generated with this CNF:
p cnf 4 3
2 0
1 3 0
-1 4 0
Unfortunately, no, I really need all OR nodes to be indexed with a decision variable.
Hrmz...then I think the node merging done during simplification needs to be modified to retain the correct decision node (parent rather than child). Is it fine for having only one reason for determinism? E.g., Or(And(1, 2), And(-1, -2))
could come from branching on either 1 or 2.
One reason is fine by me if it respect priority variables: if 1 is priority and 2 is not, 1 should be retained.
Looks like it's not the merger, but the other places where Or
nodes are created (I've identified 5 spots). Will give it a go over lunch (hour or two).
@symphorien Can you give me push access to your fork? I have a set of changes to push.
Btw, this is what we should be able to generate now (same example as above):
I think I have already ticked the box
Might need to add me as a maintainer on the repo. This is what I'm getting:
$ git push symphorien HEAD:opposing
remote: Permission to symphorien/dsharp.git denied to haz.
fatal: unable to access 'https://github.com/symphorien/dsharp/': The requested URL returned error: 403
I invited you, then :)
Thanks! That seemed to do the trick. How's e76dbc1 look?
It passes my tests, and the diff looks good :)
fixes #9