Commit a824372f authored by Daniel Le Berre's avatar Daniel Le Berre

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

parents 7159972b 309f26f0
Pipeline #373 passed with stages
in 26 minutes and 16 seconds
......@@ -13,7 +13,7 @@ java8:
image: maven:3.5.0-jdk-8
stage: build
script:
- mvn $MAVEN_CLI_OPTS clean org.jacoco:jacoco-maven-plugin:prepare-agent --settings settings.xml deploy -Dmaven.test.failure.ignore=true
- mvn $MAVEN_CLI_OPTS clean org.jacoco:jacoco-maven-plugin:prepare-agent --settings settings.xml deploy
- mvn $MAVEN_CLI_OPTS sonar:sonar
cache:
paths:
......@@ -33,11 +33,11 @@ java7:
image: maven:3.5.0-jdk-7
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.test.failure.ignore=true -Dmaven.javadoc.skip=true
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true
java9:
image: maven:3.5.0-jdk-9
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.test.failure.ignore=true -Dmaven.javadoc.skip=true
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true
allow_failure: true
......@@ -395,6 +395,17 @@ public class ConflictMap extends MapPb implements IConflict {
// updating of the degree of the conflict
degreeCons = degreeCons.multiply(this.coefMultCons);
this.degree = this.degree.multiply(this.coefMult);
// Updating the stats about the reduction.
for (int i = 0; i < cpb.size(); i++) {
if (coefsCons[i].signum() != 0) {
if (this.voc.isUnassigned(cpb.get(i))) {
this.stats.numberOfRemainingUnassigned++;
} else {
this.stats.numberOfRemainingAssigned++;
}
}
}
}
// coefficients of the conflict must be multiplied by coefMult
......@@ -404,9 +415,7 @@ public class ConflictMap extends MapPb implements IConflict {
.multiply(this.coefMult));
}
}
}
assert slackConflict().signum() < 0;
// cutting plane
......
......@@ -64,6 +64,10 @@ public class PBSolverStats extends SolverStats {
public long numberOfDerivationSteps;
public long numberOfRemainingUnassigned;
public long numberOfRemainingAssigned;
@Override
public void reset() {
super.reset();
......@@ -78,6 +82,8 @@ public class PBSolverStats extends SolverStats {
this.numberOfEndingSkipping = 0;
this.numberOfInternalSkipping = 0;
this.numberOfDerivationSteps = 0;
this.numberOfRemainingUnassigned = 0;
this.numberOfRemainingAssigned = 0;
}
@Override
......@@ -116,6 +122,10 @@ public class PBSolverStats extends SolverStats {
out.println(prefix + "number of skipped derivation steps \t: "
+ (this.numberOfInternalSkipping
+ this.numberOfEndingSkipping));
out.println(prefix + "number of remaining unassigned \t: "
+ this.numberOfRemainingUnassigned);
out.println(prefix + "number of remaining assigned \t: "
+ this.numberOfRemainingAssigned);
}
}
* #variable= 6 #constraint= 3
*
explain: x1 x2 x3 x4 x5 ;
* P 1.0.0 requires either PP 1.0.0
-1 x2 +1 x1 >= 0;
* 1223597333557 0.0.0.1223597333557 requires either P 1.0.0
......
......@@ -189,21 +189,13 @@ Sat4j is a full featured boolean reasoning library designed to bring state-of-th
</plugin>
<plugin>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.6.0</version>
<version>3.6.2</version>
<configuration>
<source>${javaSource}</source>
<target>${javaTarget}</target>
<testSource>${testSource}</testSource>
<testTarget>${testTarget}</testTarget>
<compilerId>jdt</compilerId>
</configuration>
<dependencies>
<dependency>
<groupId>org.eclipse.tycho</groupId>
<artifactId>tycho-compiler-jdt</artifactId>
<version>0.23.0</version>
</dependency>
</dependencies>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
......
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