- Parsing functions

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/FactSupportKBGSATEncoder.java

@@ -115,7 +115,6 @@ public class FactSupportKBGSATEncoder implements GMUSEncoder {
                 // and, note that as a convention, we add the group number G in the first position <G, -1 ,-2,...,K>
 
 
-                // records the id of each rule to ruleIDMap
                 var it = filteredGRI.getAtomsByPredicate(relEdgePred);
                 while (it.hasNext()) {
                     Atom relEdge = it.next();

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/KBtoGSATEncoder.java

@@ -11,8 +11,11 @@ import fr.boreal.model.logicalElements.api.Predicate;
 import fr.boreal.model.logicalElements.api.StoredFunctionalTerm;
 import fr.boreal.model.logicalElements.api.Term;
 import fr.boreal.model.rule.api.FORule;
+import org.eclipse.rdf4j.query.algebra.In;
 
 import java.util.*;
+import java.util.function.BiFunction;
+import java.util.function.Function;
 
 /**
  * This class computes an encoding of explanations as GCNF formulas that can later be processed by a MUS solver
@@ -37,16 +40,41 @@ import java.util.*;
  */
 public class KBtoGSATEncoder implements GMUSEncoder {
 
+    private Function<Integer, Integer> groupIDFunction;
+    private Function<Integer, Integer> groupIDIncrementFunction;
+    private Function<Integer, Integer> factIDFunction;
+    private Function<Integer, Integer> factIDIncrementFunction;
     StaticGRIRuleTransformer staticGRIRuleTransformer;
     Predicate REL = StaticGRIRuleTransformer.REL;
-    public BiMap<Term, Integer> propVarIDMap = HashBiMap.create();
-    public BiMap<Integer, Atom> factIDMap = HashBiMap.create();
-    public BiMap<Integer, FORule> ruleIDMap = HashBiMap.create();
-    public List<List<Integer>> clauses = new ArrayList<>();
+    public BiMap<Term, Integer> propVarIDMap;
+    public BiMap<Integer, Atom> factIDMap;
+    public BiMap<Integer, FORule> ruleIDMap;
+    public List<List<Integer>> clauses;
+    private static final int defaultQueryGroup = 0;
+    private static final int defaultQueryID = 1;
     public int nbGroup = 0;
 
+    static Function<Integer,Integer> id = i -> i;
+    static Function<Integer,Integer> defaultGroupNumber = i -> 1;
+    static Function<Integer,Integer> defaultFactNumber = i -> 1;
+    static Function<Integer,Integer> incrementGroupNumber = i -> i+1;
+    static Function<Integer,Integer> doNotIncrementGroupNumber = i -> i;
+
     public KBtoGSATEncoder(StaticGRIRuleTransformer staticGRIRuleTransformer) {
+        this(staticGRIRuleTransformer, id, id, incrementGroupNumber, incrementGroupNumber);
+    }
+
+    public KBtoGSATEncoder(StaticGRIRuleTransformer staticGRIRuleTransformer,
+                           Function<Integer,Integer> groupIDFunction,
+                           Function<Integer,Integer> factIDFunction,
+                           Function<Integer,Integer> groupIDIncrementFunction,
+                           Function<Integer,Integer> factIDIncrementFunction) {
+        this.groupIDFunction = groupIDFunction;
+        this.groupIDIncrementFunction = groupIDIncrementFunction;
+        this.factIDFunction = factIDFunction;
+        this.factIDIncrementFunction = factIDIncrementFunction;
         this.staticGRIRuleTransformer = staticGRIRuleTransformer;
+        resetDataStructures();
     }
 
     /**
@@ -60,6 +88,9 @@ public class KBtoGSATEncoder implements GMUSEncoder {
     public EncodingResult encode(
             FactBase filteredGRI,
             Atom query) {
+
+        resetDataStructures();
+
         assignDefaultGroupNumberAndCreateClauseForStartQuery(query);
         assignGroupNumbersAndComputeClausesForRELEdges(filteredGRI, query);
 
@@ -67,30 +98,22 @@ public class KBtoGSATEncoder implements GMUSEncoder {
     }
 
     /**
-     * This method assigns id 1 to the query in propvarIDMap and add the query clause of group 0
-     * It modifies:
-     * 1. propvarIDMap
-     * 2. clauses
+     * This method creates a clause whose group number is 0.
+     * The clause contains a single negated propositional variable for the query.
      *
      * @param query
      */
     public void assignDefaultGroupNumberAndCreateClauseForStartQuery(Atom query) {
         Term queryFnTermIdentifier = staticGRIRuleTransformer.createFnTermIdentifier(query);
-        propVarIDMap.put(queryFnTermIdentifier, propVarIDMap.size() + 1);
-        clauses.add(List.of(0, propVarIDMap.get(queryFnTermIdentifier) * -1));
+        propVarIDMap.put(queryFnTermIdentifier, defaultQueryID);
+        clauses.add(List.of(defaultQueryGroup, defaultQueryID * -1));
     }
 
 
     /**
-     * For every *relvant* rule r :
-     * (1) Gives a group number [nbgroup] to every *relvant* rule r and hence to every REL_EDGE_r predicate
-     * (r is relevant if it is used to compute SupRel and marked by the presence of a REL_EDGE_r atom).
-     * <p>
-     * (2) Computes a set of clauses encoding the usage of r.
-     * Every clause is derived from an atom of the form
-     * REL_EDGE_r(id_grounded_body1,id_grounded_body2...,id_grounded_head)
-     * Every clause is encoded as a list of integers the structure
-     * nbgroup -id_grounded_body1 -id_grounded_body2 ... id_grounded_head
+     * This method creates a list of clauses of 2 types:
+     * (1) the singleton clause for each relevant atom that belongs to the initial FactBase
+     * (2) the horn clause corresponding to a trigger application
      *
      * @param filteredGRI
      */
@@ -111,13 +134,13 @@ public class KBtoGSATEncoder implements GMUSEncoder {
         // Looping over all relevant rules
         // We compute a SET of clauses. Each clause represents a grounding of the rule.
         // All clauses/groundings of the same rule will be in the same group
-
+        nbGr=stqrt5-
         for (Predicate relEdgePred : allRelEdgePredicatesAfterTracing) {
             var currentRule = relEdgePredicateToRule.get(relEdgePred);
 
             // We assign a new group to the currentRule
-            nbGroup++;
-            int currentRuleID = nbGroup;
+            nbGroup = groupIDIncrementFunction.apply(nbGroup); incre;ent5-
+            int currentRuleID = this.groupIDFunction.apply(nbGroup);
             ruleIDMap.put(currentRuleID, currentRule);
 
             // we produce a clause for every REL_EDGE_currentRule atom (each represents a grounding of currentRule)
@@ -154,8 +177,8 @@ public class KBtoGSATEncoder implements GMUSEncoder {
                     if (filteredGRI.contains(relevantAtom) && !factIDMap.inverse().containsKey(relevantAtom)) {
 
                         // Assign a group to the atom
-                        nbGroup++;
-                        var relAtomGroup = nbGroup;
+                        nbGroup = this.factIDIncrementFunction.apply(nbGroup);
+                        var relAtomGroup = this.factIDFunction.apply(nbGroup);
                         factIDMap.put(relAtomGroup, relevantAtom);
 
                         // Create a singleton group with the rel atom to the gcnf
@@ -185,4 +208,12 @@ public class KBtoGSATEncoder implements GMUSEncoder {
 
         }
     }
+
+    private void resetDataStructures() {
+        propVarIDMap = HashBiMap.create();
+        factIDMap = HashBiMap.create();
+        ruleIDMap = HashBiMap.create();
+        clauses = new ArrayList<>();
+    }
+
 }

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/FactSupportGMUSProcessor.java

@@ -4,23 +4,31 @@ import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
 import fr.boreal.explanation.solving_enumerating.GMUSSolver;
 import fr.boreal.explanation.solving_enumerating.GMUSTranslator;
 import fr.boreal.explanation.solving_enumerating.encoders.FactSupportKBGSATEncoder;
+import fr.boreal.explanation.solving_enumerating.encoders.KBtoGSATEncoder;
 import fr.boreal.model.kb.api.FactBase;
 import fr.boreal.model.kb.api.KnowledgeBase;
 import fr.boreal.model.logicalElements.api.Atom;
 
 import java.util.HashSet;
 import java.util.Set;
+import java.util.function.Function;
 
 public class FactSupportGMUSProcessor {
     private Set<String> gmuses = new HashSet<>();
     private static final GMUSSolver solver = new GMUSSolver();
     private static final GMUSTranslator translator = new GMUSTranslator();
 
+    static Function<Integer,Integer> id = i -> i;
+    static Function<Integer,Integer> defaultGroupNumber = i -> 77;
+    static Function<Integer,Integer> defaultFactNumber = i -> 1;
+    static Function<Integer,Integer> incrementGroupNumber = i -> i+1;
+    static Function<Integer,Integer> doNotIncrementGroupNumber = i -> i;
+
     public Set<KnowledgeBase> computeExplanations(
             FactBase filteredGRI,
             StaticGRIRuleTransformer staticGRIRuleTransformer,
             Atom query) {
-        FactSupportKBGSATEncoder encoder = new FactSupportKBGSATEncoder(staticGRIRuleTransformer);
+        KBtoGSATEncoder encoder = new KBtoGSATEncoder(staticGRIRuleTransformer, defaultGroupNumber, id, doNotIncrementGroupNumber, incrementGroupNumber);
         var encoding = encoder.encode(filteredGRI, query);
         gmuses = solver.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
 

integraal/integraal-explanation/src/main/java/module-info.java

@@ -11,4 +11,5 @@ module fr.boreal.explanation {
     requires fr.boreal.component;
     requires org.checkerframework.checker.qual;
     requires org.slf4j;
+    requires rdf4j.queryalgebra.model;
 }
\ No newline at end of file