Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
U
updater
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Michal Čihař
updater
Commits
ef888167
Verified
Commit
ef888167
authored
Sep 22, 2016
by
Karel Koci
🤘
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'sat-proof' into updater-ng
parents
2dda016a
1acba6b9
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
63 additions
and
16 deletions
+63
-16
Makefile.dir
Makefile.dir
+2
-2
src/lib/autoload/a_12_sat.lua
src/lib/autoload/a_12_sat.lua
+1
-8
src/lib/picosat.c
src/lib/picosat.c
+53
-6
src/lib/util.c
src/lib/util.c
+4
-0
src/lib/util.h
src/lib/util.h
+3
-0
No files found.
Makefile.dir
View file @
ef888167
LUA_NAME
:=
$(
shell
for
lua
in
lua5.1 lua-5.1 lua51 lua
;
do if
pkg-config
$$
lua
;
then
echo
$$
lua
;
break
;
fi
;
done
)
VALGRIND
:=
IN_VALGRIND
=
1 valgrind
--leak-check
=
full
--show-leak-kinds
=
all
--track-fds
=
yes
--trace-children
=
no
--child-silent-after-fork
=
yes
--error-exitcode
=
1
# For picosat, it otherwise needs some headers not available on musl for a feature we don't need.
EXTRA_DEFINES
:=
NGETRUSAGE
# For picosat, it otherwise needs some headers not available on musl for a feature we don't need.
And we need trace enabled.
EXTRA_DEFINES
:=
NGETRUSAGE
TRACE
include
$(S)/build/Makefile.top
...
...
src/lib/autoload/a_12_sat.lua
View file @
ef888167
...
...
@@ -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_satisfiabl
e'
})
do
for
_
,
c
in
pairs
({
'var'
,
'assume'
,
'
clause'
,
'satisfiable'
,
'max_satisfiable'
,
'print_trac
e'
})
do
sat
[
c
]
=
function
(
sat
,
...
)
return
sat
.
_picosat
[
c
](
sat
.
_picosat
,
unpack
({
...
}))
end
...
...
src/lib/picosat.c
View file @
ef888167
...
...
@@ -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_log
(
LL_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."
);
int
assum
=
luaL_checkinteger
(
L
,
2
);
ASSERT
(
assum
!=
0
);
DBG
(
"assume %d"
,
assum
);
picosat_assume
(
ps
->
sat
,
assum
);
return
0
;
}
...
...
@@ -86,25 +102,56 @@ 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
;
}
...
...
src/lib/util.c
View file @
ef888167
...
...
@@ -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
;
}
...
...
src/lib/util.h
View file @
ef888167
...
...
@@ -47,6 +47,9 @@ 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
);
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
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment