From c549f70f9e4ae04a5a3b31a73078467b9cdf4c8f Mon Sep 17 00:00:00 2001
From: Akira <akira.charoensit@inria.fr>
Date: Mon, 24 Mar 2025 21:56:41 +0100
Subject: [PATCH] Refactoring incremental GRI
---
...actIncrementalGRIBasedExplainer_KBGRI.java | 70 ++++++++++++++-----
.../MowlOntologyTest.java | 3 +-
2 files changed, 53 insertions(+), 20 deletions(-)
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/kb_gri/explainers/incremental_gri/AbstractIncrementalGRIBasedExplainer_KBGRI.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/kb_gri/explainers/incremental_gri/AbstractIncrementalGRIBasedExplainer_KBGRI.java
index 8dee62f95..0da20ba3b 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/kb_gri/explainers/incremental_gri/AbstractIncrementalGRIBasedExplainer_KBGRI.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/kb_gri/explainers/incremental_gri/AbstractIncrementalGRIBasedExplainer_KBGRI.java
@@ -6,6 +6,7 @@ import fr.boreal.explanation.api.explainers.AtomicQueryExplainer;
import fr.boreal.explanation.api.processors.ExplanationProcessor_GRI;
import fr.boreal.explanation.api.solver.Solver;
import fr.boreal.explanation.configuration.DefaultChaseForExplanations;
+import fr.boreal.explanation.configuration.TimingUtil;
import fr.boreal.explanation.kb_gri.rule_transformation.GRIRuleTransformer;
import fr.boreal.explanation.kb_gri.rule_transformation.static_gri.RulesetForStaticGRIBuildingAndTracing;
import fr.boreal.explanation.solving_enumerating.marco.MARCOGMUSSolver;
@@ -70,7 +71,6 @@ public abstract class AbstractIncrementalGRIBasedExplainer_KBGRI<ExplanationType
// preprocessing
java.util.function.Predicate<Atom> belongsToInitialFactbase;
- boolean queryEntailed = false;
boolean queryInInitialFB = false;
// encoding
@@ -88,19 +88,6 @@ public abstract class AbstractIncrementalGRIBasedExplainer_KBGRI<ExplanationType
protected Set explanations;
protected Set<String> gmuses;
-
- protected KnowledgeBase relTracingKB;
- protected FactBase relEdgeFB;
- protected Set<String> marcoGmuses;
- BiMap<FORule, fr.boreal.model.logicalElements.api.Predicate> ruleToEdgePredicateMap;
-
-
- /**
- * The chase object used to compute the GRI, so that it can be reused for tracing.
- */
- protected Chase griKBChase;
-
-
/**
* Sets the initial KB
*
@@ -150,6 +137,44 @@ public abstract class AbstractIncrementalGRIBasedExplainer_KBGRI<ExplanationType
}
+ public void dynamicStepWithTimer(String datasetName, Collection<Atom> queries) {
+
+ TimingUtil.timer(this::recordInitialFactbase, "recordInitialFactbase", datasetName);
+
+ for (Atom query : queries) {
+ TimingUtil.timer(() -> checkQueryInInitialFB(query), "checkQueryInInitialFB", datasetName);
+
+ if (!queryInInitialFB) {
+
+ if (queryAncestorRules != null) {
+ TimingUtil.timer(this::clearAncestorRules, "clearAncestorRules", datasetName);
+ }
+
+ TimingUtil.timer(() -> computeAncestorRules(query), "computeAncestorRules", datasetName);
+ TimingUtil.timer(this::transformRules, "transformRules", datasetName);
+ TimingUtil.timer(this::chaseKBforGRI, "chaseKBforGRI", datasetName);
+
+ // filtering
+ TimingUtil.timer(() -> prepareRelTracing(query), "prepareRelTracing", datasetName);
+ TimingUtil.timer(this::chaseForRELPropagation, "chaseForRELPropagation", datasetName);
+ TimingUtil.timer(() -> encodeClauses(query), "encodeClauses", datasetName);
+
+ if (solver instanceof MARCOGMUSSolver) {
+ TimingUtil.timer(this::writeMarcoGCNF, "writeMarcoGCNF", datasetName);
+ TimingUtil.timer(this::solveGMUSviaMarco, "solveGMUSviaMarco", datasetName);
+ TimingUtil.timer(this::decodeGMUSesFromMarco, "decodeGMUSesFromMarco", datasetName);
+ } else if (solver instanceof Sat4JSolver) {
+ TimingUtil.timer(this::solveGMUSviaSat4j, "solveGMUSviaSat4j", datasetName);
+ TimingUtil.timer(this::decodeGMUSesFromSat4j, "decodeGMUSesFromSat4j", datasetName
+ );
+ }
+
+ } else {
+ TimingUtil.timer(() -> returnExplanationForQueryInFB(query), "returnExplanationForQueryInFB", datasetName);
+ }
+ }
+ }
+
/**
* This methods takes in a query and
* (1) compute queryAncestorRules of the query
@@ -213,21 +238,31 @@ public abstract class AbstractIncrementalGRIBasedExplainer_KBGRI<ExplanationType
queryAncestorRules.addAll(getAncestorRules(inputKB.getRuleBase(), query));
}
+ /**
+ * This operation transforms rules and prepares
+ * (1) static KB for static chase
+ * (2) dynamic RB for dynamic chase
+ */
public void transformRules() {
if (seenRules.isEmpty()) {
- FactBase initialFB = inputKB.getFactBase();
+
+ // building static KB (partial GRI)
KnowledgeBase queryAncestorRuleKB = new KnowledgeBaseImpl(
- initialFB,
+ new SimpleInMemoryGraphStore(inputKB.getFactBase().getAtomsInMemory()),
new RuleBaseImpl(queryAncestorRules));
+
this.transformedRB = ruleTransformer.createStaticGRIBuildingRB(queryAncestorRuleKB);
+ staticKB = new KnowledgeBaseImpl(inputKB.getFactBase(), transformedRB.getStaticRuleBase());
+ // preparing rules for dynamic chase
for (FORule rule : queryAncestorRules) {
FORule transformedRelPropRule = ruleTransformer.createRelPropagationRule(rule);
dynamicRB.add(transformedRelPropRule);
}
- staticKB = new KnowledgeBaseImpl(initialFB, transformedRB.getStaticRuleBase());
+ // recording the rules already seen
seenRules.addAll(queryAncestorRules);
+
} else if (!seenRules.containsAll(queryAncestorRules)) {
Set<FORule> rulesToAdd = new HashSet<>(queryAncestorRules);
@@ -249,7 +284,6 @@ public abstract class AbstractIncrementalGRIBasedExplainer_KBGRI<ExplanationType
}
public void chaseKBforGRI() {
-
DefaultChaseForExplanations.chase(this.staticKB);
}
diff --git a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/check_has_explanation/MowlOntologyTest.java b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/check_has_explanation/MowlOntologyTest.java
index 51e6f04c7..b66e0c7cf 100644
--- a/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/check_has_explanation/MowlOntologyTest.java
+++ b/integraal/integraal-explanation/src/test/java/fr/boreal/test/explanation/check_has_explanation/MowlOntologyTest.java
@@ -8,7 +8,6 @@ import fr.boreal.explanation.kb_gri.explainers.static_gri.KBSupportExplainer_KBG
import fr.boreal.explanation.kb_gri.explainers.static_gri.RuleSupportExplainer_KBGRI;
import fr.boreal.explanation.solving_enumerating.sat4j.Sat4JSolver;
import fr.boreal.explanation.tracker_gri.explainers.FactSupportExplainer_TrackerGRI;
-import fr.boreal.explanation.tracker_gri.explainers.UnambiguousProofTreeWhyProvenanceExplainer_TrackerGRI;
import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.kb.impl.KnowledgeBaseImpl;
import fr.boreal.model.kb.impl.RuleBaseImpl;
@@ -31,7 +30,7 @@ import java.util.stream.Stream;
public class MowlOntologyTest {
static String mowl_bench_path = "./src/test/resources/mowl-bench-main/";
- static List<String> mowl_bench_datasets = TestData.hard_mowl_bench_datasets;
+ static List<String> mowl_bench_datasets = TestData.default_mowl_bench_datasets;
enum AtomicQueryExplainerType {
STATIC_GRI_FB_MARCO,
--
GitLab