}
if (op==ExprQt.Op.ONE && ok) return ((Expression) visit_qt(ExprQt.Op.COMPREHENSION, xvars, sub)).one();
if (op==ExprQt.Op.LONE && ok) return ((Expression) visit_qt(ExprQt.Op.COMPREHENSION, xvars, sub)).lone();
}
if (op == ExprQt.Op.ONE) {
Formula f1 = (Formula) visit_qt(ExprQt.Op.LONE, xvars, sub);
Formula f2 = (Formula) visit_qt(ExprQt.Op.SOME, xvars, sub);
return f1.and(f2);
}
if (op == ExprQt.Op.LONE) {
QuantifiedFormula p1 = (QuantifiedFormula) visit_qt(ExprQt.Op.ALL, xvars, sub);
QuantifiedFormula p2 = (QuantifiedFormula) visit_qt(ExprQt.Op.ALL, xvars, sub);
Decls s1 = p1.decls(), s2 = p2.decls(), decls = null;
Formula f1 = p1.formula(), f2 = p2.formula();
Formula[] conjuncts = new Formula[s1.size()];
for(int i=0; i<conjuncts.length; i++) {
kodkod.ast.Decl d1 = s1.get(i), d2 = s2.get(i);
conjuncts[i] = d1.variable().eq(d2.variable());
if (decls==null) decls = d1.and(d2); else decls = decls.and(d1).and(d2);
}
return f1.and(f2).implies(Formula.and(conjuncts)).forAll(decls);
}
Decls dd = null;
List<Formula> guards = new ArrayList<Formula>();
for(Decl dep: xvars) {
final Expr dexexpr = addOne(dep.expr);
final Expression dv = cset(dexexpr);
for(ExprHasName dex: dep.names) {
final Variable v = Variable.nary(skolem(dex.label), dex.type().arity());
final kodkod.ast.Decl newd;
env.put((ExprVar)dex, v);
if (dex.type().arity()!=1) {
guards.add(isIn(v, dexexpr));
newd = v.setOf(dv);
} else switch(dexexpr.mult()) {
case SETOF: newd = v.setOf(dv); break;
case SOMEOF: newd = v.someOf(dv); break;
case LONEOF: newd = v.loneOf(dv); break;
default: newd = v.oneOf(dv);
}
if (frame!=null) frame.kv2typepos(v, dex.type(), dex.pos);
if (dd==null) dd = newd; else dd = dd.and(newd);
}
}
final Formula ans = (op==ExprQt.Op.SUM) ? null : cform(sub) ;
final IntExpression ians = (op!=ExprQt.Op.SUM) ? null : cint(sub) ;
for(Decl d: xvars) for(ExprHasName v: d.names) env.remove((ExprVar)v);
if (op==ExprQt.Op.COMPREHENSION) return ans.comprehension(dd); // guards.size()==0, since each var has to be unary
if (op==ExprQt.Op.SUM) return ians.sum(dd); // guards.size()==0, since each var has to be unary
if (op==ExprQt.Op.SOME) {
if (guards.size()==0) return ans.forSome(dd);
guards.add(ans);
return Formula.and(guards).forSome(dd);
} else {
if (guards.size()==0) return ans.forAll(dd);
return Formula.and(guards).implies(ans).forAll(dd);
}
}