repo.or.cz
/
cl-satwrap.git
/
search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
log
|
graphiclog1
|
graphiclog2
|
commit
|
commitdiff
|
tree
|
refs
|
edit
|
fork
first
·
prev
·
next
.gitignore update
2011-05-09
Utz-Uwe
Haus
.
giti
g
nore update
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2011-05-09
U
tz-Uwe H
a
u
s
fixe
s
fo
r
pa
c
kag
e
name confusion in swig-l
i
spify
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Reduce consing in fl
u
sh-
t
o-b
a
ckend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
H
aus
Add v
e
ctor v
a
riant for
c
lause-valid method
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uw
e
Haus
Reduce consing
a
nd recursion in split-delimited-
s
tring
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Allow assumptions to be lists or ve
c
tors in backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe Ha
u
s
Avoid double mapping
f
r
om
s
ymboli
c
li
t
e
rals to vari
a
ble
s
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
F
i
x
NNF
g
enerat
i
on if explici
t
:ATOMs are used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
fix add-formula to drop :AN
D
and :OR-symbols befo
r
e
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
F
i
x macro expansion tim
e
conf
u
sion
in with-index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-
U
we Haus
remove debugging
output and ensure empty clau
s
es are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe
Haus
Fix
c
all to minisat solve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fix no
n
-cnf for
m
u
la addition
i
nterface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uw
e
H
aus
Fix with
-
sat-solver mac
r
o t
o
corr
e
ct
l
y r
e
fer
e
nce *def
a
ult
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
(minisat backe
n
d ) Return number of
queued
a
s
sumptions
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Also bui
l
d
min
i
s
at backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Fix assu
m
ption handling in precosat
b
ackend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Ut
z
-
U
w
e Haus
Add CNF
bui
l
der conve
n
ien
c
e fu
n
c
t
ions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
U
tz-Uwe H
a
us
a
d
d-
c
lauses con
v
enience function
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Haus
New meth
o
d synchro
n
i
ze-b
a
ck
e
nd
t
o a
l
low increme
n
tal
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
tz-Uwe Haus
Add
minisat
b
ackend to lisp code,
make it the default
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
Haus
Minimalistic minis
a
t hea
d
e
r
and SWIG i
n
tegration
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
t
z-Uwe Haus
A
u
totoo
l
s set
u
p
for minisat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
H
au
s
F
i
x first line in dimacs format export
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Impor
t
mi
n
isa
t
2-070721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Hau
s
Really fix memory i
s
sue:
Precosat Solver->reset() was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uw
e
Haus
Fix with-inde
x
-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-U
w
e Ha
u
s
Properl
y
dispose of precosat
o
bjects
.
commit
|
commitdiff
|
tree
2010-06-01
U
tz
-
Uwe Hau
s
Add get-
e
ssen
t
ial-variables implementation
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree