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
Ut
z
-Uwe Hau
s
Allow
assump
t
ions to be l
i
sts or vect
o
r
s
in backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-
U
we Ha
u
s
Avoid double mappin
g
fr
o
m sym
b
olic l
i
te
r
als to variables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uw
e
Ha
u
s
F
i
x
N
NF gen
e
ration if expli
c
it :ATOMs
a
re used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uw
e
Haus
f
i
x add-formula to d
r
op :AN
D
and :O
R
-symbols before
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-U
w
e H
a
us
F
ix macro
exp
a
nsio
n
time confusion in
with-index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Ut
z
-Uwe Haus
remove debugg
i
ng output an
d
e
n
sure
em
p
ty clau
s
es are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe H
a
us
F
i
x
call t
o
m
i
nisat s
o
lve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
tz-Uwe Haus
F
i
x non-cnf formula addition
i
nterfac
e
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uwe Haus
Fix with-sat-so
l
ver macro to correctly
r
e
ference *d
e
fault
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
(minisa
t
backend )
R
et
u
rn n
u
mber
of
queued as
s
umptions
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uw
e
H
a
u
s
A
l
so build
minisat
b
ackend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Hau
s
Fix as
s
u
mpti
o
n
ha
n
dling in
p
recosa
t
backen
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-
U
we H
a
us
Add CNF buil
d
e
r conve
n
ience
functions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-
U
we Haus
add
-
clauses convenience
f
unction
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Haus
N
e
w
meth
o
d synchronize-backend to allow in
c
r
ement
a
l
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz
-
U
w
e Haus
Add
minisa
t
backen
d
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
Mi
n
i
m
al
i
sti
c
minis
a
t header and SWIG in
t
eg
r
ation
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz
-
Uwe
H
aus
Aut
o
tools
setup for minisat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Fix fi
r
st line in dimacs format export
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
H
aus
Impo
r
t
mi
n
i
s
at2-070721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z
-
Uwe Haus
Really fix
m
emor
y
issue
:
P
r
ecosat Solver->reset() w
a
s
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe
H
aus
Fi
x
with-index-ha
s
h
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Pro
p
erly d
i
spose of preco
s
a
t
object
s
.
commit
|
commitdiff
|
tree
2010-06-01
U
tz-U
w
e
H
aus
Add get-essentia
l
-va
r
iables impleme
n
ta
t
ion
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree