integraal/integraal-explanation/src/main/java/fr/boreal/explanation/kb_gri/explainers/static_gri/AbstractStaticGRIBasedExplainer_KBGRI.java

@@ -24,9 +24,7 @@ import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
 import fr.boreal.views.FederatedFactBase;
 
 import java.io.File;
-import java.util.Collection;
-import java.util.List;
-import java.util.Set;
+import java.util.*;
 
 import static fr.boreal.explanation.configuration.PathFinder.ensureFilePath;
 import static fr.boreal.explanation.configuration.Timers.measureAndPrintTime;
@@ -90,6 +88,19 @@ public abstract class AbstractStaticGRIBasedExplainer_KBGRI<ExplanationType> imp
     protected Set explanations;
     protected Set<String> gmuses;
 
+
+    protected Statistics statistics = new Statistics();
+
+    public class Statistics {
+
+        Map<Atom, DynamicStatistics> dynamic = new LinkedHashMap<>();
+
+        public class DynamicStatistics {
+            public long queryEntailmentTime;
+        }
+
+    }
+
     /**
      * Constructor
      */
@@ -229,10 +240,17 @@ public abstract class AbstractStaticGRIBasedExplainer_KBGRI<ExplanationType> imp
     }
 
     public void checkQueryEntailment(Atom query) {
+
+        long start, end;
+        start = System.currentTimeMillis();
+
         Atom queryWithFuncId = GRIRuleTransformer.instance().createAtomWithStoredFnTermIdentifier(query);
         if (staticKB.getFactBase().contains(queryWithFuncId)) {
             queryEntailed = true;
         }
+
+        end = System.currentTimeMillis();
+        //this.statistics.dynamic.get(query).queryEntailmentTime = (end - start);
     }
 
     public void checkQueryInInitialFB(Atom query) {
@@ -242,6 +260,12 @@ public abstract class AbstractStaticGRIBasedExplainer_KBGRI<ExplanationType> imp
     }
 
 
+    /**
+     * Prepares a dynamic KB that can be used for tracing relevant atoms for the input query.
+     * The dynamic KB uses a federated factbase ; inferences will be put on the local storage, which can be eas
+     *
+     * @param query
+     */
     public void prepareRelTracing(Atom query) {
         Atom RELQuery = new AtomImpl(GRIRuleTransformer.REL, GRIRuleTransformer.createFnTermIdentifier(query));
 

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/tracker_gri/encoders/AbstractGSATEncoder_TrackerGRI.java

@@ -79,7 +79,7 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
             Atom query,
             java.util.function.Predicate<Atom> belongsToInitialFactbase) {
         assignDefaultGroupNumberAndCreateClauseForStartQuery(query);
-        addClauseIfQueryBelongsToTheInitialFactbase(query,belongsToInitialFactbase);
+        addClauseIfQueryBelongsToTheInitialFactbase(query, belongsToInitialFactbase);
         assignGroupNumbersAndComputeClausesForRELEdges(gri, query, belongsToInitialFactbase);
 
         // Check that there is no redundancy
@@ -104,7 +104,7 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
 
 
     private void addClauseIfQueryBelongsToTheInitialFactbase(Atom query, java.util.function.Predicate<Atom> belongsToInitialFactbase) {
-        if(belongsToInitialFactbase.test(query)) {
+        if (belongsToInitialFactbase.test(query)) {
             clauses.add(List.of(reservedQueryGroup, reservedQueryPropVariable));
         }
     }
@@ -136,7 +136,7 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
                 for (Rule rule : ruleInstances.keySet()) {
                     for (Substitution substitution : ruleInstances.get(rule).keySet()) {
                         Set<Atom> tempAnc = ruleInstances.get(rule).get(substitution);
-                        if(tempAnc.contains(query)) {
+                        if (tempAnc.contains(query)) {
                             //skip as the rule is redundant
                             continue;
                         }
@@ -144,7 +144,8 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
 
                         // track visited
                         for (Atom ancestorAtom : tempAnc) {
-                            if (!visited.contains(ancestorAtom) && !query.equals(ancestorAtom)) {
+                            if (!visited.contains(ancestorAtom) && !toVisit.contains(ancestorAtom) && !query.equals(ancestorAtom)) {
+                                System.out.println("Adding " + ancestorAtom + " to " + toVisit);
                                 // we add the second condition because the query atom may be a different object than the data atom
                                 // and we do not need to visit it twice
                                 toVisit.add(ancestorAtom);
@@ -227,10 +228,14 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
         ruleInstanceGroupClause.add(propVarIDForHeadAtom);
 
         // The clause is ready
-
-        if (!clauses.contains(ruleInstanceGroupClause)) {
-            clauses.add(ruleInstanceGroupClause);
-        }
+        clauses.add(ruleInstanceGroupClause);
+
+        //if (!clauses.contains(ruleInstanceGroupClause)) {
+        //    clauses.add(ruleInstanceGroupClause);
+        //} else {
+        //    System.out.println("Already seen group clause: " + ruleInstanceGroupClause);
+        //    throw new RuntimeException("Already seen group clause: " + ruleInstanceGroupClause);
+        //}
 
         for (List<Integer> clause : tmpclauses) {
             if (!clauses.contains(clause)) {

integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/unit_tests/explainer/tracker_gri_s4j/KBSupportExplainerWithLinearTrackerAndSat4JTest.java

@@ -110,8 +110,6 @@ public class KBSupportExplainerWithLinearTrackerAndSat4JTest {
         Set<KnowledgeBase> explanations = explainer.getAllExplanations(query);
 
         KnowledgeBase expectedExpl = createKnowledgeBase(Set.of(TestData.pa),
-                // there is no rule in the explanation
-                // Set.of(TestData.r12_px_px)
                 Set.of()
         );