Track unknowns more carefully to prevent unknowns from being proven/d…

…isproven later

jkind/src/jkind/engines/AdviceEngine.java

@@ -11,10 +11,11 @@
 import jkind.translation.Specification;
 
 public class AdviceEngine extends AbstractInvariantGenerationEngine {
+	public static final String NAME = "advice";
 	private final List<Expr> potentialInvariants;
 
 	public AdviceEngine(Specification spec, JKindSettings settings, Director director, Advice advice) {
-		super("advice", spec, settings, director);
+		super(NAME, spec, settings, director);
 
 		advice.prune(spec.node);
 		this.potentialInvariants = advice.getInvariants();

jkind/src/jkind/engines/BmcEngine.java

@@ -19,10 +19,11 @@
 import jkind.util.StreamIndex;
 
 public class BmcEngine extends SolverBasedEngine {
+	public static final String NAME = "bmc";
 	private List<String> validProperties = new ArrayList<>();
 
 	public BmcEngine(Specification spec, JKindSettings settings, Director director) {
-		super("bmc", spec, settings, director);
+		super(NAME, spec, settings, director);
 	}
 
 	@Override
@@ -78,7 +79,7 @@ private void sendBaseStep(int k) {
 	}
 
 	private void sendUnknown(List<String> unknown) {
-		director.broadcast(new UnknownMessage(unknown));
+		director.receiveMessage(new UnknownMessage(getName(), unknown));
 	}
 
 	private void assertProperties(int k) {

jkind/src/jkind/engines/Director.java

@@ -4,8 +4,12 @@
 import java.util.ArrayList;
 import java.util.Collections;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
+import java.util.stream.Collectors;
 
 import jkind.JKindException;
 import jkind.JKindSettings;
@@ -40,6 +44,8 @@
 import jkind.writers.XmlWriter;
 
 public class Director extends MessageHandler {
+	public static final String NAME = "director";
+
 	private final JKindSettings settings;
 	private final Specification spec;
 	private final Writer writer;
@@ -73,6 +79,8 @@ public Director(JKindSettings settings, Specification spec) {
 			this.adviceWriter = new AdviceWriter(settings.writeAdvice);
 			this.adviceWriter.addVarDecls(Util.getVarDecls(spec.node));
 		}
+
+		initializeUnknowns(settings, spec.node.properties);
 	}
 
 	private final Writer getWriter() {
@@ -305,10 +313,71 @@ protected void handleMessage(InductiveCounterexampleMessage icm) {
 		}
 	}
 
+	private final Map<String, Integer> bmcUnknowns = new HashMap<>();
+	private final Set<String> kInductionUnknowns = new HashSet<>();
+	private final Set<String> pdrUnknowns = new HashSet<>();
+
+	private void initializeUnknowns(JKindSettings settings, List<String> properties) {
+		if (!settings.boundedModelChecking) {
+			for (String prop : properties) {
+				bmcUnknowns.put(prop, 0);
+			}
+		}
+
+		if (!settings.kInduction) {
+			kInductionUnknowns.addAll(properties);
+		}
+
+		if (settings.pdrMax <= 0) {
+			pdrUnknowns.addAll(properties);
+		}
+	}
+
 	@Override
 	protected void handleMessage(UnknownMessage um) {
-		remainingProperties.removeAll(um.unknown);
-		writer.writeUnknown(um.unknown, baseStep, convertInductiveCounterexamples(), getRuntime());
+		if (um.source.equals(NAME)) {
+			return;
+		}
+
+		markUnknowns(um);
+
+		Map<Integer, List<String>> completed = getCompletelyUnknownByBaseStep(um);
+		for (Entry<Integer, List<String>> entry : completed.entrySet()) {
+			int baseStep = entry.getKey();
+			List<String> unknowns = entry.getValue();
+			remainingProperties.removeAll(unknowns);
+			writer.writeUnknown(um.unknown, baseStep, convertInductiveCounterexamples(),
+					getRuntime());
+			broadcast(new UnknownMessage(NAME, unknowns));
+		}
+	}
+
+	private Map<Integer, List<String>> getCompletelyUnknownByBaseStep(UnknownMessage um) {
+		return um.unknown.stream().filter(this::isCompletelyUnknown)
+				.collect(Collectors.groupingBy(bmcUnknowns::get));
+	}
+
+	private void markUnknowns(UnknownMessage um) {
+		switch (um.source) {
+		case BmcEngine.NAME:
+			for (String prop : um.unknown) {
+				bmcUnknowns.put(prop, baseStep);
+			}
+			break;
+
+		case KInductionEngine.NAME:
+			kInductionUnknowns.addAll(um.unknown);
+			break;
+
+		case PdrEngine.NAME:
+			pdrUnknowns.addAll(um.unknown);
+			break;
+		}
+	}
+
+	public boolean isCompletelyUnknown(String prop) {
+		return bmcUnknowns.containsKey(prop) && kInductionUnknowns.contains(prop)
+				&& pdrUnknowns.contains(prop);
 	}
 
 	@Override
@@ -360,8 +429,12 @@ private void printSummary() {
 				Output.println("INVALID PROPERTIES: " + invalidProperties);
 				Output.println();
 			}
-			if (!remainingProperties.isEmpty()) {
-				Output.println("UNKNOWN PROPERTIES: " + remainingProperties);
+
+			List<String> unknownProperties = new ArrayList<>(spec.node.properties);
+			unknownProperties.removeAll(validProperties);
+			unknownProperties.removeAll(invalidProperties);
+			if (!unknownProperties.isEmpty()) {
+				Output.println("UNKNOWN PROPERTIES: " + unknownProperties);
 				Output.println();
 			}
 		}

jkind/src/jkind/engines/IntervalGeneralizationEngine.java

@@ -15,9 +15,11 @@
 import jkind.translation.Specification;
 
 public class IntervalGeneralizationEngine extends Engine {
+	public static final String NAME = "interval-generalization";
+
 	public IntervalGeneralizationEngine(Specification spec, JKindSettings settings,
 			Director director) {
-		super("interval-generalization", spec, settings, director);
+		super(NAME, spec, settings, director);
 	}
 
 	@Override

jkind/src/jkind/engines/InvariantReductionEngine.java

@@ -32,10 +32,11 @@
 import jkind.util.SexpUtil;
 
 public class InvariantReductionEngine extends SolverBasedEngine {
+	public static final String NAME = "invariant-reduction";
 	private YicesSolver yicesSolver;
 
 	public InvariantReductionEngine(Specification spec, JKindSettings settings, Director director) {
-		super("invariant-reduction", spec, settings, director);
+		super(NAME, spec, settings, director);
 	}
 
 	@Override

jkind/src/jkind/engines/KInductionEngine.java

@@ -29,12 +29,13 @@
 import jkind.util.StreamIndex;
 
 public class KInductionEngine extends SolverBasedEngine {
+	public static final String NAME = "k-induction";
 	private int kCurrent = 0;
 	private int kLimit = 0;
 	private InvariantSet invariants = new InvariantSet();
 
 	public KInductionEngine(Specification spec, JKindSettings settings, Director director) {
-		super("k-induction", spec, settings, director);
+		super(NAME, spec, settings, director);
 	}
 
 	@Override
@@ -65,11 +66,16 @@ private void checkProperties(int k) {
 			if (result instanceof SatResult || result instanceof UnknownResult) {
 				Model model = getModel(result);
 				if (model == null) {
+					sendUnknown(properties);
+					properties.clear();
 					break;
 				}
-				
+
 				List<String> bad = getFalseProperties(possiblyValid, k, model);
 				possiblyValid.removeAll(bad);
+				if (result instanceof UnknownResult) {
+					sendUnknown(bad);
+				}
 				sendInductiveCounterexamples(bad, k + 1, model);
 			} else if (result instanceof UnsatResult) {
 				properties.removeAll(possiblyValid);
@@ -123,9 +129,24 @@ private void sendInductiveCounterexamples(List<String> properties, int length, M
 		}
 	}
 
+	private void sendUnknown(List<String> unknown) {
+		director.receiveMessage(new UnknownMessage(getName(), unknown));
+	}
+
 	@Override
 	protected void handleMessage(BaseStepMessage bsm) {
 		kLimit = bsm.step;
+
+		List<String> unknown = difference(properties, bsm.properties);
+		if (!unknown.isEmpty()) {
+			sendUnknown(unknown);
+		}
+	}
+
+	private List<String> difference(List<String> list1, List<String> list2) {
+		List<String> result = new ArrayList<>(list1);
+		result.removeAll(list2);
+		return result;
 	}
 
 	@Override

jkind/src/jkind/engines/SmoothingEngine.java

@@ -22,10 +22,11 @@
 import jkind.util.StreamIndex;
 
 public class SmoothingEngine extends SolverBasedEngine {
+	public static final String NAME = "smoothing";
 	private YicesSolver yicesSolver;
 
 	public SmoothingEngine(Specification spec, JKindSettings settings, Director director) {
-		super("smoothing", spec, settings, director);
+		super(NAME, spec, settings, director);
 	}
 
 	@Override

jkind/src/jkind/engines/invariant/GraphInvariantGenerationEngine.java

@@ -8,9 +8,11 @@
 import jkind.translation.Specification;
 
 public class GraphInvariantGenerationEngine extends AbstractInvariantGenerationEngine {
+	public static final String NAME = "invariant-generation";
+
 	public GraphInvariantGenerationEngine(Specification spec, JKindSettings settings,
 			Director director) {
-		super("invariant-generation", spec, settings, director);
+		super(NAME, spec, settings, director);
 	}
 
 	@Override

jkind/src/jkind/engines/messages/UnknownMessage.java

@@ -1,16 +1,24 @@
 package jkind.engines.messages;
 
+import java.util.Collections;
 import java.util.List;
 
 import jkind.util.Util;
 
 public class UnknownMessage extends Message {
+	public final String source;
 	public final List<String> unknown;
-
-	public UnknownMessage(List<String> unknown) {
+
+	public UnknownMessage(String source, List<String> unknown) {
+		this.source = source;
 		this.unknown = Util.safeCopy(unknown);
 	}
 
+	public UnknownMessage(String source, String unknown) {
+		this.source = source;
+		this.unknown = Collections.singletonList(unknown);
+	}
+
 	@Override
 	public void accept(MessageHandler handler) {
 		handler.handleMessage(this);

jkind/src/jkind/engines/pdr/PdrEngine.java

@@ -17,11 +17,12 @@
 import jkind.translation.Specification;
 
 public class PdrEngine extends Engine {
+	public static final String NAME = "pdr";
 	private final ConcurrentMap<String, PdrSubengine> subengines = new ConcurrentHashMap<>();
 	private int scratchCounter = 1;
 
 	public PdrEngine(Specification spec, JKindSettings settings, Director director) {
-		super("pdr", spec, settings, director);
+		super(NAME, spec, settings, director);
 	}
 
 	@Override
@@ -52,6 +53,7 @@ private void spawnSubengine() {
 
 	public void reportUnknown(String prop) {
 		subengines.remove(prop);
+		director.receiveMessage(new UnknownMessage(getName(), prop));
 	}
 
 	public void reportThrowable(Throwable throwable) {