From 5a5c643f127c44bfb86fe5c417db7bc561398499 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 18 Jan 2019 20:52:02 +0100 Subject: fix bug when using reoptimization (sat4j) --- mppa_k1c/InstructionScheduler.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/mppa_k1c/InstructionScheduler.ml b/mppa_k1c/InstructionScheduler.ml index 394c5264..ae4296a2 100644 --- a/mppa_k1c/InstructionScheduler.ml +++ b/mppa_k1c/InstructionScheduler.ml @@ -735,7 +735,7 @@ let adjust_check_solution mapper solution = (* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/naps/naps" *) (* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/minisatp/build/release/bin/minisatp" *) -let pseudo_boolean_solver = ref "java -jar sat4j-pb.jar CuttingPlanesStar" +let pseudo_boolean_solver = ref "java -jar /opt/sat4j/sat4j-pb.jar CuttingPlanesStar" let pseudo_boolean_scheduler pb_type problem = try @@ -752,14 +752,18 @@ let pseudo_boolean_scheduler pb_type problem = | Unschedulable -> None;; let rec reoptimizing_scheduler (scheduler : scheduler) (previous_solution : solution) (problem : problem) = - Printf.printf "reoptimizing < %d\n" (get_max_latency previous_solution); - flush stdout; - match scheduler - { problem with max_latency = (get_max_latency previous_solution)-1 } - with - | None -> previous_solution - | Some solution -> reoptimizing_scheduler scheduler solution problem;; - + if (get_max_latency previous_solution) > 1 then + begin + Printf.printf "reoptimizing < %d\n" (get_max_latency previous_solution); + flush stdout; + match scheduler + { problem with max_latency = (get_max_latency previous_solution)-1 } + with + | None -> previous_solution + | Some solution -> reoptimizing_scheduler scheduler solution problem + end + else previous_solution;; + let cascaded_scheduler (problem : problem) = match validated_scheduler list_scheduler problem with | None -> None -- cgit