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
Reduce consing and recursion in split-delimited-string
2010-06-22
U
t
z
-
Uwe Haus
Reduce
consing and recursion in split-delimited
-
s
tring
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe Hau
s
Allow assumptions to be lists or
vectors in
backen
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe Haus
Avo
i
d doub
l
e mappin
g
from symbol
i
c lit
e
r
a
ls
to variables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-U
w
e Haus
F
ix NNF genera
t
ion i
f
explicit
:
A
T
OMs are
u
sed
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
H
aus
f
i
x
add-
f
o
r
m
u
la to drop :AND
and
:
OR-sym
b
o
l
s b
e
fore
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe
H
a
us
Fix macro ex
p
an
s
io
n
time con
f
usion in with
-
index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe
Haus
remov
e
debu
g
ging output
a
n
d
en
s
ure
e
mpt
y
cl
a
uses
are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fix call
t
o
m
i
n
i
sa
t
sol
v
e()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fi
x
non
-
cnf
f
o
r
mula additi
o
n i
n
t
e
rface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uw
e
Haus
Fix w
i
th-sat-solver mac
r
o
to corre
c
tly
r
e
f
erence
*defa
u
lt
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
(min
i
s
a
t ba
c
ke
n
d ) Return number o
f
queued ass
u
mptions
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Als
o
b
uild minisat back
e
nd
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
F
ix
assumption handling i
n
precosat backe
n
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz
-
Uw
e
Haus
Add CNF builder convenience fun
c
tions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Ut
z
-
U
w
e
Haus
add-clauses con
v
enienc
e
f
unction
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Haus
New method synchronize-
b
ackend to
all
o
w
in
c
remental
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Add
minisat backend 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 minisat header and SWIG
i
ntegratio
n
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Ut
z
-U
w
e Hau
s
Au
t
otools setup for
m
i
n
isat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Fix f
i
rst line in
d
im
a
cs format ex
p
ort
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Ut
z
-Uwe Haus
Import minisat
2
-070721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz
-
U
w
e Haus
Really
fi
x
memo
r
y issue: Precosat
S
o
lver->reset() w
a
s
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz
-
U
w
e Haus
Fix with-
i
ndex-h
a
sh
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
tz-
U
we
H
aus
Properly dispose
of precosat
objects
.
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-Uwe
H
a
us
Add get-
e
ssential-variabl
e
s i
m
plementation
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree