Add workaround for Kind 2 forward references issue

jkind-api/src/jkind/api/Kind2Api.java

@@ -7,6 +7,8 @@
 
 import jkind.JKindException;
 import jkind.api.results.JKindResult;
+import jkind.api.workarounds.WorkaroundKind2ForwardReference;
+import jkind.api.workarounds.WorkaroundKind2RecordAccess;
 import jkind.api.xml.XmlParseThread;
 import jkind.lustre.Program;
 
@@ -32,6 +34,7 @@ public class Kind2Api extends KindApi {
 	@Override
 	public void execute(Program program, JKindResult result, IProgressMonitor monitor) {
 		program = WorkaroundKind2RecordAccess.program(program);
+		program = WorkaroundKind2ForwardReference.program(program);
 		execute(program.toString(), result, monitor);
 	}
 

jkind-api/src/jkind/api/workarounds/DependencyMap.java

@@ -0,0 +1,49 @@
+package jkind.api.workarounds;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+public class DependencyMap<T> {
+	private Map<String, T> valueMap = new LinkedHashMap<>();
+	private Map<String, Set<String>> dependencyMap = new HashMap<>();
+
+	public void put(String id, T value, Set<String> dependencies) {
+		valueMap.put(id, value);
+		dependencyMap.put(id, dependencies);
+	}
+
+	public List<T> getSortedValues() {
+		List<T> result = new ArrayList<>();
+		for (String id : getSortedIds()) {
+			result.add(valueMap.get(id));
+		}
+		return result;
+	}
+
+	private List<String> getSortedIds() {
+		List<String> ordered = new ArrayList<>();
+		for (String id : valueMap.keySet()) {
+			addToSortedIdsList(id, ordered);
+		}
+		return ordered;
+	}
+
+	private void addToSortedIdsList(String id, List<String> sorted) {
+		if (sorted.contains(id)) {
+			return;
+		}
+
+		Set<String> dependencies = new HashSet<>(dependencyMap.get(id));
+		dependencies.removeAll(sorted);
+		for (String dependency : dependencies) {
+			addToSortedIdsList(dependency, sorted);
+		}
+
+		sorted.add(id);
+	}
+}

jkind-api/src/jkind/api/workarounds/WorkaroundKind2ForwardReference.java

@@ -0,0 +1,92 @@
+package jkind.api.workarounds;
+
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+import jkind.lustre.Constant;
+import jkind.lustre.Expr;
+import jkind.lustre.IdExpr;
+import jkind.lustre.NamedType;
+import jkind.lustre.Node;
+import jkind.lustre.NodeCallExpr;
+import jkind.lustre.Program;
+import jkind.lustre.Type;
+import jkind.lustre.TypeDef;
+import jkind.lustre.builders.ProgramBuilder;
+import jkind.lustre.visitors.AstIterVisitor;
+import jkind.lustre.visitors.ExprIterVisitor;
+import jkind.lustre.visitors.TypeIterVisitor;
+
+public class WorkaroundKind2ForwardReference {
+	public static Program program(Program program) {
+		ProgramBuilder bulider = new ProgramBuilder(program);
+		bulider.clearTypes().addTypes(getSortedTypes(program.types));
+		bulider.clearConstants().addConstants(getSortedConstants(program.constants));
+		bulider.clearNodes().addNodes(getSortedNodes(program.nodes));
+		return bulider.build();
+	}
+
+	private static List<TypeDef> getSortedTypes(List<TypeDef> types) {
+		DependencyMap<TypeDef> depMap = new DependencyMap<>();
+		for (TypeDef type : types) {
+			depMap.put(type.id, type, getTypeDependencies(type.type));
+		}
+		return depMap.getSortedValues();
+	}
+
+	private static Set<String> getTypeDependencies(Type type) {
+		final Set<String> dependencies = new HashSet<>();
+		type.accept(new TypeIterVisitor() {
+			@Override
+			public Void visit(NamedType e) {
+				if (!e.isBuiltin()) {
+					dependencies.add(e.name);
+				}
+				return null;
+			}
+		});
+		return dependencies;
+	}
+
+	private static Collection<Constant> getSortedConstants(List<Constant> constants) {
+		DependencyMap<Constant> depMap = new DependencyMap<>();
+		for (Constant constant : constants) {
+			depMap.put(constant.id, constant, getConstantDependencies(constant.expr));
+		}
+		return depMap.getSortedValues();
+	}
+
+	private static Set<String> getConstantDependencies(Expr expr) {
+		final Set<String> dependencies = new HashSet<>();
+		expr.accept(new ExprIterVisitor() {
+			@Override
+			public Void visit(IdExpr e) {
+				dependencies.add(e.id);
+				return null;
+			}
+		});
+		return dependencies;
+	}
+
+	private static Collection<Node> getSortedNodes(List<Node> nodes) {
+		DependencyMap<Node> depMap = new DependencyMap<>();
+		for (Node node : nodes) {
+			depMap.put(node.id, node, getNodeDependencies(node));
+		}
+		return depMap.getSortedValues();
+	}
+
+	private static Set<String> getNodeDependencies(Node node) {
+		final Set<String> dependencies = new HashSet<>();
+		node.accept(new AstIterVisitor() {
+			@Override
+			public Void visit(NodeCallExpr e) {
+				dependencies.add(e.node);
+				return null;
+			}
+		});
+		return dependencies;
+	}
+}

jkind-api/src/jkind/api/WorkaroundKind2RecordAccess.java → jkind-api/src/jkind/api/workarounds/WorkaroundKind2RecordAccess.java

@@ -1,4 +1,4 @@
-package jkind.api;
+package jkind.api.workarounds;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -31,6 +31,8 @@ public static Program program(Program program) {
 
 	@Override
 	public Node visit(Node e) {
+		newLocals.clear();
+		newEquations.clear();
 		NodeBuilder builder = new NodeBuilder(super.visit(e));
 		builder.addLocals(newLocals);
 		builder.addEquations(newEquations);