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
e886eab3
Commit
e886eab3
authored
Mar 05, 2022
by
Daniel Le Berre
Browse files
fixed more sonarqube violatons (cnf constraints)
parent
c83a715f
Pipeline
#20071
passed with stages
in 44 minutes and 41 seconds
Changes
25
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/ClausalDataStructureWL.java
View file @
e886eab3
...
...
@@ -65,10 +65,10 @@ public class ClausalDataStructureWL extends AbstractDataStructureFactory {
return
new
UnitClause
(
v
.
last
());
}
if
(
v
.
size
()
==
2
)
{
return
OriginalBinaryClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalBinaryClause
.
brandNewClause
(
getVocabulary
()
,
v
);
}
return
OriginalWLClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalWLClause
.
brandNewClause
(
getVocabulary
(),
v
);
}
public
Constr
createUnregisteredClause
(
IVecInt
literals
)
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/MixedDataStructureDanielHT.java
View file @
e886eab3
...
...
@@ -89,10 +89,10 @@ public class MixedDataStructureDanielHT extends AbstractDataStructureFactory {
return
new
UnitClause
(
v
.
last
());
}
if
(
v
.
size
()
==
2
)
{
return
OriginalBinaryClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalBinaryClause
.
brandNewClause
(
getVocabulary
()
,
v
);
}
return
OriginalHTClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalHTClause
.
brandNewClause
(
getVocabulary
(),
v
);
}
public
Constr
createUnregisteredClause
(
IVecInt
literals
)
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/MixedDataStructureDanielWL.java
View file @
e886eab3
...
...
@@ -87,10 +87,10 @@ public class MixedDataStructureDanielWL extends AbstractDataStructureFactory {
return
new
UnitClause
(
v
.
last
());
}
if
(
v
.
size
()
==
2
)
{
return
OriginalBinaryClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalBinaryClause
.
brandNewClause
(
getVocabulary
()
,
v
);
}
return
OriginalWLClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalWLClause
.
brandNewClause
(
getVocabulary
(),
v
);
}
public
Constr
createUnregisteredClause
(
IVecInt
literals
)
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/MixedDataStructureDanielWLConciseBinary.java
View file @
e886eab3
...
...
@@ -92,7 +92,7 @@ public class MixedDataStructureDanielWLConciseBinary
if
(
v
.
size
()
==
2
)
{
return
createConciseBinaryClause
(
v
);
}
return
OriginalWLClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalWLClause
.
brandNewClause
(
getVocabulary
(),
v
);
}
private
Constr
createConciseBinaryClause
(
IVecInt
literals
)
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/MixedDataStructureSingleWL.java
View file @
e886eab3
...
...
@@ -86,10 +86,10 @@ public class MixedDataStructureSingleWL extends AbstractDataStructureFactory {
return
new
UnitClause
(
v
.
last
());
}
if
(
v
.
size
()
==
2
)
{
return
OriginalBinaryClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalBinaryClause
.
brandNewClause
(
getVocabulary
()
,
v
);
}
return
OriginalWLClause
.
brandNewClause
(
this
.
solver
,
getVocabulary
(),
v
);
return
OriginalWLClause
.
brandNewClause
(
getVocabulary
(),
v
);
}
public
Constr
createUnregisteredClause
(
IVecInt
literals
)
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/card/AtLeast.java
View file @
e886eab3
...
...
@@ -145,7 +145,7 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
return
new
UnitClauses
(
ps
);
}
if
(
degree
==
1
)
{
return
OriginalWLClause
.
brandNewClause
(
s
,
voc
,
ps
);
return
OriginalWLClause
.
brandNewClause
(
voc
,
ps
);
}
Constr
constr
=
new
AtLeast
(
voc
,
ps
,
degree
);
constr
.
register
();
...
...
@@ -258,8 +258,6 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
* For learnt clauses only @author leberre
*/
public
boolean
locked
()
{
// FIXME need to be adapted to AtLeast
// return lits[0].getReason() == this;
return
true
;
}
...
...
@@ -269,7 +267,7 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
public
void
register
()
{
this
.
counter
=
0
;
for
(
int
q
:
this
.
lits
)
{
for
(
var
q
:
this
.
lits
)
{
voc
.
watch
(
q
^
1
,
this
);
if
(
voc
.
isFalsified
(
q
))
{
this
.
counter
++;
...
...
@@ -382,8 +380,8 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
}
public
boolean
isSatisfied
()
{
int
nbSatisfied
=
0
;
int
degree
=
size
()
-
this
.
maxUnsatisfied
;
var
nbSatisfied
=
0
;
var
degree
=
size
()
-
this
.
maxUnsatisfied
;
for
(
int
p
:
this
.
lits
)
{
if
(
voc
.
isSatisfied
(
p
))
{
nbSatisfied
++;
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/card/MaxWatchCard.java
View file @
e886eab3
...
...
@@ -193,7 +193,6 @@ public final class MaxWatchCard
* @see Constr#learnt()
*/
public
boolean
learnt
()
{
// TODO learnt
return
false
;
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/card/MinWatchCard.java
View file @
e886eab3
...
...
@@ -446,7 +446,7 @@ public class MinWatchCard
stb
.
append
(
this
.
voc
.
valueToString
(
this
.
lits
[
0
]));
stb
.
append
(
"]"
);
stb
.
append
(
" "
);
//$NON-NLS-1$
for
(
int
i
=
1
;
i
<
this
.
lits
.
length
;
i
++)
{
for
(
var
i
=
1
;
i
<
this
.
lits
.
length
;
i
++)
{
stb
.
append
(
Lits
.
toStringX
(
this
.
lits
[
i
]));
stb
.
append
(
"["
);
stb
.
append
(
this
.
voc
.
valueToString
(
this
.
lits
[
i
]));
...
...
@@ -687,7 +687,7 @@ public class MinWatchCard
}
this
.
savedindex
=
indSwap
+
1
;
// Si un litt?ral a ?t? trouv? on les ?change
int
tmpInt
=
this
.
lits
[
indSwap
];
var
tmpInt
=
this
.
lits
[
indSwap
];
this
.
lits
[
indSwap
]
=
this
.
lits
[
indFalsified
];
this
.
lits
[
indFalsified
]
=
tmpInt
;
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/BinaryClause.java
View file @
e886eab3
...
...
@@ -72,7 +72,7 @@ public abstract class BinaryClause
* @param ps
* A VecInt that WILL BE EMPTY after calling that method.
*/
p
ublic
BinaryClause
(
IVecInt
ps
,
ILits
voc
)
{
p
rotected
BinaryClause
(
IVecInt
ps
,
ILits
voc
)
{
assert
ps
.
size
()
==
2
;
this
.
head
=
ps
.
get
(
0
);
this
.
tail
=
ps
.
get
(
1
);
...
...
@@ -110,11 +110,8 @@ public abstract class BinaryClause
* @see Constr#simplify(Solver)
*/
public
boolean
simplify
()
{
if
(
this
.
voc
.
isSatisfied
(
this
.
head
)
||
this
.
voc
.
isSatisfied
(
this
.
tail
))
{
return
true
;
}
return
false
;
return
this
.
voc
.
isSatisfied
(
this
.
head
)
||
this
.
voc
.
isSatisfied
(
this
.
tail
);
}
public
boolean
propagate
(
UnitPropagationListener
s
,
int
p
)
{
...
...
@@ -153,7 +150,7 @@ public abstract class BinaryClause
@Override
public
String
toString
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
stb
.
append
(
Lits
.
toString
(
this
.
head
));
stb
.
append
(
"["
);
//$NON-NLS-1$
stb
.
append
(
this
.
voc
.
valueToString
(
this
.
head
));
...
...
@@ -198,7 +195,6 @@ public abstract class BinaryClause
}
public
void
assertConstraint
(
UnitPropagationListener
s
)
{
// assert this.voc.isUnassigned(this.head);
boolean
ret
=
s
.
enqueue
(
this
.
head
,
this
);
assert
ret
;
}
...
...
@@ -215,7 +211,7 @@ public abstract class BinaryClause
}
public
int
[]
getLits
()
{
int
[]
tmp
=
new
int
[
2
];
var
tmp
=
new
int
[
2
];
tmp
[
0
]
=
this
.
head
;
tmp
[
1
]
=
this
.
tail
;
return
tmp
;
...
...
@@ -231,10 +227,7 @@ public abstract class BinaryClause
}
try
{
BinaryClause
wcl
=
(
BinaryClause
)
obj
;
if
(
wcl
.
head
!=
this
.
head
||
wcl
.
tail
!=
this
.
tail
)
{
return
false
;
}
return
true
;
return
wcl
.
head
==
this
.
head
&&
wcl
.
tail
==
this
.
tail
;
}
catch
(
ClassCastException
e
)
{
return
false
;
}
...
...
@@ -274,9 +267,7 @@ public abstract class BinaryClause
public
boolean
isSatisfied
()
{
if
(
voc
.
isSatisfied
(
this
.
head
))
return
true
;
if
(
voc
.
isSatisfied
(
this
.
tail
))
return
true
;
return
false
;
return
voc
.
isSatisfied
(
this
.
tail
);
}
public
int
getAssertionLevel
(
IVecInt
trail
,
int
decisionLevel
)
{
...
...
@@ -292,7 +283,7 @@ public abstract class BinaryClause
if
(
mapper
==
null
)
{
return
toString
();
}
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
stb
.
append
(
mapper
.
map
(
LiteralsUtils
.
toDimacs
(
this
.
head
)));
stb
.
append
(
"["
);
//$NON-NLS-1$
stb
.
append
(
this
.
voc
.
valueToString
(
this
.
head
));
...
...
@@ -307,7 +298,7 @@ public abstract class BinaryClause
@Override
public
String
dump
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
stb
.
append
(
LiteralsUtils
.
toDimacs
(
head
));
stb
.
append
(
' '
);
stb
.
append
(
LiteralsUtils
.
toDimacs
(
tail
));
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/BinaryClauses.java
View file @
e886eab3
...
...
@@ -89,9 +89,8 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
* UnitPropagationListener , int)
*/
public
boolean
propagate
(
UnitPropagationListener
s
,
int
p
)
{
// assert voc.isFalsified(this.reason);
voc
.
watch
(
p
,
this
);
for
(
int
i
=
0
;
i
<
clauses
.
size
();
i
++)
{
for
(
var
i
=
0
;
i
<
clauses
.
size
();
i
++)
{
int
q
=
clauses
.
get
(
i
);
if
(!
s
.
enqueue
(
q
,
this
))
{
conflictindex
=
i
;
...
...
@@ -147,7 +146,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
* @see org.sat4j.minisat.Constr#incActivity(double)
*/
public
void
incActivity
(
double
claInc
)
{
// TODO Auto-generated method stub
}
/*
...
...
@@ -156,7 +154,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
* @see org.sat4j.minisat.Constr#getActivity()
*/
public
double
getActivity
()
{
// TODO Auto-generated method stub
return
0
;
}
...
...
@@ -175,7 +172,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
* @see org.sat4j.minisat.Constr#setLearnt()
*/
public
void
setLearnt
()
{
// TODO Auto-generated method stub
}
/*
...
...
@@ -184,7 +180,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
* @see org.sat4j.minisat.Constr#register()
*/
public
void
register
()
{
// TODO Auto-generated method stub
}
/*
...
...
@@ -193,7 +188,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
* @see org.sat4j.minisat.Constr#rescaleBy(double)
*/
public
void
rescaleBy
(
double
d
)
{
// TODO Auto-generated method stub
}
/*
...
...
@@ -211,7 +205,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
* @see org.sat4j.minisat.Constr#get(int)
*/
public
int
get
(
int
i
)
{
// TODO Auto-generated method stub
throw
new
UnsupportedOperationException
();
}
...
...
@@ -224,12 +217,11 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
}
public
String
toString
(
VarMapper
mapper
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
propagatePI
(
MandatoryLiteralListener
l
,
int
p
)
{
for
(
int
i
=
0
;
i
<
clauses
.
size
();
i
++)
{
for
(
var
i
=
0
;
i
<
clauses
.
size
();
i
++)
{
l
.
isMandatory
(
clauses
.
get
(
i
));
}
}
...
...
@@ -241,48 +233,37 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
public
void
remove
(
UnitPropagationListener
upl
)
{
throw
new
UnsupportedOperationException
(
"Cannot remove all the binary clauses at once!"
);
// if (voc.watches(reason).contains(this)) {
// voc.watches(reason).remove(this);
// }
}
public
void
calcReasonOnTheFly
(
int
p
,
IVecInt
trail
,
IVecInt
outReason
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
forwardActivity
(
double
claInc
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
setActivity
(
double
d
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
assertConstraintIfNeeded
(
UnitPropagationListener
s
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
boolean
canBeSatisfiedByCountingLiterals
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
int
requiredNumberOfSatisfiedLiterals
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
boolean
isSatisfied
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
int
getAssertionLevel
(
IVecInt
trail
,
int
decisionLevel
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/CBClause.java
View file @
e886eab3
...
...
@@ -58,9 +58,8 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
private
double
activity
;
public
static
CBClause
brandNewClause
(
UnitPropagationListener
s
,
ILits
voc
,
IVecInt
literals
)
{
CBClause
c
=
new
CBClause
(
literals
,
voc
);
public
static
CBClause
brandNewClause
(
ILits
voc
,
IVecInt
literals
)
{
var
c
=
new
CBClause
(
literals
,
voc
);
c
.
register
();
return
c
;
}
...
...
@@ -85,7 +84,7 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
* @see org.sat4j.minisat.core.Constr#remove()
*/
public
void
remove
()
{
for
(
int
i
=
0
;
i
<
lits
.
length
;
i
++)
{
for
(
var
i
=
0
;
i
<
lits
.
length
;
i
++)
{
voc
.
watches
(
lits
[
i
]
^
1
).
remove
(
this
);
}
}
...
...
@@ -102,7 +101,7 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
assert
falsified
!=
lits
.
length
;
if
(
falsified
==
lits
.
length
-
1
)
{
// find unassigned literal
for
(
int
i
=
0
;
i
<
lits
.
length
;
i
++)
{
for
(
var
i
=
0
;
i
<
lits
.
length
;
i
++)
{
if
(!
voc
.
isFalsified
(
lits
[
i
]))
{
return
s
.
enqueue
(
lits
[
i
],
this
);
}
...
...
@@ -121,7 +120,7 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
* @see org.sat4j.minisat.core.Constr#simplify()
*/
public
boolean
simplify
()
{
for
(
int
p
:
lits
)
{
for
(
var
p
:
lits
)
{
if
(
voc
.
isSatisfied
(
p
))
{
return
true
;
}
...
...
@@ -146,7 +145,7 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
*/
public
void
calcReason
(
int
p
,
IVecInt
outReason
)
{
assert
outReason
.
size
()
==
0
;
for
(
int
q
:
lits
)
{
for
(
var
q
:
lits
)
{
assert
voc
.
isFalsified
(
q
)
||
q
==
p
;
if
(
voc
.
isFalsified
(
q
))
{
outReason
.
push
(
q
^
1
);
...
...
@@ -206,11 +205,11 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
* @see org.sat4j.minisat.core.Constr#register()
*/
public
void
register
()
{
for
(
int
p
:
lits
)
{
for
(
var
p
:
lits
)
{
voc
.
watch
(
p
^
1
,
this
);
}
if
(
learnt
)
{
for
(
int
p
:
lits
)
{
for
(
var
p
:
lits
)
{
if
(
voc
.
isFalsified
(
p
))
{
voc
.
undos
(
p
^
1
).
push
(
this
);
falsified
++;
...
...
@@ -262,7 +261,7 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
@Override
public
String
toString
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
for
(
int
i
=
0
;
i
<
lits
.
length
;
i
++)
{
stb
.
append
(
lits
[
i
]);
stb
.
append
(
"["
);
//$NON-NLS-1$
...
...
@@ -274,62 +273,50 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
}
public
boolean
canBePropagatedMultipleTimes
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
String
toString
(
VarMapper
mapper
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
remove
(
UnitPropagationListener
upl
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
calcReasonOnTheFly
(
int
p
,
IVecInt
trail
,
IVecInt
outReason
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
forwardActivity
(
double
claInc
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
setActivity
(
double
d
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
assertConstraintIfNeeded
(
UnitPropagationListener
s
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
boolean
canBeSatisfiedByCountingLiterals
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
int
requiredNumberOfSatisfiedLiterals
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
boolean
isSatisfied
()
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
int
getAssertionLevel
(
IVecInt
trail
,
int
decisionLevel
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
public
void
propagatePI
(
MandatoryLiteralListener
l
,
int
p
)
{
// TODO: implement this method !
throw
new
UnsupportedOperationException
(
"Not implemented yet!"
);
}
...
...
@@ -339,8 +326,8 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
@Override
public
String
dump
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
for
(
int
p
:
lits
)
{
va
r
stb
=
new
StringBuilder
();
for
(
var
p
:
lits
)
{
stb
.
append
(
LiteralsUtils
.
toDimacs
(
p
));
stb
.
append
(
' '
);
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/Clauses.java
View file @
e886eab3
...
...
@@ -39,7 +39,12 @@ import org.sat4j.specs.UnitPropagationListener;
* @author daniel
* @since 2.1
*/
public
abstract
class
Clauses
{
public
class
Clauses
{
private
Clauses
()
{
// prevents instantiation of the class.
}
/**
* Perform some sanity check before constructing a clause a) if a literal is
* assigned true, return null (the clause is satisfied) b) if a literal is
...
...
@@ -63,7 +68,7 @@ public abstract class Clauses {
UnitPropagationListener
s
)
throws
ContradictionException
{
// si un litt???ral de ps est vrai, retourner vrai
// enlever les litt???raux falsifi???s de ps
for
(
int
i
=
0
;
i
<
ps
.
size
();)
{
for
(
var
i
=
0
;
i
<
ps
.
size
();)
{
// on verifie si le litteral est affecte
if
(
voc
.
isUnassigned
(
ps
.
get
(
i
)))
{
// on passe au literal suivant
...
...
@@ -87,7 +92,7 @@ public abstract class Clauses {
// ???limine les clauses tautologiques
// deux litt???raux de signe oppos???s apparaissent dans la m???me
// clause
for
(
int
i
=
0
;
i
<
ps
.
size
()
-
1
;
i
++)
{
for
(
var
i
=
0
;
i
<
ps
.
size
()
-
1
;
i
++)
{
if
(
ps
.
get
(
i
)
==
(
ps
.
get
(
i
+
1
)
^
1
))
{
// la clause est tautologique
return
null
;
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/HTClause.java
View file @
e886eab3
...
...
@@ -80,7 +80,7 @@ public abstract class HTClause implements Propagatable, Constr, Serializable {
* @param ps
* A VecInt that WILL BE EMPTY after calling that method.
*/
p
ublic
HTClause
(
IVecInt
ps
,
ILits
voc
)
{
p
rotected
HTClause
(
IVecInt
ps
,
ILits
voc
)
{
assert
ps
.
size
()
>
1
;
this
.
head
=
ps
.
get
(
0
);
this
.
tail
=
ps
.
last
();
...
...
@@ -146,7 +146,7 @@ public abstract class HTClause implements Propagatable, Constr, Serializable {
if
(
this
.
head
==
neg
(
p
))
{
final
int
[]
mylits
=
this
.
middleLits
;
int
temphead
=
0
;
var
temphead
=
0
;
// moving head on the right
while
(
temphead
<
mylits
.
length
&&
this
.
voc
.
isFalsified
(
mylits
[
temphead
]))
{
...
...
@@ -197,7 +197,7 @@ public abstract class HTClause implements Propagatable, Constr, Serializable {
@Override
public
String
toString
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
stb
.
append
(
Lits
.
toString
(
this
.
head
));
stb
.
append
(
"["
);
//$NON-NLS-1$
stb
.
append
(
this
.
voc
.
valueToString
(
this
.
head
));
...
...
@@ -264,7 +264,7 @@ public abstract class HTClause implements Propagatable, Constr, Serializable {
}
public
int
[]
getLits
()
{
int
[]
tmp
=
new
int
[
size
()];
var
tmp
=
new
int
[
size
()];
System
.
arraycopy
(
this
.
middleLits
,
0
,
tmp
,
1
,
this
.
middleLits
.
length
);
tmp
[
0
]
=
this
.
head
;
tmp
[
tmp
.
length
-
1
]
=
this
.
tail
;
...
...
@@ -356,7 +356,7 @@ public abstract class HTClause implements Propagatable, Constr, Serializable {
}
public
String
toString
(
VarMapper
mapper
)
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
stb
.
append
(
mapper
.
map
(
LiteralsUtils
.
toDimacs
(
this
.
head
)));
stb
.
append
(
"["
);
//$NON-NLS-1$
stb
.
append
(
this
.
voc
.
valueToString
(
this
.
head
));
...
...
@@ -378,7 +378,7 @@ public abstract class HTClause implements Propagatable, Constr, Serializable {
@Override
public
String
dump
()
{
StringBuilde
r
stb
=
new
StringBuilder
();
va
r
stb
=
new
StringBuilder
();
stb
.
append
(
LiteralsUtils
.
toDimacs
(
this
.
head
));
stb
.
append
(
' '
);
for
(
int
p
:
middleLits
)
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/LearntHTClause.java
View file @
e886eab3
...
...
@@ -60,9 +60,9 @@ public class LearntHTClause extends HTClause {
public
void
register
()
{
// looking for the literal to put in tail
if
(
this
.
middleLits
.
length
>
0
)
{
int
maxi
=
0
;