diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-01-18 20:52:02 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-01-18 20:52:02 +0100 |
| commit | 5a5c643f127c44bfb86fe5c417db7bc561398499 (patch) | |
| tree | c90b22b03589b6f9287f674faf6861fffdb014ed /mppa_k1c | |
| parent | 017d67d668d47fc67038226939653889814cbcac (diff) | |
| download | compcert-kvx-5a5c643f127c44bfb86fe5c417db7bc561398499.tar.gz compcert-kvx-5a5c643f127c44bfb86fe5c417db7bc561398499.zip | |
fix bug when using reoptimization (sat4j)
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/InstructionScheduler.ml | 22 |
1 files 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 |