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
b1ff349b
Commit
b1ff349b
authored
Mar 06, 2022
by
Daniel Le Berre
Browse files
LCDS now uses default methods.
parent
4379ff79
Pipeline
#20105
passed with stages
in 55 minutes and 41 seconds
Changes
8
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
org.sat4j.core/src/main/java/org/sat4j/minisat/core/ActivityLCDS.java
View file @
b1ff349b
...
...
@@ -79,25 +79,13 @@ public class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
+
timer
;
}
public
void
init
()
{
// do nothing
}
public
void
onClauseLearning
(
Constr
constr
)
{
// do nothing
}
@Override
public
void
onConflictAnalysis
(
Constr
reason
)
{
if
(
reason
.
learnt
())
{
solver
.
claBumpActivity
(
reason
);
}
}
public
void
onPropagation
(
Constr
from
,
int
propagated
)
{
// do nothing
}
protected
void
onRemove
(
Constr
c
)
{
// Nothing to do by default.
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/AgeLCDS.java
View file @
b1ff349b
...
...
@@ -83,21 +83,4 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
return
"Age based learned constraints deletion strategy with timer "
+
timer
;
}
public
void
init
()
{
// do nothing
}
public
void
onClauseLearning
(
Constr
constr
)
{
// do nothing
}
public
void
onConflictAnalysis
(
Constr
reason
)
{
// do nothing
}
public
void
onPropagation
(
Constr
from
,
int
propagated
)
{
// do nothing
}
}
\ No newline at end of file
org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java
View file @
b1ff349b
...
...
@@ -110,6 +110,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
this
.
timer
.
reset
();
}
@Override
public
void
onClauseLearning
(
Constr
constr
)
{
int
nblevel
=
computeLBD
(
constr
,
-
1
);
constr
.
setActivity
(
nblevel
);
...
...
@@ -129,14 +130,6 @@ class GlucoseLCDS<D extends DataStructureFactory>
return
nblevel
;
}
public
void
onConflictAnalysis
(
Constr
reason
)
{
}
public
void
onPropagation
(
Constr
from
,
int
propagated
)
{
}
protected
Solver
<
D
>
getSolver
()
{
return
solver
;
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/LearnedConstraintsDeletionStrategy.java
View file @
b1ff349b
...
...
@@ -47,7 +47,9 @@ public interface LearnedConstraintsDeletionStrategy extends Serializable {
/**
*
*/
void
init
();
default
void
init
()
{
}
ConflictTimer
getTimer
();
...
...
@@ -65,19 +67,25 @@ public interface LearnedConstraintsDeletionStrategy extends Serializable {
*
* @param outLearnt
*/
void
onClauseLearning
(
Constr
outLearnt
);
default
void
onClauseLearning
(
Constr
outLearnt
)
{
}
/**
* Hook method called on constraints participating to the conflict analysis.
*
* @param reason
*/
void
onConflictAnalysis
(
Constr
reason
);
default
void
onConflictAnalysis
(
Constr
reason
)
{
}
/**
* Hook method called when a unit clause is propagated thanks to from.
*
* @param from
*/
void
onPropagation
(
Constr
from
,
int
propagated
);
default
void
onPropagation
(
Constr
from
,
int
propagated
)
{
}
}
\ No newline at end of file
org.sat4j.core/src/main/java/org/sat4j/minisat/core/SizeLCDS.java
View file @
b1ff349b
...
...
@@ -80,22 +80,10 @@ final class SizeLCDS implements LearnedConstraintsDeletionStrategy {
+
timer
;
}
public
void
init
()
{
// do nothing
}
public
void
onClauseLearning
(
Constr
constr
)
{
// do nothing
}
@Override
public
void
onConflictAnalysis
(
Constr
reason
)
{
if
(
reason
.
learnt
())
{
solver
.
claBumpActivity
(
reason
);
}
}
public
void
onPropagation
(
Constr
from
,
int
propagated
)
{
// do nothing
}
}
\ No newline at end of file
org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java
View file @
b1ff349b
...
...
@@ -1666,27 +1666,15 @@ public class Solver<D extends DataStructureFactory>
Solver
.
this
.
learnts
.
shrinkTo
(
j
);
}
public
void
onConflictAnalysis
(
Constr
reason
)
{
}
public
void
onClauseLearning
(
Constr
outLearnt
)
{
}
@Override
public
String
toString
()
{
return
"Fixed size ("
+
maxsize
+
") learned constraints deletion strategy"
;
}
public
void
init
()
{
}
public
ConflictTimer
getTimer
()
{
return
this
.
aTimer
;
}
public
void
onPropagation
(
Constr
from
,
int
propagated
)
{
}
};
}
...
...
org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolver.java
View file @
b1ff349b
...
...
@@ -290,6 +290,7 @@ public abstract class PBSolver extends Solver<PBDataStructureFactory>
return
"Objective function driven learned constraints deletion strategy"
;
}
@Override
public
void
init
()
{
this
.
inObjectiveFunction
=
new
boolean
[
nVars
()
+
1
];
if
(
PBSolver
.
this
.
objf
==
null
)
{
...
...
@@ -303,6 +304,7 @@ public abstract class PBSolver extends Solver<PBDataStructureFactory>
this
.
clauseManagement
.
reset
();
}
@Override
public
void
onClauseLearning
(
Constr
constr
)
{
boolean
fullObj
=
true
;
...
...
@@ -317,12 +319,5 @@ public abstract class PBSolver extends Solver<PBDataStructureFactory>
}
}
public
void
onConflictAnalysis
(
Constr
reason
)
{
// do nothing
}
public
void
onPropagation
(
Constr
from
,
int
propagated
)
{
// do nothing
}
};
}
org.sat4j.pb/src/main/java/org/sat4j/pb/lcds/NullLCDS.java
View file @
b1ff349b
...
...
@@ -14,6 +14,10 @@ import org.sat4j.specs.IVec;
*/
public
class
NullLCDS
implements
LearnedConstraintsDeletionStrategy
{
/**
*
*/
private
static
final
long
serialVersionUID
=
1L
;
private
final
LearnedConstraintsDeletionStrategy
decorated
;
public
NullLCDS
(
LearnedConstraintsDeletionStrategy
decorated
)
{
...
...
@@ -33,7 +37,6 @@ public class NullLCDS implements LearnedConstraintsDeletionStrategy {
@Override
public
void
reduce
(
IVec
<
Constr
>
learnedConstrs
)
{
// TODO Auto-generated method stub
}
...
...
@@ -51,5 +54,4 @@ public class NullLCDS implements LearnedConstraintsDeletionStrategy {
public
void
onPropagation
(
Constr
from
,
int
propagated
)
{
decorated
.
onPropagation
(
from
,
propagated
);
}
}
Write
Preview
Supports
Markdown
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