CNF - Conjunktive Normal Form
Boolean expression of the form (x|y) & (-a|b|c) & ... a,b,c,x,y are LITERALS There a positive literals (x,y) and negative literals (-a, -b) Terms in parentheses are CLAUSES
Goal: Make the whole expression TRUE
Useful shortcuts:
Id p; /* first literal in rule */ Id d; /* Id offset into 'list of providers */ /* terminated by 0' as used by whatprovides; pool->whatprovides + d */ /* in case of binary rules, d == 0, w1 == p, w2 == other literal */ /* in case of disabled rules: ~d, aka -d - 1 */ Id w1, w2; /* watches, literals not-yet-decided */ /* if !w2, assertion, not rule */ Id n1, n2; /* next rules in linked list, corresponding to w1,w2 */ r->n1 = solv->watches[nsolvables + r->w1]; solv->watches[nsolvables + r->w1] = r - solv->rules; r->n2 = solv->watches[nsolvables + r->w2]; solv->watches[nsolvables + r->w2] = r - solv->rules;
Assertion keepinstalled (A), install p=A, d=0, w1=p, w2=0 uninstallable (-A), remove p=-A, d=0, w1=p, w2=0 Binary rules: (A|B) p=A, d=0, w1=p, w2=B (-A|B) p=-A, d=0, w1=p, w2=B A requires B : !A | provider1(B) | provider2(B) p=-A, d=<whatprovides_offset>, w1=, w2= B updates A : A | provider1(B) | provider2(B) p=A, d=<whatprovides_offset>, w1=, w2= A conflicts B : (!A | !provider1(B)) & (!A | !provider2(B)) ... p=-A, d=-B1, w1=, w2= p=-A, d=-B2, w1=, w2= p=-A, d=-B3, w1=, w2= ... 'not' is encoded as a negative Id Action | p | d | w1 | w2 --------------+----+---------+-------+-------- Assert A | A | 0 | A | 0 Assert -A |-A | 0 |-A | 0 Binary A,B | A | 0 | A | B Binary -A,B |-A | 0 |-A | B A requires B |-A | prov(B) |-A | whatprovidesdata(B) B updates A | A | prov(B) | A | whatprovidesdata(B) A conflicts B |-A | -B |-A |-B addrule(p, d)
/* add rule p = direct literal; always < 0 for installed rpm rules d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only) A requires b, b provided by B1,B2,B3 => (-A|B1|B2|B3) p < 0 : pkg id of A d > 0 : Offset in whatprovidesdata (list of providers of b) A conflicts b, b provided by B1,B2,B3 => (-A|-B1), (-A|-B2), (-A|-B3) p < 0 : pkg id of A d < 0 : Id of solvable (e.g. B1) d == 0: unary rule, assertion => (A) or (-A) Install: p > 0, d = 0 (A) user requested install Remove: p < 0, d = 0 (-A) user requested remove Requires: p < 0, d > 0 (-A|B1|B2|...) d: <list of providers for requirement of p> Updates: p > 0, d > 0 (A|B1|B2|...) d: <list of updates for solvable p> Conflicts: p < 0, d < 0 (-A|-B1),(-A|-B2),... either p (conflict issuer) or d (conflict provider) (binary rule) Obsoletes: p < 0, d < 0 (-A|-B1),(-A|-B2),... A: uninstalled, Bx = provider of obsoletes Learnt: p > 0, d < 0 (A|-B) No-op: p = 0, d = 0 (null) (used as policy rule placeholder) install one of: p =-SYS, d > 0 resulting watches: ------------------ Direct assertion (no watch needed)( if d <0 ) --> d = 0, w1 = p, w2 = 0 Binary rule: p = first literal, d = 0, w2 = second literal, w1 = p every other : w1 = p, w2 = whatprovidesdata[d]; Disabled rule: d < 0, w1 = 0 always returns a rule for non-rpm rules */
enablerule: if (d < 0): d = -d - 1 disablerule if (d >= 0): d = -d - 1
Watches are usually on literals that are not FALSE (either TRUE or UNDEF) Execept: If one watch is on a TRUE (set first), the other can be on a FALSE (set later). This is useful on a backtrack.
Watches 'link' rules involving the same literal Only for n-ary (n >= 2) rules, not for assertions
Watches start at solv->watches[nsolvables]
watches[nsolvables+s] == rule installing s (aka A, B, C,... in CNF clause) watches[nsolvables-s] == rule removing s (aka -A, -B, -C, ... in CNF clause)
'watches trigger when literal goes false'
watches[A] = rule involving A rule->n1 = next rule involving A watches[B] = rule involving B rule->n2 = next rule involving B
This distributes decisions among affected rules and checks that rules evaluate to 'true'.
Since rules are in CNF (conjunctive normal form), it is sufficient for one sub-term (x or y in x|y) to become 'true'.
The interesting case is a 'false' sub-term (x or y in x|y) because this requires the 'other' side to become true.
The pool marks the minimum and maximum Id of installed solvables. There might be other (non-installed) solvables in-between.