added nice print method for horn clauses

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

@@ -10,7 +10,8 @@ import fr.boreal.model.logicalElements.api.*;
 import fr.boreal.model.rule.api.FORule;
 import fr.boreal.model.rule.api.Rule;
 
-import java.util.*;
+import java.util.*;import java.util.stream.Collectors;
+
 
 /**
  * This abstract class contains the main algorithm for encoding factbase with 4 additional abstract methods
@@ -145,6 +146,8 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
 
     private void encode(Atom headAtom, Set<Atom> tempAnc, Rule rule, LineageTracker gri) {
 
+        System.out.println("\nencoding head: " + headAtom + " body: " + tempAnc + " rule: " + rule);
+
         int currentRuleIDAsGroupNumber;
 
         if (ruleIDMap.inverse().containsKey(rule)) {
@@ -157,6 +160,7 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
         List<Integer> ruleInstaceGroupClause = new ArrayList<>();
 
         ruleInstaceGroupClause.addFirst(currentRuleIDAsGroupNumber);
+        List<List<Integer>> tmpclauses = new ArrayList<>();
 
         // process the body atom
         for (Atom relevantAtom : tempAnc) {
@@ -177,7 +181,7 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
                     factIDMap.put(relAtomGroupID, relevantAtom);
                 }
                 // Create a singleton group with the atom to the gcnf
-                clauses.add(List.of(relAtomGroupID, propVarIDForCurrentAtom));
+                tmpclauses.add(List.of(relAtomGroupID, propVarIDForCurrentAtom));
             }
 
             // Add each relevant atom to the (body of) horn clause
@@ -192,7 +196,38 @@ public abstract class AbstractGSATEncoder_TrackerGRI implements GSATEncoder_GRI<
 
         // The clause is ready
         clauses.add(ruleInstaceGroupClause);
+        clauses.addAll(tmpclauses);
+        clauses.forEach(this::printHornClause);
+    }
+
+    public void printHornClause(List<Integer> clause) {
+        if (clause == null || clause.isEmpty()) {
+            System.out.println("Invalid clause");
+            return;
+        }
+
+        // Extract group number (first element)
+        int group = clause.get(0);
 
+        // Extract head and body
+        int head = 0;
+        List<Integer> body = new ArrayList<>();
+
+        for (int i = 1; i < clause.size(); i++) {
+            int literal = clause.get(i);
+            if (literal > 0) {
+                head = literal; // Positive literal is the head
+            } else {
+                body.add(-literal); // Convert negative literals to positive for printing
+            }
+        }
+
+        // Print the Horn clause in the required format
+        System.out.print("{" + group + "} ");
+        if (!body.isEmpty()) {
+            System.out.print(body.stream().map(String::valueOf).collect(Collectors.joining("^")) + " -> ");
+        }
+        System.out.println(head);
     }
 
     public abstract int computeRuleID();