diff --git a/src_colibri2/bin/options.ml b/src_colibri2/bin/options.ml
index 50976d773f7dd5b9f089ad298fe74213abf1beb2..a386e155166adf712a5d6d02ee5e8c0d11044238 100644
--- a/src_colibri2/bin/options.ml
+++ b/src_colibri2/bin/options.ml
@@ -50,7 +50,7 @@ let gc_opts minor_heap_size major_heap_increment space_overhead max_overhead
let mk_state theories gc gc_opt bt colors time_limit size_limit input_lang
input_mode input header_check header_licenses header_lang_version type_check
type_strict debug context max_warn step_limit debug_flags show_steps
- check_status dont_print_result learning limit_last_effort =
+ check_status dont_print_result learning limit_last_effort options =
let last_effort_limit =
match limit_last_effort with
| None -> None
@@ -75,7 +75,7 @@ let mk_state theories gc gc_opt bt colors time_limit size_limit input_lang
( Colibri2_solver.Input.mk_state ~gc ~gc_opt ~bt ~colors ~time_limit
~size_limit ?input_lang ?input_mode ~input ~header_check ~header_licenses
~header_lang_version ~type_check ~type_strict ~debug ~context ~max_warn
- theories ~learning ?step_limit ?last_effort_limit,
+ theories ~learning ?step_limit ?last_effort_limit ~options,
show_steps,
check_status,
not dont_print_result )
@@ -455,9 +455,11 @@ let state theories =
& opt (some c_limit_last_effort) None
& info [ "limit-last-effort" ] ~docs ~doc)
in
+ let other_options = Colibri2_core.ForSchedulers.Options.parser () in
Term.(
const (mk_state theories)
$ gc $ gc_t $ bt $ colors $ time $ size $ in_lang $ in_mode $ input
$ header_check $ header_licenses $ header_lang_version $ typing $ strict
$ debug $ context $ max_warn $ step_limit $ debug_flags $ show_steps
- $ check_status $ dont_print_result $ learning $ last_effort_limit)
+ $ check_status $ dont_print_result $ learning $ last_effort_limit
+ $ other_options)
diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index 95cca039e3abaa0be926223d58f93998a11271e8..7d0123c9d207617879df07b872ec576aa01bb31f 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -250,6 +250,8 @@ module ForSchedulers = struct
let get_event_priority = Events.Wait.get_priority
let flush_internal = Egraph.flush_internal
+
+ module Options = Options
end
module Choice = struct
@@ -269,3 +271,5 @@ module Choice = struct
module Group = Choice_group
end
+
+module Options = Options
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index 8743ba99bf2ca6e8649960629a418e83aae45521..20578036de813de2189e12835136864e058fa04b 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -1650,6 +1650,15 @@ module Debug : sig
val decr : int stat -> unit
end
+module Options : sig
+ type 'a t
+
+ val register : ?pp:'a Fmt.t -> string -> 'a Cmdliner.Term.t -> 'a t
+ (** Register a new option *)
+
+ val get : _ Egraph.t -> 'a t -> 'a
+end
+
(** {3 For schedulers} *)
(** The following functions are necessary only to the scheduler *)
@@ -1706,4 +1715,14 @@ module ForSchedulers : sig
(** Add a level of decision for fixing the model, another level could be
needed. Could raise unsatisfiable if all the model have been tried *)
end
+
+ module Options : sig
+ type options
+
+ val set_egraph : _ Egraph.t -> options -> unit
+
+ val parser : unit -> options Cmdliner.Term.t
+
+ val default_options : unit -> options
+ end
end
diff --git a/src_colibri2/core/dune b/src_colibri2/core/dune
index b258dddedc50d2f414b7bc6226c13296f5ea3605..a8235e738498a16dcde303952e863ad2c21bd97a 100644
--- a/src_colibri2/core/dune
+++ b/src_colibri2/core/dune
@@ -2,7 +2,7 @@
(name colibri2_core)
(public_name colibri2.core)
(synopsis "core for colibri2, e.g. trail, egraph")
- (libraries containers ocamlgraph str colibri2.stdlib colibri2.popop_lib dolmen.std dolmen_loop)
+ (libraries containers ocamlgraph str colibri2.stdlib colibri2.popop_lib dolmen.std dolmen_loop cmdliner)
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
diff --git a/src_colibri2/core/options.ml b/src_colibri2/core/options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e09f16ce0ad75b8ded4caf5fedcf995e04124afc
--- /dev/null
+++ b/src_colibri2/core/options.ml
@@ -0,0 +1,51 @@
+module K = Keys.Make_key ()
+
+module Data = struct
+ type 'a data = { cmd : 'a Cmdliner.Term.t; id : 'a K.t; pp : 'a Fmt.t }
+
+ let pp d = d.pp
+
+ let key d = d.id
+end
+
+module Reg = K.Make_Registry (Data)
+
+type 'a t = 'a K.t
+
+let register (type a) ?(pp = Fmt.nop) name (cmd : a Cmdliner.Term.t) =
+ let id =
+ K.create
+ (module struct
+ type t = a
+
+ let name = name
+ end)
+ in
+ Reg.register { cmd; id; pp };
+ id
+
+module KM = K.MkMap (struct
+ type ('a, 'b) t = 'a
+end)
+
+let env = Datastructure.Ref.create Fmt.nop "Core.Options" KM.empty
+
+let get d k = KM.find k (Datastructure.Ref.get env d)
+
+type options = unit KM.t
+
+let set m k v = KM.add k v m
+
+let parser () : options Cmdliner.Term.t =
+ let fold acc data =
+ Cmdliner.Term.(
+ pure (fun acc v -> set acc data.Data.id v) $ acc $ data.Data.cmd)
+ in
+ Reg.fold_initialized { fold } (Cmdliner.Term.const KM.empty)
+
+let set_egraph d m = Datastructure.Ref.set env d m
+
+let default_options () =
+ match Cmdliner.Term.eval_peek_opts ~argv:[| "colibri2" |] (parser ()) with
+ | Some r, _ -> r
+ | None, _ -> invalid_arg "Some options are not optional"
diff --git a/src_colibri2/core/options.mli b/src_colibri2/core/options.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cce31384391b9d63d0a4a9a65d7d3fbbd5e3a879
--- /dev/null
+++ b/src_colibri2/core/options.mli
@@ -0,0 +1,35 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+type 'a t
+
+val register : ?pp:'a Fmt.t -> string -> 'a Cmdliner.Term.t -> 'a t
+
+val get : _ Egraph.t -> 'a t -> 'a
+
+type options
+
+val set : options -> 'a t -> 'a -> options
+
+val parser : unit -> options Cmdliner.Term.t
+
+val set_egraph : _ Egraph.t -> options -> unit
+
+val default_options : unit -> options
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index 434729d7e5aedcdcb01ff50973a830f7431d9615..e69459bceb139d8207e06bef2dff4852d20f0469 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -47,8 +47,8 @@ let pp_status_colibri fmt = function
| `Unsat -> Fmt.pf fmt "unsat"
| `StepLimitReached -> Fmt.pf fmt "step limit reached"
-let create_ctx ?step_limit ?last_effort_limit learning theories =
- let t = Scheduler.new_solver ~learning ?last_effort_limit () in
+let create_ctx ?step_limit ?last_effort_limit ?options learning theories =
+ let t = Scheduler.new_solver ~learning ?last_effort_limit ?options () in
let ctx = Scheduler.get_context t in
Scheduler.init_theories t ~theories;
{
@@ -435,7 +435,8 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
?input_lang ?input_mode ~input ?(header_check = false)
?(header_licenses = []) ?(header_lang_version = None) ?(type_check = true)
?(type_strict = true) ?(debug = false) ?(context = true)
- ?(max_warn = max_int) ?(learning = false) ?last_effort_limit theories =
+ ?(max_warn = max_int) ?(learning = false) ?last_effort_limit ?options
+ theories =
(* Side-effects *)
let () = Gc.set gc_opt in
let () =
@@ -466,7 +467,8 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
type_check;
type_strict;
type_state = Dolmen_loop.Typer.new_state ();
- solve_state = create_ctx ?step_limit ?last_effort_limit learning theories;
+ solve_state =
+ create_ctx ?step_limit ?last_effort_limit ?options learning theories;
export_lang = [];
}
in
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 03dd7d3327daff3995ae07fdf8fe57202702be89..bb681d9dce497df4921ae14baf5506904e6b4545 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -233,7 +233,8 @@ let get_steps t = t.steps
* var_inc = t.var_inc
* } *)
-let new_solver ~learning ?last_effort_limit () =
+let new_solver ~learning ?last_effort_limit
+ ?(options = Options.default_options ()) () =
let context = Context.create () in
let creator = Context.creator context in
let daemon_count = ref (-1) in
@@ -281,6 +282,9 @@ let new_solver ~learning ?last_effort_limit () =
Prio.insert t.choices dec ~added_at:(-1)
in
Backtrackable.set_sched ~sched_daemon ~sched_decision t.solver_state;
+ let d = Backtrackable.get_delayed t.solver_state in
+ Options.set_egraph d options;
+ Backtrackable.delayed_stop t.solver_state;
t
let push kind t =
@@ -770,9 +774,9 @@ let check_sat ?step_limit t =
if Backtrackable.get_unknown t.solver_state then `Unknown d else `Sat d
with Contradiction -> `Unsat
-let run_exn ?nodec ?step_limit ?last_effort_limit ?(learning = false) ~theories
- f =
- let t = new_solver ~learning ?last_effort_limit () in
+let run_exn ?nodec ?step_limit ?last_effort_limit ?(learning = false) ?options
+ ~theories f =
+ let t = new_solver ~learning ?last_effort_limit ?options () in
init_theories ~theories t;
let check = add_assertion t f in
flush t;
@@ -780,8 +784,8 @@ let run_exn ?nodec ?step_limit ?last_effort_limit ?(learning = false) ~theories
let d = Backtrackable.get_delayed t.solver_state in
check d
-let run ?nodec ?step_limit ?last_effort_limit ~theories f =
- try `Done (run_exn ?nodec ?step_limit ?last_effort_limit ~theories f)
+let run ?nodec ?step_limit ?last_effort_limit ?options ~theories f =
+ try `Done (run_exn ?nodec ?step_limit ?last_effort_limit ?options ~theories f)
with Contradiction -> `Contradiction
let pop_to st bp = ignore (pop_to st bp)
diff --git a/src_colibri2/solver/scheduler.mli b/src_colibri2/solver/scheduler.mli
index ce31fa15d0fb26300474affc2c594c82816aac2b..42d85deb21415578f38804a9f8accb446265c68e 100644
--- a/src_colibri2/solver/scheduler.mli
+++ b/src_colibri2/solver/scheduler.mli
@@ -29,6 +29,7 @@ val run_exn :
?step_limit:int ->
?last_effort_limit:last_effort_limit ->
?learning:bool ->
+ ?options:ForSchedulers.Options.options ->
theories:(Egraph.wt -> unit) list ->
(Egraph.wt -> Egraph.wt -> 'a) ->
'a
@@ -43,6 +44,7 @@ val run :
?nodec:unit ->
?step_limit:int ->
?last_effort_limit:last_effort_limit ->
+ ?options:ForSchedulers.Options.options ->
theories:(Egraph.wt -> unit) list ->
(Egraph.wt -> Egraph.wt -> 'a) ->
[> `Contradiction | `Done of 'a ]
@@ -50,7 +52,11 @@ val run :
type t
val new_solver :
- learning:bool -> ?last_effort_limit:last_effort_limit -> unit -> t
+ learning:bool ->
+ ?last_effort_limit:last_effort_limit ->
+ ?options:ForSchedulers.Options.options ->
+ unit ->
+ t
val init_theories : theories:(Egraph.wt -> unit) list -> t -> unit
diff --git a/src_colibri2/stdlib/keys.ml b/src_colibri2/stdlib/keys.ml
index bcd44d0c3e98f13010abcb565b07141c4c66c867..873e56c320f165db891c63273b8d1e77ebcc271e 100644
--- a/src_colibri2/stdlib/keys.ml
+++ b/src_colibri2/stdlib/keys.ml
@@ -147,6 +147,11 @@ module Make_key(X:sig end) = struct
let print (type a) (k : a t) fmt s =
let data = get k in
S.pp data fmt s
+
+ type ('b,'c) fold_initialized = ('b,'c) V.fold_initialized = { fold: 'a. 'c -> 'a data -> 'c }
+ let fold_initialized f acc = V.fold_initialized f acc registry
+ type 'b iter_initialized = 'b V.iter_initialized = { iter: 'a. 'a data -> unit }
+ let iter_initialized f = V.iter_initialized f registry
end
end
diff --git a/src_colibri2/stdlib/keys_sig.ml b/src_colibri2/stdlib/keys_sig.ml
index 68c1d4ce8c033253ec977eb8ee1b46ee9b5218d9..1cff4149009e34088856c3ba758782fc8246952d 100644
--- a/src_colibri2/stdlib/keys_sig.ml
+++ b/src_colibri2/stdlib/keys_sig.ml
@@ -41,6 +41,10 @@ module type Registry = sig
val is_well_initialized : unit -> bool
val get : 'a key -> 'a data
val print : 'a key -> 'a Format.printer
+ type 'b iter_initialized = { iter: 'a. 'a data -> unit }
+ val iter_initialized : unit iter_initialized -> unit
+ type ('b,'c) fold_initialized = { fold: 'a. 'c -> 'a data -> 'c }
+ val fold_initialized : (unit,'c) fold_initialized -> 'c -> 'c
(** the key shouldn't be used before its registration and shouldn't be
registered again *)
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 1ab90f49265458cea1a99edcacf56b4709f319bc..7aaa3bba203c27e744198fd015c3c1538a34f325 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -21,11 +21,18 @@
open Colibri2_core
module RealValue = RealValue
+let fourier_option =
+ Options.register ~pp:Fmt.bool "LRA.fourier"
+ Cmdliner.Arg.(
+ value & flag
+ & info [ "lra-fourier" ]
+ ~doc:"Use FourierMotskin engine instead of Simplex engine")
+
let th_register env =
Dom_interval.init env;
Dom_polynome.init env;
RealValue.init env;
- Simplex.init env;
+ (if Options.get env fourier_option then Fourier.init else Simplex.init) env;
Mul.init env;
Dom_product.init env;
()