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

Merge branch 'depends-cleanup' into updater-ng

parents dc5e74a1 1a4138be
......@@ -3,7 +3,7 @@ LIBRARIES += src/lib/libupdater
$(O)/.gen/src/%.embedlist: $(S)/src/lib/gen_embed.sh $(S)/src/lib/embed_types.h
$(M) GEN $@
$(Q)mkdir -p $(dir $@)
# The filter-out leaves embed_types.h in. But this one is used by the script (not to be embedded, though, it's a different kind of parameter than the rest of them).
@# The filter-out leaves embed_types.h in. But this one is used by the script (not to be embedded, though, it's a different kind of parameter than the rest of them).
$(Q)$< "$(SUFFIX)" $(basename $(notdir $@)) $(abspath $(filter-out $<, $^)) >$@
$(O)/.gen/src/lib/lautoload.embedlist: $(wildcard $(S)/src/lib/autoload/*.lua)
......@@ -29,6 +29,8 @@ libupdater_MODULES_3RDPARTY := \
libupdater_PKG_CONFIGS := $(LUA_NAME) libevent
# Workaround, lua.pc doesn't containd -ldl, even when it uses dlopen
libupdater_SO_LIBS += dl
# Enable tracing for picosat
libupdater_CFLAGS := -DTRACE
LIB_DOCS := \
journal \
......
......@@ -25,6 +25,9 @@ local type = type
local setmetatable = setmetatable
local getmetatable = getmetatable
local assert = assert
local table = table
local string = string
local math = math
local io = io
local unpack = unpack
local events_wait = events_wait
......@@ -32,7 +35,7 @@ local run_command = run_command
module "utils"
-- luacheck: globals lines2set map set2arr arr2set cleanup_dirs slurp clone shallow_copy table_merge arr_append exception multi_index private filter_best strip table_overlay randstr
-- luacheck: globals lines2set map set2arr arr2set cleanup_dirs slurp clone shallow_copy table_merge arr_append exception multi_index private filter_best strip table_overlay randstr arr_prune arr_inv
--[[
Convert provided text into set of lines. Doesn't care about the order.
......@@ -75,6 +78,29 @@ function arr2set(arr)
return map(arr, function (_, name) return name, true end)
end
-- Removes all nil values by shifting upper elements down.
function arr_prune(arr)
local indxs = set2arr(arr)
table.sort(indxs)
local res = {}
for _, i in ipairs(indxs) do
table.insert(res, arr[i])
end
return res
end
-- Inverts order of array
function arr_inv(arr)
local mid = math.modf(#arr / 2)
local endi = #arr + 1
for i = 1, mid do
local v = arr[i]
arr[i] = arr[endi - i]
arr[endi - i] = v
end
return arr
end
-- Run rm -rf on all dirs in the provided table
function cleanup_dirs(dirs)
if next(dirs) then
......
......@@ -178,10 +178,7 @@ function pkg_status_dump(status)
return block_dump_ordered({
raw "Package",
raw "Version",
line("Depends", function (deps)
-- Join the dependencies together, separated by commas
return table.concat(deps, ', ')
end),
raw "Depends",
raw "Conflicts",
line("Status", function (status)
-- Join status flags together, separated by spaces
......@@ -297,13 +294,7 @@ function package_postprocess(status)
-- Conffiles are lines with two „words“
replace("Conffiles", "\n", "%s*(%S+)%s+(%S+)")
status.Conffiles = slashes_sanitize(status.Conffiles)
-- Depends are separated by commas and may contain a version in parentheses
local idx = 0
replace("Depends", ",", function (s)
idx = idx + 1
return idx, s:gsub("^%s", ""):gsub("%s$", "")
end)
idx = 0
replace("Status", " ", function (s)
idx = idx + 1
return idx, s
......
......@@ -261,7 +261,6 @@ function pkg_aggregate()
available_packages[pkg.name] = {candidates = {}, modifiers = {}}
end
local pkg_group = available_packages[pkg.name]
utils.private(pkg).group = pkg_group
if pkg.virtual then
table.insert(pkg_group.candidates, pkg)
pkg_group.virtual = true
......@@ -340,9 +339,10 @@ function pkg_aggregate()
-- Canonize dependencies
modifier.deps = deps_canon(modifier.deps)
for _, candidate in ipairs(pkg_group.candidates or {}) do
local candidate_deps = { candidate.deps } -- deps from updater configuration file
table.insert(candidate_deps, candidate.Depends) -- Depends from repository)
candidate.deps = deps_canon(candidate_deps)
candidate.deps = deps_canon(utils.arr_prune({
candidate.deps, -- deps from updater configuration file
candidate.Depends -- Depends from repository
}))
end
pkg_group.modifier = modifier
-- We merged them together, they are no longer needed separately
......
......@@ -29,10 +29,10 @@ local table = table
local DIE = DIE
local DBG = DBG
local WARN = WARN
local picosat = picosat
local utils = require "utils"
local backend = require "backend"
local requests = require "requests"
local sat = require "sat"
module "planner"
......@@ -73,7 +73,6 @@ function candidates_choose(candidates, version, repository)
end
return compliant
end
--[[
Build dependencies for all touched packages. We do it recursively across
dependencies of requested packages, this makes searched space smaller and building
......@@ -330,8 +329,7 @@ local function build_plan(pkgs, requests, sat, satmap)
-- Recursively add all packages this package depends on --
inwstack[name] = #wstack + 1 -- Signal that we are working on this package group.
table.insert(wstack, name)
local alldeps = { utils.multi_index(pkg, 'modifier', 'deps') }
table.insert(alldeps, (candidate or {}).deps or {})
local alldeps = utils.arr_prune({ utils.multi_index(pkg, 'modifier', 'deps'), (candidate or {}).deps })
for _, p in pkg_dep_iterate(alldeps) do
pkg_plan(p, ignore_missing or utils.arr2set(utils.multi_index(pkg, 'modifier', 'ignore') or {})["deps"], false, "Package " .. name .. " requires package")
end
......@@ -373,15 +371,13 @@ Take list of available packages (in the format of pkg candidate groups
produced in postprocess.available_packages) and list of requests what
to install and remove. Produce list of packages, in the form:
{
{action = "require"/"reinstall"/"remove", package = pkg_source, modifier = modifier}
{action = "require"/"reinstall", package = pkg_source, modifier = modifier}
}
The action specifies if the package should be made present in the system (installed
if missing), reinstalled (installed no matter if it is already present) or
removed from the system.
if missing) or reinstalled (installed no matter if it is already present)
• Required to be installed
• Required to be reinstalled even when already present (they ARE part of the previous set)
• Required to be removed if present (they are not present in the previous two lists)
The pkg_source is the package object (in case it contains the source field or is virtual)
or the description produced from parsing the repository. The modifier is the object
......@@ -389,7 +385,7 @@ constructed from package objects during the aggregation, holding additional proc
info (hooks, etc).
]]
function required_pkgs(pkgs, requests)
local sat = sat.new()
local sat = picosat.new()
-- Tables that's mapping packages, requests and candidates with sat variables
local satmap = {
pkg2sat = {},
......@@ -410,6 +406,7 @@ function required_pkgs(pkgs, requests)
table.insert(reqs_critical, req)
else
if not req.priority then req.priority = 50 end
if not reqs_by_priority[req.priority] then reqs_by_priority[req.priority] = {} end
if req.tp ~= (utils.map(reqs_by_priority[req.priority], function(_, r) return r.package.name, r.tp end)[req.package.name] or req.tp) then
error(utils.exception('invalid-request', 'Requested both Install and Uninstall with same priority for package ' .. req.package.name))
......@@ -417,12 +414,7 @@ function required_pkgs(pkgs, requests)
table.insert(reqs_by_priority[req.priority], req)
end
end
local prios = utils.set2arr(reqs_by_priority)
table.sort(prios, function(a, b) return a > b end)
local reqs_prior = {}
for _, p in ipairs(prios) do
table.insert(reqs_prior, reqs_by_priority[p])
end
reqs_by_priority = utils.arr_inv(utils.arr_prune(reqs_by_priority))
-- Executes sat solver and adds clauses for maximal satisfiable set
local function clause_max_satisfiable()
......@@ -446,7 +438,7 @@ function required_pkgs(pkgs, requests)
-- Install and Uninstall requests.
DBG("Resolving Install and Uninstall requests")
for _, reqs in ipairs(reqs_prior) do
for _, reqs in ipairs(reqs_by_priority) do
for _, req in pairs(reqs) do
-- Assume all request for this priority
sat:assume(satmap.req2sat[req])
......@@ -492,9 +484,10 @@ function required_pkgs(pkgs, requests)
end
--[[
Go through the list of requests on the input. Pass the needed ones through
and leave the extra (eg. requiring already installed package) out. Add
requests to remove not required packages.
Go through the list of requests on the input. Pass the needed ones through and
leave the extra (eg. requiring already installed package) out. And creates
additional requests with action "remove", such package is present on system, but
is not required any more and should be removed.
]]
function filter_required(status, requests)
local installed = {}
......@@ -520,22 +513,11 @@ function filter_required(status, requests)
unused[request.name] = nil
elseif request.action == "reinstall" then
-- Make a shallow copy and change the action requested
local new_req = {}
for k, v in pairs(request) do
new_req[k] = v
end
local new_req = utils.shallow_copy(request)
new_req.action = "require"
DBG("Want to reinstall " .. request.name)
table.insert(result, new_req)
unused[request.name] = nil
elseif request.action == "remove" then
if installed[request.name] then
DBG("Want to remove " .. request.name)
table.insert(result, request)
else
DBG("Package " .. request.name .. " not installed, ignoring request to remove")
end
unused[request.name] = nil
else
DIE("Unknown action " .. request.action)
end
......
--[[
Copyright 2016, CZ.NIC z.s.p.o. (http://www.nic.cz/)
This file is part of the turris updater.
Updater is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
Updater is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with Updater. If not, see <http://www.gnu.org/licenses/>.
]]--
local pairs = pairs
local ipairs = ipairs
local rawget = rawget
local setmetatable = setmetatable
local unpack = unpack
local table = table
local picosat = picosat
module "sat"
-- luacheck: globals new
--[[
Creates new batch object for given picosat. Batch stores clauses without pushing
them to picosat. You can call "clause" and "var" same as with picosat (Note that
"var" is immediate call to picosat). When you want to add batch to picosat, you
call "commit".
It also allows creation of sub-batches using "new_batch" method of original batch.
Such new batch is just new batch, except that it's committed when original batch
is committed. Although it can be committed on its own too.
]]--
local function new_batch(sat)
local batch = {
tp = "sat.batch",
clauses = {},
batches = {},
sat = sat
}
-- Add given clause to batch
function batch:clause(...)
table.insert(self.clauses, {...})
end
-- Just a wrapper for calling picosat var method
function batch:var(num)
return self.sat:var(num)
end
-- Function to add clauses batch to picosat and all batches created as part of this batch
function batch:commit()
if not self.clauses then
return
end
for _, clause in ipairs(batch.clauses) do
batch.sat:clause(unpack(clause))
end
batch.clauses = nil
for b, _ in pairs(batch.batches) do
b:commit()
end
batch.batches = nil
end
-- Creates new sub-batch
function batch:new_batch()
local nbatch = self.sat:new_batch()
self:reg_batch(nbatch)
return nbatch
end
-- Registers existing batch as sub-batch
function batch:reg_batch(b)
self.batches[b] = true
end
-- Unregister given batch
function batch:unreg_batch(b)
self.batches[b] = nil
end
return batch
end
local function __index(sat, key)
local v = rawget(sat, key)
if v then return v end
return sat._picosat[key]
end
--[[
Creates new sat object. It is extension for picosat, so you can call all methods
from picosat in addition to "new_batch".
]]--
function new()
local picosat = picosat.new()
local sat = {
tp = "sat",
_picosat = picosat,
new_batch = new_batch,
}
for _, c in pairs({ 'var', 'assume', 'clause', 'satisfiable', 'max_satisfiable', 'print_trace' }) do
sat[c] = function(sat, ...)
return sat._picosat[c](sat._picosat, unpack({...}))
end
end
setmetatable(sat, { __index = __index })
return sat
end
......@@ -38,8 +38,7 @@ LUA_TESTS := \
transaction \
utils \
uri \
picosat \
sat
picosat
# Ignore stacktraceplus and dumper, not our creation.
LUA_AUTOLOAD := $(filter-out 01_stacktraceplus 05_dumper,$(patsubst a_%.lua,%,$(notdir $(wildcard $(S)/src/lib/autoload/a_*.lua))))
......
......@@ -127,7 +127,7 @@ function test_package_postprocces()
assert_equal(package, output)
assert_table_equal({"install", "user", "installed"}, output.Status)
assert_table_equal({["/etc/config/dhcp"] = "f81fe9bd228dede2165be71e5c9dcf76cc", ["/etc/dnsmasq.conf"] = "1e6ab19c1ae5e70d609ac7b6246541d520"}, output.Conffiles)
assert_table_equal({"libc", "kernel (= 3.18.21-1-70ea6b9a4b789c558ac9d579b5c1022f-10)", "kmod-nls-base"}, output.Depends)
assert_table_equal("libc, kernel (= 3.18.21-1-70ea6b9a4b789c558ac9d579b5c1022f-10), kmod-nls-base", output.Depends)
--[[
Now check it doesn't get confused when some of the modified fields aren't there
(or none, in this case).
......@@ -166,11 +166,7 @@ function test_status_parse()
["Installed-Size"] = "22537",
Description = "Kernel support for USB Mass Storage devices",
["Installed-Time"] = "1453896142",
Depends = {
"kernel (=3.18.21-1-70ea6b9a4b789c558ac9d579b5c1022f-10)",
"kmod-scsi-core",
"kmod-usb-core"
},
Depends = "kernel (=3.18.21-1-70ea6b9a4b789c558ac9d579b5c1022f-10), kmod-scsi-core, kmod-usb-core",
Status = std_status,
files = {
["/lib/modules/3.18.21-70ea6b9a4b789c558ac9d579b5c1022f-10/usb-storage.ko"] = true,
......@@ -189,7 +185,7 @@ function test_status_parse()
["Installed-Size"] = "5822",
Description = "Terminal Info Database (ncurses)",
["Installed-Time"] = "1453896265",
Depends = {"libc"},
Depends = "libc",
Status = std_status,
files = {
["/usr/share/terminfo/x/xterm"] = true,
......@@ -218,7 +214,7 @@ function test_status_parse()
This is a variant with DHCPv6 support]],
["Installed-Time"] = "1453896240",
Depends = {"libc"},
Depends = "libc",
Status = std_status,
files = {
["/etc/dnsmasq.conf"] = true,
......@@ -238,7 +234,7 @@ function test_status_parse()
Version = "27",
Architecture = "mpc85xx",
["Installed-Time"] = "1453896279",
Depends = {"libc", "ucollect-prog"},
Depends = "libc, ucollect-prog",
Status = std_status,
files = {}
})
......@@ -339,7 +335,7 @@ function test_pkg_unpack()
Architecture = "mpc85xx",
["Installed-Size"] = "14773",
Description = "updater",
Depends = {"libc", "vixie-cron", "openssl-util", "libatsha204", "curl", "cert-backup", "opkg", "bzip2", "cznic-cacert-bundle"},
Depends = "libc, vixie-cron, openssl-util, libatsha204, curl, cert-backup, opkg, bzip2, cznic-cacert-bundle",
Conffiles = conffiles,
Status = {"install", "user", "installed"},
files = files
......@@ -688,13 +684,13 @@ Installed-Time: 1
Version = "1",
["Installed-Time"] = "1",
Extra = "xxxx",
Depends = { "dep1", "dep2" },
Depends = "dep1, dep2",
Status = { "flag" },
Conffiles = { ["file"] = "1234567890123456" }
}))
end
function test_status_dump()
function test_status_parse_dump()
-- Read the status
local status = B.status_parse()
-- Make a copy of the status file, we'are going to write into it
......@@ -710,7 +706,7 @@ function test_status_dump()
Package = "New",
Version = "1",
["Installed-Time"] = "1",
Depends = { "Dep1", "dep2" },
Depends = "Dep1, dep2",
Status = { "flag" }
}
-- Do one more store-read-compare cycle
......@@ -850,12 +846,12 @@ function test_repo_parse()
["base-files"] = {
Package = "base-files",
Version = "160-r49274",
Depends = {"libc", "netifd", "procd", "jsonfilter"}
Depends = "libc, netifd, procd, jsonfilter"
},
["block-mount"] = {
Package = "block-mount",
Version = "2015-05-24-09027fc86babc3986027a0e677aca1b6999a9e14",
Depends = {"libc", "ubox", "libubox", "libuci"}
Depends = "libc, ubox, libubox, libuci"
}
}, B.repo_parse([[
Package: base-files
......
......@@ -16,5 +16,5 @@ globals = {
-- Picosat
"picosat",
-- Modules
"stacktraceplus", "utils", "backend", "transaction", "uri", "requests", "sandbox", "postprocess", "planner", "updater", "migrator", "sat"
"stacktraceplus", "utils", "backend", "transaction", "uri", "requests", "sandbox", "postprocess", "planner", "updater", "migrator"
}
......@@ -48,7 +48,6 @@ function test_no_deps()
package = {
tp = 'package',
name = 'pkg1',
group = pkgs.pkg1
}
},
{
......@@ -214,7 +213,6 @@ function test_deps()
package = {
tp = 'package',
name = 'pkg1',
group = pkgs.pkg1
}
},
{
......@@ -222,7 +220,6 @@ function test_deps()
package = {
tp = 'package',
name = 'pkg2',
group = pkgs.pkg2
}
}
}
......@@ -282,7 +279,6 @@ function test_missing_dep()
package = {
tp = 'package',
name = 'pkg',
group = pkgs.pkg
}
}
}
......@@ -721,9 +717,6 @@ function test_filter_required()
},
pkg4 = {
Version = "4"
},
pkg5 = {
Version = "5"
}
}
local requests = {
......@@ -757,22 +750,13 @@ function test_filter_required()
},
modifier = {}
},
{
-- Installed and we want to remove it
action = "remove",
name = "pkg4",
package = {
Version = "4",
repo = def_repo
}
},
-- The pkg5 is not mentioned, it shall be uninstalled at the end
-- The pkg4 is not mentioned, it shall be uninstalled at the end
{
-- Not installed and we want it
action = "require",
name = "pkg6",
name = "pkg5",
package = {
Version = "6",
Version = "5",
repo = def_repo
},
modifier = {}
......@@ -791,12 +775,11 @@ function test_filter_required()
modifier = {}
},
requests[4],
requests[5],
{
action = "remove",
name = "pkg5",
name = "pkg4",
package = {
Version = "5"
Version = "4"
-- No repo field here, this comes from the status, there are no repositories
}
}
......@@ -935,7 +918,6 @@ function test_missing_install()
package = {
tp = 'package',
name = 'pkg1',
group = pkgs.pkg1
}
},
{
......@@ -975,7 +957,6 @@ function test_missing_dep_ignore()
package = {
tp = 'package',
name = 'pkg1',
group = pkgs.pkg1
}
}
}
......@@ -1006,7 +987,6 @@ function test_complex_deps()
local pkg2 = {
tp = "package",
name = "pkg2",
group = pkgs.pkg2
}
pkgs.meta = {
candidates = {{Package = "meta", repo = def_repo}},
......@@ -1047,7 +1027,6 @@ function test_complex_deps()
package = {
tp = 'package',
name = 'meta',
group = pkgs.meta
}
}
}
......@@ -1302,8 +1281,7 @@ function assert_plan_dep_order(expected, plan)
-- 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 {})
local alldeps = utils.arr_prune({p.modifier.deps, p.package.deps})
local pi = p2i[p.name]
for _, dep in ipairs(alldeps) do
for _, pkg in planner.pkg_dep_iterate(dep) do
......
......@@ -51,7 +51,7 @@ local example_output = {
list = {
["6in4"] = {
Architecture = "all",
Depends = {"libc", "kmod-sit"},
Depends = "libc, kmod-sit",
Description = [[Provides support for 6in4 tunnels in /etc/config/network.
Refer to http://wiki.openwrt.org/doc/uci/network for
configuration details.]],
......@@ -70,7 +70,7 @@ local example_output = {
},
["6rd"] = {
Architecture = "all",
Depends = {"libc", "kmod-sit"},
Depends = "libc, kmod-sit",
Description = [[Provides support for 6rd tunnels in /etc/config/network.
Refer to http://wiki.openwrt.org/doc/uci/network for
configuration details.]],
......@@ -188,7 +188,8 @@ function test_pkg_merge()
tp = 'pkg-list',
list = {
xyz = {Package = "xyz", Version = "1"},
abc = {Package = "abc", Version = "2"}
abc = {Package = "abc", Version = "2", Depends = "cde"},
cde = {Package = "cde", Version = "1"}
}
}
}
......@@ -247,11 +248,15 @@ function test_pkg_merge()
local exp = {
abc = {
candidates = {
{Package = "abc", Version = "2", repo = requests.known_repositories_all[1]},
{Package = "abc", Depends = "cde", deps = "cde", Version = "2", repo = requests.known_repositories_all[1]},
{Package = "abc", Version = "1", repo = requests.known_repositories_all[2]}
},
modifier = {name = "abc"}
},
cde = {
candidates = {{Package = "cde", Version = "1", repo = requests.known_repositories_all[1]}},
modifier = {name = "cde"}
},
another = {
candidates = {{Package = "another", Version = "4", repo = requests.known_repositories_all[2]}},
modifier = {name = "another"}
......@@ -295,7 +300,6 @@ function test_pkg_merge()
end
end
assert_table_equal(exp, postprocess.available_packages)
assert_table_equal(utils.private(postprocess.available_packages.virt.candidates[1]).group, exp.virt)
end
function test_deps_canon()
......@@ -305,6 +309,7 @@ function test_deps_canon()
assert_equal("x", postprocess.deps_canon("x"))
assert_equal("x", postprocess.deps_canon(" x "))
assert_equal("x", postprocess.deps_canon({"x"}))
assert_equal("x", postprocess.deps_canon({"x", ""}))
assert_equal("x", postprocess.deps_canon({tp = 'dep-and', sub = {"x"}}))
assert_equal("x", postprocess.deps_canon({tp = 'dep-or', sub = {"x"}}))
assert_equal("x", postprocess.deps_canon("x ( )"))
......
--[[
Copyright 2016, CZ.NIC z.s.p.o. (http://www.nic.cz/)
This file is part of the turris updater.
Updater is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
Updater is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with Updater. If not, see <http://www.gnu.org/licenses/>.
]]--
require "lunit"
local sat = require "sat"
module("sat-tests", package.seeall, lunit.testcase)
-- This is from tests for picosat. We use it here to check that sat is really extension for picosat.
function test_sat()
local sat = sat.new()
local var1, var2, var3 = sat:var(3)
-- (3 => 2) && (1 xor 2)
sat:clause(-var3, var2)
sat:clause(var1, var2)
sat:clause(-var1, -var2)
sat:assume(var2)
sat:assume(var3)
assert_true(sat:satisfiable())
assert_false(sat[var1])
assert_true(sat[var2])
assert_true(sat[var3])
sat:assume(-var2)
sat:assume(var3)
assert_false(sat:satisfiable())
local maxassum = sat:max_satisfiable()
-- Solution can be -var2 or var3. So we check for both.
assert_true((not maxassum[var2] and maxassum[var3] == nil) or (maxassum[var2] == nil and maxassum[var3]))
-- and souldn't contain var1
assert_nil(maxassum[var1])
end
function test_batch()
local s = sat.new()
local var1, var2 = s:var(2)
-- (1 => 2) && (1)
s:clause(-var1, var2)
s:clause(var1)
assert_true(s:satisfiable())
assert_true(s[var1])
assert_true(s[var2])
local batch1 = s:new_batch()
local var3 = batch1:var()
-- (2 xor 3)
batch1:clause(var2, var3)
batch1:clause(-var2, -var3)
local batch2 = s:new_batch()
-- (-2)
batch2:clause(-var2)
batch1:commit()
assert_true(s:satisfiable())
assert_true(s[var1])
assert_true(s[var2])
assert_false(s[var3])
batch2:commit()
assert_false(s:satisfiable())
end
function test_nested_batches()
local s = sat.new()
local var1, var2 = s:var(2)
-- (1 => 2) && (1)
s:clause(-var1, var2)
s:clause(var1)
local batch1 = s:new_batch()
local var3 = batch1:var()
-- (2 xor 3)
batch1:clause(var2, var3)
batch1:clause(-var2, -var3)
local batch2 = batch1:new_batch()
-- (-2)
batch2:clause(-var2)
batch1:commit()