From d66abde730f70c7a278fa4fb2520239074c7134f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 26 Jan 2023 10:35:42 +0100
Subject: [PATCH] [Scheduler] add --no-fix-model mode
Stop with steplimitreached when getting to fix-model
---
colibri2/solver/scheduler.ml | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/colibri2/solver/scheduler.ml b/colibri2/solver/scheduler.ml
index fa881cd4a..222107b59 100644
--- a/colibri2/solver/scheduler.ml
+++ b/colibri2/solver/scheduler.ml
@@ -52,6 +52,12 @@ let stats_con_fix = Debug.register_stats_int "Scheduler.conflict_fix_model"
let stats_step = Debug.register_stats_int "Scheduler.step"
let stats_fix_model = Debug.register_stats_int "Scheduler.fix_model"
+let no_fixmodel_option =
+ Colibri2_core.Options.register ~pp:Fmt.bool "Scheduler.fixmodel"
+ Cmdliner.Arg.(
+ value & flag
+ & info [ "no-fix-model" ] ~doc:"Stop at the start of FixModel")
+
exception Contradiction
exception ReachStepLimit
@@ -657,7 +663,11 @@ let run_one_step ~nodec t =
Context.Ref.set t.solve_step step;
make_choice t choice choices;
true)
- | FixModel -> run_one_step_fix_model ~nodec t
+ | FixModel ->
+ let d = Backtrackable.get_delayed t.solver_state in
+ if Colibri2_core.Options.get d no_fixmodel_option then
+ raise ReachStepLimit;
+ run_one_step_fix_model ~nodec t
let rec flush t =
try Backtrackable.flush t.solver_state
--
GitLab