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 in flush-to-backend
2010-06-22
U
tz-
U
w
e
Haus
Reduce consin
g
in flush-to
-
backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-U
w
e H
a
us
Add vector variant for clause-v
a
lid me
t
hod
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-
U
w
e
Haus
R
e
duce consing and re
c
ursion
in split-delimite
d
-str
i
ng
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Ha
u
s
Allo
w
assumptions to be li
s
ts or
v
e
c
t
ors in bac
k
end
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe
Ha
u
s
A
v
oid double mapping from symbolic li
t
erals to variable
s
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-
U
we
Hau
s
Fi
x
NNF ge
n
erati
o
n if
e
xplicit :
A
TO
M
s are used
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
U
t
z-Uwe Haus
fi
x
ad
d
-for
m
ula to
d
rop :A
N
D and :OR-symbols be
f
ore
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-22
Utz-Uwe Ha
u
s
Fix macro
e
x
p
ansion
t
ime confusion in with-ind
e
x
-
hash
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-
U
w
e
H
aus
r
em
o
v
e debugging output an
d
ensure empt
y
clauses are
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe
H
a
u
s
Fix cal
l
to mi
n
isat s
o
lve()
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-17
Utz-Uwe Haus
Fix non-
c
nf formula
a
dd
i
t
ion interface
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-16
Utz-Uwe
Ha
u
s
Fix with
-
sat-solver macro
t
o correctly
r
efer
e
nce *default
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
U
tz-
U
we
H
a
us
(minisat ba
c
kend ) Return numbe
r
of queued
a
s
sumptions
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Utz-Uw
e
Haus
Also bui
l
d minisat backend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-15
Ut
z
-Uw
e
Hau
s
F
i
x assumption h
a
ndling in
precosat
b
ackend
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
Utz-U
w
e
H
aus
Add CNF
b
uilde
r
convenience functions
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-10
Utz-
U
we Haus
add-claus
e
s convenie
n
ce f
u
nction
commit
|
commitdiff
|
tree
2010-06-03
U
t
z-Uwe H
a
us
New me
t
hod syn
c
hronize
-
backend t
o
a
l
low incre
m
e
n
tal
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Haus
Add minisat
b
ackend t
o
lisp cod
e
, make it
t
h
e
d
efau
l
t
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
U
t
z-Uwe Haus
Minimalistic mi
n
isat header
a
nd
S
WIG in
t
egra
t
ion
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-
U
we Haus
Autot
o
ols setu
p
for
m
inisat
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe Ha
u
s
Fix f
i
rst lin
e
in dimacs forma
t
expor
t
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-02
Utz-Uwe
Haus
Import
m
ini
s
at2-070721
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-U
w
e Haus
Really fix memo
r
y issue: Precosat Solve
r
->reset()
w
as
.
.
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
F
i
x with-index-hash
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-Uwe Haus
Prope
r
ly
d
ispose of
p
recosat obj
e
cts
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
tz-Uwe Ha
u
s
Add ge
t
-
e
ssen
t
ial-var
i
ables i
m
p
l
e
mentat
i
o
n
.
Signed-off-by:
Utz-Uwe Haus
<lisp@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z-Uwe Haus
Add with-sat-s
o
lver and with-index-ha
s
h macros
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz
-
Uwe Haus
Add dimac
s
reade
r
/writer
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
U
t
z
-Uwe Haus
Proper garbage collection of foreign objects usi
n
g
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-06-01
Utz-U
w
e Haus
SWIG w
r
apper layer and
.
i
file fo
r
pr
e
cosat, mi
n
imali
s
tic
.
.
.
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz-Uwe
Haus
Import p
r
ecosa
t
-465r2-2ce82ba-1
0
0514
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree
2010-05-30
Utz-
U
we Haus
Initial layou
t
Signed-off-by:
Utz-Uwe Haus
<haus@uuhaus.de>
commit
|
commitdiff
|
tree