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 in flush-to-backend
2010-06-22
Ut
z
-Uwe Haus
Re
d
u
c
e consi
n
g
in f
l
ush-
t
o-
b
ackend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-U
w
e Haus
Add v
e
ctor
v
arian
t
f
or cl
a
u
se-vali
d
method
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Hau
s
Reduce
consin
g
a
n
d
recursion in split-
d
e
l
im
i
ted
-
string
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz
-
Uwe
Haus
Allow assum
p
tions to be l
i
sts or vectors
in backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-
U
we H
a
us
Avoid double
m
apping from symbolic litera
l
s to variables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe Haus
F
i
x NNF g
e
ne
r
a
t
ion if e
x
plicit :
A
TOMs
a
re
used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
fi
x
add-formula
to drop :AND a
n
d
:OR-symbols before
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe Haus
F
ix macr
o
expan
s
i
on time confusio
n
in with-index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
r
e
m
ove debuggi
n
g output and ensure empty clauses are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fix ca
l
l to mini
s
a
t
solve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Ut
z
-Uwe Haus
Fix non-cnf formula addition int
e
r
f
a
ce
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Ut
z
-
U
we Hau
s
Fix with-
s
at-solver macro to correctly
referen
c
e *d
e
fault
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe
Haus
(minisat backend
)
R
eturn number
o
f queued assumpti
o
ns
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-U
w
e Haus
Also build
mini
s
at back
e
nd
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe H
a
us
Fix
assumption han
d
ling in
precosat backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-U
w
e
Haus
A
d
d
CNF builder
c
onvenience functions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uw
e
Haus
add-clauses convenience
f
uncti
o
n
commit
|
commitdiff
|
tree
2010-06-03
U
t
z-Uw
e
H
a
us
N
e
w
method s
y
nc
h
ron
i
z
e
-
ba
c
kend
to all
o
w
i
ncremental
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Ad
d
minisat back
e
nd to lisp code,
make it the default
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
H
aus
Mi
n
im
a
listic
minisat he
a
der and
S
WIG integratio
n
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Autotoo
l
s se
t
u
p
for m
i
nis
a
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-U
w
e Haus
Fix first line i
n
dimacs
format expo
r
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
I
m
port mi
n
isat2-
0
70721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
we Haus
Real
l
y
f
ix memory issu
e
: Precosat Solver->re
s
et() was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Fi
x
with-ind
e
x-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Prope
r
ly disp
o
se of pr
e
cosat objects
.
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-Uwe Haus
Ad
d
get-essenti
a
l-v
a
riables impleme
n
tation
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree