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
Add vector variant for clause-valid method
2010-06-22
Utz
-
Uwe
H
a
us
Add vector
variant for clause-valid method
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz
-
U
w
e Haus
Re
d
uce co
n
sing
and rec
u
rsion in
split-
d
elimited-str
i
ng
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
H
aus
Allow assumptions to be l
i
s
ts
o
r
v
ector
s
in b
a
ckend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe H
a
us
Avoid double mapping from symbolic
l
iterals to
v
aria
b
les
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe H
a
us
Fix NNF generation if
e
xp
l
icit :ATOMs
a
re
u
sed
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
H
aus
fix add-for
m
ula to d
r
op
:A
N
D and :
O
R-symbols before
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-
U
we Haus
Fix
macro expansion time confu
s
ion in with-index-ha
s
h
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
tz-Uw
e
H
a
u
s
remove debugging
o
utp
u
t and ensur
e
empty clauses are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fi
x
call to mini
s
at solve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uw
e
Haus
Fix non-cnf
formula addition i
n
terface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uwe
H
aus
F
ix with-sat-solver mac
r
o to correctl
y
re
f
erence *default
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe
H
aus
(minisat
backend
)
Return n
u
mber of queued assumpti
o
n
s
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Also bu
i
ld min
i
sat ba
c
ke
n
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Ut
z
-Uw
e
H
a
us
Fi
x
assum
p
tio
n
handling in precosat
b
ackend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uw
e
H
aus
A
dd
C
NF builder convenience fu
n
ctio
n
s
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Haus
add-clauses conveni
e
nc
e
funct
i
on
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Haus
New method synchronize-backend to allow incr
e
mental
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Ha
u
s
Add mini
s
at backen
d
to lis
p
c
o
de, m
a
ke 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 he
a
der and S
W
IG
i
nteg
r
ation
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
Ut
z
-Uwe Haus
Fix
f
irst li
n
e
in dimacs format export
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
tz-Uwe
H
a
u
s
Impo
r
t
mi
n
isat2-070721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Really fi
x
memory issue: Precosat
So
l
ver
-
>reset(
)
was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
F
i
x w
i
th-ind
e
x-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Ut
z
-Uwe Ha
u
s
Properly di
s
pose of p
r
ecosat
o
bjects
.
commit
|
commitdiff
|
tree
2010-06-01
Utz-U
w
e
Haus
Add get-essentia
l
-v
a
r
i
ables imp
l
ementation
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
