public static AnnotatedNode<Formula> flatten(AnnotatedNode<Formula> annotated, boolean breakupQuantifiers) {  
	final FormulaFlattener flat = new FormulaFlattener(annotated.sharedNodes(), breakupQuantifiers);
	annotated.node().accept(flat);
	final List<Formula> roots = new ArrayList<Formula>(flat.conjuncts.size());
	roots.addAll(flat.conjuncts.keySet());
	for(Iterator<Map.Entry<Formula,Node>> itr = flat.conjuncts.entrySet().iterator(); itr.hasNext(); ) { 
		final Map.Entry<Formula, Node> entry = itr.next();
		final Node source = annotated.sourceOf(entry.getValue());
		if (entry.getKey()==source) 	{ itr.remove(); }
		else 							{ entry.setValue(source); }
	}
	return AnnotatedNode.annotate(Formula.and(roots), flat.conjuncts);
} static AnnotatedNode<Formula> skolemize(final AnnotatedNode<Formula> annotated, Bounds bounds, Options options) {
	if (options.logTranslation()>0) {
		final Map<Node,Node> source = new IdentityHashMap<Node,Node>();
		final Skolemizer r = new Skolemizer(annotated, bounds, options) {
			protected Formula source(Formula f, Node n) {
				//System.out.println("logging " + f + " <-- " + n);
				final Node nsource = annotated.sourceOf(n);
				if (f!=nsource) source.put(f, nsource);
				return f;
			}
		};
		final Formula f = annotated.node().accept(r);
		return f==annotated.node() ? annotated : annotate(f, source);
	} else {
		final Skolemizer r = new Skolemizer(annotated, bounds, options) {};
		final Formula f = annotated.node().accept(r);
		return f==annotated.node() ? annotated : annotate(f);
	}
} public static <N extends Node> AnnotatedNode<N> annotate(N node) { return new AnnotatedNode<N>(node); } public static AnnotatedNode<Formula> annotateRoots(Formula formula) { 
	final Formula flat = Formula.and(Nodes.roots(formula));
	return new AnnotatedNode<Formula>(flat, Collections.singletonMap(flat, formula));
} public static final <T> Set<T> setDifference(Set<T> left, Set<T> right) { 
	final Set<T> ret = new LinkedHashSet<T>(left);
	ret.removeAll(right);
	return ret;
} public abstract class Expression extends Node {
	
	/** The universal relation:  contains all atoms in a {@link kodkod.instance.Universe universe of discourse}. */
	public static final Expression UNIV = new ConstantExpression("univ", 1);
	
	/** The identity relation: maps all atoms in a {@link kodkod.instance.Universe universe of discourse} to themselves. */
	public static final Expression IDEN = new ConstantExpression("iden", 2);
	
	/** The empty relation: contains no atoms. */
	public static final Expression NONE = new ConstantExpression("none", 1);
	
	/** The integer relation: contains all atoms {@link kodkod.instance.Bounds bound} to integers */
	public static final Expression INTS = new ConstantExpression("ints", 1);
	
    /**
     * Constructs a leaf expression
     * @ensures no this.children'
     */
    Expression() { }

    /**
     * Returns the join of this and the specified expression.  The effect
     * of this method is the same as calling this.compose(JOIN, expr).
     * @return this.compose(JOIN, expr)
     */
    public final Expression join(Expression expr) {
        return compose(JOIN,expr);
    }
    
    /**
     * Returns the product of this and the specified expression.  The effect
     * of this method is the same as calling this.compose(PRODUCT, expr).
     * @return this.compose(PRODUCT, expr)
     */
    public final Expression product(Expression expr) {
        return compose(PRODUCT,expr);
    }
    
    /**
     * Returns the union of this and the specified expression.  The effect
     * of this method is the same as calling this.compose(UNION, expr).
     * @return this.compose(UNION, expr)
     */
    public final Expression union(Expression expr) {
    	return compose(UNION,expr);
    }
    
    /**
     * Returns the difference of this and the specified expression.  The effect
     * of this method is the same as calling this.compose(DIFFERENCE, expr).
     * @return this.compose(DIFFERENCE, expr)
     */
    public final Expression difference(Expression expr) {
    	return compose(DIFFERENCE,expr);
    }
    
    /**
     * Returns the intersection of this and the specified expression.  The effect
     * of this method is the same as calling this.compose(INTERSECTION, expr).
     * @return this.compose(INTERSECTION, expr)
     */
    public final Expression intersection(Expression expr) {
    	return compose(INTERSECTION,expr);
    }
    
    /**
     * Returns the relational override of this with the specified expression.  The effect
     * of this method is the same as calling this.compose(OVERRIDE, expr).
     * @return this.compose(OVERRIDE, expr)
     */
    public final Expression override(Expression expr) {
    	return compose(OVERRIDE,expr);
    }
    
    /**
     * Returns the composition of this and the specified expression, using the
     * given binary operator.
     * @requires op in ExprOperator.BINARY
     * @return {e: Expression | e.left = this and e.right = expr and e.op = this }
     */
    public final Expression compose(ExprOperator op, Expression expr) {
    	return new BinaryExpression(this, op, expr);
    }
    
    /**
     * Returns the union of the given expressions.  The effect of this method is the
     * same as calling compose(UNION, exprs).
     * @return compose(UNION, exprs)
     */
    public static Expression union(Expression...exprs) { 
    	return compose(UNION, exprs);
    }
    
    /**
     * Returns the union of the given expressions.  The effect of this method is the
     * same as calling compose(UNION, exprs).
     * @return compose(UNION, exprs)
     */
    public static Expression union(Collection<? extends Expression> exprs) { 
    	return compose(UNION, exprs);
    }
       
    /**
     * Returns the intersection of the given expressions.  The effect of this method is the
     * same as calling compose(INTERSECTION, exprs).
     * @return compose(INTERSECTION, exprs)
     */
    public static Expression intersection(Expression...exprs) { 
    	return compose(INTERSECTION, exprs);
    }
    
    /**
     * Returns the intersection of the given expressions.  The effect of this method is the
     * same as calling compose(INTERSECTION, exprs).
     * @return compose(INTERSECTION, exprs)
     */
    public static Expression intersection(Collection<? extends Expression> exprs) { 
    	return compose(INTERSECTION, exprs);
    }
    
    /**
     * Returns the product of the given expressions.  The effect of this method is the
     * same as calling compose(PRODUCT, exprs).
     * @return compose(PRODUCT, exprs)
     */
    public static Expression product(Expression...exprs) { 
    	return compose(PRODUCT, exprs);
    }
    
    /**
     * Returns the product of the given expressions.  The effect of this method is the
     * same as calling compose(PRODUCT, exprs).
     * @return compose(PRODUCT, exprs)
     */
    public static Expression product(Collection<? extends Expression> exprs) { 
    	return compose(PRODUCT, exprs);
    }
    
    /**
     * Returns the override of the given expressions.  The effect of this method is the
     * same as calling compose(OVERRIDE, exprs).
     * @return compose(OVERRIDE, exprs)
     */
    public static Expression override(Expression...exprs) { 
    	return compose(OVERRIDE, exprs);
    }
    
    /**
     * Returns the override of the given expressions.  The effect of this method is the
     * same as calling compose(OVERRIDE, exprs).
     * @return compose(OVERRIDE, exprs)
     */
    public static Expression override(Collection<? extends Expression> exprs) { 
    	return compose(OVERRIDE, exprs);
    }
    
    /**
     * Returns the composition of the given expressions using the given operator. 
     * @requires exprs.length = 2 => op.binary(), exprs.length > 2 => op.nary()
     * @return exprs.length=1 => exprs[0] else {e: Expression | e.children = exprs and e.op = this }
     */
    public static Expression compose(ExprOperator op, Expression...exprs) { 
    	switch(exprs.length) { 
    	case 0 : 	throw new IllegalArgumentException("Expected at least one argument: " + Arrays.toString(exprs));
    	case 1 : 	return exprs[0];
    	case 2 : 	return new BinaryExpression(exprs[0], op, exprs[1]);
    	default : 	return new NaryExpression(op, Containers.copy(exprs, new Expression[exprs.length]));
    	}
    }
    
    /**
     * Returns the composition of the given expressions using the given operator. 
     * @requires exprs.size() = 2 => op.binary(), exprs.size() > 2 => op.nary()
     * @return exprs.size()=1 => exprs.iterator().next() else {e: Expression | e.children = exprs.toArray() and e.op = this }
     */
    public static Expression compose(ExprOperator op, Collection<? extends Expression> exprs) { 
    	switch(exprs.size()) { 
    	case 0 : 	throw new IllegalArgumentException("Expected at least one argument: " + exprs);
    	case 1 : 	return exprs.iterator().next();
    	case 2 :
    		final Iterator<? extends Expression> itr = exprs.iterator();
    		return new BinaryExpression(itr.next(), op, itr.next());
    	default : 			
    		return new NaryExpression(op, exprs.toArray(new Expression[exprs.size()]));
    	}
    }
    
    
    
    /**
     * Returns the transpose of this.  The effect of this method is the same
     * as calling this.apply(TRANSPOSE).
     * @return this.apply(TRANSPOSE)
     */
    public final Expression transpose() {
        return apply(TRANSPOSE);
    }
    
    /**
     * Returns the transitive closure of this.  The effect of this  method is the same
     * as calling this.apply(CLOSURE).
     * @return this.apply(CLOSURE)
     */
    public final Expression closure() {
        return apply(CLOSURE);
    }
    
    /**
     * Returns the reflexive transitive closure of this.  The effect of this 
     * method is the same
     * as calling this.apply(REFLEXIVE_CLOSURE).
     * @return this.apply(REFLEXIVE_CLOSURE)
     */
    public final Expression reflexiveClosure() {
    	return apply(REFLEXIVE_CLOSURE);
    }
    
    /**
     * Returns the expression that results from applying the given unary operator
     * to this.  
     * @requires op.unary()
     * @return {e: Expression | e.expression = this && e.op = this }
     * @throws IllegalArgumentException  this.arity != 2
     */
    public final Expression apply(ExprOperator op) {
    	return new UnaryExpression(op, this);
    }
    
    /**
     * Returns the projection of this expression onto the specified columns.
     * @return {e: Expression | e = project(this, columns) }
     * @throws IllegalArgumentException  columns.length < 1
     */
    public final Expression project(IntExpression... columns) {
    	return new ProjectExpression(this, columns);
    }
    
    /**
     * Returns the cardinality of this expression.  The effect of this method is the
     * same as calling this.apply(CARDINALITY).  
     * @return this.apply(CARDINALITY)
     */
    public final IntExpression count() {
    	return apply(CARDINALITY);
    }
    
    /**
     * Returns the sum of the integer atoms in this expression.  The effect of this method is the
     * same as calling this.apply(SUM).  
     * @return this.apply(SUM)
     */
    public final IntExpression sum() {
    	return apply(SUM);
    }
    
    /**
     * Returns the cast of this expression to an integer expression,
     * that represents either the cardinality of this expression (if op is CARDINALITY)
     * or the sum of the integer atoms it contains (if op is SUM).
     * @return {e: IntExpression | e.op = op && e.expression = this} 
     */
    public final IntExpression apply(ExprCastOperator op) { 
    	return new ExprToIntCast(this, op);
    }
    
    /**
     * Returns the formula 'this = expr'. The effect of this method is the same 
     * as calling this.compare(EQUALS, expr).
     * @return this.compare(EQUALS, expr)
     */
    public final Formula eq(Expression expr) {
    	return compare(EQUALS, expr);
    }
    
    /**
     * Returns the formula 'this in expr'.  The effect of this method is the same 
     * as calling this.compare(SUBSET, expr).
     * @return this.compare(SUBSET, expr)
     */
    public final Formula in(Expression expr) {
    	return compare(SUBSET, expr);
    }
    
    /**
     * Returns the formula that represents the comparison of this and the
     * given expression using the given comparison operator.
     * @return {f: Formula | f.left = this && f.right = expr  && f.op = op}
     */
    public final Formula compare(ExprCompOperator op, Expression expr) {
    	return new ComparisonFormula(this, op, expr);
    }
    
    /**
     * Returns the formula 'some this'.  The effect of this method is the same as calling
     * this.apply(SOME).
     * @return this.apply(SOME)
     */
    public final Formula some() {
        return apply(SOME);
    }
    
    /**
     * Returns the formula 'no this'.  The effect of this method is the same as calling
     * this.apply(NO).
     * @return this.apply(NO)
     */
    public final Formula no() {
        return apply(NO);
    }
    
    /**
     * Returns the formula 'one this'.  The effect of this method is the same as calling
     * this.apply(ONE).
     * @return this.apply(ONE)
     */
    public final Formula one() {
        return apply(ONE);
    }
    
    /**
     * Returns the formula 'lone this'.  The effect of this method is the same as calling
     * this.apply(LONE).
     * @return this.apply(LONE)
     */
    public final Formula lone() {
        return apply(LONE);
    }
    
    /**
     * Returns the formula that results from applying the specified multiplicity to
     * this expression.  The SET multiplicity is not allowed.
     * @return {f: Formula | f.multiplicity = mult && f.expression = this}
     * @throws IllegalArgumentException  mult = SET
     */
    public final Formula apply(Multiplicity mult) {
    	return new MultiplicityFormula(mult, this);
    }
    
    /**
     * Returns the arity of this expression.
     * @return this.arity
     */
    public abstract int arity();
        
    /**
     * Accepts the given visitor and returns the result.
     * @see kodkod.ast.Node#accept(kodkod.ast.visitor.ReturnVisitor)
     */
    public abstract <E, F, D, I> E accept(ReturnVisitor<E, F, D, I> visitor);
 } public abstract class IntExpression extends Node {

	/**
	 * Constructs an IntExpression.
	 */
	IntExpression() {}

	/**
	 * Returns a formula stating that the given int expression and 
	 * this have the same value.  The effect
     * of this method is the same as calling this.compare(EQ, intExpr).
	 * @return this.compare(EQ, intExpr)
	 */
	public final Formula eq(IntExpression intExpr) {
		return this.compare(EQ, intExpr);
	}
	
	/**
	 * Returns a formula stating that the value of this int expression is less than the 
	 * value of the given int expression  The effect
     * of this method is the same as calling this.compare(LT, intExpr).
	 * @return this.compare(LT, intExpr)
	 */
	public final Formula lt(IntExpression intExpr) {
		return this.compare(LT, intExpr);
	}
	
	/**
	 * Returns a formula stating that the value of this int expression is less than
	 * or equal to the  value of the given int expression  The effect
     * of this method is the same as calling this.compare(LTE, intExpr).
	 * @return this.compare(LTE, intExpr)
	 */
	public final Formula lte(IntExpression intExpr) {
		return this.compare(LTE, intExpr);
	}
	
	/**
	 * Returns a formula stating that the value of this int expression is greater than the 
	 * value of the given int expression  The effect
     * of this method is the same as calling this.compare(GT, intExpr).
	 * @return this.compare(GT, intExpr)
	 */
	public final Formula gt(IntExpression intExpr) {
		return this.compare(GT, intExpr);
	}
	
	/**
	 * Returns a formula stating that the value of this int expression is greater than
	 * or equal to the  value of the given int expression  The effect
     * of this method is the same as calling this.compare(GTE, intExpr).
	 * @return this.compare(GTE, intExpr)
	 */
	public final Formula gte(IntExpression intExpr) {
		return this.compare(GTE, intExpr);
	}
	
	/**
	 * Returns a formula comparing this and the given integer expression using the
	 * specified operator.
	 * @return {f: Formula | f.left = this and f.right = intExpr and f.op = op }
	 */
	public Formula compare(IntCompOperator op, IntExpression intExpr) {
		if (op==null || intExpr==null)
			throw new NullPointerException();
		return new IntComparisonFormula(this, op, intExpr);	
	}
	
	/**
	 * Returns an integer expression that is the sum of all
	 * values that this integer expression can take given the
	 * provided declarations.
	 * @return {e: IntExpression | e.decls = decls and e.intExpr = this }
	 */
	public final IntExpression sum(Decls decls) {
		return new SumExpression(decls, this);
	}
	
	/**
	 * Returns an IntExpression that represents the sum of this and
	 * the given int node.  The effect of this method is the same as calling
	 * this.compose(PLUS, intExpr).
	 * @return this.compose(PLUS, intExpr)
	 */
	public final IntExpression plus(IntExpression intExpr) {
		return compose(PLUS, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the difference between this and
	 * the given int node.  The effect of this method is the same as calling
	 * this.compose(MINUS, intExpr).
	 * @return this.compose(MINUS, intExpr)
	 */
	public final IntExpression minus(IntExpression intExpr) {
		return compose(MINUS, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the product of this and
	 * the given int node.  The effect of this method is the same as calling
	 * this.compose(MULTIPLY, intExpr).
	 * @return this.compose(MULTIPLY, intExpr)
	 */
	public final IntExpression multiply(IntExpression intExpr) {
		return compose(MULTIPLY, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the quotient of the division
	 * between this and the given int node.  The effect of this method is the same as calling
	 * this.compose(DIVIDE, intExpr).
	 * @return this.compose(DIVIDE, intExpr)
	 */
	public final IntExpression divide(IntExpression intExpr) {
		return compose(DIVIDE, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the remainder of the division
	 * between this and the given int node.  The effect of this method is the same as calling
	 * this.compose(MODULO, intExpr).
	 * @return this.compose(MODULO, intExpr)
	 */
	public final IntExpression modulo(IntExpression intExpr) {
		return compose(MODULO, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the bitwise AND of this and
	 * the given int node.  The effect of this method is the same as calling
	 * this.compose(AND, intExpr).
	 * @return this.compose(AND, intExpr)
	 */
	public final IntExpression and(IntExpression intExpr) {
		return compose(AND, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the bitwise OR of this and
	 * the given int node.  The effect of this method is the same as calling
	 * this.compose(OR, intExpr).
	 * @return this.compose(OR, intExpr)
	 */
	public final IntExpression or(IntExpression intExpr) {
		return compose(OR, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the bitwise XOR of this and
	 * the given int node.  The effect of this method is the same as calling
	 * this.compose(XOR, intExpr).
	 * @return this.compose(XOR, intExpr)
	 */
	public final IntExpression xor(IntExpression intExpr) {
		return compose(XOR, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the left shift of this by
	 * the given int node.  The effect of this method is the same as calling
	 * this.compose(SHL, intExpr).
	 * @return this.compose(SHL, intExpr)
	 */
	public final IntExpression shl(IntExpression intExpr) {
		return compose(SHL, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the right shift of this and
	 * the given int node, with zero extension.  The effect of this method is the same as calling
	 * this.compose(SHR, intExpr).
	 * @return this.compose(SHR, intExpr)
	 */
	public final IntExpression shr(IntExpression intExpr) {
		return compose(SHR, intExpr);
	}
	
	/**
	 * Returns an IntExpression that represents the right shift of this and
	 * the given int node, with sign extension.  The effect of this method is the same as calling
	 * this.compose(SHA, intExpr).
	 * @return this.compose(SHA, intExpr)
	 */
	public final IntExpression sha(IntExpression intExpr) {
		return compose(SHA, intExpr);
	}
	
	/**
	 * Returns an expression that combines this and the given integer expression using the
	 * specified operator.
	 * @requires op.binary()
	 * @return {e: IntExpression | e.left = this and e.right = intExpr and e.op = op }
	 */
	public final IntExpression compose(IntOperator op, IntExpression intExpr) {
		if (op==null || intExpr==null)
			throw new NullPointerException();
		return new BinaryIntExpression(this, op, intExpr);	
	}
	
	/**
     * Returns the sum of the given int expressions.  The effect of this method is the
     * same as calling compose(PLUS, intExprs).
     * @return compose(PLUS, intExprs)
     */
    public static IntExpression plus(IntExpression...intExprs) { 
    	return compose(PLUS, intExprs);
    }
    
    /**
     * Returns the plus of the given int expressions.  The effect of this method is the
     * same as calling compose(PLUS, intExprs).
     * @return compose(PLUS, intExprs)
     */
    public static IntExpression plus(Collection<? extends IntExpression> intExprs) { 
    	return compose(PLUS, intExprs);
    }
    
	/**
     * Returns the product of the given int expressions.  The effect of this method is the
     * same as calling compose(MULTIPLY, intExprs).
     * @return compose(MULTIPLY, intExprs)
     */
    public static IntExpression multiply(IntExpression...intExprs) { 
    	return compose(MULTIPLY, intExprs);
    }
    
    /**
     * Returns the product of the given int expressions.  The effect of this method is the
     * same as calling compose(MULTIPLY, intExprs).
     * @return compose(MULTIPLY, intExprs)
     */
    public static IntExpression multiply(Collection<? extends IntExpression> intExprs) { 
    	return compose(MULTIPLY, intExprs);
    }
    
	/**
     * Returns the bitwise and of the given int expressions.  The effect of this method is the
     * same as calling compose(AND, intExprs).
     * @return compose(AND, intExprs)
     */
    public static IntExpression and(IntExpression...intExprs) { 
    	return compose(AND, intExprs);
    }
    
    /**
     * Returns the bitwise and of the given int expressions.  The effect of this method is the
     * same as calling compose(AND, intExprs).
     * @return compose(AND, intExprs)
     */
    public static IntExpression and(Collection<? extends IntExpression> intExprs) { 
    	return compose(AND, intExprs);
    }
    
    /**
     * Returns the bitwise or of the given int expressions.  The effect of this method is the
     * same as calling compose(OR, intExprs).
     * @return compose(OR, intExprs)
     */
    public static IntExpression or(IntExpression...intExprs) { 
    	return compose(OR, intExprs);
    }
    
    /**
     * Returns the bitwise or of the given int expressions.  The effect of this method is the
     * same as calling compose(OR, intExprs).
     * @return compose(OR, intExprs)
     */
    public static IntExpression or(Collection<? extends IntExpression> intExprs) { 
    	return compose(OR, intExprs);
    }
  	
	/**
     * Returns the composition of the given int expressions using the given operator. 
     * @requires intExprs.length = 2 => op.binary(), intExprs.length > 2 => op.nary()
     * @return intExprs.length=1 => intExprs[0] else {e: IntExpression | e.children = intExprs and e.op = this }
     */
    public static IntExpression compose(IntOperator op, IntExpression...intExprs) { 
    	switch(intExprs.length) { 
    	case 0 : 	throw new IllegalArgumentException("Expected at least one argument: " + Arrays.toString(intExprs));
    	case 1 : 	return intExprs[0];
    	case 2 : 	return new BinaryIntExpression(intExprs[0], op, intExprs[1]);
    	default :
    		return new NaryIntExpression(op, Containers.copy(intExprs, new IntExpression[intExprs.length]));
    	}
    }
    
    /**
     * Returns the composition of the given int expressions using the given operator. 
     * @requires intExprs.length = 2 => op.binary(), intExprs.length > 2 => op.nary()
     * @return intExprs.size() = 1 => intExprs.iterator().next() else {e: IntExpression | e.children = intExprs.toArray() and e.op = this }
     */
    public static IntExpression compose(IntOperator op, Collection<? extends IntExpression> intExprs) { 
    	switch(intExprs.size()) { 
    	case 0 : 	throw new IllegalArgumentException("Expected at least one argument: " + intExprs);
    	case 1 : 	return intExprs.iterator().next();
    	case 2 :
    		final Iterator<? extends IntExpression> itr = intExprs.iterator();
    		return new BinaryIntExpression(itr.next(), op, itr.next());
    	default : 			
    		return new NaryIntExpression(op, intExprs.toArray(new IntExpression[intExprs.size()]));
    	}
    }
	
	/**
	 * Returns an IntExpression that represents the negation of this int expression.
	 * The effect of this method is the same as calling this.apply(NEG).
	 * @return this.apply(NEG)
	 */
	public final IntExpression negate() {
		return apply(NEG);
	}
	
	/**
	 * Returns an IntExpression that represents the bitwise negation of this int expression.
	 * The effect of this method is the same as calling this.apply(NOT).
	 * @return this.apply(NOT)
	 */
	public final IntExpression not() {
		return apply(NOT);
	}
	
	/**
	 * Returns an IntExpression that represents the absolute value of this int expression.
	 * The effect of this method is the same as calling this.apply(ABS).
	 * @return this.apply(ABS)
	 */
	public final IntExpression abs() {
		return apply(ABS);
	}
	
	/**
	 * Returns an IntExpression that represents the sign of this int expression.
	 * The effect of this method is the same as calling this.apply(SGN).
	 * @return this.apply(SGN)
	 */
	public final IntExpression signum() {
		return apply(SGN);
	}
	
	/**
	 * Returns an expression that represents the application of the given unary
	 * operator to this integer expression.
	 * @requires op.unary()
	 * @return {e: IntExpression | e.op = op and e.intExpr = this }
	 */
	public final IntExpression apply(IntOperator op) {
		return new UnaryIntExpression(op, this);
	}
	
	/**
	 * Returns an expression whose meaning is the singleton set containing the atom 
	 * that represents the integer given by this integer expression.
	 * The effect of this method is the same as calling this.cast(INTCAST).
	 * @return this.cast(INTCAST)
	 */
	public final Expression toExpression() {
		return cast(INTCAST);
	}
	
	/**
	 * Returns an expression whose meaning is the set containing the atoms 
	 * that represent the powers of 2 (bits) present in this integer expression.
	 * The effect of this method is the same as calling this.cast(BITSETCAST).
	 * @return this.cast(BITSETCAST)
	 */
	public final Expression toBitset() { 
		return cast(BITSETCAST);
	}
	
	/**
	 * Returns an expression that is the relational representation of this
	 * integer expression specified by the given operator.
	 * @return an expression that is the relational representation of this
	 * integer expression specified by the given operator.
	 */
	public final Expression cast(IntCastOperator op) { 
		if (op==null) throw new NullPointerException();
		return new IntToExprCast(this, op);
	}
	
	/**
	 * {@inheritDoc}
	 * @see kodkod.ast.Node#accept(kodkod.ast.visitor.ReturnVisitor)
	 */
	public abstract <E, F, D, I> I accept(ReturnVisitor<E, F, D, I> visitor) ;

	/**
	 * {@inheritDoc}
	 * @see kodkod.ast.Node#accept(kodkod.ast.visitor.VoidVisitor)
	 */
	public abstract void accept(VoidVisitor visitor);

} public abstract class AbstractReplacer implements ReturnVisitor<Expression, Formula, Decls, IntExpression> {
	protected final Map<Node,Node> cache;
	protected final Set<Node> cached;
	
	/**
	 * Constructs a depth-first replaces which will cache
	 * the results of visiting the given nodes and re-use them
	 * on subsequent visits.
	 * @ensures this.cached' = cached && no this.cache'
	 */
	protected AbstractReplacer(Set<Node> cached) { 
		this.cached = cached;
		this.cache = new IdentityHashMap<Node,Node>(cached.size());
	}
	
	/**
	 * Constructs a depth-first replacer which will cache
	 * the results of visiting the given nodes in the given map, 
	 * and re-use them on subsequent visits.
	 * @ensures this.cached' = cached && this.cache' = cache
	 */
	protected AbstractReplacer(Set<Node> cached, Map<Node,Node> cache) { 
		this.cached = cached;
		this.cache = cache;
	}

	
	/**
	 * If the given node has already been visited and its replacement
	 * cached, the cached value is returned.  Otherwise, null is returned.
	 * @return this.cache[node]
	 */
	@SuppressWarnings("unchecked")
	protected <N extends Node> N lookup(N node) {
		return (N) cache.get(node);
	}
	
	/**
	 * Caches the given replacement for the specified node, if this is 
	 * a caching visitor.  Otherwise does nothing.  The method returns
	 * the replacement node.  
	 * @ensures node in this.cached => this.cache' = this.cache ++ node->replacement,
	 *           this.cache' = this.cache
	 * @return replacement
	 */
	protected <N extends Node> N cache(N node, N replacement) {
		if (cached.contains(node)) {
			cache.put(node, replacement);
		}
		return replacement;
	}
	
	/** 
	 * Calls lookup(decls) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits each of the children's 
	 * variable and expression.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement Decls object is cached and returned.
	 * @return { d: Decls | d.size = decls.size && 
	 *                      all i: [0..d.size) | d.declarations[i] = decls.declarations[i].accept(this) } 
	 */
	public Decls visit(Decls decls) { 
		Decls ret = lookup(decls);
		if (ret!=null) return ret;
		
		Decls visitedDecls = null;
		boolean allSame = true;
		for(Decl decl : decls) {
			Decls newDecl = visit(decl);
			if (newDecl != decl) 
				allSame = false;
			visitedDecls = (visitedDecls==null) ? newDecl : visitedDecls.and(newDecl);
		}
		ret = allSame ? decls : visitedDecls;
		return cache(decls, ret);
	}
	
	/** 
	 * Calls lookup(decl) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the declaration's 
	 * variable and expression.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement Decl object is cached and returned.
	 * @return { d: Declaration |  d.variable = declaration.variable.accept(this) && 
	 *                             d.multiplicity = decl.multiplicity && 
	 *                             d.expression = declaration.expression.accept(this) 
	 */
	public Decl visit(Decl decl) {
		Decl ret = lookup(decl);
		if (ret!=null) return ret;
		
		final Variable variable = (Variable) decl.variable().accept(this);
		final Expression expression = decl.expression().accept(this);
		ret = (variable==decl.variable() && expression==decl.expression()) ?
			  decl : variable.declare(decl.multiplicity(), expression); 
		return cache(decl,ret);
	}
	
	/** 
	 * Calls lookup(relation) and returns the cached value, if any.  
	 * If a replacement has not been cached, the relation is cached and
	 * returned.
	 * @return relation 
	 */
	public Expression visit(Relation relation) { 
		final Expression ret = lookup(relation);
		return ret==null ? cache(relation,relation) : ret; 
	}
	
	/** 
	 * Calls lookup(variable) and returns the cached value, if any.  
	 * If a replacement has not been cached, the variable is cached and
	 * returned.
	 * @return variable 
	 */
	public Expression visit(Variable variable) { 
		final Expression ret = lookup(variable);
		return ret==null ? cache(variable,variable) : variable; 
	}
	
	/** 
	 * Calls lookup(constExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, the constExpr is cached and
	 * returned.
	 * @return constExpr 
	 */
	public Expression visit(ConstantExpression constExpr) {
		final Expression ret = lookup(constExpr);
		return ret==null ? cache(constExpr,constExpr) : constExpr;
	}
	
	/** 
	 * Calls lookup(expr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expr's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expr is cached and returned.
	 * @return { e: Expression | e.op = expr.op && #e.children = #expr.children && all i: [0..expr.children) | e.child(i) = expr.child(i).accept(this) }
	 */
	public Expression visit(NaryExpression expr) {
		Expression ret = lookup(expr);
		if (ret!=null) return ret;
		
		final Expression[] visited = new Expression[expr.size()];
		boolean allSame = true;
		for(int i = 0 ; i < visited.length; i++) { 
			final Expression child = expr.child(i);
			visited[i] = child.accept(this);
			allSame = allSame && visited[i]==child;
		}
		
		ret = allSame ? expr : Expression.compose(expr.op(), visited);
		return cache(expr,ret);
	}
	
	/** 
	 * Calls lookup(binExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { b: BinaryExpression | b.left = binExpr.left.accept(this) &&
	 *                                 b.right = binExpr.right.accept(this) && b.op = binExpr.op }
	 */
	public Expression visit(BinaryExpression binExpr) {
		Expression ret = lookup(binExpr);
		if (ret!=null) return ret;
		
		final Expression left  = binExpr.left().accept(this);
		final Expression right = binExpr.right().accept(this);
		ret = (left==binExpr.left() && right==binExpr.right()) ?
			  binExpr : left.compose(binExpr.op(), right);
		return cache(binExpr,ret);
	}
	
	/** 
	 * Calls lookup(unaryExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * child.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { u: UnaryExpression | u.left = unaryExpr.expression.accept(this) && u.op = unaryExpr.op }
	 */
	public Expression visit(UnaryExpression unaryExpr) {
		Expression ret = lookup(unaryExpr);
		if (ret!=null) return ret;

		final Expression child = unaryExpr.expression().accept(this);
		ret = (child==unaryExpr.expression()) ? 
			  unaryExpr : child.apply(unaryExpr.op());
		return cache(unaryExpr,ret);
	}
	
	/** 
	 * Calls lookup(comprehension) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { c: Comprehension | c.declarations = comprehension.declarations.accept(this) &&
	 *                              c.formula = comprehension.formula.accept(this) }
	 */
	public Expression visit(Comprehension comprehension) {
		Expression ret = lookup(comprehension);
		if (ret!=null) return ret;
		
		final Decls decls = (Decls)comprehension.decls().accept(this);
		final Formula formula = comprehension.formula().accept(this);
		ret = (decls==comprehension.decls() && formula==comprehension.formula()) ? 
			  comprehension : formula.comprehension(decls); 
		return cache(comprehension,ret);
	}
	
	
	/** 
	 * Calls lookup(ifExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { i: IfExpression | i.condition = ifExpr.condition.accept(this) &&
	 *                             i.thenExpr = ifExpr.thenExpr.accept(this) &&
	 *                             i.elseExpr = ifExpr.elseExpr.accept(this) }
	 */
	public Expression visit(IfExpression ifExpr) {
		Expression ret = lookup(ifExpr);
		if (ret!=null) return ret;

		final Formula condition = ifExpr.condition().accept(this);
		final Expression thenExpr = ifExpr.thenExpr().accept(this);
		final Expression elseExpr = ifExpr.elseExpr().accept(this);
		ret = (condition==ifExpr.condition() && thenExpr==ifExpr.thenExpr() &&
			   elseExpr==ifExpr.elseExpr()) ? 
		      ifExpr : condition.thenElse(thenExpr, elseExpr);
		return cache(ifExpr,ret);
	}
    
	/** 
	 * Calls lookup(decls) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits each of the children's 
	 * variable and expression.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement Decls object is cached and returned.
	 * @return { d: Decls | d.size = decls.size && 
	 *                      all i: [0..d.size) | d.declarations[i] = decls.declarations[i].accept(this) } 
	 */
	public Expression visit(ProjectExpression project) { 
		Expression ret = lookup(project);
		if (ret!=null) return ret;

		final Expression expr = project.expression().accept(this);
		final IntExpression[] cols = new IntExpression[project.arity()];
		boolean allSame = expr==project.expression();
		for(int i = 0, arity = project.arity(); i < arity; i++) {
			cols[i] = project.column(i).accept(this);
			allSame = allSame && (cols[i]==project.column(i));
		}
		ret = allSame ? project : expr.project(cols);
		return cache(project, ret);
	}
	/**
	 * Calls lookup(castExpr) and returns the cached value, if any.  If a replacement
	 * has not been cached, visits the expression's child.  If nothing changes, the argument
	 * is cached and returned, otherwise a replacement expression is cached and returned.
	 * @return { e: Expression | e = castExpr.intExpr.accept(this).toExpression() }
	 */
	public Expression visit(IntToExprCast castExpr) {
		Expression ret = lookup(castExpr);
		if (ret!=null) return ret;

		final IntExpression intExpr = castExpr.intExpr().accept(this);
		ret = (intExpr==castExpr.intExpr()) ? castExpr : intExpr.cast(castExpr.op());
		return cache(castExpr, ret);
	}
	
    /** 
	 * Calls lookup(intconst) and returns the cached value, if any.  
	 * If a replacement has not been cached, the constant is cached and returned.
	 * @return intconst
	 */
    public IntExpression visit(IntConstant intconst) {
		IntExpression ret = lookup(intconst);
		return ret==null ? cache(intconst, intconst) : intconst;
    }
    
    /** 
	 * Calls lookup(intExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { i: IfIntExpression | i.condition = intExpr.condition.accept(this) &&
	 *                             i.thenExpr = intExpr.thenExpr.accept(this) &&
	 *                             i.elseExpr = intExpr.elseExpr.accept(this) }
	 */
	public IntExpression visit(IfIntExpression intExpr) {
		IntExpression ret = lookup(intExpr);
		if (ret!=null) return ret;

		final Formula condition = intExpr.condition().accept(this);
		final IntExpression thenExpr = intExpr.thenExpr().accept(this);
		final IntExpression elseExpr = intExpr.elseExpr().accept(this);
		ret = (condition==intExpr.condition() && thenExpr==intExpr.thenExpr() &&
			   elseExpr==intExpr.elseExpr()) ? 
		      intExpr : condition.thenElse(thenExpr, elseExpr);
		return cache(intExpr,ret);
	}
    
    /** 
	 * Calls lookup(intExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * child.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { i: ExprToIntCast | i.expression = intExpr.expression.accept(this) && i.op = intExpr.op}
	 */
    public IntExpression visit(ExprToIntCast intExpr) {
		IntExpression ret = lookup(intExpr);
		if (ret!=null) return ret;
	
		final Expression expr = intExpr.expression().accept(this);
		ret = expr==intExpr.expression() ? intExpr : expr.apply(intExpr.op());
		return cache(intExpr, ret);
    }
 
    /** 
	 * Calls lookup(intExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the intExpr's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement intExpr is cached and returned.
	 * @return { e: IntExpression | e.op = intExpr.op && #e.children = #intExpr.children && all i: [0..intExpr.children) | e.child(i) = intExpr.child(i).accept(this) }
	 */
    public IntExpression visit(NaryIntExpression intExpr) {
		IntExpression ret = lookup(intExpr);
		if (ret!=null) return ret;
	
		final IntExpression[] visited = new IntExpression[intExpr.size()];
		boolean allSame = true;
		for(int i = 0 ; i < visited.length; i++) { 
			final IntExpression child = intExpr.child(i);
			visited[i] = child.accept(this);
			allSame = allSame && visited[i]==child;
		}
		
		ret = allSame ? intExpr : IntExpression.compose(intExpr.op(), visited);
		return cache(intExpr,ret);
    }
    /** 
	 * Calls lookup(intExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { c: IntExpression | [[c]] = intExpr.left.accept(this) op intExpr.right.accept(this) }
	 */
    public IntExpression visit(BinaryIntExpression intExpr) {
		IntExpression ret = lookup(intExpr);
		if (ret!=null) return ret;
	
		final IntExpression left  = intExpr.left().accept(this);
		final IntExpression right = intExpr.right().accept(this);
		ret =  (left==intExpr.left() && right==intExpr.right()) ? 
				intExpr : left.compose(intExpr.op(), right);
		return cache(intExpr,ret);
    }
    
    /** 
	 * Calls lookup(intExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * child.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { u: UnaryIntExpression | u.expression = intExpr.expression.accept(this) && u.op = intExpr.op }
	 */
	public IntExpression visit(UnaryIntExpression intExpr) {
		IntExpression ret = lookup(intExpr);
		if (ret!=null) return ret;

		final IntExpression child = intExpr.intExpr().accept(this);
		ret = (child==intExpr.intExpr()) ?  intExpr : child.apply(intExpr.op());
		return cache(intExpr,ret);
	}
	
    /** 
	 * Calls lookup(intExpr) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the expression's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement expression is cached and returned.
	 * @return { c: IntExpression | [[c]] = sum intExpr.decls.accept(this) | intExpr.intExpr.accept(this) }
	 */
    public IntExpression visit(SumExpression intExpr) {
		IntExpression ret = lookup(intExpr);
		if (ret!=null) return ret;
	
		final Decls decls  = intExpr.decls().accept(this);
		final IntExpression expr = intExpr.intExpr().accept(this);
		ret =  (decls==intExpr.decls() && expr==intExpr.intExpr()) ? 
				intExpr : expr.sum(decls);
		return cache(intExpr,ret);
    }
    
    /** 
	 * Calls lookup(intComp) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { c: Formula | [[c]] = intComp.left.accept(this) op intComp.right.accept(this) }
	 */
    public Formula visit(IntComparisonFormula intComp) {
		Formula ret = lookup(intComp);
		if (ret!=null) return ret;

		final IntExpression left  = intComp.left().accept(this);
		final IntExpression right = intComp.right().accept(this);
		ret =  (left==intComp.left() && right==intComp.right()) ? 
				intComp : left.compare(intComp.op(), right);
		return cache(intComp,ret);
    }
	
    /** 
	 * Calls lookup(constant) and returns the cached value, if any.  
	 * If a replacement has not been cached, the constant is cached and
	 * returned.
	 * @return constant 
	 */
	public Formula visit(ConstantFormula constant) {
		final Formula ret = lookup(constant);
		return ret==null ? cache(constant,constant) : constant;
	}

	/** 
	 * Calls lookup(quantFormula) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { q: QuantifiedFormula | q.declarations = quantFormula.declarations.accept(this) &&
	 *                                  q.formula = quantFormula.formula.accept(this) }
	 */
	public Formula visit(QuantifiedFormula quantFormula) {
		Formula ret = lookup(quantFormula);
		if (ret!=null) return ret;
		
		final Decls decls = (Decls)quantFormula.decls().accept(this);
		final Formula formula = quantFormula.formula().accept(this);
		ret = (decls==quantFormula.decls() && formula==quantFormula.formula()) ? 
			  quantFormula : formula.quantify(quantFormula.quantifier(), decls);
		return cache(quantFormula,ret);
	}
	
	/** 
	 * Calls lookup(formula) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { e: Expression | e.op = formula.op && #e.children = #formula.children && all i: [0..formula.children) | e.child(i) = formula.child(i).accept(this) }
	 */
	public Formula visit(NaryFormula formula) {
		Formula ret = lookup(formula);
		if (ret!=null) return ret;
		
		final Formula[] visited = new Formula[formula.size()];
		boolean allSame = true;
		for(int i = 0 ; i < visited.length; i++) { 
			final Formula child = formula.child(i);
			visited[i] = child.accept(this);
			allSame = allSame && visited[i]==child;
		}
		
		ret = allSame ? formula : Formula.compose(formula.op(), visited);
		return cache(formula,ret);
	}
	
	/** 
	 * Calls lookup(binFormula) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { b: BinaryFormula | b.left = binExpr.left.accept(this) &&
	 *                              b.right = binExpr.right.accept(this) && b.op = binExpr.op }
	 */
	public Formula visit(BinaryFormula binFormula) {
		Formula ret = lookup(binFormula);
		if (ret!=null) return ret;
		
		final Formula left  = binFormula.left().accept(this);
		final Formula right = binFormula.right().accept(this);
		ret = (left==binFormula.left() && right==binFormula.right()) ? 
			  binFormula : left.compose(binFormula.op(), right);     
		return cache(binFormula,ret);
	}
	
	/** 
	 * Calls lookup(binFormula) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * child.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { n: NotFormula | n.child = not.child.accept(this) }
	 */
	public Formula visit(NotFormula not) {
		Formula ret = lookup(not);
		if (ret!=null) return ret;

		final Formula child = not.formula().accept(this);
		ret = (child==not.formula()) ? not : child.not();
		return cache(not,ret);
	}
	
	/** 
	 * Calls lookup(compFormula) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { c: ComparisonFormula | c.left = compFormula.left.accept(this) &&
	 *                                  c.right = compFormula.right.accept(this) &&
	 *                                  c.op = compFormula.op }
	 */
	public Formula visit(ComparisonFormula compFormula) {
		Formula ret = lookup(compFormula);
		if (ret!=null) return ret;
			
		final Expression left  = compFormula.left().accept(this);
		final Expression right = compFormula.right().accept(this);
		ret =  (left==compFormula.left() && right==compFormula.right()) ? 
			   compFormula : left.compare(compFormula.op(), right);	
		return cache(compFormula,ret);
	}
	
	/** 
	 * Calls lookup(multFormula) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { m: MultiplicityFormula | m.multiplicity = multFormula.multiplicity &&
	 *                                    m.expression = multFormula.expression.accept(this) }
	 */
	public Formula visit(MultiplicityFormula multFormula) {
		Formula ret = lookup(multFormula);
		if (ret!=null) return ret;
		
		final Expression expression = multFormula.expression().accept(this);
		ret = (expression==multFormula.expression()) ? 
			  multFormula : expression.apply(multFormula.multiplicity());
		return cache(multFormula,ret);
	}
	
	/** 
	 * Calls lookup(pred) and returns the cached value, if any.  
	 * If a replacement has not been cached, visits the formula's 
	 * children.  If nothing changes, the argument is cached and
	 * returned, otherwise a replacement formula is cached and returned.
	 * @return { p: RelationPredicate | p.name = pred.name && p.relation = pred.relation.accept(this) &&
	 *                                  p.name = FUNCTION => p.targetMult = pred.targetMult && 
	 *                                                       p.domain = pred.domain.accept(this) &&
	 *                                                       p.range = pred.range.accept(this),
	 *                                  p.name = TOTAL_ORDERING => p.ordered = pred.ordered.accept(this) &&
	 *                                                             p.first = pred.first.accept(this) &&
	 *                                                             p.last = pred.last.accept(this) }
	 */
	public Formula visit(RelationPredicate pred) {
		Formula ret = lookup(pred);
		if (ret!=null) return ret;
	
		final Relation r = (Relation)pred.relation().accept(this);
		switch(pred.name()) {
		case ACYCLIC :  
			ret = (r==pred.relation()) ? pred : r.acyclic(); 
			break;
		case FUNCTION :
			final RelationPredicate.Function fp = (RelationPredicate.Function) pred;
			final Expression domain = fp.domain().accept(this);
			final Expression range = fp.range().accept(this);
			ret = (r==fp.relation() && domain==fp.domain() && range==fp.range()) ?
					fp : 
					(fp.targetMult()==Multiplicity.ONE ? r.function(domain, range) : r.partialFunction(domain,range));
			break;
		case TOTAL_ORDERING : 
			final RelationPredicate.TotalOrdering tp = (RelationPredicate.TotalOrdering) pred;
			final Relation ordered = (Relation) tp.ordered().accept(this);
			final Relation first = (Relation)tp.first().accept(this);
			final Relation last = (Relation)tp.last().accept(this);
			ret = (r==tp.relation() && ordered==tp.ordered() && first==tp.first() && last==tp.last()) ? 
					tp : r.totalOrder(ordered, first, last);
			break;
		default :
			throw new IllegalArgumentException("unknown relation predicate: " + pred.name());
		}
		return cache(pred,ret);
	}
	
} public abstract class BooleanFactory {
	/**
	 * A circuit factory used internally to assemble circuits.
	 */
	private final CBCFactory circuits;
	
	private int numVars;
	
	/** The bitwidth used for integer computations */
	final int bitwidth;
	
	/**
	 * Constructs a boolean factory with the given number of input variables.  Gates are
	 * checked for semantic equality down to the given depth.  Integers are represented
	 * using the given number of bits.
	 * @requires 0 <= numVars < Integer.MAX_VALUE
	 * @requires checkToDepth >= 0 && bitwidth > 0
	 * @ensures #this.components' = numInputVariables && this.components' in BooleanVariable 
	 * @ensures this.bitwidth' = bitwidth
	 * @ensures this.comparisonDepth' = comparisonDepth
	 */
	private BooleanFactory(int numVars, int comparisonDepth, int bitwidth) {
		this.circuits = new CBCFactory(numVars, 1<<comparisonDepth);
		this.bitwidth = bitwidth;
		this.numVars = numVars;
	}
	
	/**
	 * Returns a boolean factory, initialized to contain the given number
	 * of boolean variables.  
	 * <p>Gates are checked for semantic equality 
	 * down to the depth given by options.sharing when checking for cached values.  In general,  setting the
	 * comparison depth to a higher value will result in more 
	 * subcomponents being shared.  However, it will also slow down
	 * gate construction.  </p>
	 * <p>Integers are created/manipulated according to the specifications in the given Options object.</p>
	 * @return {f: BooleanFactory | #(f.components & BooleanVariable) = numVars &&
	 *                              BooleanConstant in f.components && f.components in BooleanVariable + BooleanConstant &&
	 *                              f.comparisonDepth = options.sharing && 
	 *                              f.bitwidth = options.bitwidth && f.intEncoding = options.intEncoding && 
	 *                              (all i: [1..numVars] | one f.components.label & i }}
	 * @throws IllegalArgumentException  numVars < 0 || numVars = Integer.MAX_VALUE
	 * @throws NullPointerException  options = null
	 */
	public static BooleanFactory factory(int numVars, Options options) {
		switch(options.intEncoding()) {
		case TWOSCOMPLEMENT : 
			return new TwosComplementFactory(numVars, options.sharing(), options.bitwidth()); 
		default :
			throw new IllegalArgumentException("unknown encoding: " + options.intEncoding());
		}
	}
	
	/**
	 * Returns a BooleanFactory with no variables; the returned factory
	 * can manipulate only constants.  
	 * @return {f: BooleanFactory | f.components = BooleanConstant &&
	 *                              f.comparisonDepth = options.sharing && 
	 *                              f.bitwidth = options.bitwidth && f.intEncoding = options.intEncoding }
	 * @throws NullPointerException  options = null
	 */
	public static BooleanFactory constantFactory(Options options) {
		return factory(0, options);
	}
	
	/**
	 * Returns the depth (from the root) to which components are checked for 
	 * semantic equality during gate construction.
	 * @return this.comparisonDepth
	 */
	public final int comparisonDepth() { return Integer.numberOfTrailingZeros(circuits.cmpMax()); }
	
	/**
	 * Sets the comparison depth to the given value.  Setting the
	 * comparison depth to a high value will result in more 
	 * subcomponents being shared.  However, it will also slow down
	 * gate construction.
	 * @ensures this.comparisonDepth' = newDepth
	 * @throws IllegalArgumentException  newDepth < 1
	 */
	public final void setComparisonDepth(int newDepth) {
		if (newDepth < 1)
			throw new IllegalArgumentException("newDepth < 1: " + newDepth);
		circuits.setCmpMax(1<<newDepth);
	}
	
	/**
	 * Returns the bitwidth used for integer representation.
	 * @return this.bitwidth
	 */
	public final int bitwidth() { return bitwidth; }
	
	/**
	 * Returns the encoding used by this factory to represent integers.
	 * @return this.intEncoding
	 */
	public abstract Options.IntEncoding intEncoding();
	
	/**
	 * Returns true if v is in this.components.
	 * @return v in this.components
	 * @throws NullPointerException  v = null
	 */
	public final boolean contains(BooleanValue v) {
		return circuits.canAssemble(v);
	}
	
	/**
	 * Returns the maximum label of a {@link BooleanVariable variable} in {@code this.components}.
	 * @return max((this.components & BooleanVariable).label)
	 */
	public final int maxVariable() { return circuits.maxVariable(); }
	
	/**
	 * Returns the maximum label of a {@link BooleanFormula formula} in {@code this.components}.
	 * Note that {@link #maxFormula()} >= {@link #maxVariable()} since variables themselves are formulas.
	 * @return max((this.components & BooleanFormula).label)
	 */
	public final int maxFormula() { return circuits.maxFormula(); }
	
	/**
	 * Returns the variable with the given label.
	 * @requires 0 < label <= numberOfVariables()
	 * @return (this.components & BooleanVariable).label
	 */
	public final BooleanVariable variable(int label) {
		return circuits.variable(label);
	}
	
	/**
	 * Adds the specified number of fresh variables to {@code this.components}.
	 * @requires numVars >= 0
	 * @ensures let diff = this.components' - this.components | 
	 *           diff in BooleanVariable && #diff = numVars && 
	 *           diff.label = { i: int | this.maxFormula() < i <= this.maxFormula() + numVars }
	 */
	public final void addVariables(int numVars) { 
		if (numVars < 0) {
			throw new IllegalArgumentException("Expected numVars >= 0, given numVars = " + numVars);
		} else if (numVars > 0) {
			circuits.addVariables(numVars);
			this.numVars += numVars;
		} // else do nothing
	}
	
	/**
	 * Returns the number of variables in this factory.
	 * @return #(this.components & BooleanVariable)
	 */
	public final int numberOfVariables() {
		return numVars;
	}
	
	/**
	 * Returns the negation of the given boolean value.
	 * @return {n: BooleanValue | n.label = -v.label && [[n]] = ![[v]] }
	 * @ensures (components.v).components' = (components.v).components + n 
	 * @throws NullPointerException  v = null                             
	 */
	public final BooleanValue not(BooleanValue v) {
		return v.negation();
	}
	
	/**
	 * Returns a boolean value whose meaning is the conjunction of the input components.  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return {v: BooleanValue | [[v]] = [[v0]] AND [[v1]] }
	 * @ensures this.components' = this.components + v 
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue and(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(AND, v0, v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is the disjunction of the input components.  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return {v: BooleanValue | [[v]] = [[v0]] OR [[v1]] }
	 * @ensures this.components' = this.components + v 
	 * @throws NullPointerException  any of the arguments are null
	 * @throws IllegalArgumentException  v0 + v1 !in this.components
	 */
	public final BooleanValue or(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(OR, v0, v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is [[v0]] ^ [[v1]].  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return { v: BooleanValue | [[v]] = [[v0]] xor [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue xor(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(v0, v1.negation(), v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is [[v0]] => [[v1]].  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return { v: BooleanValue | [[v]] = [[v0]] => [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue implies(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(OR, v0.negation(), v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is [[v0]] <=> [[v1]].
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return { v: BooleanValue | [[v]] = [[v0]] iff [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue iff(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(v0, v1, v1.negation());
	}
	
	/**
	 * Returns a boolean value whose meaning is [[i]] ? [[t]] : [[e]].
	 * The behavior of this method is unspecified if i, t, or e are not components of this factory.
	 * @requires i + t + e in this.components 
	 * @return { v: BooleanValue | [[v]] = [[i]] ? [[t]] : [[e]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue ite(BooleanValue i, BooleanValue t, BooleanValue e) {
		return circuits.assemble(i, t, e);
	}
	
	/**
	 * Returns a boolean value whose meaning is the sum bit of a full binary adder.
	 * The behavior of this method is unspecified if v0, v1, or cin are not components of this factory.
	 * @requires v0 + v1 + cin in this.components 
	 * @return { v: BooleanValue | [[v]] = [[cin]] xor [[v0]] xor [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue sum(BooleanValue v0, BooleanValue v1, BooleanValue cin) {
		return xor(cin, xor(v0, v1));
	}
	
	/**
	 * Returns a boolean value whose meaning is the carry out bit of a full binary adder.
	 * The behavior of this method is unspecified if v0, v1, or cin are not components of this factory.
	 * @requires v0 + v1 + cin in this.components 
	 * @return { v: BooleanValue | [[v]] = ([[v0]] and [[v1]]) or ([[cin]] and ([[v0]] xor [[v1]]))  }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue carry(BooleanValue v0, BooleanValue v1, BooleanValue cin) {
		return or(and(v0, v1), and(cin, xor(v0, v1)));
	}
	
	/**
	 * Converts the given accumulator into an immutable boolean value and adds it to this.components.
	 * This method requires that all of g's inputs are in this.components.  If g has no inputs,
	 * its operator's identity constant is returned.  If g has one input, that input is returned.
	 * Otherwise, an immutable value that is semantically equivalent to g is returned.
	 * The behavior of this method is unspecified if the components of g are not components of this factory.
	 * @requires g.components in this.components 
	 * @return no g.inputs => g.op.identity(), 
	 *         one g.inputs => g.inputs, 
	 *         {g' : BooleanValue - BooleanAccumulator | [[g']] = [[g]] }
	 * @ensures this.components' = this.components + g'
	 */
	public final BooleanValue accumulate(BooleanAccumulator g) {
		return circuits.assemble(g);
	}
	
	/**
	 * Returns an Int that represents the given number using this.intEncoding.
	 * @return { i: Int | [[i]] = number && i.encoding && this.intEncoding && i.factory = this}
	 * @throws IllegalArgumentException  the number cannot be represented using 
	 * the specified encoding
	 */
	public abstract Int integer(int number);
	
	/**
	 * Returns an Int that represents 0 or the given number, depending on the value of the given bit.
	 * The behavior of this method is unspecified if the bit is not a component of this factory.
	 * @return { i: Int | [[bit]] => [[i]] = number, [[i]] = 0 && i.encoding = this.intEncoding && i.factory = this}
	 */
	public abstract Int integer(int number, BooleanValue bit);
	
	/**
	 * Returns an Int that represents the sum of the elements returned by the iterator,
	 * using this.intEncoding.
	 * @param lo the first element of the current partial sum. Initial should be 0.
	 * @param hi the last element of the current partial sum.  Initial should be size-1, where size is the total
	 * number of elements returned by the iterator.
	 * @return  an Int that represents the sum of the elements returned by the iterator,
	 * using this.intEncoding.
	 */
	private Int sum(Iterator<BooleanValue> values, int low, int high) {
		if (low > high) 
			return integer(0);
		else if (low == high) 
			return integer(1, values.next());
		else {
			final int mid = (low + high) / 2;
			final Int lsum = sum(values, low, mid);
			final Int hsum = sum(values, mid+1, high);
			return lsum.plus(hsum);
		}
	}
	
	/**
	 * Returns an Int that represents the sum of all values in the given collection.
	 * @return an Int that represents the sum of all values in the given collection.
	 */
	public final Int sum(Collection<BooleanValue> bits) {
		return sum(bits.iterator(), 0, bits.size()-1);
	}
	
	/**
	 * Returns a BooleanMatrix with the given dimensions and this 
	 * as the factory for its non-FALSE components.  The returned matrix 
	 * can store any value from this.components at all
	 * indices between 0, inclusive, and d.capacity(), exclusive.  
	 * @throws NullPointerException  d = null
	 * @return { m: BooleanMatrix | m.factory = this && m.dimensions = d && m.elements = [0..d.capacity) -> one FALSE }
	 */
	public final BooleanMatrix matrix(Dimensions d) {
		if (d == null ) throw new NullPointerException();
		return new BooleanMatrix(d, this);
	}
	
	/**
	 * @throws IllegalArgumentException  indices !in [0..d.capacity())
	 */
	private static void validate(IntSet indices, Dimensions d) {
		if (!indices.isEmpty()) {
			if (!d.validate(indices.min()) ||	!d.validate(indices.max()))
				throw new IllegalArgumentException();
		}
	}
	
	/**
	 * Returns a BooleanMatrix <tt>m</tt> with the given dimensions, this
	 * as its factory, and the indices from the set <tt>trueIndices</tt> initialized
	 * to TRUE.  An IndexOutOfBoundsException may be thrown
	 * if {@link BooleanMatrix#set(int, BooleanValue)} is called on <tt>m</tt> with an index 
	 * not contained in <tt>allIndices</tt>.  If <tt>allIndices.equals(trueIndices)</tt>, 
	 * <tt>m</tt> may be a constant matrix; that is, an IllegalArgumentException may be
	 * thrown if {@link BooleanMatrix#set(int, BooleanValue)} is called on <tt>m</tt> with
	 * a non-constant value.  Finally, if cloning <tt>trueIndices</tt> results in an immutable
	 * set, then {@link BooleanMatrix#set(int, BooleanValue) m.set(int, BooleanValue)} may throw
	 * an UnsupportedOperationException when called with a member of <tt>trueIndices</tt>.
	 * @requires allIndices.containsAll(trueIndices)
	 * @return { m: BooleanMatrix |  m.factory = this && m.dimensions = dims && 
	 *           m.elements = [0..d.capacity()-1] ->one FALSE ++ indices->TRUE }
	 * @throws IllegalArgumentException  allIndices !in [0..d.capacity())
	 * @throws IllegalArgumentException  one of the input sets is not cloneable
	 * @throws NullPointerException  d = null || allIndices = null || trueIndices = null	 	 
	 */
	public final BooleanMatrix matrix(Dimensions d, IntSet allIndices, IntSet trueIndices) {
		assert allIndices.size() >= trueIndices.size(); // sanity check
		validate(allIndices, d); validate(trueIndices, d);
		try {
			return new BooleanMatrix(d, this, allIndices, trueIndices.clone());
		} catch (CloneNotSupportedException e) {
			throw new IllegalArgumentException();
		}
	
	}
		
	/**
	 * BooleanFactory that produces TwosComplementInts.
	 * @invariant encoding = TwosComplement
	 * @author Emina Torlak
	 */
	private static final class TwosComplementFactory extends BooleanFactory {

		/**
		 * Constructs a boolean factory with the given number of input variables.  Gates are
		 * checked for semantic equality down to the given depth.  Integers are represented
		 * using the given number of bits.
		 * @requires 0 <= numVars < Integer.MAX_VALUE
		 * @requires checkToDepth >= 0 && bitwidth > 0
		 * @ensures #this.components' = numInputVariables && this.components' in BooleanVariable 
		 * @ensures this.bitwidth' = bitwidth
		 * @ensures this.comparisonDepth' = comparisonDepth
		 * @ensures this.intEncoding' = BINARY
		 */
		TwosComplementFactory(int numVars, int comparisonDepth, int bitwidth) {
			super(numVars, comparisonDepth, bitwidth);
		}
		/**
		 * Returns TWOSCOMPLEMENT.
		 * @return TWOSCOMPLEMENT
		 * @see kodkod.engine.bool.BooleanFactory#intEncoding()
		 */
		@Override
		public IntEncoding intEncoding() {
			return IntEncoding.TWOSCOMPLEMENT;
		}
		
		/**
		 * {@inheritDoc}
		 * @see kodkod.engine.bool.BooleanFactory#integer(int)
		 */
		@Override
		public Int integer(int number) {
			return new TwosComplementInt(this, number, BooleanConstant.TRUE);
		}
		
		/**
		 * {@inheritDoc}
		 * @see kodkod.engine.bool.BooleanFactory#integer(int, kodkod.engine.bool.BooleanValue)
		 */
		@Override
		public Int integer(int number, BooleanValue bit) {
			return new TwosComplementInt(this, number, bit);
		}
		
	}
} public final class BooleanMatrix implements Iterable<IndexedEntry<BooleanValue>>, Cloneable {
	
	private final Dimensions dims;
	private final BooleanFactory factory;
	private final SparseSequence<BooleanValue> cells;
	

	/**  
	 * Constructs a new matrix with the given dimensions, factory, and entries.
	 * 
	 * @requires dimensions != null && factory != null && seq != null
	 * @requires seq.indices() in [0..dimensions.capacity)
	 * @ensures this.dimensions' = dimensions && this.factory' = factory && 
	 *          this.elements' = [0..dimensions.capacity)->one FALSE 
	 */
	private BooleanMatrix(Dimensions dimensions, BooleanFactory factory, SparseSequence<BooleanValue> seq) {
		this.dims = dimensions;
		this.factory = factory;
		this.cells = seq;
	}
	
	/**
	 * Constructs a new matrix with the given dimensions and factory, 
	 * backed by a sparse sequence which can most efficiently hold
	 * the elements storable in the sparse sequences s0 and s1.
	 * @ensures this.dimensions' = dimensions && this.factory' = factory && 
	 *          this.elements' = [0..dimensions.capacity)->one FALSE 
	 */
	private BooleanMatrix(Dimensions d, BooleanFactory f, SparseSequence<BooleanValue> s0, SparseSequence<BooleanValue> s1) {
		this.dims = d;
		this.factory = f;
		final Class<?> c0 = s0.getClass(), c1 = s1.getClass();
		if (c0!=c1 || c0==RangeSequence.class) 
			this.cells = new RangeSequence<BooleanValue>();
		else if (c0==HomogenousSequence.class) 
			this.cells = new HomogenousSequence<BooleanValue>(TRUE, Ints.bestSet(d.capacity())); 
		else 
			this.cells = new TreeSequence<BooleanValue>();	
	}
	
	/**
	 * Constructs a new matrix with the given dimensions and factory, 
	 * backed by a sparse sequence which can most efficiently hold
	 * the elements storable in the matrices m and rest.
	 * @requires null !in d + m + rest[int]
	 * @requires m.factory = rest[int].factory
	 * @requires d.equals(m.dims) => d.equals(rest[int].dims)
	 * @ensures this.dimensions' = dimensions && this.factory' = m.factory && 
	 *          this.elements' = [0..dimensions.capacity)->one FALSE 
	 * @throws IllegalArgumentException m.factory != rest[int].factory
	 * @throws IllegalArgumentException !(d.equals(m.dims) => d.equals(rest[int].dims))
	 */
	private BooleanMatrix(Dimensions d, BooleanMatrix m, BooleanMatrix...rest) {
		this.dims = d;
		this.factory = m.factory;
		
		final Class<?> h = HomogenousSequence.class, t = TreeSequence.class;
		final boolean sameDim = d.equals(m);
		
		Class<?> c = m.cells.getClass();
		int cId = c==h ? 1 : c==t ? 2 : 4;
		
		for(BooleanMatrix other : rest) { 
			checkFactory(factory, other.factory);
			if (sameDim) checkDimensions(d, other.dims);
			
			c = other.cells.getClass();
			cId |= c==h ? 1 : c==t ? 2 : 4;
		}
		
		switch(cId) { 
		case 1 : this.cells = new HomogenousSequence<BooleanValue>(TRUE, Ints.bestSet(d.capacity())); break;
		case 2 : this.cells = new TreeSequence<BooleanValue>(); break;
		default : this.cells = new RangeSequence<BooleanValue>(); 
		}
	}
	
	/**  
	 * Constructs a new matrix with the given dimensions and factory.
	 * The constructed matrix can store any kind of BooleanValue.
	 * 
	 * @requires dimensions != null && factory != null 
	 * @ensures this.dimensions' = dimensions && this.factory' = factory && 
	 *          this.elements' = [0..dimensions.capacity)->one FALSE 
	 */
	BooleanMatrix(Dimensions dims, BooleanFactory factory) {
		this.dims = dims;
		this.factory = factory;
		this.cells = new RangeSequence<BooleanValue>();
	}
	
	/**  
	 * Constructs a new matrix with the given dimensions and factory, 
	 * and initializes the indices in the given set to TRUE.
	 * The constructed matrix will be capable of storing only constants
	 * iff trueIndeces.equals(allIndices).  Otherwise, it will be able to store any kind of BooleanValue
	 * ONLY at the indices given by allIndices.  Any attempt to call {@link #set(int, BooleanValue) } on
	 * an index outside of allIndices may result in an IndexOutOfBoundsException.
	 * 
	 * @requires allIndices.containsAll(trueIndices)
	 * @requires trueIndices is not modifiable using an external handle
	 * @requires dimensions != null && factory != null && trueIndices != null && allIndices != null
	 * @requires dimensions.validate(allIndices.min()) && dimensions.validate(allIndices.max())
	 * @ensures this.dimensions' = dimensions && this.factory' = factory && 
	 *          this.elements' = [0..dimensions.capacity)->one FALSE ++ trueIndices -> one TRUE
	 */
	BooleanMatrix(Dimensions dims, BooleanFactory factory, IntSet allIndices, IntSet trueIndices) {
		this.dims = dims;
		this.factory = factory;
		final int tsize = trueIndices.size(), asize = allIndices.size();
		if (tsize==asize)
			this.cells = new HomogenousSequence<BooleanValue>(TRUE, trueIndices);
		else {
			this.cells = tsize==0 || asize/tsize >= 2 ? new  ArraySequence<BooleanValue>(allIndices) : new RangeSequence<BooleanValue>();
			for(IntIterator iter = trueIndices.iterator(); iter.hasNext(); ) {
				cells.put(iter.next(), TRUE);
			}
		}
	}
	
	/**
	 * Returns the dimensions of this matrix.
     * @return this.dimensions
     */
	public final Dimensions dimensions() { return dims; }
	
	/**
	 * Returns the factory used to construct all the non-constant
	 * entries in this matrix.
	 * @return this.factory
	 */
	public final BooleanFactory factory() { return factory; }
	
	/**
     * Returns the number of non-FALSE entries in this matrix.
     * @return #this.elements.(BooleanValue - FALSE)
     */
	public final int density() { return cells.size(); }
	
	/**
	 * Returns an IndexedEntry-based view of the non-FALSE entries in this matrix.  The returned
	 * iterator enumerates indexed entries that represent the non-FALSE entries in the matrix, in the ascending
	 * order of indeces.  For example, suppose that the elements of this are 0->FALSE, 1->(a & b), 2->FALSE, 3->(c | d).  Then,
	 * the Iterator will return two IndexedEntries, c1 then c2, such that c1.index=1 && c1.value = a & b and
	 * c2.index=3 && c.value = c | d.  Calling {@link Iterator#remove()} on the returned iterator has the same effect
	 * as setting the entry obtained through the last call to {@link Iterator#next()} to FALSE.
	 * @return an iterator over IndexedEntries representing the non-FALSE entries in this matrix.
	 */
	public final Iterator<IndexedEntry<BooleanValue>> iterator() {
		return cells.iterator();
	}
	
	/**
	 * Returns the set of all indices in this matrix that contain
	 * non-FALSE values.
	 * @return the set of all indices in this matrix that contain
	 * non-FALSE values.
	 */
	public final IntSet denseIndices() {
		return cells.indices();
	}
	
	/**
	 * Return FALSE if value is null; otherwise return value itself.
	 * @return FALSE if value is null; otherwise return value itself.
	 */
	private final BooleanValue maskNull(BooleanValue value) {
		return value == null ? FALSE : value;
	}
	
	/**
	 * Returns the value at the given index, without checking that the index is in bounds.
	 * @return this.elements[index]
	 */
	private final BooleanValue fastGet(final int index) {
		return maskNull(cells.get(index));
	}
	
	/**
     * Returns the element at the specified index.
     * @return this.elements[index]
     * @throws IndexOutOfBoundsException  index < 0 || index >= this.dimensions.capacity
     */
	public final BooleanValue get(final int index) {
		if (!dims.validate(index)) throw new IndexOutOfBoundsException(index + " is not a valid index.");
		return maskNull(cells.get(index));
	}
	
	
	/**
     * Returns a new matrix each of whose entries is a negation of the 
     * corresponding entry in this matrix.
     * 
     * @return { m: BooleanMatrix | m.dimensions=this.dimensions && m.factory = this.factory &&
     *                              all i: [0..m.dimensions.capacity) | m.elements[i] = !this.elements[i] }
     */
	public final BooleanMatrix not() {
		final BooleanMatrix negation = new BooleanMatrix(dims, factory, cells, cells);
		
		for (int i = 0, max = dims.capacity(); i < max; i++) {
			BooleanValue v = cells.get(i);
			if (v==null)
				negation.cells.put(i, TRUE);
			else if (v!=TRUE)
				negation.cells.put(i, v.negation());
		}
		
		return negation;
	}
	
	/**
	 * @throws IllegalArgumentException  f != this.factory
	 */
	private static final void checkFactory(BooleanFactory f0, BooleanFactory f1) {
		if (f0 != f1) throw new IllegalArgumentException("Incompatible factories: " + f0 + " and " + f1);
	}
	
	/**
	 * @throws IllegalArgumentException  !d0.equals(d1)
	 */
	private static final void checkDimensions(Dimensions d0, Dimensions d1) {
		if (!d0.equals(d1)) throw new IllegalArgumentException("Incompatible dimensions: " + d0 + " and " + d1);
	}
	
	/**
	 * 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);
		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;
	}
	
	/**
	 * Returns a new matrix such that an entry in the returned matrix represents a 
	 * conjunction of the corresponding entries in this and other matrices.  
	 * 
	 * @requires all i: [0..others.length) | others[i].dimensions = this.dimensions && others[i].factory = this.factory
	 * @return others.length = 0 => m else 
	 * 		   { m: BooleanMatrix | m.dimensions = this.dimensions && m.factory = this.factory &&
	 *            all i: [0..m.dimensions.capacity) | m.elements[i] = AND(this.elements[i], others[int].elements[i]) }
	 * @throws NullPointerException  others = null
	 * @throws IllegalArgumentException  some m: others[int] | !m.dimensions.equals(this.dimensions) || m.factory != this.factory
	 */
	public final BooleanMatrix and(final BooleanMatrix...others) {
		final BooleanMatrix ret = new BooleanMatrix(dims, this, others);
		
		for(IndexedEntry<BooleanValue> cell : cells) {
			final BooleanAccumulator acc = BooleanAccumulator.treeGate(AND, cell.value());
			for(BooleanMatrix other : others) { 
				if (acc.add(other.fastGet(cell.index()))==BooleanConstant.FALSE)
					break;
			}
			if (!acc.isShortCircuited()) { ret.fastSet(cell.index(), factory.accumulate(acc)); }
		}
		return ret;
	}
	
	/**
	 * 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);
		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;
	}
	
	/**
	 * Returns a new matrix such that an entry in the returned matrix represents a 
	 * disjunction of the corresponding entries in this and other matrices. 
	 * 
	 * @requires all i: [0..others.length) | others[i].dimensions = this.dimensions && others[i].factory = this.factory
	 * @return others.length = 0 => m else 
	 * 		   { m: BooleanMatrix | m.dimensions = this.dimensions && m.factory = this.factory &&
	 *            all i: [0..m.dimensions.capacity) | m.elements[i] = OR(this.elements[i], others[int].elements[i]) }
	 * @throws NullPointerException  others = null
	 * @throws IllegalArgumentException  some m: others[int] | !m.dimensions.equals(this.dimensions) || m.factory != this.factory
	 */
	public final BooleanMatrix or(final BooleanMatrix... others) {
		final BooleanMatrix ret = new BooleanMatrix(dims, this, others);
			
		for(IndexedEntry<BooleanValue> cell : cells) {
			final BooleanAccumulator acc = BooleanAccumulator.treeGate(OR, cell.value());
			for(BooleanMatrix other : others) { 
				if (acc.add(other.fastGet(cell.index()))==BooleanConstant.TRUE)
					break;
			}
			ret.fastSet(cell.index(), factory.accumulate(acc)); 
		}
		
		for(int i = 0, length = others.length; i < length; i++) { 
			for(IndexedEntry<BooleanValue> cell : others[i].cells) {
				if (ret.cells.containsIndex(cell.index())) continue;
				final BooleanAccumulator acc = BooleanAccumulator.treeGate(OR, cell.value());
				for(int j = i+1; j < length; j++) { 
					if (acc.add(others[j].fastGet(cell.index()))==BooleanConstant.TRUE)
						break;
				}
				ret.fastSet(cell.index(), factory.accumulate(acc)); 
			}
		}
		
		return ret;
	}
	
	/**
     * 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);
		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;
	}
	
	/**
	 * Updates the itrs and idxs arrays for the next step of the cross-product computation and returns a partial
	 * index based on the updated idxs values.
	 * @requires matrices.length = itrs.length = idxs.length
	 * @requires all m: matrices[int] | m.density() > 0
	 * @requires currentIdx is a partial index based on the current value of idxs
	 * @ensures  updates the itrs and idxs arrays for the next step cross-product computation
	 * @return a partial index based on the freshly updated idxs values.
	 */
	private static int nextCross(final BooleanMatrix[] matrices, final IntIterator[] itrs, final int[] idxs, int currentIdx) { 
	
		int mult = 1;
		for(int i = itrs.length-1; i >= 0; i--) {
			if (itrs[i].hasNext()) { 
				final int old = idxs[i];
				idxs[i] = itrs[i].next();
				return currentIdx - mult*old + mult*idxs[i];
			} else {
				itrs[i] = matrices[i].cells.indices().iterator();
				final int old = idxs[i];
				idxs[i] = itrs[i].next();
				currentIdx = currentIdx - mult*old + mult*idxs[i];
				mult *= matrices[i].dims.capacity();
			}
		}
		
		return -1;
	}
	
	/**
	 * Initializes the itrs and idxs arrays for cross-product computation and returns a partial
	 * index based on the freshly computed idxs values.
	 * @requires matrices.length = itrs.length = idxs.length
	 * @requires all m: matrices[int] | m.density() > 0
	 * @ensures  initializes the itrs and idxs arrays for cross-product computation
	 * @return a partial index based on the freshly computed idxs values.
	 */
	private static int initCross(final BooleanMatrix[] matrices, final IntIterator[] itrs, final int[] idxs) { 
		int mult = 1, idx = 0;
		for(int i = matrices.length-1; i >= 0; i--) { 
			itrs[i] = matrices[i].cells.indices().iterator();
			idxs[i] = itrs[i].next();
			idx += mult*idxs[i];
			mult *= matrices[i].dims.capacity();
		}
		return idx;
	}
	
	/**
     * Returns the cross product of this and other matrices, using conjunction instead of 
     * multiplication.
     * @requires this.factory = others[int].factory
     * @return others.length=0 => { m: BooleanMatrix | m.dimensions = this.dimensions && no m.elements } else
     *           { m: BooleanMatrix | m = this x others[0] x ... x others[others.length-1] }
     * @throws NullPointerException  others = null
     * @throws IllegalArgumentException  this.factory != others[int].factory
     */
	public final BooleanMatrix cross(final BooleanMatrix...others) {
		Dimensions retDims = dims;
		boolean empty = cells.isEmpty();
		for(BooleanMatrix other : others) { 
			retDims = retDims.cross(other.dims);
			empty = empty || other.cells.isEmpty();
		}
		
		final BooleanMatrix ret = new BooleanMatrix(retDims, this, others);
		if (empty) return ret;
		
		final IntIterator[] itrs = new IntIterator[others.length];
		final int[] otherIdxs = new int[others.length];
		
		final int ocap = retDims.capacity() / dims.capacity();
		
		for(IndexedEntry<BooleanValue> cell : cells) {
			final int idx = ocap * cell.index();
			for(int restIdx = initCross(others, itrs, otherIdxs); restIdx >= 0; restIdx = nextCross(others, itrs, otherIdxs, restIdx)) { 
				final BooleanAccumulator acc = BooleanAccumulator.treeGate(AND, cell.value());
				for(int i = others.length-1; i >= 0; i--) {
					if (acc.add(others[i].fastGet(otherIdxs[i]))==BooleanConstant.FALSE) 
						break;
				}
				if (!acc.isShortCircuited()) {	ret.fastSet(idx + restIdx, factory.accumulate(acc)); }
			}
			
		}
		
		return ret;
	}
	
	/**
     * Sets the value at the specified index to the given value;
     * returns the value previously at the specified position.  
     * It performs no index or null checking.
     * 
     * @ensures this.elements'[index] = formula
     */
	private final void fastSet(final int index, final BooleanValue formula) {
		if (formula==FALSE) cells.remove(index);
		else cells.put(index,formula);
	}
	
	/**
     * Returns the dot product of this and other matrix, using conjunction instead of 
     * multiplication and disjunction instead of addition.
     * 
     * @return { m: BooleanMatrix | m = this*other }
     * @throws NullPointerException  other = null
     * @throws IllegalArgumentException  this.factory != other.factory
     * @throws IllegalArgumentException  dimensions incompatible for multiplication
     */
	public final BooleanMatrix dot(final BooleanMatrix other) {  
		checkFactory(this.factory, other.factory);
		
		final BooleanMatrix ret =  new BooleanMatrix(dims.dot(other.dims), factory, cells, other.cells);
		if (cells.isEmpty() || other.cells.isEmpty()) return ret;
		
		final SparseSequence<BooleanValue> mutableCells = ret.clone().cells;
		final int b = other.dims.dimension(0); 
		final int c = other.dims.capacity() / b; 
		
		for(IndexedEntry<BooleanValue> e0 : cells) {
			int i = e0.index();
			BooleanValue iVal = e0.value();
			int rowHead = (i % b)*c, rowTail = rowHead + c - 1;
			for(Iterator<IndexedEntry<BooleanValue>> iter1 = other.cells.iterator(rowHead, rowTail); iter1.hasNext();) {
				IndexedEntry<BooleanValue> e1 = iter1.next();
				BooleanValue retVal = factory.and(iVal, e1.value());
				if (retVal != FALSE) {
					int k = (i / b)*c + e1.index()%c;
					if (retVal==TRUE) mutableCells.put(k, TRUE);
					else {
						BooleanValue kVal = mutableCells.get(k);
						if (kVal != TRUE) {
							if (kVal==null) {
								kVal = BooleanAccumulator.treeGate(OR);
								mutableCells.put(k, kVal);
							} 
							((BooleanAccumulator) kVal).add(retVal);
						}
					}
				}
			}		
		}
		
		// make mutable gates immutable
		for(IndexedEntry<BooleanValue> e : mutableCells) {
			if (e.value()!=TRUE) {
				ret.fastSet(e.index(), factory.accumulate((BooleanAccumulator) e.value()));
			} else {
				ret.fastSet(e.index(), TRUE);
			}
		}
		return ret;
	}
	
	/**
	 * Returns a formula stating that the entries in this matrix are a subset of 
	 * the entries in the given matrix; i.e. the value of every entry in this matrix
	 * implies the value of the corresponding entry in the given matrix.
	 * @return { f: BooleanValue | f <=> (this.elements[0]=>other.elements[0]) AND ... 
	 *            AND (this.elements[this.dimensions.capacity-1]=>other.elements[this.dimensions.capacity-1]))
	 * @throws NullPointerException   other = null 
	 * @throws IllegalArgumentException  !other.dimensions.equals(this.dimensions) || this.factory != other.factory           
	 */
	public final BooleanValue subset(BooleanMatrix other) {
		checkFactory(this.factory, other.factory); checkDimensions(this.dims, other.dims);
		final BooleanAccumulator a = BooleanAccumulator.treeGate(AND);
		for(IndexedEntry<BooleanValue> e0: cells) {
			if (a.add(factory.or(e0.value().negation(), other.fastGet(e0.index())))==FALSE)
				return FALSE;
		}
		return factory.accumulate(a);
	}
	
	/**
	 * Returns a formula stating that the entries in this matrix are equivalent to 
	 * the entries in the given matrix; i.e. the value of every entry in this matrix
	 * is true if and only if the value of the corresponding entry in the given matrix is true.
	 * The same formula can be obtained by calling factory.and(this.subset(other), other.subset(this)),
	 * but this method performs the operation more efficiently.
	 * @return { f: BooleanValue | f <=> (this.elements[0]<=>other.elements[0]) AND ... 
	 *            AND (this.elements[this.dimensions.capacity-1]<=>other.elements[this.dimensions.capacity-1]))
	 * @throws NullPointerException   other = null 
	 * @throws IllegalArgumentException  !other.dimensions.equals(this.dimensions) || this.factory != other.factory           
	 */
	public final BooleanValue eq(BooleanMatrix other) {
		return factory.and(this.subset(other), other.subset(this));
	}
	
	/**
	 * Returns a matrix representing the asymmetric difference between
	 * the entries in this and the given matrix.  The same matrix can 
	 * be obtained by calling this.and(other.not()), but this method
	 * performs the operation more efficiently (intermediate
	 * values are not explicitly created).
	 * @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 difference(BooleanMatrix other) {
		checkFactory(this.factory, other.factory); 
		checkDimensions(this.dims, other.dims);
		if (this.cells.isEmpty() || other.cells.isEmpty()) return this.clone();
		final BooleanMatrix ret = new BooleanMatrix(dims, factory, cells, other.cells);
		for(IndexedEntry<BooleanValue> e0 : cells) {
			ret.fastSet(e0.index(), factory.and(e0.value(), other.fastGet(e0.index()).negation()));
		}
		return ret;
	}
	
	/**
     * 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;
	}
	
	/**
     * Returns the transpose of this matrix.
     * 
     * @return { m: BooleanMatrix | m = ~this }
     * @throws UnsupportedOperationException  #this.dimensions != 2
     */
	public final BooleanMatrix transpose() {
		final BooleanMatrix ret = new BooleanMatrix(dims.transpose(), factory, cells, cells);
		final int rows = dims.dimension(0), cols = dims.dimension(1);
		for (IndexedEntry<BooleanValue> e0 : cells) {
			ret.cells.put((e0.index()%cols)*rows + (e0.index()/cols), e0.value());
		}
		return ret;
	}
		
	/**
	 * 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()));
		}
		return ret;
	}
		
	/**
	 * Returns a matrix m such that the relational value of m is equal to the
	 * relational value of this projected on the specified columns. 
	 * @requires column[int] in this.dimensions.dimensions[int]
	 * @requires this.dimensions.isSquare()
	 * @return { m: BooleanMatrix | [[m]] = project([[this]], columns) }
	 * @throws IllegalArgumentExceptions  columns.length < 1 || !this.dimensions.isSquare()
	 * @throws NullPointerException  columns = null
	 */
	public final BooleanMatrix project(Int[] columns) {
		if (!dims.isSquare())
			throw new IllegalArgumentException("!this.dimensions.isSquare()");
		
		final int rdnum = columns.length;
		
		if (rdnum < 1)
			throw new IllegalArgumentException("columns.length < 1");
		
		final Dimensions rdims = Dimensions.square(dims.dimension(0), rdnum);
		final BooleanMatrix ret = new BooleanMatrix(rdims, factory, cells, cells);
		
		final int tdnum = dims.numDimensions();
		final int[] tvector = new int[tdnum];
		final int[] ivector = new int[rdnum];
		final int[] rvector = new int[rdnum];
		
		int nVarCols = 1;
		
		// detect constant columns to avoid unnecessary looping;
		for(int i = 0; i < rdnum; i++) {
			if (columns[i].isConstant()) {
				int value = columns[i].value();
				if (value < 0 || value >= tdnum) {
					return ret;
				} else { // distinguish constants by making them negative
					ivector[i] = -value;
				}
			} else {
				nVarCols *= tdnum;
			}
		}
		
		PROJECT : for(int i = 0; i < nVarCols; i++) {
			BooleanValue colVal = TRUE;
			for(int j = 0; j < rdnum; j++) {
				// if the jth column is non-constant, check that it can take on the value ivector[j]
				if (ivector[j] >= 0) { 
					colVal = factory.and(colVal, columns[j].eq(factory.integer(ivector[j])));
					if (colVal==FALSE)
						continue PROJECT;
				}
			}
			for(IndexedEntry<BooleanValue> e : cells) {
				dims.convert(e.index(), tvector);
				for(int j = 0; j < rdnum; j++) {
					rvector[j] = tvector[StrictMath.abs(ivector[j])];
				}
				int rindex = rdims.convert(rvector);
				ret.fastSet(rindex, factory.or(factory.and(e.value(), colVal), ret.fastGet(rindex)));
			}
			for(int j = rdnum-1; j >= 0; j--) { // update ivector
				// update ivector[j] only if the jth column is not constant
				if (ivector[j]>=0) {
					if (ivector[j]+1==tdnum) {
						ivector[j] = 0;
					} else {
						ivector[j] += 1;
						break;
					}
				}
			}
		}
		
		return ret;
	}
	
	/**
	 * Returns a conjunction of the negated values between 
	 * start, inclusive, and end, exclusive.
	 * @requires 0 <= start < end <= this.dimensions.capacity() 
	 * @return !this.elements[start] && !this.elements[start+1] && ... && !this.elements[end-1]
	 */
	private final BooleanValue nand(int start, int end) {
		final BooleanAccumulator g = BooleanAccumulator.treeGate(AND);
		for(Iterator<IndexedEntry<BooleanValue>> iter = cells.iterator(start, end-1); iter.hasNext(); ) {
			if (g.add(iter.next().value().negation())==FALSE) 
				return FALSE;
		}
		return factory.accumulate(g);
	}
	
	/**
	 * 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.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;
	}
	
	/**
	 * Overrides the values in this matrix with those in <code>other</code>.
	 * @return others.length = 0 => { m: BooleanMatrix | m.dimensions = this.dimensions && m.elements = this.elements) else
	 * 		   others.length = 1 => {m: BooleanMatrix | m.dimensions = this.dimensions &&
	 *                               all i: [0..m.capacity()) | m.elements[i] = 
	 *                                other.elements[i] || this.elements[i] && !OR(other.elements[rowOf(i)]) } else
	 *                              this.override(others[0).override(others[1..others.length))
	 * @throws NullPointerException  others = null
	 * @throws IllegalArgumentException  others[int].factory != this.factory or others[int].dimensions != this.dimensions
	 */
	public final BooleanMatrix override(BooleanMatrix... others) {
		if (others.length==0) return clone();
		final BooleanMatrix[] matrices = Containers.copy(others, 0, new BooleanMatrix[others.length+1], 1, others.length);
		matrices[0] = this;
		for(int part = matrices.length; part > 1; part -= part/2) { 
			final int max = part-1;
			for(int i = 0; i < max; i += 2) { 
				matrices[i/2] = matrices[i].override(matrices[i+1]);
			}
			if (max%2==0) { // even max => odd number of entries
				matrices[max/2] = matrices[max];
			}
		}
		return matrices[0];
	}
	
	/**
	 * Returns an Int that represents the cardinality (number of non-FALSE entries) of this
	 * matrix using this.factory.intEncoding.
	 * @return {i: Int | [[i]] = sum({v: elements[int] | if [[v]] then 1 else 0}) }  
	 */
	public final Int cardinality() {
		return factory.sum(cells.values());
	}
	
	/**
	 * Returns a BooleanValue that constrains at least one value in this.elements to be true.  The
	 * effect of this method is the same as calling this.orFold().
	 * @return { f: BooleanValue | f <=> this.elements[0] || ... || this.elements[this.dimensions.capacity-1] }
	 */
	public final BooleanValue some() {
		final BooleanAccumulator g = BooleanAccumulator.treeGate(OR);
		for(IndexedEntry<BooleanValue> e : cells) {
			if (g.add(e.value())==TRUE) 
				return TRUE;
		}
		return factory.accumulate(g);
	}
	
	/**
	 * 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() {
		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());
			}

			return factory.accumulate(g);
		}
	}
	
	/**
	 * 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() {
		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);
			return factory.accumulate(g);
		}
	}
	
	/**
	 * Returns a BooleanValue that constraints all values in this.elements to be false.
	 * The effect of this method is the same as calling this.factory.not(this.some()).
	 * @return { f: BooleanValue | f <=> !(this.elements[0] || ... || !this.elements[this.dimensions.capacity-1]) }
	 */
	public final BooleanValue none() {
		return some().negation();
	}
	
	/**
     * Sets the specified index to the given value.
     * 
     * @requires value in this.factory.components
     * @ensures this.elements'[index] = value
     * @throws NullPointerException  value = null
     * @throws IllegalArgumentException  the given is a formula, and this matrix accepts only constants
     * @throws IndexOutOfBoundsException  the given index does not belong to the set of indices at which
     * this matrix can store non-FALSE values.
     */
	public final void set(final int index, final BooleanValue value) {
		if (!dims.validate(index)) throw new IndexOutOfBoundsException("index < 0 || index >= this.dimensions.capacity");
		if (value==null) throw new NullPointerException("formula=null");
		if (value==FALSE) 
			cells.remove(index);
		else 
			cells.put(index,value);
	}
	
	/**
	 * Returns a copy of this boolean matrix.
	 * @return {m: BooleanMatrix - this | m.dimensions = this.dimensions &&
	 *                                    m.elements = copy of this.elements } 
	 */
	public BooleanMatrix clone()  {
		try {
			return new BooleanMatrix(dims, factory, cells.clone());
		} catch (CloneNotSupportedException e) {
			throw new InternalError(); // unreachable code.
		}
	}
	
	/**
	 * @see java.lang.Object#toString()
	 */
	public String toString() {
		final StringBuilder buff = new StringBuilder("dimensions: ");
		buff.append(dims);
		buff.append(", elements: ");
		buff.append(cells);
		return buff.toString();
	}	
} public abstract class Int {
	final BooleanFactory factory;
	
	/**
	 * Creates an Int with the given factory
	 * @ensures this.factory' = factory
	 */
	Int(BooleanFactory factory) {
		this.factory = factory;
	}
	
	/**
	 * Throws IllegalArgumentException if other.factory != this.factory.
	 * @throws IllegalArgumentException  other.factory != this.factory.
	 */
	final void validate(Int other) {
		if (other.factory != factory)
			throw new IllegalArgumentException("other.factory != this.factory");
	}
	
	/**
	 * Returns the BooleanValue at the specified index.
	 * @requires 0 <= i < this.factory.bitwidth
	 * @return this.bits[i]
	 */
	abstract BooleanValue bit(long i);
	
	/**
	 * Returns the little endian two's complement representation of this integer that is 
	 * this.factory.bitwidth bits wide.  Specifically, the returned list L has 
	 * this.factory.bitwidth boolean values such that the meaning of this integer is 
	 * 1*[[L.get(0)]] + ... + (1<<i)*[[L.get(i)]] + ... + (-1<<(L.size()-1))*[[L.get(L.size()-1)]].
	 * @return a list containing the little endian two's complement representation of this integer.
	 * @throws UnsupportedOperationException  this integer encoding cannot be converted to two's complement.
	 */
	public abstract List<BooleanValue> twosComplementBits();
		
	/**
	 * Returns this.factory
	 * @return this.factory
	 */
	public final BooleanFactory factory() { return factory; }
	
	/**
	 * Returns the number of bits in the representation of this Int,
	 * including sign bits (if any).
	 * @return this.width
	 */
	public abstract int width(); 
	
	/**
	 * Returns true if all the bits representing this Int
	 * are BooleanConstants.
	 * @return this.bits[int] in BooleanConstant
	 */
	public abstract boolean isConstant();
	
	/**
	 * If this Int is constant, returns its value.  Otherwise
	 * throws an IllegalStateException.
	 * @return this.isConstant() => [[this.bits]]
	 * @throws IllegalStateException  !this.isConstant()
	 */
	public abstract int value();
	
	/**
	 * Returns a BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is equal to the integer represented by the specified Int.
	 * @requires this.factory = other.factory
	 * @return BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is equal to the integer represented by the specified Int
	 * @throws IllegalArgumentException  this.factory != other.factory 
	 */
	public abstract BooleanValue eq(Int other);
	
	/**
	 * Returns a BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is less than or equal to the integer
	 * represented by the specified Int
	 * @requires this.factory = other.factory 
	 * @return BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is less than or equal to the integer
	 * represented by the specified Int
	 * @throws IllegalArgumentException  this.factory != other.factory 
	 */
	public abstract BooleanValue lte(Int other);
	
	/**
	 * Returns a BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is less than the integer
	 * represented by the specified Int.
	 * @requires this.factory = other.factory
	 * @return BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is less than the integer
	 * represented by the specified Int
	 * @throws IllegalArgumentException  this.factory != other.factory 
	 */
	public abstract BooleanValue lt(Int other);
	
	/**
	 * Returns a BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is greater than or equal to the integer
	 * represented by the specified Int.
	 * @requires this.factory = other.factory 
	 * @return BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is greater than or equal to the integer
	 * represented by the specified Int
	 * @throws IllegalArgumentException  this.factory != other.factory 
	 */
	public BooleanValue gte(Int other) {
		return other.lte(this);
	}
	
	/**
	 * Returns a BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is greater than the integer
	 * represented by the specified Int.
	 * @requires this.factory = other.factory 
	 * @return BooleanValue encoding the comparator circuit
	 * that checks whether the integer represented by this
	 * Int is greater than the integer
	 * represented by the specified Int
	 * @throws IllegalArgumentException  this.factory != other.factory
	 */
	public BooleanValue gt(Int other) {
		return other.lt(this);
	}
	
	/**
	 * Returns an Int that represents the sum of this and the given Int.
	 * @requires this.factory = other.factory 
	 * @return an Int that represents the sum of this and the given Int
	 * @throws IllegalArgumentException  this.factory != other.factory
	 */
	public abstract Int plus(Int other);
	
	/**
	 * Returns an Int that represents the sum of this and the given Ints.
	 * @requires this.factory = others[int].factory 
	 * @return an Int that represents the sum of this and the given Ints
	 * @throws IllegalArgumentException  this.factory != others[int].factory
	 */
	public abstract Int plus(Int... others);
	
	/**
	 * Returns an Int that represents the product between this and the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents the product between this and the given Int
	 * @throws UnsupportedOperationException  this.encoding does not support multiplication
	 */
	public abstract Int multiply(Int other);
	
	/**
	 * Returns an Int that represents the product between this and the given Ints.
	 * @requires this.factory = others[int].factory
	 * @return an Int that represents the product between this and the given Ints
	 * @throws UnsupportedOperationException  this.encoding does not support multiplication
	 */
	public abstract Int multiply(Int... others);
	
	/**
	 * Returns an Int that represents the difference between this and the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents the difference between this and the given Int
	 * @throws UnsupportedOperationException  this.encoding does not support subtraction
	 */
	public abstract Int minus(Int other);
	
	/**
	 * Returns an Int that represents the quotient of the division between this and the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents the quotient of the division between this and the given Int
	 * @throws UnsupportedOperationException  this.encoding does not support division
	 */
	public abstract Int divide(Int other);
	
	/**
	 * Returns an Int that represents the remainder of the division between this and the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents the remainder of the division between this and the given Int
	 * @throws UnsupportedOperationException  this.encoding does not support division
	 */
	public abstract Int modulo(Int other);
	
	/**
	 * Returns an Int that evaluates to this if the condition is true, otherwise it
	 * evaluates to the given Int.
	 * @requires other + condition in this.factory.components
	 * @return an Int that evaluates to this if the condition is true, and
	 * to the given Int if the condition is false.
	 */
	public abstract Int choice(BooleanValue condition, Int other);
	
	/**
	 * Returns an Int that represents the bitwise conjunction of this and the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents the bitwise conjunction of this and the given Int.
	 */
	public abstract Int and(Int other);
	
	/**
	 * Returns an Int that represents the bitwise conjunction of this and the given Ints.
	 * @requires this.factory = others[int].factory
	 * @return an Int that represents the bitwise conjunction of this and the given Ints.
	 */
	public abstract Int and(Int... others);
	
	/**
	 * Returns an Int that represents the bitwise disjunction of this and the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents the bitwise disjunction of this and the given Int.
	 */
	public abstract Int or(Int other);
	
	/**
	 * Returns an Int that represents the bitwise disjunction of this and the given Ints.
	 * @requires this.factory = others[int].factory
	 * @return an Int that represents the bitwise disjunction of this and the given Ints.
	 */
	public abstract Int or(Int... others);
	
	/**
	 * Returns an Int that represents the bitwise XOR of this and the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents the bitwise XOR of this and the given Int.
	 * @throws UnsupportedOperationException  this.encoding does not support XOR
	 */
	public abstract Int xor(Int other);
	
	/**
	 * Returns an Int that represents this shifted to the left by the given Int.
	 * @requires this.factory = other.factory
	 * @return an Int that represents this shifted to the left by the given Int.
	 * @throws UnsupportedOperationException  this.encoding does not support SHL
	 */
	public abstract Int shl(Int other);
	
	/**
	 * Returns an Int that represents this shifted to the right by the given Int, 
	 * with zero extension.
	 * @requires this.factory = other.factory
	 * @return an Int that represents this shifted to the right by the given Int, 
	 * with zero extension.
	 * @throws UnsupportedOperationException  this.encoding does not support SHR
	 */
	public abstract Int shr(Int other);
	
	/**
	 * Returns an Int that represents this shifted to the right by the given Int, 
	 * with sign extension.
	 * @requires this.factory = other.factory
	 * @return an Int that represents this shifted to the right by the given Int, 
	 * with sign extension.
	 * @throws UnsupportedOperationException  this.encoding does not support SHA
	 */
	public abstract Int sha(Int other);
	
	/**
	 * Returns an Int that represents the negation of this integer.
	 * @return -[[this]]
	 * @throws UnsupportedOperationException  this.encoding does not support negation
	 */
	public abstract Int negate();
	
	/**
	 * Returns an Int that represents bitwise negation of this integer.
	 * @return ~[[this]]
	 * @throws UnsupportedOperationException  this.encoding does not support bitwise negation
	 */
	public abstract Int not();
	
	/**
	 * Returns an Int that represents the absolute value of this integer.
	 * @return abs([[this]])
	 */
	public abstract Int abs();
	
	/**
	 * Returns an Int that represents the signum of this integer.
	 * @return sgn([[this]])
	 */
	public abstract Int sgn();
	
	
} public final class Bounds implements Cloneable {
	private final TupleFactory factory;
	private final Map<Relation, TupleSet> lowers, uppers;
	private final SparseSequence<TupleSet> intbounds;
	private final Set<Relation> relations;
	
	/**
	 * Constructs a Bounds object with the given factory and mappings.
	 */
	private Bounds(TupleFactory factory, Map<Relation, TupleSet> lower, Map<Relation, TupleSet> upper, SparseSequence<TupleSet> intbounds) {
		this.factory = factory;
		this.lowers = lower;
		this.uppers = upper;
		this.intbounds = intbounds;
		this.relations = relations(lowers, uppers);
	}
	
	/**
	 * Constructs new Bounds over the given universe.
	 * @ensures this.universe' = universe && no this.relations' && no this.intBound'
	 * @throws NullPointerException  universe = null
	 */
	public Bounds(Universe universe) {
		this.factory = universe.factory();
		this.lowers = new LinkedHashMap<Relation, TupleSet>();
		this.uppers = new LinkedHashMap<Relation, TupleSet>();
		this.intbounds = new TreeSequence<TupleSet>();
		this.relations = relations(lowers, uppers);
	}
	
	/**
	 * Returns a set view of the relations mapped by the given lower/upper bounds.
	 * @requires lowers.keySet().equals(uppers.keySet())
	 * @return a set view of the relations mapped by the given lower/upper bounds
	 */
	private static Set<Relation> relations(final Map<Relation, TupleSet> lowers, final Map<Relation, TupleSet> uppers) {
		return new AbstractSet<Relation>() {

			public Iterator<Relation> iterator() {
				return new Iterator<Relation>() {
					final Iterator<Relation> itr = uppers.keySet().iterator();
					Relation last = null;
					public boolean hasNext() { return itr.hasNext(); }
					public Relation next() { return last = itr.next(); }
					public void remove() {
						itr.remove();
						lowers.remove(last);					
					}
				};
			}

			public int size() { return uppers.size(); }			
			public boolean contains(Object key) { return uppers.containsKey(key); }
			
			public boolean remove(Object key) { 
				return (uppers.remove(key) != null) && (lowers.remove(key) != null); 
			}
			public boolean removeAll(Collection<?> c) {
				return uppers.keySet().removeAll(c) && lowers.keySet().removeAll(c);
			}
			public boolean retainAll(Collection<?> c) {
				return uppers.keySet().retainAll(c) && lowers.keySet().retainAll(c);
			}
		};
	}
	
	/**
	 * Returns this.universe.
	 * @return this.universe
	 */
	public Universe universe() { return factory.universe(); }

	/**
	 * Returns the set of all relations bound by this Bounds.
	 * The returned set does not support the add operation.
	 * It supports removal iff this is not an unmodifiable Bounds.
	 * @return this.relations
	 */
	public Set<Relation> relations() { 
		return relations; 
	}
	
	/**
	 * Returns the set of all integers bound by this Bounds.
	 * The returned set does not support the add operation.
	 * It supports removal iff this is not an unmodifiable Bounds.
	 * @return this.intBounds.TupleSet
	 */
	public IntSet ints() {
		return intbounds.indices();
	}
	
	/**
	 * Returns the set of tuples that r must contain (the lower bound on r's contents).
	 * If r is not mapped by this, null is returned.
	 * @return r in this.relations => lowerBound[r], null
	 */
	public TupleSet lowerBound(Relation r) {
		return lowers.get(r);
	}
	
	/**
	 * Returns a map view of this.lowerBound.  The returned map is not modifiable.
	 * @return a map view of this.lowerBound
	 */
	public Map<Relation, TupleSet> lowerBounds() {
		return unmodifiableMap(lowers);
	}
	
	/**
	 * Returns the set of tuples that r may contain (the upper bound on r's contents).
	 * If r is not mapped by this, null is returned.
	 * @return r in this.relations => upperBound[r], null
	 */
	public TupleSet upperBound(Relation r) {
		return uppers.get(r);
	}
	
	/**
	 * Returns a map view of this.upperBound.  The returned map is not modifiable.
	 * @return a map view of this.upperBound
	 */
	public Map<Relation, TupleSet> upperBounds() {
		return unmodifiableMap(uppers);
	}
	
	/**
	 * Returns the set of tuples representing the given integer.  If i is not
	 * mapped by this, null is returned.
	 * @return this.intBound[i]
	 */
	public TupleSet exactBound(int i) {
		return intbounds.get(i);
	}
	
	/**
	 * Returns a sparse sequence view of this.intBound.  The returned sequence
	 * is not modifiable.
	 * @return a sparse sequence view of this.intBound
	 */
	public SparseSequence<TupleSet> intBounds() {
		return unmodifiableSequence(intbounds);
	}
	
	/**
	 * @throws IllegalArgumentException  arity != bound.arity
	 * @throws IllegalArgumentException  bound.universe != this.universe
	 */
	private void checkBound(int arity, TupleSet bound) {
		if (arity != bound.arity())
			throw new IllegalArgumentException("bound.arity != r.arity");
		if (!bound.universe().equals(factory.universe()))
			throw new IllegalArgumentException("bound.universe != this.universe");	
	}
	
	/**
	 * Sets both the lower and upper bounds of the given relation to 
	 * the given set of tuples. 
	 * 
	 * @requires tuples.arity = r.arity && tuples.universe = this.universe
	 * @ensures this.relations' = this.relations + r 
	 *          this.lowerBound' = this.lowerBound' ++ r->tuples &&
	 *          this.upperBound' = this.lowerBound' ++ r->tuples
	 * @throws NullPointerException  r = null || tuples = null 
	 * @throws IllegalArgumentException  tuples.arity != r.arity || tuples.universe != this.universe
	 */
	public void boundExactly(Relation r, TupleSet tuples) {
		checkBound(r.arity(), tuples);
		final TupleSet unmodifiableTuplesCopy = tuples.clone().unmodifiableView();
		lowers.put(r, unmodifiableTuplesCopy);
		uppers.put(r, unmodifiableTuplesCopy);
	}
	
	/**
	 * Sets the lower and upper bounds for the given relation. 
	 * 
	 * @requires lower.tuples in upper.tuples && lower.arity = upper.arity = r.arity &&
	 *           lower.universe = upper.universe = this.universe 
	 * @ensures this.relations' = this.relations + r &&
	 *          this.lowerBound' = this.lowerBound ++ r->lower &&
	 *          this.upperBound' = this.upperBound ++ r->upper
	 * @throws NullPointerException  r = null || lower = null || upper = null
	 * @throws IllegalArgumentException  lower.arity != r.arity || upper.arity != r.arity
	 * @throws IllegalArgumentException  lower.universe != this.universe || upper.universe != this.universe
	 * @throws IllegalArgumentException  lower.tuples !in upper.tuples                               
	 */
	public void bound(Relation r, TupleSet lower, TupleSet upper) {
		if (!upper.containsAll(lower))
			throw new IllegalArgumentException("lower.tuples !in upper.tuples");
		if (upper.size()==lower.size()) { 
			// upper.containsAll(lower) && upper.size()==lower.size() => upper.equals(lower)
			boundExactly(r, lower);
		} else {
			checkBound(r.arity(), lower);
			checkBound(r.arity(), upper);		
			lowers.put(r, lower.clone().unmodifiableView());
			uppers.put(r, upper.clone().unmodifiableView());
		}
	}
	
	/**
	 * Makes the specified tupleset the upper bound on the contents of the given relation.  
	 * The lower bound automatically become an empty tupleset with the same arity as
	 * the relation. 
	 * 
	 * @requires upper.arity = r.arity && upper.universe = this.universe
	 * @ensures this.relations' = this.relations + r 
	 *          this.lowerBound' = this.lowerBound ++ r->{s: TupleSet | s.universe = this.universe && s.arity = r.arity && no s.tuples} && 
	 *          this.upperBound' = this.upperBound ++ r->upper
	 * @throws NullPointerException  r = null || upper = null 
	 * @throws IllegalArgumentException  upper.arity != r.arity || upper.universe != this.universe
	 */
	public void bound(Relation r, TupleSet upper) {
		checkBound(r.arity(), upper);
		lowers.put(r, factory.noneOf(r.arity()).unmodifiableView());
		uppers.put(r, upper.clone().unmodifiableView());
	}
	
	/**
	 * Makes the specified tupleset an exact bound on the relational value
	 * that corresponds to the given integer.
	 * @requires ibound.arity = 1 && i.bound.size() = 1
	 * @ensures this.intBound' = this.intBound' ++ i -> ibound
	 * @throws NullPointerException  ibound = null
	 * @throws IllegalArgumentException  ibound.arity != 1 || ibound.size() != 1
	 * @throws IllegalArgumentException  ibound.universe != this.universe
	 */
	public void boundExactly(int i, TupleSet ibound) {
		checkBound(1, ibound);
		if (ibound.size() != 1)
			throw new IllegalArgumentException("ibound.size != 1: " + ibound);
		intbounds.put(i, ibound.clone().unmodifiableView());
	}
	

	/**
	 * Returns an unmodifiable view of this Bounds object.
	 * @return an unmodifiable view of his Bounds object.
	 */
	public Bounds unmodifiableView() {
		return new Bounds(factory, unmodifiableMap(lowers), unmodifiableMap(uppers), unmodifiableSequence(intbounds));
	}
	
	/**
	 * Returns a deep (modifiable) copy of this Bounds object.
	 * @return a deep (modifiable) copy of this Bounds object.
	 */
	public Bounds clone() {
		try {
			return new Bounds(factory, new LinkedHashMap<Relation, TupleSet>(lowers), 
					new LinkedHashMap<Relation, TupleSet>(uppers), intbounds.clone());
		} catch (CloneNotSupportedException cnse) {
			throw new InternalError(); // should not be reached
		}
	}
	
	/**
	 * @see java.lang.Object#toString()
	 */
	public String toString() {
		final StringBuilder str = new StringBuilder();
		str.append("relation bounds:");
		for(Map.Entry<Relation, TupleSet> entry: lowers.entrySet()) {
			str.append("\n ");
			str.append(entry.getKey());
			str.append(": [");
			str.append(entry.getValue());
			TupleSet upper = uppers.get(entry.getKey());
			if (!upper.equals(entry.getValue())) {
				str.append(", ");
				str.append(upper);
			} 
			str.append("]");
		}
		str.append("\nint bounds: ");
		str.append("\n ");
		str.append(intbounds);
		return str.toString();
	}
} public final class Instance implements Cloneable {
	private final Map<Relation, TupleSet> tuples;
	private final SparseSequence<TupleSet> ints;
	private final Universe universe;
	
	private Instance(Universe u, Map<Relation, TupleSet> tuples, SparseSequence<TupleSet> ints) {
		this.universe = u;
		this.tuples = tuples;
		this.ints = ints;
	}
	
	/**
	 * Constructs an empty instance over the given universe
	 * 
	 * @ensures this.universe' = universe && no this.tuples' 
	 * @throws NullPointerException  universe = null
	 */
	public Instance(final Universe universe) {
		if (universe==null) throw new NullPointerException("universe=null");
		this.universe = universe;
		this.tuples = new LinkedHashMap<Relation, TupleSet>();
		this.ints = new TreeSequence<TupleSet>();
	}
	
	/**
	 * Returns the universe from which the tuples in this instance
	 * are drawn.
	 * @return this.universe
	 */
	public Universe universe() {
		return universe;
	}
	
	/** 
	 * Returns true if this instance maps the given relation to a set
	 * of tuples; otherwise returns false.
	 * @return r in this.relations
	 */
	public boolean contains(Relation relation) {
		return tuples.containsKey(relation);
	}
	
	/**
	 * Returns true if this instance maps the given integer to a singleton
	 * tupleset; otherwise returns false.
	 * @return some this.tuples[i]
	 */
	public boolean contains(int i) {
		return ints.containsIndex(i);
	}
	
	/**
	 * Returns the relations mapped by this instance.  The returned set
	 * does not support addition.  It supports removal if this is not an
	 * unmodifiable instance.
	 * @return this.relations
	 */
	public Set<Relation> relations() {
		return tuples.keySet();
	}
	
	/**
	 * Returns the integers mapped by this instance.  The returned set 
	 * does not support addition.  It supports removal if this is not an
	 * unmodifiable instance.
	 * @return this.ints.TupleSet
	 */
	public IntSet ints() { 
		return ints.indices();
	}
	
	/**
	 * Maps the given relation to the given tuple set.  
	 * @ensures this.tuples' = this.tuples ++ relation->s
	 * @throws NullPointerException  relation = null || s = null
	 * @throws IllegalArgumentException  relation.arity != s.arity
	 * @throws IllegalArgumentException  s.universe != this.universe
	 * @throws UnsupportedOperationException  this is an unmodifiable instance
	 */
	public void add(final Relation relation, TupleSet s) {
		if (!s.universe().equals(universe))
			throw new IllegalArgumentException("s.universe!=this.universe");
		if (relation.arity()!=s.arity())
			throw new IllegalArgumentException("relation.arity!=s.arity");
		tuples.put(relation, s.clone().unmodifiableView());
	}

	/**
	 * Maps the given integer to the given tuple set.  
	 * @ensures this.tuples' = this.tuples ++ i->s
	 * @throws NullPointerException  s = null
	 * @throws IllegalArgumentException  s.arity != 1 || s.size() != 1
	 * @throws IllegalArgumentException  s.universe != this.universe
	 * @throws UnsupportedOperationException  this is an unmodifiable instance
	 */
	public void add(int i, TupleSet s) {
		if (!s.universe().equals(universe))
			throw new IllegalArgumentException("s.universe!=this.universe");
		if (s.arity()!=1)
			throw new IllegalArgumentException("s.arity!=1: " + s);
		if (s.size()!=1)
			throw new IllegalArgumentException("s.size()!=1: " + s);
		ints.put(i, s.clone().unmodifiableView());
	}
	
	/**
	 * Returns the set of tuples assigned to the given relation by this Instance.
	 * If the relation is not mapped by the model, null is returned.
	 * 
	 * @return this.tuples[relation]
	 */
	public TupleSet tuples(Relation relation) {
		return tuples.get(relation);
	}
	
	/**
	 * Returns a map view of Relation<:this.tuples.  The returned map is unmodifiable.
	 * @return a map view of Relation<:this.tuples.  
	 */
	public Map<Relation, TupleSet> relationTuples() {
		return Collections.unmodifiableMap(tuples);
	}
	
	/**
	 * Returns the set of tuples assigned to the given integer by this Instance.
	 * If the integer is not mapped by the model, null is returned.
	 * 
	 * @return this.tuples[i]
	 */
	public TupleSet tuples(int i) {
		return ints.get(i);
	}
	
	/**
	 * Returns a sparse sequence view of int<:this.tuples.  The returned sequence is unmodifiable.
	 * @return a sparse sequence view of int<:this.tuples.
	 */
	public SparseSequence<TupleSet> intTuples() {
		return Ints.unmodifiableSequence(ints);
	}
	
	/**
	 * Returns an unmodifiable view of this instance.
	 * @return an unmodifiable view of this instance.
	 */
	public Instance unmodifiableView() {
		return new Instance(universe, Collections.unmodifiableMap(tuples),  Ints.unmodifiableSequence(ints));
	}
	
	/**
	 * Returns a deep copy of this Instance object.
	 * @return a deep copy of this Instance object.
	 */
	public Instance clone() {
		try {
			return new Instance(universe, new LinkedHashMap<Relation, TupleSet>(tuples), ints.clone());
		} catch (CloneNotSupportedException cnse) {
			throw new InternalError(); // should not be reached
		}
	}
	
	/**
	 * {@inheritDoc}
	 * @see java.lang.Object#toString()
	 */
	public String toString() {
		return "relations: "+tuples.toString() + "\nints: " + ints;
	}

} public final class AnnotatedNode<N extends Node> {
	private final N node;
	private final Set<Node> sharedNodes;
	private final Map<? extends Node, ? extends Node> source;
	
	/**
	 * Constructs a new annotator for the given node.
	 * @ensures this.node' = node && this.source' = node.*components<:iden
	 */
	private AnnotatedNode(N node) {
		this.node = node;
		final SharingDetector detector = new SharingDetector();
		node.accept(detector);
		this.sharedNodes = Collections.unmodifiableSet(detector.sharedNodes());
		this.source = Collections.emptyMap();
	}
	
	
	/**
	 * Constructs a new annotator for the given node and source map.
	 * @ensures this.node' = node && this.source' = node.*components<:iden ++ source
	 */
	private AnnotatedNode(N node, Map<? extends Node, ? extends Node> source) {
		this.node = node;
		final SharingDetector detector = new SharingDetector();
		node.accept(detector);
		this.sharedNodes = Collections.unmodifiableSet(detector.sharedNodes());
		this.source = source;
	}
	
	/**
	 * Returns an annotation for the given node.  The source map of the returned annotation object
	 * maps each descendant of the node to itself.
	 * @return { a: AnnotatedNode<N> | a.node = node && a.source = node.*components<:iden }
	 */
	public static <N extends Node> AnnotatedNode<N> annotate(N node) { return new AnnotatedNode<N>(node); }
	
	/**
	 * Returns an annotation for the given node.  The source map of the returned annotation object
	 * maps each descendant of the node to its value in the given source map, or to itself
	 * if the given source map has no value for that descendant.
	 * @return { a: AnnotatedNode<N> | a.node = node && a.source = (node.*components<:iden) ++ source }
	 */
	public static <N extends Node> AnnotatedNode<N> annotate(N node, Map<? extends Node, ? extends Node> source) { return new AnnotatedNode<N>(node,source); }
	
	/**
	 * Returns an annotation for an n-ary conjunctions of  {@linkplain Nodes#roots(Formula) roots} of the given formula. 
	 * The source map of the returned annotation object maps each descendant of the node to itself.  
	 * The root conjunction itself is mapped to the input formula.
	 * @return { a: AnnotatedNode<Formula> | a.node = Formula.and(Nodes.roots(formula)) && a.source = (node.^components<:iden) + a.node->formula }
	 */
	public static AnnotatedNode<Formula> annotateRoots(Formula formula) { 
		final Formula flat = Formula.and(Nodes.roots(formula));
		return new AnnotatedNode<Formula>(flat, Collections.singletonMap(flat, formula));
	}
	
	/**
	 * Returns this.node.
	 * @return this.node
	 */
	public final N node() {
		return node;
	}
	
	/**
	 * Returns the source of the given descendant of this.node.
	 * @requires n in this.node.*components
	 * @return this.source[n]
	 */
	public final Node sourceOf(Node n) {
		final Node d = source.get(n);
		return d==null ? n : d;
	}

	
	/**
	 * Returns the set of all non-leaf descendants of this.node that have more than one parent.
	 * @return {n: Node | some n.children && #(n.~components & this.node.*components) > 1 }
	 */
	public final Set<Node> sharedNodes() { 
		return sharedNodes;
	}
	
	/**
	 * Returns the set of all relations at the leaves of this annotated node.
	 * @return Relation & this.node.*components
	 */
	public final Set<Relation> relations() {
		final Set<Relation> relations = new IdentityHashSet<Relation>();
		final AbstractVoidVisitor visitor = new AbstractVoidVisitor() {
			private final Set<Node> visited = new IdentityHashSet<Node>(sharedNodes.size());
			protected boolean visited(Node n) {
				return sharedNodes.contains(n) && !visited.add(n);
			}
			public void visit(Relation relation) {
				relations.add(relation);
			}
		};
		node.accept(visitor);
		return relations;
	}
	
	/**
	 * Returns true if this.node contains a child whose meaning depends on 
	 * integer bounds (i.e. an ExprToIntCast node with SUM operator or an IntToExprCast node or Expression.INTS constant).
	 * @return true if this.node contains a child whose meaning depends on 
	 * integer bounds (i.e. an ExprToIntCast node with SUM operator or an IntToExprCast node or Expression.INTS constant).
	 */
	public final boolean usesInts() {
		final AbstractDetector detector = new AbstractDetector(sharedNodes) {
			public Boolean visit(IntToExprCast expr) {
				return cache(expr, Boolean.TRUE);
			}
			public Boolean visit(ExprToIntCast intExpr) {
				if (intExpr.op()==ExprCastOperator.CARDINALITY)
					super.visit(intExpr);
				return cache(intExpr, Boolean.TRUE);
			}
			public Boolean visit(ConstantExpression expr) {
				return expr==Expression.INTS ? Boolean.TRUE : Boolean.FALSE;
			}
		};
		return (Boolean)node.accept(detector);
	}
	
	/**
	 * Returns a map of RelationPredicate names to sets of top-level relation predicates with
	 * the corresponding names in this.node.  
	 * @return a map of RelationPredicate names to sets of top-level relation predicates with
	 * the corresponding names in this.node.  A predicate is considered 'top-level'  
	 * if it is a component of the top-level conjunction, if any, of this.node.  
	 */
	public final Map<RelationPredicate.Name, Set<RelationPredicate>> predicates() {
		final PredicateCollector collector = new PredicateCollector(sharedNodes);
		node.accept(collector);
		return collector.preds;
	}
	
	/**
	 * Returns a Detector that will return TRUE when applied to a descendant
	 * of this.node iff the descendant contains a quantified formula.
	 * @return a Detector that will return TRUE when applied to a descendant
	 * of this.node iff the descendant contains a quantified formula.
	 */
	public final AbstractDetector quantifiedFormulaDetector() {
		return new AbstractDetector(sharedNodes) {
			public Boolean visit(QuantifiedFormula quantFormula) {
				return cache(quantFormula, true);
			}
		};
	}
	
	/**
	 * Returns a Detector that will return TRUE when applied to a descendant
	 * of this.node iff the descendant contains a free variable.
	 * @return a Detector that will return TRUE when applied to a descendant
	 * of this.node iff the descendant contains a free variable.
	 */
	public final AbstractDetector freeVariableDetector() {
		return new FreeVariableDetector(sharedNodes);
	}
	
	/**
	 * Returns a string representation of this annotated node.
	 * @return string representation of this annotated node.
	 */
	public String toString() {
		final StringBuilder ret =  new StringBuilder();
		ret.append("node: ");
		ret.append(node);
		ret.append("\nshared nodes: ");
		ret.append(sharedNodes);
		ret.append("\nsources: ");
		ret.append(source);
		return ret.toString();
	}
	
	/**
	 * Detects shared non-leaf descendants of a given node.
	 * 
	 * @specfield node: Node // node to which the analyzer is applied
	 */
	private static final class SharingDetector extends AbstractVoidVisitor {
		/* maps each internal node with more than one parent to TRUE and all
		 * other internal nodes to FALSE */
		final IdentityHashMap<Node,Boolean> sharingStatus;
		/* @invariant numShareNodes = #sharingStatus.TRUE */
		int numSharedNodes;
		
		SharingDetector() {
			sharingStatus = new IdentityHashMap<Node,Boolean>();
		}
		
		/**
		 * Returns the shared internal nodes of this.node.  This method should
		 * be called only after this visitor has been applied to this.node.
		 * @return {n: Node | #(n.~children & node.*children) > 1 }
		 */
		IdentityHashSet<Node> sharedNodes() {
			final IdentityHashSet<Node> shared = new IdentityHashSet<Node>(numSharedNodes);
			for(Map.Entry<Node,Boolean> entry : sharingStatus.entrySet()) {
				if (entry.getValue()==Boolean.TRUE)
					shared.add(entry.getKey());
			}
			return shared;
		}
		
		/**
		 * Records the visit to the given node in the status map.
		 * If the node has not been visited before, it is mapped
		 * to Boolean.FALSE and false is returned.  Otherwise, 
		 * it is mapped to Boolean.TRUE and true is returned.
		 * The first time a Node is mapped to true, numSharedNodes
		 * is incremented by one.
		 * @ensures no this.shared[node] => this.shared' = this.shared + node->FALSE,
		 *          this.shared[node] = FALSE => this.shared' = this.shared + node->TRUE,
		 *          this.shared' = this.shared
		 * @return this.shared'[node]
		 */
		protected final boolean visited(Node node) {
			Boolean status = sharingStatus.get(node);
			if (!Boolean.TRUE.equals(status)) {
				if (status==null) {
					status = Boolean.FALSE;
				} else { // status == Boolean.FALSE
					status = Boolean.TRUE;
					numSharedNodes++;
				}
				sharingStatus.put(node,status);
			}
			return status;
		}
	}

	/**
	 * A visitor that detects free variables of a node.
	 * @author Emina Torlak
	 */
	private static final class FreeVariableDetector extends AbstractDetector {
		/* Holds the variables that are currently in scope, with the
		 * variable at the top of the stack being the last declared variable. */
		
		private final Stack<Variable> varsInScope = new ArrayStack<Variable>();
		
		/**
		 * Constructs a new free variable detector.
		 */
		FreeVariableDetector(Set<Node> sharedNodes) {
			super(sharedNodes);
		}
		
		/**
		 * Visits the given comprehension, quantified formula, or sum expression.  
		 * The method returns TRUE if the creator body contains any 
		 * variable not bound by the decls; otherwise returns FALSE.  
		 */
		private Boolean visit(Node creator, Decls decls, Node body) {
			Boolean ret = lookup(creator);
			if (ret!=null) return ret;
			boolean retVal = false;
			for(Decl decl : decls) {
				retVal = decl.expression().accept(this) || retVal;
				varsInScope.push(decl.variable());
			}
			retVal = ((Boolean)body.accept(this)) || retVal;
			for(int i = decls.size(); i > 0; i--) {
				varsInScope.pop();
			}
			return cache(creator, retVal);
		}
		/**
		 * Returns TRUE if the given variable is free in its parent, otherwise returns FALSE.
		 * @return TRUE if the given variable is free in its parent, otherwise returns FALSE.
		 */
		public Boolean visit(Variable variable) {
			return Boolean.valueOf(varsInScope.search(variable)<0);
		}	
		public Boolean visit(Decl decl) {
			Boolean ret = lookup(decl);
			if (ret!=null) return ret;
			return cache(decl, decl.expression().accept(this));
		}	
		public Boolean visit(Comprehension comprehension) {
			return visit(comprehension, comprehension.decls(), comprehension.formula());
		}		
		public Boolean visit(SumExpression intExpr) {
			return visit(intExpr, intExpr.decls(), intExpr.intExpr());
		}
		public Boolean visit(QuantifiedFormula qformula) {
			return visit(qformula, qformula.decls(), qformula.formula());
		}
	}
	
	/**
	 * A visitor that detects and collects
	 * top-level relation predicates; i.e. predicates that
	 * are components in the top-level conjunction, if any, on ANY
	 * path starting at the root.
	 */
	private static final class PredicateCollector extends AbstractVoidVisitor {
		protected boolean negated;
		private final Set<Node> sharedNodes;
		/* if a given node is not mapped at all, it means that it has not been visited;
		 * if it is mapped to FALSE, it has been visited with negated=FALSE, 
		 * if it is mapped to TRUE, it has been visited with negated=TRUE,
		 * if it is mapped to null, it has been visited with both values of negated. */
		private final Map<Node,Boolean> visited;	
		/* holds the top level predicates at the end of the visit*/
		final EnumMap<RelationPredicate.Name, Set<RelationPredicate>> preds;
		/**
		 * Constructs a new collector.
		 * @ensures this.negated' = false
		 */
		PredicateCollector(Set<Node> sharedNodes) {
			this.sharedNodes = sharedNodes;
			this.visited = new IdentityHashMap<Node,Boolean>();
			this.negated = false;
			preds = new EnumMap<RelationPredicate.Name, Set<RelationPredicate>>(RelationPredicate.Name.class);	
			preds.put(ACYCLIC, new IdentityHashSet<RelationPredicate>(4));
			preds.put(TOTAL_ORDERING, new IdentityHashSet<RelationPredicate>(4));
			preds.put(FUNCTION, new IdentityHashSet<RelationPredicate>(8));
		}
		/**
		 * Returns true if n has already been visited with the current value of the
		 * negated flag; otherwise returns false.
		 * @ensures records that n is being visited with the current value of the negated flag
		 * @return true if n has already been visited with the current value of the
		 * negated flag; otherwise returns false.
		 */
		@Override
		protected final boolean visited(Node n) {
			if (sharedNodes.contains(n)) {
				if (!visited.containsKey(n)) { // first visit
					visited.put(n, Boolean.valueOf(negated));
					return false;
				} else {
					final Boolean visit = visited.get(n);
					if (visit==null || visit==negated) { // already visited with same negated value
						return true; 
					} else { // already visited with different negated value
						visited.put(n, null);
						return false;
					}
				}
			}
			return false;
		}
		/**
		 * Calls visited(comp); comp's children are not top-level formulas
		 * so they are not visited.
		 */
		public void visit(Comprehension comp) {
			visited(comp);
		}
		/**
		 * Calls visited(ifexpr); ifexpr's children are not top-level formulas
		 * so they are not visited.
		 */
		public void visit(IfExpression ifexpr) {
			visited(ifexpr);
		}
		/**
		 * Calls visited(ifexpr); ifexpr's children are not top-level formulas
		 * so they are not visited.
		 */
		public void visit(IfIntExpression ifexpr) {
			visited(ifexpr);
		}
		/**
		 * Calls visited(intComp); intComp's children are not top-level formulas
		 * so they are not visited.
		 */
		public void visit(IntComparisonFormula intComp) {
			visited(intComp);
		}
		/**
		 * Calls visited(quantFormula); quantFormula's children are not top-level formulas
		 * so they are not visited.
		 */
		public void visit(QuantifiedFormula quantFormula) {
			visited(quantFormula);
		}
		/**
		 * Visits the children of the given formula if it has not been visited already with
		 * the given value of the negated flag and if binFormula.op==IMPLIES && negated or
		 * binFormula.op==AND && !negated or binFormula.op==OR && negated.  Otherwise does nothing.
		 * @see kodkod.ast.visitor.AbstractVoidVisitor#visit(kodkod.ast.BinaryFormula)
		 */
		public void visit(BinaryFormula binFormula) {
			if (visited(binFormula)) return;
			final FormulaOperator op = binFormula.op();
		
			if ((!negated && op==AND) || (negated && op==OR)) { // op==AND || op==OR
				binFormula.left().accept(this);
				binFormula.right().accept(this);
			} else if (negated && op==IMPLIES) { // !(a => b) = !(!a || b) = a && !b
				negated = !negated;
				binFormula.left().accept(this);
				negated = !negated;
				binFormula.right().accept(this);
			} 
		}
		/**
		 * Visits the children of the given formula if it has not been visited already with
		 * the given value of the negated flag and if formula.op==OR && negated or
		 * formula.op==AND && !negated. Otherwise does nothing.
		 * @see kodkod.ast.visitor.AbstractVoidVisitor#visit(kodkod.ast.NaryFormula)
		 */
		public void visit(NaryFormula formula) { 
			if (visited(formula)) return;
			final FormulaOperator op = formula.op();
			if ((!negated && op==AND) || (negated && op==OR)) { // op==AND || op==OR
				for(Formula child : formula) { 
					child.accept(this);
				}
			}
		}
		
		/**
		 * Visits the children of the child of the child formula, with
		 * the negation of the current value of the negated flag, 
		 * if it has not already been visited 
		 * with the current value of this.negated; otherwise does nothing.
		 */
		public void visit(NotFormula not) {
			if (visited(not)) return;
			negated = !negated;
			not.formula().accept(this);
			negated = !negated;
		}
		/**
		 * Calls visited(compFormula); compFormula's children are not top-level formulas
		 * so they are not visited.
		 */
		public void visit(ComparisonFormula compFormula) {
			visited(compFormula);
		}
		/**
		 * Calls visited(multFormula); multFormula's child is not top-level formulas
		 * so it is not visited.
		 */
		public void visit(MultiplicityFormula multFormula) {
			visited(multFormula);
		}
		/**
		 * Records the visit to this predicate if it is not negated.
		 */
		public void visit(RelationPredicate pred) {
			if (visited(pred)) return;
			if (!negated) {
				preds.get(pred.name()).add(pred);
			}
		}
	}
}
import static kodkod.engine.fol2sat.FormulaFlattener.flatten;
import static kodkod.engine.fol2sat.Skolemizer.skolemize;
import static kodkod.util.nodes.AnnotatedNode.annotate;
import static kodkod.util.nodes.AnnotatedNode.annotateRoots;
import static kodkod.util.collections.Containers.setDifference;
import java.util.Collections;
import java.util.IdentityHashMap;
import java.util.LinkedHashSet;
import java.util.Map;
import java.util.Set;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.IntExpression;
import kodkod.ast.Node;
import kodkod.ast.Relation;
import kodkod.ast.RelationPredicate;
import kodkod.ast.visitor.AbstractReplacer;
import kodkod.engine.bool.BooleanAccumulator;
import kodkod.engine.bool.BooleanConstant;
import kodkod.engine.bool.BooleanFactory;
import kodkod.engine.bool.BooleanFormula;
import kodkod.engine.bool.BooleanMatrix;
import kodkod.engine.bool.BooleanValue;
import kodkod.engine.bool.Int;
import kodkod.engine.bool.Operator;
import kodkod.engine.config.Options;
import kodkod.engine.satlab.SATSolver;
import kodkod.instance.Bounds;
import kodkod.instance.Instance;
import kodkod.instance.TupleSet;
import kodkod.util.ints.IndexedEntry;
import kodkod.util.ints.IntSet;
import kodkod.util.nodes.AnnotatedNode;
/* 
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.engine.fol2sat;




/** 
 * Translates, evaluates, and approximates {@link Node nodes} with
 * respect to given {@link Bounds bounds} (or {@link Instance instances}) and {@link Options}.
 * 
 * @author Emina Torlak 
 */
public final class Translator {
	
	/*---------------------- public methods ----------------------*/
	/**
	 * Overapproximates the value of the given expression using the provided bounds and options.
	 * @return a BooleanMatrix whose TRUE entries represent the tuples contained in a sound overapproximation
	 * of the expression.
	 * @throws expression = null || instance = null || options = null
	 * @throws UnboundLeafException  the expression refers to an undeclared variable or a relation not mapped by the instance
	 * @throws HigherOrderDeclException  the expression contains a higher order declaration
	 */
	@SuppressWarnings("unchecked")
	public static BooleanMatrix approximate(Expression expression, Bounds bounds, Options options) {