Commit 075d1403 authored by leberre's avatar leberre

Updated code to be in sync with core module.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@313 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent beedda29
......@@ -31,7 +31,7 @@ import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.pb.constraints.pb.IDataStructurePB;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.constraints.pb.WatchPb;
......@@ -95,7 +95,7 @@ public abstract class AbstractPBClauseCardConstrDataStructure extends
BigInteger[] normCoefs = new BigInteger[size];
mpb.buildConstraintFromMapPb(theLists, normCoefs);
if (mpb.getDegree().equals(BigInteger.ONE)) {
IVecInt v = WLClause.sanityCheck(new VecInt(theLists), getVocabulary(),
IVecInt v = Clauses.sanityCheck(new VecInt(theLists), getVocabulary(),
solver);
if (v == null)
return null;
......
......@@ -31,7 +31,7 @@ import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.pb.constraints.pb.IDataStructurePB;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.constraints.pb.WatchPb;
......@@ -97,7 +97,7 @@ public abstract class AbstractPBClauseCardConstrDataStructurePB extends
BigInteger[] normCoefs = new BigInteger[size];
mpb.buildConstraintFromMapPb(theLits, normCoefs);
if (mpb.getDegree().equals(BigInteger.ONE)) {
IVecInt v = WLClause.sanityCheck(new VecInt(theLits),
IVecInt v = Clauses.sanityCheck(new VecInt(theLits),
getVocabulary(), solver);
if (v == null)
return null;
......
......@@ -30,9 +30,9 @@ package org.sat4j.pb.constraints;
import java.math.BigInteger;
import org.sat4j.minisat.constraints.AbstractDataStructureFactory;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.pb.constraints.pb.AtLeastPB;
......@@ -51,7 +51,7 @@ import org.sat4j.specs.IVecInt;
* Window>Preferences>Java>Code Generation>Code and Comments
*/
public abstract class AbstractPBDataStructureFactory extends
AbstractDataStructureFactory<ILits> implements PBDataStructureFactory<ILits>, IInternalPBConstraintCreator {
AbstractDataStructureFactory implements PBDataStructureFactory, IInternalPBConstraintCreator {
/**
*
......@@ -59,7 +59,7 @@ public abstract class AbstractPBDataStructureFactory extends
private static final long serialVersionUID = 1L;
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, getVocabulary(), solver);
IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
if (v == null)
return null;
return WLClausePB.brandNewClause(solver, getVocabulary(), v);
......
......@@ -29,6 +29,7 @@ package org.sat4j.pb.constraints;
import java.math.BigInteger;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.constraints.pb.WLClausePB;
import org.sat4j.specs.ContradictionException;
......@@ -60,7 +61,7 @@ public abstract class AbstractPBDataStructureFactoryPB extends
@Override
public PBConstr createClause(IVecInt literals) throws ContradictionException {
IVecInt theLits = WLClausePB.sanityCheck(literals,getVocabulary(), solver);
IVecInt theLits = Clauses.sanityCheck(literals,getVocabulary(), solver);
if (theLits==null) {
return null;
}
......
......@@ -31,7 +31,7 @@ import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.constraints.pb.WatchPb;
import org.sat4j.specs.ContradictionException;
......@@ -70,7 +70,7 @@ public class CompetPBMaxClauseCardConstrDataStructure
if (bigDegree == null)
return null;
if (bigDegree.equals(BigInteger.ONE)) {
IVecInt v = WLClause.sanityCheck(new VecInt(theLits), getVocabulary(),
IVecInt v = Clauses.sanityCheck(new VecInt(theLits), getVocabulary(),
solver);
if (v == null)
return null;
......
......@@ -31,13 +31,12 @@ import java.math.BigInteger;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.ILits;
import org.sat4j.pb.constraints.pb.IDataStructurePB;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public interface PBDataStructureFactory<L extends ILits> extends DataStructureFactory<L> {
public interface PBDataStructureFactory extends DataStructureFactory {
Constr createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
......
......@@ -30,7 +30,6 @@ package org.sat4j.pb.core;
import java.math.BigInteger;
import org.sat4j.minisat.core.AssertingClauseGenerator;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
......@@ -44,8 +43,8 @@ import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public abstract class PBSolver<L extends ILits> extends
Solver<L, PBDataStructureFactory<L>> implements IPBSolver {
public abstract class PBSolver extends
Solver<PBDataStructureFactory> implements IPBSolver {
/**
*
......@@ -53,16 +52,16 @@ public abstract class PBSolver<L extends ILits> extends
private static final long serialVersionUID = 1L;
public PBSolver(AssertingClauseGenerator acg,
LearningStrategy<L, PBDataStructureFactory<L>> learner,
PBDataStructureFactory<L> dsf, IOrder<L> order,
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order,
RestartStrategy restarter) {
super(acg, learner, dsf, order, restarter);
}
public PBSolver(AssertingClauseGenerator acg,
LearningStrategy<L, PBDataStructureFactory<L>> learner,
PBDataStructureFactory<L> dsf, SearchParams params,
IOrder<L> order, RestartStrategy restarter) {
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params,
IOrder order, RestartStrategy restarter) {
super(acg, learner, dsf, params, order, restarter);
}
......@@ -90,7 +89,7 @@ public abstract class PBSolver<L extends ILits> extends
}
public void setObjectiveFunction(ObjectiveFunction obj) {
IOrder<L> order = getOrder();
IOrder order = getOrder();
if (order instanceof VarOrderHeapObjective) {
((VarOrderHeapObjective) order).setObjectiveFunction(obj);
}
......
......@@ -31,7 +31,6 @@ import org.sat4j.core.Vec;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.core.AssertingClauseGenerator;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.Pair;
......@@ -47,7 +46,7 @@ import org.sat4j.specs.IVec;
* @author parrain To change the template for this generated type comment go to
* Window - Preferences - Java - Code Generation - Code and Comments
*/
public class PBSolverCP<L extends ILits> extends PBSolver<L> {
public class PBSolverCP extends PBSolver {
private static final long serialVersionUID = 1L;
......@@ -56,16 +55,16 @@ public class PBSolverCP<L extends ILits> extends PBSolver<L> {
* @param learner
* @param dsf
*/
public PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<L,PBDataStructureFactory<L>> learner,
PBDataStructureFactory<L> dsf, IOrder<L> order) {
public PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order) {
super(acg, learner, dsf, new SearchParams(1.5, 100), order,new MiniSATRestarts());
}
public PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<L,PBDataStructureFactory<L>> learner, PBDataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter) {
public PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter) {
super(acg, learner, dsf, params, order, restarter);
}
public PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<L,PBDataStructureFactory<L>> learner, PBDataStructureFactory<L> dsf, SearchParams params, IOrder<L> order) {
public PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order) {
super(acg, learner, dsf, params, order,new MiniSATRestarts());
}
......
......@@ -28,14 +28,13 @@
package org.sat4j.pb.core;
import org.sat4j.minisat.core.AssertingClauseGenerator;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapClause;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverClause extends PBSolverCP<ILits> {
public class PBSolverClause extends PBSolverCP {
/**
*
......@@ -43,7 +42,7 @@ public class PBSolverClause extends PBSolverCP<ILits> {
private static final long serialVersionUID = 1L;
public PBSolverClause(AssertingClauseGenerator acg,
LearningStrategy<ILits,PBDataStructureFactory<ILits>> learner, PBDataStructureFactory<ILits> dsf, IOrder<ILits> order) {
LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order) {
super(acg, learner, dsf, order);
}
......
......@@ -28,14 +28,13 @@
package org.sat4j.pb.core;
import org.sat4j.minisat.core.AssertingClauseGenerator;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapMerging;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverMerging extends PBSolverCP<ILits> {
public class PBSolverMerging extends PBSolverCP {
/**
*
......@@ -43,8 +42,8 @@ public class PBSolverMerging extends PBSolverCP<ILits> {
private static final long serialVersionUID = 1L;
public PBSolverMerging(AssertingClauseGenerator acg,
LearningStrategy<ILits, PBDataStructureFactory<ILits>> learner,
PBDataStructureFactory<ILits> dsf, IOrder<ILits> order) {
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order) {
super(acg, learner, dsf, order);
}
......
......@@ -28,13 +28,12 @@
package org.sat4j.pb.core;
import org.sat4j.minisat.core.AssertingClauseGenerator;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
public class PBSolverResolution extends PBSolver<ILits> {
public class PBSolverResolution extends PBSolver {
/**
*
......@@ -43,18 +42,18 @@ public class PBSolverResolution extends PBSolver<ILits> {
public PBSolverResolution(
AssertingClauseGenerator acg,
LearningStrategy<ILits, PBDataStructureFactory<ILits>> learner,
PBDataStructureFactory<ILits> dsf,
SearchParams params, IOrder<ILits> order,
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
SearchParams params, IOrder order,
RestartStrategy restarter) {
super(acg, learner, dsf, params, order, restarter);
}
public PBSolverResolution(
AssertingClauseGenerator acg,
LearningStrategy<ILits, PBDataStructureFactory<ILits>> learner,
PBDataStructureFactory<ILits> dsf,
IOrder<ILits> order, RestartStrategy restarter) {
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
IOrder order, RestartStrategy restarter) {
super(acg, learner, dsf, order, restarter);
}
......
......@@ -30,7 +30,6 @@ package org.sat4j.pb.core;
import java.math.BigInteger;
import org.sat4j.minisat.core.AssertingClauseGenerator;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.pb.constraints.pb.PBConstr;
......@@ -39,10 +38,10 @@ import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public class PBSolverWithImpliedClause extends PBSolverCP<ILits> {
public class PBSolverWithImpliedClause extends PBSolverCP {
public PBSolverWithImpliedClause(AssertingClauseGenerator acg,
LearningStrategy<ILits,PBDataStructureFactory<ILits>> learner, PBDataStructureFactory<ILits> dsf, IOrder<ILits> order) {
LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order) {
super(acg, learner, dsf, order);
}
......
......@@ -32,7 +32,6 @@ import static org.sat4j.core.LiteralsUtils.var;
import java.math.BigInteger;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IPhaseSelectionStrategy;
import org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy;
import org.sat4j.minisat.orders.VarOrderHeap;
......@@ -40,7 +39,7 @@ import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public class VarOrderHeapObjective extends VarOrderHeap<ILits> {
public class VarOrderHeapObjective extends VarOrderHeap {
/**
*
......
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