for(Sig sig:frame.sigs) for(Field f: sig.getFields()) if (f.label.compareToIgnoreCase("next")==0) {
List<List<PrimSig>> fold = f.type().fold();
if (fold.size()==1) {
List<PrimSig> t = fold.get(0);
if (t.size()==3 && t.get(0).isOne!=null && t.get(1)==t.get(2) && !nexts.containsKey(t.get(1))) {
TupleSet set = frame.eval.evaluate(frame.a2k(t.get(1)));
if (set.size()<=1) continue;
TupleSet next = frame.eval.evaluate(frame.a2k(t.get(0)).join(frame.a2k(f)));
List<Tuple> test = isOrder(next, set);
if (test!=null) nexts.put(t.get(1), test);
} else if (t.size()==2 && t.get(0)==t.get(1) && !nexts.containsKey(t.get(0))) {
TupleSet set = frame.eval.evaluate(frame.a2k(t.get(0)));
if (set.size()<=1) continue;
TupleSet next = frame.eval.evaluate(frame.a2k(f));
List<Tuple> test = isOrder(next, set);
if (test!=null) nexts.put(t.get(1), test);
}
}
}
for(Sig sig:frame.sigs) for(Field f: sig.getFields()) if (f.label.compareToIgnoreCase("prev")==0) {
List<List<PrimSig>> fold = f.type().fold();
if (fold.size()==1) {
List<PrimSig> t = fold.get(0);
if (t.size()==3 && t.get(0).isOne!=null && t.get(1)==t.get(2) && !nexts.containsKey(t.get(1))) {
TupleSet set = frame.eval.evaluate(frame.a2k(t.get(1)));
if (set.size()<=1) continue;
TupleSet next = frame.eval.evaluate(frame.a2k(t.get(0)).join(frame.a2k(f)).transpose());
List<Tuple> test = isOrder(next, set);
if (test!=null) nexts.put(t.get(1), test);
} else if (t.size()==2 && t.get(0)==t.get(1) && !nexts.containsKey(t.get(0))) {
TupleSet set = frame.eval.evaluate(frame.a2k(t.get(0)));
if (set.size()<=1) continue;
TupleSet next = frame.eval.evaluate(frame.a2k(f).transpose());
List<Tuple> test = isOrder(next, set);
if (test!=null) nexts.put(t.get(1), test);
}
}
}
// Assign atom->name and atom->MostSignificantSig
for(Tuple t:frame.eval.evaluate(Relation.INTS)) { frame.atom2sig.put(t.atom(0), SIGINT); }
for(Tuple t:frame.eval.evaluate(KK_SEQIDX)) { frame.atom2sig.put(t.atom(0), SEQIDX); }
for(Tuple t:frame.eval.evaluate(KK_STRING)) { frame.atom2sig.put(t.atom(0), STRING); }
for(Sig sig:frame.sigs) if (sig instanceof PrimSig && !sig.builtin && ((PrimSig)sig).isTopLevel()) rename(frame, (PrimSig)sig, nexts, un);
// These are redundant atoms that were not chosen to be in the final instance
int unused=0;
for(Tuple tuple:frame.eval.evaluate(Relation.UNIV)) {
Object atom = tuple.atom(0);
if (!frame.atom2sig.containsKey(atom)) { frame.atom2name.put(atom, "unused"+unused); unused++; }
}
// Add the skolems
for(int num=skolems.size(), i=0; i<num-2; i=i+3) {
String n = (String) skolems.get(i);
while(n.length()>0 && n.charAt(0)=='$') n=n.substring(1);
Type t = (Type) skolems.get(i+1);
Relation r = (Relation) skolems.get(i+2);
frame.addSkolem(un.make("$"+n), t, r);
}
return;
}
for(PrimSig c: s.children()) rename(frame, c, nexts, un);
String signame = un.make(s.label.startsWith("this/") ? s.label.substring(5) : s.label);
List<Tuple> list = new ArrayList<Tuple>();
for(Tuple t: frame.eval.evaluate(frame.a2k(s))) list.add(t);
List<Tuple> order = nexts.get(s);
if (order!=null && order.size()==list.size() && order.containsAll(list)) { list=order; }
int i = 0;
for(Tuple t: list) {
if (frame.atom2sig.containsKey(t.atom(0))) continue; // This means one of the subsig has already claimed this atom.
String x = signame + "$" + i;
i++;
frame.atom2sig.put(t.atom(0), s);
frame.atom2name.put(t.atom(0), x);
ExprVar v = ExprVar.make(null, x, s.type());
TupleSet ts = t.universe().factory().range(t, t);
Relation r = Relation.unary(x);
frame.eval.instance().add(r, ts);
frame.a2k.put(v, r);
frame.atoms.add(v);
}