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

Remove unneeded sat module

This module was originally for ability to decide if clauses are valid
after they are generated. This is not required with current
implementation.
parent fca34826
......@@ -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
......@@ -388,7 +387,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 = {},
......
--[[
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))))
......
......@@ -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"
}
--[[
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()
assert_false(s:satisfiable())
batch2:commit() -- committing batch2 should make no difference, it is empty now
assert_false(s:satisfiable())
end
function test_registered_batch()
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 = s:new_batch()
batch1:reg_batch(batch2)
-- (-2)
batch2:clause(-var2)
batch1:commit()
assert_false(s:satisfiable())
batch2:commit() -- committing batch2 should make no difference, it is empty now
assert_false(s:satisfiable())
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