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 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
Avoid double ma
p
ping from
s
ymb
o
l
ic lit
e
rals
t
o
v
a
r
iables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-
U
we Haus
Fix NNF generation if
e
xp
l
icit :ATOMs are us
e
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
fix add-f
o
rmula to drop :AN
D
a
nd :
O
R-symbols
b
e
fore
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
Fix macro e
x
pansion
t
ime confus
i
on in wi
t
h-inde
x
-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe
H
aus
remove de
b
ugging output and ensure empt
y
clauses are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
t
z-Uwe Haus
Fix call to minisa
t
solve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
t
z-Uwe Haus
Fix non-cnf formul
a
a
dd
i
t
i
on i
n
terface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz
-
Uw
e
Ha
u
s
Fix with-sat-s
o
l
v
e
r macro
t
o correct
l
y reference *defaul
t
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
U
t
z-
U
we Haus
(m
i
nisat back
e
nd
)
Return
n
u
mber
of queued ass
u
mptio
n
s
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uw
e
Ha
u
s
Also b
u
ild minis
a
t backe
n
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
U
tz-U
w
e H
a
us
Fix assu
m
ption handling in
preco
s
a
t
b
a
cken
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
U
tz-Uwe
H
a
u
s
Add
C
NF b
u
ilder co
n
venien
c
e functio
n
s
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
U
t
z-Uwe Haus
add-
c
lau
s
e
s conv
e
nien
c
e function
commit
|
commitdiff
|
tree
2010-06-03
Utz-
U
we Haus
New
m
etho
d
syn
c
hron
i
z
e
-backend to
a
l
l
ow incremental
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe H
a
us
Add minisat b
a
ckend to lisp code, make it the de
f
au
l
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-
U
we
H
au
s
Minimalistic minisat
h
eader and SWIG
i
ntegration
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
tz-
U
w
e Haus
Au
t
otools
setup
f
o
r
minisat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uw
e
Ha
u
s
Fix first
line in dima
c
s format exp
o
r
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
Haus
I
m
port m
i
nis
a
t
2-
0
70721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
we Haus
R
e
a
lly fix memory issue: Precosat
So
l
ver-
>
reset
(
) was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
tz-Uw
e
Hau
s
Fix with-i
n
dex-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uw
e
Hau
s
Properly dispos
e
of precosat obje
c
ts
.
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe
H
aus
A
d
d
get-essential-variables implementa
t
i
o
n
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree