Skip to content

GitLab

Commit 1357b084 authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

By default, no activity computed on constraints

parent 1271bdea
Pipeline #20136 passed with stages
in 45 minutes and 45 seconds
Hide whitespace changes
Inline Side-by-side
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/card/AtLeast.java
View file @ 1357b084
......@@ -234,26 +234,6 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
return false;
}
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.datatype.Constr#getActivity()
*/
public double getActivity() {
return 0;
}
public void setActivity(double d) {
}
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.datatype.Constr#incActivity(double)
*/
public void incActivity(double claInc) {
}
/*
* For learnt clauses only @author leberre
*/
......@@ -326,12 +306,6 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
return stb.toString();
}
/**
* @since 2.1
*/
public void forwardActivity(double claInc) {
}
public boolean canBePropagatedMultipleTimes() {
return false;
}
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/card/MaxWatchCard.java
View file @ 1357b084
......@@ -163,29 +163,6 @@ public final class MaxWatchCard
}
}
/**
* Obtenir la valeur de l'activit? de la contrainte
*
* @return la valeur de l'activit? de la contrainte
* @see Constr#getActivity()
*/
public double getActivity() {
return 0;
}
/**
* Incr?mente la valeur de l'activit? de la contrainte
*
* @param claInc
* incr?ment de l'activit? de la contrainte
* @see Constr#incActivity(double claInc)
*/
public void incActivity(double claInc) {
}
public void setActivity(double d) {
}
/**
* D?termine si la contrainte est apprise
*
......@@ -330,15 +307,6 @@ public final class MaxWatchCard
}
}
/**
* Permet le r??chantillonage de l'activit? de la contrainte
*
* @param d
* facteur d'ajustement
*/
public void rescaleBy(double d) {
}
/**
* Simplifie la contrainte(l'all?ge)
*
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/card/MinWatchCard.java
View file @ 1357b084
......@@ -191,29 +191,6 @@ public class MinWatchCard
}
}
/**
* Returns the activity of the constraint
*
* @return activity value of the constraint
* @see Constr#getActivity()
*/
public double getActivity() {
return 0;
}
/**
* Increments activity of the constraint
*
* @param claInc
* value to be added to the activity of the constraint
* @see Constr#incActivity(double claInc)
*/
public void incActivity(double claInc) {
}
public void setActivity(double d) {
}
/**
* Returns wether the constraint is learnt or not.
*
......@@ -407,15 +384,6 @@ public class MinWatchCard
}
}
/**
* Rescales the activity value of the constraint
*
* @param d
* rescale factor
*/
public void rescaleBy(double d) {
}
/**
* simplifies the constraint
*
......@@ -630,13 +598,6 @@ public class MinWatchCard
return (int) sum / (this.lits.length + 1);
}
/**
* @since 2.1
*/
public void forwardActivity(double claInc) {
// do nothing
}
public boolean canBePropagatedMultipleTimes() {
return false;
}
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/BinaryClauses.java
View file @ 1357b084
......@@ -140,23 +140,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
return false;
}
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.Constr#incActivity(double)
*/
public void incActivity(double claInc) {
}
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.Constr#getActivity()
*/
public double getActivity() {
return 0;
}
/*
* (non-Javadoc)
*
......@@ -182,14 +165,6 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
public void register() {
}
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.Constr#rescaleBy(double)
*/
public void rescaleBy(double d) {
}
/*
* (non-Javadoc)
*
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/LearntBinaryClause.java
View file @ 1357b084
......@@ -58,10 +58,6 @@ public class LearntBinaryClause extends BinaryClause {
return true;
}
public void forwardActivity(double claInc) {
}
/**
* @param claInc
*/
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/LearntHTClause.java
View file @ 1357b084
......@@ -89,10 +89,6 @@ public class LearntHTClause extends HTClause {
// do nothing
}
public void forwardActivity(double claInc) {
}
/**
* @param claInc
*/
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/LearntWLClause.java
View file @ 1357b084
......@@ -82,16 +82,10 @@ public final class LearntWLClause extends WLClause {
// do nothing
}
/**
* @since 2.1
*/
public void forwardActivity(double claInc) {
}
/**
* @param claInc
*/
@Override
public void incActivity(double claInc) {
this.activity += claInc;
}
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/OriginalBinaryClause.java
View file @ 1357b084
......@@ -73,19 +73,4 @@ public class OriginalBinaryClause extends BinaryClause {
c.register();
return c;
}
public void forwardActivity(double claInc) {
this.activity += claInc;
}
/**
* @param claInc
*/
public void incActivity(double claInc) {
}
public void setActivity(double claInc) {
// do nothing
}
}
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/OriginalHTClause.java
View file @ 1357b084
......@@ -87,21 +87,6 @@ public class OriginalHTClause extends HTClause {
return c;
}
public void forwardActivity(double claInc) {
this.activity += claInc;
}
/**
* @param claInc
*/
public void incActivity(double claInc) {
}
public void setActivity(double claInc) {
// do nothing
}
public void propagatePI(MandatoryLiteralListener l, int p) {
if (this.head == neg(p)) {
final int[] mylits = this.middleLits;
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/OriginalWLClause.java
View file @ 1357b084
......@@ -83,20 +83,6 @@ public final class OriginalWLClause extends WLClause {
return c;
}
/**
* @since 2.1
*/
public void forwardActivity(double claInc) {
this.activity += claInc;
}
/**
* @param claInc
*/
public void incActivity(double claInc) {
}
private int savedindex = 2;
public void propagatePI(MandatoryLiteralListener s, int p) {
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/UnitClause.java
View file @ 1357b084
......@@ -46,6 +46,10 @@ import org.sat4j.specs.VarMapper;
@Feature("constraint")
public class UnitClause implements Constr {
/**
*
*/
private static final long serialVersionUID = 1L;
protected final int literal;
protected double activity;
......@@ -133,10 +137,6 @@ public class UnitClause implements Constr {
return 1;
}
public void forwardActivity(double claInc) {
// silent to prevent problems with xplain trick.
}
@Override
public String toString() {
return Lits.toString(this.literal);
......
org.sat4j.core/src/main/java/org/sat4j/minisat/constraints/cnf/UnitClauses.java
View file @ 1357b084
......@@ -64,18 +64,11 @@ public class UnitClauses implements Constr {
}
@Override
public double getActivity() {
throw new UnsupportedOperationException();
}
public void incActivity(double claInc) {
// silent to prevent problems with xplain trick.
}
public void setActivity(double claInc) {
// do nothing
}
public boolean locked() {
throw new UnsupportedOperationException();
}
......@@ -95,6 +88,7 @@ public class UnitClauses implements Constr {
}
}
@Override
public void rescaleBy(double d) {
throw new UnsupportedOperationException();
}
......@@ -123,10 +117,6 @@ public class UnitClauses implements Constr {
throw new UnsupportedOperationException();
}
public void forwardActivity(double claInc) {
// silent to prevent problems with xplain trick.
}
public boolean canBePropagatedMultipleTimes() {
return false;
}
......
org.sat4j.core/src/main/java/org/sat4j/specs/Constr.java
View file @ 1357b084
......@@ -94,10 +94,6 @@ public interface Constr extends IConstr {
"A tautology cannot be a reason");
}
public void incActivity(double claInc) {
// do nothing
}
public void forwardActivity(double claInc) {
// do nothing
}
......@@ -114,14 +110,6 @@ public interface Constr extends IConstr {
// do nothing
}
public void rescaleBy(double d) {
// do nothing
}
public void setActivity(double d) {
// do nothing
}
public void assertConstraint(UnitPropagationListener s) {
// do nothing
}
......@@ -211,7 +199,9 @@ public interface Constr extends IConstr {
* @param claInc
* the value to increase the activity with
*/
void incActivity(double claInc);
default void incActivity(double claInc) {
}
/**
*
......@@ -220,10 +210,12 @@ public interface Constr extends IConstr {
*
*/
@Deprecated
void forwardActivity(double claInc);
default void forwardActivity(double claInc) {
}
/**
* Indicate wether a constraint is responsible from an assignment.
* Indicate weather a constraint is responsible from an assignment.
*
* @return true if a constraint is a "reason" for an assignment.
*/
......@@ -246,7 +238,9 @@ public interface Constr extends IConstr {
* @param d
* the value to rescale the clause activity with.
*/
void rescaleBy(double d);
default void rescaleBy(double d) {
}
/**
* Set the activity at a specific value
......@@ -255,7 +249,9 @@ public interface Constr extends IConstr {
* the new activity
* @since 2.3.1
*/
void setActivity(double d);
default void setActivity(double d) {
}
/**
* Method called when the constraint is to be asserted. It means that the
......
org.sat4j.core/src/main/java/org/sat4j/specs/IConstr.java
View file @ 1357b084
......@@ -67,7 +67,9 @@ public interface IConstr extends Serializable {
* @return the activity of the clause.
* @since 2.1
*/
double getActivity();
default double getActivity() {
return 0.0;
}
/**
* Partition constraints into the ones that only propagate once (e.g.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment