From be345dcc8d75143c8554f547be21eea860216b78 Mon Sep 17 00:00:00 2001
From: Antonius Weinzierl <antonius.weinzierl@gmail.com>
Date: Mon, 10 Feb 2020 20:11:36 +0100
Subject: [PATCH] Address issue #211.

- AnalyzeUnjustified uses more general atom to test for exclusion due to
  prior analysis, i.e., less atoms are (falsely) discarded.
- Unifier can report which variables are mapped.
---
 .../ac/tuwien/kr/alpha/grounder/Unifier.java  | 12 ++++++
 .../structure/AnalyzeUnjustified.java         | 38 ++++++++++++++++---
 2 files changed, 44 insertions(+), 6 deletions(-)

diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java
index 8d65fa7ca..b5f46b9b5 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java
@@ -47,6 +47,18 @@ public Unifier extendWith(Substitution extension) {
 		return this;
 	}
 
+	/**
+	 * Returns a list of all variables that this unifier maps to something else, i.e., it returns all variables on the left-hand side of the unifier.
+	 * @return the list of mapped variables.
+	 */
+	public List<Term> getMappedVariables() {
+		ArrayList<Term> ret = new ArrayList<>();
+		for (Map.Entry<VariableTerm, Term> substitution : substitution.entrySet()) {
+			ret.add(substitution.getKey());
+		}
+		return ret;
+	}
+
 
 	public <T extends Comparable<T>> Term put(VariableTerm variableTerm, Term term) {
 		// If term is not ground, store it for right-hand side reverse-lookup.
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java
index 8f17cbe11..f98d19dc2 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java
@@ -1,13 +1,34 @@
 package at.ac.tuwien.kr.alpha.grounder.structure;
 
-import at.ac.tuwien.kr.alpha.common.*;
-import at.ac.tuwien.kr.alpha.common.atoms.*;
-import at.ac.tuwien.kr.alpha.grounder.*;
+import at.ac.tuwien.kr.alpha.common.Assignment;
+import at.ac.tuwien.kr.alpha.common.AtomStore;
+import at.ac.tuwien.kr.alpha.common.DisjunctiveHead;
+import at.ac.tuwien.kr.alpha.common.Predicate;
+import at.ac.tuwien.kr.alpha.common.Rule;
+import at.ac.tuwien.kr.alpha.common.atoms.Atom;
+import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
+import at.ac.tuwien.kr.alpha.common.atoms.ComparisonLiteral;
+import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral;
+import at.ac.tuwien.kr.alpha.common.atoms.Literal;
+import at.ac.tuwien.kr.alpha.common.terms.Term;
+import at.ac.tuwien.kr.alpha.grounder.Instance;
+import at.ac.tuwien.kr.alpha.grounder.NonGroundRule;
+import at.ac.tuwien.kr.alpha.grounder.Unification;
+import at.ac.tuwien.kr.alpha.grounder.Unifier;
 import at.ac.tuwien.kr.alpha.solver.ThriceTruth;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.LinkedHashMap;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.NoSuchElementException;
+import java.util.Set;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
 
@@ -219,10 +240,15 @@ private Set<LitSet> unjustCover(List<Literal> vB, Set<Unifier> vY, Set<Unifier>
 				if (!bSigma.isGround()) {
 					throw oops("Resulting atom is not ground.");
 				}
+				List<Term> variablesMappedBySigma = sigma.getMappedVariables();
 				if (Unification.instantiate(bSigmaY, bSigma) != null) {
 					for (Unifier sigmaN : vN) {
-						if (Unification.instantiate(b.substitute(sigmaN), bSigma) != null) {
-							log("Atom is excluded by: {}", sigmaN);
+						ArrayList<Term> occurringVariables = new ArrayList<>(variablesMappedBySigma);
+						occurringVariables.addAll(sigmaN.getMappedVariables());
+						BasicAtom genericAtom = new BasicAtom(Predicate.getInstance("_", occurringVariables.size(), true), occurringVariables);
+						BasicAtom genericSubstituted = genericAtom.substitute(sigmaN);
+						if (Unification.instantiate(genericSubstituted, genericAtom.substitute(sigma)) != null) {
+							log("Atom {} is excluded by: {} via {}", genericSubstituted, sigmaN, sigma);
 							continue atomLoop;
 						}
 					}