import kodkod.ast.Node; //导入依赖的package包/类
/**
 * Constructs a new file log for the sources of the given annotated formula,
 * using the provided fixed map, file, and tuplefactory.
 * @requires all f: annotated.node.*children & Formula | logMap.get(f) = freeVariables(f)
 * @requires the file was written by a FileLogger using the given map
 */
FileLog(AnnotatedNode<Formula> annotated, FixedMap<Formula, Variable[]> logMap, File file, Bounds bounds) {
	this.file = file;
	this.bounds = bounds;
	this.roots = Nodes.conjuncts(annotated.node());
	
	final int size = logMap.entrySet().size();
	this.original = new Node[size];
	this.translated = new Formula[size];
	this.freeVars = new Variable[size][];
	int index = 0;
	for(Map.Entry<Formula, Variable[]> e : logMap.entrySet()) {
		translated[index] = e.getKey();
		original[index] = annotated.sourceOf(e.getKey());
		freeVars[index] = e.getValue();
		index++;
	}
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * Constructs a proof finder for the given log.
 * 
 * @ensures this.log' = log
 */
NodePruner(TranslationLog log) {
	visited = new IdentityHashSet<Node>();
	relevant = new IdentityHashSet<Node>();

	final RecordFilter filter = new RecordFilter() {
		public boolean accept(Node node, Formula translated, int literal, Map<Variable,TupleSet> env) {
			return env.isEmpty();
		}
	};

	constNodes = new LinkedHashMap<Formula,Boolean>();
	for (Iterator<TranslationRecord> itr = log.replay(filter); itr.hasNext();) {
		TranslationRecord rec = itr.next();
		int lit = rec.literal();
		if (Math.abs(lit) != Integer.MAX_VALUE) {
			constNodes.remove(rec.translated());
		} else if (lit == Integer.MAX_VALUE) {
			constNodes.put(rec.translated(), Boolean.TRUE);
		} else {
			constNodes.put(rec.translated(), Boolean.FALSE);
		}
	}
}
 

import kodkod.ast.Node; //导入依赖的package包/类
public static AnnotatedNode<Formula> toNNF(AnnotatedNode<Formula> annotated, Reporter reporter) {
	if (reporter != null)
		reporter.convertingToNNF();
	final FullNegationPropagator flat = new FullNegationPropagator(annotated.sharedNodes());
	annotated.node().accept(flat);
	final List<Formula> roots = new ArrayList<Formula>(flat.annotations.size());
	roots.addAll(flat.annotations.keySet());
	for (Iterator<Map.Entry<Formula,Node>> itr = flat.annotations.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();
			/* TODO: what is this for? */ } else {
			entry.setValue(source);
		}
	}
	return AnnotatedNode.annotate(Formula.and(flat.conjuncts), flat.annotations);
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * Constructs a new file log for the sources of the given annotated
 * formula, using the provided fixed map, file, and tuplefactory.
 * 
 * @requires all f: annotated.node.*children & Formula | logMap.get(f) =
 *           freeVariables(f)
 * @requires the file was written by a FileLogger using the given map
 */
FileLog(AnnotatedNode<Formula> annotated, FixedMap<Formula,Variable[]> logMap, File file, Bounds bounds) {
	this.file = file;
	this.bounds = bounds;
	this.roots = Nodes.conjuncts(annotated.node());

	final int size = logMap.entrySet().size();
	this.original = new Node[size];
	this.translated = new Formula[size];
	this.freeVars = new Variable[size][];
	int index = 0;
	for (Map.Entry<Formula,Variable[]> e : logMap.entrySet()) {
		translated[index] = e.getKey();
		original[index] = annotated.sourceOf(e.getKey());
		freeVars[index] = e.getValue();
		index++;
	}
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * 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;
}
 

import kodkod.ast.Node; //导入依赖的package包/类
public static AnnotatedNode<Formula> toPNF(AnnotatedNode<Formula> annotated) {
	final PrenexNFConverter pnfConv = new PrenexNFConverter(annotated.sharedNodes());
	List<Formula> conj = new ArrayList<Formula>();
	for (Formula f : Nodes.allConjuncts(annotated.node(), null))
		conj.add(f.accept(pnfConv));
	Formula ans = Formula.and(conj);

	final List<Formula> roots = new ArrayList<Formula>(pnfConv.annotations.size());
	roots.addAll(pnfConv.annotations.keySet());
	for (Iterator<Map.Entry<Formula,Node>> itr = pnfConv.annotations.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(ans, pnfConv.annotations);
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * Returns the result of applying this visitor to the given annotated
 * formula.
 * 
 * @return the result of applying this visitor to the given annotated
 *         formula.
 */
final AnnotatedNode<Formula> apply(AnnotatedNode<Formula> annotated) {
	annotated.node().accept(this);
	final List<Formula> roots = new ArrayList<Formula>(conjuncts.size());
	roots.addAll(conjuncts.keySet());
	for (Iterator<Map.Entry<Formula,Node>> itr = 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), conjuncts);
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * Calls nf.formula.accept(this) after flipping the negation flag.
 * 
 * @see kodkod.ast.visitor.AbstractVoidVisitor#visit(kodkod.ast.NotFormula)
 */
public final void visit(NotFormula nf) {
	if (visited(nf))
		return;

	final Map<Formula,Node> oldConjuncts = conjuncts;
	conjuncts = new LinkedHashMap<Formula,Node>();
	negated = !negated;
	nf.formula().accept(this);
	negated = !negated;
	if (conjuncts.size() > 1) { // was broken down further
		oldConjuncts.putAll(conjuncts);
		conjuncts = oldConjuncts;
	} else { // wasn't broken down further
		conjuncts = oldConjuncts;
		conjuncts.put(negated ? nf.formula() : nf, nf);
	}
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.engine.Proof#highLevelCore()
 */
public final Map<Formula, Node> highLevelCore() {
	if (coreRoots == null) { 
		final RecordFilter unitFilter = new RecordFilter() {
			final IntSet coreUnits = StrategyUtils.coreUnits(solver.proof());
			final Set<Formula> roots = log().roots();
			public boolean accept(Node node, Formula translated, int literal, Map<Variable, TupleSet> env) {
				return roots.contains(translated) && coreUnits.contains(Math.abs(literal));
			}
			
		};
		coreRoots = new LinkedHashMap<Formula, Node>();
		final IntSet seenUnits = new IntTreeSet();
		for(Iterator<TranslationRecord> itr = log().replay(unitFilter); itr.hasNext(); ) {
			// it is possible that two top-level formulas have identical meaning,
			// and are represented with the same core unit; in that case, we want only
			// one of them in the core.
			final TranslationRecord rec = itr.next();
			if (seenUnits.add(rec.literal())) {
				coreRoots.put(rec.translated(), rec.node());
			}  
		}
		coreRoots = Collections.unmodifiableMap(coreRoots);
	}
	return coreRoots;
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * 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);
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * 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;
}
 

import kodkod.ast.Node; //导入依赖的package包/类
private void edge(Node n1, Node n2) { 
	if (n2 instanceof LeafExpression || n2 instanceof ConstantFormula || n2 instanceof IntConstant) {
		
	}
	graph.append(id(n1));
	graph.append("->");
	graph.append(id(n2));
	graph.append(";\n");
}
 

import kodkod.ast.Node; //导入依赖的package包/类
static String apply(Node node) { 
	final Dotifier dot = new Dotifier();
	dot.graph.append("digraph {\n");
	node.accept(dot);
	dot.graph.append("}");
	return dot.graph.toString();
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.Proof#highLevelCore()
 */
public final Map<Formula,Node> highLevelCore() {
	if (coreRoots == null) {
		final RecordFilter unitFilter = new RecordFilter() {
			final IntSet		coreUnits	= StrategyUtils.coreUnits(solver.proof());
			final Set<Formula>	roots		= log().roots();

			public boolean accept(Node node, Formula translated, int literal, Map<Variable,TupleSet> env) {
				return roots.contains(translated) && coreUnits.contains(Math.abs(literal));
			}

		};
		coreRoots = new LinkedHashMap<Formula,Node>();
		final IntSet seenUnits = new IntTreeSet();
		for (Iterator<TranslationRecord> itr = log().replay(unitFilter); itr.hasNext();) {
			// it is possible that two top-level formulas have identical
			// meaning,
			// and are represented with the same core unit; in that case, we
			// want only
			// one of them in the core.
			final TranslationRecord rec = itr.next();
			if (seenUnits.add(rec.literal())) {
				coreRoots.put(rec.translated(), rec.node());
			}
		}
		coreRoots = Collections.unmodifiableMap(coreRoots);
	}
	return coreRoots;
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.Proof#highLevelCore()
 */
public final Map<Formula,Node> highLevelCore() {
	if (coreRoots == null) {
		final Iterator<TranslationRecord> itr = core();
		final Set<Formula> roots = log().roots();
		coreRoots = new LinkedHashMap<Formula,Node>();
		while (itr.hasNext()) {
			TranslationRecord rec = itr.next();
			if (roots.contains(rec.translated()))
				coreRoots.put(rec.translated(), rec.node());
		}
		coreRoots = Collections.unmodifiableMap(coreRoots);
	}
	return coreRoots;
}
 

import kodkod.ast.Node; //导入依赖的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 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.Node; //导入依赖的package包/类
private void visit(Node parent, Object label, Iterator<? extends Node> children) {
	if (visited(parent)) return;
	node(parent, label.toString());
	while(children.hasNext()) {
		Node child = children.next();
		child.accept(this);
		edge(parent, child);
	}
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * Caches the given replacement for the specified node, if 
 * the node is a syntactically shared expression, int expression or declaration with
 * no free variables.  Otherwise does nothing.  The method returns
 * the replacement node.  
 * @return replacement
 */
@Override
protected final <N extends Node> N cache(N node, N replacement) {
	if (cache.containsKey(node)) {
		cache.put(node, replacement);
	}
	return replacement;
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.ast.visitor.AbstractVoidVisitor#visit(kodkod.ast.QuantifiedFormula)
 */
public final void visit(QuantifiedFormula qf) {
	if (visited(qf)) return;
	
	if (breakupQuantifiers) {
		
		final Quantifier quant = qf.quantifier();
		
		if ((!negated && quant==ALL) || (negated && quant==SOME)) { // may break down further
			final Map<Formula, Node> oldConjuncts = conjuncts;
			conjuncts = new LinkedHashMap<Formula, Node>();
			qf.formula().accept(this);
			if (conjuncts.size()>1) { // was broken down further
				final Decls decls = qf.decls();
				for(Map.Entry<Formula, Node> entry : conjuncts.entrySet()) { 
					oldConjuncts.put(entry.getKey().forAll(decls), entry.getValue());
				}
				conjuncts = oldConjuncts;
				return;
			} else { // wasn't broken down further
				conjuncts = oldConjuncts;
			}
		} // won't break down further
	} 

	addConjunct(qf);
	
}
 

import kodkod.ast.Node; //导入依赖的package包/类
/**
 * Constructs a new translation cache for the given annotated node.
 * @ensures this.node' = annotated.node 
 */
FOL2BoolCache(AnnotatedNode<? extends Node> annotated) {
	final CacheCollector collector = new CacheCollector(annotated.sharedNodes());
	annotated.node().accept(collector);

	this.cache = new IdentityHashMap<Node, Record>(collector.cache().size());
	for(Map.Entry<Node, Set<Variable>> e :  collector.cache().entrySet()) {
		Set<Variable> freeVars = e.getValue();
		if (freeVars.isEmpty())
			this.cache.put(e.getKey(), new NoVarRecord());
		else 
			this.cache.put(e.getKey(), new MultiVarRecord(freeVars));
	}
}