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
fix minisat compile on modern c++ compilers
2016-05-31
u-u
-
h
fix
m
ini
s
a
t compile on
m
odern c++
compilers
commit
|
commitdiff
|
tree
2016-05-30
Utz
-
U
w
e H
a
us
m
o
dern
i
ze a
u
totools usage
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2011-05-13
U
tz-Uwe Hau
s
a
d
d miss
i
ng
c
onfigure
.
ac and ltmain
.
sh in
m
i
n
isa
t
s
u
btr
e
e
commit
|
commitdiff
|
tree
2011-05-09
Utz-Uwe
H
aus
upd
a
te to new
e
r libtool, keep in-tree
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2011-05-09
Ut
z
-
Uwe Haus
another round
o
f
de
f
a
ult test predic
a
t
e
mess
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2011-05-09
U
t
z-Uwe Hau
s
m
e
ssing with def
a
ult
test pre
d
icat
e
in macro again
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2011-05-09
Utz-Uwe Haus
.
giti
g
nore
update
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2011-05-09
Utz-U
w
e
Haus
fixes f
o
r
package name
c
on
f
us
i
on in swig-lispify
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-Uwe Haus
Reduce consing in flush-
t
o-backe
n
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Add vector variant for
clause-valid
m
e
thod
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe Haus
Reduce consing and recursion
in s
p
lit-deli
m
it
e
d
-
stri
n
g
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-Uwe Haus
Allow assumption
s
to be lists or v
e
ctors
i
n
b
acken
d
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz
-
U
w
e
Hau
s
Avoi
d
doub
l
e map
p
ing from symbolic literals
t
o
variables
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Haus
Fix
NNF ge
n
eration if expl
i
cit :ATO
M
s are used
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
Ut
z
-
Uwe Haus
fix add
-
f
o
rmu
l
a t
o
drop :AND and :
O
R-symbo
l
s before
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-22
U
tz-Uwe H
a
us
Fix macro ex
p
a
ns
i
o
n
tim
e
c
o
nf
u
sion in w
i
th-i
n
d
ex-hash
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-U
w
e Haus
remove debu
g
ging outpu
t
an
d
e
n
sure e
m
p
ty claus
e
s are
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
F
ix call to minisat sol
v
e()
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-17
Ut
z
-Uwe
Haus
F
ix non
-
c
n
f formula addition
interface
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-16
Ut
z
-Uwe Haus
Fix with-sat-solver macro to correctly refe
r
ence *defau
l
t
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uw
e
Ha
u
s
(minisat ba
c
kend ) Return n
u
mber of que
u
ed assu
m
ption
s
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Haus
Also build mini
s
at backend
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uwe Hau
s
Fix assumption ha
n
dlin
g
in p
r
e
c
osat b
a
c
k
e
nd
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-U
w
e H
a
us
Add CNF builder convenience fun
c
tions
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-10
Utz-Uwe Haus
add-clauses
c
onvenience function
commit
|
commitdiff
|
tree
2010-06-03
Utz-Uwe Haus
N
e
w m
e
tho
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
U
t
z-
U
we Haus
A
dd minisat backend
to l
i
sp code, make it the default
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-
U
we
H
aus
Minimalistic m
i
nisat
header and SWIG in
t
eg
r
a
t
io
n
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Hau
s
A
u
totools
s
etup f
o
r
minisat
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
F
ix firs
t
line in dimac
s
format
e
x
p
ort
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-02
U
t
z-Uwe Haus
Import minisat2
-
0
7
0721
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe
H
aus
Really
fix memory issue: Precosat
S
o
l
ver
-
>reset() was
.
.
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Fix wi
t
h-index
-
h
a
sh
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
2010-06-01
U
tz-Uwe Hau
s
Pro
p
erly
dispose
o
f pr
e
cosat o
b
jects
.
commit
|
commitdiff
|
tree
2010-06-01
Utz
-
Uwe Haus
Add get-esse
n
tial-varia
b
le
s
impl
e
men
t
a
t
ion
.
Signed-off-by: Utz-Uwe Haus <
lisp@uuhaus.de
>
commit
|
commitdiff
|
tree
