本文整理汇总了Java中kodkod.ast.IntComparisonFormula类的典型用法代码示例。如果您正苦于以下问题：Java IntComparisonFormula类的具体用法？Java IntComparisonFormula怎么用？Java IntComparisonFormula使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
IntComparisonFormula类属于kodkod.ast包，在下文中一共展示了IntComparisonFormula类的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的Java代码示例。
示例1: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Calls lookup(intComp) and returns the cached value, if any.
* If a translation has not been cached, translates the formula,
* calls cache(...) on it and returns it.
*
* This is the only place where <code>Int</code>s are turned into
* formulas, so that's where the overflow circuits of individual
* <code>Int</code>s are built into the translated formula.
*
* @return let t = lookup(intComp) | some t => t,
* cache(intComp, intComp.left.accept(this) intComp.op intComp.right.accept(this))
*/
public final BooleanValue visit(IntComparisonFormula intComp) {
BooleanValue ret = lookup(intComp);
if (ret!=null) return ret;
final Int left = intComp.left().accept(this);
final Int right = intComp.right().accept(this);
switch(intComp.op()) {
case EQ : ret = left.eq(right, env); break;
case NEQ : ret = left.neq(right, env); break;
case LT : ret = left.lt(right, env); break;
case LTE : ret = left.lte(right, env); break;
case GT : ret = left.gt(right, env); break;
case GTE : ret = left.gte(right, env); break;
default:
throw new IllegalArgumentException("Unknown operator: " + intComp.op());
}
return cache(intComp, ret);
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:30，代码来源:FOL2BoolTranslator.java
示例2: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Calls lookup(intComp) and returns the cached value, if any.
* If a translation has not been cached, translates the formula,
* calls cache(...) on it and returns it.
* @return let t = lookup(intComp) | some t => t,
* cache(intComp, intComp.left.accept(this) intComp.op intComp.right.accept(this))
*/
public final BooleanValue visit(IntComparisonFormula intComp) {
BooleanValue ret = lookup(intComp);
if (ret!=null) return ret;
final Int left = intComp.left().accept(this);
final Int right = intComp.right().accept(this);
switch(intComp.op()) {
case EQ : ret = left.eq(right); break;
case LT : ret = left.lt(right); break;
case LTE : ret = left.lte(right); break;
case GT : ret = left.gt(right); break;
case GTE : ret = left.gte(right); break;
default:
throw new IllegalArgumentException("Unknown operator: " + intComp.op());
}
return cache(intComp, ret);
}
开发者ID:emina，项目名称:kodkod，代码行数:24，代码来源:FOL2BoolTranslator.java
示例3: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
public Formula visit(IntComparisonFormula formula) {
Formula ret = lookup(formula);
if (ret!=null) return ret;
final IntCompOperator op = formula.op();
final IntExpression left = formula.left().accept(this);
final IntExpression right = formula.right().accept(this);
if (left==right) return cache(formula,Formula.TRUE);
final int hash = hash(op, left, right);
for(Iterator<PartialCannonicalizer.Holder<Formula>> itr = formulas.get(hash); itr.hasNext(); ) {
final Formula next = itr.next().obj;
if (next instanceof IntComparisonFormula) {
final IntComparisonFormula hit = (IntComparisonFormula) next;
if (hit.op()==op && hit.left()==left && hit.right()==right) {
return cache(formula, hit);
}
}
}
ret = left==formula.left()&&right==formula.right() ? formula : left.compare(op, right);
formulas.add(new PartialCannonicalizer.Holder<Formula>(ret, hash));
return cache(formula,ret);
}
开发者ID:wala，项目名称:MemSAT，代码行数:26，代码来源:PartialCannonicalizer.java
示例4: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* 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(delegate) op
* intComp.right.accept(delegate) }
*/
public Formula visit(IntComparisonFormula intComp) {
Formula ret = lookup(intComp);
if (ret != null)
return ret;
final IntExpression left = intComp.left().accept(delegate);
final IntExpression right = intComp.right().accept(delegate);
ret = (left == intComp.left() && right == intComp.right()) ? intComp : left.compare(intComp.op(), right);
return cache(intComp, ret);
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:20，代码来源:AbstractReplacer.java
示例5: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Visits the children of the given integer comparison formula if
* this.visited(intComp) returns false. Otherwise does nothing.
*
* @ensures intComp.left.accept(this) && intComp.right.accept(this)
*/
public void visit(IntComparisonFormula intComp) {
if (visited(intComp))
return;
intComp.left().accept(this);
intComp.right().accept(this);
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:13，代码来源:AbstractVoidVisitor.java
示例6: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Calls lookup(intComp) and returns the cached value, if any. If no cached
* value exists, visits each child, caches the union of the children's
* return values and returns it.
*
* @return let x = lookup(intComp) | x != null => x, cache(intComp,
* intComp.left.accept(this) + intComp.right.accept(this))
*/
public Set<T> visit(IntComparisonFormula intComp) {
Set<T> ret = lookup(intComp);
if (ret != null)
return ret;
ret = newSet();
ret.addAll(intComp.left().accept(this));
ret.addAll(intComp.right().accept(this));
return cache(intComp, ret);
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:18，代码来源:AbstractCollector.java
示例7: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/** @see #visitFormula(Formula) */
public final void visit(IntComparisonFormula cf) {
if (visited(cf))
return;
if (!negated) {
addConjunct(cf);
} else {
switch (cf.op()) {
case GT :
addConjunct(cf.left().lte(cf.right()), false, cf);
hasChanged = true;
break;
case GTE :
addConjunct(cf.left().lt(cf.right()), false, cf);
hasChanged = true;
break;
case LT :
addConjunct(cf.left().gte(cf.right()), false, cf);
hasChanged = true;
break;
case LTE :
addConjunct(cf.left().gt(cf.right()), false, cf);
hasChanged = true;
break;
case EQ :
addConjunct(cf.left().neq(cf.right()), false, cf);
hasChanged = true;
break;
case NEQ :
addConjunct(cf.left().eq(cf.right()), false, cf);
hasChanged = true;
break;
default :
addConjunct(cf);
}
}
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:38，代码来源:FullNegationPropagator.java
示例8: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Calls super.visit(icf) after disabling skolemization and returns the
* result.
*
* @return super.visit(icf)
**/
public final Formula visit(IntComparisonFormula icf) {
final int oldDepth = skolemDepth;
skolemDepth = -1; // cannot skolemize inside an int comparison formula
final Formula ret = super.visit(icf);
skolemDepth = oldDepth;
return source(ret, icf);
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:14，代码来源:Skolemizer.java
示例9: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Calls lookup(intComp) and returns the cached value, if any. If a
* translation has not been cached, translates the formula, calls cache(...)
* on it and returns it. This is the only place where <code>Int</code>s are
* turned into formulas, so that's where the overflow circuits of individual
* <code>Int</code>s are built into the translated formula.
*
* @return let t = lookup(intComp) | some t => t, cache(intComp,
* intComp.left.accept(this) intComp.op intComp.right.accept(this))
*/
public final BooleanValue visit(IntComparisonFormula intComp) {
BooleanValue ret = lookup(intComp);
if (ret != null)
return ret;
final Int left = intComp.left().accept(this);
final Int right = intComp.right().accept(this);
switch (intComp.op()) {
case EQ :
ret = left.eq(right, env);
break;
case NEQ :
ret = left.neq(right, env);
break;
case LT :
ret = left.lt(right, env);
break;
case LTE :
ret = left.lte(right, env);
break;
case GT :
ret = left.gt(right, env);
break;
case GTE :
ret = left.gte(right, env);
break;
default :
throw new IllegalArgumentException("Unknown operator: " + intComp.op());
}
return cache(intComp, ret);
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:41，代码来源:FOL2BoolTranslator.java
示例10: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(IntComparisonFormula x) {
String newname = makename(x);
if (newname == null)
return;
String left = make(x.left());
String right = make(x.right());
switch (x.op()) {
case NEQ :
file.printf("Formula %s=%s.neq(%s);%n", newname, left, right);
break;
case EQ :
file.printf("Formula %s=%s.eq(%s);%n", newname, left, right);
break;
case GT :
file.printf("Formula %s=%s.gt(%s);%n", newname, left, right);
break;
case GTE :
file.printf("Formula %s=%s.gte(%s);%n", newname, left, right);
break;
case LT :
file.printf("Formula %s=%s.lt(%s);%n", newname, left, right);
break;
case LTE :
file.printf("Formula %s=%s.lte(%s);%n", newname, left, right);
break;
default :
throw new RuntimeException("Unknown kodkod operator \"" + x.op() + "\" encountered");
}
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:31，代码来源:TranslateKodkodToJava.java
示例11: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(IntComparisonFormula x) {
String newname=makename(x); if (newname==null) return;
String left=make(x.left());
String right=make(x.right());
switch(x.op()) {
case NEQ: file.printf("Formula %s=%s.neq(%s);%n", newname, left, right); break;
case EQ: file.printf("Formula %s=%s.eq(%s);%n", newname, left, right); break;
case GT: file.printf("Formula %s=%s.gt(%s);%n", newname, left, right); break;
case GTE: file.printf("Formula %s=%s.gte(%s);%n", newname, left, right); break;
case LT: file.printf("Formula %s=%s.lt(%s);%n", newname, left, right); break;
case LTE: file.printf("Formula %s=%s.lte(%s);%n", newname, left, right); break;
default: throw new RuntimeException("Unknown kodkod operator \""+x.op()+"\" encountered");
}
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:16，代码来源:TranslateKodkodToJava.java
示例12: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* 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);
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:18，代码来源:AbstractReplacer.java
示例13: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Calls lookup(intComp) and returns the cached value, if any.
* If no cached value exists, visits each child, caches the
* union of the children's return values and returns it.
* @return let x = lookup(intComp) |
* x != null => x,
* cache(intComp, intComp.left.accept(this) + intComp.right.accept(this))
*/
public Set<T> visit(IntComparisonFormula intComp) {
Set<T> ret = lookup(intComp);
if (ret!=null) return ret;
ret = newSet();
ret.addAll(intComp.left().accept(this));
ret.addAll(intComp.right().accept(this));
return cache(intComp, ret);
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:17，代码来源:AbstractCollector.java
示例14: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/** @see #visitFormula(Formula) */
public final void visit(IntComparisonFormula cf) {
if (visited(cf)) return;
if (!negated) {
addConjunct(cf);
} else {
switch (cf.op()) {
case GT:
addConjunct(cf.left().lte(cf.right()), false, cf);
hasChanged = true;
break;
case GTE:
addConjunct(cf.left().lt(cf.right()), false, cf);
hasChanged = true;
break;
case LT:
addConjunct(cf.left().gte(cf.right()), false, cf);
hasChanged = true;
break;
case LTE:
addConjunct(cf.left().gt(cf.right()), false, cf);
hasChanged = true;
break;
case EQ:
addConjunct(cf.left().neq(cf.right()), false, cf);
hasChanged = true;
break;
case NEQ:
addConjunct(cf.left().eq(cf.right()), false, cf);
hasChanged = true;
break;
default:
addConjunct(cf);
}
}
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:37，代码来源:FullNegationPropagator.java
示例15: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/** @see #visitFormula(Formula) */
public final Formula visit(IntComparisonFormula cf) {
//if (visited(cf)) return;
IntExpression lh = cf.left().accept(this);
IntExpression rh = cf.right().accept(this);
if (!negated) {
if (lh == cf.left() && rh == cf.right()) {
return addMapping(cf, cf);
} else {
return addMapping(lh.compare(cf.op(), rh), cf);
}
} else {
switch (cf.op()) {
case GT:
return addMapping(lh.lte(rh), cf);
case GTE:
return addMapping(lh.lt(rh), cf);
case LT:
return addMapping(lh.gte(rh), cf);
case LTE:
return addMapping(lh.gt(rh), cf);
case EQ:
return addMapping(lh.neq(rh), cf);
case NEQ:
return addMapping(lh.eq(rh), cf);
default:
return addMapping(cf, cf);
}
}
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:31，代码来源:NNFConverter.java
示例16: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/**
* Calls super.visit(icf) after disabling skolemization and returns the result.
* @return super.visit(icf)
**/
public final Formula visit(IntComparisonFormula icf) {
final int oldDepth = skolemDepth;
skolemDepth = -1; // cannot skolemize inside an int comparison formula
final Formula ret = super.visit(icf);
skolemDepth = oldDepth;
return source(ret,icf);
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:12，代码来源:Skolemizer.java
示例17: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
/** @effects this.tokens' = concat[ this.tokens, tokenize[node.left], node.op, tokenize[node.right] */
public void visit(IntComparisonFormula node) {
if (displayed(node)) return;
final boolean oldTop = notTop();
visitChild(node.left(), parenthesize(node.left()));
infix(node.op());
visitChild(node.right(), parenthesize(node.right()));
top = oldTop;
}
开发者ID:wala，项目名称:MemSAT，代码行数:10，代码来源:PrettyPrinter.java
示例18: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
public Formula visit(IntComparisonFormula formula) {
Formula ret = lookup(formula);
if (ret!=null) return ret;
final IntCompOperator op = formula.op();
final IntExpression left = formula.left().accept(this);
final IntExpression right = formula.right().accept(this);
if (left==right) return cache(formula,Formula.TRUE);
ret = left==formula.left()&&right==formula.right() ? formula : left.compare(op, right);
return cache(formula,ret);
}
开发者ID:wala，项目名称:MemSAT，代码行数:14，代码来源:Simplifier.java
示例19: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
@Override
public F visit(IntComparisonFormula intComp) {
start(intComp);
return end(intComp, visitor.visit(intComp));
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:6，代码来源:AspectReturnVisitor.java
示例20: visit
import kodkod.ast.IntComparisonFormula; //导入依赖的package包/类
public void visit(IntComparisonFormula intComp) {
if (visited(intComp))
return;
relevant.add(intComp);
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:6，代码来源:TrivialProof.java
注：本文中的kodkod.ast.IntComparisonFormula类示例整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。 |
客服电话
APP下载
官方微信
请发表评论