Commit 078f9d16 authored by Romain WALLON's avatar Romain WALLON
Browse files

Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j into assertion-level

parents bee57b12 ca754f5a
Pipeline #16857 failed with stages
in 25 minutes
......@@ -1074,7 +1074,8 @@ public class Solver<D extends DataStructureFactory>
this.order.updateVar(p);
}
public void varBumpActivity(Constr constr, int i, int p) {
public void varBumpActivity(Constr constr, int i, int p,
boolean conflicting) {
this.order.updateVar(constr.get(i));
}
......
......@@ -53,7 +53,7 @@ public interface VarActivityListener extends Serializable {
/**
* Update the activity of a variable v.
*/
void varBumpActivity(Constr constr, int i, int p);
void varBumpActivity(Constr constr, int i, int p, boolean conflicting);
void postBumpActivity(Constr constr);
......
......@@ -31,6 +31,7 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.specs.IVec;
......@@ -208,13 +209,15 @@ public class MapPb implements IDataStructurePB {
assert this.degree.signum() > 0;
if (reducedCoefs == null) {
for (int i = 0; i < cpb.size(); i++) {
val.varBumpActivity(cpb, i, p);
val.varBumpActivity(cpb, i, p, weightedLits
.containsKey(LiteralsUtils.neg(cpb.get(i))));
cuttingPlaneStep(cpb.get(i),
multiplyCoefficient(cpb.getCoef(i), coefMult));
}
} else {
for (int i = 0; i < cpb.size(); i++) {
val.varBumpActivity(cpb, i, p);
val.varBumpActivity(cpb, i, p, weightedLits
.containsKey(LiteralsUtils.neg(cpb.get(i))));
cuttingPlaneStep(cpb.get(i),
multiplyCoefficient(reducedCoefs[i], coefMult));
}
......
......@@ -340,9 +340,10 @@ public class PBSolverCP extends PBSolver {
}
@Override
public void varBumpActivity(Constr constr, int i, int p) {
public void varBumpActivity(Constr constr, int i, int p,
boolean conflicting) {
bumper.varBumpActivity(voc, bumpStrategy, getOrder(), (PBConstr) constr,
i, p);
i, p, conflicting);
}
@Override
......
......@@ -34,7 +34,7 @@ public abstract class AbstractLBDComputerStrategy
nblevel += assignedLiteral(voc, constr, i);
}
}
return nblevel;
return fixLbd(constr, nblevel);
}
protected void startComputeLBD(PBConstr constr, int propagated) {
......
......@@ -54,6 +54,11 @@ public class EffectiveLiteralsOnlyLBDComputerStrategy
@Override
protected int fixLbd(PBConstr constr, int lbd) {
// For each level, the candidate literal is the one with the highest
// coefficient.
// As such, if it is effective, the level indeed appears in the LBD.
// Otherwise, all other literals at this level will have a smaller
// coefficient, and will not be effective either.
int newLbd = 0;
for (IteratorInt it = lbdCandidates.iterator(); it.hasNext();) {
int v = it.next();
......
......@@ -35,7 +35,8 @@ public enum Bumper implements IBumper {
};
public void varBumpActivity(ILits voc, BumpStrategy bumpStrategy,
IOrder order, PBConstr constr, int i, int propagated) {
IOrder order, PBConstr constr, int i, int propagated,
boolean conflicting) {
if (isBumpable(voc, constr.get(i), constr.get(propagated))) {
bumpStrategy.varBumpActivity(order, constr, i);
}
......
......@@ -25,7 +25,7 @@ public class BumperEffective implements IBumper {
@Override
public void varBumpActivity(ILits voc, BumpStrategy bStrategy, IOrder order,
PBConstr constr, int lit, int propagated) {
PBConstr constr, int lit, int propagated, boolean conflicting) {
if (lit == 0) {
// A new constraint is being bumped.
constrDegree = constr.getDegree();
......
......@@ -27,7 +27,7 @@ public class BumperEffectiveAndPropagated implements IBumper {
@Override
public void varBumpActivity(ILits voc, BumpStrategy bStrategy, IOrder order,
PBConstr constr, int lit, int propagated) {
PBConstr constr, int lit, int propagated, boolean conflicting) {
if (lit == 0) {
// A new constraint is being bumped.
constrDegree = constr.getDegree();
......
......@@ -14,10 +14,13 @@ public class DoubleBumpClashingLiteralsDecorator implements IBumper {
@Override
public void varBumpActivity(ILits voc, BumpStrategy bumpStrategy,
IOrder order, PBConstr constr, int i, int propagated) {
IOrder order, PBConstr constr, int i, int propagated,
boolean conflicting) {
decorated.varBumpActivity(voc, bumpStrategy, order, constr, i,
propagated);
bumpStrategy.varBumpActivity(order, constr, i);
propagated, conflicting);
if (conflicting)
decorated.varBumpActivity(voc, bumpStrategy, order, constr, i,
propagated, conflicting);
}
@Override
......
......@@ -7,7 +7,7 @@ import org.sat4j.pb.constraints.pb.PBConstr;
public interface IBumper {
void varBumpActivity(ILits voc, BumpStrategy bumpStrategy, IOrder order,
PBConstr constr, int i, int propagated);
PBConstr constr, int i, int propagated, boolean conflicting);
void postBumpActivity(IOrder order, PBConstr constr);
......
......@@ -614,10 +614,10 @@ public class KTHLauncher {
} catch (ContradictionException e) {
log("UNSATISFIABLE", "s ");
} catch (Exception e) {
e.printStackTrace();
log("Unexpected Exception:" + e.getMessage());
}
} catch (ParseException exp) {
log("Unexpected exception:" + exp.getMessage());
log("Unexpected parsing exception:" + exp.getMessage());
}
}
}
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