Commit 3986cf11 authored by Karel Koci's avatar Karel Koci 🤘

Merge branch 'deps' into updater-ng

Conflict resolved by hand. File a_12_sat.lua wasn't recognized like
moved, definitions of globals was moved from luacheck.config to files
it self and new file a_13_migrator.lua is renamed to a_14*.
parents 439156b3 d5b6e30e
Subproject commit 37ed327ffa68a2b413c06cc08e73490b07ff91aa
Subproject commit c555a99d459430783b2f66d627ed844b41a93b1b
......@@ -32,11 +32,7 @@ We provide several kinds of variables:
version-dependencies.
* Auxiliary variables. As there may be complex dependencies, it is
easier to use something like Tseytin transformation ‒ have a
„result“ variable for each `Or`, `And` and `Not` operator. Note that
since a dependency on the expression is an implication (the
expression must be true when the package is installed, but we don't
care about its value when it is not), we are free to produce only
one direction of value enforcement (eg. propagating down).
„result“ variable for each `Or`, `And` and `Not` operator.
* Penalty variables. When we choose from multiple options, we want to
prefer some based on local criteria. These variables are added to
these choices and are forced to false whenever a non-optimal choice
......
......@@ -18,9 +18,14 @@ libupdater_MODULES := \
events \
journal \
locks \
util \
picosat \
util
libupdater_MODULES_3RDPARTY := \
md5 \
sha256
sha256 \
picosat-960/picosat
libupdater_PKG_CONFIGS := $(LUA_NAME) libevent
# Workaround, lua.pc doesn't containd -ldl, even when it uses dlopen
libupdater_SO_LIBS += dl
......
......@@ -157,23 +157,34 @@ end
--[[
Canonicize the dependencies somewhat. This does several things:
• Splits dependencies from strings (eg. "a b c" becomes a real dep-and object holding "a", "b", "c").
• Splits dependencies from strings (eg. "a, b, c" becomes a real dep-and object holding "a", "b", "c").
• Splits version limitations from dependency string (ex.: "a (>=1)" becomes { tp="dep-package", name="a", version=">=1" }).
• Table dependencies are turned to real dep-and object.
• Empty dependencies are turned to nil.
• Single dependencies are turned to just the string (except with the not dependency)
TODO: There may be versions. These are ignored for now.
]]
function deps_canon(old_deps)
if type(old_deps) == 'string' then
if old_deps:match('%s') then
if old_deps:match(',') then
local sub = {}
for dep in old_deps:gmatch('%S+') do
table.insert(sub, dep)
for dep in old_deps:gmatch('[^,]+') do
table.insert(sub, deps_canon(dep))
end
return deps_canon({
tp = 'dep-and',
sub = sub
})
elseif old_deps:match('%s') then
-- When there is space in parsed name, then there might be version specified
local dep = old_deps:gsub('^%s', ''):gsub('%s$', '')
local name = dep:match('^%S+')
local version = dep:match('%(.+%)$')
version = version and version:sub(2,-2):gsub('^%s', ''):gsub('%s$', '')
if not version or version == "" then
return name -- No version detected, use just name.
else
return { tp = "dep-package", name = name, version = version }
end
elseif old_deps == '' then
return nil
else
......@@ -327,6 +338,12 @@ function pkg_aggregate()
modifier.replan = modifier.replan or m.replan
end
modifier.deps = deps_canon(modifier.deps)
for _, candidate in ipairs(pkg_group.candidates or {}) do
candidate.deps = deps_canon(candidate.deps) or {} -- deps from updater configuration file
for _, d in ipairs(candidate.Depends or {}) do -- Depends from repository
table.insert(candidate.deps, deps_canon(d))
end
end
pkg_group.modifier = modifier
-- We merged them together, they are no longer needed separately
pkg_group.modifiers = nil
......
--[[
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', 'clause', 'assume', 'satisfiable', 'max_satisfiable' }) do
sat[c] = function(sat, ...)
return sat._picosat[c](sat._picosat, unpack({...}))
end
end
setmetatable(sat, { __index = __index })
return sat
end
......@@ -25,6 +25,7 @@
#include "sha256.h"
#include "locks.h"
#include "arguments.h"
#include "picosat.h"
#include <lua.h>
#include <lualib.h>
......@@ -752,6 +753,7 @@ struct interpreter *interpreter_create(struct events *events, const struct file_
// Some binary embedded modules
journal_mod_init(L);
locks_mod_init(L);
picosat_mod_init(L);
return result;
}
......
......@@ -199,6 +199,36 @@ The format of journal returned by recover is a table with records.
Each record contains `type` ‒ one of the types above, and `params` ‒
table with all the parameters stored with the record.
Pisocat
-------
Picosat can be used trough module `picosat`. Here is briefly described
its interface as it can be used from Lua. For more information about
usage see Picosat documentation in its source file.
You can create picosat instance by calling `picosat.new` function.
It returns object with following methods:
var(count):: Creates given number of new variables and returns them.
If no argument is given, it returns one new variable.
clause(var, ...):: Adds clause. Arguments `var` are variables
previously created with `var` method. Appending minus before variable
adds boolean negation.
assume(var):: Adds assumption about value `val` for next satisfiable
check. Appending minus before `var` assumes false, not appending it
assumes true.
satisfiable():: Checks if clauses are satisfiable with given
assumptions. Returns true or false accordingly.
max_satisfiable():: Generates maximal satisfiable subset of assumptions.
Can be called only after `satisfiable`. Returns set of all assumptions
that can be assumed at the same time. Note that this reassumes previous
assumptions, so they are again valid for next `satisfiable` call.
After calling `satisfiable` you can access assigned values by indexing
object with variable you are interested in. It returns true or false.
It can also return nil if variable was added after `satisfiable` method
call.
Others
------
......
......@@ -83,3 +83,7 @@ script::
dep-and, dep-or, dep-not::
Dependency composition objects. They contain the field `sub`, which
is a table of sub-dependencies.
dep-package::
Package description from dependencies. It must contain field `name`
containing name of package group and optionally also field
`version` containing version limitations.
Copyright (c) 2006 - 2014, Armin Biere, Johannes Kepler University.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
deal in the Software without restriction, including without limitation the
rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
IN THE SOFTWARE.
news for release 960 since 959
------------------------------
* fixed various issues pointed out by Stefan Hengelein:
- fixed incremental usage of 'picosat_adjust'
- added CPP fixes (STATS, NO_BINARY_CLAUSE versus TRACE mix-ups)
- removed redundant explicit set to zero on reset
* fixed various usage bugs with 'picomus' (thanks to Stefan Hengelein)
* removed '-fno-strict-aliasing' (thanks to Jerry James)
news for release 959 since 953
------------------------------
* fixed header comments
* fixed minor compilation issues
* fixed unitialized memory access problem for 'picosat_deref_partial'
and another issue with partial models
* added 'picosat_add_arg' and 'picosat_add_lits'
* '--plain' and 'picosat_set_plain' to disable failed literal probing
* new '#define PICOSAT_REENTRANT_API' in 'picosat.h'
* added manager so no more global variables
(allows multiple instances, requires manager object)
news for release 951 since 941
------------------------------
* cleaned up code (based on comments by Donald Knuth)
* lreduce=O(conflicts^.5)
* added 'picosat_visits' and 'picosat_decisions'
* added '--partial' command line option
* added 'picosat_deref_partial' and 'picosat_save_original_clauses'
* added 'picomcs' as example for MSS computation
news for release 941 since 936
------------------------------
* added 'picogcnf'
* added All-SAT mode ('--all' command line option)
* statistics include time spent in failed literal preprocessing (probing)
* 'picosat_failed_context' for 'push & pop'
(and tested failed assumptions for 'push & pop')
* 'picosat_simplify' for forced garbage collection
* undefined NFL, defined NADC (= failed literals on, ADC's off)
* 'picosat_push' and 'picosat_pop' (beta version)
* fixed some issues related to binary clause handling and
generating list of failed assumptions
news for release 936 since 935
------------------------------
* simple minimal unsatisfiable core (MUS) extractor 'picomus'
(example for using 'picosat_mus_assumptions' and 'picosat_coreclause')
* added 'picosat_mus_assumptions'
* added 'picosat_{set_}propagations'
* new 'int' return value for 'picosat_enable_trace_generation' to
check for trace code being compiled
news for release 935 since 926
------------------------------
* added 'picosat_failed_assumptions' (plural)
* new '-A <failedlits>' command line option
* fixed failed assumption issues
* added 'picosat_remove_learned'
* added 'picosat_reset_{phases,scores}'
* added 'picosat_set_less_important_lit'
* added 'picosat_res'
news for release 926 since 846
------------------------------
* random initial phase (API of 'picosat_set_default_phase' changed)
* fixed accumulative failed assumption (multiple times)
* fixed missing original clause in core generation with assumptions
* fixed debugging code for memory allocation
* shared library in addition to static library
* removed potential UNKNOWN result without decision limit
* added picosat_set_more_important_lit
* added picosat_coreclause
* propagation of binary clauses until completion
* fixed API usage 'assume;sat;sat'
* literals move to front (LMTF) during traversal of visited clauses
* switched from inner/outer to Luby style restart scheduling
* less agressive reduce schedule
* replaced watched literals with head and tail pointers
* add 'picosat_failed_assumption', which allows to avoid tracing and core
generation, if one is only interested in assumptions in the core
* fixed a BUG in the generic iterator code of clauses
(should rarely happen unless you use a very sophisticated malloc lib)
news for release 846 since 632
------------------------------
* cleaned up assumption handling (actually removed buggy optimization)
* incremental core generation
* experimental 'all different constraint' handling as in our FMCAD'08 paper
* new API calls:
- picosat_add_ado_lit (add all different object literal)
- picosat_deref_top_level (deref top level assignment)
- picosat_changed (check whether extension was possible)
- picosat_measure_all_calls (per default do not measure adding time)
- picosat_set_prefix (set prefix for messages)
* 64 bit port (and compilation options)
* optional NVSIDS visualization code
* resource controlled failed literal implementation
* disconnect long clauses satisfied at lower decision level
* controlling restarts
These are the sources of the PicoSAT solver.
The preprocessor is not included.
To compile run './configure && make'.
The API is document in 'picosat.h'.
See also 'NEWS' and 'LICENSE'.
This diff is collapsed.
#!/bin/sh
satcompetition=no
log=no
debug=no
stats=undefined
trace=undefined
static=yes
shared=no
thirtytwobit=no
static=no
while [ $# -gt 0 ]
do
case $1 in
-g|--debug) debug=yes;;
-O|--optimize) debug=no;;
-l|--log) log=yes;;
-s|--stats) stats=yes;;
-t|--trace) trace=yes;;
--no-stats) stats=no;;
--no-trace) trace=no;;
-32|--32|-m32) thirtytwobit=yes;;
-static|--static) static=yes;;
-shared|--shared) shared=yes;;
*) cat <<EOF
usage: ./configure [<option> ...]
where <option> is one of the following:
-g|--debug include debugging code and symbols
-O|--optimize optimized compilation (default)
-l|--log add low level logging code (default with '-g')
-s|--stats more expensive statististcs (default with '-g')
-t|--trace trace generation (more memory, default with '-g')
--no-stats disable expensive stats
--no-trace enable trace generation
-32|--32|-m32 compile for 32 bit machine even on 64 bit host
-static|--static produce static binary
-shared|--shared produce shared library
EOF
exit 1
;;
esac
shift
done
echo "version ... `cat VERSION`"
if [ $satcompetition = yes ]
then
debug=no
stats=no
trace=no
thirtytwobit=yes
static=yes
shared=no
fi
echo "debug ... $debug"
echo "log ... $log"
[ $stats = undefined ] && stats=$debug
echo "stats ... $stats"
[ $trace = undefined ] && trace=$debug
echo "trace ... $trace"
echo "static ... $static"
echo "shared ... $shared"
[ "X$CC" = X ] && CC=gcc
if [ X"$CFLAGS" = X ]
then
case X"$CC" in
*wine*|*mingw*) CFLAGS="-DNGETRUSAGE -DNALLSIGNALS";;
*);;
esac
[ $log = yes ] && CFLAGS="$CFLAGS -DLOGGING"
[ $stats = yes ] && CFLAGS="$CFLAGS -DSTATS"
[ $trace = yes ] && CFLAGS="$CFLAGS -DTRACE"
[ $static = yes ] && CFLAGS="$CFLAGS -static"
case X"$CC" in
X*gcc*)
CFLAGS="$CFLAGS -Wall -Wextra"
[ $thirtytwobit = yes ] && CFLAGS="$CFLAGS -m32"
if [ $debug = yes ]
then
CFLAGS="$CFLAGS -g3 -ggdb"
else
CFLAGS="$CFLAGS -DNDEBUG -O3"
fi
;;
*)
if [ $debug = yes ]
then
CFLAGS="$CFLAGS -g"
else
CFLAGS="$CFLAGS -O"
fi
;;
esac
fi
TARGETS="picosat picomcs picomus picogcnf libpicosat.a"
if [ $shared = yes ]
then
TARGETS="$TARGETS libpicosat.so"
CFLAGS="$CFLAGS -fPIC"
fi
echo "targets ... $TARGETS"
echo "cc ... $CC"
echo "cflags ... $CFLAGS"
printf "makefile ..."
rm -f makefile
sed \
-e "s,@CC@,$CC," \
-e "s,@CFLAGS@,$CFLAGS," \
-e "s,@TARGETS@,$TARGETS," \
makefile.in > makefile
echo " done"
#include <signal.h>
#include <stdlib.h>
#include <string.h>
#include "picosat.h"
int picosat_main (PicoSAT **, int, char **);
static PicoSAT * ps;
static int catched;
static void (*sig_int_handler);
static void (*sig_segv_handler);
static void (*sig_abrt_handler);
static void (*sig_term_handler);
#ifndef NALLSIGNALS
static void (*sig_kill_handler);
static void (*sig_xcpu_handler);
static void (*sig_xfsz_handler);
#endif
static void
resetsighandlers (void)
{
(void) signal (SIGINT, sig_int_handler);
(void) signal (SIGSEGV, sig_segv_handler);
(void) signal (SIGABRT, sig_abrt_handler);
(void) signal (SIGTERM, sig_term_handler);
#ifndef NALLSIGNALS
(void) signal (SIGKILL, sig_kill_handler);
(void) signal (SIGXCPU, sig_xcpu_handler);
(void) signal (SIGXFSZ, sig_xfsz_handler);
#endif
}
static void
message (int sig)
{
picosat_message (ps, 1, "");
picosat_message (ps, 1, "*** CAUGHT SIGNAL %d ***", sig);
picosat_message (ps, 1, "");
}
static void
catch (int sig)
{
if (!catched)
{
message (sig);
catched = 1;
picosat_stats (ps);
message (sig);
}
resetsighandlers ();
raise (sig);
}
static void
setsighandlers (void)
{
sig_int_handler = signal (SIGINT, catch);
sig_segv_handler = signal (SIGSEGV, catch);
sig_abrt_handler = signal (SIGABRT, catch);
sig_term_handler = signal (SIGTERM, catch);
#ifndef NALLSIGNALS
sig_kill_handler = signal (SIGKILL, catch);
sig_xcpu_handler = signal (SIGXCPU, catch);
sig_xfsz_handler = signal (SIGXFSZ, catch);
#endif
}
int
main (int argc, char **argv)
{
int res, verbose;
for (verbose = argc - 1; verbose; verbose--)
if (!strcmp (argv[verbose], "-v"))
break;
if (verbose)
setsighandlers ();
res = picosat_main (&ps, argc, argv);
if (verbose)
resetsighandlers ();
return res;
}
CC=@CC@
CFLAGS=@CFLAGS@
all: @TARGETS@
clean:
rm -f picosat picomcs picomus picogcnf
rm -f *.exe *.s *.o *.a *.so *.plist
rm -f makefile config.h
rm -f gmon.out *~
analyze:
clang --analyze $(CFLAGS) *.c *.h
picosat: libpicosat.a app.o main.o
$(CC) $(CFLAGS) -o $@ main.o app.o -L. -lpicosat
picomcs: libpicosat.a picomcs.o
$(CC) $(CFLAGS) -o $@ picomcs.o -L. -lpicosat
picomus: libpicosat.a picomus.o
$(CC) $(CFLAGS) -o $@ picomus.o -L. -lpicosat
picogcnf: libpicosat.a picogcnf.o
$(CC) $(CFLAGS) -o $@ picogcnf.o -L. -lpicosat
app.o: app.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
picomcs.o: picomcs.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
picomus.o: picomus.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
picogcnf.o: picogcnf.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
main.o: main.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
picosat.o: picosat.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
version.o: version.c config.h makefile
$(CC) $(CFLAGS) -c $<
config.h: makefile VERSION mkconfig # and actually picosat.c
rm -f $@; ./mkconfig > $@
libpicosat.a: picosat.o version.o
ar rc $@ picosat.o version.o
ranlib $@
SONAME=-Xlinker -soname -Xlinker libpicosat.so
libpicosat.so: picosat.o version.o
$(CC) $(CFLAGS) -shared -o $@ picosat.o version.o $(SONAME)
.PHONY: all clean
#!/bin/sh
die () {
echo "*** mkconfig: $*" 1>&2