diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/GRI/dynamicProcessing/RELTracer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/GRI/dynamicProcessing/RELTracer.java
index eb96ba7ce92fe65cb342526872c9dc8daca784f0..2bfbe3b6b0637e8d9e654a4bb24d87df7e0762b5 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/GRI/dynamicProcessing/RELTracer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/GRI/dynamicProcessing/RELTracer.java
@@ -26,12 +26,11 @@ public class RELTracer {
*/
public FactBase computeQueryRelevant(
KnowledgeBase gri,
- StaticGRIRuleTransformer ruleTransformerFactory,
Atom query) {
gri = new KnowledgeBaseImpl(new SimpleInMemoryGraphStore(gri.getFactBase().getAtomsInMemory()), gri.getRuleBase());
//first, check that the query is entailed
- Atom queryWithFuncId = ruleTransformerFactory.createAtomWithStoredFnTermIdentifier(query);
+ Atom queryWithFuncId = StaticGRIRuleTransformer.instance().createAtomWithStoredFnTermIdentifier(query);
if (!gri.getFactBase().contains(queryWithFuncId)) {
LOG.warn("Query " + query + " not entailed by the input KB.");
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/encoders/GSATEncoder_GRI.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/encoders/GSATEncoder_GRI.java
new file mode 100644
index 0000000000000000000000000000000000000000..692aa4f6acf9dbebae875504eaf69006b75803d2
--- /dev/null
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/encoders/GSATEncoder_GRI.java
@@ -0,0 +1,20 @@
+package fr.boreal.explanation.api.encoders;
+
+import fr.boreal.explanation.solving_enumerating.encoders.GSATEncodingResult_GRI;
+
+/**
+ * Computes at GSAT encoding of the GRI and the Query for GMUS enumeration
+ * @param <DataStructureType> the data structure holding the GRI
+ * @param <QueryType> the query type
+ */
+public interface GSATEncoder_GRI<DataStructureType, QueryType> {
+
+ /**
+ *
+ * @param filteredGRI
+ * @param query
+ * @return at GSAT encoding of the filteredGRI and the Query for GMUS enumeration
+ */
+ GSATEncodingResult_GRI encode(DataStructureType filteredGRI, QueryType query);
+
+}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/AtomicQueryExplanationEnumerator.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/AtomicQueryExplainer.java
similarity index 91%
rename from integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/AtomicQueryExplanationEnumerator.java
rename to integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/AtomicQueryExplainer.java
index 71ed9bb3190353146e394ff088938a620453e520..30c3f44085542686a5dcc64413dd83939a4b949c 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/AtomicQueryExplanationEnumerator.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/AtomicQueryExplainer.java
@@ -1,4 +1,4 @@
-package fr.boreal.explanation.api;
+package fr.boreal.explanation.api.explainers;
import fr.boreal.model.formula.api.FOFormulaConjunction;
import fr.boreal.model.kb.api.KnowledgeBase;
@@ -11,7 +11,7 @@ import java.util.Arrays;
*
* @param <ExplanationType> the type of the (set of) explanations which is returned by the enumerator
*/
-public interface AtomicQueryExplanationEnumerator<ExplanationType> extends QueryExplainer<ExplanationType,Atom> {
+public interface AtomicQueryExplainer<ExplanationType> extends QueryExplainer<ExplanationType, Atom, KnowledgeBase> {
/**
* Checks if an atom can be explained
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/QueryExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/QueryExplainer.java
similarity index 81%
rename from integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/QueryExplainer.java
rename to integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/QueryExplainer.java
index ded40bc2dcb46888a85ea64311f1d64d6d62da1d..a2ebdedaf3044cef92949fbfe3e5626cd74ec932 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/QueryExplainer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/explainers/QueryExplainer.java
@@ -1,6 +1,4 @@
-package fr.boreal.explanation.api;
-
-import fr.boreal.model.kb.api.KnowledgeBase;
+package fr.boreal.explanation.api.explainers;
import java.util.Iterator;
import java.util.Set;
@@ -11,7 +9,7 @@ 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
*/
-public interface QueryExplainer<ExplanationType, QueryType> {
+public interface QueryExplainer<ExplanationType, QueryType, KnowledgeBaseType> {
/**
* @param query
@@ -36,6 +34,6 @@ public interface QueryExplainer<ExplanationType, QueryType> {
* @param query
* @return true iff the explainer surpports the query and the knowledget base
*/
- boolean canExplain(KnowledgeBase kb, QueryType query);
+ boolean canExplain(KnowledgeBaseType kb, QueryType query);
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/gmus/GMUSEncoder.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/gmus/GMUSEncoder.java
deleted file mode 100644
index 1db42f51d199ea0960668433815d7fb026d03c24..0000000000000000000000000000000000000000
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/gmus/GMUSEncoder.java
+++ /dev/null
@@ -1,10 +0,0 @@
-package fr.boreal.explanation.api.gmus;
-
-import fr.boreal.explanation.solving_enumerating.encoders.EncodingResult;
-import fr.boreal.model.kb.api.FactBase;
-import fr.boreal.model.logicalElements.api.Atom;
-
-public interface GMUSEncoder {
-
- EncodingResult encode(FactBase filteredGRI, Atom query);
-}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/gri/GRIExplanationProcessor.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/processors/ExplanationProcessor_GRI.java
similarity index 85%
rename from integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/gri/GRIExplanationProcessor.java
rename to integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/processors/ExplanationProcessor_GRI.java
index 4c532df4bba6e931646b06a2f18f169cec30c736..d0386a2b276f496fb83ba21cc2a9e828ecfc7b3e 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/gri/GRIExplanationProcessor.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/processors/ExplanationProcessor_GRI.java
@@ -1,4 +1,4 @@
-package fr.boreal.explanation.api.gri;
+package fr.boreal.explanation.api.processors;
import java.util.Iterator;
import java.util.Set;
@@ -10,7 +10,7 @@ import java.util.Set;
* @param <DataStructureType>
* @param <QueryType>
*/
-public interface GRIExplanationProcessor<ExplanationType, DataStructureType, QueryType> {
+public interface ExplanationProcessor_GRI<ExplanationType, DataStructureType, QueryType> {
/**
* @param GRI
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/processors/ExplanationProcessor_Rewriting.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/processors/ExplanationProcessor_Rewriting.java
new file mode 100644
index 0000000000000000000000000000000000000000..e11af5fa12854ba02886397663b794b0e9f1d78f
--- /dev/null
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/api/processors/ExplanationProcessor_Rewriting.java
@@ -0,0 +1,34 @@
+package fr.boreal.explanation.api.processors;
+
+import fr.boreal.model.kb.api.KnowledgeBase;
+
+import java.util.Iterator;
+import java.util.Set;
+
+/**
+ * Uses query rewriting to compute the Explanations of a Query
+ * Supports different types of Explanations, and Query types.
+ *
+ * @param <ExplanationType>
+ * @param <QueryType>
+ */
+public interface ExplanationProcessor_Rewriting<ExplanationType, QueryType> {
+
+ /**
+ * @param kb
+ * @param query
+ * @return the set of all explanations of a query given the kb
+ */
+ Set<ExplanationType> computeAllExplanations(KnowledgeBase kb, QueryType query);
+
+
+ /**
+ * @param kb
+ * @param query
+ * @return an iterator for all explanations of a query given the kb
+ */
+ default Iterator<ExplanationType> computeExplanations(KnowledgeBase kb, QueryType query) {
+ return this.computeAllExplanations(kb, query).iterator();
+ }
+
+}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/configuration/DefaultChaseForExplanations.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/configuration/DefaultChaseForExplanations.java
index 4469a013ca77ccd454f1b4cef6e5ac54dc5b3477..29da3d65ddacf8e9ec6591a6edf5d099effa0b06 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/configuration/DefaultChaseForExplanations.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/configuration/DefaultChaseForExplanations.java
@@ -1,6 +1,7 @@
package fr.boreal.explanation.configuration;
import fr.boreal.forward_chaining.api.ForwardChainingAlgorithm;
+import fr.boreal.forward_chaining.chase.Chase;
import fr.boreal.forward_chaining.chase.ChaseBuilder;
import fr.boreal.model.kb.api.KnowledgeBase;
@@ -9,12 +10,13 @@ import fr.boreal.model.kb.api.KnowledgeBase;
*/
public class DefaultChaseForExplanations {
- public static void chase(KnowledgeBase kb) {
- ForwardChainingAlgorithm chase = ChaseBuilder.defaultBuilder(kb.getFactBase(), kb.getRuleBase())
+ public static Chase chase(KnowledgeBase kb) {
+ Chase chase = ChaseBuilder.defaultBuilder(kb.getFactBase(), kb.getRuleBase())
.useObliviousChecker()
.useNaiveComputer()
.useNaiveRuleScheduler()
.build().get();
chase.execute();
+ return chase;
}
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/AbstractStaticGRIBasedExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/AbstractStaticGRIBasedExplainer.java
index cbf7eaca3a18dfad442c37cb356a886812c301c3..7dc09fbf85481497f4bc94c7f6f7e11274b7ad30 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/AbstractStaticGRIBasedExplainer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/AbstractStaticGRIBasedExplainer.java
@@ -2,17 +2,28 @@ package fr.boreal.explanation.explainers;
import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
import fr.boreal.explanation.GRI.staticProcessing.GRIBuilder;
+import fr.boreal.explanation.api.explainers.AtomicQueryExplainer;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
+import fr.boreal.explanation.configuration.DefaultChaseForExplanations;
+import fr.boreal.explanation.ruleFactories.RuleTransformationRecord;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
-import fr.boreal.explanation.solving_enumerating.gmus_processors.FactSupportGMUSProcessor;
+import fr.boreal.forward_chaining.chase.Chase;
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.logicalElements.api.Atom;
+import fr.boreal.model.logicalElements.impl.AtomImpl;
+import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
import org.apache.commons.lang3.tuple.Pair;
import java.util.Set;
-public abstract class AbstractStaticGRIBasedExplainer {
+public abstract class AbstractStaticGRIBasedExplainer<ExplanationType> implements AtomicQueryExplainer<ExplanationType> {
+ private final KnowledgeBase originalRB;
+ private final RuleTransformationRecord transformedRB;
+ private final Chase griKBChase;
/*
* A KB whose factbase will contain the GRI and whose rulebase the rules needed to compute the GRI
*/
@@ -29,8 +40,10 @@ public abstract class AbstractStaticGRIBasedExplainer {
* @param kb the current kb
*/
public AbstractStaticGRIBasedExplainer(KnowledgeBase kb) {
- Pair<KnowledgeBase, StaticGRIRuleTransformer> pair = GRIBuilder.buildGRI(kb);
- this.griKB = pair.getLeft();
+ this.originalRB = kb;
+ this.transformedRB = StaticGRIRuleTransformer.instance().createTransformedRB(kb);
+ this.griKB = new KnowledgeBaseImpl(kb.getFactBase(), transformedRB.getStaticRuleBase());
+ this.griKBChase = DefaultChaseForExplanations.chase(griKB);
}
/**
@@ -39,12 +52,23 @@ public abstract class AbstractStaticGRIBasedExplainer {
* @param query
* @return
*/
- public Set<KnowledgeBase> getAllExplanations(Atom query) {
- RELTracer tracer = new RELTracer();
- FactBase filteredGRI = tracer.computeQueryRelevant(griKB, ruleTransformer, query);
+ public Set<ExplanationType> getAllExplanations(Atom query) {
+ Atom queryWithFuncId = StaticGRIRuleTransformer.instance().createAtomWithStoredFnTermIdentifier(query);
- return getGMUSProcessor().computeExplanations(filteredGRI, ruleTransformer, query);
+ if (!griKB.getFactBase().contains(queryWithFuncId)) {
+ return Set.of();
+ }
+
+ // add seed atom to the factbase
+ Atom RELquery = new AtomImpl(StaticGRIRuleTransformer.REL, StaticGRIRuleTransformer.createFnTermIdentifier(query));
+ griKB.getFactBase().add(RELquery);
+
+ // set tracing rules
+ griKBChase.setRuleBase(this.transformedRB.getDynamicRuleBase());
+ griKBChase.execute();
+
+ return getGMUSProcessor().computeAllExplanations(griKB, query);
}
- abstract FactSupportGMUSProcessor getGMUSProcessor();
+ abstract ExplanationProcessor_GRI getGMUSProcessor();
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportExplainer.java
index a8dfae0d2f3e3831a76287d6689631fb0b2d4dc1..d39e9c01157ef9b8857acace3a6fc1b39fd2fddf 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportExplainer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportExplainer.java
@@ -1,21 +1,15 @@
package fr.boreal.explanation.explainers;
-import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
-import fr.boreal.explanation.GRI.staticProcessing.GRIBuilder;
-import fr.boreal.explanation.api.AtomicQueryExplanationEnumerator;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.explanation.solving_enumerating.gmus_processors.FactSupportGMUSProcessor;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
-import fr.boreal.model.logicalElements.api.Atom;
-import org.apache.commons.lang3.tuple.Pair;
-
-import java.util.Set;
/**
- * Computes kb-support explanations for a knowledge base and a ground atomic query
+ * Computes fact-support explanations for a knowledge base and a ground atomic query
*/
-public class FactSupportExplainer implements AtomicQueryExplanationEnumerator<KnowledgeBase> {
+public class FactSupportExplainer extends AbstractStaticGRIBasedExplainer<FactBase> {
KnowledgeBase gri;
StaticGRIRuleTransformer ruleTransformer;
/**
@@ -24,16 +18,12 @@ public class FactSupportExplainer implements AtomicQueryExplanationEnumerator<Kn
* @param kb the current kb
*/
public FactSupportExplainer(KnowledgeBase kb) {
- Pair<KnowledgeBase, StaticGRIRuleTransformer> pair = GRIBuilder.buildGRI(kb);
- gri = pair.getLeft();
- ruleTransformer = pair.getRight();
+ super(kb);
}
- public Set<KnowledgeBase> getAllExplanations(Atom query) {
- RELTracer tracer = new RELTracer();
- FactBase filteredGRI = tracer.computeQueryRelevant(gri, ruleTransformer, query);
-
- FactSupportGMUSProcessor gmusProcessor = new FactSupportGMUSProcessor();
- return gmusProcessor.computeExplanations(filteredGRI, ruleTransformer, query);
+ @Override
+ ExplanationProcessor_GRI getGMUSProcessor() {
+ return new FactSupportGMUSProcessor();
}
+
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportProvenanceExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportProvenanceExplainer.java
index 2f2a4434c7589509cc0fefb8b0b37ff737436f39..8c422cf0cc24cf7d68915e21e7b47a9473f6ee49 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportProvenanceExplainer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/FactSupportProvenanceExplainer.java
@@ -1,6 +1,6 @@
package fr.boreal.explanation.explainers;
-import fr.boreal.explanation.api.AtomicQueryExplanationEnumerator;
+import fr.boreal.explanation.api.explainers.AtomicQueryExplainer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.logicalElements.api.Atom;
@@ -9,7 +9,7 @@ import java.util.Set;
/**
* Computes fact-support-why-provenance explanations for a knowledge base and a ground atomic query
*/
-public class FactSupportProvenanceExplainer implements AtomicQueryExplanationEnumerator<FactBase> {
+public class FactSupportProvenanceExplainer implements AtomicQueryExplainer<FactBase> {
public Set<FactBase> getAllExplanations(Atom query) {
return Set.of();
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/KBSupportExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/KBSupportExplainer.java
index 3edd76fc5c47f18734e2d1064b990b58c73bae34..7eef5bd6833e6fcd753bac0491b0e59bb32724c8 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/KBSupportExplainer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/KBSupportExplainer.java
@@ -1,39 +1,31 @@
package fr.boreal.explanation.explainers;
-import fr.boreal.explanation.api.AtomicQueryExplanationEnumerator;
-import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
-import fr.boreal.explanation.solving_enumerating.gmus_processors.KBSupportGMUSProcessor;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
-import fr.boreal.explanation.GRI.staticProcessing.GRIBuilder;
+import fr.boreal.explanation.solving_enumerating.gmus_processors.FactSupportGMUSProcessor;
+import fr.boreal.explanation.solving_enumerating.gmus_processors.KBSupportGMUSProcessor;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
-import fr.boreal.model.logicalElements.api.Atom;
-import org.apache.commons.lang3.tuple.Pair;
-
-import java.util.Set;
/**
* Computes kb-support explanations for a knowledge base and a ground atomic query
*/
-public class KBSupportExplainer implements AtomicQueryExplanationEnumerator<KnowledgeBase> {
+public class KBSupportExplainer extends AbstractStaticGRIBasedExplainer<KnowledgeBase> {
KnowledgeBase gri;
StaticGRIRuleTransformer ruleTransformer;
+
/**
* Sets the initial KB and compute the GRI
*
* @param kb the current kb
*/
public KBSupportExplainer(KnowledgeBase kb) {
- Pair<KnowledgeBase, StaticGRIRuleTransformer> pair = GRIBuilder.buildGRI(kb);
- gri = pair.getLeft();
- ruleTransformer = pair.getRight();
+ super(kb);
}
- public Set<KnowledgeBase> getAllExplanations(Atom query) {
- RELTracer tracer = new RELTracer();
- FactBase filteredGRI = tracer.computeQueryRelevant(gri, ruleTransformer, query);
-
- KBSupportGMUSProcessor gmusProcessor = new KBSupportGMUSProcessor();
- return gmusProcessor.computeExplanations(filteredGRI, ruleTransformer, query);
+ @Override
+ ExplanationProcessor_GRI getGMUSProcessor() {
+ return new KBSupportGMUSProcessor();
}
+
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/NewFactSupportExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/NewFactSupportExplainer.java
deleted file mode 100644
index aef885070da6e8cf029cc9eb795704c06e1678d3..0000000000000000000000000000000000000000
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/NewFactSupportExplainer.java
+++ /dev/null
@@ -1,35 +0,0 @@
-package fr.boreal.explanation.explainers;
-
-import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
-import fr.boreal.explanation.GRI.staticProcessing.GRIBuilder;
-import fr.boreal.explanation.api.AtomicQueryExplanationEnumerator;
-import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
-import fr.boreal.explanation.solving_enumerating.gmus_processors.FactSupportGMUSProcessor;
-import fr.boreal.model.kb.api.FactBase;
-import fr.boreal.model.kb.api.KnowledgeBase;
-import fr.boreal.model.logicalElements.api.Atom;
-import org.apache.commons.lang3.tuple.Pair;
-
-import java.util.Set;
-
-/**
- * Computes kb-support explanations for a knowledge base and a ground atomic query
- */
-public class NewFactSupportExplainer extends AbstractStaticGRIBasedExplainer implements AtomicQueryExplanationEnumerator<KnowledgeBase> {
- KnowledgeBase gri;
- StaticGRIRuleTransformer ruleTransformer;
- /**
- * Sets the initial KB and compute the GRI
- *
- * @param kb the current kb
- */
- public NewFactSupportExplainer(KnowledgeBase kb) {
- super(kb);
- }
-
- @Override
- FactSupportGMUSProcessor getGMUSProcessor() {
- return new FactSupportGMUSProcessor();
- }
-
-}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/RuleSupportExplainer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/RuleSupportExplainer.java
index 24b1abb675b8d029780c080365dac0c5c9aa10d0..852d2bebb2068a4a2e7185a562d0844f543a0b03 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/RuleSupportExplainer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/explainers/RuleSupportExplainer.java
@@ -1,22 +1,16 @@
package fr.boreal.explanation.explainers;
-import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
-import fr.boreal.explanation.GRI.staticProcessing.GRIBuilder;
-import fr.boreal.explanation.api.AtomicQueryExplanationEnumerator;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.explanation.solving_enumerating.gmus_processors.FactSupportGMUSProcessor;
import fr.boreal.explanation.solving_enumerating.gmus_processors.RuleSupportGMUSProcessor;
-import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
-import fr.boreal.model.logicalElements.api.Atom;
-import org.apache.commons.lang3.tuple.Pair;
-
-import java.util.Set;
+import fr.boreal.model.kb.api.RuleBase;
/**
- * Computes kb-support explanations for a knowledge base and a ground atomic query
+ * Computes rule-support explanations for a knowledge base and a ground atomic query
*/
-public class RuleSupportExplainer implements AtomicQueryExplanationEnumerator<KnowledgeBase> {
+public class RuleSupportExplainer extends AbstractStaticGRIBasedExplainer<RuleBase> {
KnowledgeBase gri;
StaticGRIRuleTransformer ruleTransformer;
/**
@@ -25,16 +19,12 @@ public class RuleSupportExplainer implements AtomicQueryExplanationEnumerator<Kn
* @param kb the current kb
*/
public RuleSupportExplainer(KnowledgeBase kb) {
- Pair<KnowledgeBase, StaticGRIRuleTransformer> pair = GRIBuilder.buildGRI(kb);
- gri = pair.getLeft();
- ruleTransformer = pair.getRight();
+ super(kb);
}
- public Set<KnowledgeBase> getAllExplanations(Atom query) {
- RELTracer tracer = new RELTracer();
- FactBase filteredGRI = tracer.computeQueryRelevant(gri, ruleTransformer, query);
-
- RuleSupportGMUSProcessor gmusProcessor = new RuleSupportGMUSProcessor();
- return gmusProcessor.computeExplanations(filteredGRI, ruleTransformer, query);
+ @Override
+ ExplanationProcessor_GRI getGMUSProcessor() {
+ return new RuleSupportGMUSProcessor();
}
+
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/ruleFactories/RuleTransformationRecord.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/ruleFactories/RuleTransformationRecord.java
new file mode 100644
index 0000000000000000000000000000000000000000..4440a518a5d8808367ae200a2a25a304aa81fb43
--- /dev/null
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/ruleFactories/RuleTransformationRecord.java
@@ -0,0 +1,36 @@
+package fr.boreal.explanation.ruleFactories;
+
+import fr.boreal.model.kb.api.RuleBase;
+import fr.boreal.model.kb.impl.RuleBaseImpl;
+import fr.boreal.model.rule.api.FORule;
+import fr.boreal.model.rule.api.Rule;
+
+import java.util.Collection;
+import java.util.LinkedHashSet;
+
+public record RuleTransformationRecord(Collection<FORule> nodeBuildingRules, Collection<FORule> edgeBuildingRules,
+ Collection<FORule> relTracingRules){
+
+ public RuleBase getStaticRuleBase() {
+ Collection<FORule> temp = new LinkedHashSet<>();
+ temp.addAll(this.nodeBuildingRules);
+ temp.addAll(this.edgeBuildingRules);
+ return new RuleBaseImpl(temp);
+ }
+
+ public RuleBase getDynamicRuleBase() {
+ Collection<FORule> temp = new LinkedHashSet<>();
+ temp.addAll(this.relTracingRules);
+ return new RuleBaseImpl(temp);
+ }
+
+ public RuleBase getAllRules() {
+ Collection<FORule> temp = new LinkedHashSet<>();
+ temp.addAll(this.nodeBuildingRules);
+ temp.addAll(this.edgeBuildingRules);
+ temp.addAll(this.relTracingRules);
+ return new RuleBaseImpl(temp);
+ }
+
+
+}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/ruleFactories/StaticGRIRuleTransformer.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/ruleFactories/StaticGRIRuleTransformer.java
index c57cfc7fdd2d210c88390e12a57497dbd238060c..a7952bbf5e934f4550dd79876c55caad7c444306 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/ruleFactories/StaticGRIRuleTransformer.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/ruleFactories/StaticGRIRuleTransformer.java
@@ -5,8 +5,6 @@ import com.google.common.collect.HashBiMap;
import fr.boreal.model.formula.api.FOFormula;
import fr.boreal.model.formula.factory.FOFormulaFactory;
import fr.boreal.model.kb.api.KnowledgeBase;
-import fr.boreal.model.kb.api.RuleBase;
-import fr.boreal.model.kb.impl.RuleBaseImpl;
import fr.boreal.model.logicalElements.api.*;
import fr.boreal.model.logicalElements.factory.api.PredicateFactory;
import fr.boreal.model.logicalElements.factory.api.TermFactory;
@@ -66,21 +64,22 @@ public class StaticGRIRuleTransformer {
* (3) rel propagation rules
*/
- public RuleBase createTransformedRB(KnowledgeBase kb) {
-
- RuleBase rb = new RuleBaseImpl();
+ public RuleTransformationRecord createTransformedRB(KnowledgeBase kb) {
+ Set<FORule> nodeBuildingRules = new LinkedHashSet<>();
+ Set<FORule> edgeBuildingRules = new LinkedHashSet<>();
+ Set<FORule> relTracingRules = new LinkedHashSet<>();
for (Iterator<Predicate> it = kb.getFactBase().getPredicates(); it.hasNext(); ) {
Predicate p = it.next();
- rb.add(createGRINodeBuildingRule(p));
+ nodeBuildingRules.add(createGRINodeBuildingRule(p));
}
for (FORule r : kb.getRuleBase().getRules()) {
- rb.add(createGRIEdgeBuildingRule(r));
- rb.add(createRelPropagationRule(r));
+ edgeBuildingRules.add(createGRIEdgeBuildingRule(r));
+ relTracingRules.add(createRelPropagationRule(r));
}
- return rb;
+ return new RuleTransformationRecord(nodeBuildingRules,edgeBuildingRules,relTracingRules);
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSSolver.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSSolverImpl.java
similarity index 87%
rename from integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSSolver.java
rename to integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSSolverImpl.java
index 4bc61a0d51877c25f200795f2801d433abaf2c5f..d528efbdcafb902584085b508e31e343dde3cb30 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSSolver.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSSolverImpl.java
@@ -1,7 +1,6 @@
package fr.boreal.explanation.solving_enumerating;
import com.google.common.collect.BiMap;
-import com.google.common.collect.HashBiMap;
import fr.boreal.model.logicalElements.api.Term;
import java.io.*;
@@ -10,17 +9,12 @@ import java.util.List;
import java.util.Set;
-public class GMUSSolver {
+public class GMUSSolverImpl {
- private static final GMUSSolver INSTANCE = new GMUSSolver();
- public static GMUSSolver instance() {
- return INSTANCE;
- }
-
- String tmpFileName = "gsat.gcnf";
- File gcnfFile = new File(tmpFileName);
+ private static final String tmpFileName = "gsat.gcnf";
+ private static final File gcnfFile = new File(tmpFileName);
- int timeout = 0;
+ private static final int timeout = 0;
/**
* This main methods call two methods:
@@ -33,7 +27,7 @@ public class GMUSSolver {
*
* @return gmuses
**/
- public Set<String> solve(BiMap<Term, Integer> propVarIDMap,
+ public static Set<String> solve(BiMap<Term, Integer> propVarIDMap,
List<List<Integer>> clauses,
int nbGroup) {
Set<String> gmuses = new HashSet<>();
@@ -49,7 +43,7 @@ public class GMUSSolver {
* @param clauses
* @param nbGroup
*/
- public void writeGCNF(BiMap<Term, Integer> propVarIDMap,
+ public static void writeGCNF(BiMap<Term, Integer> propVarIDMap,
List<List<Integer>> clauses,
int nbGroup
) {
@@ -89,7 +83,7 @@ public class GMUSSolver {
* @param gcnfFile
* @return
*/
- public Set<String> getGMUSes(File gcnfFile) {
+ public static Set<String> getGMUSes(File gcnfFile) {
Set<String> gmuses = new HashSet<>();
ProcessBuilder build = new ProcessBuilder().redirectErrorStream(true);
if (timeout == 0)
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSTranslator.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSTranslatorImpl.java
similarity index 89%
rename from integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSTranslator.java
rename to integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSTranslatorImpl.java
index 10b6027c851fbe17fd6a357ffece4debf033d1be..f29c8cc52feb8ef05798c385df68bb9fbf5f12ff 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSTranslator.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSTranslatorImpl.java
@@ -13,11 +13,7 @@ import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
import java.util.HashSet;
import java.util.Set;
-public class GMUSTranslator {
- private static final GMUSTranslator INSTANCE = new GMUSTranslator();
- public static GMUSTranslator instance() {
- return INSTANCE;
- }
+public class GMUSTranslatorImpl {
/**
* This method takes in the set of strings (each string represents a gmus) and the factIDMap/ruleIDMap
@@ -27,7 +23,7 @@ public class GMUSTranslator {
* @param ruleIDMap
* @return set of explanations
*/
- public Set<KnowledgeBase> translateGMUSes(
+ public static Set<KnowledgeBase> translateGMUSes(
Set<String> gmuses,
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap
@@ -51,7 +47,7 @@ public class GMUSTranslator {
* @param ruleIDMap
* @return
*/
- public KnowledgeBase gmusToExpl(
+ public static KnowledgeBase gmusToExpl(
String gmus,
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap) {
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/AbstractKBtoGSATEncoder.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/AbstractGSATEncoderGRI.java
similarity index 88%
rename from integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/AbstractKBtoGSATEncoder.java
rename to integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/AbstractGSATEncoderGRI.java
index 34142c0195d8a01c0a966fd155222f797b843a1f..b9ed1393863738eea7ee1853fcdc93dda87d8a6a 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/AbstractKBtoGSATEncoder.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/AbstractGSATEncoderGRI.java
@@ -2,9 +2,10 @@ package fr.boreal.explanation.solving_enumerating.encoders;
import com.google.common.collect.BiMap;
import com.google.common.collect.HashBiMap;
-import fr.boreal.explanation.api.gmus.GMUSEncoder;
+import fr.boreal.explanation.api.encoders.GSATEncoder_GRI;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
+import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.logicalElements.api.Predicate;
import fr.boreal.model.logicalElements.api.StoredFunctionalTerm;
@@ -18,7 +19,7 @@ import java.util.Set;
/**
* This abstract class contains the main algorithm for encoding factbase with 4 additional abstract methods
- *
+ * <p>
* This class computes an encoding of explanations as GCNF formulas that can later be processed by a MUS solver
* <p>
* Ground atoms are represented as propositional variables
@@ -39,19 +40,31 @@ import java.util.Set;
* 1. factIDmap (nbGroup - atom)
* 2. ruleIDmap (nbGroup - ungrounded rule)
*/
-public abstract class AbstractKBtoGSATEncoder implements GMUSEncoder {
+public abstract class AbstractGSATEncoderGRI implements GSATEncoder_GRI<KnowledgeBase, Atom> {
- StaticGRIRuleTransformer staticGRIRuleTransformer;
+ StaticGRIRuleTransformer staticGRIRuleTransformer = StaticGRIRuleTransformer.instance();
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 int nbGroup;
+ protected int nbGroup;
+
+ public AbstractGSATEncoderGRI() {
+ this.nbGroup = getStartingGroupNumber();
+ }
- public AbstractKBtoGSATEncoder(StaticGRIRuleTransformer staticGRIRuleTransformer, int nbGroup) {
- this.staticGRIRuleTransformer = staticGRIRuleTransformer;
- this.nbGroup = nbGroup;
+
+ /**
+ * @return the starting group number for the encoding
+ */
+ abstract int getStartingGroupNumber();
+
+ /**
+ * @return the number of groups
+ */
+ public int getNumberOfGroups() {
+ return this.nbGroup;
}
/**
@@ -62,13 +75,13 @@ public abstract class AbstractKBtoGSATEncoder implements GMUSEncoder {
* @return set of explanations
*/
- public EncodingResult encode(
- FactBase filteredGRI,
+ public GSATEncodingResult_GRI encode(
+ KnowledgeBase filteredGRI,
Atom query) {
assignDefaultGroupNumberAndCreateClauseForStartQuery(query);
- assignGroupNumbersAndComputeClausesForRELEdges(filteredGRI, query);
+ assignGroupNumbersAndComputeClausesForRELEdges(filteredGRI.getFactBase(), query);
- return new EncodingResult(propVarIDMap,factIDMap,ruleIDMap,clauses, nbGroup);
+ return new GSATEncodingResult_GRI(propVarIDMap, factIDMap, ruleIDMap, clauses, nbGroup);
}
/**
@@ -104,9 +117,9 @@ public abstract class AbstractKBtoGSATEncoder implements GMUSEncoder {
// we collect all RELEDGE_r predicates after tracing
Set<Predicate> allRelEdgePredicatesAfterTracing = new HashSet<>();
var predIt = filteredGRI.getPredicates();
- while(predIt.hasNext()){
+ while (predIt.hasNext()) {
var p = predIt.next();
- if(p.label().startsWith(StaticGRIRuleTransformer.REL_EDGE_prefix)){
+ if (p.label().startsWith(StaticGRIRuleTransformer.REL_EDGE_prefix)) {
allRelEdgePredicatesAfterTracing.add(p);
}
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/EncodingResult.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/EncodingResult.java
deleted file mode 100644
index 20d749827ca562807ffaf0399431d4c3fde93234..0000000000000000000000000000000000000000
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/EncodingResult.java
+++ /dev/null
@@ -1,12 +0,0 @@
-package fr.boreal.explanation.solving_enumerating.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;
-
-public record EncodingResult(BiMap<Term, Integer> propVarIDMap, BiMap<Integer, Atom> factIDMap,
- BiMap<Integer, FORule> ruleIDMap, List<List<Integer>>clauses, int nbGroup) {}
-
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/FactSupportKBGSATEncoder.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/FactSupportKBGSATEncoder.java
index 64acfd076ce239562f80882189e324534be3bde0..5a115bcc713107cd01713a82968a59d73f9cdad9 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/FactSupportKBGSATEncoder.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/FactSupportKBGSATEncoder.java
@@ -1,16 +1,14 @@
package fr.boreal.explanation.solving_enumerating.encoders;
-import fr.boreal.explanation.api.gmus.GMUSEncoder;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
+import fr.boreal.model.kb.api.KnowledgeBase;
+import fr.boreal.model.logicalElements.api.Atom;
-public class FactSupportKBGSATEncoder extends AbstractKBtoGSATEncoder implements GMUSEncoder {
+public class FactSupportKBGSATEncoder extends AbstractGSATEncoderGRI {
- /**
- * Constructor for Fact-support KB to GSAT encoder
- * @param staticGRIRuleTransformer
- */
- public FactSupportKBGSATEncoder(StaticGRIRuleTransformer staticGRIRuleTransformer) {
- super(staticGRIRuleTransformer, 1);
+ @Override
+ int getStartingGroupNumber() {
+ return 1;
}
/**
@@ -57,4 +55,9 @@ public class FactSupportKBGSATEncoder extends AbstractKBtoGSATEncoder implements
public boolean needFact() {
return true;
}
+
+ @Override
+ public GSATEncodingResult_GRI encode(KnowledgeBase filteredGRI, Atom query) {
+ return null;
+ }
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/GSATEncodingResult_GRI.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/GSATEncodingResult_GRI.java
new file mode 100644
index 0000000000000000000000000000000000000000..38f279edd4c841ffd74e8f9e39f502406a1d76d0
--- /dev/null
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/GSATEncodingResult_GRI.java
@@ -0,0 +1,22 @@
+package fr.boreal.explanation.solving_enumerating.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;
+
+/**
+ *
+ * @param propVarIDMap map from propositional variables to integers
+ * @param factIDMap map from atoms to integers
+ * @param ruleIDMap maps from rules to integers
+ * @param clauses encoded GSAT
+ * @param nbGroup number of groups in the GSAT
+ */
+public record GSATEncodingResult_GRI(BiMap<Term, Integer> propVarIDMap,
+ BiMap<Integer, Atom> factIDMap,
+ BiMap<Integer, FORule> ruleIDMap,
+ List<List<Integer>>clauses, int nbGroup) {}
+
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/KBSupportKBGSATEncoder.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/KBSupportKBGSATEncoder.java
index 0fea45cafeec70694050b03642283cf11c7f6fbc..e3edc8d3829ded4314ffa0562bd935dd2e7d99c2 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/KBSupportKBGSATEncoder.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/KBSupportKBGSATEncoder.java
@@ -1,16 +1,13 @@
package fr.boreal.explanation.solving_enumerating.encoders;
-import fr.boreal.explanation.api.gmus.GMUSEncoder;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
+import fr.boreal.model.kb.api.KnowledgeBase;
+import fr.boreal.model.logicalElements.api.Atom;
-public class KBSupportKBGSATEncoder extends AbstractKBtoGSATEncoder implements GMUSEncoder {
+public class KBSupportKBGSATEncoder extends AbstractGSATEncoderGRI {
- /**
- * constructor for KB-support GCNF encoder
- * @param staticGRIRuleTransformer
- */
- public KBSupportKBGSATEncoder(StaticGRIRuleTransformer staticGRIRuleTransformer) {
- super(staticGRIRuleTransformer, 0);
+ int getStartingGroupNumber() {
+ return 0;
}
/**
@@ -60,4 +57,6 @@ public class KBSupportKBGSATEncoder extends AbstractKBtoGSATEncoder implements G
public boolean needFact() {
return true;
}
+
+
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/RuleSupportKBGSATEncoder.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/RuleSupportKBGSATEncoder.java
index f12b2da61c0de444abd57691338a5852e36cec1b..e01165da7b4c752b5b938de50c782f6a33d4cc2d 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/RuleSupportKBGSATEncoder.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/encoders/RuleSupportKBGSATEncoder.java
@@ -1,12 +1,11 @@
package fr.boreal.explanation.solving_enumerating.encoders;
-import fr.boreal.explanation.api.gmus.GMUSEncoder;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
-public class RuleSupportKBGSATEncoder extends AbstractKBtoGSATEncoder implements GMUSEncoder {
+public class RuleSupportKBGSATEncoder extends AbstractGSATEncoderGRI {
- public RuleSupportKBGSATEncoder(StaticGRIRuleTransformer staticGRIRuleTransformer) {
- super(staticGRIRuleTransformer,2);
+ int getStartingGroupNumber() {
+ return 2;
}
/**
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/AbstractSupportGMUSProcessor.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/AbstractSupportGMUSProcessor.java
new file mode 100644
index 0000000000000000000000000000000000000000..42b6b5eba04162277139294b777189dd204f3b08
--- /dev/null
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/AbstractSupportGMUSProcessor.java
@@ -0,0 +1,44 @@
+package fr.boreal.explanation.solving_enumerating.gmus_processors;
+
+import fr.boreal.explanation.api.encoders.GSATEncoder_GRI;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
+import fr.boreal.explanation.solving_enumerating.GMUSSolverImpl;
+import fr.boreal.explanation.solving_enumerating.GMUSTranslatorImpl;
+import fr.boreal.explanation.solving_enumerating.encoders.GSATEncodingResult_GRI;
+import fr.boreal.explanation.solving_enumerating.encoders.KBSupportKBGSATEncoder;
+import fr.boreal.model.kb.api.KnowledgeBase;
+import fr.boreal.model.logicalElements.api.Atom;
+
+import java.util.Set;
+
+public abstract class AbstractSupportGMUSProcessor<ExplanationType> implements ExplanationProcessor_GRI<ExplanationType,KnowledgeBase, Atom> {
+
+ protected static final GMUSSolverImpl solver = new GMUSSolverImpl();
+ protected static final GMUSTranslatorImpl translator = new GMUSTranslatorImpl();
+ protected GSATEncodingResult_GRI encoding;
+ protected Set<String> gmuses;
+ /**
+ * This method
+ * (1) takes in the filteredGRI (the factbase with REL/RELEDGES atom)
+ * (2) calls the encoder to construct the gcnf formula according to the type of explanations
+ * (3) calls the solver solve the formula from (2)
+ * and returns the set of rule-support explanations (in the form of knowledge base)
+ *
+ * @param filteredGRI
+ * @param query
+ * @return set of explanations
+ */
+ @Override
+ public Set<ExplanationType> computeAllExplanations(KnowledgeBase filteredGRI, Atom query) {
+
+ GSATEncoder_GRI encoder = getEncoder();
+ encoding = encoder.encode(filteredGRI, query);
+ gmuses = solver.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
+ return translate();
+
+ }
+
+ abstract GSATEncoder_GRI getEncoder();
+ abstract Set<ExplanationType> translate();
+
+}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/FactSupportGMUSProcessor.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/FactSupportGMUSProcessor.java
index e1ddf57cc1957cd0702989f786d7b630d66d98ee..8d0869d483b26d65c8b93ce076039beafea1cc01 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/FactSupportGMUSProcessor.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/FactSupportGMUSProcessor.java
@@ -1,8 +1,10 @@
package fr.boreal.explanation.solving_enumerating.gmus_processors;
+import fr.boreal.explanation.api.encoders.GSATEncoder_GRI;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
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.GMUSSolverImpl;
+import fr.boreal.explanation.solving_enumerating.GMUSTranslatorImpl;
import fr.boreal.explanation.solving_enumerating.encoders.FactSupportKBGSATEncoder;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
@@ -10,33 +12,18 @@ 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();
+public class FactSupportGMUSProcessor extends AbstractSupportGMUSProcessor<FactBase> {
- /**
- * This method
- * (1) takes in the filteredGRI (the factbase with REL/RELEDGES atom)
- * (2) calls the fact-support encoder to construct the gcnf formula
- * (3) calls the solver solve the formula from (2)
- * and returns the set of fact-support explanations (in the form of knowledge base with empty rulebase)
- *
- * @param filteredGRI
- * @param staticGRIRuleTransformer
- * @param query
- * @return set of explanations
- */
- public Set<KnowledgeBase> computeExplanations(
- FactBase filteredGRI,
- StaticGRIRuleTransformer staticGRIRuleTransformer,
- Atom query) {
- FactSupportKBGSATEncoder encoder = new FactSupportKBGSATEncoder(staticGRIRuleTransformer);
- var encoding = encoder.encode(filteredGRI, query);
- gmuses = solver.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
+ @Override
+ GSATEncoder_GRI getEncoder() {
+ return new FactSupportKBGSATEncoder();
+ }
- return translator.translateGMUSes(gmuses, encoding.factIDMap(), encoding.ruleIDMap());
+ @Override
+ Set<FactBase> translate() {
+ return Set.of();
+ // TODO adapt output translator.translateGMUSes(gmuses, encoding.factIDMap(), encoding.ruleIDMap());
}
+
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/KBSupportGMUSProcessor.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/KBSupportGMUSProcessor.java
index 542d62c690737d857da9fb1032024a2ba88f5f29..9e021bb7cd7153f24a01ef84fc940787fa5e118f 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/KBSupportGMUSProcessor.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/KBSupportGMUSProcessor.java
@@ -1,9 +1,10 @@
package fr.boreal.explanation.solving_enumerating.gmus_processors;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
-import fr.boreal.explanation.api.gmus.GMUSEncoder;
-import fr.boreal.explanation.solving_enumerating.GMUSSolver;
-import fr.boreal.explanation.solving_enumerating.GMUSTranslator;
+import fr.boreal.explanation.api.encoders.GSATEncoder_GRI;
+import fr.boreal.explanation.solving_enumerating.GMUSSolverImpl;
+import fr.boreal.explanation.solving_enumerating.GMUSTranslatorImpl;
import fr.boreal.explanation.solving_enumerating.encoders.KBSupportKBGSATEncoder;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
@@ -12,31 +13,16 @@ import fr.boreal.model.logicalElements.api.Atom;
import java.util.HashSet;
import java.util.Set;
-public class KBSupportGMUSProcessor {
- private Set<String> gmuses = new HashSet<>();
- private static final GMUSSolver solver = new GMUSSolver();
- private static final GMUSTranslator translator = new GMUSTranslator();
+public class KBSupportGMUSProcessor extends AbstractSupportGMUSProcessor<KnowledgeBase> {
- /**
- * This method
- * (1) takes in the filteredGRI (the factbase with REL/RELEDGES atom)
- * (2) calls the KB-support encoder to construct the gcnf formula
- * (3) calls the solver solve the formula from (2)
- * and returns the set of rule-support explanations (in the form of knowledge base)
- *
- * @param filteredGRI
- * @param staticGRIRuleTransformer
- * @param query
- * @return set of explanations
- */
- public Set<KnowledgeBase> computeExplanations(
- FactBase filteredGRI,
- StaticGRIRuleTransformer staticGRIRuleTransformer,
- Atom query) {
- GMUSEncoder encoder = new KBSupportKBGSATEncoder(staticGRIRuleTransformer);
- var encoding = encoder.encode(filteredGRI, query);
- gmuses = solver.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
+ @Override
+ GSATEncoder_GRI getEncoder() {
+ return new KBSupportKBGSATEncoder();
+ }
+ @Override
+ Set<KnowledgeBase> translate() {
return translator.translateGMUSes(gmuses, encoding.factIDMap(), encoding.ruleIDMap());
}
+
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/RuleSupportGMUSProcessor.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/RuleSupportGMUSProcessor.java
index 8fe8d04371b0b38468b3867dc35a72592b7ee8f9..f5b5e1926ed3c5ce0cf73b07074b6f3264273bc3 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/RuleSupportGMUSProcessor.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/RuleSupportGMUSProcessor.java
@@ -1,42 +1,32 @@
package fr.boreal.explanation.solving_enumerating.gmus_processors;
+import fr.boreal.explanation.api.encoders.GSATEncoder_GRI;
+import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
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.GMUSSolverImpl;
+import fr.boreal.explanation.solving_enumerating.GMUSTranslatorImpl;
import fr.boreal.explanation.solving_enumerating.encoders.FactSupportKBGSATEncoder;
import fr.boreal.explanation.solving_enumerating.encoders.RuleSupportKBGSATEncoder;
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.logicalElements.api.Atom;
import java.util.HashSet;
import java.util.Set;
-public class RuleSupportGMUSProcessor {
- private Set<String> gmuses = new HashSet<>();
- private static final GMUSSolver solver = new GMUSSolver();
- private static final GMUSTranslator translator = new GMUSTranslator();
+public class RuleSupportGMUSProcessor extends AbstractSupportGMUSProcessor<FactBase> {
- /**
- * This method
- * (1) takes in the filteredGRI (the factbase with REL/RELEDGES atom)
- * (2) calls the rule-support encoder to construct the gcnf formula
- * (3) calls the solver solve the formula from (2)
- * and returns the set of rule-support explanations (in the form of knowledge base with empty factbase)
- *
- * @param filteredGRI
- * @param staticGRIRuleTransformer
- * @param query
- * @return set of explanations
- */
- public Set<KnowledgeBase> computeExplanations(
- FactBase filteredGRI,
- StaticGRIRuleTransformer staticGRIRuleTransformer,
- Atom query) {
- RuleSupportKBGSATEncoder encoder = new RuleSupportKBGSATEncoder(staticGRIRuleTransformer);
- var encoding = encoder.encode(filteredGRI, query);
- gmuses = solver.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
+ @Override
+ GSATEncoder_GRI getEncoder() {
+ return new RuleSupportKBGSATEncoder();
+ }
- return translator.translateGMUSes(gmuses, encoding.factIDMap(), encoding.ruleIDMap());
+ @Override
+ Set<FactBase> translate() {
+ return Set.of();
+ // TODO adapt output translator.translateGMUSes(gmuses, encoding.factIDMap(), encoding.ruleIDMap());
}
+
+
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/sat4j/FactSupportMUSSat4JProcessor.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/sat4j/FactSupportMUSSat4JProcessor.java
index 28ce162ccc059fb9c006430cfe7636479506d350..3540084fedced43b91cfe0be613415734f6d32ed 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/sat4j/FactSupportMUSSat4JProcessor.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/gmus_processors/sat4j/FactSupportMUSSat4JProcessor.java
@@ -13,11 +13,11 @@ public class FactSupportMUSSat4JProcessor {
private Set<String> gmuses = new HashSet<>();
public Set<KnowledgeBase> computeExplanations(
- FactBase filteredGRI,
+ KnowledgeBase filteredGRI,
StaticGRIRuleTransformer staticGRIRuleTransformer,
Atom query) {
- FactSupportKBGSATEncoder encoder = new FactSupportKBGSATEncoder(staticGRIRuleTransformer);
+ FactSupportKBGSATEncoder encoder = new FactSupportKBGSATEncoder();
var encoding = encoder.encode(filteredGRI, query);
var gmuses = Sat4JSolver.enumerateGMUSes(encoding.clauses());
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/FactSupportExplainerTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/FactSupportExplainerTest.java
index de1fd1c937b71054c325afdeacfc042fdf889f6c..5e8f789d37f9a4a3cc2750f62564962e6448aa28 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/FactSupportExplainerTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/FactSupportExplainerTest.java
@@ -1,6 +1,5 @@
package fr.boreal.test.explanation.explainer;
-import fr.boreal.explanation.explainers.FactSupportExplainer;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/KBSupportExplainerTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/KBSupportExplainerTest.java
index 037479564763b428fd3b4a0682ca14f4afc7b61a..7027933bc2525f71d94b7b112de5ba22ba451ac5 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/KBSupportExplainerTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/KBSupportExplainerTest.java
@@ -1,6 +1,5 @@
package fr.boreal.test.explanation.explainer;
-import fr.boreal.explanation.explainers.KBSupportExplainer;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/RuleSupportExplainerTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/RuleSupportExplainerTest.java
index 0b0f742831a6ee8347d94a0c14bca360559c8259..2dd0f0a26003510a1876a13bfb03ee9d84b8845c 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/RuleSupportExplainerTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/explainer/RuleSupportExplainerTest.java
@@ -1,6 +1,5 @@
package fr.boreal.test.explanation.explainer;
-import fr.boreal.explanation.explainers.RuleSupportExplainer;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/FactSupportKBGSATEncoderTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/FactSupportKBGSATEncoderTest.java
index 349df57cc8d2269a1e6bdda2b94b3e594c6e581c..dd4f8396ef742812d12004df6f5adefdcda27232 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/FactSupportKBGSATEncoderTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/FactSupportKBGSATEncoderTest.java
@@ -29,7 +29,7 @@ public class FactSupportKBGSATEncoderTest {
@BeforeEach
public void setUp() {
staticGRIRuleTransformer = new StaticGRIRuleTransformer();
- encoder = new FactSupportKBGSATEncoder(staticGRIRuleTransformer);
+ encoder = new FactSupportKBGSATEncoder();
}
@Test
public void startQueryTest() {
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSSolverTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSSolverTest.java
index 5ef9ce6e40979c5898c764809842b81b67393709..ce89b94164bcac4f761fec05b7ddf8090604f3a2 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSSolverTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSSolverTest.java
@@ -2,8 +2,8 @@ package fr.boreal.test.explanation.solvingViaGMUS;
import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
import fr.boreal.explanation.solving_enumerating.encoders.KBSupportKBGSATEncoder;
-import fr.boreal.explanation.solving_enumerating.GMUSSolver;
-import fr.boreal.explanation.solving_enumerating.GMUSTranslator;
+import fr.boreal.explanation.solving_enumerating.GMUSSolverImpl;
+import fr.boreal.explanation.solving_enumerating.GMUSTranslatorImpl;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
@@ -23,8 +23,8 @@ import java.util.Set;
public class GMUSSolverTest {
KBSupportKBGSATEncoder gmusProcessor;
- GMUSTranslator gmusTranslator;
- GMUSSolver gmusSolver;
+ GMUSTranslatorImpl gmusTranslator;
+ GMUSSolverImpl gmusSolver;
StaticGRIRuleTransformer staticGRIRuleTransformer;
Predicate REL = staticGRIRuleTransformer.REL;
@@ -32,9 +32,9 @@ public class GMUSSolverTest {
@BeforeEach
public void setUp() {
staticGRIRuleTransformer = new StaticGRIRuleTransformer();
- gmusProcessor = new KBSupportKBGSATEncoder(staticGRIRuleTransformer);
- gmusTranslator = new GMUSTranslator();
- gmusSolver = new GMUSSolver();
+ gmusProcessor = new KBSupportKBGSATEncoder();
+ gmusTranslator = new GMUSTranslatorImpl();
+ gmusSolver = new GMUSSolverImpl();
}
@@ -46,17 +46,17 @@ public class GMUSSolverTest {
RuleBase ruleBase = new RuleBaseImpl(List.of(TestData.r1, TestData.r4));
KnowledgeBase kb = new KnowledgeBaseImpl(factBase, ruleBase);
- KnowledgeBase transformedKB = new KnowledgeBaseImpl(factBase, staticGRIRuleTransformer.createTransformedRB(kb));
+ KnowledgeBase transformedKB = new KnowledgeBaseImpl(factBase, staticGRIRuleTransformer.createTransformedRB(kb).getAllRules());
TestData.chase(transformedKB);
RELTracer tracer = new RELTracer();
- FactBase relAtoms = tracer.computeQueryRelevant(transformedKB, staticGRIRuleTransformer, TestData.qa);
+ FactBase relAtoms = tracer.computeQueryRelevant(transformedKB, TestData.qa);
gmusProcessor.assignDefaultGroupNumberAndCreateClauseForStartQuery(query);
gmusProcessor.assignGroupNumbersAndComputeClausesForRELEdges(relAtoms, query);
- Set<String> actual = gmusSolver.solve(gmusProcessor.propVarIDMap, gmusProcessor.clauses, gmusProcessor.nbGroup);
+ Set<String> actual = gmusSolver.solve(gmusProcessor.propVarIDMap, gmusProcessor.clauses, gmusProcessor.getNumberOfGroups());
Assertions.assertEquals(Set.of("2 1"), actual);
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSTranslatorTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSTranslatorTest.java
index 610a0205a17c89834144a456aec5ffec4388471e..919ff801afc69305b580e3e6f4c955661c569b7c 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSTranslatorTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/GMUSTranslatorTest.java
@@ -2,7 +2,7 @@ package fr.boreal.test.explanation.solvingViaGMUS;
import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
import fr.boreal.explanation.solving_enumerating.encoders.KBSupportKBGSATEncoder;
-import fr.boreal.explanation.solving_enumerating.GMUSTranslator;
+import fr.boreal.explanation.solving_enumerating.GMUSTranslatorImpl;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
@@ -23,7 +23,7 @@ import java.util.List;
public class GMUSTranslatorTest {
KBSupportKBGSATEncoder gmusProcessor;
- GMUSTranslator gmusTranslator;
+ GMUSTranslatorImpl gmusTranslator;
StaticGRIRuleTransformer staticGRIRuleTransformer;
Predicate REL = staticGRIRuleTransformer.REL;
@@ -31,8 +31,8 @@ public class GMUSTranslatorTest {
@BeforeEach
public void setUp() {
this.staticGRIRuleTransformer = new StaticGRIRuleTransformer();
- gmusProcessor = new KBSupportKBGSATEncoder(staticGRIRuleTransformer);
- gmusTranslator = new GMUSTranslator();
+ gmusProcessor = new KBSupportKBGSATEncoder();
+ gmusTranslator = new GMUSTranslatorImpl();
}
@Test
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/KBSupportKBGSATEncoderTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/KBSupportKBGSATEncoderTest.java
index 463066de09760aa63d1b5ba172cda1660b8b1fb5..6dc5948c97ba4a7eb7ec1b369b676abbc655ae3a 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/KBSupportKBGSATEncoderTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/KBSupportKBGSATEncoderTest.java
@@ -29,7 +29,7 @@ public class KBSupportKBGSATEncoderTest {
@BeforeEach
public void setUp() {
staticGRIRuleTransformer = new StaticGRIRuleTransformer();
- kBtoGSATEncoder = new KBSupportKBGSATEncoder(staticGRIRuleTransformer);
+ kBtoGSATEncoder = new KBSupportKBGSATEncoder();
}
@Test
public void startQueryTest() {
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/sat4j/MUSSat4JSolverTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/sat4j/MUSSat4JSolverTest.java
index 1410e4e31713162528eafbd08872f9cc2eef9331..29be82562ad8faebf9b248d4abd20d6cd045a8b4 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/sat4j/MUSSat4JSolverTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/solvingViaGMUS/sat4j/MUSSat4JSolverTest.java
@@ -1,12 +1,9 @@
package fr.boreal.test.explanation.solvingViaGMUS.sat4j;
import fr.boreal.explanation.GRI.dynamicProcessing.RELTracer;
-import fr.boreal.explanation.explainers.FactSupportExplainer;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
-import fr.boreal.explanation.solving_enumerating.GMUSTranslator;
import fr.boreal.explanation.solving_enumerating.encoders.FactSupportKBGSATEncoder;
import fr.boreal.explanation.solving_enumerating.encoders.KBSupportKBGSATEncoder;
-import fr.boreal.explanation.solving_enumerating.gmus_processors.FactSupportGMUSProcessor;
import fr.boreal.explanation.solving_enumerating.gmus_processors.sat4j.Sat4JSolver;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
@@ -17,12 +14,10 @@ import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.logicalElements.api.Predicate;
import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
import fr.boreal.test.explanation.TestData;
-import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;
import java.util.List;
-import java.util.Set;
public class MUSSat4JSolverTest {
StaticGRIRuleTransformer staticGRIRuleTransformer;
@@ -78,7 +73,7 @@ public class MUSSat4JSolverTest {
@Test
public void gmusToFactSupportExplTest() {
- FactSupportKBGSATEncoder gmusProcessor = new FactSupportKBGSATEncoder(staticGRIRuleTransformer);
+ FactSupportKBGSATEncoder gmusProcessor = new FactSupportKBGSATEncoder();
Atom query = TestData.qa;
FactBase factBase = new SimpleInMemoryGraphStore(List.of(TestData.pa, TestData.ta));
@@ -101,7 +96,7 @@ public class MUSSat4JSolverTest {
@Test
public void gmusToKBSupportExplTest() {
- KBSupportKBGSATEncoder encoder = new KBSupportKBGSATEncoder(staticGRIRuleTransformer);
+ KBSupportKBGSATEncoder encoder = new KBSupportKBGSATEncoder();
Atom query = TestData.qa;
FactBase factBase = new SimpleInMemoryGraphStore(List.of(TestData.pa, TestData.ta));