Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix bug in justification analysis, address issue #211. #220

Merged
merged 3 commits into from
Jul 16, 2020
Merged

Fix bug in justification analysis, address issue #211. #220

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
be345dc
Address issue #211.
AntoniusW Feb 10, 2020
599b7eb
Update copyright year.
AntoniusW Feb 10, 2020
f440077
Fix LitSet coverage check in justification analysis.
AntoniusW Feb 15, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
/**
* A variable substitution allowing variables to occur on the right-hand side. Chains of variable substitutions are
* resolved automatically, i.e., adding the substitutions (X -> A) and (A -> d) results in (X -> d), (A -> d).
* Copyright (c) 2018, the Alpha Team.
* Copyright (c) 2018-2020, the Alpha Team.
*/
public class Unifier extends Substitution {

Expand Down Expand Up @@ -47,6 +47,19 @@ public Unifier extendWith(Substitution extension) {
return this;
}

/**
* Returns a list of all variables occurring in that unifier, i.e., variables that are mapped and those that occur (nested) in the right-hand side of the unifier.
* @return the list of variables occurring somewhere in the unifier.
*/
public List<Term> getOccurringVariables() {
ArrayList<Term> ret = new ArrayList<>();
for (Map.Entry<VariableTerm, Term> substitution : substitution.entrySet()) {
ret.add(substitution.getKey());
ret.addAll(substitution.getValue().getOccurringVariables());
}
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.
Expand Down
40 changes: 33 additions & 7 deletions src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,18 +1,39 @@
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;

/**
* Copyright (c) 2018, the Alpha Team.
* Copyright (c) 2018-2020, the Alpha Team.
*/
public class AnalyzeUnjustified {
private static final Logger LOGGER = LoggerFactory.getLogger(AnalyzeUnjustified.class);
Expand Down Expand Up @@ -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> variablesOccurringInSigma = sigma.getOccurringVariables();
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<>(variablesOccurringInSigma);
occurringVariables.addAll(sigmaN.getOccurringVariables());
BasicAtom genericAtom = new BasicAtom(Predicate.getInstance("_", occurringVariables.size(), true), occurringVariables);
Atom genericSubstituted = genericAtom.substitute(sigmaN).renameVariables("_analyzeTest");
if (Unification.instantiate(genericSubstituted, genericAtom.substitute(sigma)) != null) {
log("Atom {} is excluded by: {} via {}", genericSubstituted, sigmaN, sigma);
continue atomLoop;
}
}
Expand Down