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-U
w
e
Haus
Add
v
ector variant
for cla
u
se-
v
alid method
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe Haus
Reduce co
n
sing and recursion
i
n split-d
e
l
i
mite
d
-s
t
ring
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Allow
assumptions
t
o be l
i
sts or vector
s
i
n
back
e
nd
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Haus
Av
o
id doub
l
e mapping from symbol
i
c litera
l
s to v
a
r
iables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe
H
aus
Fix NNF
g
e
n
eratio
n
if exp
l
icit :A
T
OMs a
r
e used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-Uwe Haus
fi
x
add-f
o
rmu
l
a t
o
d
rop :AND an
d
:OR-symb
o
ls before
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe Haus
Fix
ma
c
ro ex
p
ans
i
on time confu
s
i
o
n
in with-index-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Hau
s
remov
e
de
b
u
g
ging o
u
tput
a
nd ensure
e
m
p
t
y c
l
auses
a
re
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
U
tz-Uwe Haus
F
i
x call to minisat so
l
ve()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-U
w
e Haus
Fix no
n
-cnf form
u
la addition in
t
erface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Ut
z
-U
w
e
Haus
Fix wit
h
-sat-solver macro to corr
e
c
tly reference *default
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
U
tz-Uwe H
a
us
(minisat bac
k
end ) Return number
o
f queued ass
u
mptions
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Also build minisa
t
ba
c
kend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Ha
u
s
F
i
x assumpti
o
n
h
andlin
g
in precosat b
a
ckend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-
U
we Ha
u
s
Add CNF b
u
ilder convenience f
u
n
c
tions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe
Haus
a
d
d
-
clauses
con
v
enience function
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Hau
s
N
e
w method synchroni
z
e-bac
k
end to
a
l
l
ow
i
n
cremen
t
al
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
H
aus
Add minisat backen
d
t
o lisp
c
o
d
e
,
m
ake it the de
f
au
l
t
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Mi
n
i
m
alistic minisat header and SWIG
i
ntegration
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Autotools s
e
tup for mi
n
isat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Fix first lin
e
in dimacs format e
x
port
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
H
aus
Import minisat2-
0
70
7
21
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Ut
z
-Uwe Haus
Rea
l
l
y
fix memory
issue
:
Prec
o
sat
S
olver->reset() was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
tz
-
Uwe H
a
us
Fix wit
h
-ind
e
x-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Ha
u
s
Properly dispose of precosat
objects
.
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe
Haus
Add get-essen
t
i
a
l
-var
i
ables
i
mplementation
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree