import kodkod.ast.Relation; //導入方法依賴的package包/類

/**

* Calls lookup(pred) 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 { p: RelationPredicate | p.name = pred.name && p.relation = pred.relation.accept(this) &&

* p.name = FUNCTION => p.targetMult = pred.targetMult &&

* p.domain = pred.domain.accept(this) &&

* p.range = pred.range.accept(this),

* p.name = TOTAL_ORDERING => p.ordered = pred.ordered.accept(this) &&

* p.first = pred.first.accept(this) &&

* p.last = pred.last.accept(this) }

*/

public Formula visit(RelationPredicate pred) {

Formula ret = lookup(pred);

if (ret!=null) return ret;

final Relation r = (Relation)pred.relation().accept(this);

switch(pred.name()) {

case ACYCLIC :

ret = (r==pred.relation()) ? pred : r.acyclic();

break;

case FUNCTION :

final RelationPredicate.Function fp = (RelationPredicate.Function) pred;

final Expression domain = fp.domain().accept(this);

final Expression range = fp.range().accept(this);

ret = (r==fp.relation() && domain==fp.domain() && range==fp.range()) ?

fp :

(fp.targetMult()==Multiplicity.ONE ? r.function(domain, range) : r.partialFunction(domain,range));

break;

case TOTAL_ORDERING :

final RelationPredicate.TotalOrdering tp = (RelationPredicate.TotalOrdering) pred;

final Relation ordered = (Relation) tp.ordered().accept(this);

final Relation first = (Relation)tp.first().accept(this);

final Relation last = (Relation)tp.last().accept(this);

ret = (r==tp.relation() && ordered==tp.ordered() && first==tp.first() && last==tp.last()) ?

tp : r.totalOrder(ordered, first, last);

break;

default :

throw new IllegalArgumentException("unknown relation predicate: " + pred.name());

}

return cache(pred,ret);

}