diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/QueryExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/QueryExplainer.java
index a2ebdedaf3044cef92949fbfe3e5626cd74ec932..2fee7e271022aa03e54520c65bd5ba575c0f3875 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/QueryExplainer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/QueryExplainer.java
@@ -8,8 +8,9 @@ import java.util.Set;
*
* @param <ExplanationType> the type of the (set of) explanations which is returned by the enumerator
* @param <QueryType> the type of the query
+ * @param <ExplanationContext> the context to use for finding explanations (eg. a knowledge base, a factbase, a rulebase)
*/
-public interface QueryExplainer<ExplanationType, QueryType, KnowledgeBaseType> {
+public interface QueryExplainer<ExplanationType, QueryType, ExplanationContext> {
/**
* @param query
@@ -20,20 +21,18 @@ public interface QueryExplainer<ExplanationType, QueryType, KnowledgeBaseType> {
/**
* @param query
* @return an iterator for the set of explanations for the query on the current KB
- * TODO :
*/
default Iterator<ExplanationType> getExplanations(QueryType query) {
return getAllExplanations(query).iterator();
}
- ;
-
/**
* Checks if an atom can be explained
*
* @param query
+ * @param context to use for finding explanations (eg. a knowledge base, a factbase, a rulebase)
* @return true iff the explainer surpports the query and the knowledget base
*/
- boolean canExplain(KnowledgeBaseType kb, QueryType query);
+ boolean canExplain(ExplanationContext context, QueryType query);
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java
index 9873dcf2a449ce2847778879f673ca819601109c..aeb48bdce03437d437550b0ec1ddc28c5a4ec143 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java
@@ -11,9 +11,9 @@ import java.util.*;
public class UnambiguousProofTreeWhyProvenanceSolver implements Solver {
- private List<Triple> loadLevel(Atom current, LineageTracker gri) {
+ private List<Trigger> loadLevel(Atom current, LineageTracker gri) {
var triggers = gri.getRuleInstancesYielding(current);
- List<Triple> stack = new Stack<>();
+ List<Trigger> stack = new Stack<>();
for (Map.Entry<Rule, Map<Substitution, Set<Atom>>> ruleEntry : triggers.entrySet()) {
Rule rule = ruleEntry.getKey();
@@ -23,7 +23,7 @@ public class UnambiguousProofTreeWhyProvenanceSolver implements Solver {
Substitution substitution = subEntry.getKey();
Set<Atom> atoms = subEntry.getValue();
- stack.add(new Triple(rule, substitution, atoms));
+ stack.add(new Trigger(rule, substitution, atoms, current));
}
}
return stack;
@@ -31,76 +31,82 @@ public class UnambiguousProofTreeWhyProvenanceSolver implements Solver {
public Object computeAllExplanations(LineageTracker gri, Atom query, HashSet<Atom> intialAtoms) {
- List<Object> currentProof = new ArrayList<>();
- Set<Atom> proved = new LinkedHashSet<>();
- List<List<Triple>> levels = new ArrayList<>();
- List<Atom> levelAtom = new ArrayList<>();
- List<Integer> levelPosition = new ArrayList<>();
- levelAtom.add(query);
- int level = 0;
-
- while (level!=-1) {
-
- Atom current = levelAtom.get(level);
-
- if (levelPosition.size() == 0 || levelPosition.size() - 1 < level) {
- //load level
- levelPosition.add(0);
- var alternativeTriggersForCurrent = this.loadLevel(current, gri);
-
- if (alternativeTriggersForCurrent.isEmpty()) {
- proved.add(current);
- if (levelAtom.size()-1==level) {
- // we reached the end : print the solution
- for (int i = 0; i < levels.size(); i++) {
- System.out.println(levels.get(i).get(levelPosition.get(i)));
- System.out.println(current);
+ char backtracked = '0';
+ char loaded = '1';
+ char lastOperation = loaded;
+
+ // atom level
+ int k = 0;
+ List<List<Trigger>> levels = new ArrayList<>();
+ levels.add(loadLevel(query, gri));
+
+ // atom alternative
+ ArrayList<Integer> jk = new ArrayList<>();
+ jk.add(0);
+
+ // list of seen and to prove atoms
+ List<Atom> toProve = new ArrayList<>();
+ toProve.add(query);
+ List<Atom> provedAtoms = new ArrayList<>();
+ provedAtoms.add(query);
+ List<Trigger> solutionTriggers = new ArrayList<>();
+
+ while (k >= 0) {
+ if (lastOperation == loaded) {
+
+ if (levels.get(k).isEmpty()) {
+ //nothing to load into toProve
+ } else {
+ Trigger current = levels.get(k).get(jk.get(k));
+ solutionTriggers.add(current);
+ toProve.remove(current.head);
+ provedAtoms.add(current.head);
+
+ //load next atoms into toProve
+ for (Atom a : current.atoms()) {
+ if (!provedAtoms.contains(a)) {
+ toProve.add(a);
}
- //backtrack
- level--;
}
- continue;
}
- levels.add(alternativeTriggersForCurrent);
- } else {
- // try to advance into level
- var pos = levelPosition.get(level);
- if (levels.get(level).size() - 1 == pos) {
- level--;
- continue;
+
+ if (toProve.isEmpty()) {
+ System.out.println("Solution " + provedAtoms+"\n");
+ solutionTriggers.forEach(System.out::println);
+ lastOperation = backtracked;
} else {
- levelPosition.add(level, pos + 1);
+ Atom next = toProve.remove(0);
+ //provedAtoms.add(next);
+ levels.add(loadLevel(next, gri));
+ jk.add(0);
+ k++;
+ lastOperation = loaded;
}
+ continue;
}
-
- // find atoms for the next levels
- Triple trigger = levels.get(level).get(levelPosition.get(level));
- for (Atom ancestor : trigger.atoms()) {
- if (!proved.contains(ancestor)) {
- levelAtom.add(ancestor);
+ if (lastOperation == backtracked) {
+
+ if (levels.get(k).size() - 1 >= jk.get(k) + 1) {
+ // move to the next level
+ jk.set(k, jk.get(k) + 1);
+ var current = levels.get(k).get(jk.get(k));
+ solutionTriggers.add(current);
+ provedAtoms.set(k, current.head);
+ lastOperation = loaded;
+ } else {
+ levels.remove(k);
+ jk.remove(k);
+ k--;
}
- }
- proved.add(current);
-
- if (levelAtom.size()==level) {
- // we reached the end : print the solution
- for (int i = 0; i < levels.size(); i++) {
- System.out.println(levels.get(i).get(levelPosition.get(i)));
- }
- //backtrack
- level--;
- continue;
- }
- if (levels.isEmpty()) {
- break;
}
- level++;
+
}
+
return null;
}
- record Triple(Rule rule, Substitution substitution, Set<Atom> atoms) {
+ record Trigger(Rule rule, Substitution substitution, Set<Atom> atoms, Atom head) {
}
}