Commit 05a61639 authored by Karel Koci's avatar Karel Koci 🤘

Merge branch 'sat_stage2' into updater-ng

parents fae95e6f 47bd27ce
......@@ -24,6 +24,7 @@ local setmetatable = setmetatable
local unpack = unpack
local table = table
local picosat = picosat
local DBG = DBG
module "sat"
......@@ -91,6 +92,11 @@ local function __index(sat, key)
return sat._picosat[key]
end
local function clause(sat, ...)
DBG('SAT add clause: ' .. table.concat({...}, ', '))
return sat._picosat:clause(...)
end
--[[
Creates new sat object. It is extension for picosat, so you can call all methods
from picosat in addition to "new_batch".
......@@ -100,9 +106,10 @@ function new()
local sat = {
tp = "sat",
_picosat = picosat,
new_batch = new_batch
new_batch = new_batch,
clause = clause
}
for _, c in pairs({ 'var', 'clause', 'assume', 'satisfiable', 'max_satisfiable' }) do
for _, c in pairs({ 'var', 'assume', 'satisfiable', 'max_satisfiable' }) do
sat[c] = function(sat, ...)
return sat._picosat[c](sat._picosat, unpack({...}))
end
......
......@@ -71,8 +71,8 @@ local function build_deps(sat, satmap, pkgs, requests)
end
-- Create new variable for this package and new sat clauses batch
local pkg_var = sat:var()
DBG("SAT add package " .. name .. " with var: " .. tostring(pkg_var))
satmap.pkg2sat[name] = pkg_var
DBG("Adding dependencies for package " .. name)
local pkg = pkgs[name]
local candidate
if pkg and pkg.candidates and next(pkg.candidates) then
......@@ -86,14 +86,12 @@ local function build_deps(sat, satmap, pkgs, requests)
utils.arr_append(alldeps, (candidate or {}).deps or {})
-- Note that for no dependencies we will receive dummy variable that isn't in any clause.
local dep_var = dep_traverse(alldeps)
-- TODO when penalty variables are added, we should make from this implication equivalence.
sat:clause(-pkg_var, dep_var)
sat:clause(-pkg_var, dep_var) -- We only do implication here. Equivalence could result in package selection because its dependencies are satisfied.
-- And return variable for this package
return pkg_var
end
-- Recursively adds implications for given package to its dependencies. It returns sat variable for whole dependency.
-- As additional to canonized dependencies it also supports table without any type as and, this is for convenience.
-- TODO when penalty variables are added, we should make from all of implications here equivalences.
function dep_traverse(deps)
if type(deps) == 'string' or deps.tp == 'package' or deps.tp == 'dep-package' then
local name = deps
......@@ -109,13 +107,34 @@ local function build_deps(sat, satmap, pkgs, requests)
end
local wvar = sat:var()
if (type(deps) == 'table' and not deps.tp) or deps.tp == 'dep-and' then
-- wid implies all variables, in result they are all in and statement if wid is true
-- wid <=> var for every variable. Result is that they are all in and statement.
for _, sub in ipairs(deps.sub or deps) do
sat:clause(-wvar, dep_traverse(sub))
local var = dep_traverse(sub)
sat:clause(-wvar, var)
sat:clause(-var, wvar)
end
elseif deps.tp == 'dep-or' then
-- If wvar is true, at least one of sat variables must also be true, so vwar => vars...
local vars = utils.map(deps.sub, function(key, sub) return key, dep_traverse(sub) end)
-- Same as if one of vars is true, wvar must be also true, so var => wvar
local vars = {}
local prev_penalty = nil
for _, sub in ipairs(deps.sub) do
local var = dep_traverse(sub)
-- var => wvar
sat:clause(-var, wvar)
-- penalty => not var and potentially prev_penalty => penalty
if #vars ~= 0 then -- skip first one, it isn't penalized.
local penalty = sat:var()
if prev_penalty then
sat:clause(-prev_penalty, penalty)
end
sat:clause(-penalty, -var)
prev_penalty = penalty
satmap.penaltysat[penalty] = true -- store that this is penalty variable
end
-- wvar => vars...
table.insert(vars, var)
end
sat:clause(-wvar, unpack(vars))
else
error(utils.exception('bad value', "Invalid dependency description " .. (deps.tp or "<nil>")))
......@@ -290,6 +309,7 @@ function required_pkgs(pkgs, requests)
pkg2sat = {},
req2sat = {},
pkg2candidate = {}, -- TODO replace with candidate2sat
penaltysat = {} -- Set of all penalty variables
}
-- Build dependencies
build_deps(sat, satmap, pkgs, requests)
......@@ -327,6 +347,7 @@ function required_pkgs(pkgs, requests)
end
-- Install critical packages requests (set all critical packages to be true)
DBG("Resolving critical packages")
for _, req in ipairs(reqs_critical) do
sat:clause(satmap.req2sat[req])
end
......@@ -336,6 +357,7 @@ function required_pkgs(pkgs, requests)
end
-- Install and Uninstall requests.
DBG("Resolving Install and Uninstall requests")
for _, reqs in ipairs(reqs_prior) do
for _, req in pairs(reqs) do
-- Assume all request for this priority
......@@ -345,18 +367,24 @@ function required_pkgs(pkgs, requests)
end
-- Deny any packages missing or without candidates if possible
-- TODO use penalty variables for this
DBG("Denying packages without any candidate")
for name, var in pairs(satmap.pkg2sat) do
local pkg = pkgs[name]
if not pkg or not pkg.candidates or next(pkg.candidates) then
if not pkg or not pkg.candidates or not next(pkg.candidates) then
sat:assume(-var)
end
end
clause_max_satisfiable()
-- TODO add penalty variables and go trough them here
-- Chose alternatives with penalty variables
DBG("Forcing penalty on expressions with free alternatives")
for var, _ in pairs(satmap.penaltysat) do
sat:assume(var)
end
clause_max_satisfiable()
-- Now solve all packages selections from dependencies of already selected packages
DBG("Deducing minimal set of required packages")
for _, var in pairs(satmap.pkg2sat) do
-- We assume false (not selected) for all packages
sat:assume(-var)
......
......@@ -452,6 +452,154 @@ function test_request_collision()
assert_exception(function() planner.required_pkgs(pkgs, requests) end, 'invalid-request')
end
function test_penalty()
local pkgs = {
pkg = {
candidates = {{Package = 'pkg', deps = {}, repo = def_repo}},
modifier = {
deps = {
tp = "dep-or",
sub = {"dep1", "dep2", "dep3", "dep4"}
}
}
},
dep1 = {
candidates = {{Package = 'dep1', deps = {}, repo = def_repo}},
modifier = {}
},
dep2 = {
candidates = {{Package = 'dep2', deps = {}, repo = def_repo}},
modifier = {}
},
dep3 = {
candidates = {{Package = 'dep3', deps = {}, repo = def_repo}},
modifier = {}
},
dep4 = {
candidates = {{Package = 'dep4', deps = {}, repo = def_repo}},
modifier = {}
}
}
local requests = {
{
tp = 'install',
package = {
tp = 'package',
name = 'pkg',
}
}
}
local expected = {
pkg = {
action = "require",
package = {Package = 'pkg', deps = {}, repo = def_repo},
modifier = {
deps = {
tp = "dep-or",
sub = {"dep1", "dep2", "dep3", "dep4"}
}
},
name = "pkg"
},
dep1 = {
action = "require",
package = {Package = 'dep1', deps = {}, repo = def_repo},
modifier = {},
name = "dep1"
}
}
local result = planner.required_pkgs(pkgs, requests)
assert_plan_dep_order(expected, result)
table.insert(requests, {
tp = 'install',
package = {
tp = 'package',
name = 'dep3'
}
})
expected['dep1'] = nil
expected['dep3'] = {
action = "require",
package = {Package = 'dep3', deps = {}, repo = def_repo},
modifier = {},
name = 'dep3'
}
result = planner.required_pkgs(pkgs, requests)
assert_plan_dep_order(expected, result)
end
function test_penalty_and_missing()
local pkgs = {
pkg = {
candidates = {{Package = 'pkg', deps = {}, repo = def_repo}},
modifier = {
deps = {
tp = "dep-or",
sub = {"dep1", "dep2", "dep3", "dep4"}
}
}
},
dep1 = {
candidates = {},
modifier = {}
},
dep2 = {
candidates = {{Package = 'dep2', deps = {}, repo = def_repo}},
modifier = {}
},
dep3 = {
candidates = {{Package = 'dep3', deps = {}, repo = def_repo}},
modifier = {}
},
dep4 = {
candidates = {},
modifier = {}
}
}
local requests = {
{
tp = 'install',
package = {
tp = 'package',
name = 'pkg',
}
}
}
local expected = {
pkg = {
action = "require",
package = {Package = 'pkg', deps = {}, repo = def_repo},
modifier = {
deps = {
tp = "dep-or",
sub = {"dep1", "dep2", "dep3", "dep4"}
}
},
name = "pkg"
},
dep2 = {
action = "require",
package = {Package = 'dep2', deps = {}, repo = def_repo},
modifier = {},
name = "dep2"
}
}
local result = planner.required_pkgs(pkgs, requests)
assert_plan_dep_order(expected, result)
pkgs.dep2.candidates = {}
expected.dep2 = nil
expected.dep3 = {
action = 'require',
package = {Package = 'dep3', deps = {}, repo = def_repo},
modifier = {},
name = "dep3"
}
result = planner.required_pkgs(pkgs, requests)
assert_plan_dep_order(expected, result)
end
function test_filter_required()
local status = {
pkg1 = {
......@@ -815,14 +963,12 @@ function test_pkg_dep_iterate()
assert_nil(next(expected))
end
-- This checks plan order by checking dependencies and tables in plan are checked agains expected ones by name of package
-- This checks plan order by checking dependencies and tables in plan are checked against expected ones by name of package
function assert_plan_dep_order(expected, plan)
local p2i = {}
for key, p in ipairs(plan) do
assert_table_equal(expected[p.name], p)
expected[p.name] = nil -- We checked this one, by this we ensure that it wont be used again and we can check that all that shoudl be is in plan
p2i[p.name] = key
end
-- Check that plan contains all and only expected entries
assert_table_equal(expected, utils.map(plan, function(_, p) return p.name, p end))
-- Check that objects are in correct order
local p2i = utils.map(plan, function(k, v) return v.name, k end)
for _, p in ipairs(plan) do
local alldeps = {p.modifier.deps}
utils.arr_append(alldeps, p.package.deps or {})
......@@ -836,5 +982,4 @@ function assert_plan_dep_order(expected, plan)
end
end
end
assert_nil(next(expected))
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