本文整理汇总了Java中kodkod.ast.visitor.AbstractReplacer类的典型用法代码示例。如果您正苦于以下问题:Java AbstractReplacer类的具体用法?Java AbstractReplacer怎么用?Java AbstractReplacer使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
AbstractReplacer类属于kodkod.ast.visitor包,在下文中一共展示了AbstractReplacer类的5个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Java代码示例。
示例1: inlinePredicates
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);
}
开发者ID:AlloyTools,项目名称:org.alloytools.alloy,代码行数:27,代码来源:Translator.java
示例2: inlinePredicates
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);
}
开发者ID:ModelWriter,项目名称:Tarski,代码行数:49,代码来源:Translator.java
示例3: inlinePredicates
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));
}
开发者ID:emina,项目名称:kodkod,代码行数:21,代码来源:Translator.java
示例4: makeReadable
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));
}
开发者ID:wala,项目名称:MemSAT,代码行数:34,代码来源:AngelicTests.java
示例5: solveNext
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;
}
开发者ID:AlloyTools,项目名称:org.alloytools.alloy,代码行数:48,代码来源:HOLTranslationNew.java
注:本文中的kodkod.ast.visitor.AbstractReplacer类示例整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论