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 Haus
Add ve
c
tor variant for clause-valid method
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz
-
Uwe Haus
Re
d
uce consing
a
n
d
r
ecursion in split-delimited-string
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe Hau
s
Allow assumpti
o
ns to b
e
lists or ve
c
t
ors in back
e
nd
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe Haus
Av
o
id double mapping from symbolic lite
r
als
t
o
variables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe H
a
us
F
i
x NNF g
e
neration if ex
p
licit :ATOMs
are used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
fix
add-formula t
o
drop :AND and :OR-symbols
b
efore
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-
U
w
e Haus
Fix macro
expansion time confusion in with-index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
t
z
-Uwe Haus
remov
e
deb
u
gging output and e
n
sure
e
mpty cl
a
uses are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
t
z-Uwe Haus
Fix
c
al
l
to minisat s
o
lve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
t
z-Uwe Haus
Fix non-
c
nf formu
l
a
addition interface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-U
w
e Haus
Fix wi
t
h
-
s
at-s
o
lver mac
r
o to
correctly reference *d
e
f
ault
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
U
tz
-
U
w
e Haus
(
minis
a
t backend )
R
eturn num
b
e
r
of queued assumptions
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Ha
u
s
Als
o
bui
l
d minis
a
t backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
U
t
z
-Uwe Haus
Fix as
s
umpt
i
on handli
n
g in precosat b
a
ckend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Haus
Add C
N
F bui
l
der conveni
e
nce functions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Haus
add-
c
lauses conve
n
i
e
nc
e
function
commit
|
commitdiff
|
tree
2010-06-03
U
tz
-
U
w
e
H
aus
New
m
e
th
o
d
synchronize-b
a
ckend to allow incr
e
m
e
ntal
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Add minisat backend to lisp
c
ode, make it the default
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
H
a
u
s
Minima
l
istic m
i
nisat head
e
r an
d
SW
I
G int
e
gration
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Au
t
otools setup for minisat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Fix first line in dimacs format export
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
I
mport minisat2-0707
2
1
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-
U
we Haus
Rea
l
ly fix memory
issue: Precosat Solver->r
e
set() was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Fi
x
w
ith-inde
x
-h
a
sh
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Ut
z
-Uwe H
a
us
Properly dis
p
os
e
of precosat objec
t
s
.
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe H
a
us
Add
g
et-
e
ssen
t
i
al-variabl
e
s
implementati
o
n
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree