(cut off the parts where I agree and there's nothing to add)
On pią, 2017-06-09 at 16:16 +0200, Alexis Ballier wrote:
> [...]
> > > In your example above, we'd call 'nsolve("|| ( X )")' and
> > > 'nsolve("|| ( Y )")' (or even simpler, depending on how simplify()
> > > is defined). If both X and Y are masked on a profile, then that'd
> > > reduce to 'nsolve("False")' which would rant.
> >
> > So you're talking about reducing prior to transforming? Yes, that'd
> > work. As I mentioned in one of the first mails wrt my reference
> > implementation, I've used reordering (stable sort) instead of reducing
> > since it was simpler.
> >
> > If you reduce (simplify), you need to account for special cases like
> > getting '|| ()' etc. If you reorder only, things just fail the normal
> > way.
>
> While the reordering idea seems nice as it factors both user
> preference and masks, the problem with reordering is that nothing
> guarantees that the solver won't try to enable a masked flag. We'd have
> to deal with that somehow.Well, yes and no. The algorithm always needs to account for the possibility of constraints altering immutable flags. Of course, there's more than one way of doing it. AFAIU you are aiming for separate processing of immutable flags and explicit failure if the constraints would attempt to force value of those flags. That surely makes sense for verification. My approach was simpler -- marking the flags immutable, and failing if something actually tries to alter their value. I think it's a simpler solution for the plain solver and it works as well. After all, we do not want the solver to attempt to find workarounds for the problem but just fail. The above applies clearly to the plain conflicts such as: foo? ( bar ) where bar is immutable. The n-ary operators can be flexed a little. That's what reordering achieves -- it makes sure they come as the most or the least preferred as appropriate. Which means that the same algorithm either succeeds (by not having to touch them) or fails at attempting to flip them. Think of: ?? ( a b c ) with both b&c in use.force. This gets reordered to: ?? ( b c a ) The order between b&c doesn't matter. Since b comes first now, it forces c being disabled. Since c is immutable, the solver fails with ImmutabilityError. We solve the problem with minimal code redundancy. > I think reordering should be kept for user preferences > (soft-enable/soft-disable) while masks for hard-no's or hard-yes'es. > > > Be careful with reordering though: > '^^ ( a b ) b? ( a )' can be solved in one pass. > (it disables b if both are set and enables a if none are set) > > while: > '^^ ( b a ) b? ( a )' loops > (if both are set it disables 'a' for the 1st clause but then enables it > for the 2nd) > > This is not checked by nsolve(). Yes, this is a problem I was considering. I planned to think a bit if we could possibly generate some more complex transformations to trigger nsolve to notice this kind of issues. And now two updates on other matters. Firstly, all-of inside ??. Per the construct: ?? ( ( a b ) c ) the expansion would be: [a b]? ( !c ) c? ( ![a b] ) which means we should be able to easily affect the effective behavior of both implementations by defining how to handle/expand negations of all- of groups. It's then a matter of replacing it with: a. !a, or b. !a !b. As you pointed out, a. has the advantage that we alter less flags. b. has the advantage that we alter more flags -- so it's less likely we'll actually leave some unused flag enabled. Whichever we choose, it probably doesn't matter as I can't think of a valid use case for this constraint that would clearly define the result. Secondly, nested n-ary operators. I have taken the following snippet as a simple example: || ( a || ( b c ) ) Logically (and per constraint checking algo), this should be equivalent to: || ( a b c ) However, if we expand it to implication form, we get: ![ || ( b c ) ] => a ![ !c => b ] => a At this point, we already see some contract problem/ambiguity. Per contract, we are supposed not to alter any flags on LHS of implication. However, we have another implication there, so it is unclear if RHS of that nested implication should be mutable or not. Let's consider the nested implication first: !c => b Per the constraint checking rules, this constraint is met (evaluates to true) either if c is enabled, or both c is disabled and b is enabled. In other words, it fails (evaluates to false) only if both b and c are disabled. Putting that into a table we get: b c | ? 0 0 | 0 (fail -- LHS matches, RHS does not) 0 1 | 1 (LHS does not match) 1 0 | 1 (LHS & RHS matches) 1 1 | 1 (LHS does not match) Per the solving rules, in the only failing case we should enforce RHS -- i.e. enable b. Now, let's consider its negation: ![ !c => b ] Per the rules of logic, it is true (= matches the constraint) only if both b and c are disabled. While it is unclear if we should be enforcing RHS inside negation, logically saying I don't think it can actually happen. Because: 1. if b=c=0, the whole negated constraint is satisfied, so we shouldn't apply any solving to it (attempting to solve it would be inconsistent with the case where whole REQUIRED_USE is satisfied immediately), 2. in any other case, the inner constraint is satisfied, so there's no change to be applied. That considered, I think we could reasonably replace the negation of implication with plain conjunction of LHS and negation of RHS: [ !c !b ] This would render the outer expression as: [ !c !b ] => a which is equivalent to || ( a b c ). The question is whether applying that rule for implications nested on LHS of another implication is going to work fine for all our expansions. -- Best regards, Michał Górny
signature.asc
Description: This is a digitally signed message part
