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
Allow assumptions to be lists or vectors in backend
2010-06-22
Utz-
U
we
Haus
Allo
w
assumpt
i
o
ns to be lis
t
s
or vectors in backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Avoid double mapping fro
m
symbolic
l
ite
r
als
to
v
ariables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
Fix N
N
F generation if expli
c
it :A
T
O
M
s
are used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
fix add-f
o
rmula to drop
:
AND and :OR-symb
o
ls befor
e
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
Fix mac
r
o
expansion time confu
s
ion in
w
ith-
i
n
d
ex-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Ut
z
-U
w
e
H
aus
re
m
ove d
e
bug
g
in
g
output and en
s
ure em
p
ty
c
lauses are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fix call to mini
s
at solve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe
Haus
Fix non-c
n
f formul
a
addition interface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uwe Haus
F
i
x with-sat
-
sol
v
er macro
t
o
c
o
r
r
ectly reference *def
a
u
lt
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Ut
z
-Uwe
Haus
(minisat backend ) Return number of q
u
e
ued ass
u
m
ptions
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Ut
z
-Uwe Haus
A
lso bu
i
ld
minisa
t
ba
c
k
en
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
U
tz-Uwe Haus
Fix ass
u
mption hand
l
i
ng in precosa
t
backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uw
e
Haus
Add CNF buil
d
er convenience functions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe
H
aus
add-claus
e
s
c
o
n
v
e
nience function
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe
H
aus
N
ew m
e
thod synchronize-backend to allow incr
e
ment
a
l
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-
U
we Ha
u
s
Add minisat backend to li
s
p code, make it the
de
f
ault
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uw
e
Haus
Minimalistic minisat header and SWIG integration
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Autotools setup for minisat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz
-
Uwe H
a
us
Fix first line
i
n
d
imacs
f
ormat export
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Impor
t
minisat2-070721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
we Haus
R
eally f
i
x
memory issue: Pr
e
cosat So
l
ver->re
s
et() was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z
-Uw
e
Haus
Fix with-index-h
a
s
h
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-U
w
e Hau
s
Prop
e
rly dis
p
ose o
f
prec
o
sat
o
bj
e
cts
.
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
we Haus
Add g
e
t-e
s
sential-variables impleme
n
tation
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree