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
U
t
z-U
w
e Ha
u
s
Allow as
s
um
p
tions to be lis
t
s
or vecto
r
s in backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-
Uwe
Ha
u
s
Avoi
d
d
o
ub
l
e ma
p
ping from symbolic
l
iterals to variab
l
es
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uw
e
H
a
us
Fix NNF generation if explicit :ATOMs ar
e
used
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-
U
we Ha
u
s
f
ix a
d
d-formula
to drop :AND and :OR-symbols
befor
e
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Fix
m
a
cro expansion time co
n
fusion in with-
i
nd
e
x-hash
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz
-
Uwe H
a
us
remove debugg
i
ng
output and ensure emp
t
y cl
a
u
s
es are
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz
-
Uwe Hau
s
Fix call to minis
a
t solve()
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fix
non-cnf formula additi
o
n interface
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uwe Haus
Fix with-sat-sol
v
e
r mac
r
o to cor
r
ectly refer
e
nce *defa
u
lt
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe
Haus
(min
i
sa
t
backen
d
) Return num
b
e
r of
q
ueue
d
assumptions
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Hau
s
A
lso bui
l
d minisat
backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
F
i
x
assu
m
ption handl
i
n
g
i
n
precosat ba
c
kend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Haus
Add
C
NF builder convenie
n
ce f
u
nction
s
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Haus
add-clau
s
e
s
convenience
funct
i
on
commit
|
commitdiff
|
tree
2010-06-03
Utz
-
Uwe Haus
New method sy
n
chronize-backend t
o
allow incremental
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uw
e
Hau
s
Add minisat backend
t
o lisp cod
e
, make it the de
f
a
u
lt
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
U
t
z
-
Uwe Haus
Minimalistic
minisat
h
eader and SWI
G
integration
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-
U
we Haus
A
utotoo
l
s
set
u
p
for min
i
sa
t
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-
U
we Haus
Fix fi
r
st line in dim
a
cs format export
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Ut
z
-Uwe Haus
Import minisat2-070721
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Rea
l
ly fix memor
y
issue
:
Precosat Solver
-
>re
s
et()
w
as
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Ut
z
-Uwe Haus
Fix
with-index-ha
s
h
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Proper
l
y dispose o
f
precosat obje
c
ts
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-U
w
e
Haus
Add ge
t
-es
s
ential-v
a
r
iables i
m
pl
e
mentation
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-Uwe Ha
u
s
Add with-sat-solver and wi
t
h-index-hash macros
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz
-
U
w
e Hau
s
Add dimacs reader/writer
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Ha
u
s
Proper garbage collection of
foreign
objects using
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Ha
u
s
SW
I
G wr
a
pper
l
ayer
a
nd
.
i f
i
le for precosa
t
, minimalis
t
ic
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz-
U
we Haus
I
m
port precosa
t
-465r2-
2
c
e
8
2b
a
-100514
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz-Uwe Haus
In
i
t
i
al layout
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree