Use graph based representation for boolean invariants

src/jkind/invariant/Candidate.java

@@ -0,0 +1,51 @@
+package jkind.invariant;
+
+import java.math.BigInteger;
+
+import jkind.sexp.Cons;
+import jkind.sexp.Sexp;
+import jkind.sexp.Symbol;
+import jkind.solvers.BoolValue;
+import jkind.solvers.Model;
+
+public class Candidate {
+	final public String id;
+	final public Sexp sexp;
+
+	public Candidate(String id, Sexp sexp) {
+		this.id = id;
+		this.sexp = sexp;
+	}
+
+	public boolean isTrue(Model model, BigInteger k) {
+		BoolValue bv = (BoolValue) model.getFunctionValue(id, k);
+		return bv.getBool();
+	}
+
+	public Sexp getDeclaration() {
+		Sexp type = new Cons("->", new Symbol("nat"), new Symbol("bool"));
+		return new Cons("define", new Symbol(id), new Symbol("::"), type);
+	}
+
+	public Sexp getDefinition() {
+		return new Cons("assert", new Cons("=", new Symbol(id), sexp));
+	}
+
+	public Sexp index(Sexp index, boolean pure) {
+		if (pure) {
+			return new Cons(sexp, index);
+		} else {
+			return new Cons(id, index);
+		}
+	}
+
+	@Override
+	public String toString() {
+		return id;
+	}
+
+	final public static Candidate TRUE = new Candidate("canTrue", new Cons("lambda", new Cons("i",
+			new Symbol("::"), new Symbol("nat")), new Symbol("true")));
+	final public static Candidate FALSE = new Candidate("canFalse", new Cons("lambda", new Cons("i",
+			new Symbol("::"), new Symbol("nat")), new Symbol("false")));
+}

src/jkind/invariant/CandidateGenerator.java

@@ -0,0 +1,60 @@
+package jkind.invariant;
+
+import java.math.BigInteger;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+
+import jkind.lustre.SubrangeIntType;
+import jkind.lustre.Type;
+import jkind.sexp.Cons;
+import jkind.sexp.Sexp;
+import jkind.sexp.Symbol;
+import jkind.translation.Util;
+
+public class CandidateGenerator {
+	private Map<String, Type> typeMap;
+	private Sexp i;
+	private List<Candidate> candidates;
+	private int candidateIndex;
+
+	public CandidateGenerator(Map<String, Type> typeMap, Sexp i) {
+		this.typeMap = typeMap;
+		this.i = i;
+	}
+
+	public List<Candidate> generate() {
+		candidates = new ArrayList<Candidate>();
+		candidateIndex = 0;
+
+		candidates.add(Candidate.TRUE);
+		candidates.add(Candidate.FALSE);
+
+		for (String id : typeMap.keySet()) {
+			Type type = typeMap.get(id);
+			if (type == Type.BOOL) {
+				Sexp s = new Cons("$" + id, i);
+				addCandidate(s);
+				// addCandidate(new Cons("not", s));
+			} else if (type instanceof SubrangeIntType) {
+				SubrangeIntType subrange = (SubrangeIntType) type;
+				addCandidate(Util.subrangeConstraint(id, i, subrange));
+
+				Sexp s = new Cons("$" + id, i);
+				for (BigInteger r = subrange.low; r.compareTo(subrange.high) <= 0; r = r.add(BigInteger.ONE)) {
+					addCandidate(new Cons("=", s, Sexp.fromBigInt(r)));
+					// addCandidate(new Cons("/=", s, Sexp.fromBigInt(r)));
+				}
+			}
+		}
+
+		return candidates;
+	}
+
+	private void addCandidate(Sexp s) {
+		Sexp iType = new Cons(i, new Symbol("::"), new Symbol("nat"));
+		Candidate candidate = new Candidate("can" + candidateIndex, new Cons("lambda", iType, s));
+		candidateIndex++;
+		candidates.add(candidate);
+	}
+}

src/jkind/invariant/Edge.java

@@ -0,0 +1,25 @@
+package jkind.invariant;
+
+import jkind.sexp.Cons;
+import jkind.sexp.Sexp;
+
+public class Edge {
+	final public Node source;
+	final public Node destination;
+
+	public Edge(Node source, Node destination) {
+		this.source = source;
+		this.destination = destination;
+	}
+
+	public Sexp toInvariant(Sexp index, boolean pure) {
+		Sexp sRep = source.getRepresentative().index(index, pure);
+		Sexp dRep = destination.getRepresentative().index(index, pure);
+		return new Cons("=>", sRep, dRep);
+	}
+
+	@Override
+	public String toString() {
+		return source + " -> " + destination;
+	}
+}

src/jkind/invariant/Graph.java

@@ -0,0 +1,216 @@
+package jkind.invariant;
+
+import java.math.BigInteger;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
+
+import jkind.sexp.Cons;
+import jkind.sexp.Sexp;
+import jkind.sexp.Symbol;
+import jkind.solvers.Model;
+
+public class Graph {
+	private List<Node> nodes;
+	private Map<Node, Set<Node>> incoming;
+	private Map<Node, Set<Node>> outgoing;
+
+	public Graph(List<Candidate> candidates) {
+		this.nodes = new ArrayList<Node>();
+		nodes.add(new Node(candidates));
+		this.incoming = new HashMap<Node, Set<Node>>();
+		this.outgoing = new HashMap<Node, Set<Node>>();
+	}
+
+	public int size() {
+		return nodes.size();
+	}
+
+	public boolean isTrivial() {
+		return nodes.isEmpty() || (nodes.size() == 1 && nodes.get(0).isSingleton());
+	}
+
+	private void addEdge(Node source, Node destination) {
+		safeGet(outgoing, source).add(destination);
+		safeGet(incoming, destination).add(source);
+	}
+
+	private Set<Node> safeGet(Map<Node, Set<Node>> map, Node node) {
+		Set<Node> result = map.get(node);
+		if (result == null) {
+			result = new HashSet<Node>();
+			map.put(node, result);
+		}
+		return result;
+	}
+
+	private Set<Edge> getEdges() {
+		Set<Edge> edges = new HashSet<Edge>();
+		for (Entry<Node, Set<Node>> entry : outgoing.entrySet()) {
+			Node source = entry.getKey();
+			for (Node destination : entry.getValue()) {
+				edges.add(new Edge(source, destination));
+			}
+		}
+		return edges;
+	}
+
+	private void setEdges(List<Edge> edges) {
+		incoming.clear();
+		outgoing.clear();
+		for (Edge edge : edges) {
+			addEdge(edge.source, edge.destination);
+		}
+	}
+
+	public Sexp toInvariant(Sexp index) {
+		return toInvariant(index, false);
+	}
+
+	public Sexp toFinalInvariant(Sexp index) {
+		removeTrivialInvariants();
+		if (isTrivial()) {
+			return new Symbol("true");
+		} else {
+			return toInvariant(index, true);
+		}
+	}
+
+	@Override
+	public String toString() {
+		StringBuilder sb = new StringBuilder();
+		sb.append("digraph {\n");
+		for (Node node : nodes) {
+			sb.append("  \"" + node + "\";\n");
+		}
+		for (Edge edge : getEdges()) {
+			sb.append("  \"" + edge.source + "\" -> \"" + edge.destination + "\";\n");
+		}
+		sb.append("}");
+		return sb.toString();
+	}
+
+	private void removeTrivialInvariants() {
+		for (Node node : nodes) {
+			if (node.getRepresentative() == Candidate.TRUE) {
+				Set<Node> in = safeGet(incoming, node);
+				for (Node other : in) {
+					safeGet(outgoing, other).remove(node);
+				}
+				in.clear();
+			} else if (node.getRepresentative() == Candidate.FALSE) {
+				Set<Node> out = safeGet(outgoing, node);
+				for (Node other : out) {
+					safeGet(incoming, other).remove(node);
+				}
+				out.clear();
+			}
+		}
+
+		removeUselessNodes();
+	}
+
+	private Sexp toInvariant(Sexp index, boolean pure) {
+		List<Sexp> conjuncts = new ArrayList<Sexp>();
+		for (Node node : nodes) {
+			conjuncts.addAll(node.toInvariants(index, pure));
+		}
+		for (Edge edge : getEdges()) {
+			conjuncts.add(edge.toInvariant(index, pure));
+		}
+		return new Cons("and", conjuncts);
+	}
+
+	public void refine(Model model, BigInteger k) {
+		splitNodes(model, k);
+		removeEmptyNodes();
+		removeUselessNodes();
+	}
+
+	private void splitNodes(Model model, BigInteger k) {
+		List<Node> newNodes = new ArrayList<Node>();
+		List<Edge> newEdges = new ArrayList<Edge>();
+		Map<Node, List<Node>> chains = new HashMap<Node, List<Node>>();
+
+		// Split nodes into chains
+		for (Node curr : nodes) {
+			List<Node> chain = curr.split(model, k);
+			chains.put(curr, chain);
+			newNodes.addAll(chain);
+			if (!chain.get(0).isEmpty() && !chain.get(1).isEmpty()) {
+				newEdges.add(new Edge(chain.get(0), chain.get(1)));
+			}
+		}
+
+		// Join chains based on previous edges
+		for (Edge edge : getEdges()) {
+			List<Node> sourceChain = chains.get(edge.source);
+			List<Node> destinationChain = chains.get(edge.destination);
+			newEdges.add(new Edge(sourceChain.get(0), destinationChain.get(0)));
+			newEdges.add(new Edge(sourceChain.get(1), destinationChain.get(1)));
+			if (sourceChain.get(1).isEmpty() && destinationChain.get(0).isEmpty()) {
+				newEdges.add(new Edge(sourceChain.get(0), destinationChain.get(1)));
+			}
+		}
+
+		nodes = newNodes;
+		setEdges(newEdges);
+	}
+
+	private void removeEmptyNodes() {
+		Iterator<Node> iterator = nodes.iterator();
+		while (iterator.hasNext()) {
+			Node node = iterator.next();
+			if (node.isEmpty()) {
+				iterator.remove();
+				rerouteEdgesAroundNode(node);
+			}
+		}
+	}
+
+	private void rerouteEdgesAroundNode(Node node) {
+		Set<Node> in = incoming(node);
+		Set<Node> out = outgoing(node);
+
+		incoming.remove(node);
+		outgoing.remove(node);
+
+		for (Node source : in) {
+			safeGet(outgoing, source).remove(node);
+		}
+		for (Node destination : out) {
+			safeGet(incoming, destination).remove(node);
+		}
+
+		for (Node source : in) {
+			for (Node destination : out) {
+				addEdge(source, destination);
+			}
+		}
+	}
+
+	private Set<Node> incoming(Node destination) {
+		return safeGet(incoming, destination);
+	}
+
+	private Set<Node> outgoing(Node source) {
+		return safeGet(outgoing, source);
+	}
+
+	private void removeUselessNodes() {
+		Iterator<Node> iterator = nodes.iterator();
+		while (iterator.hasNext()) {
+			Node node = iterator.next();
+			if (node.isSingleton() && incoming(node).isEmpty() && outgoing(node).isEmpty()) {
+				iterator.remove();
+				incoming.remove(node);
+				outgoing.remove(node);
+			}
+		}
+	}
+}