Commit beedda29 authored by leberre's avatar leberre

Added back the DataStructureFactory class parameter (else the PB solvers cannot be built properly).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@312 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 007cb5e2
......@@ -35,7 +35,7 @@ import java.io.Serializable;
*
* @author leberre
*/
public interface LearningStrategy extends Serializable {
public interface LearningStrategy<D extends DataStructureFactory> extends Serializable {
/**
* hook method called just before the search begins. Useful to compute
......@@ -48,5 +48,5 @@ public interface LearningStrategy extends Serializable {
void setVarActivityListener(VarActivityListener s);
void setSolver(Solver s);
void setSolver(Solver<D> s);
}
......@@ -81,7 +81,7 @@ import org.sat4j.specs.TimeoutException;
*
* @author leberre
*/
public class Solver
public class Solver<D extends DataStructureFactory>
implements ISolver, UnitPropagationListener, ActivityListener, Learner {
private static final long serialVersionUID = 1L;
......@@ -148,7 +148,7 @@ public class Solver
private final SolverStats stats = new SolverStats();
private final LearningStrategy learner;
private final LearningStrategy<D> learner;
protected final AssertingClauseGenerator analyzer;
......@@ -158,7 +158,7 @@ public class Solver
private boolean timeBasedTimeout = true;
protected DataStructureFactory dsfactory;
protected D dsfactory;
private SearchParams params;
......@@ -198,13 +198,13 @@ public class Solver
* an asserting clause generator
*/
public Solver(AssertingClauseGenerator acg, LearningStrategy learner,
DataStructureFactory dsf, IOrder order, RestartStrategy restarter) {
public Solver(AssertingClauseGenerator acg, LearningStrategy<D> learner,
D dsf, IOrder order, RestartStrategy restarter) {
this(acg, learner, dsf, new SearchParams(), order, restarter);
}
public Solver(AssertingClauseGenerator acg, LearningStrategy learner,
DataStructureFactory dsf, SearchParams params, IOrder order,
public Solver(AssertingClauseGenerator acg, LearningStrategy<D> learner,
D dsf, SearchParams params, IOrder order,
RestartStrategy restarter) {
analyzer = acg;
this.learner = learner;
......@@ -221,7 +221,7 @@ public class Solver
* @param dsf
* the internal factory
*/
public final void setDataStructureFactory(DataStructureFactory dsf) {
public final void setDataStructureFactory(D dsf) {
dsfactory = dsf;
dsfactory.setUnitPropagationListener(this);
dsfactory.setLearner(this);
......
......@@ -28,6 +28,7 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.core.VarActivityListener;
......@@ -43,7 +44,7 @@ import org.sat4j.minisat.core.VarActivityListener;
* @author daniel
*
*/
abstract class AbstractLearning implements LearningStrategy {
abstract class AbstractLearning<D extends DataStructureFactory> implements LearningStrategy<D> {
/**
*
......@@ -56,7 +57,7 @@ abstract class AbstractLearning implements LearningStrategy {
this.val = s;
}
public void setSolver(Solver s) {
public void setSolver(Solver<D> s) {
this.val = s;
}
......
......@@ -28,6 +28,7 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.Solver;
......@@ -36,7 +37,7 @@ import org.sat4j.minisat.core.Solver;
*
* @author leberre
*/
public class ActiveLearning extends LimitedLearning {
public class ActiveLearning<D extends DataStructureFactory> extends LimitedLearning<D> {
private static final long serialVersionUID = 1L;
......@@ -59,7 +60,7 @@ public class ActiveLearning extends LimitedLearning {
}
@Override
public void setSolver(Solver s) {
public void setSolver(Solver<D> s) {
super.setSolver(s);
this.order = s.getOrder();
}
......
......@@ -29,6 +29,7 @@ package org.sat4j.minisat.learning;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
/**
* The solver only records among all the constraints only the clauses.
......@@ -38,7 +39,7 @@ import org.sat4j.minisat.core.Constr;
* @param <L> a data structure for the literals.
* @param <D> a data structure for the clauses.
*/
public class ClauseOnlyLearning extends LimitedLearning {
public class ClauseOnlyLearning<D extends DataStructureFactory> extends LimitedLearning<D> {
/**
*
......
......@@ -28,6 +28,7 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
/**
* A learning scheme for learning constraints of size smaller than a given
......@@ -35,7 +36,7 @@ import org.sat4j.minisat.core.Constr;
*
* @author leberre
*/
public class FixedLengthLearning extends LimitedLearning {
public class FixedLengthLearning<D extends DataStructureFactory> extends LimitedLearning<D> {
private static final long serialVersionUID = 1L;
......
......@@ -28,6 +28,7 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.Solver;
......@@ -40,24 +41,24 @@ import org.sat4j.minisat.core.VarActivityListener;
*
* @author leberre
*/
public abstract class LimitedLearning implements LearningStrategy {
public abstract class LimitedLearning<D extends DataStructureFactory> implements LearningStrategy<D> {
private static final long serialVersionUID = 1L;
private final NoLearningButHeuristics none;
private final NoLearningButHeuristics<D> none;
private final MiniSATLearning all;
private final MiniSATLearning<D> all;
protected ILits lits;
private SolverStats stats;
public LimitedLearning() {
none = new NoLearningButHeuristics();
all = new MiniSATLearning();
none = new NoLearningButHeuristics<D>();
all = new MiniSATLearning<D>();
}
public void setSolver(Solver s) {
public void setSolver(Solver<D> s) {
this.lits = s.getVocabulary();
setVarActivityListener(s);
all.setDataStructureFactory(s.getDSFactory());
......
......@@ -41,7 +41,7 @@ import org.sat4j.minisat.core.Solver;
*
* @author leberre
*/
public class MiniSATLearning extends AbstractLearning {
public class MiniSATLearning<D extends DataStructureFactory> extends AbstractLearning<D> {
private static final long serialVersionUID = 1L;
private DataStructureFactory dsf;
......@@ -51,7 +51,7 @@ public class MiniSATLearning extends AbstractLearning {
}
@Override
public void setSolver(Solver s) {
public void setSolver(Solver<D> s) {
super.setSolver(s);
this.dsf = s.getDSFactory();
}
......
......@@ -28,6 +28,7 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
/**
* Allows MiniSAT to do backjumping without learning. The literals appearing in
......@@ -36,7 +37,7 @@ import org.sat4j.minisat.core.Constr;
*
* @author leberre
*/
public class NoLearningButHeuristics extends AbstractLearning {
public class NoLearningButHeuristics<D extends DataStructureFactory> extends AbstractLearning<D> {
private static final long serialVersionUID = 1L;
......
......@@ -28,6 +28,7 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
/**
* Allows MiniSAT to do backjumping without learning. The literals appearing in
......@@ -36,7 +37,7 @@ import org.sat4j.minisat.core.Constr;
*
* @author leberre
*/
public class NoLearningNoHeuristics extends AbstractLearning {
public class NoLearningNoHeuristics<D extends DataStructureFactory> extends AbstractLearning<D> {
private static final long serialVersionUID = 1L;
......
......@@ -28,6 +28,7 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
/**
* Selects the constraints to learn according to its length as a percentage of
......@@ -36,7 +37,7 @@ import org.sat4j.minisat.core.Constr;
* @author daniel
*
*/
public class PercentLengthLearning extends LimitedLearning {
public class PercentLengthLearning<D extends DataStructureFactory> extends LimitedLearning<D> {
/**
*
......
......@@ -32,6 +32,7 @@ import java.io.IOException;
import junit.framework.TestCase;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.Solver;
import org.sat4j.reader.InstanceReader;
import org.sat4j.reader.ParseFormatException;
......@@ -286,7 +287,7 @@ public class TestsFonctionnels extends TestCase {
reader = new InstanceReader(solver);
}
private Solver solver;
private Solver<DataStructureFactory> solver;
private InstanceReader reader;
}
\ No newline at end of file
Markdown is supported
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