fix OR node choice variables

[symphorien]

• choice variables are variables (unsigned) not literals (signed)
• remove conditional in NNF code that becomes redundant based on the
  above
• fix that literals are translated but not choice variables, which could lead to
  wrong OR node labeling

fixes #9

[haz]

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?

[symphorien]

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.

[haz]

It's this line I'm concerned with. varTranslation comes in as vector<int>, and while the other instances are int, this one comes in as unsigned.

[symphorien]

Oh indeed ! I had missed this one !
I went all the way and fixed the translation vector to contain unsigned values. i'm fairly confident that it's correct because I can compile sucessfully with -Wsign-promo -Wsign-conversion -Wsign-compare -Werror

[haz]

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

[symphorien]

Unfortunately, no, I really need all OR nodes to be indexed with a decision variable.

[haz]

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.

[symphorien]

One reason is fine by me if it respect priority variables: if 1 is priority and 2 is not, 1 should be retained.

[haz]

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).

[haz]

@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):

[symphorien]

I think I have already ticked the box

[haz]

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

[symphorien]

I invited you, then :)

[haz]

Thanks! That seemed to do the trick. How's e76dbc1 look?

[symphorien]

It passes my tests, and the diff looks good :)