Commit c64255db authored by Karel Koci's avatar Karel Koci 🤘

Describe dependencies in planner using equivalency

Using only implication is problematic if we add negation to chain. In
such case its meaning isn't that it implies negative value, but that it
doesn't imply. That is problem if we use use negative dependencies. New
approach uses equivalency instead of implications. We used equivalency
originally because formulas added to sat solver as dependencies of one
package would introduced limitation on package even if original package
isn't selected and that is wrong. Now instead of that we use formulas
activators. It's variable that ensures that if it isn't set than
formula is always true. Activator is package group or candidate for
which given dependency is build. This way we are able to ignore
dependency formulas that don't have to be activated because we don't
choose that package.
parent d9d41819
......@@ -79,17 +79,20 @@ function candidates_choose(candidates, pkg_name, version, repository)
end
-- Adds penalty variable for given var.
function sat_penalize(state, var, penalty_group, lastpen)
function sat_penalize(state, activator, var, penalty_group, lastpen)
if not lastpen then
return 0 -- skip first one, it isn't penalized.
end
if not activator then
activator = state.sat.v_true -- if no activator given than it should be always active
end
local penalty = state.sat:var()
TRACE("SAT add penalty variable " .. tostring(penalty) .. " for variable " .. tostring(var))
-- penalty => not pen
state.sat:clause(-penalty, -var)
state.sat:clause(-activator, -penalty, -var)
if lastpen ~= 0 then
-- previous penalty variable implies this one
state.sat:clause(-lastpen, penalty)
state.sat:clause(-activator, -lastpen, penalty)
end
table.insert(penalty_group, penalty)
return penalty
......@@ -129,7 +132,7 @@ function sat_pkg_group(state, name)
end
table.insert(sat_candidates_exclusive, cand)
end
lastpen = sat_penalize(state, cand, state.penalty_candidates, lastpen) -- penalize candidates
lastpen = sat_penalize(state, nil, cand, state.penalty_candidates, lastpen) -- penalize candidates
table.insert(sat_candidates, cand)
end
-- We solve dependency afterward to ensure that even when they are cyclic, we won't encounter package group in sat that don't have its candidates in sat yet.
......@@ -140,7 +143,7 @@ function sat_pkg_group(state, name)
sat_pkg_group(state, candidates[i].Package) -- Ensure that candidate's package is also added
-- Note: not processing dependencies here ensures that dependencies are added only once
elseif candidates[i].deps and (type(candidates[i].deps) ~= 'table' or next(candidates[i].deps)) then
local dep = sat_dep_traverse(state, candidates[i].deps)
local dep = sat_dep_traverse(state, sat_candidates[i], candidates[i].deps)
state.sat:clause(-sat_candidates[i], dep) -- candidate implies its dependencies
end
end
......@@ -155,7 +158,7 @@ function sat_pkg_group(state, name)
-- Add dependencies of package group
local deps = utils.multi_index(pkg, 'modifier', 'deps')
if deps and (type(deps) ~= 'table' or deps.tp) then
local dep = sat_dep_traverse(state, deps)
local dep = sat_dep_traverse(state, pkg_var, deps)
state.sat:clause(-pkg_var, dep)
end
-- And return variable for this package
......@@ -181,9 +184,10 @@ function sat_dep(state, pkg, version, repository)
-- We add here basically or, but without penalizations. Penalization is ensured from dep_pkg_group.
local vars = utils.map(chosen_candidates, function(i, candidate)
assert(state.candidate2sat[candidate]) -- candidate we require should be already in sat
state.sat:clause(-state.candidate2sat[candidate], var) -- candidate => var
return i, state.candidate2sat[candidate]
end)
state.sat:clause(-var, unpack(vars)) -- imply that at least one of the possible candidates is chosen
state.sat:clause(-var, unpack(vars)) -- var => (candidate or candidate or ...)
else
TRACE("SAT candidate selection empty")
state.missing[pkg] = var -- store that this package (as object not group) points to no candidate
......@@ -199,50 +203,43 @@ function sat_dep(state, pkg, version, repository)
end
end
-- Recursively adds dependency to sat. It returns sat variable for whole dependency and another variable for penalty variable if reqpenalty argument is true
function sat_dep_traverse(state, deps, reqpenalty)
-- Recursively adds dependency to sat. It returns sat variable for whole dependency.
function sat_dep_traverse(state, activator, deps)
if type(deps) == 'string' or deps.tp == 'package' or deps.tp == 'dep-package' then
local var = sat_dep(state, deps, deps.version)
return var, var
return sat_dep(state, deps, deps.version)
end
if deps.tp == 'dep-not' then
assert(#deps.sub == 1)
-- just do negation of var, so 'not' is propagated to upper clause
local var, pen = sat_dep_traverse(state, deps.sub[1], reqpenalty)
return -var, -pen
return -sat_dep_traverse(state, activator, deps.sub[1])
end
local wvar = state.sat:var()
local pvar = nil
if reqpenalty then
pvar = state.sat:var()
end
if deps.tp == 'dep-and' then
TRACE("SAT dep and var: " .. tostring(wvar) .. " penvar: " .. tostring(pvar))
TRACE("SAT dep and var: " .. tostring(wvar))
-- wid => var for every variable. Result is that they are all in and statement.
local pens = {}
local vars = {}
for _, sub in ipairs(deps.sub or deps) do
local var, pen = sat_dep_traverse(state, sub, reqpenalty)
state.sat:clause(-wvar, var)
if reqpenalty then table.insert(pens, -pen) end
local var = sat_dep_traverse(state, activator, sub)
state.sat:clause(-activator, -wvar, var) -- wvar => var
table.insert(vars, -var)
end
if pvar then state.sat:clause(pvar, unpack(pens)) end -- (pen and pen and ...) => pvar
state.sat:clause(-activator, wvar, unpack(vars)) -- (var and var and ...) => wvar
elseif deps.tp == 'dep-or' then
TRACE("SAT dep or var: " .. tostring(wvar) .. " penvar: " .. tostring(pvar))
TRACE("SAT dep or var: " .. tostring(wvar))
-- If wvar is true, at least one of sat variables must also be true, so vwar => vars...
local vars = {}
local lastpen = nil
for _, sub in ipairs(deps.sub) do
local var, pen = sat_dep_traverse(state, sub, true)
if pvar then state.sat:clause(-pen, pvar) end -- pen => pvar
lastpen = sat_penalize(state, pen, state.penalty_or, lastpen)
-- wvar => vars...
local var = sat_dep_traverse(state, activator, sub)
state.sat:clause(-activator, -var, wvar) -- var => wvar
lastpen = sat_penalize(state, activator, var, state.penalty_or, lastpen)
table.insert(vars, var)
end
state.sat:clause(-wvar, unpack(vars))
state.sat:clause(-activator, -wvar, unpack(vars)) -- wvar => (var and var and ...)
else
error(utils.exception('bad value', "Invalid dependency description " .. (deps.tp or "<nil>")))
end
return wvar, pvar
return wvar
end
--[[
......
......@@ -2348,7 +2348,9 @@ end
local function sat_dummy()
local sat = {
clauses = {},
varcount = 0
v_true = 1,
v_false = -1,
varcount = 1
}
function sat:var(count)
assert_nil(count) -- we don't support this now here
......@@ -2377,29 +2379,29 @@ function test_sat_penalize()
}
local lastpen = nil
local penalty_group = {}
lastpen = planner.sat_penalize(state, state.sat:var(), penalty_group, lastpen)
lastpen = planner.sat_penalize(state, state.sat.v_true, state.sat:var(), penalty_group, lastpen)
assert_equal(0, lastpen)
lastpen = planner.sat_penalize(state, state.sat:var(), penalty_group, lastpen)
assert_equal(3, lastpen)
lastpen = planner.sat_penalize(state, state.sat:var(), penalty_group, lastpen)
assert_equal(5, lastpen)
assert_equal(5, state.sat.varcount)
assert_table_equal({{-3, -2}, {-5, -4}, {-3, 5}}, state.sat.clauses)
lastpen = planner.sat_penalize(state, state.sat.v_true, state.sat:var(), penalty_group, lastpen)
assert_equal(4, lastpen)
lastpen = planner.sat_penalize(state, state.sat:var(), state.sat:var(), penalty_group, lastpen)
assert_equal(7, lastpen)
assert_equal(7, state.sat.varcount)
assert_table_equal({{-1, -4, -3}, {-5, -7, -6}, {-5, -4, 7}}, state.sat.clauses)
end
function test_sat_dep_traverse()
local state = {
pkg2sat = {
["pkg1"] = 1,
["pkg2"] = 2,
["pkg3"] = 3,
["pkg4"] = 4
["pkg1"] = 2,
["pkg2"] = 3,
["pkg3"] = 4,
["pkg4"] = 5
},
penalty_or = {},
sat = sat_dummy()
-- candidate2sat, req2sat, missing, penalty_candidates and pkgs shouldn't be required
}
state.sat.varcount = 4
state.sat.varcount = 5
local dep = {
tp = "dep-and",
sub = {
......@@ -2431,26 +2433,28 @@ function test_sat_dep_traverse()
}
}
}
local wvar, pvar = planner.sat_dep_traverse(state, dep)
assert_nil(pvar) -- we didn't requested penalty dependencies
assert_equal(5, wvar) -- created as fist after call
local wvar = planner.sat_dep_traverse(state, state.sat.v_true, dep)
assert_equal(6, wvar) -- created as fist after call
assert_table_equal({9}, state.penalty_or)
assert_table_equal({
-- and implies not pkg1
{-5, -1},
-- and variable implies not pkg1
{ -1, -6, -2 },
-- pkg2 or (pkg3 and not pkg4)
{-7, 3}, -- and variable implies pkg3
{-7, -4}, -- and variable implies not pkg4
{8, -3, 4}, -- penalty and variable
{-9, -8}, -- penalty variable implies on penalty dependency
{-6, 2, 7}, -- or variable implies pkg2 or second and variable
{-5, 6} -- and variable implies or variable
{ -1, -3, 7 }, -- pkg2 implies or variable
{ -1, -8, 4 }, -- second and variable implies pkg3
{ -1, -8, -5 }, -- second and variable implies not pkg4
{ -1, 8, -4, 5 }, -- (pkg3 and not pkg4) implies second and variable
{ -1, -8, 7 }, -- second and variable implies or variable
{ -1, -9, -8 }, -- penalty
{ -1, -7, 3, 8 }, -- or variable implies that pkg2 or second and variable
{ -1, -6, 7 }, -- and variable implies or variable
{ -1, 6, 2, -7 } -- not pkg1 and or variable implies and variable
}, state.sat.clauses)
end
function test_sat_pkg_group()
local state = {
pkg2sat = {["otherpkg"] = 1, ["deppkg"] = 2},
pkg2sat = {["otherpkg"] = 2, ["deppkg"] = 3},
candidate2sat = {},
penalty_candidates = {},
pkgs = {
......@@ -2465,28 +2469,28 @@ function test_sat_pkg_group()
sat = sat_dummy()
-- req2sat, missing and penalty_or shouldn't be required
}
state.sat.varcount = 2
state.sat.varcount = 3
local satvar = planner.sat_pkg_group(state, "pkg")
assert_equal(3, satvar)
assert_equal(4, satvar)
assert_table_equal({
["otherpkg"] = 1,
["deppkg"] = 2,
["pkg"] = 3
["otherpkg"] = 2,
["deppkg"] = 3,
["pkg"] = 4
}, state.pkg2sat)
assert_table_equal({
[state.pkgs.pkg.candidates[1]] = 4,
[state.pkgs.pkg.candidates[2]] = 5
[state.pkgs.pkg.candidates[1]] = 5,
[state.pkgs.pkg.candidates[2]] = 6
}, state.candidate2sat)
assert_table_equal({6}, state.penalty_candidates)
assert_equal(6, state.sat.varcount)
assert_table_equal({7}, state.penalty_candidates)
assert_equal(7, state.sat.varcount)
assert_table_equal({
{-4, 3}, -- candidate version 2 implies its package group
{-5, 3}, -- candidate version 1 implies its package group
{-5, -4}, -- candidates are exclusive
{-6, -5}, -- penalize second candidate
{-4, 1}, -- candidate version 2 depends on otherpkg
{-3, 4, 5}, -- package group implies that one of candidates is chosen
{-3, 2} -- package group implies its dependencies
{-5, 4}, -- candidate version 2 implies its package group
{-6, 4}, -- candidate version 1 implies its package group
{-6, -5}, -- candidates are exclusive
{-1, -7, -6}, -- penalize second candidate (active only if pkg group is enabled)
{-5, 2}, -- candidate version 2 depends on otherpkg
{-4, 5, 6}, -- package group implies that one of candidates is chosen
{-4, 3} -- package group implies its dependencies
}, state.sat.clauses)
end
......@@ -2502,22 +2506,24 @@ function test_sat_dep()
}
local state = {
pkg2sat = {
["pkg"] = 1
["pkg"] = 2
},
candidate2sat = {
[pkgs.pkg.candidates[1]] = 2,
[pkgs.pkg.candidates[2]] = 3
[pkgs.pkg.candidates[1]] = 3,
[pkgs.pkg.candidates[2]] = 4
},
pkgs = pkgs,
sat = sat_dummy()
-- req2sat, missing, penalty_candidates and penalty_or shouldn't be required
}
state.sat.varcount = 3
state.sat.varcount = 4
local var = planner.sat_dep(state, {tp = "package", name = "pkg"}, ">=1")
assert_equal(4, var)
assert_equal(5, var)
assert_table_equal({
{-4, 2, 3}, -- candidate selection variable implies at least one of candidates are chosen
{-4, 1} -- candidate selection implies target package group
{-3, 5},
{-4, 5}, -- both candidates implies its selection variables
{-5, 3, 4}, -- candidate selection variable implies at least one of candidates is chosen
{-5, 2} -- candidate selection implies target package group
}, state.sat.clauses)
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment