On śro, 2017-06-07 at 10:17 +0200, Alexis Ballier wrote: > > Also, do I presume correctly that for all supported cases (i.e. those > > which your nsolve does not reject), solve and nsolve are compatible? > > > > Not sure what you mean here. nsolve does not solve anything, it just > validates REQUIRED_USE so that it is guaranteed it can be solved.
What I mean is whether you can guarantee that: a. for every X that nsolve(X) == ok, solve() will be able to find a valid solution, b. for every X that solve() can solve reliably, nsolve(X) == ok. > We first need to define properly & formally how to solve requse > constraints if we want ppl to be able to rely on it (or rather write > requse that give the expected result). > > The way I see it, REQUIRED_USE ast looks like: > (assuming ^^ is already expanded to || + ??) > > clause = > AllOf(list of clauses) > | AnyOf(list of clauses) > | AtMostOne(list of clauses) > | Implication(useflag, clause) > | useflag > > Now, portage already has the function 'eval(input, clause)'. We need to > define 'trueify(input, clause)' that modifies input so that 'eval(input, > clause)' is always true afterwards. Since this is SAT, there is no > hope to make this work for all clauses. From the discussions here, a > good algorithm would be: > > trueify(input, clause) = match clause with > AllOf(l) -> for i in l: trueify(input, i) > > AnyOf(l) -> if not eval(input, clause): trueify(input, l[0]) > > AtMostOne(l) -> f = (lambda x,y: pass) > > for i in l: > f(input, i) > if eval(input, i): f = falsify > > Implication(useflag, consequence) -> > > if input[useflag]: trueify(input, consequence) > > useflag -> input[useflag] = True > > > Now you see that for the AtMostOne case we need its dual, the > 'falsify(input, clause)' function: > > falsify(input, clause) = match clause with > AllOf(l) -> falsify(input, l[0]) That's a debatable case. My solve() actually 'falsifies' all the subexpressions which might be more reliable. > > AnyOf(l) -> for i in l: falsify(input, i) > > AtMostOne(l) -> for i in l: > > if eval(input, clause): trueify(input, i) Do I read this correctly that it pretty much implies enabling the first two subexpressions? > > Implication(useflag, consequence) -> > > if not input[useflag]: raise "impossible" Why impossible? Unless I'm missing something, it's false already. > else: falsify(input, consequence) > > useflag -> input[useflag] = False Looks mostly sane. You've missed '!flag' but that's trivial to add. > > Note how the above favors leftmost in all cases. If it needs to change > something, it always tries to leave the leftmost untouched. Note also > that it processes everything left to right (the AllOf case where > REQUIRED_USE="AllOf(list of clauses)" ). You need to be able to reorder the clauses to handle use.force and use.mask. > So, the very first thing to do is to agree that the above solver > (the trueify function) is what we want to implement and set this in > stone. There's no point in implementing a proper requse checker if the > algorithm is meant to change. Having a formal definition will also be > necessary to mandate that in future EAPIs. > > Then, and only then, we'd need to have the above solver implemented into > portage (hidden under a FEATURES) and import my nsolve into repoman > (after due cleanup). > Yes, that's my goal. However, before we can set the algorithm in stone we need to verify that it will work in all of the supported cases. Preferably it should also be as simple as possible to avoid putting too much complexity in the spec. -- Best regards, Michał Górny
signature.asc
Description: This is a digitally signed message part
