Commit 8573e2f5 authored by Karel Koci's avatar Karel Koci 🤘

Print proofs from picosat when result is unsatisfiable

This prints a lot of text, but syslog should handle it. This should
allows us to found out why sat concluded result it concluded when we
encounter some bugs.
parent 2db5f1ad
......@@ -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 \
......
......@@ -24,7 +24,6 @@ local setmetatable = setmetatable
local unpack = unpack
local table = table
local picosat = picosat
local DBG = DBG
module "sat"
......@@ -92,11 +91,6 @@ 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".
......@@ -107,9 +101,8 @@ function new()
tp = "sat",
_picosat = picosat,
new_batch = new_batch,
clause = clause
}
for _, c in pairs({ 'var', 'assume', 'satisfiable', 'max_satisfiable' }) do
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
......
......@@ -34,6 +34,7 @@ struct picosat {
static int lua_picosat_new(lua_State *L) {
struct picosat *ps = lua_newuserdata(L, sizeof *ps);
ps->sat = picosat_init(); // Always successful. Calls abort if fails.
picosat_enable_trace_generation(ps->sat);
// Set corresponding meta table
luaL_getmetatable(L, PICOSAT_META);
lua_setmetatable(L, -2);
......@@ -63,22 +64,37 @@ static int lua_picosat_clause(lua_State *L) {
struct picosat *ps = luaL_checkudata(L, 1, PICOSAT_META);
int count = lua_gettop(L) - 1;
if (count < 1)
return luaL_error(L, "picosat:clause requires at least one argument");
return luaL_error(L, "clause requires at least one argument");
FILE *dbg = NULL;
char *dbg_buff;
size_t dbg_len;
if (WOULD_DBG())
dbg = open_memstream(&dbg_buff, &dbg_len);
if (dbg) fputs("clause: ", dbg);
for (int i = 0; i < count; i++) {
int var = luaL_checkinteger(L, i + 2);
ASSERT(var != 0);
if (dbg) fprintf(dbg, "%d ", var);
picosat_add(ps->sat, var);
}
picosat_add(ps->sat, 0);
picosat_add(ps->sat, 0); // close clause
if (dbg) {
fclose(dbg);
DBG("%s", dbg_buff);
free(dbg_buff);
}
return 0;
}
static int lua_picosat_assume(lua_State *L) {
struct picosat *ps = luaL_checkudata(L, 1, PICOSAT_META);
if (lua_gettop(L) < 2)
return luaL_error(L, "picosat:assume requires one argument.");
return luaL_error(L, "assume requires one argument.");
int assum = luaL_checkinteger(L, 2);
ASSERT(assum != 0);
DBG("assume %d", assum);
picosat_assume(ps->sat, assum);
return 0;
}
......@@ -86,25 +102,54 @@ static int lua_picosat_assume(lua_State *L) {
static int lua_picosat_satisfiable(lua_State *L) {
struct picosat *ps = luaL_checkudata(L, 1, PICOSAT_META);
int res = picosat_sat(ps->sat, -1);
ASSERT(res != PICOSAT_UNKNOWN); // Unknown should never happen. We don't limit number of decisions.
ASSERT_MSG(res == PICOSAT_SATISFIABLE || res == PICOSAT_UNSATISFIABLE, "We expect only SATISFIABLE and UNSATISFIABLE from picosat.");
lua_pushboolean(L, res == PICOSAT_SATISFIABLE);
if (!WOULD_DBG())
return 1;
if (res == PICOSAT_SATISFIABLE) {
DBG("satisfiable");
} else {
char *buffer;
size_t len;
FILE *file = open_memstream(&buffer, &len);
ASSERT(file);
picosat_write_compact_trace(ps->sat, file);
fclose(file);
buffer[len - 1] = '\0'; // Dump last char, picosat always ends this output with new line char.
DBG("unsatisfiable, trace follows\n%s", buffer);
free(buffer);
}
return 1;
}
static int lua_picosat_max_satisfiable(lua_State *L) {
struct picosat *ps = luaL_checkudata(L, 1, PICOSAT_META);
lua_newtable(L);
if (picosat_inconsistent(ps->sat))
if (picosat_inconsistent(ps->sat)) {
DBG("max-assume: "); // For consistency with following code we print this not saying line.
// If there is some empty clause, then there are no valid assumptions, return empty table.
return 1;
}
FILE *dbg = NULL;
char *dbg_buff;
size_t dbg_len;
if (WOULD_DBG())
dbg = open_memstream(&dbg_buff, &dbg_len);
if (dbg) fputs("max-assume: ", dbg);
// TODO this might be faster if we would set phase for assumptions to true. See picosat documentation for more details.
const int *assum = picosat_maximal_satisfiable_subset_of_assumptions(ps->sat);
while(*assum != 0) {
if (dbg) fprintf(dbg, "%d ", *assum);
lua_pushinteger(L, *assum);
lua_pushboolean(L, true);
lua_settable(L, -3);
assum++;
}
if (dbg) {
fclose(dbg);
DBG("%s", dbg_buff);
free(dbg_buff);
}
return 1;
}
......
......@@ -105,6 +105,10 @@ void log_internal(enum log_level level, const char *file, size_t line, const cha
}
}
bool would_log(enum log_level level) {
return (level <= syslog_level) || (level <= stderr_level);
}
void log_syslog_level(enum log_level level) {
syslog_level = level;
}
......
......@@ -47,6 +47,14 @@ void log_internal(enum log_level level, const char *file, size_t line, const cha
#define ASSERT_MSG(COND, ...) do { if (!(COND)) DIE(__VA_ARGS__); } while (0)
#define ASSERT(COND) do { if (!(COND)) DIE("Failed assert: " #COND); } while (0)
// If prepare of log would be long, check if it would be printed first.
bool would_log(enum log_level level);
#define WOULD_ERROR() would_log(LL_ERROR)
#define WOULD_WARN() would_log(LL_WARN)
#define WOULD_INFO() would_log(LL_INFO)
#define WOULD_DBG() would_log(LL_DBG)
enum log_level log_level_get(const char *str) __attribute__((nonnull));
// Sets if state and error should be dumped into files in /tmp/updater-state directory
......
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