Commit 4d8c5574 authored by Daniel Le Berre's avatar Daniel Le Berre

Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j

parents c2ab17e2 4e856a4d
/dist
/bin
/target
*.class
*.rupproof
*/.gitignore
......@@ -8,9 +8,9 @@
</classpathentry>
<classpathentry kind="src" output="target/test-classes" path="src/test/java">
<attributes>
<attribute name="test" value="true"/>
<attribute name="optional" value="true"/>
<attribute name="maven.pomderived" value="true"/>
<attribute name="test" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
......@@ -19,8 +19,9 @@
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.7">
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8">
<attributes>
<attribute name="module" value="true"/>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
......
......@@ -11,9 +11,9 @@ org.eclipse.jdt.core.codeComplete.staticFinalFieldPrefixes=
org.eclipse.jdt.core.codeComplete.staticFinalFieldSuffixes=
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.7
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=1.7
org.eclipse.jdt.core.compiler.compliance=1.8
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
......@@ -21,10 +21,9 @@ org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enablePreviewFeatures=disabled
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.problem.forbiddenReference=warning
org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning
org.eclipse.jdt.core.compiler.release=disabled
org.eclipse.jdt.core.compiler.source=1.7
org.eclipse.jdt.core.compiler.source=1.8
org.eclipse.jdt.core.formatter.align_type_members_on_columns=false
org.eclipse.jdt.core.formatter.alignment_for_additive_operator=16
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=16
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_annotation=0
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_enum_constant=16
......@@ -32,17 +31,20 @@ org.eclipse.jdt.core.formatter.alignment_for_arguments_in_explicit_constructor_c
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_method_invocation=16
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_qualified_allocation_expression=16
org.eclipse.jdt.core.formatter.alignment_for_assignment=0
org.eclipse.jdt.core.formatter.alignment_for_binary_expression=16
org.eclipse.jdt.core.formatter.alignment_for_bitwise_operator=16
org.eclipse.jdt.core.formatter.alignment_for_compact_if=16
org.eclipse.jdt.core.formatter.alignment_for_conditional_expression=80
org.eclipse.jdt.core.formatter.alignment_for_enum_constants=0
org.eclipse.jdt.core.formatter.alignment_for_expressions_in_array_initializer=16
org.eclipse.jdt.core.formatter.alignment_for_logical_operator=16
org.eclipse.jdt.core.formatter.alignment_for_method_declaration=0
org.eclipse.jdt.core.formatter.alignment_for_multiple_fields=16
org.eclipse.jdt.core.formatter.alignment_for_multiplicative_operator=16
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_constructor_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_method_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_resources_in_try=80
org.eclipse.jdt.core.formatter.alignment_for_selector_in_method_invocation=16
org.eclipse.jdt.core.formatter.alignment_for_string_concatenation=16
org.eclipse.jdt.core.formatter.alignment_for_superclass_in_type_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_enum_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_type_declaration=16
......@@ -126,11 +128,12 @@ org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=insert
org.eclipse.jdt.core.formatter.insert_space_after_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_after_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation_type_declaration=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_binary_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_brace_in_block=insert
......@@ -160,6 +163,8 @@ org.eclipse.jdt.core.formatter.insert_space_after_comma_in_superinterfaces=inser
org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_ellipsis=insert
org.eclipse.jdt.core.formatter.insert_space_after_logical_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_parameters=do not insert
......@@ -184,13 +189,17 @@ org.eclipse.jdt.core.formatter.insert_space_after_postfix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_wildcard=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_for=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_try_resources=insert
org.eclipse.jdt.core.formatter.insert_space_after_shift_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_after_unary_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_before_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_at_in_annotation_type_declaration=insert
org.eclipse.jdt.core.formatter.insert_space_before_binary_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_parameters=do not insert
......@@ -237,6 +246,8 @@ org.eclipse.jdt.core.formatter.insert_space_before_comma_in_superinterfaces=do n
org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_parameters=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_ellipsis=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_logical_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_parameters=do not insert
......@@ -273,9 +284,12 @@ org.eclipse.jdt.core.formatter.insert_space_before_postfix_operator=do not inser
org.eclipse.jdt.core.formatter.insert_space_before_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_wildcard=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_for=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_try_resources=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_shift_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_before_unary_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_brackets_in_array_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_empty_braces_in_array_initializer=do not insert
......@@ -301,6 +315,10 @@ org.eclipse.jdt.core.formatter.tabulation.char=space
org.eclipse.jdt.core.formatter.tabulation.size=4
org.eclipse.jdt.core.formatter.use_on_off_tags=false
org.eclipse.jdt.core.formatter.use_tabs_only_for_leading_indentations=true
org.eclipse.jdt.core.formatter.wrap_before_binary_operator=true
org.eclipse.jdt.core.formatter.wrap_before_additive_operator=true
org.eclipse.jdt.core.formatter.wrap_before_bitwise_operator=true
org.eclipse.jdt.core.formatter.wrap_before_logical_operator=true
org.eclipse.jdt.core.formatter.wrap_before_multiplicative_operator=true
org.eclipse.jdt.core.formatter.wrap_before_or_operator_multicatch=true
org.eclipse.jdt.core.formatter.wrap_before_string_concatenation=true
org.eclipse.jdt.core.formatter.wrap_outer_expressions_when_nested=true
......@@ -34,12 +34,12 @@ import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
@Feature(value = "deletion", parent = "expert")
final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
public class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
private static final long serialVersionUID = 1L;
private final ConflictTimer timer;
private final Solver<? extends DataStructureFactory> solver;
protected final Solver<? extends DataStructureFactory> solver;
ActivityLCDS(Solver<? extends DataStructureFactory> solver,
public ActivityLCDS(Solver<? extends DataStructureFactory> solver,
ConflictTimer timer) {
this.timer = timer;
this.solver = solver;
......@@ -53,6 +53,7 @@ final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
if (c.locked() || c.size() == 2) {
learnedConstrs.set(j++, learnedConstrs.get(i));
} else {
onRemove(c);
c.remove(solver);
solver.slistener.delete(c);
}
......@@ -94,7 +95,11 @@ final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
}
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
protected void onRemove(Constr c) {
// Nothing to do by default.
}
}
\ No newline at end of file
......@@ -68,7 +68,8 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
}
if (solver.isVerbose()) {
solver.out.log(solver.getLogPrefix() + "cleaning " //$NON-NLS-1$
+ (solver.learnts.size() - j) + " clauses out of " + solver.learnts.size()); //$NON-NLS-1$
+ (solver.learnts.size() - j) + " clauses out of " //$NON-NLS-1$
+ solver.learnts.size());
// out.flush();
}
solver.learnts.shrinkTo(j);
......@@ -97,7 +98,7 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
// do nothing
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
}
\ No newline at end of file
......@@ -33,11 +33,12 @@ import org.sat4j.annotations.Feature;
import org.sat4j.specs.Constr;
@Feature(value = "deletion", parent = "expert")
class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
public class Glucose2LCDS<D extends DataStructureFactory>
extends GlucoseLCDS<D> {
private static final long serialVersionUID = 1L;
Glucose2LCDS(Solver<D> solver, ConflictTimer timer) {
protected Glucose2LCDS(Solver<D> solver, ConflictTimer timer) {
super(solver, timer);
}
......@@ -48,9 +49,9 @@ class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
}
@Override
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
if (from.getActivity() > 2.0) {
int nblevel = computeLBD(from);
int nblevel = computeLBD(from, propagated);
if (nblevel < from.getActivity()) {
getSolver().stats.incUpdateLBD();
from.setActivity(nblevel);
......@@ -58,4 +59,4 @@ class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
}
}
}
\ No newline at end of file
}
......@@ -35,11 +35,11 @@ import org.sat4j.specs.IVec;
/**
* LBD based clauses cleaning strategy, as found in Glucose.
*
*
* This strategy expects the constraints to be clauses, i.e. the LBD computation
* may not be correct for other constraints (cardinality constraints, PB
* constraints).
*
*
* @author leberre
*
* @param <D>
......@@ -49,9 +49,9 @@ class GlucoseLCDS<D extends DataStructureFactory>
implements LearnedConstraintsDeletionStrategy {
/**
*
*
*/
private final Solver<D> solver;
protected final Solver<D> solver;
private static final long serialVersionUID = 1L;
private int[] flags = new int[0];
private int flag = 0;
......@@ -59,7 +59,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
private final ConflictTimer timer;
GlucoseLCDS(Solver<D> solver, ConflictTimer timer) {
protected GlucoseLCDS(Solver<D> solver, ConflictTimer timer) {
this.solver = solver;
this.timer = timer;
}
......@@ -75,6 +75,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
} else {
c.remove(solver);
solver.slistener.delete(c);
onRemove(c);
}
}
if (solver.isVerbose()) {
......@@ -88,6 +89,10 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
protected void onRemove(Constr c) {
// Nothing to do by default.
}
public ConflictTimer getTimer() {
return this.timer;
}
......@@ -109,11 +114,11 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
public void onClauseLearning(Constr constr) {
int nblevel = computeLBD(constr);
int nblevel = computeLBD(constr, -1);
constr.setActivity(nblevel);
}
protected int computeLBD(Constr constr) {
protected int computeLBD(Constr constr, int propagated) {
int nblevel = 1;
this.flag++;
int currentLevel;
......@@ -131,11 +136,11 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
}
protected Solver<D> getSolver() {
return solver;
}
}
\ No newline at end of file
}
......@@ -80,6 +80,16 @@ public interface IOrder {
*/
void updateVar(int p);
/**
* To be called when the activity of a literal changed.
*
* @param p
* a literal. The associated variable will be updated.
* @param value
* The value to update the literal with.
*/
void updateVar(int p, double value);
/**
* that method has the responsibility to initialize all arrays in the
* heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
......
......@@ -79,5 +79,5 @@ public interface LearnedConstraintsDeletionStrategy extends Serializable {
*
* @param from
*/
void onPropagation(Constr from);
void onPropagation(Constr from, int propagated);
}
\ No newline at end of file
......@@ -96,7 +96,7 @@ final class SizeLCDS implements LearnedConstraintsDeletionStrategy {
}
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
}
\ No newline at end of file
......@@ -575,7 +575,7 @@ public class Solver<D extends DataStructureFactory>
this.voc.setReason(p, from);
this.trail.push(p);
if (from != null && from.learnt()) {
this.learnedConstraintsDeletionStrategy.onPropagation(from);
this.learnedConstraintsDeletionStrategy.onPropagation(from, p);
}
return true;
}
......@@ -1074,6 +1074,10 @@ public class Solver<D extends DataStructureFactory>
this.order.updateVar(p);
}
public void varBumpActivity(Constr constr, int i, int p) {
this.order.updateVar(constr.get(i));
}
private void claRescalActivity() {
for (int i = 0; i < this.learnts.size(); i++) {
this.learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
......@@ -1694,7 +1698,7 @@ public class Solver<D extends DataStructureFactory>
return this.aTimer;
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// TODO Auto-generated method stub
}
......@@ -2595,4 +2599,9 @@ public class Solver<D extends DataStructureFactory>
public void setUnitClauseConsumer(UnitClauseConsumer ucc) {
this.unitClauseConsumer = ucc;
}
@Override
public void postBumpActivity(Constr constr) {
// Nothing to do by default.
}
}
......@@ -31,6 +31,8 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import org.sat4j.specs.Constr;
/**
* Interface providing the capability to increase the activity of a given
* variable.
......@@ -47,4 +49,12 @@ public interface VarActivityListener extends Serializable {
* <code>v&lt;&lt;1^1</code>)
*/
void varBumpActivity(int p);
/**
* Update the activity of a variable v.
*/
void varBumpActivity(Constr constr, int i, int p);
void postBumpActivity(Constr constr);
}
......@@ -81,6 +81,11 @@ public class NaturalStaticOrder implements IOrder {
public void updateVar(int p) {
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
@Override
public void init() {
index = 1;
......
......@@ -69,6 +69,11 @@ public class OrientedOrder implements IOrder {
}
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
@Override
public void init() {
order.init();
......
......@@ -132,6 +132,11 @@ public class RandomWalkDecorator implements IOrder, Serializable {
this.decorated.updateVar(q);
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
public double varActivity(int q) {
return this.decorated.varActivity(q);
}
......
......@@ -127,6 +127,11 @@ public class TabuListDecorator implements IOrder {
this.decorated.updateVar(q);
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
public double varActivity(int q) {
return this.decorated.varActivity(q);
}
......
......@@ -150,16 +150,21 @@ public class VarOrderHeap implements IOrder, Serializable {
* a literal
*/
public void updateVar(int p) {
updateVar(p, 1);
}
@Override
public void updateVar(int p, double value) {
int var = var(p);
updateActivity(var);
updateActivity(var, value);
this.phaseStrategy.updateVar(p);
if (this.heap.inHeap(var)) {
this.heap.increase(var);
}
}
protected void updateActivity(final int var) {
if ((this.activity[var] += this.varInc) > VAR_RESCALE_BOUND) {
protected void updateActivity(final int var, double inc) {
if ((this.activity[var] += (inc * varInc)) > VAR_RESCALE_BOUND) {
varRescaleActivity();
}
}
......
......@@ -149,4 +149,9 @@ public final class AtLeastPB extends AtLeast implements PBConstr {
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -51,7 +51,7 @@ public class ConflictMap extends MapPb implements IConflict {
protected boolean hasBeenReduced = false;
protected long numberOfReductions = 0;
private boolean allowSkipping = false;
private SkipStrategy skip = SkipStrategy.NO_SKIP;
private boolean endingSkipping = true;
/**
* to store the slack of the current resolvant
......@@ -64,6 +64,7 @@ public class ConflictMap extends MapPb implements IConflict {
final PBSolverStats stats;
protected IPreProcess preProcess = NoPreProcess.instance();
/**
* allows to access directly to all variables belonging to a particular
* level At index 0, unassigned literals are stored (usually level -1); so
......@@ -82,24 +83,25 @@ public class ConflictMap extends MapPb implements IConflict {
*/
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy,
boolean noRemove, SkipStrategy skip, IPreProcess preProcessing,
IPostProcess postProcessing, IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMap(cpb, level, noRemove, skip, postProcessing,
weakeningStrategy, autoDivisionStrategy, stats);
return new ConflictMap(cpb, level, noRemove, skip, preProcessing,
postProcessing, weakeningStrategy, autoDivisionStrategy, stats);
}
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
boolean noRemove, SkipStrategy skip, IPreProcess preprocess,
IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,
PBSolverStats stats) {
return ConflictMap.createConflict(cpb, level, noRemove, skip,
postprocess, weakeningStrategy, autoDivisionStrategy,
stats);
preprocess, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
}
@Override
......@@ -110,32 +112,35 @@ public class ConflictMap extends MapPb implements IConflict {
}
ConflictMap(PBConstr cpb, int level) {