The codes now build but with most tests failing.

integraal/integraal-explanation/pom.xml

@@ -98,6 +98,6 @@
 			<artifactId>org.ow2.sat4j.core</artifactId>
 			<version>2.3.6</version>
 		</dependency>
-	</dependencies>
+    </dependencies>
 
 </project>
\ No newline at end of file

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/encoders/GSATEncodingResult_GRI.java

@@ -2,6 +2,7 @@ package fr.boreal.explanation.api.encoders;
 
 import com.google.common.collect.BiMap;
 import fr.boreal.model.logicalElements.api.Atom;
+import fr.boreal.model.logicalElements.api.Term;
 import fr.boreal.model.rule.api.FORule;
 
 import java.util.List;
@@ -14,7 +15,7 @@ import java.util.List;
  * @param clauses encoded GSAT
  * @param nbGroup number of groups in the GSAT
  */
-public record GSATEncodingResult_GRI(BiMap<?, Integer> propVarIDMap,
+public record GSATEncodingResult_GRI(BiMap<Atom, Integer> propVarIDMap,
                                      //TODO : can we put a more precise object?
                                      BiMap<Integer, Atom> factIDMap,
                                      BiMap<Integer, FORule> ruleIDMap,

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/processors/AbstractExplanationsProcessor_GMUS_GRI.java

@@ -42,8 +42,8 @@ public abstract class AbstractExplanationsProcessor_GMUS_GRI<ExplanationType, Da
 
     protected void solve() {
         this.gmuses = switch (solver) {
-            case MARCOGMUSSolver ignore ->
-                    MARCOGMUSSolver.solve(encoding.propVarIDMap().size(), encoding.clauses(), encoding.nbGroup());
+            case MARCOGMUSSolver marco ->
+                    marco.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
             case Sat4JSolver ignore -> Sat4JSolver.enumerateGMUSes(encoding.clauses());
             default -> throw new IllegalArgumentException("unsupported solver");
         };

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/kb_gri/encoders/AbstractGSATEncoder_KBGRI.java

@@ -45,7 +45,7 @@ public abstract class AbstractGSATEncoder_KBGRI implements GSATEncoder_GRI<Knowl
 
     StaticGRIRuleTransformer staticGRIRuleTransformer = StaticGRIRuleTransformer.instance();
     Predicate REL = StaticGRIRuleTransformer.REL;
-    public BiMap<Term, Integer> propVarIDMap = HashBiMap.create();
+    public BiMap<Atom, 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<>();
@@ -94,10 +94,8 @@ public abstract class AbstractGSATEncoder_KBGRI implements GSATEncoder_GRI<Knowl
      * @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(query, propVarIDMap.size() + 1);
+        clauses.add(List.of(0, propVarIDMap.get(query) * -1));
     }
 
 
@@ -161,7 +159,7 @@ public abstract class AbstractGSATEncoder_KBGRI implements GSATEncoder_GRI<Knowl
 
                     // Assign an integer to the relevant atom if unseen
                     propVarIDMap
-                            .putIfAbsent(relevantAtomIdentifier, propVarIDMap.size() + 1);
+                            .putIfAbsent(relevantAtom, propVarIDMap.size() + 1);
 
                     // Check that
                     // (1) the relevant atom belongs to the original factbase
@@ -187,7 +185,7 @@ public abstract class AbstractGSATEncoder_KBGRI implements GSATEncoder_GRI<Knowl
                 Atom headAtom = staticGRIRuleTransformer.getAtomFromFnTerm((StoredFunctionalTerm) headAtomIdentifier);
 
                 propVarIDMap
-                        .putIfAbsent(headAtomIdentifier, propVarIDMap.size() + 1);
+                        .putIfAbsent(headAtom, propVarIDMap.size() + 1);
 
 
                 relEdgeAtomClause.add(

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/kb_gri/rule_transformation/static_gri/StaticGRIRuleTransformer.java

@@ -19,8 +19,7 @@ import java.util.*;
 
 /**
  * This class implements a rule transformation for :
- * <p>
- * <p/>
+ * <p></p>
  * (1) statically computing the GRI (all the GRI is computed in one step)
  * (2) tracing relevant atoms
  */

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/marco/MARCOGMUSSolver.java

+package fr.boreal.explanation.solving_enumerating.marco;
+
+import com.google.common.collect.BiMap;
+import fr.boreal.explanation.api.solver.Solver;
+import fr.boreal.model.logicalElements.api.Atom;
+import fr.boreal.model.logicalElements.api.Term;
+
+import java.io.*;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+
+public class MARCOGMUSSolver implements Solver {
+
+    private static final MARCOGMUSSolver INSTANCE = new MARCOGMUSSolver();
+    public static MARCOGMUSSolver instance() {
+        return INSTANCE;
+    }
+
+    String tmpFileName = "gsat.gcnf";
+    File gcnfFile = new File(tmpFileName);
+
+    int timeout = 0;
+
+    /**
+     * This main methods call two methods:
+     * 1. writeGCNF: Writing the clauses to temporary gsat.gcnf file
+     * 2. getGMUSes: Call marco.py (marco.py MUS solver) with gsat.gcnf
+     * and return
+     * @param propVarIDMap
+     * @param clauses
+     * @param nbGroup
+     *
+     * @return gmuses
+     **/
+    public Set<String> solve(BiMap<Atom, Integer> propVarIDMap,
+                             List<List<Integer>> clauses,
+                             int nbGroup) {
+        Set<String> gmuses = new HashSet<>();
+        writeGCNF(propVarIDMap, clauses, nbGroup);
+        gmuses = getGMUSes(gcnfFile);
+        return gmuses;
+    };
+
+    /**
+     * write the temporary gsat.gcnf file
+     *
+     * @param propVarIDMap
+     * @param clauses
+     * @param nbGroup
+     */
+    public void writeGCNF(BiMap<Atom, Integer> propVarIDMap,
+                          List<List<Integer>> clauses,
+                          int nbGroup
+    ) {
+        try {
+            FileWriter writerCNF = new FileWriter(gcnfFile, false);
+
+            // the header of a gcnf file with the following format
+            // p gcnf + #variables + #clauses + #groups
+            writerCNF.write("p gcnf "
+                    + propVarIDMap.size() + " "
+                    + clauses.size() + " "
+                    + nbGroup + "\n");
+
+            for (List<Integer> clause: clauses) {
+                assert clause.getFirst() != null;
+                writerCNF.write(
+                        "{" + clause.getFirst() + "} "
+                );
+
+                for (int i = 1; i < clause.size(); i++) {
+                    // assert clause.get(i) != null;
+                    writerCNF.write(
+                            clause.get(i) + " "
+                    );
+                }
+                writerCNF.write(" 0\n");
+            }
+            writerCNF.close();
+
+        } catch (IOException e1) {
+            throw new RuntimeException("Unable to write tmp file for gcnf solver");
+        }
+    }
+
+    /**
+     * call the external marco gmus solver
+     * @param gcnfFile
+     * @return
+     */
+    public Set<String> getGMUSes(File gcnfFile) {
+        Set<String> gmuses = new HashSet<>();
+        ProcessBuilder build = new ProcessBuilder().redirectErrorStream(true);
+        if (timeout == 0)
+            build.command("MARCO-MUS/marco.py", "-v", "-b", "MUSes", gcnfFile.getAbsolutePath());
+        else
+            build.command("MARCO-MUS/marco.py", "-v", "-b", "MUSes", "-s", "-T", Long.toString(timeout), gcnfFile.getAbsolutePath());
+        Process proc;
+        try {
+            proc = build.start();
+        } catch (IOException e) {
+            throw new RuntimeException("MARCO process ended with an error\n" + e);
+        }
+
+        BufferedReader in = new BufferedReader(new InputStreamReader(proc.getInputStream()));
+        String line;
+        try {
+            while ((line = in.readLine()) != null) {
+                if (line.startsWith("U")) {
+                    gmuses.add(line.split("U ")[1]);
+                } else {
+                    System.err.println(line);
+                }
+            }
+        } catch (IOException e) {
+            throw new RuntimeException("MARCO process wrote an incorrect line\n" + e);
+        }
+        proc.destroy();
+
+        return gmuses;
+    }
+}

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/marco/MARCOGMUSTranslator.java

+package fr.boreal.explanation.solving_enumerating.marco;
+
+import com.google.common.collect.BiMap;
+import fr.boreal.model.kb.api.FactBase;
+import fr.boreal.model.kb.api.KnowledgeBase;
+import fr.boreal.model.kb.api.RuleBase;
+import fr.boreal.model.kb.impl.KnowledgeBaseImpl;
+import fr.boreal.model.kb.impl.RuleBaseImpl;
+import fr.boreal.model.logicalElements.api.Atom;
+import fr.boreal.model.rule.api.FORule;
+import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
+
+import java.util.HashSet;
+import java.util.Set;
+
+public class MARCOGMUSTranslator {
+
+    /**
+     * This method takes in the set of strings (each string represents a gmus) and the factIDMap/ruleIDMap
+     * and compute the set of explanations
+     *
+     * @param gmuses
+     * @param factIDMap
+     * @param ruleIDMap
+     * @return set of explanations
+     */
+    public static Set<KnowledgeBase> translateGMUSes(
+            Set<String> gmuses,
+            BiMap<Integer, Atom> factIDMap,
+            BiMap<Integer, FORule> ruleIDMap
+    ) {
+
+        Set<KnowledgeBase> explanations = new HashSet<>();
+        for (String gmus : gmuses) {
+            explanations.add(gmusToExpl(gmus, factIDMap, ruleIDMap));
+        }
+
+        return explanations;
+    }
+
+    /**
+     * This method takes in a gmus string which consists of integers separated by a space.
+     * Each integer is a group number.
+     * Then we find the element in the group and translate it back to fact or rule from the original KB.
+     *
+     * @param gmus
+     * @param factIDMap
+     * @param ruleIDMap
+     * @return
+     */
+    public static KnowledgeBase gmusToExpl(
+            String gmus,
+            BiMap<Integer, Atom> factIDMap,
+            BiMap<Integer, FORule> ruleIDMap) {
+
+        FactBase explFB = new SimpleInMemoryGraphStore();
+        RuleBase explRB = new RuleBaseImpl();
+
+        for (String clause : gmus.split(" ")) {
+
+            int nbGroup = Integer.parseInt(clause);
+
+            if (nbGroup > 0) {
+                if (factIDMap.containsKey(nbGroup)) {
+                    explFB.add(factIDMap.get(nbGroup));
+                } else if (ruleIDMap.containsKey(nbGroup)) {
+                    explRB.add(ruleIDMap.get(nbGroup));
+                }
+            }
+        }
+
+        KnowledgeBase expl = new KnowledgeBaseImpl(explFB, explRB);
+
+        return expl;
+    }
+}

integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSSolverTest.java → integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/MARCOGMUSSolverTest.java

@@ -21,7 +21,7 @@ import org.junit.jupiter.api.Test;
 import java.util.List;
 import java.util.Set;
 
-public class GMUSSolverTest {
+public class MARCOGMUSSolverTest {
     KBSupportKBGSATEncoder_KBGRI gmusProcessor;
     MARCOGMUSTranslator gmusTranslator;
     MARCOGMUSSolver gmusSolver;
@@ -56,7 +56,7 @@ public class GMUSSolverTest {
         gmusProcessor.assignGroupNumbersAndComputeClausesForRELEdges(relAtoms, query);
 
 
-        Set<String> actual = gmusSolver.solve(gmusProcessor.propVarIDMap.size(), gmusProcessor.clauses, gmusProcessor.getNumberOfGroups());
+        Set<String> actual = gmusSolver.solve(gmusProcessor.propVarIDMap, gmusProcessor.clauses, gmusProcessor.getNumberOfGroups());
 
         Assertions.assertEquals(Set.of("2 1"), actual);