Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
SAT4J
sat4j
Commits
45b9a78b
Commit
45b9a78b
authored
Mar 06, 2022
by
Daniel Le Berre
Browse files
fixed more sonarqube violatons (minisat core package)
parent
e886eab3
Pipeline
#20096
passed with stages
in 48 minutes and 20 seconds
Changes
17
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
org.sat4j.core/src/main/java/org/sat4j/minisat/SolverFactory.java
View file @
45b9a78b
...
...
@@ -146,7 +146,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
public
static
Solver
<
DataStructureFactory
>
newGlucose21
()
{
Solver
<
DataStructureFactory
>
solver
=
newMiniLearningHeapRsatExpSimp
();
solver
.
setRestartStrategy
(
new
Glucose21Restarts
());
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
lbd
_b
ased
);
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
lbd
B
ased
);
return
solver
;
}
...
...
@@ -237,7 +237,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
new
MixedDataStructureSingleWL
());
solver
.
setSimplifier
(
solver
.
EXPENSIVE_SIMPLIFICATION_WLONLY
);
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
activity
_b
ased
_low_m
emory
);
solver
.
activity
B
ased
LowM
emory
);
LimitedLearning
<
DataStructureFactory
>
learning
=
new
PercentLengthLearning
<>(
10
);
solver
.
setLearningStrategy
(
learning
);
...
...
@@ -249,7 +249,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
*/
public
static
Solver
<
DataStructureFactory
>
newGlucose
()
{
Solver
<
DataStructureFactory
>
solver
=
newBestWL
();
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
lbd
_b
ased
);
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
lbd
B
ased
);
solver
.
setRestartStrategy
(
new
LubyRestarts
(
512
));
return
solver
;
}
...
...
@@ -372,7 +372,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
*/
public
static
ISolver
newAgeLCDS
()
{
Solver
<?>
solver
=
newGlucose21
();
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
age
_b
ased
);
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
age
B
ased
);
return
solver
;
}
...
...
@@ -382,7 +382,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
*/
public
static
ISolver
newActivityLCDS
()
{
Solver
<?>
solver
=
newGlucose21
();
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
activity
_b
ased
);
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
activity
B
ased
);
return
solver
;
}
...
...
@@ -392,7 +392,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
*/
public
static
ISolver
newSizeLCDS
()
{
Solver
<?>
solver
=
newGlucose21
();
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
size
_b
ased
);
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
size
B
ased
);
return
solver
;
}
...
...
@@ -464,7 +464,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
Solver
<
DataStructureFactory
>
solver
=
newGlucose21
();
solver
.
setRestartStrategy
(
new
LubyRestarts
(
100
));
solver
.
setLearnedConstraintsDeletionStrategy
(
solver
.
activity
_b
ased
_low_m
emory
);
solver
.
activity
B
ased
LowM
emory
);
return
solver
;
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/WLClause.java
View file @
45b9a78b
...
...
@@ -69,7 +69,7 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
* @param ps
* A VecInt that WILL BE EMPTY after calling that method.
*/
p
ublic
WLClause
(
IVecInt
ps
,
ILits
voc
)
{
p
rotected
WLClause
(
IVecInt
ps
,
ILits
voc
)
{
this
.
lits
=
new
int
[
ps
.
size
()];
ps
.
moveTo
(
this
.
lits
);
assert
ps
.
size
()
==
0
;
...
...
@@ -83,8 +83,6 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
* @see Constr#calcReason(Solver, Lit, Vec)
*/
public
void
calcReason
(
int
p
,
IVecInt
outReason
)
{
// assert outReason.size() == 0
// && ((p == ILits.UNDEFINED) || (p == lits[0]));
final
int
[]
mylits
=
this
.
lits
;
for
(
int
i
=
p
==
ILits
.
UNDEFINED
?
0
:
1
;
i
<
mylits
.
length
;
i
++)
{
assert
this
.
voc
.
isFalsified
(
mylits
[
i
]);
...
...
@@ -122,14 +120,13 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
mylits
[
0
]
=
mylits
[
1
];
mylits
[
1
]
=
p
^
1
;
}
// assert mylits[1] == (p ^ 1);
if
(
this
.
voc
.
isSatisfied
(
mylits
[
0
]))
{
this
.
voc
.
watch
(
p
,
this
);
return
true
;
}
int
previous
=
p
^
1
,
tmp
;
// look for new literal to watch: applying move to front strategy
for
(
int
i
=
2
;
i
<
mylits
.
length
;
i
++)
{
for
(
var
i
=
2
;
i
<
mylits
.
length
;
i
++)
{
if
(
this
.
voc
.
isFalsified
(
mylits
[
i
]))
{
tmp
=
previous
;
previous
=
mylits
[
i
];
...
...
@@ -141,7 +138,6 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
return
true
;
}
}
// assert voc.isFalsified(mylits[1]);
// the clause is now either unit or null
// move back the literals to their initial position
System
.
arraycopy
(
mylits
,
2
,
mylits
,
1
,
mylits
.
length
-
2
);
...
...
@@ -171,7 +167,7 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
@Override
public
String
toString
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
for
(
int
lit
:
this
.
lits
)
{
stb
.
append
(
Lits
.
toString
(
lit
));
stb
.
append
(
"["
);
//$NON-NLS-1$
...
...
@@ -188,7 +184,7 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
if
(
mapper
==
null
)
{
return
toString
();
}
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
for
(
int
lit
:
this
.
lits
)
{
stb
.
append
(
mapper
.
map
(
LiteralsUtils
.
toDimacs
(
lit
)));
stb
.
append
(
"["
);
//$NON-NLS-1$
...
...
@@ -241,7 +237,7 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
}
public
int
[]
getLits
()
{
int
[]
tmp
=
new
int
[
size
()];
var
tmp
=
new
int
[
size
()];
System
.
arraycopy
(
this
.
lits
,
0
,
tmp
,
0
,
size
());
return
tmp
;
}
...
...
@@ -326,7 +322,7 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
@Override
public
String
dump
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
for
(
int
p
:
lits
)
{
stb
.
append
(
LiteralsUtils
.
toDimacs
(
p
));
stb
.
append
(
' '
);
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/xor/Xor.java
View file @
45b9a78b
...
...
@@ -44,8 +44,7 @@ public class Xor implements Constr, Propagatable {
public
static
Xor
createParityConstraint
(
IVecInt
lits
,
boolean
parity
,
ILits
voc
)
{
// TODO ensure normal form
Xor
xor
=
new
Xor
(
lits
,
parity
,
voc
);
var
xor
=
new
Xor
(
lits
,
parity
,
voc
);
xor
.
register
();
return
xor
;
}
...
...
@@ -74,7 +73,6 @@ public class Xor implements Constr, Propagatable {
@Override
public
double
getActivity
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
...
...
@@ -103,7 +101,7 @@ public class Xor implements Constr, Propagatable {
nbSatisfied
=
1
;
}
// look for new literal to watch and counting satisfied literals
for
(
int
i
=
2
;
i
<
lits
.
length
;
i
++)
{
for
(
var
i
=
2
;
i
<
lits
.
length
;
i
++)
{
if
(
this
.
voc
.
isSatisfied
(
lits
[
i
]))
{
nbSatisfied
++;
}
else
if
(
this
.
voc
.
isUnassigned
(
lits
[
i
]))
{
...
...
@@ -149,8 +147,8 @@ public class Xor implements Constr, Propagatable {
@Override
public
void
calcReason
(
int
p
,
IVecInt
outReason
)
{
int
nbUnassigned
=
0
;
for
(
int
i
=
0
;
i
<
lits
.
length
;
i
++)
{
var
nbUnassigned
=
0
;
for
(
var
i
=
0
;
i
<
lits
.
length
;
i
++)
{
if
(
this
.
voc
.
isFalsified
(
lits
[
i
]))
{
outReason
.
push
(
lits
[
i
]
^
1
);
}
else
if
(
this
.
voc
.
isSatisfied
(
lits
[
i
]))
{
...
...
@@ -242,12 +240,15 @@ public class Xor implements Constr, Propagatable {
@Override
public
String
toString
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
for
(
int
l
:
lits
)
{
stb
.
append
(
LiteralsUtils
.
toDimacs
(
l
));
stb
.
append
(
" "
);
stb
.
append
(
voc
.
isUnassigned
(
l
)
?
"U"
:
(
voc
.
isFalsified
(
l
)
?
"F"
:
"T"
));
if
(
voc
.
isUnassigned
(
l
))
{
stb
.
append
(
"U"
);
}
else
{
stb
.
append
(
voc
.
isFalsified
(
l
)
?
"F"
:
"T"
);
}
stb
.
append
(
" x "
);
}
stb
.
append
(
parity
);
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/ActivityLCDS.java
View file @
45b9a78b
...
...
@@ -49,7 +49,7 @@ public class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
learnedConstrs
.
sort
(
solver
.
getActivityComparator
());
int
i
,
j
;
for
(
i
=
j
=
0
;
i
<
learnedConstrs
.
size
()
/
2
;
i
++)
{
Const
r
c
=
learnedConstrs
.
get
(
i
);
va
r
c
=
learnedConstrs
.
get
(
i
);
if
(
c
.
locked
()
||
c
.
size
()
==
2
)
{
learnedConstrs
.
set
(
j
++,
learnedConstrs
.
get
(
i
));
}
else
{
...
...
@@ -65,7 +65,6 @@ public class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
solver
.
out
.
log
(
solver
.
getLogPrefix
()
+
"cleaning "
//$NON-NLS-1$
+
(
learnedConstrs
.
size
()
-
j
)
+
" clauses out of "
//$NON-NLS-1$
+
learnedConstrs
.
size
());
// out.flush();
}
learnedConstrs
.
shrinkTo
(
j
);
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/CounterBasedPrimeImplicantStrategy.java
View file @
45b9a78b
...
...
@@ -55,14 +55,14 @@ public class CounterBasedPrimeImplicantStrategy
public
int
[]
compute
(
Solver
<?
extends
DataStructureFactory
>
solver
)
{
long
begin
=
System
.
currentTimeMillis
();
IVecInt
[]
watched
=
new
IVecInt
[
solver
.
voc
.
nVars
()
*
2
+
2
];
var
watched
=
new
IVecInt
[
solver
.
voc
.
nVars
()
*
2
+
2
];
for
(
int
d
:
solver
.
fullmodel
)
{
watched
[
toInternal
(
d
)]
=
new
VecInt
();
}
int
[]
count
=
new
int
[
solver
.
constrs
.
size
()];
var
count
=
new
int
[
solver
.
constrs
.
size
()];
Constr
constr
;
IVecInt
watch
;
for
(
int
i
=
0
;
i
<
solver
.
constrs
.
size
();
i
++)
{
for
(
var
i
=
0
;
i
<
solver
.
constrs
.
size
();
i
++)
{
constr
=
solver
.
constrs
.
get
(
i
);
if
(!
constr
.
canBeSatisfiedByCountingLiterals
())
{
throw
new
IllegalStateException
(
...
...
@@ -70,7 +70,7 @@ public class CounterBasedPrimeImplicantStrategy
+
constr
.
getClass
());
}
count
[
i
]
=
0
;
for
(
int
j
=
0
;
j
<
constr
.
size
();
j
++)
{
for
(
var
j
=
0
;
j
<
constr
.
size
();
j
++)
{
watch
=
watched
[
constr
.
get
(
j
)];
if
(
watch
!=
null
)
{
// satisfied literal
...
...
@@ -86,18 +86,18 @@ public class CounterBasedPrimeImplicantStrategy
}
this
.
prime
=
new
int
[
solver
.
voc
.
nVars
()
+
1
];
int
d
;
for
(
int
i
=
0
;
i
<
this
.
prime
.
length
;
i
++)
{
for
(
var
i
=
0
;
i
<
this
.
prime
.
length
;
i
++)
{
this
.
prime
[
i
]
=
0
;
}
for
(
IteratorInt
it
=
solver
.
implied
.
iterator
();
it
.
hasNext
();)
{
d
=
it
.
next
();
this
.
prime
[
Math
.
abs
(
d
)]
=
d
;
}
int
removed
=
0
;
int
posremoved
=
0
;
int
propagated
=
0
;
var
removed
=
0
;
var
posremoved
=
0
;
var
propagated
=
0
;
int
constrNumber
;
top:
for
(
int
i
=
0
;
i
<
solver
.
decisions
.
size
();
i
++)
{
top:
for
(
var
i
=
0
;
i
<
solver
.
decisions
.
size
();
i
++)
{
d
=
solver
.
decisions
.
get
(
i
);
for
(
IteratorInt
it
=
watched
[
toInternal
(
d
)].
iterator
();
it
.
hasNext
();)
{
...
...
@@ -118,8 +118,8 @@ public class CounterBasedPrimeImplicantStrategy
count
[
it
.
next
()]--;
}
}
int
[]
implicant
=
new
int
[
this
.
prime
.
length
-
removed
-
1
];
int
index
=
0
;
var
implicant
=
new
int
[
this
.
prime
.
length
-
removed
-
1
];
var
index
=
0
;
for
(
int
i
:
this
.
prime
)
{
if
(
i
!=
0
)
{
implicant
[
index
++]
=
i
;
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java
View file @
45b9a78b
...
...
@@ -55,7 +55,6 @@ class GlucoseLCDS<D extends DataStructureFactory>
private
static
final
long
serialVersionUID
=
1L
;
private
int
[]
flags
=
new
int
[
0
];
private
int
flag
=
0
;
// private int wall = 0;
private
final
ConflictTimer
timer
;
...
...
@@ -69,7 +68,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
int
i
,
j
;
for
(
i
=
j
=
learnedConstrs
.
size
()
/
2
;
i
<
learnedConstrs
.
size
();
i
++)
{
Const
r
c
=
learnedConstrs
.
get
(
i
);
va
r
c
=
learnedConstrs
.
get
(
i
);
if
(
c
.
locked
()
||
c
.
getActivity
()
<=
2.0
)
{
learnedConstrs
.
set
(
j
++,
learnedConstrs
.
get
(
i
));
}
else
{
...
...
@@ -83,7 +82,6 @@ class GlucoseLCDS<D extends DataStructureFactory>
+
(
learnedConstrs
.
size
()
-
j
)
+
" clauses out of "
//$NON-NLS-1$
+
learnedConstrs
.
size
()
+
" with flag "
//$NON-NLS-1$
+
this
.
flag
+
"/"
+
solver
.
stats
.
getConflicts
());
// out.flush();
}
learnedConstrs
.
shrinkTo
(
j
);
...
...
@@ -105,7 +103,6 @@ class GlucoseLCDS<D extends DataStructureFactory>
public
void
init
()
{
final
int
howmany
=
solver
.
voc
.
nVars
();
// wall = constrs.size() > 10000 ? constrs.size() : 10000;
if
(
this
.
flags
.
length
<=
howmany
)
{
this
.
flags
=
new
int
[
howmany
+
1
];
}
...
...
@@ -119,10 +116,10 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
protected
int
computeLBD
(
Constr
constr
,
int
propagated
)
{
int
nblevel
=
1
;
var
nblevel
=
1
;
this
.
flag
++;
int
currentLevel
;
for
(
int
i
=
1
;
i
<
constr
.
size
();
i
++)
{
for
(
var
i
=
1
;
i
<
constr
.
size
();
i
++)
{
currentLevel
=
solver
.
voc
.
getLevel
(
constr
.
get
(
i
));
if
(
currentLevel
>=
0
&&
this
.
flags
[
currentLevel
]
!=
this
.
flag
)
{
this
.
flags
[
currentLevel
]
=
this
.
flag
;
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/Heap.java
View file @
45b9a78b
...
...
@@ -60,39 +60,39 @@ public final class Heap implements Serializable {
return
i
>>
1
;
}
private
final
IVecInt
heap
=
new
VecInt
();
// heap of ints
private
final
IVecInt
variables
=
new
VecInt
();
// heap of ints
private
final
IVecInt
indices
=
new
VecInt
();
// int -> index in heap
private
final
VariableComparator
comparator
;
void
percolateUp
(
int
i
)
{
int
x
=
this
.
heap
.
get
(
i
);
int
x
=
this
.
variables
.
get
(
i
);
int
p
=
parent
(
i
);
while
(
i
!=
1
&&
comparator
.
preferredTo
(
x
,
this
.
heap
.
get
(
p
)))
{
this
.
heap
.
set
(
i
,
this
.
heap
.
get
(
p
));
this
.
indices
.
set
(
this
.
heap
.
get
(
p
),
i
);
while
(
i
!=
1
&&
comparator
.
preferredTo
(
x
,
this
.
variables
.
get
(
p
)))
{
this
.
variables
.
set
(
i
,
this
.
variables
.
get
(
p
));
this
.
indices
.
set
(
this
.
variables
.
get
(
p
),
i
);
i
=
p
;
p
=
parent
(
p
);
}
this
.
heap
.
set
(
i
,
x
);
this
.
variables
.
set
(
i
,
x
);
this
.
indices
.
set
(
x
,
i
);
}
void
percolateDown
(
int
i
)
{
int
x
=
this
.
heap
.
get
(
i
);
while
(
left
(
i
)
<
this
.
heap
.
size
())
{
int
child
=
right
(
i
)
<
this
.
heap
.
size
()
&&
comparator
.
preferredTo
(
this
.
heap
.
get
(
right
(
i
)),
this
.
heap
.
get
(
left
(
i
)))
?
right
(
i
)
:
left
(
i
);
if
(!
comparator
.
preferredTo
(
this
.
heap
.
get
(
child
),
x
))
{
int
x
=
this
.
variables
.
get
(
i
);
while
(
left
(
i
)
<
this
.
variables
.
size
())
{
int
child
=
right
(
i
)
<
this
.
variables
.
size
()
&&
comparator
.
preferredTo
(
this
.
variables
.
get
(
right
(
i
)),
this
.
variables
.
get
(
left
(
i
)))
?
right
(
i
)
:
left
(
i
);
if
(!
comparator
.
preferredTo
(
this
.
variables
.
get
(
child
),
x
))
{
break
;
}
this
.
heap
.
set
(
i
,
this
.
heap
.
get
(
child
));
this
.
indices
.
set
(
this
.
heap
.
get
(
i
),
i
);
this
.
variables
.
set
(
i
,
this
.
variables
.
get
(
child
));
this
.
indices
.
set
(
this
.
variables
.
get
(
i
),
i
);
i
=
child
;
}
this
.
heap
.
set
(
i
,
x
);
this
.
variables
.
set
(
i
,
x
);
this
.
indices
.
set
(
x
,
i
);
}
...
...
@@ -102,7 +102,7 @@ public final class Heap implements Serializable {
public
Heap
(
VariableComparator
comparator
)
{
// NOPMD
this
.
comparator
=
comparator
;
this
.
heap
.
push
(-
1
);
this
.
variables
.
push
(-
1
);
}
public
void
setBounds
(
int
size
)
{
...
...
@@ -122,20 +122,20 @@ public final class Heap implements Serializable {
}
public
boolean
empty
()
{
return
this
.
heap
.
size
()
==
1
;
return
this
.
variables
.
size
()
==
1
;
}
public
int
size
()
{
return
this
.
heap
.
size
()
-
1
;
return
this
.
variables
.
size
()
-
1
;
}
public
int
get
(
int
i
)
{
int
r
=
this
.
heap
.
get
(
i
);
this
.
heap
.
set
(
i
,
this
.
heap
.
last
());
this
.
indices
.
set
(
this
.
heap
.
get
(
i
),
i
);
int
r
=
this
.
variables
.
get
(
i
);
this
.
variables
.
set
(
i
,
this
.
variables
.
last
());
this
.
indices
.
set
(
this
.
variables
.
get
(
i
),
i
);
this
.
indices
.
set
(
r
,
0
);
this
.
heap
.
pop
();
if
(
this
.
heap
.
size
()
>
1
)
{
this
.
variables
.
pop
();
if
(
this
.
variables
.
size
()
>
1
)
{
percolateDown
(
1
);
}
return
r
;
...
...
@@ -143,8 +143,8 @@ public final class Heap implements Serializable {
public
void
insert
(
int
n
)
{
assert
ok
(
n
);
this
.
indices
.
set
(
n
,
this
.
heap
.
size
());
this
.
heap
.
push
(
n
);
this
.
indices
.
set
(
n
,
this
.
variables
.
size
());
this
.
variables
.
push
(
n
);
percolateUp
(
this
.
indices
.
get
(
n
));
}
...
...
@@ -157,9 +157,9 @@ public final class Heap implements Serializable {
}
public
boolean
heapProperty
(
int
i
)
{
return
i
>=
this
.
heap
.
size
()
||
(
parent
(
i
)
==
0
||
!
comparator
.
preferredTo
(
this
.
heap
.
get
(
i
),
this
.
heap
.
get
(
parent
(
i
))))
&&
heapProperty
(
left
(
i
))
return
i
>=
this
.
variables
.
size
()
||
(
parent
(
i
)
==
0
||
!
comparator
.
preferredTo
(
this
.
variables
.
get
(
i
),
this
.
variables
.
get
(
parent
(
i
))))
&&
heapProperty
(
left
(
i
))
&&
heapProperty
(
right
(
i
));
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/ILits.java
View file @
45b9a78b
...
...
@@ -109,11 +109,11 @@ public interface ILits {
* are removed. It is equivalent in our implementation to falsify the two
* phases of that variable.
*
* @param var
* @param var
iable
* a variable in Dimacs format.
* @since 2.3.2
*/
void
forgets
(
int
var
);
void
forgets
(
int
var
iable
);
/**
* Check if a literal is satisfied.
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/IPhaseSelectionStrategy.java
View file @
45b9a78b
...
...
@@ -64,12 +64,12 @@ public interface IPhaseSelectionStrategy extends Serializable {
* initialize the phase of a given variable to the given value. That method
* is suppose to be called AFTER init(int).
*
* @param var
* @param var
iable
* a variable
* @param p
* it's initial phase
*/
void
init
(
int
var
,
int
p
);
void
init
(
int
var
iable
,
int
p
);
/**
* indicate that a literal has been satisfied.
...
...
@@ -82,12 +82,13 @@ public interface IPhaseSelectionStrategy extends Serializable {
* selects the phase of the variable according to a phase selection
* strategy.
*
* @param var
* @param var
iable
* a variable chosen by the heuristics
* @return either var or not var, depending of the selection strategy.
* @return either variable or not variable, depending of the selection
* strategy.
*
*/
int
select
(
int
var
);
int
select
(
int
var
iable
);
/**
* Allow to perform a specific action when a literal of the current decision
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/IntQueue.java
View file @
45b9a78b
...
...
@@ -53,14 +53,13 @@ public final class IntQueue implements Serializable {
* the element to add
*/
public
void
insert
(
final
int
x
)
{
// ensure(size + 1);
assert
this
.
size
<
this
.
myarray
.
length
;
this
.
myarray
[
this
.
size
++]
=
x
;
}
/**
* returns the nex
d
t element in the queue. Unexpected results if the queue
*
is
empty!
* returns the next element in the queue. Unexpected results if the queue
is
* empty!
*
* @return the firsst element on the queue
*/
...
...
@@ -94,7 +93,7 @@ public final class IntQueue implements Serializable {
*/
public
void
ensure
(
final
int
nsize
)
{
if
(
nsize
>=
this
.
myarray
.
length
)
{
int
[]
narray
=
new
int
[
Math
.
max
(
nsize
,
this
.
size
*
2
)];
var
narray
=
new
int
[
Math
.
max
(
nsize
,
this
.
size
*
2
)];
System
.
arraycopy
(
this
.
myarray
,
0
,
narray
,
0
,
this
.
size
);
this
.
myarray
=
narray
;
}
...
...
@@ -102,7 +101,7 @@ public final class IntQueue implements Serializable {
@Override
public
String
toString
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
stb
.
append
(
">"
);
//$NON-NLS-1$
for
(
int
i
=
this
.
first
;
i
<
this
.
size
-
1
;
i
++)
{
stb
.
append
(
this
.
myarray
[
i
]);
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/QuadraticPrimeImplicantStrategy.java
View file @
45b9a78b
...
...
@@ -81,7 +81,7 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
}
prime
=
new
int
[
solver
.
realNumberOfVariables
()
+
1
];
int
p
,
d
;
for
(
int
i
=
0
;
i
<
prime
.
length
;
i
++)
{
for
(
var
i
=
0
;
i
<
prime
.
length
;
i
++)
{
prime
[
i
]
=
0
;
}
boolean
noproblem
;
...
...
@@ -94,13 +94,13 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
}
boolean
canBeRemoved
;
int
rightlevel
;
int
removed
=
0
;
int
posremoved
=
0
;
int
propagated
=
0
;
int
tested
=
0
;
int
l2propagation
=
0
;
var
removed
=
0
;
var
posremoved
=
0
;
var
propagated
=
0
;
var
tested
=
0
;
var
l2propagation
=
0
;
for
(
int
i
=
0
;
i
<
solver
.
decisions
.
size
();
i
++)
{
for
(
var
i
=
0
;
i
<
solver
.
decisions
.
size
();
i
++)
{
d
=
solver
.
decisions
.
get
(
i
);
assert
!
solver
.
voc
.
isFalsified
(
toInternal
(
d
));
if
(
solver
.
voc
.
isSatisfied
(
toInternal
(
d
)))
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/RestartStrategy.java
View file @
45b9a78b
...
...
@@ -56,11 +56,12 @@ public interface RestartStrategy extends Serializable, ConflictTimer {
void
init
(
SearchParams
params
,
SolverStats
stats
);
/**
* Ask for the next restart in number of conflicts.
Deprecated since 2.3.2
* Ask for the next restart in number of conflicts.
*
* @deprecated since 2.3.2
* @return the delay in conflicts before the next restart.
*/
@Deprecated
@Deprecated
(
since
=
"2.3.2"
)
long
nextRestartNumberOfConflict
();
/**
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/SearchParams.java
View file @
45b9a78b
...
...
@@ -113,7 +113,7 @@ public class SearchParams implements Serializable {
*/
@Override
public
String
toString
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
for
(
Field
field
:
SearchParams
.
class
.
getDeclaredFields
())
{