Support #Forall _/ #Exists _
@@ -995,7 +995,7 @@ public class ModuleToKORE {
private KLabel computePolyKLabel(KApply k) {
String labelName = k.klabel().name();
- List<Set<Integer>> poly = polyKLabels.get(labelName);
+ List<Set<Integer>> poly = new ArrayList<>(polyKLabels.get(labelName));
if (mlBinders.contains(labelName)) { // ML binders are not parametric in the variable so we remove it
poly.remove(0);
}
@@ -1204,6 +1204,30 @@ public class ModuleToKORE {
@Override
public String toString() { return sb.toString(); }
+ public Set<K> collectAnonymousVariables(K k){
+ Set <K> anonymousVariables = new HashSet<>();
+ new VisitK() {
+ @Override
+ public void apply(KApply k) {
+ if (mlBinders.contains(k.klabel().name()) && k.items().get(0).att().contains("anonymous")){
+ throw KEMException.internalError("Nested quantifier over anonymous variables.");
+ }
+ for (K item : k.items()) {
+ apply(item);
+ }
+ }
+
+ @Override
+ public void apply(KVariable k) {
+ if (k.att().contains("anonymous")) {
+ anonymousVariables.add(k);
+ }
+ }
+
+ }.apply(k);
+ return anonymousVariables;
+ }
+
public void convert(K k) {
new VisitK() {
@Override
@@ -1215,14 +1239,32 @@ public class ModuleToKORE {
if (polyKLabels.containsKey(k.klabel().name())) {
label = computePolyKLabel(k);
}
+ String conn = "";
+ if (mlBinders.contains(k.klabel().name()) && k.items().get(0).att().contains("anonymous")){
+ // Handle #Forall _ / #Exists _
+ Set<K> anonymousVariables = collectAnonymousVariables(k.items().get(1));
+
+ // Quantify over all anonymous variables.
+ for (K variable : anonymousVariables) {
+ sb.append(conn);
+ convert(label, false);
+ sb.append("(");
+ apply(variable);
+ conn = ",";
+ }
+
+ // We assume that mlBinder only has two children.
+ sb.append(conn);
+ apply(k.items().get(1));
+ } else {
convert(label, false);
sb.append("(");
- String conn = "";
for (K item : k.items()) {
sb.append(conn);
apply(item);
conn = ",";
}
+ }
sb.append(")");
}
