Release 0.3.10

Makefile

@@ -15,4 +15,4 @@ clean:
 install:
 	mkdir -p $(to)
 	cp -f README.md $(to)/chocosolver-README.md
-	cp -f target/chocosolver-0.3.9-jar-with-dependencies.jar $(to)/chocosolver.jar
+	cp -f target/chocosolver-0.3.10-jar-with-dependencies.jar $(to)/chocosolver.jar

README.md

@@ -1,7 +1,7 @@
 chocosolver
 ===========
 
-v0.3.9
+v0.3.10
 
 A backend for [Clafer](http://clafer.org) using the Choco 3.3 constraint programming library. There are two ways to use the project: programmatically via the Java API, or the Javascript CLI.
 
@@ -10,13 +10,15 @@ Contributors
 
 * [Jimmy Liang](http://gsd.uwaterloo.ca/jliang), MSc. Candidate. Main developer.
 * [Michal Antkiewicz](http://gsd.uwaterloo.ca/mantkiew), Research Engineer. Release Management, testing.
+* [Alexandr Murashkin](http://gsd.uwaterloo.ca/amurashk). Stress testing.
+* [Jordan Ross](http://gsd.uwaterloo.ca/j25ross). Stress testing.
 
 Getting Clafer Tools
 --------------------
 
 ### Installation from binaries
 
-Binary distributions of the release 0.3.9 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from [Clafer Tools - Binary Distributions](http://http://gsd.uwaterloo.ca/clafer-tools-binary-distributions). 
+Binary distributions of the release 0.3.10 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from [Clafer Tools - Binary Distributions](http://http://gsd.uwaterloo.ca/clafer-tools-binary-distributions).
 
 1. download the binaries and unpack `<target directory>` of your choice
 2. add the `<target directory>` to your system path so that the executables can be found
@@ -25,20 +27,29 @@ Binary distributions of the release 0.3.9 of Clafer Tools for Windows, Mac, and
 
 Prerequisites
 -------------
-* [Choco 3](https://github.com/chocoteam/choco3) v3.3.0
+* [Choco 3](https://github.com/chocoteam/choco3) v3.3.1-SNAPSHOT
 * [Java 8+](http://www.oracle.com/technetwork/java/javase/downloads/index.html)
 * [Maven 3](http://maven.apache.org/) - Required for building the project.
 
 Optional
 --------
-* [Clafer compiler](https://github.com/gsdlab/clafer) - This backend provides an API for solving Clafer models. The Clafer compiler can compile a Clafer model down to the proper API calls. Can also be done manually by hand quite easily with a bit of typing (examples down below). v0.3.9.
+* [Clafer compiler](https://github.com/gsdlab/clafer) - This backend provides an API for solving Clafer models. The Clafer compiler can compile a Clafer model down to the proper API calls. Can also be done manually by hand quite easily with a bit of typing (examples down below). v0.3.10.
 
 Follow the installation instructions in the [README.md](https://github.com/gsdlab/clafer#clafer).
 
 Installation
 ------------
 
+Install Choco3 development snapshot:
+
+```bash
+git clone https://github.com/chocoteam/choco3.git -b develop
+cd choco3
+mvn install -DskipTests
+```
+
 Install the API and CLI.
+
 ```bash
 git clone https://github.com/gsdlab/chocosolver.git
 cd chocosolver
@@ -51,15 +62,15 @@ Include the following XML snippet in your POM to use the API in your Maven proje
 <dependency>
     <groupId>org.clafer</groupId>
     <artifactId>chocosolver</artifactId>
-    <version>0.3.9</version>
+    <version>0.3.10</version>
 </dependency>
 ```
-The CLI is installed to target/chocosolver-0.3.9-jar-with-dependencies.jar. Start the CLI using the command "java -jar chocosolver-0.3.9-jar-with-dependencies.jar mymodel.js".
+The CLI is installed to target/chocosolver-0.3.10-jar-with-dependencies.jar. Start the CLI using the command "java -jar chocosolver-0.3.10-jar-with-dependencies.jar mymodel.js".
 
 ### Important: Branches must correspond
 
-All related projects are following the *simultaneous release model*. 
-The branch `master` contains releases, whereas the branch `develop` contains code under development. 
+All related projects are following the *simultaneous release model*.
+The branch `master` contains releases, whereas the branch `develop` contains code under development.
 When building the tools, the branches should match.
 Releases from branches 'master` are guaranteed to work well together.
 Development versions from branches `develop` should work well together but this might not always be the case.
@@ -83,7 +94,7 @@ import static org.clafer.ast.Asts.*;
 
 public static void main(String[] args) {
     AstModel model = newModel();
-    
+
     AstConcreteClafer installation = model.addChild("Installation").withCard(Mandatory);
         // withCard(Mandatory) and withCard(1, 1) is the same. Pick the one you find more readable.
         AstConcreteClafer status = installation.addChild("Status").withCard(1, 1).withGroupCard(1, 1);
@@ -109,7 +120,7 @@ import org.clafer.scope.*;
 
 public static void main(String[] args) {
     ...
-    ClaferSolver solver = ClaferCompiler.compile(model, 
+    ClaferSolver solver = ClaferCompiler.compile(model,
         Scope.setScope(installation, 1).setScope(status, 1).setScope(ok, 1).setScope(bad, 1).setScope(time, 1)
         // Set the scope of every Clafer to 1. The code above could be replaced with
         // "Scope.defaultScope(1)".
@@ -130,16 +141,16 @@ Optimizing on a single objective is supported. Suppose we wanted to optimize on
 ```java
 import org.clafer.objective.*;
 ...
-ClaferOptimizer solver = ClaferCompiler.compile(model, 
-    Scope.defaultScope(1).intLow(-16).intHigh(16), 
+ClaferOptimizer solver = ClaferCompiler.compile(model,
+    Scope.defaultScope(1).intLow(-16).intHigh(16),
     Objective.maximize(sum(global(time))));
 while (solver.find()) {
     // The instances where time is maximal.
     System.out.println(solver.instance());
 }
 
-solver = ClaferCompiler.compile(model, 
-    Scope.defaultScope(1).intLow(-16).intHigh(16), 
+solver = ClaferCompiler.compile(model,
+    Scope.defaultScope(1).intLow(-16).intHigh(16),
     Objective.minimize(sum(global(time))));
 while (solver.find()) {
     // The instances where time is minimal.
@@ -236,7 +247,7 @@ For this backend, the constraint is always unsatisfiable. For the Alloy backend,
 Possible Future Work?
 ---------------------
 * API for choosing branching strategy. Two reasons. The advantage of constraint programming is the ability to tune the solver to the specific problem. Choosing the right branching strategy can make a world of difference. Secondly, it allows the user to control the order of instances generated. For example, the user would like to see instances where Feature A is present and Feature B is absent before any other instances. This can be done by choosing the branching strategy.
-* Transitive closure, inverse 
+* Transitive closure, inverse
 * Reals
 
 Need help?

pom.xml

@@ -5,7 +5,7 @@
 
     <groupId>org.clafer</groupId>
     <artifactId>chocosolver</artifactId>
-    <version>0.3.9</version>
+    <version>0.3.10</version>
     <packaging>jar</packaging>
 
     <name>chocosolver</name>
@@ -27,7 +27,7 @@
         <dependency>
             <groupId>org.choco-solver</groupId>
             <artifactId>choco-solver</artifactId>
-            <version>3.3.0</version>
+            <version>3.3.1-SNAPSHOT</version>
         </dependency>
         <dependency>
             <groupId>org.mozilla</groupId>

src/main/java/org/clafer/ast/compiler/AstCompiler.java

@@ -86,6 +86,7 @@
 import org.clafer.collection.Pair;
 import org.clafer.collection.Triple;
 import org.clafer.common.Check;
+import org.clafer.common.UnsatisfiableException;
 import org.clafer.common.Util;
 import org.clafer.graph.GraphUtil;
 import org.clafer.graph.KeyGraph;
@@ -95,6 +96,7 @@
 import org.clafer.domain.Domain;
 import org.clafer.domain.Domains;
 import static org.clafer.domain.Domains.*;
+import org.clafer.ir.IllegalIntException;
 import org.clafer.ir.IrExpr;
 import org.clafer.ir.IrIntArrayExpr;
 import org.clafer.ir.IrIntExpr;
@@ -112,7 +114,6 @@
 import org.clafer.ir.Sum;
 import org.clafer.objective.Objective;
 import org.clafer.scope.Scope;
-import org.clafer.scope.ScopeBuilder;
 
 /**
  * Compile from AST to IR.
@@ -1313,7 +1314,11 @@ public IrExpr visit(AstArithm ast, Void a) {
                 case Sub:
                     return sub(operands);
                 case Mul:
-                    return mul(operands, getMulRange());
+                    try {
+                        return mul(operands, getMulRange());
+                    } catch (IllegalIntException e) {
+                        throw new UnsatisfiableException(e);
+                    }
                 case Div:
                     IrIntExpr quotient = operands[0];
                     for (int i = 1; i < operands.length; i++) {

src/main/java/org/clafer/collection/Either.java

@@ -2,7 +2,9 @@
 
 import java.lang.reflect.Array;
 import java.util.ArrayList;
+import java.util.HashSet;
 import java.util.List;
+import java.util.Set;
 import org.clafer.common.Check;
 
 /**
@@ -40,6 +42,16 @@ public static <A, B> List<A> filterLeft(List<Either<A, B>> eithers) {
         return lefts;
     }
 
+    public static <A, B> Set<A> filterLeft(Set<Either<A, B>> eithers) {
+        Set<A> lefts = new HashSet<>();
+        for (Either<A, B> either : eithers) {
+            if (either.isLeft()) {
+                lefts.add(either.getLeft());
+            }
+        }
+        return lefts;
+    }
+
     @SafeVarargs
     public static <A, B> A[] filterLeft(Either<A, B>[] eithers, A... array) {
         List<A> lefts = new ArrayList<>();

src/main/java/org/clafer/instance/InstanceClafer.java

@@ -91,7 +91,7 @@ private void print(String indent, Appendable out) throws IOException {
         }
         out.append('\n');
         for (InstanceClafer child : getChildren()) {
-            child.print(indent + "    ", out);
+            child.print(indent + "  ", out);
         }
     }
 

src/main/java/org/clafer/ir/analysis/LinearEquationOptimizer.java

@@ -6,6 +6,8 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import org.clafer.collection.DisjointSets;
+import org.clafer.collection.Either;
 import org.clafer.common.Util;
 import org.clafer.domain.Domain;
 import org.clafer.domain.Domains;
@@ -216,17 +218,28 @@ public static IrModule optimize(IrModule module) {
         if (equations.size() > 0) {
             Map<Variable, IrIntVar> inverse = Util.inverse(map);
 
-            LinearSystem system = new LinearSystem(equations);
-            for (LinearEquation equation : system
-                    .equalityElimination()
-                    .fourierMotzkinElimination()
-                    .strengthenInequalities()
-                    .gaussJordanElimination()
-                    .addEquations(equations)
-                    .dominantElimination()
-                    .getEquations()) {
-                for (IrBoolExpr constraint : boolExpr(equation, inverse)) {
-                    constraints.add(constraint);
+            DisjointSets<Either<LinearEquation, Variable>> ds = new DisjointSets<>();
+            for (LinearEquation equation : equations) {
+                Either<LinearEquation, Variable> left = Either.left(equation);
+                for (Variable variable : equation.getVariables()) {
+                    Either<LinearEquation, Variable> right = Either.right(variable);
+                    ds.union(left, right);
+                }
+            }
+            for (Set<Either<LinearEquation, Variable>> component : ds.connectedComponents()) {
+                Set<LinearEquation> componentEquation = Either.filterLeft(component);
+                LinearSystem system = new LinearSystem(componentEquation);
+                for (LinearEquation equation : system
+                        .equalityElimination()
+                        .fourierMotzkinElimination()
+                        .strengthenInequalities()
+                        .gaussJordanElimination()
+                        .addEquations(componentEquation)
+                        .dominantElimination()
+                        .getEquations()) {
+                    for (IrBoolExpr constraint : boolExpr(equation, inverse)) {
+                        constraints.add(constraint);
+                    }
                 }
             }
             return new IrModule().addConstraints(constraints);

src/main/java/org/clafer/math/LinearSystem.java

@@ -7,6 +7,8 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Iterator;
@@ -88,27 +90,25 @@ public LinearSystem gaussJordanElimination() {
             variableIds.put(variable, id++);
         }
         int slack = 0;
-        Rational[][] rows = new Rational[equations.length][id];
+        MatrixBuilder matrix = new MatrixBuilder(equations.length, id);
         Rational[] column = new Rational[equations.length];
 
-        for (int i = 0; i < rows.length; i++) {
+        for (int i = 0; i < matrix.numberOfRows(); i++) {
             LinearEquation equation = equations[i];
-            Rational[] row = rows[i];
-            Arrays.fill(row, Rational.Zero);
             if (equation.getOp().equals(Op.LessThanEqual)) {
-                row[slack++] = Rational.One;
+                matrix.set(i, slack++, Rational.One);
             }
             LinearFunction function = equation.getLeft();
             for (int j = 0; j < function.getCoefficients().length; j++) {
                 Rational coeffient = function.getCoefficients()[j];
                 int variable = variableIds.get(function.getVariables()[j]);
-                assert row[variable].isZero();
-                row[variable] = coeffient;
+                assert matrix.get(i, variable).isZero();
+                matrix.set(i, variable, coeffient);
             }
             column[i] = equation.getRight();
         }
 
-        Matrix a = new Matrix(rows);
+        Matrix a = matrix.toMatrix();
         Matrix b = new Matrix(column);
         Matrix p = a.addColumns(Matrix.identity(a.numberOfRows())).gaussJordanElimination()
                 .subColumns(a.numberOfColumns());
@@ -300,6 +300,10 @@ private static <T> HashSet<T> singletonHashSet(T t) {
         return set;
     }
 
+    private int tieBreaker(LinearEquation eq1, LinearEquation eq2) {
+        return eq1.getVariables().length - eq2.getVariables().length;
+    }
+
     private boolean cost(LinearEquation equation,
             Map<Variable, Pair<Set<LinearEquation>, Rational>> bestLowBound,
             Map<Variable, Pair<Set<LinearEquation>, Rational>> bestHighBound,
@@ -467,10 +471,10 @@ public LinearSystem fourierMotzkinElimination() {
         Set<LinearEquation> newEquations = new LinkedHashSet<>(
                 bestLowBound.size() + bestHighBound.size());
         for (Pair<Set<LinearEquation>, ?> b : bestLowBound.values()) {
-            newEquations.addAll(b.getFst());
+            newEquations.add(Collections.min(b.getFst(), this::tieBreaker));
         }
         for (Pair<Set<LinearEquation>, ?> b : bestHighBound.values()) {
-            newEquations.addAll(b.getFst());
+            newEquations.add(Collections.min(b.getFst(), this::tieBreaker));
         }
         return new LinearSystem(newEquations);
     }

src/main/java/org/clafer/math/Matrix.java

@@ -1,7 +1,6 @@
 package org.clafer.math;
 
 import gnu.trove.TCollections;
-import gnu.trove.function.TObjectFunction;
 import gnu.trove.iterator.TIntObjectIterator;
 import gnu.trove.map.TIntObjectMap;
 import gnu.trove.map.hash.TIntObjectHashMap;
@@ -43,7 +42,7 @@ public Matrix(Rational[][] rows) {
         }
     }
 
-    private Matrix(TIntObjectHashMap<Rational>[] data, int columns) {
+    Matrix(TIntObjectHashMap<Rational>[] data, int columns) {
         for (TIntObjectHashMap<Rational> d : data) {
             for (Rational o : d.valueCollection()) {
                 if (o.isZero()) {
@@ -107,6 +106,11 @@ public int numberOfColumns() {
         return numberOfColumns;
     }
 
+    public Rational get(int row, int column) {
+        Rational value = rows[row].get(column);
+        return value == null ? Rational.Zero : value;
+    }
+
     public boolean isSquare() {
         return numberOfRows() == numberOfColumns();
     }
@@ -274,19 +278,13 @@ public Matrix gaussJordanElimination() {
                 TIntObjectHashMap<Rational> rowR = matrix[r];
                 final Rational divisor = rowR.get(lead);
                 assert divisor != null;
-                rowR.transformValues(new TObjectFunction<Rational, Rational>() {
-
-                    @Override
-                    public Rational execute(Rational value) {
-                        return value.div(divisor);
-                    }
-                });
+                rowR.transformValues(value -> value.div(divisor));
             }
+            TIntObjectHashMap<Rational> rowR = matrix[r];
             for (i = 0; i < rowCount; i++) {
                 if (i != r) {
                     // Subtract M[i, lead] multiplied by row r from row I
                     TIntObjectHashMap<Rational> rowI = matrix[i];
-                    TIntObjectHashMap<Rational> rowR = matrix[r];
                     Rational multiplier = rowI.get(lead);
                     if (multiplier != null) {
                         TIntObjectIterator<Rational> iter = rowR.iterator();
@@ -322,7 +320,7 @@ public boolean equals(Object obj) {
 
     @Override
     public int hashCode() {
-        return Arrays.deepHashCode(rows);
+        return Arrays.deepHashCode(rows) ^ numberOfColumns;
     }
 
     @Override