Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
SAT4J
sat4j
Commits
cc4e1322
Commit
cc4e1322
authored
Nov 10, 2018
by
Daniel Le Berre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fixes a few sonarqube violation.
parent
79ee6a46
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
45 additions
and
38 deletions
+45
-38
org.sat4j.pb/src/main/java/org/sat4j/pb/ObjectiveFunction.java
...at4j.pb/src/main/java/org/sat4j/pb/ObjectiveFunction.java
+6
-9
org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/WatchPb.java
...pb/src/main/java/org/sat4j/pb/constraints/pb/WatchPb.java
+19
-13
org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/WatchPbLong.java
...rc/main/java/org/sat4j/pb/constraints/pb/WatchPbLong.java
+3
-0
org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/WatchPbLongCP.java
.../main/java/org/sat4j/pb/constraints/pb/WatchPbLongCP.java
+16
-14
org.sat4j.pb/src/main/java/org/sat4j/pb/tools/AtLeastCard.java
...at4j.pb/src/main/java/org/sat4j/pb/tools/AtLeastCard.java
+1
-2
No files found.
org.sat4j.pb/src/main/java/org/sat4j/pb/ObjectiveFunction.java
View file @
cc4e1322
...
...
@@ -90,11 +90,10 @@ public class ObjectiveFunction implements Serializable {
BigInteger
tempDegree
=
BigInteger
.
ZERO
;
for
(
int
i
=
0
;
i
<
this
.
vars
.
size
();
i
++)
{
BigInteger
coeff
=
this
.
coeffs
.
get
(
i
);
if
(
varInModel
(
this
.
vars
.
get
(
i
),
lazyModel
))
{
tempDegree
=
tempDegree
.
add
(
coeff
);
}
else
if
(
coeff
.
signum
()
<
0
if
(
varInModel
(
this
.
vars
.
get
(
i
),
lazyModel
)
||
coeff
.
signum
()
<
0
&&
!
varInModel
(-
this
.
vars
.
get
(
i
),
lazyModel
))
{
// the variable does not appear in the model: it can be assigned
// if the variable does not appear in the model, it can be
// assigned
// either way
tempDegree
=
tempDegree
.
add
(
coeff
);
}
...
...
@@ -117,12 +116,10 @@ public class ObjectiveFunction implements Serializable {
BigInteger
tempDegree
=
BigInteger
.
ZERO
;
for
(
int
i
=
0
;
i
<
this
.
vars
.
size
();
i
++)
{
BigInteger
coeff
=
this
.
coeffs
.
get
(
i
);
if
(
solver
.
primeImplicant
(
this
.
vars
.
get
(
i
)))
{
tempDegree
=
tempDegree
.
add
(
coeff
);
}
else
if
(
coeff
.
signum
()
<
0
if
(
solver
.
primeImplicant
(
this
.
vars
.
get
(
i
))
||
coeff
.
signum
()
<
0
&&
!
solver
.
primeImplicant
(-
this
.
vars
.
get
(
i
)))
{
// the variable does not appear in the model
:
it can be
assigned
// either way
//
if
the variable does not appear in the model
,
it can be
//
assigned
either way
tempDegree
=
tempDegree
.
add
(
coeff
);
}
}
...
...
org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/WatchPb.java
View file @
cc4e1322
...
...
@@ -51,12 +51,12 @@ import org.sat4j.specs.VarMapper;
* @author anne
*
*/
public
abstract
class
WatchPb
implements
IWatchPb
,
Propagatable
,
Undoable
,
Serializable
{
public
abstract
class
WatchPb
implements
IWatchPb
,
Propagatable
,
Undoable
,
Serializable
{
/**
*
*/
*
*/
private
static
final
long
serialVersionUID
=
1L
;
private
static
final
int
LIMIT_SELECTION_SORT
=
15
;
...
...
@@ -137,8 +137,8 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
BigInteger
slack
=
BigInteger
.
ZERO
;
for
(
int
i
=
0
;
i
<
this
.
lits
.
length
;
i
++)
{
if
(
this
.
coefs
[
i
].
signum
()
>
0
&&
(!
this
.
voc
.
isFalsified
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
))
{
&&
(!
this
.
voc
.
isFalsified
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
))
{
slack
=
slack
.
add
(
this
.
coefs
[
i
]);
}
}
...
...
@@ -148,8 +148,8 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
}
for
(
int
i
=
0
;
i
<
this
.
lits
.
length
;
i
++)
{
if
(
this
.
coefs
[
i
].
signum
()
>
0
&&
(
this
.
voc
.
isUnassigned
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
)
&&
(
this
.
voc
.
isUnassigned
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
)
&&
slack
.
compareTo
(
this
.
coefs
[
i
])
<
0
)
{
return
true
;
}
...
...
@@ -175,7 +175,8 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
if
(
this
.
voc
.
isFalsified
(
q
))
{
outReason
.
push
(
q
^
1
);
sumfalsified
=
sumfalsified
.
add
(
this
.
coefs
[
i
]);
if
(
this
.
sumcoefs
.
subtract
(
sumfalsified
).
compareTo
(
this
.
degree
)
<
0
)
{
if
(
this
.
sumcoefs
.
subtract
(
sumfalsified
)
.
compareTo
(
this
.
degree
)
<
0
)
{
return
;
}
}
...
...
@@ -360,7 +361,7 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
for
(
j
=
i
+
1
;
j
<
to
;
j
++)
{
if
(
this
.
coefs
[
j
].
compareTo
(
this
.
coefs
[
bestIndex
])
>
0
||
this
.
coefs
[
j
].
equals
(
this
.
coefs
[
bestIndex
])
&&
this
.
lits
[
j
]
>
this
.
lits
[
bestIndex
])
{
&&
this
.
lits
[
j
]
>
this
.
lits
[
bestIndex
])
{
bestIndex
=
j
;
}
}
...
...
@@ -446,12 +447,12 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
i
++;
}
while
(
this
.
coefs
[
i
].
compareTo
(
pivot
)
>
0
||
this
.
coefs
[
i
].
equals
(
pivot
)
&&
this
.
lits
[
i
]
>
litPivot
);
&&
this
.
lits
[
i
]
>
litPivot
);
do
{
j
--;
}
while
(
pivot
.
compareTo
(
this
.
coefs
[
j
])
>
0
||
this
.
coefs
[
j
].
equals
(
pivot
)
&&
this
.
lits
[
j
]
<
litPivot
);
&&
this
.
lits
[
j
]
<
litPivot
);
if
(
i
>=
j
)
{
break
;
...
...
@@ -582,6 +583,9 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
if
(
pb
==
null
)
{
return
false
;
}
if
(
this
.
getClass
()
!=
pb
.
getClass
())
{
return
false
;
}
// this method should be simplified since now two constraints should
// have
// always
...
...
@@ -654,7 +658,8 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
outReason
.
push
(
q
);
index
=
vlits
.
indexOf
(
q
^
1
);
sumfalsified
=
sumfalsified
.
add
(
this
.
coefs
[
index
]);
if
(
this
.
sumcoefs
.
subtract
(
sumfalsified
).
compareTo
(
this
.
degree
)
<
0
)
{
if
(
this
.
sumcoefs
.
subtract
(
sumfalsified
)
.
compareTo
(
this
.
degree
)
<
0
)
{
return
;
}
}
...
...
@@ -673,6 +678,7 @@ public abstract class WatchPb implements IWatchPb, Propagatable, Undoable,
public
boolean
isSatisfied
()
{
throw
new
UnsupportedOperationException
(
"Not implemented yet"
);
}
public
String
toString
(
VarMapper
mapper
)
{
StringBuilder
stb
=
new
StringBuilder
();
...
...
org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/WatchPbLong.java
View file @
cc4e1322
...
...
@@ -561,6 +561,9 @@ public abstract class WatchPbLong
if
(
pb
==
null
)
{
return
false
;
}
if
(
this
.
getClass
()
!=
pb
.
getClass
())
{
return
false
;
}
// this method should be simplified since now two constraints should
// have
// always
...
...
org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/WatchPbLongCP.java
View file @
cc4e1322
...
...
@@ -45,12 +45,12 @@ import org.sat4j.specs.Propagatable;
import
org.sat4j.specs.UnitPropagationListener
;
import
org.sat4j.specs.VarMapper
;
public
abstract
class
WatchPbLongCP
implements
IWatchPb
,
Propagatable
,
Undoable
,
Serializable
{
public
abstract
class
WatchPbLongCP
implements
IWatchPb
,
Propagatable
,
Undoable
,
Serializable
{
/**
*
*/
*
*/
private
static
final
long
serialVersionUID
=
1L
;
private
static
final
int
LIMIT_SELECTION_SORT
=
15
;
...
...
@@ -156,9 +156,8 @@ public abstract class WatchPbLongCP implements IWatchPb, Propagatable,
public
boolean
isAssertive
(
int
dl
)
{
long
slack
=
0
;
for
(
int
i
=
0
;
i
<
this
.
lits
.
length
;
i
++)
{
if
(
this
.
coefs
[
i
]
>
0
&&
(!
this
.
voc
.
isFalsified
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
))
{
if
(
this
.
coefs
[
i
]
>
0
&&
(!
this
.
voc
.
isFalsified
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
))
{
slack
=
slack
+
this
.
coefs
[
i
];
}
}
...
...
@@ -168,8 +167,8 @@ public abstract class WatchPbLongCP implements IWatchPb, Propagatable,
}
for
(
int
i
=
0
;
i
<
this
.
lits
.
length
;
i
++)
{
if
(
this
.
coefs
[
i
]
>
0
&&
(
this
.
voc
.
isUnassigned
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
)
&&
(
this
.
voc
.
isUnassigned
(
this
.
lits
[
i
])
||
this
.
voc
.
getLevel
(
this
.
lits
[
i
])
>=
dl
)
&&
slack
<
this
.
coefs
[
i
])
{
return
true
;
}
...
...
@@ -389,7 +388,7 @@ public abstract class WatchPbLongCP implements IWatchPb, Propagatable,
for
(
j
=
i
+
1
;
j
<
to
;
j
++)
{
if
(
this
.
coefs
[
j
]
>
this
.
coefs
[
bestIndex
]
||
this
.
coefs
[
j
]
==
this
.
coefs
[
bestIndex
]
&&
this
.
lits
[
j
]
>
this
.
lits
[
bestIndex
])
{
&&
this
.
lits
[
j
]
>
this
.
lits
[
bestIndex
])
{
bestIndex
=
j
;
}
}
...
...
@@ -474,12 +473,12 @@ public abstract class WatchPbLongCP implements IWatchPb, Propagatable,
for
(;;)
{
do
{
i
++;
}
while
(
this
.
coefs
[
i
]
>
pivot
||
this
.
coefs
[
i
]
==
pivot
&&
this
.
lits
[
i
]
>
litPivot
);
}
while
(
this
.
coefs
[
i
]
>
pivot
||
this
.
coefs
[
i
]
==
pivot
&&
this
.
lits
[
i
]
>
litPivot
);
do
{
j
--;
}
while
(
pivot
>
this
.
coefs
[
j
]
||
this
.
coefs
[
j
]
==
pivot
&&
this
.
lits
[
j
]
<
litPivot
);
}
while
(
pivot
>
this
.
coefs
[
j
]
||
this
.
coefs
[
j
]
==
pivot
&&
this
.
lits
[
j
]
<
litPivot
);
if
(
i
>=
j
)
{
break
;
...
...
@@ -596,6 +595,9 @@ public abstract class WatchPbLongCP implements IWatchPb, Propagatable,
if
(
pb
==
null
)
{
return
false
;
}
if
(
this
.
getClass
()
!=
pb
.
getClass
())
{
return
false
;
}
// this method should be simplified since now two constraints should
// have
// always
...
...
org.sat4j.pb/src/main/java/org/sat4j/pb/tools/AtLeastCard.java
View file @
cc4e1322
...
...
@@ -83,8 +83,7 @@ public class AtLeastCard {
if
(
degree
!=
other
.
degree
)
return
false
;
if
(
lits
==
null
)
{
if
(
other
.
lits
!=
null
)
return
false
;
return
other
.
lits
==
null
;
}
Set
<
Integer
>
litsSet1
=
new
HashSet
<
Integer
>();
for
(
IteratorInt
it
=
lits
.
iterator
();
it
.
hasNext
();)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment