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
Utz-Uwe
Haus
Allow assumptions t
o
b
e
li
s
ts or
vectors i
n
backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Avoid
double m
a
pp
i
ng f
r
om sym
b
ol
i
c literals
t
o va
r
i
a
bles
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz
-
Uwe
H
aus
Fix NNF
generation if expl
i
cit :A
T
OMs are used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe Haus
fix add-for
m
ula to
d
rop
:A
N
D
a
nd :OR-symbols before
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Ha
u
s
Fix macro e
x
pans
i
on time con
f
u
s
i
o
n in with-i
n
dex-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz
-
Uwe Haus
remove de
b
ugging output a
n
d ensure
empty clau
s
es
a
re
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
tz-Uwe Haus
Fix c
a
l
l to min
i
sat solve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-
U
we Haus
Fix non-
c
nf formula
a
ddi
t
ion
i
nter
f
ace
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uwe
Haus
Fi
x
with-sat-solver macro to c
o
r
r
e
c
tly
reference *default
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Ut
z
-
U
we Hau
s
(minisat backe
n
d )
R
eturn n
u
mber of queued assu
m
pt
i
ons
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
A
lso build minisa
t
backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-
U
we Hau
s
Fix assumptio
n
h
andling i
n
p
rec
o
sat backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-U
w
e Ha
u
s
Add CNF
builder convenience
f
unct
i
ons
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz
-
Uwe Ha
u
s
add-clauses conven
i
ence fun
c
tion
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Haus
New method sync
h
roni
z
e-backend to
allow incremental
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Add minis
a
t backend to lisp code, make it
the
d
efaul
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Min
i
malistic minisat
h
ead
e
r and SWIG
integrat
i
on
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Autotools setup for minisat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
F
i
x first
line in dima
c
s
format export
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-U
w
e
Ha
u
s
Import mini
s
at2-070721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Really fix memory
i
ssue: Precos
a
t
S
olver->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 with-index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Prop
e
rly dispo
s
e
of
p
re
c
osat objects
.
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
we Haus
Add get-es
s
enti
a
l-variables implementat
i
on
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree