import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns an iterator over this.components, in the increasing order of
 * labels. The returned iterator does not support removal.
 * 
 * @return an iterator over this.components, in the increasing order of
 *         labels.
 */
public Iterator<BooleanValue> iterator() {
	return new Iterator<BooleanValue>() {
		final Iterator<IndexedEntry<BooleanValue>> iter = inputs.iterator();

		public boolean hasNext() {
			return iter.hasNext();
		}

		public BooleanValue next() {
			return iter.next().value();
		}

		public void remove() {
			throw new UnsupportedOperationException();
		}

	};
	// return inputs.iterator();
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a new matrix such that an entry in the returned matrix represents
 * a conjunction of the corresponding entries in this and other matrix. The
 * effect of this method is the same as calling
 * this.compose(ExprOperator.Binary.AND, other).
 *
 * @return { m: BooleanMatrix | m.dimensions = this.dimensions && m.factory
 *         = this.factory && all i: [0..m.dimensions.capacity) |
 *         m.elements[i] = this.elements[i] AND other.elements[i] }
 * @throws NullPointerException other = null
 * @throws IllegalArgumentException
 *             !other.dimensions.equals(this.dimensions) || this.factory !=
 *             other.factory
 */
public final BooleanMatrix and(BooleanMatrix other) {
	checkFactory(this.factory, other.factory);
	checkDimensions(this.dims, other.dims);

	final BooleanMatrix ret = new BooleanMatrix(dims, factory, cells, other.cells);
	ret.mergeDefConds(this, other);

	final SparseSequence<BooleanValue> s1 = other.cells;
	if (cells.isEmpty() || s1.isEmpty())
		return ret;
	for (IndexedEntry<BooleanValue> e0 : cells) {
		BooleanValue v1 = s1.get(e0.index());
		if (v1 != null)
			ret.fastSet(e0.index(), factory.and(e0.value(), v1));
	}
	return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a new matrix such that an entry in the returned matrix represents
 * a combination of the corresponding entries in this and other matrix. The
 * effect of this method is the same as calling
 * this.compose(ExprOperator.Binary.OR, other).
 *
 * @return { m: BooleanMatrix | m.dimensions = this.dimensions && m.factory
 *         = this.factory && all i: [0..m.dimensions.capacity) |
 *         m.elements[i] = this.elements[i] OR other.elements[i] }
 * @throws NullPointerException other = null
 * @throws IllegalArgumentException
 *             !other.dimensions.equals(this.dimensions) || this.factory !=
 *             other.factory
 */
public final BooleanMatrix or(BooleanMatrix other) {
	checkFactory(this.factory, other.factory);
	checkDimensions(this.dims, other.dims);
	if (this.cells.isEmpty())
		return other.clone();
	else if (other.cells.isEmpty())
		return this.clone();

	final BooleanMatrix ret = new BooleanMatrix(dims, factory, cells, other.cells);
	ret.mergeDefConds(this, other);

	final SparseSequence<BooleanValue> retSeq = ret.cells;
	for (IndexedEntry<BooleanValue> e0 : cells) {
		BooleanValue v1 = other.cells.get(e0.index());
		if (v1 == null)
			retSeq.put(e0.index(), e0.value());
		else
			retSeq.put(e0.index(), factory.or(e0.value(), v1));
	}
	for (IndexedEntry<BooleanValue> e1 : other.cells) {
		if (!cells.containsIndex(e1.index()))
			retSeq.put(e1.index(), e1.value());
	}
	return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns the cross product of this and other matrix, using conjunction
 * instead of multiplication.
 *
 * @return { m: BooleanMatrix | m = this x other }
 * @throws NullPointerException other = null
 * @throws IllegalArgumentException this.factory != other.factory
 */
public final BooleanMatrix cross(final BooleanMatrix other) {
	checkFactory(this.factory, other.factory);

	final BooleanMatrix ret = new BooleanMatrix(dims.cross(other.dims), factory, cells, other.cells);
	ret.mergeDefConds(this, other);

	if (cells.isEmpty() || other.cells.isEmpty())
		return ret;

	final int ocap = other.dims.capacity();
	for (IndexedEntry<BooleanValue> e0 : cells) {
		int i = ocap * e0.index();
		for (IndexedEntry<BooleanValue> e1 : other.cells) {
			BooleanValue conjunction = factory.and(e0.value(), e1.value());
			if (conjunction != FALSE)
				ret.cells.put(i + e1.index(), conjunction);
		}
	}

	return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns the transitive closure of this matrix.
 *
 * @return { m: BooleanMatrix | m = ^this }
 * @throws UnsupportedOperationException #this.diensions != 2 ||
 *             !this.dimensions.square()
 */
public final BooleanMatrix closure() {
	if (dims.numDimensions() != 2 || !dims.isSquare()) {
		throw new UnsupportedOperationException("#this.diensions != 2 || !this.dimensions.square()");
	}
	if (cells.isEmpty())
		return clone();

	// System.out.println("closure of " + this);
	BooleanMatrix ret = this;

	// compute the number of rows in the matrix
	int rowNum = 0;
	final int rowFactor = dims.dimension(1);
	for (IndexedEntry<BooleanValue> rowLead = cells.first(); rowLead != null; rowLead = cells
			.ceil(((rowLead.index() / rowFactor) + 1) * rowFactor)) {
		rowNum++;
	}

	// compute closure using iterative squaring
	for (int i = 1; i < rowNum; i *= 2) {
		ret = ret.or(ret.dot(ret));
	}
	// System.out.println(ret);
	return ret == this ? clone() : ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Overrides the values in this matrix with those in <code>other</code>.
 * Specifically, for each index i of the returned matrix m, m.elements[i] is
 * true iff other.elements[i] is true or this.elements[i] is true and all
 * elements of <code>other</code> that are in the same row as i are false.
 * 
 * @return {m: BooleanMatrix | m.dimensions = this.dimensions && all i:
 *         [0..m.capacity()) | m.elements[i] = other.elements[i] ||
 *         this.elements[i] && !OR(other.elements[row(i)]) } where
 *         other.elements[row(i)] selects all elements of <code>other</code>
 *         that are in the same row as i.
 * @throws NullPointerException other = null
 * @throws IllegalArgumentException other.dimensions != this.dimensions
 */
public final BooleanMatrix override(BooleanMatrix other) {
	checkFactory(this.factory, other.factory);
	checkDimensions(this.dims, other.dims);
	if (other.cells.isEmpty())
		return this.clone();

	final BooleanMatrix ret = new BooleanMatrix(dims, factory, cells, other.cells);
	ret.mergeDefConds(this, other);

	ret.cells.putAll(other.cells);
	final int rowLength = dims.capacity() / dims.dimension(0);
	int row = -1;
	BooleanValue rowVal = BooleanConstant.TRUE;
	for (IndexedEntry<BooleanValue> e0 : cells) {
		int e0row = e0.index() / rowLength;
		if (row != e0row) {
			row = e0row;
			rowVal = other.nand(row * rowLength, (row + 1) * rowLength);
		}
		ret.fastSet(e0.index(), factory.or(ret.fastGet(e0.index()), factory.and(e0.value(), rowVal)));
	}
	return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a BooleanValue that constrains at most one value in this.elements
 * to be true. The effect of this method is the same as calling
 * this.factory.or(this.one(), this.none()).
 * 
 * @return { f: BooleanValue | f <=> this.one() || this.none() }
 */
public final BooleanValue lone(Environment< ? , ? > env) {
	if (cells.isEmpty())
		return TRUE;
	else {
		final BooleanAccumulator g = BooleanAccumulator.treeGate(AND);

		BooleanValue partial = FALSE;
		for (IndexedEntry<BooleanValue> e : cells) {
			if (g.add(factory.or(e.value().negation(), partial.negation())) == FALSE)
				return FALSE;
			partial = factory.or(partial, e.value());
		}

		final BooleanValue val = factory.accumulate(g);
		return DefCond.ensureDef(factory, env, val, this.defCond());
	}
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a BooleanValue that constraints exactly one value in
 * this.elements to be true.
 * 
 * @return { f: BooleanValue | f <=> #this.elements[int] = 1 }
 */
public final BooleanValue one(Environment< ? , ? > env) {
	if (cells.isEmpty())
		return FALSE;
	else {
		final BooleanAccumulator g = BooleanAccumulator.treeGate(AND);

		BooleanValue partial = FALSE;
		for (IndexedEntry<BooleanValue> e : cells) {
			if (g.add(factory.or(e.value().negation(), partial.negation())) == FALSE)
				return FALSE;
			partial = factory.or(partial, e.value());
		}
		g.add(partial);

		final BooleanValue val = factory.accumulate(g);
		return DefCond.ensureDef(factory, env, val, this.defCond());
	}
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows (where A_0...A_|A| stand
 * for boolean variables that represent the tuples of the expression A,
 * etc.): let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }"
 * | { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b,
 * ..., x) }.
 * 
 * @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 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 }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, BooleanValue declConstraints,
		int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl == decls.size()) {
		// TODO: what about this and overflow???
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int) StrictMath.pow(interpreter.universe().size(), decls.size() - currentDecl - 1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for (IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl + 1, factory.and(entry.value(), declConstraints),
				partialIndex + entry.index() * position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);
	}
	env = env.parent();
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows (where A_0...A_|A| stand
 * for boolean variables that represent the tuples of the expression A,
 * etc.): let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " | sum a:
 * A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b,
 * ..., x) else 0 }.
 * 
 * @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 values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size() == currentDecl) {
		Int intExpr = expr.accept(this);
		Int newInt = intExpr.choice(declConstraints, factory.integer(0));
		values.add(newInt);
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for (IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl + 1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);
	}
	env = env.parent();
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
		 * Returns an iterator over this.components, in
		 * the increasing order of labels.  The returned iterator
		 * does not support removal.
		 * @return an iterator over this.components, in the
		 * increasing order of labels.
		 */
		public Iterator<BooleanValue> iterator() {
			return new Iterator<BooleanValue>() {
				final Iterator<IndexedEntry<BooleanValue>> iter = inputs.iterator();
				public boolean hasNext() {
					return iter.hasNext();
				}

				public BooleanValue next() {
					return iter.next().value();
				}

				public void remove() {
					throw new UnsupportedOperationException();
				}
				
			};
//			return inputs.iterator();
		}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a new matrix such that an entry in the returned matrix represents a 
 * combination of the corresponding entries in this and other matrix.  The effect 
 * of this method is the same as calling this.compose(ExprOperator.Binary.OR, other).
 * 
 * @return { m: BooleanMatrix | m.dimensions = this.dimensions && m.factory = this.factory &&
 *                              all i: [0..m.dimensions.capacity) | 
 *                               m.elements[i] = this.elements[i] OR other.elements[i] }
 * @throws NullPointerException  other = null 
 * @throws IllegalArgumentException  !other.dimensions.equals(this.dimensions) || this.factory != other.factory
 */
public final BooleanMatrix or(BooleanMatrix  other) {
    checkFactory(this.factory, other.factory); checkDimensions(this.dims, other.dims);
    
    final BooleanMatrix ret = new BooleanMatrix(dims, factory, cells, other.cells);
    ret.mergeDefConds(this, other);
    
    final SparseSequence<BooleanValue> retSeq = ret.cells;
    for(IndexedEntry<BooleanValue> e0 : cells) {
        BooleanValue v1 = other.cells.get(e0.index());
        if (v1==null)
            retSeq.put(e0.index(), e0.value());
        else
            retSeq.put(e0.index(), factory.or(e0.value(), v1));
    }
    for(IndexedEntry<BooleanValue> e1 : other.cells) {
        if (!cells.containsIndex(e1.index()))
            retSeq.put(e1.index(), e1.value());
    }
    return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns the cross product of this and other matrix, using conjunction instead of 
 * multiplication.
 * 
 * @return { m: BooleanMatrix | m = this x other }
 * @throws NullPointerException  other = null
 * @throws IllegalArgumentException  this.factory != other.factory
 */
public final BooleanMatrix cross(final BooleanMatrix other) {
    checkFactory(this.factory, other.factory);
    
    final BooleanMatrix ret =  new BooleanMatrix(dims.cross(other.dims), factory, cells, other.cells);
    ret.mergeDefConds(this, other);
    
    if (cells.isEmpty() || other.cells.isEmpty()) return ret;
    
    final int ocap = other.dims.capacity();
    for(IndexedEntry<BooleanValue> e0 : cells) {
        int i = ocap * e0.index();
        for(IndexedEntry<BooleanValue> e1: other.cells) {
            BooleanValue conjunction = factory.and(e0.value(), e1.value());
            if (conjunction != FALSE)
                ret.cells.put(i + e1.index(), conjunction);
        }
    }
    
    return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
     * Returns the transitive closure of this matrix.
     * 
     * @return { m: BooleanMatrix | m = ^this }
     * @throws UnsupportedOperationException  #this.diensions != 2 || !this.dimensions.square()
     */
    public final BooleanMatrix closure() {
        if (dims.numDimensions() != 2 || !dims.isSquare()) {
            throw new UnsupportedOperationException("#this.diensions != 2 || !this.dimensions.square()");
        }
        if (cells.isEmpty())
            return clone();
        
//      System.out.println("closure of " + this);
        BooleanMatrix ret = this;
    
        // compute the number of rows in the matrix
        int rowNum = 0;
        final int rowFactor = dims.dimension(1);
        for(IndexedEntry<BooleanValue> rowLead = cells.first(); 
            rowLead != null; rowLead = cells.ceil(((rowLead.index()/rowFactor) + 1) * rowFactor)) {
            rowNum++; 
        }   
        
        // compute closure using iterative squaring
        for(int i = 1; i < rowNum; i*=2) {
            ret = ret.or(ret.dot(ret));
        }
//      System.out.println(ret);
        return ret==this ? clone() : ret;
    }
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a boolean matrix m such that m = this if the given condition evaluates
 * to TRUE and m = other otherwise.
 * 
 * @return { m: BooleanMatrix | m.dimensions = this.dimensions &&
 *                              all i: [0..m.dimensions.capacity) | 
 *                                 m.elements[i] = condition => this.elements[i], other.elements[i] }
 * @throws NullPointerException  other = null || condition = null
 * @throws IllegalArgumentException  !other.dimensions.equals(this.dimensions) || this.factory != other.factory
 */
public final BooleanMatrix choice(BooleanValue condition, BooleanMatrix other) {
    checkFactory(this.factory, other.factory); checkDimensions(this.dims, other.dims);
    if (condition==TRUE) return this.clone();
    else if (condition==FALSE) return other.clone();

    final BooleanMatrix ret =  new BooleanMatrix(dims, factory);
    final SparseSequence<BooleanValue> otherCells = other.cells;
    for(IndexedEntry<BooleanValue> e0 : cells) {
        BooleanValue v1 = otherCells.get(e0.index());
        if (v1==null)
            ret.fastSet(e0.index(), factory.and(condition, e0.value()));
        else
            ret.fastSet(e0.index(), factory.ite(condition, e0.value(), v1));
    }
    for(IndexedEntry<BooleanValue> e1 : other.cells) {
        if (!cells.containsIndex(e1.index()))
            ret.fastSet(e1.index(), factory.and(condition.negation(), e1.value()));
    }
    
    BooleanValue of = factory.ite(condition, defCond().getOverflow(), other.defCond().getOverflow());
    BooleanValue accumOF = factory.ite(condition, defCond().getAccumOverflow(), other.defCond().getAccumOverflow());
    ret.defCond().setOverflows(of, accumOF);
    return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Overrides the values in this matrix with those in <code>other</code>.
 * Specifically, for each index i of the returned matrix m,
 * m.elements[i] is true iff other.elements[i] is true or
 * this.elements[i] is true and all elements of <code>other</code> 
 * that are in the same row as i are false.
 * @return {m: BooleanMatrix | m.dimensions = this.dimensions &&
 *                             all i: [0..m.capacity()) | m.elements[i] = 
 *                               other.elements[i] || 
 *                               this.elements[i] && !OR(other.elements[row(i)]) }
 * where other.elements[row(i)] selects all elements of <code>other</code>
 * that are in the same row as i.  
 * @throws NullPointerException  other = null
 * @throws IllegalArgumentException  other.dimensions != this.dimensions
 */
public final BooleanMatrix override(BooleanMatrix other) {
    checkFactory(this.factory, other.factory); checkDimensions(this.dims, other.dims);
    if (other.cells.isEmpty()) return this.clone();
    
    final BooleanMatrix ret = new BooleanMatrix(dims, factory, cells, other.cells);
    ret.mergeDefConds(this, other);
    
    ret.cells.putAll(other.cells);
    final int rowLength = dims.capacity() / dims.dimension(0);
    int row = -1;
    BooleanValue rowVal = BooleanConstant.TRUE;
    for(IndexedEntry<BooleanValue> e0 : cells) {
        int e0row = e0.index() / rowLength;
        if (row != e0row) {
            row = e0row;
            rowVal = other.nand(row*rowLength, (row+1)*rowLength);
        }
        ret.fastSet(e0.index(), factory.or(ret.fastGet(e0.index()), 
                   factory.and(e0.value(), rowVal)));
    }
    return ret;
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a BooleanValue that constrains at most one value in this.elements to be true.
 * The effect of this method is the same as calling this.factory.or(this.one(), this.none()).
 * @return { f: BooleanValue | f <=> this.one() || this.none() }
 */
public final BooleanValue lone(Environment<?, ?> env) {
    if (cells.isEmpty())
        return TRUE; 
    else {
        final BooleanAccumulator g = BooleanAccumulator.treeGate(AND);
        
        BooleanValue partial = FALSE;
        for(IndexedEntry<BooleanValue> e: cells) {
            if (g.add(factory.or(e.value().negation(), partial.negation()))==FALSE)
                return FALSE;
            partial = factory.or(partial, e.value());
        }

        final BooleanValue val = factory.accumulate(g);
        return DefCond.ensureDef(factory, env, val, this.defCond());
    }
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Returns a BooleanValue that constraints exactly one value in this.elements to be true.
 * @return { f: BooleanValue | f <=> #this.elements[int] = 1 }
 */
public final BooleanValue one(Environment<?, ?> env) {
    if (cells.isEmpty())
        return FALSE; 
    else {
        final BooleanAccumulator g = BooleanAccumulator.treeGate(AND);
        
        BooleanValue partial = FALSE;
        for(IndexedEntry<BooleanValue> e: cells) {
            if (g.add(factory.or(e.value().negation(), partial.negation()))==FALSE)
                return FALSE;
            partial = factory.or(partial, e.value());
        }
        g.add(partial);
        
        final BooleanValue val = factory.accumulate(g);
        return DefCond.ensureDef(factory, env, val, this.defCond());
    }
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }" |
 *     { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b, ..., x) }.
 * @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 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 }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, 
		BooleanValue declConstraints, int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl==decls.size()) {
	    //TODO: what about this and overflow???
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int)StrictMath.pow(interpreter.universe().size(), decls.size()-currentDecl-1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), 
				partialIndex + entry.index()*position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.util.ints.IndexedEntry; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " |
 *     sum a: A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b, ..., x) else 0 }.
 * @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 values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size()==currentDecl) {
		Int intExpr = expr.accept(this);
           Int newInt = intExpr.choice(declConstraints, factory.integer(0));
           values.add(newInt);
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl+1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}