import kodkod.ast.visitor.AbstractReplacer; //导入依赖的package包/类
/**
 * Returns an annotated formula f such that f.node is equivalent to
 * annotated.node with its <tt>truePreds</tt> replaced with the constant
 * formula TRUE and the remaining predicates replaced with equivalent
 * constraints.
 * 
 * @requires truePreds in annotated.predicates()[RelationnPredicate.NAME]
 * @requires truePreds are trivially true with respect to this.bounds
 * @return an annotated formula f such that f.node is equivalent to
 *         annotated.node with its <tt>truePreds</tt> replaced with the
 *         constant formula TRUE and the remaining predicates replaced with
 *         equivalent constraints.
 */
private AnnotatedNode<Formula> inlinePredicates(final AnnotatedNode<Formula> annotated,
		final Set<RelationPredicate> truePreds) {
	final AbstractReplacer inliner = new AbstractReplacer(annotated.sharedNodes()) {
		public Formula visit(RelationPredicate pred) {
			Formula ret = lookup(pred);
			if (ret != null)
				return ret;
			return truePreds.contains(pred) ? cache(pred, Formula.TRUE) : cache(pred, pred.toConstraints());
		}
	};
	Formula x = annotated.node().accept(inliner);
	return annotate(x);
}
 

import kodkod.ast.visitor.AbstractReplacer; //导入依赖的package包/类
/**
 * Returns an annotated formula f such that f.node is equivalent to annotated.node
 * with its <tt>simplified</tt> predicates replaced with their corresponding Formulas and the remaining
 * predicates replaced with equivalent constraints.  The annotated formula f will contain transitive source 
 * information for each of the subformulas of f.node.  Specifically, let t be a subformula of f.node, and
 * s be a descdendent of annotated.node from which t was derived.  Then, f.source[t] = annotated.source[s]. </p>
 * @requires this.options.logTranslation = true
 * @requires simplified.keySet() in annotated.predicates()[RelationPredicate.NAME]
 * @requires no disj p, p': simplified.keySet() | simplified.get(p) = simplifed.get(p') // this must hold in order
 * to maintain the invariant that each subformula of the returned formula has exactly one source
 * @requires for each p in simplified.keySet(), the formulas "p and [[this.bounds]]" and
 * "simplified.get(p) and [[this.bounds]]" are equisatisfiable
 * @return an annotated formula f such that f.node is equivalent to annotated.node
 * with its <tt>simplified</tt> predicates replaced with their corresponding Formulas and the remaining
 * predicates replaced with equivalent constraints.
 */
private AnnotatedNode<Formula> inlinePredicates(final AnnotatedNode<Formula> annotated, final Map<RelationPredicate,Formula> simplified) {
	final Map<Node,Node> sources = new IdentityHashMap<Node,Node>();
	final AbstractReplacer inliner = new AbstractReplacer(annotated.sharedNodes()) {
		private RelationPredicate source =  null;			
		protected <N extends Node> N cache(N node, N replacement) {
			if (replacement instanceof Formula) {
				if (source==null) {
					final Node nsource = annotated.sourceOf(node);
					if (replacement!=nsource) 
						sources.put(replacement, nsource);
				} else {
					sources.put(replacement, source);
				}
			}
			return super.cache(node, replacement);
		}
		public Formula visit(RelationPredicate pred) {
			Formula ret = lookup(pred);
			if (ret!=null) return ret;
			source = pred;
			if (simplified.containsKey(pred)) {
				ret = simplified.get(pred).accept(this);
			} else {
				ret = pred.toConstraints().accept(this);
			}
			source = null;
			return cache(pred, ret);
		}
	};

	return annotate(annotated.node().accept(inliner), sources);
}
 

import kodkod.ast.visitor.AbstractReplacer; //导入依赖的package包/类
/**
 * Returns an annotated formula f such that f.node is equivalent to annotated.node
 * with its <tt>truePreds</tt> replaced with the constant formula TRUE and the remaining
 * predicates replaced with equivalent constraints.
 * @requires truePreds in annotated.predicates()[RelationnPredicate.NAME]
 * @requires truePreds are trivially true with respect to this.bounds
 * @return an annotated formula f such that f.node is equivalent to annotated.node
 * with its <tt>truePreds</tt> replaced with the constant formula TRUE and the remaining
 * predicates replaced with equivalent constraints.
 */
private AnnotatedNode<Formula> inlinePredicates(final AnnotatedNode<Formula> annotated, final Set<RelationPredicate> truePreds) {
	final AbstractReplacer inliner = new AbstractReplacer(annotated.sharedNodes()) {
		public Formula visit(RelationPredicate pred) {
			Formula ret = lookup(pred);
			if (ret!=null) return ret;
			return truePreds.contains(pred) ? cache(pred, Formula.TRUE) : cache(pred, pred.toConstraints());
		}
	};
	return annotate(annotated.node().accept(inliner));	
}
 

import kodkod.ast.visitor.AbstractReplacer; //导入依赖的package包/类
@SuppressWarnings("unchecked")
private Formula makeReadable(Formula formula) { 
	final List<Formula> replacements = new ArrayList<Formula>();
	final Map<Expression, Integer> levels = new LinkedHashMap<Expression, Integer>();
	final AbstractReplacer replacer = new AbstractReplacer(Collections.EMPTY_SET) { 
		protected <N extends Node> N cache(N node, N replacement) {
			cache.put(node, replacement);
			return replacement;
		}
		public Expression visit(BinaryExpression expr) { 
			Expression ret = lookup(expr);
			if (ret!=null) return ret;
			final Expression left = expr.left().accept(this);
			final Expression right = expr.right().accept(this);
			if (expr.op()==ExprOperator.OVERRIDE && left instanceof Relation) { 
				final int level = levels.containsKey(left) ? levels.get(left) : 0;
				final Relation r = Relation.nary(((Relation)left).name()+"'", expr.arity());
				replacements.add(r.eq(left.compose(expr.op(), right)));
				levels.put(left, level+1);
				return cache(expr, r);
			}
			return cache(expr, left.compose(expr.op(), right));
		}
	};
	
	int size;
	do {
		size = replacements.size();
		formula = formula.accept(replacer);
	} while (size < replacements.size());
	
	return formula.and(Formula.and(replacements));
}
 

import kodkod.ast.visitor.AbstractReplacer; //导入依赖的package包/类
public boolean solveNext() {
	convInst = null;
	iterCnt = 0;
	int maxIter = options.getHolSome4AllMaxIter();
	HOLTranslation currTr = convTr;
	while (currTr.cnf().solve()) {
		final Instance currInst = currTr.interpret();
		final Evaluator eval = new Evaluator(currInst);
		convTr = currTr;
		convInst = currTr.interpret();
		if (iterCnt == 0)
			rep.holFixpointFirstSolution(Fixpoint.this, currInst);
		else
			rep.holFixpointIncrementingOutcome(Fixpoint.this, currInst);
		if (maxIter > 0 && iterCnt > maxIter)
			throw new HOLException("[Fixpoint] Max number of iterations reached: " + maxIter);
		iterCnt++;
		// TODO: works only when inc is first order
		Formula inc = proc.fullConditionFormula().accept(new AbstractReplacer(new HashSet<Node>()) {
			@Override
			public Expression visit(UnaryExpression unaryExpr) {
				if (unaryExpr.op() != ExprOperator.PRE)
					return super.visit(unaryExpr);
				TupleSet val = eval.evaluate(unaryExpr.expression());
				return bounds.ts2expr(val);
			}
		});
		// if (iterCnt == 1) {
		// List<Formula> fix = new
		// ArrayList<Formula>(bounds.relations().size());
		// for (Relation r: bounds.relations()) {
		// if (r.isAtom()) continue;
		// if (!r.name().endsWith("_clq") &&
		// !r.name().endsWith("_e")) {
		// Expression val = bounds.ts2expr(currInst.tuples(r));
		// fix.add(val == Expression.NONE ? r.no() : r.eq(val));
		// }
		// }
		// inc = inc.and(Formula.and(fix));
		// }
		rep.holFixpointIncrementing(Fixpoint.this, inc);
		currTr = currTr.next(inc);
	}
	if (convInst != null && iterCnt > 0)
		rep.holFixpointIncrementingOutcome(Fixpoint.this, null);
	return convInst != null;
}