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
Utz-Uwe
H
aus
Reduce
consing in
flush-
t
o-b
a
ckend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uw
e
Haus
Add
vector variant for clause-v
a
lid method
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-
U
w
e H
a
us
Reduce
c
onsing
a
nd rec
u
rsion
i
n sp
l
it
-
d
e
li
m
i
te
d
-stri
n
g
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe H
a
us
A
l
low a
s
sumpti
o
n
s to be
lists or
vectors in ba
c
kend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Avoid double mapping f
r
o
m
symbolic literals to variables
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Fix NNF generation if e
x
pli
c
it :AT
O
Ms
a
re used
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-
U
we
Haus
fix add-formula to dr
o
p :AND
a
n
d
:OR-symbols
b
efore
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-Uwe Haus
Fix macro expans
i
on
t
im
e
c
onfu
s
ion in with-index-hash
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
remove debugg
i
n
g
output and ensure empty clauses are
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-
U
we Haus
Fix
c
all to minisat solve()
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
U
tz-Uwe
Haus
Fix non-cnf f
o
rmula add
i
t
i
o
n interface
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-16
U
tz-Uwe
H
a
u
s
Fix
with-s
a
t-solver m
a
cro
t
o
c
orrectly refe
r
e
n
ce *de
f
ault
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
(mini
s
at
ba
c
kend ) Ret
u
r
n numbe
r
o
f
queued
a
ssumptio
n
s
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uw
e
Haus
Also
build
m
inisat bac
k
en
d
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Fix assumption handling in precosat backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Hau
s
Ad
d
CNF buil
d
er convenience
f
u
nction
s
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uw
e
Haus
ad
d
-clauses convenience function
commit
|
commitdiff
|
tree
2010-06-03
Utz-U
w
e
Haus
New m
e
tho
d
synchro
n
ize-
b
ac
k
end
t
o allo
w
incremen
t
al
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-
U
we Haus
Add min
i
sa
t
b
ack
e
nd
to lisp co
d
e, make it
the
d
efault
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Mi
n
imalistic minisat head
e
r and SWIG in
t
eg
r
atio
n
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-U
w
e H
a
us
Autotools setup for minisat
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uw
e
Haus
Fix first li
n
e i
n
dimacs format expor
t
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Imp
o
rt min
i
sat2-070721
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-U
w
e H
a
us
R
eally
fi
x
memory issue: Precosat Solv
e
r-
>
reset() w
a
s
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
F
i
x wi
t
h-in
d
ex-hash
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z
-
Uwe Ha
u
s
Prop
e
rly
d
i
s
pose of precosat ob
j
ects
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
we
H
aus
Add g
e
t-es
s
ential-variables imp
l
ementation
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe H
a
us
A
d
d with-sat-solver and with-index-hash macros
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-Uw
e
Haus
Add dima
c
s
r
eader/write
r
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Hau
s
Prop
e
r garbag
e
c
o
l
lection of
f
orei
g
n
objects using
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
SWIG wrapper layer and
.
i fi
l
e for
p
re
c
osat, minimalistic
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz-Uwe H
a
us
Import
p
recosat-465r2-2ce82ba-10051
4
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz-Uwe Haus
I
nitial la
y
out
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree