Merge remote-tracking branch 'upstream/master'

README.md

@@ -3,16 +3,21 @@ Kodkod
 
 This repository includes the source code for the
 [Kodkod](http://emina.github.io/kodkod/) solver for relational
-logic.  Kodkod provides a clean Java [API](http://emina.github.io/kodkod/release/current/doc/) for constructing,
+logic.  Kodkod provides a clean Java [API](http://emina.github.io/kodkod/doc/) for constructing,
 manipulating, and solving relational constraints. The
 source code is extensively documented, and the repository includes
 many [examples](https://github.com/emina/kodkod/tree/master/examples/kodkod/examples) demonstrating the use of the Kodkod API.
 
 Kodkod is open-source and available under the [MIT license](LICENSE). However, the implementation relies on third-party SAT solvers ([SAT4J](http://www.sat4j.org), [MiniSat](http://minisat.se), [Glucose](http://www.labri.fr/perso/lsimon/glucose/), and [(P)Lingeling](http://fmv.jku.at/lingeling/)), some of which are released under stricter licenses. Please see the solver licenses for details.  
 
-### Building and installing Kodkod
+### Downloading Kodkod
 
-The following compilation and installation instructions have been
+The easiest way to get started is to [download](https://github.com/emina/kodkod/releases) the latest release, which includes precompiled binaries for Kodkod and various SAT solvers. You will need Java 8 running on Linux or Mac OS X.
+
+
+### Building Kodkod
+
+The following instructions for building Kodkod from source have been
 tested on Linux (Fedora 22 with gcc 5.1.1) and on Mac OS X (10.10.5 with clang 6.0 and gcc 4.9). You may
 need to modify the build scripts for other operating systems.
 
@@ -23,8 +28,8 @@ point to the JDK 8 home directory.
 
 * Set the JAVA_HOME variable.  For example, on OS X:
 
-  ``$ export JAVA_HOME=`/usr/libexec/java_home` `` 
-  
+  ``$ export JAVA_HOME=`/usr/libexec/java_home` ``
+
 * Clone the kodkod repository:
 
   `$ git clone https://github.com/emina/kodkod.git`  
@@ -41,11 +46,11 @@ point to the JDK 8 home directory.
   `$ waf configure --prefix=. --libdir=lib build install`  
 
 ### Running Kodkod
-	
-[Download](http://emina.github.io/kodkod/download.html) (or [build](https://github.com/emina/kodkod#building-and-installing-kodkod)) the ``kodkod.jar`` binary, solver binaries, and the ``examples.jar`` binary. Assuming that the current working directory contains these binaries, run the  [Sudoku example](https://github.com/emina/kodkod/blob/master/examples/kodkod/examples/sudoku/Sudoku.java) as follows:
+
+[Download](#downloading-kodkod) or [build](#building-kodkod) the ``kodkod.jar`` binary, solver binaries, and the ``examples.jar`` binary. Assuming that the current working directory contains these binaries, run the  [Sudoku example](https://github.com/emina/kodkod/blob/master/examples/kodkod/examples/sudoku/Sudoku.java) as follows:
 
   `$ java -cp kodkod.jar:examples.jar -Djava.library.path=. kodkod.examples.sudoku.Sudoku`  
-  
+
 The program will produce a solution to a sample Sudoku puzzle:
 
 ```
@@ -54,23 +59,16 @@ primary variables: 486
 translation time: 176 ms
 solving time: 2 ms
 +-------+-------+-------+
-| 6 4 7 | 2 1 3 | 9 5 8 | 
-| 9 1 8 | 5 6 4 | 7 2 3 | 
-| 2 5 3 | 8 7 9 | 4 6 1 | 
+| 6 4 7 | 2 1 3 | 9 5 8 |
+| 9 1 8 | 5 6 4 | 7 2 3 |
+| 2 5 3 | 8 7 9 | 4 6 1 |
 +-------+-------+-------+
-| 1 9 5 | 6 4 7 | 8 3 2 | 
-| 4 8 2 | 3 5 1 | 6 7 9 | 
-| 7 3 6 | 9 2 8 | 1 4 5 | 
+| 1 9 5 | 6 4 7 | 8 3 2 |
+| 4 8 2 | 3 5 1 | 6 7 9 |
+| 7 3 6 | 9 2 8 | 1 4 5 |
 +-------+-------+-------+
-| 5 7 4 | 1 9 2 | 3 8 6 | 
-| 8 2 9 | 7 3 6 | 5 1 4 | 
-| 3 6 1 | 4 8 5 | 2 9 7 | 
+| 5 7 4 | 1 9 2 | 3 8 6 |
+| 8 2 9 | 7 3 6 | 5 1 4 |
+| 3 6 1 | 4 8 5 | 2 9 7 |
 +-------+-------+-------+
 ```
-
-
-
-
-
-
-

examples/kodkod/examples/alloy/Lists.java

@@ -29,7 +29,7 @@ public final class Lists {
 	private final Relation car, cdr, equivTo, prefixes;
 
 	/**
-	 * Constructs a new isntance of the Lists model.
+	 * Constructs a new instance of the Lists model.
 	 */
 	public Lists() {
 		Thing = Relation.unary("Thing");

examples/kodkod/examples/tptp/ALG212.java

@@ -25,7 +25,7 @@ public final class ALG212 {
 	private final Relation f;
 
 	/**
-	 * Constucts a new instance of ALG212.
+	 * Constructs a new instance of ALG212.
 	 */
 	public ALG212() {
 		f = Relation.nary("f", 4);
@@ -99,7 +99,7 @@ public final Formula associativity() {
 	}
 
 	/**
-	 * Returns the conjuction of all axioms.
+	 * Returns the conjunction of all axioms.
 	 * @return axioms
 	 */
 	public final Formula axioms() { 

examples/kodkod/examples/tptp/NUM374.java

@@ -221,7 +221,7 @@ public final Formula exponentExponent() {
 	}
 
 	/**
-	 * Returns the conjuction of all axioms.
+	 * Returns the conjunction of all axioms.
 	 * @return axioms
 	 */
 	public final Formula axioms() {

src/kodkod/ast/Decl.java

@@ -80,7 +80,7 @@ public final class Decl extends Decls {
 
     /**
      * Returns the expression in this declaration.
-     * @return this.exresssion
+     * @return this.expresssion
      */
     public Expression expression() { return expression;  }
 

src/kodkod/ast/LeafExpression.java

@@ -24,9 +24,9 @@
 /** 
  * An expression with no children.  
  * {@link kodkod.ast.Relation Relation} and {@link kodkod.ast.Variable Variable} 
- * are examples of leaf exressions.  Two leaf expressions are equal 
+ * are examples of leaf expressions.  Two leaf expressions are equal
  * if and only if they refer to the same object.  That is, 
- * leaf1.eauls(leaf2) <=> leaf1 == leaf2.  A leaf has a name, which is 
+ * leaf1.equals(leaf2) <=> leaf1 == leaf2.  A leaf has a name, which is
  * basically a comment for the purpose of printing, viewing, etc.  The name 
  * has no meaning otherwise.  
  * 

src/kodkod/ast/Variable.java

@@ -29,7 +29,7 @@
  * Represents a variable in a {@link QuantifiedFormula quantified formula}, 
  * a {@link Comprehension comprehension expression}, or a {@link SumExpression sum expression}.  
  * Two variables are the same if and only if they
- * refer to the same object.  That is, v1.eauls(v2) <=> v1 == v2.  Each
+ * refer to the same object.  That is, v1.equals(v2) <=> v1 == v2.  Each
  * variable has a name, which is basically a comment for the purpose of 
  * printing, viewing, etc.  The name has no meaning otherwise.  The arity of
  * a variable specifies the arity of expressions over which the variable can

src/kodkod/engine/Evaluator.java

@@ -43,7 +43,7 @@
  * that an Instance i is a solution to a formula f found using options o.
  * If you create an evaluator e such that e.instance = i, but e.options
  * is an Options object with different integer settings than o, 
- * e.evalate(f) may return false. </p>
+ * e.evaluate(f) may return false. </p>
  * 
  * @specfield options: Options
  * @specfield instance: Instance
@@ -103,7 +103,7 @@ public boolean evaluate(Formula formula){
 	}
 
 	/**
-	 * Evaluates the specified expession with respect to the relation-tuple mappings 
+	 * Evaluates the specified expression with respect to the relation-tuple mappings
 	 * given by this.instance and using this.options.
 	 * @return  {@link kodkod.instance.TupleSet set} of tuples to which the expression evaluates given the
 	 * mappings in this.instance and the options in this.options.
@@ -118,7 +118,7 @@ public TupleSet evaluate(Expression expression){
 	}
 
 	/**
-	 * Evaluates the specified int expession with respect to the relation-tuple mappings 
+	 * Evaluates the specified int expression with respect to the relation-tuple mappings
 	 * given by this.instance and using this.options.
 	 * @return  the integer to which the expression evaluates given the
 	 * mappings in this.instance and the options in this.options.

src/kodkod/engine/Solver.java

@@ -158,7 +158,7 @@ public Solution solve(Formula formula, Bounds bounds) throws HigherOrderDeclExce
 	 * to prove the formula's unsatisfiability.
 	 * If the operation is successful, the method returns an iterator over n Solution objects. The outcome
 	 * of the first n-1 solutions is SAT or trivially SAT, and the outcome of the nth solution is UNSAT
-	 * or tirivally  UNSAT.  Note that an unsatisfiability
+	 * or trivially  UNSAT.  Note that an unsatisfiability
 	 * proof will be constructed for the last solution iff this.options specifies the use of a core extracting SATSolver.
 	 * Additionally, the CNF variables in the proof can be related back to the nodes in the given formula 
 	 * iff this.options has variable tracking enabled.  Translation logging also requires that 

src/kodkod/engine/Statistics.java

@@ -89,19 +89,19 @@ public int clauses() {
 	}
 
 	/**
-	 * Returns the number of miliseconds spent
+	 * Returns the number of milliseconds spent
 	 * on translation this.formula to CNF.
-	 * @return the number of miliseconds spent
+	 * @return the number of milliseconds spent
 	 * on translation this.formula to CNF.
 	 */
 	public long translationTime() {
 		return translation;
 	}
 
 	/**
-	 * Returns the number of miliseconds spent
+	 * Returns the number of milliseconds spent
 	 * on solving the CNF encoding of this.formula.
-	 * @return the number of miliseconds spent
+	 * @return the number of milliseconds spent
 	 * on solving the CNF encoding of this.formula.
 	 */
 	public long solvingTime() {
@@ -132,4 +132,4 @@ public String toString() {
 		ret.append(" ms");
 		return ret.toString();
 	}
-}
+}

src/kodkod/engine/TrivialProof.java

@@ -52,7 +52,7 @@
 
 /**
  * A proof of unsatisfiability for a trivially unsatisfiable formula.
- * A formula is considered trivally unsatisfiable if its unsatisfiability
+ * A formula is considered trivially unsatisfiable if its unsatisfiability
  * is discovered through translation alone.
  *  
  * @author Emina Torlak
@@ -357,4 +357,4 @@ public void visit(NaryFormula formula) {
 		}
 	}
 
-}
+}

src/kodkod/engine/bool/BooleanMatrix.java

@@ -43,7 +43,7 @@
 /** 
  * <p>An n-dimensional matrix of {@link kodkod.engine.bool.BooleanValue boolean values}.  
  * Boolean matrices are indexed using flat integer indeces.  For example,
- * let m be a the 2 x 3 matrix of boolean variables identifed by labels [0 4 1; 5 10 2].  
+ * let m be the 2 x 3 matrix of boolean variables identified by labels [0 4 1; 5 10 2].
  * Then, m[0] = 0, m[3] = 5, m[5] = 2, etc. </p> 
  * 
  * <p>All values stored in the same matrix must be created by the same {@link kodkod.engine.bool.BooleanFactory circuit factory}.  

src/kodkod/engine/bool/TwosComplementInt.java

@@ -305,7 +305,7 @@ private BooleanValue[] extend(int extwidth) {
 	 * Performs non-restoring signed division of this and the given integer.  Returns 
 	 * the this.factory.bitwidth low-order bits of the quotient if the quotient flag 
 	 * is true; otherwise returns the this.factory.bitwidth low-order bits of the remainder.  
-	 * Both the quotionent and the remainder are given in little endian format.  
+	 * Both the quotient and the remainder are given in little endian format.
 	 * @see Behrooz Parhami, Computer Arithmetic: Algorithms and Hardware Designs,
 	 * Oxford University Press, 2000, pp. 218-221.
 	 * @requires this.factory = d.factory && d instanceof BinaryInt

src/kodkod/engine/fol2sat/FOL2BoolTranslator.java

@@ -136,8 +136,8 @@ BooleanValue cache(Formula formula, BooleanValue translation) {
 	/**
 	 * Translates the given annotated expression into a boolean
 	 * matrix that is a least sound upper bound on the expression's
-	 * value, given the leaf and variable bindings in the 
-	 * the provided interpreter and environment.
+	 * value, given the leaf and variable bindings in the
+	 * provided interpreter and environment.
 	 * @requires interpreter.relations = AnnotatedNode.relations(annotated)
 	 * @return a boolean matrix that is a least sound upper bound on the expression's value
 	 * @throws HigherOrderDeclException  annotated.node contains a higher order declaration
@@ -419,7 +419,7 @@ public final BooleanMatrix visit(UnaryExpression unaryExpr) {
 	 * @param decls the declarations comprehension
 	 * @param param formula the body of the comprehension
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE initially
 	 * @param partialIndex partial index into the provided matrix; should be 0 initially
 	 * @param matrix boolean matrix that will retain the final results; should be an empty matrix of dimensions universe.size^decls.length initially
 	 * @ensures the given matrix contains the translation of the comprehension "{ decls | formula }"
@@ -520,7 +520,7 @@ public final BooleanValue visit(ConstantFormula constant) {
 	 * @param decls formula declarations
 	 * @param formula the formula body
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.FALSE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.FALSE initially
 	 * @param acc the accumulator that contains the top level conjunction; should be an empty AND accumulator initially
 	 * @ensures the given accumulator contains the translation of the formula "all decls | formula"
 	 */
@@ -556,7 +556,7 @@ private void all(Decls decls, Formula formula, int currentDecl, BooleanValue dec
 	 * @param decls formula declarations
 	 * @param formula the formula body
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE initially
 	 * @param acc the accumulator that contains the top level conjunction; should be an empty OR accumulator initially
 	 * @ensures the given accumulator contains the translation of the formula "some decls | formula"
 	 */
@@ -953,7 +953,7 @@ public final Int visit(UnaryIntExpression intExpr) {
 	 * @param decls intexpr declarations
 	 * @param formula the formula body
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE initially
 	 * @param values integer values computed so far
 	 */
 	private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,

src/kodkod/engine/fol2sat/Skolemizer.java

@@ -78,7 +78,7 @@ abstract class Skolemizer extends AbstractReplacer {
 	 * Skolemizes the given annotated formula using the given bounds and options.  If 
 	 * Options.trackFormulas is set and the formula is skolemizable, the resulting annotated
 	 * formula will contain transitive source information for each of its subformulas. 
-	 * Specifically, let f be the returned annotated formula, t be a descendeant of f.node, and
+	 * Specifically, let f be the returned annotated formula, t be a descendant of f.node, and
 	 * s a descendant of annotated.node from which t was derived.  Then, 
 	 * f.source[t] = annotated.source[s].  If options.trackFormulas is false, no source 
 	 * information will be recorded (i.e. f.source[t] = t for all descendants t of f).
@@ -157,7 +157,7 @@ private Skolemizer(AnnotatedNode<Formula> annotated, Bounds bounds, Options opti
 		super(annotated.sharedNodes());
 
 		// only cache intermediate computations for expressions with no free variables
-		// and formulas with no free variables and no quantified descendents
+		// and formulas with no free variables and no quantified descendants
 
 		for(Node n: annotated.sharedNodes()) {
 			final AbstractDetector fvdetect = annotated.freeVariableDetector();
@@ -274,7 +274,7 @@ public final  Decls visit(Decls decls) {
 	/** 
 	 * Returns the binding for the given variable in the current replacement environment.
 	 * @return the binding for the given variable in the current replacement environment.
-	 * @throws UnboundLeafException  variable not bound in teh replacement environment.
+	 * @throws UnboundLeafException  variable not bound in the replacement environment.
 	 */
 	@Override
 	public final Expression visit(Variable variable) { 

src/kodkod/engine/fol2sat/SymmetryBreaker.java

@@ -259,7 +259,7 @@ private static final BooleanValue leq(BooleanFactory f, List<BooleanValue> l0, L
 	/**
 	 * Let t be the tuple represent by the given arity and tupleIndex.
 	 * This method returns the tuple index of the tuple t' such t'
-	 * is equal to t with each occurence of atomIndex0
+	 * is equal to t with each occurrence of atomIndex0
 	 * replaced by atomIndex1 and vice versa.
 	 * @return the index of the tuple to which the given symmetry
 	 * maps the tuple specified by arith and tupleIndex
@@ -318,7 +318,7 @@ public int compare(RelationPredicate o1, RelationPredicate o2) {
 	 * this.bounds.upperBound[acyclic.relation] is the cross product of some partition in this.symmetries with
 	 * itself. Assuming that this is the case, we then break symmetry on acyclic.relation using one of the methods
 	 * described in {@linkplain #breakMatrixSymmetries(Map, boolean)}; the method used depends
-	 * on the value of the "agressive" flag.
+	 * on the value of the "aggressive" flag.
 	 * The partition that formed the upper bound of acylic.relation is removed from this.symmetries.</p>
 	 * 
 	 * @return null if symmetry cannot be broken on acyclic; otherwise returns a formula
@@ -370,13 +370,13 @@ private final Formula breakAcyclic(RelationPredicate.Acyclic acyclic, boolean ag
 	 * cross-multiplied with itself gives the upper bound of total.relation. Assuming that this is the case, 
 	 * we then break symmetry on total.relation, total.first, total.last, and total.ordered using one of the methods
 	 * described in {@linkplain #breakMatrixSymmetries(Map, boolean)}; the method used depends
-	 * on the value of the "agressive" flag.
+	 * on the value of the "aggressive" flag.
 	 * The partition that formed the upper bound of total.ordered is removed from this.symmetries.</p>
 	 * 
 	 * @return null if symmetry cannot be broken on total; otherwise returns a formula
 	 * f such that the meaning of total with respect to this.bounds is equivalent to the
 	 * meaning of f with respect to this.bounds' 
-	 * @ensures this.symmetries and this.bounds are modified as desribed in {@linkplain #breakMatrixSymmetries(Map, boolean)} 
+	 * @ensures this.symmetries and this.bounds are modified as described in {@linkplain #breakMatrixSymmetries(Map, boolean)}
 	 * iff total.first, total.last, and total.ordered have the same upper bound, which, when 
 	 * cross-multiplied with itself gives the upper bound of total.relation
 	 * 

src/kodkod/engine/fol2sat/SymmetryDetector.java

@@ -247,7 +247,7 @@ private void refinePartitions(IntSet set) {
 	 * Returns an IntSet that can store elements
 	 * in the range [0..size), and that holds
 	 * the given number.
-	 * @requries 0 <= num < size
+	 * @requires 0 <= num < size
 	 * @return {s: IntSet | s.ints = num } 
 	 */
 	private static final IntSet oneOf(int size, int num) {