package jkind.advice;

import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.function.Predicate;

import jkind.engines.invariant.InvariantSet;
import jkind.lustre.Expr;
import jkind.lustre.Node;
import jkind.lustre.Type;
import jkind.lustre.VarDecl;
import jkind.util.Util;

public class Advice {
	private final List<VarDecl> varDecls = new ArrayList<>();
	private final InvariantSet invariants = new InvariantSet();

	public void addVarDecls(List<VarDecl> newVarDecls) {
		varDecls.addAll(newVarDecls);
	}

	public void addInvariant(Expr newInvariant) {
		invariants.add(newInvariant);
	}

	public void addInvariants(List<Expr> newInvariants) {
		invariants.addAll(newInvariants);
	}

	public List<VarDecl> getVarDecls() {
		return varDecls;
	}

	public List<Expr> getInvariants() {
		return invariants.getInvariants();
	}

	public void prune(Node node) {
		Map<String, Type> map = Util.getTypeMap(node);

		Predicate<VarDecl> noLongerExists = vd -> !map.containsKey(vd.id);
		varDecls.removeIf(noLongerExists);

		Predicate<VarDecl> typeChanged = vd -> !baseTypesMatch(map.get(vd.id), vd.type);
		varDecls.removeIf(typeChanged);

		VariableUsageChecker checker = new VariableUsageChecker(varDecls);
		Predicate<Expr> usesUndefinedVariables = inv -> !checker.check(inv);
		invariants.removeIf(usesUndefinedVariables);
	}

	private boolean baseTypesMatch(Type type1, Type type2) {
		return Util.getName(type1).equals(Util.getName(type2));
	}
}

@@ -197,36 +197,134 @@
 re.E
-xpr;%0Aimport jkind.lustre.Nod
+numType;%0Aimport jkind.lustre.Expr;%0Aimport jkind.lustre.NamedType;%0Aimport jkind.lustre.Node;%0Aimport jkind.lustre.SubrangeIntTyp
 e;%0Ai
@@ -1517,24 +1517,23 @@
 %09return 
-Util.get
+getBase
 Name(typ
@@ -1547,29 +1547,447 @@
 als(
-Util.getName(type2));
+getBaseName(type2));%0A%09%7D%0A%0A%09private String getBaseName(Type type) %7B%0A%09%09if (type instanceof EnumType) %7B%0A%09%09%09EnumType et = (EnumType) type;%0A%09%09%09return et.id;%0A%09%09%7D else if (type instanceof NamedType) %7B%0A%09%09%09NamedType nt = (NamedType) type;%0A%09%09%09return nt.name;%0A%09%09%7D else if (type instanceof SubrangeIntType) %7B%0A%09%09%09return NamedType.INT.name;%0A%09%09%7D else %7B%0A%09%09%09throw new IllegalArgumentException(%22Unexpected type: %22%0A%09%09%09%09%09+ type.getClass().getSimpleName());%0A%09%09%7D
 %0A%09%7D%0A

Fix bug in type comparison for advice file