From 1c3c5129b740159d837699e4c2099a511be0923d Mon Sep 17 00:00:00 2001
From: Federico Ulliana <ulliana@lirmm.fr>
Date: Tue, 25 Mar 2025 10:59:39 +0100
Subject: [PATCH] added a condition to force backtrack
---
.../UnambiguousProofTreeWhyProvenanceSolver.java | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java
index a0077f6fb..5977debce 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/whyprovenance/UnambiguousProofTreeWhyProvenanceSolver.java
@@ -120,8 +120,8 @@ public class UnambiguousProofTreeWhyProvenanceSolver implements Solver {
}
if(foundImprovableAtom){
- // see how to hanlde properly lastOperation = Operation.BACKTRACK;
- //continue;
+ //we force backtrack
+ atomsToProveQueue.clear();
}
atomsToProveQueue.sort(Comparator.comparingInt(a -> alternativesFor.get(a).size()));
--
GitLab