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
Reduce con
s
ing
i
n flush-to-backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-U
w
e Haus
Add vecto
r
varia
n
t for cl
a
use-valid m
e
thod
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-U
w
e
H
a
us
Reduce consing and r
e
cursion
in sp
l
it-delimited-string
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uw
e
Haus
Allow assumptions to be lists or vectors in backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Avoi
d
d
o
ub
l
e
mapping
f
rom sy
m
bolic literals
t
o variabl
e
s
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Fix NNF
genera
t
ion
i
f expl
i
cit :ATOMs are used
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
fi
x
add-f
o
rmula to drop :AND
and :OR
-
symbols be
f
ore
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-
U
w
e
Haus
Fix mac
r
o ex
p
an
s
i
on time confusion in
w
ith-ind
e
x
-hash
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe
H
aus
r
em
o
v
e
deb
u
gging outp
u
t and ensure
empty c
l
auses are
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
U
tz-Uwe Haus
Fix call to minisat
s
olve()
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fix non-cnf fo
r
m
u
la addi
t
ion interface
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uwe Ha
u
s
Fix with-sat
-
sol
v
e
r
m
a
c
ro t
o
correctly
r
eference *default
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
U
tz-Uwe Haus
(
minisat
b
ackend ) Return number of q
u
e
u
ed
ass
u
mptions
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Also build minisat bac
k
end
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-
U
we Haus
F
i
x assumption h
a
ndling in
p
recos
a
t backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Hau
s
Ad
d
CNF b
u
ilder convenie
n
ce fu
n
c
t
ions
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
U
tz-Uwe Haus
add-clauses co
n
venience function
commit
|
commitdiff
|
tree
2010-06-03
U
t
z-Uwe
H
aus
New met
h
od synchronize
-
back
e
nd
t
o
al
l
ow inc
r
e
mental
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe H
a
u
s
Add minisat bac
k
end to lisp
c
ode, make
it
the default
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Hau
s
M
i
n
imalistic minisat header
a
nd SW
I
G in
t
egratio
n
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
U
tz-Uw
e
Haus
Autotoo
l
s setup f
o
r minisat
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Ha
u
s
Fix first li
n
e in d
i
macs form
a
t exp
o
rt
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Import minisat2-070721
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe H
a
u
s
Really fix memor
y
issue: Precosat
S
olver->res
e
t()
w
a
s
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Ut
z
-Uwe Haus
Fix with-
i
ndex
-
h
as
h
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
w
e Haus
Properly
d
i
spose of p
r
e
c
o
s
a
t
objects
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Ut
z
-Uwe Hau
s
A
dd get-essential-var
i
ables
implementatio
n
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-Uwe Haus
Add with-s
a
t-solver and with-index-hash macros
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Add dimacs
r
eader/
w
riter
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z
-Uw
e
Haus
Proper garbage collection of fo
r
eig
n
objects usi
n
g
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Ut
z
-Uwe Haus
SWIG wrapper layer
and
.
i fil
e
for precosat, minima
l
i
stic
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz
-
Uwe
Hau
s
I
m
port precos
a
t-465r2-2ce82ba-1
0
0514
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz
-
Uwe Haus
Initial lay
o
ut
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
