From 0fcf8ee246c94dbeed9421937955792e6af5417c Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Fri, 18 Nov 2022 14:50:18 +0100
Subject: [PATCH] Fix build
---
colibri2/bin/options.ml | 13 +--
colibri2/solver/input.ml | 2 +-
colibri2/stdlib/debug.ml | 63 +++++++---
colibri2/stdlib/flags.ml | 65 -----------
colibri2/stdlib/flags.mli | 15 ---
colibri2/stdlib/std_sig.ml | 17 ---
.../LRA/stages/compare_stage/compare_stage.ml | 6 +
.../theories/LRA/stages/stage1/interval.ml | 39 ++++++-
colibri2/theories/array/array.ml | 110 +++++++++---------
colibrics/bin/loop.ml | 2 +-
10 files changed, 152 insertions(+), 180 deletions(-)
delete mode 100644 colibri2/stdlib/flags.ml
delete mode 100644 colibri2/stdlib/flags.mli
diff --git a/colibri2/bin/options.ml b/colibri2/bin/options.ml
index 54b90bc2d..bb0f7552c 100644
--- a/colibri2/bin/options.ml
+++ b/colibri2/bin/options.ml
@@ -48,7 +48,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
- debug max_warn step_limit debug_flags flags show_steps check_status
+ debug max_warn step_limit debug_flags show_steps check_status
dont_print_result learning limit_last_effort print_success negate_goal
options =
let last_effort_limit =
@@ -67,11 +67,8 @@ let mk_state theories gc gc_opt bt colors time_limit size_limit input_lang
(int_of_float (f *. float step_limit))))
in
List.iter
- Colibri2_stdlib.Flags.Debug.(fun s -> set_flag (lookup_flag s))
+ Colibri2_stdlib.Debug.(fun s -> set_flag (lookup_flag s))
debug_flags;
- List.iter
- Colibri2_stdlib.Flags.Solve.(fun s -> set_flag (lookup_flag s))
- flags;
(if debug then
Colibri2_stdlib.Debug.(
List.iter (fun (_, f, info, _) -> if info then set_flag f) (list_flags ())));
@@ -385,10 +382,6 @@ let state theories =
let doc = Format.asprintf "Debug flags." in
Arg.(value & opt_all string [] & info [ "debug-flag" ] ~docs ~doc)
in
- let flags =
- let doc = Format.asprintf "Solving flags." in
- Arg.(value & opt_all string [] & info [ "flag" ] ~docs ~doc)
- in
let check_status =
let doc =
Format.asprintf
@@ -454,6 +447,6 @@ let state theories =
const (mk_state theories)
$ gc $ gc_t $ bt $ colors $ time $ size $ in_lang $ in_mode $ input
$ header_check $ header_licenses $ header_lang_version $ typing $ debug
- $ max_warn $ step_limit $ debug_flags $ flags $ show_steps $ check_status
+ $ max_warn $ step_limit $ debug_flags $ show_steps $ check_status
$ dont_print_result $ learning $ last_effort_limit $ print_success
$ negate_goal $ other_options)
diff --git a/colibri2/solver/input.ml b/colibri2/solver/input.ml
index 3251c303a..8403567b3 100644
--- a/colibri2/solver/input.ml
+++ b/colibri2/solver/input.ml
@@ -96,7 +96,7 @@ let reset_ctx env =
env.state <- `Search;
env.pushpop <- []
-let solver_state = Dolmen_loop.State.create_key "solver_state"
+let solver_state = Dolmen_loop.State.create_key "solver_state" ~pipe:""
let get_state = Dolmen_loop.State.get solver_state
let split_input = function
diff --git a/colibri2/stdlib/debug.ml b/colibri2/stdlib/debug.ml
index 3bab44b25..8ad188f34 100644
--- a/colibri2/stdlib/debug.ml
+++ b/colibri2/stdlib/debug.ml
@@ -26,37 +26,62 @@ let () =
print_endline "Stopped by user";
exit 1))
-type flag = Flags.flag
+exception UnknownFlag of string
-let _true = Flags._true
-
-include Flags.Debug
+type flag = bool ref
+let _true = ref true
let todo = _true
+let modifiable s = not (Base.phys_equal s _true)
+let flag_table = Hashtbl.create 17
+let fst3 (flag, _, _) = flag
+let snd3 (_, info, _) = info
+let thd3 (_, _, desc) = desc
let gen_register_flag (desc : (unit, unit, unit, unit, unit, unit) format6) s
info =
- gen_register_flag ~rep:(fun flag -> (flag, info, desc)) s
+ try fst3 (Hashtbl.find flag_table s)
+ with Not_found ->
+ let flag = ref false in
+ Hashtbl.replace flag_table s (flag, info, desc);
+ flag
let register_info_flag ~desc s = gen_register_flag desc s true
let register_flag ~desc s = gen_register_flag desc s false
-let list_flags () = map_list (fun s (f, i, d) -> (s, f, i, d))
+
+let list_flags () =
+ Hashtbl.fold
+ (fun s (v, info, desc) acc -> (s, v, info, desc) :: acc)
+ flag_table []
+
+let lookup_flag s =
+ try fst3 (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s)
let is_info_flag s =
- match lookup s with
- | _, i, _ -> i
- | exception Not_found -> raise (Flags.UnknownFlag s)
+ try snd3 (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s)
let flag_desc s =
- match lookup s with
- | _, _, desc -> desc
- | exception Not_found -> raise (Flags.UnknownFlag s)
+ try thd3 (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s)
+
+let test_flag s = !s
+let test_noflag s = not !s
+
+let set_flag s =
+ assert (modifiable s);
+ s := true
+
+let unset_flag s =
+ assert (modifiable s);
+ s := false
+
+let toggle_flag s =
+ assert (modifiable s);
+ s := not !s
let () =
Printexc.register_printer (fun e ->
match e with
- | Flags.UnknownFlag s ->
- Some (Format.asprintf "unknown debug flag `%s'" s)
+ | UnknownFlag s -> Some (Format.asprintf "unknown debug flag `%s'" s)
| _ -> None)
let stack_trace =
@@ -198,7 +223,11 @@ module Args = struct
in
let list () =
(if !opt_list_flags then
- let list = map_list (fun s (_, info, desc) -> (s, info, desc)) in
+ let list =
+ Hashtbl.fold
+ (fun s (_, info, desc) acc -> (s, info, desc) :: acc)
+ flag_table []
+ in
let pp fmt (p, info, desc) =
Format.fprintf fmt "@[%s%s @[%( %)@]@]" p
(if info then " *" else "")
@@ -216,7 +245,9 @@ module Args = struct
let opt_list_flags = ref []
let add_flag s = opt_list_flags := s :: !opt_list_flags
- let add_all_flags () = iter (fun s (_, info, _) -> if info then add_flag s)
+
+ let add_all_flags () =
+ Hashtbl.iter (fun s (_, info, _) -> if info then add_flag s) flag_table
let remove_flag s =
opt_list_flags :=
diff --git a/colibri2/stdlib/flags.ml b/colibri2/stdlib/flags.ml
deleted file mode 100644
index 0763cc51d..000000000
--- a/colibri2/stdlib/flags.ml
+++ /dev/null
@@ -1,65 +0,0 @@
-type flag = bool ref
-
-let _true = ref true
-let todo = _true
-let modifiable s = not (Base.phys_equal s _true)
-
-exception UnknownFlag of string
-
-let () =
- Printexc.register_printer (fun e ->
- match e with
- | UnknownFlag s -> Some (Format.asprintf "unknown debug flag `%s'" s)
- | _ -> None)
-
-module Make (S : sig
- type t
-
- val flag : t -> bool ref
-end) : Std_sig.Flags with type t = S.t = struct
- type t = S.t
-
- let table : (string, t) Hashtbl.t = Hashtbl.create 17
-
- let gen_register_flag ~rep s =
- try S.flag (Hashtbl.find table s)
- with Not_found ->
- let flag = ref false in
- Hashtbl.replace table s (rep flag);
- flag
-
- let lookup s = Hashtbl.find table s
-
- let lookup_flag s =
- try S.flag (lookup s) with Not_found -> raise (UnknownFlag s)
-
- let to_list () = Hashtbl.fold (fun s v acc -> (s, v) :: acc) table []
- let iter f = Hashtbl.iter f table
- let map_list f = Hashtbl.map_list f table
- let test_flag s = !s
- let test_noflag s = not !s
-
- let set_flag s =
- assert (modifiable s);
- s := true
-
- let unset_flag s =
- assert (modifiable s);
- s := false
-
- let toggle_flag s =
- assert (modifiable s);
- s := not !s
-end
-
-module Debug = Make (struct
- type t = flag * bool * (unit, unit, unit, unit, unit, unit) format6
-
- let flag ((f, _, _) : t) = f
-end)
-
-module Solve = Make (struct
- type t = flag * (unit, unit, unit, unit, unit, unit) format6
-
- let flag ((f, _) : t) = f
-end)
diff --git a/colibri2/stdlib/flags.mli b/colibri2/stdlib/flags.mli
deleted file mode 100644
index b129948c6..000000000
--- a/colibri2/stdlib/flags.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-type flag = bool ref
-
-val _true : bool ref
-val todo : bool ref
-val modifiable : bool ref -> bool
-
-exception UnknownFlag of string
-
-module Debug :
- Std_sig.Flags
- with type t = flag * bool * (unit, unit, unit, unit, unit, unit) format6
-
-module Solve :
- Std_sig.Flags
- with type t = flag * (unit, unit, unit, unit, unit, unit) format6
diff --git a/colibri2/stdlib/std_sig.ml b/colibri2/stdlib/std_sig.ml
index b4ad085b4..41076deb8 100644
--- a/colibri2/stdlib/std_sig.ml
+++ b/colibri2/stdlib/std_sig.ml
@@ -45,20 +45,3 @@ end
* and type M.key = M.key
* module H : Exthtbl.Hashtbl.S with type key = t
* end *)
-
-module type Flags = sig
- type t
-
- val table : (string, t) Hashtbl.t
- val gen_register_flag : rep:(bool ref -> t) -> string -> bool ref
- val lookup : string -> t
- val lookup_flag : string -> bool ref
- val to_list : unit -> (string * t) list
- val iter : (string -> t -> unit) -> unit
- val map_list : (string -> t -> 'a) -> 'a list
- val test_flag : 'a ref -> 'a
- val test_noflag : bool ref -> bool
- val set_flag : bool ref -> unit
- val unset_flag : bool ref -> unit
- val toggle_flag : bool ref -> unit
-end
diff --git a/colibri2/theories/LRA/stages/compare_stage/compare_stage.ml b/colibri2/theories/LRA/stages/compare_stage/compare_stage.ml
index 024529049..798a68867 100644
--- a/colibri2/theories/LRA/stages/compare_stage/compare_stage.ml
+++ b/colibri2/theories/LRA/stages/compare_stage/compare_stage.ml
@@ -178,4 +178,10 @@ module Cmp (S1 : S) (S2 : S) : S = struct
let open Base.Option in
S1.reduce_integers s1 >>= fun s1 ->
S2.reduce_integers s2 >>| fun s2 -> { s1; s2 }
+
+ let neg { s1; s2 } = { s1 = S1.neg s1; s2 = S2.neg s2 }
+ let floor { s1; s2 } = { s1 = S1.floor s1; s2 = S2.floor s2 }
+ let ceil { s1; s2 } = { s1 = S1.ceil s1; s2 = S2.ceil s2 }
+ let truncate { s1; s2 } = { s1 = S1.truncate s1; s2 = S2.truncate s2 }
+ let relu { s1; s2 } = { s1 = S1.relu s1; s2 = S2.relu s2 }
end
diff --git a/colibri2/theories/LRA/stages/stage1/interval.ml b/colibri2/theories/LRA/stages/stage1/interval.ml
index 0980283d5..02bfa9eb5 100644
--- a/colibri2/theories/LRA/stages/stage1/interval.ml
+++ b/colibri2/theories/LRA/stages/stage1/interval.ml
@@ -40,6 +40,7 @@ module Convexe = struct
let of_int = A.of_bigint
let floor a = A.to_z (A.floor a)
let ceil a = A.to_z (A.ceil a)
+ let truncate a = A.to_z (truncate a)
end)
include Convexe
@@ -151,6 +152,38 @@ module Convexe = struct
let q2 = ceilb q2 b2 in
if A.lt q2 q1 then None else Some (Finite (q1, Large, q2, Large))
+ let truncate = function
+ | Finite (q1, b1, q2, b2) -> Finite (A.truncate q1, b1, A.truncate q2, b2)
+ | InfFinite (q, b) -> InfFinite (A.truncate q, b)
+ | FiniteInf (q, b) -> FiniteInf (A.truncate q, b)
+ | Inf -> Inf
+
+ let neg = function
+ | Finite (q1, b1, q2, b2) -> Finite (A.neg q2, b2, A.neg q1, b1)
+ | InfFinite (q, b) -> FiniteInf (A.neg q, b)
+ | FiniteInf (q, b) -> InfFinite (A.neg q, b)
+ | Inf -> Inf
+
+ let floor = function
+ | Finite (q1, b1, q2, b2) -> Finite (A.floor q1, b1, A.floor q2, b2)
+ | InfFinite (q, b) -> InfFinite (A.floor q, b)
+ | FiniteInf (q, b) -> FiniteInf (A.floor q, b)
+ | Inf -> Inf
+
+ let ceil = function
+ | Finite (q1, b1, q2, b2) -> Finite (A.ceil q1, b1, A.ceil q2, b2)
+ | InfFinite (q, b) -> InfFinite (A.ceil q, b)
+ | FiniteInf (q, b) -> FiniteInf (A.ceil q, b)
+ | Inf -> Inf
+
+ let a_relu a = if A.ge a A.zero then a else A.zero
+
+ let relu = function
+ | Finite (q1, b1, q2, b2) -> Finite (a_relu q1, b1, a_relu q2, b2)
+ | InfFinite (q, b) -> InfFinite (a_relu q, b)
+ | FiniteInf (q, b) -> FiniteInf (a_relu q, b)
+ | Inf -> Inf
+
(* let nb_incr = 100
* let z_nb_incr = Z.of_int nb_incr
* let choose_rnd rnd = function
@@ -167,7 +200,7 @@ module Convexe = struct
* assert (A.lt minv q);
* assert (A.lt q maxv);
* q
- *
+ *
* let get_convexe_hull e =
* let mk v b =
* match A.classify v with
@@ -175,11 +208,11 @@ module Convexe = struct
* | A.INF | A.MINF -> None
* | A.UNDEF -> assert false in
* mk e.minv e.minb, mk e.maxv e.maxb
- *
+ *
* let is_Large = function
* | Large -> true
* | Strict -> false
- *
+ *
* let inter_with_integer t =
* let t = {
* minb = if A.equal A.minus_inf t.minv then Large else Strict;
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 4a753b9b2..79f947017 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -23,24 +23,25 @@ open Colibri2_core
open Colibri2_popop_lib
let restrict_ext =
- Colibri2_stdlib.Flags.Solve.gen_register_flag
- ~rep:(fun flag -> (flag, "Restrict the extensionality rule"))
- "Array.res-ext"
+ Options.register ~pp:Fmt.bool "Array.res-ext"
+ Cmdliner.Arg.(
+ value & flag
+ & info [ "array-res-ext" ] ~doc:"Restrict the extensionality rule")
let restrict_aup =
- Colibri2_stdlib.Flags.Solve.gen_register_flag
- ~rep:(fun flag -> (flag, "Restrict the ⇑ rule"))
- "Array.res-aup"
+ Options.register ~pp:Fmt.bool "Array.res-ext"
+ Cmdliner.Arg.(
+ value & flag & info [ "array-res-aup" ] ~doc:"Restrict the ⇑ rule")
let extended_comb =
- Colibri2_stdlib.Flags.Solve.gen_register_flag
- ~rep:(fun flag -> (flag, "Extended combinators"))
- "Array.ext-comb"
+ Options.register ~pp:Fmt.bool "Array.res-ext"
+ Cmdliner.Arg.(
+ value & flag & info [ "array-ext-comb" ] ~doc:"Extended combinators")
let default_values =
- Colibri2_stdlib.Flags.Solve.gen_register_flag
- ~rep:(fun flag -> (flag, "Default values"))
- "Array.def-values"
+ Options.register ~pp:Fmt.bool "Array.def-values"
+ Cmdliner.Arg.(
+ value & flag & info [ "array-def-values" ] ~doc:"Default values")
let debug = Debug.register_info_flag ~desc:"For array theory" "Array"
let stats = Debug.register_stats_int "Array.rule"
@@ -60,6 +61,8 @@ let alpha_ty = Expr.Ty.of_var alpha_ty_var
let array_ty = Expr.Ty.array ind_ty val_ty
let bind_tys tyvl ty = Expr.Ty.pi tyvl ty
let replicate n v = List.init n (fun _ -> v)
+let mk_store_term = Expr.Term.Array.store
+let mk_select_term = Expr.Term.Array.select
(* Builtins *)
module Builtin = struct
@@ -213,14 +216,14 @@ module Theory = struct
[
Expr.Term.eq ta tb;
Expr.Term.neq
- (Expr.Term.select ta diff_term)
- (Expr.Term.select tb diff_term);
+ (mk_select_term ta diff_term)
+ (mk_select_term tb diff_term);
]
(* ⇓: a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)
let adown_pattern, adown_run =
- let a = Expr.Term.store tb ti tv in
- let term = Expr.Term.select a tj in
+ let a = mk_store_term tb ti tv in
+ let term = mk_select_term a tj in
let adown_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let adown_run env subst =
Debug.dprintf2 debug "Found adown with %a" Ground.Subst.pp subst;
@@ -230,7 +233,7 @@ module Theory = struct
(Expr.Term._or
[
Expr.Term.eq ti tj;
- Expr.Term.eq (Expr.Term.select a tj) (Expr.Term.select tb tj);
+ Expr.Term.eq (mk_select_term a tj) (mk_select_term tb tj);
])
in
Egraph.register env n;
@@ -241,13 +244,13 @@ module Theory = struct
(* ⇑: a ≡ b[i <- v], b[j] |> (i = j) \/ a[j] = b[j] *)
let aup_pattern, aup_run =
- let term = Expr.Term.store tb ti tv in
+ let term = mk_store_term tb ti tv in
let aup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let aup_run env subst =
let n = convert ~subst env term in
Egraph.register env n;
Debug.dprintf2 debug "Found aup1 with %a" Ground.Subst.pp subst;
- let term_bis = Expr.Term.select tb tj in
+ let term_bis = mk_select_term tb tj in
let aup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
let aup_run_bis env subst_bis =
Debug.incr stats;
@@ -258,8 +261,7 @@ module Theory = struct
(Expr.Term._or
[
Expr.Term.eq ti tj;
- Expr.Term.eq (Expr.Term.select term tj)
- (Expr.Term.select tb tj);
+ Expr.Term.eq (mk_select_term term tj) (mk_select_term tb tj);
])
in
Egraph.register env v;
@@ -302,13 +304,13 @@ module Theory = struct
(* ⇑ᵣ: a ≡ b[i <- v], b[j], b ∈ non-linear |> (i = j) \/ a[j] = b[j] *)
let raup_pattern, raup_run =
- let term = Expr.Term.store tb ti tv in
+ let term = mk_store_term tb ti tv in
let raup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let raup_run env subst =
Debug.dprintf2 debug "Found raup1 with %a" Ground.Subst.pp subst;
let n = convert ~subst env term in
Egraph.register env n;
- let term_bis = Expr.Term.select tb tj in
+ let term_bis = mk_select_term tb tj in
let raup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
let raup_run_bis env subst_bis =
Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst;
@@ -320,8 +322,7 @@ module Theory = struct
(Expr.Term._or
[
Expr.Term.eq ti tj;
- Expr.Term.eq (Expr.Term.select term tj)
- (Expr.Term.select tb tj);
+ Expr.Term.eq (mk_select_term term tj) (mk_select_term tb tj);
])
in
Egraph.register env v;
@@ -339,7 +340,7 @@ module Theory = struct
Debug.dprintf2 debug "Found const1 with %a" Ground.Subst.pp subst;
let n = convert ~subst env term in
Egraph.register env n;
- let term_bis = Expr.Term.select term tj in
+ let term_bis = mk_select_term term tj in
let const_pattern_bis = Pattern.of_term_exn ~subst term_bis in
let const_run_bis env subst_bis =
Debug.dprintf2 debug "Found const2 with %a" Ground.Subst.pp subst;
@@ -354,19 +355,24 @@ module Theory = struct
let init env =
let l = [ (adown_pattern, adown_run) ] in
- let l = if !restrict_ext then (rext_pattern, rext_run) :: l else l in
let l =
- if !restrict_aup then (raup_pattern, raup_run) :: l
+ if Options.get env restrict_ext then (rext_pattern, rext_run) :: l else l
+ in
+ let l =
+ if Options.get env restrict_aup then (raup_pattern, raup_run) :: l
else (aup_pattern, aup_run) :: l
in
- let l = if !extended_comb then (const_pattern, const_run) :: l else l in
+ let l =
+ if Options.get env extended_comb then (const_pattern, const_run) :: l
+ else l
+ in
List.iter (fun (p, r) -> InvertedPath.add_callback env p r) l
let new_array =
let db = Datastructure.Push.create Ground.pp "Array.db" in
fun env s_index_ty s_value_ty f ->
(* Extensionality rule ext: a, b ⇒ (a = b) ⋠(a[k] ≠b[k]) *)
- if not !restrict_ext then (
+ if not (Options.get env restrict_ext) then (
Datastructure.Push.iter db env ~f:(fun f2 ->
let subst =
mk_subst
@@ -379,7 +385,7 @@ module Theory = struct
Boolean.set_true env n);
Datastructure.Push.push db env f);
(* ðð›¿: a |> a[ð] = 𛿠*)
- if !extended_comb then (
+ if Options.get env extended_comb then (
Debug.dprintf0 debug "Application of the epsilon_delta rule";
let subst =
mk_subst
@@ -389,7 +395,7 @@ module Theory = struct
let epsilon_app = apply_def_index ta in
let delta_app = apply_def_value ta in
let epsilon_delta_eq =
- Expr.Term.eq (Expr.Term.select ta epsilon_app) delta_app
+ Expr.Term.eq (mk_select_term ta epsilon_app) delta_app
in
let n = convert ~subst env epsilon_delta_eq in
Egraph.register env n;
@@ -408,17 +414,16 @@ module Theory = struct
(* map⇓: a = map(f, b1, ..., bn), a[j] |> a[j] = f(b1[j], ..., bn[j]) *)
let map_adowm map_term f_term bitl =
let map_read_pattern =
- Pattern.of_term_exn ~subst:Ground.Subst.empty
- (Expr.Term.select map_term tj)
+ Pattern.of_term_exn ~subst:Ground.Subst.empty (mk_select_term map_term tj)
in
let map_read_run env subst =
Debug.dprintf2 debug "Found array_map(f,b1, ..., bn)[j] with %a"
Ground.Subst.pp subst;
let term =
Expr.Term.eq
- (Expr.Term.select map_term tj)
+ (mk_select_term map_term tj)
(Expr.Term.apply f_term []
- (List.map (fun bi -> Expr.Term.select bi tj) bitl))
+ (List.map (fun bi -> mk_select_term bi tj) bitl))
in
let n = convert ~subst env term in
Egraph.register env n;
@@ -433,9 +438,9 @@ module Theory = struct
let map_run env subst =
Debug.dprintf2 debug "Found array_map(f,b1, ..., bn) with %a"
Ground.Subst.pp subst;
- if !extended_comb then (
+ if Options.get env extended_comb then (
Debug.dprintf0 debug "Application of the map_aup rule";
- let bkjl = List.map (fun bi -> Expr.Term.select bi tj) bitl in
+ let bkjl = List.map (fun bi -> mk_select_term bi tj) bitl in
let bkjl_patterns = List.map (Pattern.of_term_exn ~subst) bkjl in
let bkj_run =
let seen = ref false in
@@ -446,9 +451,9 @@ module Theory = struct
seen := true;
let term =
Expr.Term.eq
- (Expr.Term.select map_term tj)
+ (mk_select_term map_term tj)
(Expr.Term.apply f_term []
- (List.map (fun bi -> Expr.Term.select bi tj) bitl))
+ (List.map (fun bi -> mk_select_term bi tj) bitl))
in
let n = convert ~subst env term in
Egraph.register env n;
@@ -457,7 +462,7 @@ module Theory = struct
List.iter
(fun pattern -> InvertedPath.add_callback env pattern bkj_run)
bkjl_patterns);
- if !default_values then (
+ if Options.get env default_values then (
Debug.dprintf0 debug "Application of the map_delta rule";
let d_a = Expr.Term.apply_cst Builtin.array_default_value [] [ ta ] in
let d_bil =
@@ -493,7 +498,8 @@ module Theory = struct
in
let map_pattern, map_run = map_adowm map_term f_term bitl in
let map_read_pattern, map_read_run = map_adowm map_term f_term bitl in
- if !extended_comb then InvertedPath.add_callback env map_pattern map_run;
+ if Options.get env extended_comb then
+ InvertedPath.add_callback env map_pattern map_run;
InvertedPath.add_callback env map_read_pattern map_read_run)
end
@@ -510,10 +516,10 @@ let converter env (f : Ground.t) =
| { app = { builtin = Expr.Base; id_ty; _ }; args; tyargs; _ } ->
let fn = Ground.node f in
if IArray.is_empty args then (
- if !restrict_aup && f_is_array then
+ if Options.get env restrict_aup && f_is_array then
(* update of the Linearity domain *)
Linearity_dom.upd_dom env fn Empty)
- else if !restrict_ext then
+ else if Options.get env restrict_ext then
(* update of the Foreign domain *)
let subst, param_tys =
match id_ty.ty_descr with
@@ -545,7 +551,7 @@ let converter env (f : Ground.t) =
Egraph.register env i;
(* update of the Foreign domain *)
if
- !restrict_ext
+ Options.get env restrict_ext
&&
match s_ind_ty with
| { app = { builtin = Expr.Array; _ }; _ } -> true
@@ -554,7 +560,7 @@ let converter env (f : Ground.t) =
(* application of the `not default` rule ð≠: v = a[i], i ≠ð |> i ≠ð *)
(* should only be applied if the index sort is infinite,
otherwise the blast rule should be applied *)
- if !extended_comb then (
+ if Options.get env extended_comb then (
let subst =
mk_subst
[ (Theory.va, a); (Theory.vi, i) ]
@@ -581,22 +587,22 @@ let converter env (f : Ground.t) =
Egraph.register env k;
Egraph.register env v;
(* update of the Linearity domain *)
- if !restrict_aup then Linearity_dom.upd_dom env (Ground.node f) (Linear a);
+ if Options.get env restrict_aup then Linearity_dom.upd_dom env (Ground.node f) (Linear a);
(* application of the `idx` rule *)
let subst =
mk_subst
[ (Theory.va, a); (Theory.vk, k); (Theory.vv, v) ]
[ (ind_ty_var, s_ind_ty); (val_ty_var, s_val_ty) ]
in
- let store_term = Expr.Term.store Theory.ta Theory.tk Theory.tv in
+ let store_term = mk_store_term Theory.ta Theory.tk Theory.tv in
let rn =
convert ~subst env
- (Expr.Term.eq (Expr.Term.select store_term Theory.tk) Theory.tv)
+ (Expr.Term.eq (mk_select_term store_term Theory.tk) Theory.tv)
in
Egraph.register env rn;
Boolean.set_true env rn;
(* application of the `Uð›¿` rule *)
- if !default_values then (
+ if Options.get env default_values then (
let eq_term =
Expr.Term.eq (apply_def_value store_term) (apply_def_value Theory.ta)
in
@@ -616,7 +622,7 @@ let converter env (f : Ground.t) =
let v = IArray.extract1_exn args in
Egraph.register env v;
(* application of the `Kð›¿` rule *)
- if !default_values then (
+ if Options.get env default_values then (
let subst = mk_subst [ (Theory.vv, v) ] [ (val_ty_var, s_val_ty) ] in
let eq_node =
convert ~subst env
@@ -625,7 +631,7 @@ let converter env (f : Ground.t) =
Egraph.register env eq_node;
Boolean.set_true env eq_node)
| { app = { builtin = Builtin.Array_map; _ }; _ }
- when !extended_comb || !default_values ->
+ when Options.get env extended_comb || Options.get env default_values ->
Theory.new_map env f
| _ -> ()
diff --git a/colibrics/bin/loop.ml b/colibrics/bin/loop.ml
index 4d2b0111b..9717918fb 100644
--- a/colibrics/bin/loop.ml
+++ b/colibrics/bin/loop.ml
@@ -15,4 +15,4 @@ module Typer = struct
include Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(T)
end
-let solver_state : Dolmen_to_colibrics.t State.key = State.create_key "solver_state"
+let solver_state : Dolmen_to_colibrics.t State.key = State.create_key ~pipe:"" "solver_state"
--
GitLab