Skip to content

Commit

Permalink
fixed skolem labels
Browse files Browse the repository at this point in the history
  • Loading branch information
nmacedo committed Jun 3, 2024
1 parent f0973ee commit 9990d5b
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,7 @@ private AlloySet makeSet(String label, boolean isPrivate, boolean isMeta, boolea
* Create a new AlloyRelation whose label is unambiguous with any existing one.
*/
private AlloyRelation makeRel(String label, boolean isPrivate, boolean isMeta, boolean isVar, boolean isSkolem, List<AlloyType> types) {
label = Util.tail(label);
while (label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label))
label = label + "'";
while (true) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -821,7 +821,8 @@ public static boolean onMac() {
/** Returns the substring after the last "/" */
public static String tail(String string) {
int i = string.lastIndexOf('/');
return (i < 0) ? string : string.substring(i + 1);
String label = (i < 0) ? string : string.substring(i + 1);
return string.charAt(0) == '$' && label.charAt(0) != '$' ? "$" + label : label;
}

/** Returns the substring without "this/". May not start with "this/" in skolems. */
Expand Down

0 comments on commit 9990d5b

Please sign in to comment.