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
Reduce consing and recursion in split-delimited-string
2010-06-22
Utz-Uwe Hau
s
Reduce consing and r
e
cursion in split
-
delimi
t
ed-string
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
Allow a
s
su
m
ptions to be
l
ist
s
or vectors in bac
k
e
nd
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-Uwe Haus
Avoid d
o
ubl
e
m
apping from symbolic lite
r
als to varia
b
l
e
s
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z
-Uwe Haus
Fix NNF gen
e
ration if explicit :ATOMs are
u
sed
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
fi
x
a
dd-for
m
ul
a
to dr
o
p
:AND and :OR-symbols before
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-U
w
e
Haus
Fix macro exp
a
n
s
i
o
n
tim
e
confu
s
io
n
in
w
ith-index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
remove d
e
bugging
o
u
t
pu
t
a
n
d ensure empty cl
a
u
s
es are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Ut
z
-Uw
e
Ha
u
s
F
i
x
cal
l
to minis
a
t solve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe H
a
us
Fix
non-cnf formula addit
i
on interface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Utz-
U
we Haus
Fix with-sat
-
solver
macro to co
r
r
ectly
r
eferenc
e
*defa
u
lt
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe
H
a
u
s
(minisat backend ) Retu
r
n num
b
e
r
of que
u
ed assumpti
o
ns
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
U
t
z-Uwe Haus
Also bui
l
d minis
a
t b
a
ckend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz
-
Uwe Haus
Fix
assumptio
n
handling in precosat backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe
Haus
Add CNF builde
r
conven
i
enc
e
functions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
U
t
z-Uwe Haus
a
d
d
-clauses convenience
f
u
n
ction
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Haus
New m
e
thod synchron
i
z
e-backe
n
d
to allow incremental
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
tz
-
Uw
e
H
aus
Add minisat
backend to lisp code, make it the defaul
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Ut
z
-U
w
e Hau
s
Minimalisti
c
minis
a
t header and
SWIG
integrati
o
n
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
t
z-Uwe Haus
Autotools setup for minisa
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Fi
x
first l
i
ne in dimacs format
e
x
port
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
t
z-Uwe Haus
Import minisat2
-
070721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Really fix memo
r
y iss
u
e: Precosat Solver->reset() was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Fix
w
ith-in
d
ex
-
hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
tz-Uwe Haus
P
r
operly d
i
s
p
o
se of
p
reco
s
at objec
t
s
.
commit
|
commitdiff
|
tree
2010-06-01
Utz-U
w
e
Haus
A
d
d
get-esse
n
tial-variable
s
implementation
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree