From e2865f6a45285a2962bc72b0e5910964bc73ade1 Mon Sep 17 00:00:00 2001
From: Yann Thierry-Mieg <Yann.Thierry-Mieg@lip6.fr>
Date: Sun, 5 May 2024 16:24:24 +0200
Subject: [PATCH] refactoring to prepare TrapAlongRefiner + break every 20
 traps found

---
 .../move/gal/structural/smt/TrapRefiner.java  | 45 ++++++++++++++-----
 1 file changed, 33 insertions(+), 12 deletions(-)

diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/TrapRefiner.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/TrapRefiner.java
index b03cd0663c..0cc7917ace 100644
--- a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/TrapRefiner.java
+++ b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/TrapRefiner.java
@@ -42,13 +42,12 @@ public int refine(SolverState solver, ProblemSet problems, RefinementMode mode,
         			if (problem.getSolution().getReply() != SMTReply.SAT) {
         				continue;
         			} else {
-        				problem.updateWitness(solver, "s");
+        				updateWitness(solver, problem);
         			}
         			if (solver.getNumericType() ==SolutionType.Real && problem.getSolution().getReply() == SMTReply.REAL) {
         				continue;
         			}
-                    CandidateSolution candidate = problem.getSolution();
-                    boolean newTrapFound = findTrap(net, candidate.getState(), knownTraps, solver);            
+                    boolean newTrapFound = findTrap(net, problem.getSolution(), knownTraps, solver);            
                 }
                 constraintsAdded += knownTraps.refine(solver, problems, mode, current, timeout);
                 totalConstraints += constraintsAdded;        	        	
@@ -73,11 +72,10 @@ public int refine(SolverState solver, ProblemSet problems, RefinementMode mode,
         			if (problem.getSolution().getReply() != SMTReply.SAT) {
         				break;
         			} else {
-        				problem.updateWitness(solver, "s");
+        				updateWitness(solver, problem);
         			}
         			
-        			CandidateSolution candidate = problem.getSolution();
-        			boolean newTrapFound = findTrap(net, candidate.getState(), knownTraps, solver);
+        			boolean newTrapFound = findTrap(net, problem.getSolution(), knownTraps, solver);
         			if (newTrapFound) {
         				int added = knownTraps.refine(solver, problems, mode, current, timeout);
         				totalConstraints += added;
@@ -85,6 +83,10 @@ public int refine(SolverState solver, ProblemSet problems, RefinementMode mode,
         			} else {
         				break;
         			}
+					if (totalConstraints >= 20) {
+						// let other refiners do some work
+						return totalConstraints;
+					}
         		}
             }
             problems.update();
@@ -94,9 +96,22 @@ public int refine(SolverState solver, ProblemSet problems, RefinementMode mode,
         return totalConstraints;
     }
 
-    private boolean findTrap(ISparsePetriNet net, SparseIntArray state, StaticRefiner known, SolverState solver) {
+	public void updateWitness(SolverState solver, Problem problem) {
+		problem.updateWitness(solver, "s");
+	}
+
+    /**
+     * Look for a trap that contradicts the given state, create and add a constraint to the known traps if found.
+     * @param net the net
+     * @param state the solution on SAT of the problem
+     * @param known the known traps to add to
+     * @param solver the solver state
+     * @return true if a new trap was found
+     */
+    private boolean findTrap(ISparsePetriNet net, CandidateSolution solution, StaticRefiner known, SolverState solver) {
         boolean trapFound = false;
         
+        SparseIntArray state = solution.getState();
 		if (state == null || state.size() == 0) {
 			return false;
 		}
@@ -109,17 +124,23 @@ private boolean findTrap(ISparsePetriNet net, SparseIntArray state, StaticRefine
             IFactory ef = solver.getSMT().smtConfig.exprFactory;
             List<IExpr> vars = trap.stream().map(n -> ef.symbol("s"+n)).collect(Collectors.toList());
             IExpr sum = buildSum(vars);
-            ICommand constraint = new C_assert(ef.fcn(ef.symbol(">="), sum , ef.numeral(1)));
-            VarSet support = new VarSet();
-            for (Integer p : trap) {
-            	support.addVar("s", p);
-            }
+            IExpr trapPredicate = ef.fcn(ef.symbol(">="), sum , ef.numeral(1));
+            VarSet support = computeSupport(trap);
+            ICommand constraint = new C_assert(trapPredicate);            
             known.addConstraint(new SMTConstraint(constraint, support));
             trapFound = true;
         }
         return trapFound;
     }
 
+	public VarSet computeSupport(List<Integer> trap) {
+		VarSet support = new VarSet();
+		for (Integer p : trap) {
+			support.addVar("s", p);
+		}
+		return support;
+	}
+
 
     @Override
     public void reset() {