import kodkod.util.collections.CacheSet; //导入依赖的package包/类
/**
 * Constructs a new concurrent memory handler for the given info and 
 * options, set to translate the thread with id 0.
 * @effects this.info' = info and this.options' = options and this.thread' = 0 and 
 * this.factory' = new ExpressionFactory(info, options) no this.actions'
 * and no this.guards'
 */
public ConcurrentMemoryHandler(WalaInformation info, Options options) {
	this.factory = new ConcurrentFactory(new ExpressionFactory(info, options));
	
	this.insts = new CacheSet<InlinedInstruction>();
	this.guards = new LinkedHashMap<InlinedInstruction, Formula>();
	for(CGNode thread : info.threads()) { 
		final WalaConcurrentInformation tInfo = info.concurrentInformation(thread);
		insts.addAll( tInfo.actions() );
		guards.put( tInfo.start(), Formula.TRUE);
		guards.put( tInfo.end(), Formula.TRUE);
	}	
	this.locations = new LinkedHashMap<InlinedInstruction, Expression>();
	this.monitors = new LinkedHashMap<InlinedInstruction, Expression>();
	this.reads = new LinkedHashMap<InlinedInstruction, Relation>();
	this.writes = new LinkedHashMap<InlinedInstruction, Expression>();
}
 

import kodkod.util.collections.CacheSet; //导入依赖的package包/类
PartialCannonicalizer() { 
	exprs = new CacheSet<PartialCannonicalizer.Holder<Expression>>();
	formulas = new CacheSet<PartialCannonicalizer.Holder<Formula>>();
	intExprs = new CacheSet<PartialCannonicalizer.Holder<IntExpression>>();
}
 

import kodkod.util.collections.CacheSet; //导入依赖的package包/类
/**
 * Returns the cache for gates with the given operator.
 * 
 * @requires op in AND + OR + ITE
 * @return cache[op.ordinal]
 */
private CacheSet<BooleanFormula> opCache(Operator op) {
	return cache[op.ordinal];
}
 

import kodkod.util.collections.CacheSet; //导入依赖的package包/类
/**
 * Returns the cache for gates with the given operator.
 * @requires op in AND + OR + ITE
 * @return cache[op.ordinal]
 */
private CacheSet<BooleanFormula> opCache(Operator op) {
	return cache[op.ordinal];
}