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.
alpha-asp · Feb 10, 2020 · be345dc · be345dc
1 parent 3c27810
commit be345dc
Show file tree

Hide file tree

Showing 2 changed files with 44 additions and 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
@@ -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
@@ -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;
  }
  }