diff --git a/Makefile b/Makefile
index 7e960182f3bbea98549bf2cad5f016fd3ad59223..8b904d0f486664e8f7f0b953a19539ed572645ad 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@
##########################################################################
all:
- dune build --root=$$(pwd)
+ dune build --root=$$(pwd) @install
test:
dune runtest --root=$$(pwd)
diff --git a/src_colibri2/bin/dune b/src_colibri2/bin/dune
new file mode 100644
index 0000000000000000000000000000000000000000..88e93b1f91bc235181149288bf7d1ad893efa5c1
--- /dev/null
+++ b/src_colibri2/bin/dune
@@ -0,0 +1,29 @@
+(executable
+ (name main)
+ (public_name colibri2)
+ (libraries
+ ; external deps
+ cmdliner fmt gen
+ ; dolmen deps
+ dolmen dolmen.intf dolmen.std
+ dolmen_type dolmen_loop
+ ; colibrics
+ colibri2.solver
+ colibri2.theories.bool
+ colibri2.theories.LRA
+ )
+ (package colibri2)
+)
+
+; Rule to generate a man page for colibrics
+(rule
+ (target colibri2.1)
+ (action (with-outputs-to %{target} (run colibri2 --help=groff)))
+)
+
+; Install the man page
+(install
+ (files colibri2.1)
+ (section man)
+ (package colibri2)
+)
diff --git a/src_colibri2/bin/main.ml b/src_colibri2/bin/main.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5dc0bb5589b7d82f61a49d8295ce9181861fcd1e
--- /dev/null
+++ b/src_colibri2/bin/main.ml
@@ -0,0 +1,30 @@
+(* This file is free software, copied from dolmen. See file "LICENSE" for more information *)
+
+let theories =
+ [Colibri2_theories_bool.Boolean.th_register;
+ Colibri2_theories_bool.Equality.th_register;
+ Colibri2_theories_bool.Uninterp.th_register;
+ Colibri2_theories_LRA.LRA.th_register]
+
+let () =
+ let man = [
+ `S Options.common_section;
+ `P "Common options for the colibrics binary";
+ `S Options.gc_section;
+ `P "Options to fine-tune the gc, only experts should use these.";
+ `S Cmdliner.Manpage.s_bugs;
+ `P "You can report bugs at https://git.frama-c.com/";
+ `S Cmdliner.Manpage.s_authors;
+ `P "Francois Bobot <francois.bobot@cea.fr>"
+ ] in
+ let info = Cmdliner.Term.info ~man ~version:"0.1" "dolmen" in
+ let st,step_limit = match Cmdliner.Term.eval (Options.state theories, info) with
+ | `Version | `Help -> exit 0
+ | `Error `Parse | `Error `Term | `Error `Exn -> exit 2
+ | `Ok opt -> opt
+ in
+ Colibri2_solver.Input.read
+ ?limit:step_limit
+ ~set_true:Colibri2_theories_bool.Boolean.set_true
+ ~handle_exn:Colibri2_solver.Input.handle_exn_with_exit
+ st
diff --git a/src_colibri2/bin/options.ml b/src_colibri2/bin/options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..97beea19d407815042d140dc5240dba092eeec20
--- /dev/null
+++ b/src_colibri2/bin/options.ml
@@ -0,0 +1,301 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+open Cmdliner
+
+(* Sections *)
+(* ************************************************************************* *)
+
+let gc_section = "GC OPTIONS"
+let common_section = Manpage.s_options
+
+(* State creation *)
+(* ************************************************************************* *)
+
+let gc_opts
+ minor_heap_size major_heap_increment
+ space_overhead max_overhead allocation_policy =
+ Gc.({ (get ()) with
+ minor_heap_size; major_heap_increment;
+ space_overhead; max_overhead; allocation_policy;
+ }
+ )
+
+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
+ =
+ List.iter Colibri2_popop_lib.Debug.(fun s -> set_flag (lookup_flag s)) debug_flags;
+ if debug then
+ Colibri2_popop_lib.Debug.(
+ List.iter (fun (_,f,_,_) -> set_flag f) (list_flags ()));
+ 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, step_limit
+
+(* Input source converter *)
+(* ************************************************************************* *)
+
+(* Converter for input formats/languages *)
+let input_format_conv = Arg.enum Dolmen_loop.Logic.enum
+
+(* Converter for input file/stdin *)
+let input_to_string = function
+ | `Stdin -> "<stdin>"
+ | `Raw _ -> "<raw>"
+ | `File f -> f
+
+let input_source_conv =
+ let parse x = Ok (`File x) in
+ let print fmt i = Format.fprintf fmt "%s" (input_to_string i) in
+ Arg.conv (parse, print)
+
+(* Converter for permissions *)
+let perm_conv = Arg.enum [
+ "allow", Dolmen_loop.State.Allow;
+ "warn", Dolmen_loop.State.Warn;
+ "error", Dolmen_loop.State.Error;
+ ]
+
+(* Converter for input modes *)
+let mode_conv = Arg.enum [
+ "full", `Full;
+ "incremental", `Incremental;
+ ]
+
+(* Output converters *)
+(* ************************************************************************* *)
+
+let output_to_string = function
+ | `Stdout -> "<stdout>"
+ | `File f -> f
+
+let parse_output = function
+ | "stdout" -> Ok `Stdout
+ | f -> Ok (`File f)
+
+let output_conv =
+ let print fmt o = Format.fprintf fmt "%s" (output_to_string o) in
+ Arg.conv (parse_output, print)
+
+
+(* Argument converter for integer with multiplier suffix *)
+(* ************************************************************************ *)
+
+let nb_sec_minute = 60
+let nb_sec_hour = 60 * nb_sec_minute
+let nb_sec_day = 24 * nb_sec_hour
+
+let time_string f =
+ let n = int_of_float f in
+ let aux n div = n / div, n mod div in
+ let n_day, n = aux n nb_sec_day in
+ let n_hour, n = aux n nb_sec_hour in
+ let n_min, n = aux n nb_sec_minute in
+ let print_aux s n = if n <> 0 then (string_of_int n) ^ s else "" in
+ (print_aux "d" n_day) ^
+ (print_aux "h" n_hour) ^
+ (print_aux "m" n_min) ^
+ (print_aux "s" n)
+
+let print_time fmt f = Format.fprintf fmt "%s" (time_string f)
+
+let parse_time arg =
+ let l = String.length arg in
+ let multiplier m =
+ let arg1 = String.sub arg 0 (l-1) in
+ `Ok (m *. (float_of_string arg1))
+ in
+ assert (l > 0);
+ try
+ match arg.[l-1] with
+ | 's' -> multiplier 1.
+ | 'm' -> multiplier 60.
+ | 'h' -> multiplier 3600.
+ | 'd' -> multiplier 86400.
+ | '0'..'9' -> `Ok (float_of_string arg)
+ | _ -> `Error "bad numeric argument"
+ with Failure _ -> `Error "bad numeric argument"
+
+let size_string f =
+ let n = int_of_float f in
+ let aux n div = n / div, n mod div in
+ let n_tera, n = aux n 1_000_000_000_000 in
+ let n_giga, n = aux n 1_000_000_000 in
+ let n_mega, n = aux n 1_000_000 in
+ let n_kilo, n = aux n 1_000 in
+ let print_aux s n = if n <> 0 then (string_of_int n) ^ s else "" in
+ (print_aux "To" n_tera) ^
+ (print_aux "Go" n_giga) ^
+ (print_aux "Mo" n_mega) ^
+ (print_aux "ko" n_kilo) ^
+ (print_aux "" n)
+
+let print_size fmt f =
+ Format.fprintf fmt "%s" (size_string f)
+
+let parse_size arg =
+ let l = String.length arg in
+ let multiplier m =
+ let arg1 = String.sub arg 0 (l-1) in
+ `Ok (m *. (float_of_string arg1))
+ in
+ assert (l > 0);
+ try
+ match arg.[l-1] with
+ | 'k' -> multiplier 1e3
+ | 'M' -> multiplier 1e6
+ | 'G' -> multiplier 1e9
+ | 'T' -> multiplier 1e12
+ | '0'..'9' -> `Ok (float_of_string arg)
+ | _ -> `Error "bad numeric argument"
+ with Failure _ -> `Error "bad numeric argument"
+
+let c_time = parse_time, print_time
+let c_size = parse_size, print_size
+
+(* Gc Options parsing *)
+(* ************************************************************************* *)
+
+let gc_t =
+ let docs = gc_section in
+ let minor_heap_size =
+ let doc = "Set Gc.minor_heap_size" in
+ Arg.(value & opt int 1_000_000 & info ["gc-s"] ~doc ~docs)
+ in
+ let major_heap_increment =
+ let doc = "Set Gc.major_heap_increment" in
+ Arg.(value & opt int 100 & info ["gc-i"] ~doc ~docs)
+ in
+ let space_overhead =
+ let doc = "Set Gc.space_overhead" in
+ Arg.(value & opt int 200 & info ["gc-o"] ~doc ~docs)
+ in
+ let max_overhead =
+ let doc = "Set Gc.max_overhead" in
+ Arg.(value & opt int 500 & info ["gc-O"] ~doc ~docs)
+ in
+ let allocation_policy =
+ let doc = "Set Gc.allocation policy" in
+ Arg.(value & opt int 0 & info ["gc-a"] ~doc ~docs)
+ in
+ Term.((const gc_opts $ minor_heap_size $ major_heap_increment $
+ space_overhead $ max_overhead $ allocation_policy))
+
+(* Main Options parsing *)
+(* ************************************************************************* *)
+
+let state theories =
+ let docs = common_section in
+ let gc =
+ let doc = "Print statistics about the gc upon exiting" in
+ Arg.(value & flag & info ["g"; "gc"] ~doc ~docs)
+ in
+ let bt =
+ let doc = "Enables printing of backtraces." in
+ Arg.(value & flag & info ["b"; "backtrace"] ~doc ~docs)
+ in
+ let colors =
+ let doc = "Activate coloring of output" in
+ Arg.(value & opt bool true & info ["color"] ~doc ~docs)
+ in
+ let time =
+ let doc = "Stop the program after a time lapse of $(docv).
+ Accepts usual suffixes for durations : s,m,h,d.
+ Without suffix, default to a time in seconds." in
+ Arg.(value & opt c_time 300. & info ["t"; "time"] ~docv:"TIME" ~doc ~docs)
+ in
+ let size =
+ let doc = "Stop the program if it tries and use more the $(docv) memory space. " ^
+ "Accepts usual suffixes for sizes : k,M,G,T. " ^
+ "Without suffix, default to a size in octet." in
+ Arg.(value & opt c_size 1_000_000_000. & info ["s"; "size"] ~docv:"SIZE" ~doc ~docs)
+ in
+ let in_lang =
+ let doc = Format.asprintf
+ "Set the input language to $(docv) (%s)."
+ (Arg.doc_alts_enum ~quoted:false Dolmen_loop.Logic.enum) in
+ Arg.(value & opt (some input_format_conv) None & info ["i"; "input"; "lang"] ~docv:"INPUT" ~doc ~docs)
+ in
+ let in_mode =
+ let doc = Format.asprintf
+ "Set the input mode. the full mode parses the entire file before iterating
+ over its contents whereas the incremental mode processes each delcaration
+ before parsing the next one. Default is incremental mode." in
+ Arg.(value & opt (some mode_conv) None & info ["m"; "mode"] ~doc ~docs)
+ in
+ let input =
+ let doc = "Input problem file. If no file is specified,
+ dolmen will enter interactive mode and read on stdin." in
+ Arg.(value & pos 0 input_source_conv `Stdin & info [] ~docv:"FILE" ~doc)
+ in
+ let header_check =
+ let doc = "If true, then the presence of headers will be checked in the
+ input file (and errors raised if they are not present)." in
+ Arg.(value & opt bool false & info ["check-headers"] ~doc ~docs)
+ in
+ let header_licenses =
+ let doc = "Set the allowed set of licenses in the headers.
+ An empty list means allow everything." in
+ Arg.(value & opt (list string) [] & info ["header-licenses"] ~doc ~docs)
+ in
+ let header_lang_version =
+ let doc = "Set the only allowed language verison for headers. If not set,
+ all conforming version numbers are allowed." in
+ Arg.(value & opt (some string) None & info ["header-lang-version"] ~docs ~doc)
+ in
+ let typing =
+ let doc = "Decide whether to type-check input expressions. If false, only parsing
+ is done. " in
+ Arg.(value & opt bool true & info ["type"] ~doc ~docs)
+ in
+ let strict =
+ let doc = "Be strict or more lenient wrt to typing" in
+ Arg.(value & opt bool true & info ["strict"] ~doc ~docs)
+ in
+ (*
+ let locs =
+ let doc = "Whether to keep location information during typing. \
+ Setting this to true results in better warning/error \
+ messages, but will use more memory when running." in
+ Arg.(value & opt bool true & info ["locs"] ~doc ~docs)
+ in
+ *)
+ let debug =
+ let doc = Format.asprintf
+ "Print the parsed dolmen statement (after expansion of includes)" in
+ Arg.(value & flag & info ["debug"] ~docs ~doc)
+ in
+ let context =
+ let doc = Format.asprintf
+ "Print the context / fragment of parsed AST with errors" in
+ Arg.(value & flag & info ["context"] ~docs ~doc)
+ in
+ let max_warn =
+ let doc = Format.asprintf
+ "Maximum number of warnings to display (excess warnings will be
+ counted and a count of silenced warnings repoted at the end)." in
+ Arg.(value & opt int max_int & info ["max-warn"] ~docs ~doc)
+ in
+ let step_limit =
+ let doc = Format.asprintf
+ "Maximum number of steps." in
+ Arg.(value & opt (some int) None & info ["max-step"] ~docs ~doc)
+ in
+ let debug_flags =
+ let doc = Format.asprintf "Debug flags." in
+ Arg.(value & opt_all string [] & info ["debug-flag"] ~docs ~doc)
+ 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)
diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index f8db92ec3ba08f5c739bd1cb6333228af6467f72..cf40ddff8b2f943c1581fd440b6cad03b12a683a 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -28,6 +28,7 @@ module Keys = Keys
module Node = struct
include Nodes.Node
+ module HC = Datastructure.HNode
end
module ThTermKind = struct
@@ -85,6 +86,8 @@ module Egraph = Egraph
module Events = Events
module Demon = Demon
+module Datastructure = Datastructure
+
exception UnwaitedEvent = Nodes.UnwaitedEvent
(** Can be raised by daemon when receiving an event that they don't
waited for. It is the sign of a bug in the core solver *)
diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e28c7200245e7a5f647b837d5daa074646e99d14
--- /dev/null
+++ b/src_colibri2/core/datastructure.ml
@@ -0,0 +1,89 @@
+(*************************************************************************)
+(* This file is part of Colibrics. *)
+(* *)
+(* Copyright (C) 2017 *)
+(* 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). *)
+(*************************************************************************)
+
+module type Sig = sig
+ type 'a t
+ type key
+
+ val create: 'a Format.printer -> string -> 'a t
+
+ val remove : 'a t -> Egraph.t -> key -> unit
+ val set : 'a t -> Egraph.t -> key -> 'a -> unit
+ val find : 'a t -> Egraph.t -> key -> 'a
+ val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
+end
+
+module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t = struct
+
+ type 'a t = 'a option Context.Ref.t S.H.t Env.Unsaved.t
+
+ let create : type a. a Colibri2_popop_lib.Pp.pp -> _ -> a t = fun pp name ->
+ let module M = struct
+ type t = a option Context.Ref.t S.H.t
+ let name = name end
+ in
+ let key = Env.Unsaved.create_key (module M) in
+ let init () = S.H.create 5 in
+ let iter f = S.H.iter (fun k r -> match Context.Ref.get r with None -> () | Some v -> f k v) in
+ let pp = Colibri2_popop_lib.Pp.(iter2 iter semi arrow S.pp pp) in
+ Env.Unsaved.register ~init ~pp key;
+ key
+
+ let find t d k =
+ let r = S.H.find (Egraph.get_unsaved_env d t) k in
+ match Context.Ref.get r with
+ | Some v -> v
+ | None -> raise Not_found
+
+ let set t d k v =
+ let h = Egraph.get_unsaved_env d t in
+ let r = match S.H.find_opt h k with
+ | Some r -> r
+ | None ->
+ let r = Context.Ref.create (Egraph.context d) None in
+ S.H.add h k r;
+ r
+ in
+ Context.Ref.set r (Some v)
+
+ let remove t d k =
+ let h = Egraph.get_unsaved_env d t in
+ match S.H.find_opt h k with
+ | Some r -> Context.Ref.set r None
+ | None -> ()
+
+ let change f t d k =
+ let h = Egraph.get_unsaved_env d t in
+ let change = function
+ | Some r as o ->
+ let v = f (Context.Ref.get r) in
+ Context.Ref.set r v;
+ o
+ | None ->
+ let r = Context.Ref.create (Egraph.context d) None in
+ let v = f None in
+ Context.Ref.set r v;
+ (Some r)
+ in
+ S.H.change change h k
+
+end
+
+module HNode = Hashtbl(Nodes.Node)
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
new file mode 100644
index 0000000000000000000000000000000000000000..86dd3cf6b61f6735117ab2743daefe7213f5e58f
--- /dev/null
+++ b/src_colibri2/core/datastructure.mli
@@ -0,0 +1,36 @@
+(*************************************************************************)
+(* This file is part of Colibrics. *)
+(* *)
+(* Copyright (C) 2017 *)
+(* 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). *)
+(*************************************************************************)
+
+module type Sig = sig
+ type 'a t
+ type key
+
+ val create: 'a Format.printer -> string -> 'a t
+
+ val remove : 'a t -> Egraph.t -> key -> unit
+ val set : 'a t -> Egraph.t -> key -> 'a -> unit
+ val find: 'a t -> Egraph.t -> key -> 'a
+ val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
+end
+
+
+module Hashtbl (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t
+
+module HNode : Sig with type key := Nodes.Node.t
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index eb2fecf18f0a4585f05f3253abfe001d2f720531..5a68dc1b0ee9c0d731d4a843bc2771a6ca0f050d 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -87,7 +87,7 @@ module Key = struct
type ('k,'d,'i) t = {
dk_id : ('k * 'd, 'k) Events.Dem.t;
- dk_data : ('k,'d,'i) demtable Env.t;
+ dk_data : ('k,'d,'i) demtable Env.Saved.t;
}
let create (type k d i) name =
@@ -96,7 +96,7 @@ module Key = struct
type nonrec d = k
let name = name
end);
- dk_data = Env.create_key (module struct
+ dk_data = Env.Saved.create_key (module struct
type t = (k,d,i) demtable
let name = name
end)
@@ -241,7 +241,7 @@ module Key = struct
let l = DT.Key.M.bindings DT.state in
Format.list ~sep:newline aux fmt l
in
- Env.register print_demtable D.key.dk_data;
+ Env.Saved.register print_demtable D.key.dk_data;
(** Interface for generic daemon *)
let module Dem = struct
type runable = D.Key.t
@@ -348,7 +348,7 @@ module Fast = struct
type 'd t = {
dk_id : ('d, unit) Events.Dem.t;
- dk_data : 'd Events.Fired.event list Env.t;
+ dk_data : 'd Events.Fired.event list Env.Saved.t;
(** for throttling *)
mutable dk_remaining: int; (** 0 if the demon is not the current one *)
dk_current : 'd Events.Fired.event Queue.t; (** empty if idem *)
@@ -361,7 +361,7 @@ module Fast = struct
type d = unit
let name = name
end);
- dk_data = Env.create_key (module struct
+ dk_data = Env.Saved.create_key (module struct
type t = d Events.Fired.event list
let name = name
end);
@@ -452,7 +452,7 @@ module Fast = struct
let () =
let print_demtable = Format.(list ~sep:(const char ',') Events.Fired.pp) in
- Env.register print_demtable D.key.dk_data;
+ Env.Saved.register print_demtable D.key.dk_data;
(** Interface for generic daemon *)
let module Dem = struct
type runable = unit
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 465a0e1eda12c1297d2e43570cf624ed109b85d4..615913292903f5294cdbd3aad8c468fe78e69a6e 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -72,7 +72,7 @@ module Def = struct
saved_dom : delayed_t VDomTable.t;
saved_sem : semtable VSemTable.t;
saved_value : unit VValueTable.t;
- saved_envs : Env.VectorH.t;
+ saved_envs : Env.Saved.VectorH.t;
}
@@ -87,8 +87,9 @@ module Def = struct
dom : delayed_t VDomTable.t;
sem : semtable VSemTable.t;
value : unit VValueTable.t;
- envs : Env.VectorH.t;
+ envs : Env.Saved.VectorH.t;
mutable current_delayed : delayed_t; (** For assert-check *)
+ unsaved_envs: Env.Unsaved.VectorH.t;
history : saved Context.history;
}
@@ -119,7 +120,7 @@ module Def = struct
and choice_state =
| DecNo
- | DecTodo of (delayed_t -> unit)
+ | DecTodo of (delayed_t -> unit) list
and choice = {
choice: delayed_t -> choice_state;
@@ -137,7 +138,7 @@ type choice = Def.choice = {
}
type choice_state = Def.choice_state =
| DecNo
- | DecTodo of (delayed_t -> unit)
+ | DecTodo of (delayed_t -> unit) list
(** {2 Define events} *)
@@ -185,7 +186,7 @@ module Hidden = Context.Make(struct
saved_dom = VDomTable.copy t.dom;
saved_sem = VSemTable.copy t.sem;
saved_value = VValueTable.copy t.value;
- saved_envs = Env.VectorH.copy t.envs;
+ saved_envs = Env.Saved.VectorH.copy t.envs;
}
let restore (s:saved) (t:t) =
@@ -198,7 +199,7 @@ module Hidden = Context.Make(struct
VDomTable.move ~from:s.saved_dom ~to_:t.dom;
VSemTable.move ~from:s.saved_sem ~to_:t.sem;
VValueTable.move ~from:s.saved_value ~to_:t.value;
- Env.VectorH.move ~from:s.saved_envs ~to_:t.envs;
+ Env.Saved.VectorH.move ~from:s.saved_envs ~to_:t.envs;
t.current_delayed <- dumb_delayed
let get_history t = t.history
@@ -266,18 +267,28 @@ module T = struct
let node = find_def t node in
get_direct_value t value node
- let get_env : type a. t -> a Env.t -> a
+ let get_env : type a. t -> a Env.Saved.t -> a
= fun t k ->
- Env.check_is_registered k;
- if Env.VectorH.is_uninitialized t.envs k then
- raise (UninitializedEnv (Env.name k))
+ Env.Saved.check_is_registered k;
+ if Env.Saved.VectorH.is_uninitialized t.envs k then
+ raise (UninitializedEnv (Env.Saved.name k))
else
- Env.VectorH.get t.envs k
+ Env.Saved.VectorH.get t.envs k
- let set_env : type a. t -> a Env.t -> a -> unit
+ let set_env : type a. t -> a Env.Saved.t -> a -> unit
= fun t k ->
- Env.check_is_registered k;
- Env.VectorH.set t.envs k
+ Env.Saved.check_is_registered k;
+ Env.Saved.VectorH.set t.envs k
+
+ let get_unsaved_env : type a. t -> a Env.Unsaved.t -> a
+ = fun t k ->
+ Env.Unsaved.check_is_registered k;
+ if Env.Unsaved.VectorH.is_uninitialized t.unsaved_envs k then
+ let v = Env.Unsaved.init k in
+ Env.Unsaved.VectorH.set t.unsaved_envs k v;
+ v
+ else
+ Env.Unsaved.VectorH.get t.unsaved_envs k
let is_registered t node =
Node.M.mem node t.repr
@@ -431,6 +442,10 @@ module Delayed = struct
assert (is_current_env t);
set_env t.env env v
+ let get_unsaved_env t env =
+ assert (is_current_env t);
+ get_unsaved_env t.env env
+
let is_registered t node =
assert (is_current_env t);
is_registered t.env node
@@ -599,10 +614,11 @@ module Delayed = struct
let old_other_s = Node.M.find_opt node1 domtable.table in
let old_repr_s = Node.M.find_opt node2 domtable.table in
let (module Dom) = VDom.get_dom dom in
- Debug.dprintf12 debug_few
- "[Egraph] @[merge dom (%a(%a),%a)@ and (%a(%a),%a)@]"
+ Debug.dprintf13 debug_few
+ "[Egraph] @[merge dom (%a(%a),%a)@ %s@ (%a(%a),%a)@]"
Node.pp node1 Node.pp node1_0
(Format.opt Dom.pp) old_other_s
+ (if inv then "<-" else "->")
Node.pp node2 Node.pp node2_0
(Format.opt Dom.pp) old_repr_s;
match old_other_s, old_repr_s with
@@ -984,7 +1000,8 @@ module Backtrackable = struct
dom = VDomTable.create 5;
sem = VSemTable.create 5;
value = VValueTable.create 5;
- envs = Env.VectorH.create 5;
+ envs = Env.Saved.VectorH.create 5;
+ unsaved_envs = Env.Unsaved.VectorH.create 5;
current_delayed = dumb_delayed;
history = Hidden.create context;
}
@@ -1001,7 +1018,7 @@ module Backtrackable = struct
* dom = VDomTable.copy t.dom;
* sem = VSemTable.copy t.sem;
* value = VValueTable.copy t.value;
- * envs = Env.VectorH.copy t.envs;
+ * envs = Env.Saved.VectorH.copy t.envs;
* trail = Trail.new_handle t.trail;
* current_delayed = t.current_delayed;
* } *)
@@ -1074,6 +1091,11 @@ module Backtrackable = struct
assert (check_disabled_delayed t);
T.set_env t env v
+ let get_unsaved_env t env =
+ let t = Hidden.rw t in
+ assert (check_disabled_delayed t);
+ T.get_unsaved_env t env
+
let is_repr t node =
let t = Hidden.rw t in
assert (check_disabled_delayed t);
@@ -1113,8 +1135,9 @@ module type Getter = sig
val is_registered : t -> Node.t -> bool
- val get_env : t -> 'a Env.t -> 'a
- val set_env : t -> 'a Env.t -> 'a -> unit
+ val get_env : t -> 'a Env.Saved.t -> 'a
+ val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+ val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
val context : t -> Context.creator
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index 3321434f6e6a17683c7e7310149d57e305f2d965..f5b86bcfe7a2ffb6e42266b78d098fefdfb8f4ea 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -49,8 +49,10 @@ module type Getter = sig
val is_registered : t -> Node.t -> bool
- val get_env : t -> 'a Env.t -> 'a
- val set_env : t -> 'a Env.t -> 'a -> unit
+ val get_env : t -> 'a Env.Saved.t -> 'a
+ val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+
+ val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
val context : t -> Context.creator
@@ -108,9 +110,9 @@ val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
type choice_state =
| DecNo
- | DecTodo of (t -> unit)
+ | DecTodo of (t -> unit) list
-type choice = {
+and choice = {
choice: t -> choice_state;
prio: int;
}
diff --git a/src_colibri2/core/env.ml b/src_colibri2/core/env.ml
index a93539cdc946e6739d84d8d08150468d37fc46bd..8480613c5a8db73fbd95bbe6cf27ce140a883241 100644
--- a/src_colibri2/core/env.ml
+++ b/src_colibri2/core/env.ml
@@ -18,18 +18,41 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-module Env = Keys.Make_key(struct end)
+module Saved = struct
+ module Env = Keys.Make_key(struct end)
-include Env
+ include Env
-type 'a data = {key: 'a Env.t; pp: 'a Format.printer}
+ type 'a data = {key: 'a Env.t; pp: 'a Format.printer}
-module VEnv = Env.Make_Registry(struct
- type nonrec 'a data = 'a data
- let pp d = d.pp
- let key d = d.key
- end)
+ module VEnv = Env.Make_Registry(struct
+ type nonrec 'a data = 'a data
+ let pp d = d.pp
+ let key d = d.key
+ end)
-let register pp key = VEnv.register {key;pp}
-let print = VEnv.print
-let check_is_registered = VEnv.check_is_registered
+ let register pp key = VEnv.register {key;pp}
+ let print = VEnv.print
+ let check_is_registered = VEnv.check_is_registered
+end
+
+module Unsaved = struct
+ module Env = Keys.Make_key(struct end)
+
+ include Env
+
+ type 'a data = {key: 'a Env.t; pp: 'a Format.printer;
+ init : (unit -> 'a)}
+
+ module VEnv = Env.Make_Registry(struct
+ type nonrec 'a data = 'a data
+ let pp (d:_ data) = d.pp
+ let key (d:_ data) = d.key
+ end)
+
+ let register ~init ~pp key = VEnv.register {key;pp;init}
+ let print = VEnv.print
+ let check_is_registered = VEnv.check_is_registered
+ let init k = (VEnv.get k).init ()
+
+end
diff --git a/src_colibri2/core/env.mli b/src_colibri2/core/env.mli
index bf2e683bfdc1548bcc0809e8686acdf02d6472f7..a3ff99395f89f2f29a5f061f7a3d98e4a59f6be8 100644
--- a/src_colibri2/core/env.mli
+++ b/src_colibri2/core/env.mli
@@ -20,16 +20,36 @@
(** Theory specific environment *)
-(** Environment should currently be persistent data-structure in order
- to be backtracked correctly *)
+module Saved: sig
+ (** Environment should currently be persistent data-structure in order
+ to be backtracked correctly *)
-include Keys.Key
+ include Keys.Key
-val register: 'a Format.printer -> 'a t -> unit
-(** Only a pretty printer is needed for registration *)
+ val register: 'a Format.printer -> 'a t -> unit
+ (** Only a pretty printer is needed for registration *)
-val print: 'a t -> 'a Format.printer
-(** Get a pretty printer for a particular environment *)
+ val print: 'a t -> 'a Format.printer
+ (** Get a pretty printer for a particular environment *)
-val check_is_registered: 'a t -> unit
-(** Check if all the keys created have been registered *)
+ val check_is_registered: 'a t -> unit
+ (** Check if all the keys created have been registered *)
+end
+
+module Unsaved: sig
+ (** These environment are context insensitive *)
+
+ include Keys.Key
+
+ val register: init:(unit -> 'a) -> pp:'a Format.printer -> 'a t -> unit
+ (** Only a pretty printer and an initialization function is needed for registration *)
+
+ val print: 'a t -> 'a Format.printer
+ (** Get a pretty printer for a particular environment *)
+
+ val check_is_registered: 'a t -> unit
+ (** Check if all the keys created have been registered *)
+
+ val init: 'a t -> 'a
+ (** Create the initial value *)
+end
diff --git a/src_colibri2/core/structures/domKind.mli b/src_colibri2/core/structures/domKind.mli
index 07abe1cf62749a9bec986110b47b7435bd38c3ed..71cc718a0a29e93796b76515f0ac082f1f5dd8d8 100644
--- a/src_colibri2/core/structures/domKind.mli
+++ b/src_colibri2/core/structures/domKind.mli
@@ -36,6 +36,11 @@ module type Dom_partial = sig
t option * Node.t -> t option * Node.t ->
bool ->
unit
+ (** [merge d (dom1,cl1) (dom2,cl2) inv]
+ - if inv is false, cl2 will be the new representative
+ - if inv is true, cl1 will be the new representative
+ *)
+
val pp: Format.formatter -> t -> unit
val key: t dom
end
diff --git a/src_colibri2/core/synTerm.ml b/src_colibri2/core/synTerm.ml
index 9161e0cadef3c0a0f2faa5293fc883017762f650..17550576e19fb735cdcac850d832b17394a8f912 100644
--- a/src_colibri2/core/synTerm.ml
+++ b/src_colibri2/core/synTerm.ml
@@ -39,7 +39,7 @@ type env = {
decvars: (Expr.Term.t -> Node.t -> Egraph.choice option) list;
}
-let converters = Env.create_key (module struct
+let converters = Env.Saved.create_key (module struct
type t = env
let name = "Synsem.converters"
end)
@@ -52,7 +52,7 @@ let register_decvars env r =
let e = Egraph.get_env env converters in
Egraph.set_env env converters {e with decvars = r::e.decvars}
-let () = Env.register (fun _ _ -> ()) converters
+let () = Env.Saved.register (fun _ _ -> ()) converters
module DaemonConvertTerm = struct
let key = Demon.Fast.create "Synsem.DaemonConvertTerm"
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index 024c098b59128511f7150519c860b21a7ce72e0d..4d5d445056a7fa7f45cbfd91e17eaa103c9f16fc 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -288,7 +288,7 @@ let mk_state
?input_lang ?input_mode ~input
?(header_check=false) ?(header_licenses=[])
?(header_lang_version=None)
- ?(type_strict=true)
+ ?(type_check=true) ?(type_strict=true)
?(debug=false) ?(context=true) ?(max_warn=max_int)
theories
=
@@ -317,7 +317,7 @@ let mk_state
header_check; header_licenses; header_lang_version;
header_state = Dolmen_loop.Headers.empty;
- type_check = true; type_strict;
+ type_check; type_strict;
type_state = Dolmen_loop.Typer.new_state ();
solve_state = create_ctx theories;
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 50c8a377e1bad0c0a28cd3dfa3bd00f66c87ec2a..4461c9feb28b7ed1b848290e79e26e51567bd824 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -72,11 +72,13 @@ type bp =
{ pre_wakeup_daemons : Prio.t;
pre_prev_scheduler_state : bp option;
pre_backtrack_point : Context.bp;
+ pre_choices : (Egraph.t -> unit) list;
}
type t =
{ mutable wakeup_daemons : Prio.t;
mutable prev_scheduler_state : bp option;
+ mutable choices : (Egraph.t -> unit) list;
solver_state : Egraph.Backtrackable.t;
mutable delayed : Egraph.t option;
(* global *)
@@ -109,6 +111,7 @@ let new_solver () =
let context = Context.create () in
{ wakeup_daemons = Prio.empty;
prev_scheduler_state = None;
+ choices = [];
solver_state = Egraph.Backtrackable.new_t (Context.creator context);
context;
delayed = None;
@@ -124,6 +127,7 @@ let push t =
{ pre_wakeup_daemons = t.wakeup_daemons;
pre_prev_scheduler_state = t.prev_scheduler_state;
pre_backtrack_point = Context.bp t.context;
+ pre_choices = t.choices;
} in
t.prev_scheduler_state <- Some prev;
ignore (Context.push t.context);
@@ -240,26 +244,35 @@ and conflict_analysis t =
and try_run_dec:
t -> Egraph.t -> Prio.t -> Egraph.choice -> Egraph.t = fun t d prio choice ->
(** First we verify its the decision is at this point needed *)
- try
+ assert (t.choices = []);
+ try
match choice.choice d with
- | Egraph.DecNo ->
+ | Egraph.DecNo | Egraph.DecTodo [] ->
t.wakeup_daemons <- prio;
d (** d can be precised by choose_decision *)
- | Egraph.DecTodo todo ->
- Debug.incr stats_dec;
- Egraph.Backtrackable.delayed_stop d;
- (** The registered state keep the old prio *)
- ignore (push t);
- (** We use the priority list without the decision only in the
- branch where the decision is made *)
+ | Egraph.DecTodo (todo::todos) ->
+ (** We remove the decision it is replaced by the todos,
+ we can change the interface of choice and in that case
+ we want to keep the decision in the current branch *)
t.wakeup_daemons <- prio;
- let d = new_delayed t in
- todo d;
- d
+ Debug.incr stats_dec;
+ make_choice t d todo todos
with Egraph.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction";
conflict_analysis t
+and make_choice t d todo todos =
+ Egraph.Backtrackable.delayed_stop d;
+ t.choices <- todos;
+ begin match todos with
+ | [] -> ()
+ | _ -> ignore (push t)
+ end;
+ let d = new_delayed t in
+ todo d;
+ d
+
+
and run_until_dec t d =
let act = Prio.min t.wakeup_daemons in
match act with
@@ -275,18 +288,27 @@ and run_until_dec t d =
let run_one_step t d =
- let act, prio = Prio.extract_min t.wakeup_daemons in
- match act with
- | Att.Daemon (_,att) -> begin
- Debug.incr stats_propa;
- t.wakeup_daemons <- prio;
- try
- Egraph.Backtrackable.run_daemon d att; d
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t
+ match t.choices with
+ | [] -> begin
+ let act, prio = Prio.extract_min t.wakeup_daemons in
+ match act with
+ | Att.Daemon (_,att) -> begin
+ Debug.incr stats_propa;
+ t.wakeup_daemons <- prio;
+ try
+ Egraph.Backtrackable.run_daemon d att; d
+ with Egraph.Contradiction ->
+ Debug.dprintf0 debug "[Scheduler] Contradiction";
+ conflict_analysis t
+ end
+ | Att.Decision (_,chogen) -> try_run_dec t d prio chogen
end
- | Att.Decision (_,chogen) -> try_run_dec t d prio chogen
+ | todo::todos ->
+ try
+ make_choice t d todo todos
+ with Egraph.Contradiction ->
+ Debug.dprintf0 debug "[Scheduler] Contradiction";
+ conflict_analysis t
let rec flush t d =
try
diff --git a/src_colibri2/stdlib/keys.ml b/src_colibri2/stdlib/keys.ml
index 19ba8d71d095e831219cfe42a6aea4f5a5d05404..cf4545104a196c751fdc6bde4c6d92cabb9c1c00 100644
--- a/src_colibri2/stdlib/keys.ml
+++ b/src_colibri2/stdlib/keys.ml
@@ -38,7 +38,7 @@ module Make_key(X:sig end) = struct
id : int;
iseq : 'b. 'b gadt -> ('a,'b) Poly.iseq }
- let pp fmt x = String.pp fmt x.name
+ let pp fmt x = Format.pp_print_string fmt x.name
let equal a b = a.id = b.id
let compare x y = compare x.id y.id
let hash x = x.id
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index bed8dab1037c2a3e8a2f3386038d0db88c8ab582..fd01bf8840645b84aa52679e165c675610c18243 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -99,4 +99,22 @@ module Q = struct
in
Q.(sgn * (int_part + dec_part))
+ let is_integer q = Z.equal Z.one q.Q.den
+
+ let floor q =
+ if is_integer q then q
+ else Q.of_bigint
+ (if Q.lt q Q.zero
+ then Z.pred (Q.to_bigint q)
+ else Q.to_bigint q)
+
+ let ceil q =
+ if is_integer q then q
+ else
+ Q.of_bigint
+ (if Q.gt q Q.zero
+ then Z.succ (Q.to_bigint q)
+ else Q.to_bigint q)
+
+
end
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index 041b1e0d96da25a25b615de2bfdc5bb420f4ee9c..e4100647a86f0536591dea6e08d5329a4a3a8a39 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -57,4 +57,7 @@ module Q : sig
val ge : t -> t -> bool
val le : t -> t -> bool
val of_string_decimal : string -> t
+ val floor: t -> t
+ val ceil : t -> t
+ val is_integer : t -> bool
end
diff --git a/src_colibri2/tests/dune b/src_colibri2/tests/dune
index 010bdcbd5dc61bde01c9aa0532c7f42196b871d6..7695ec893c847a0506a979fdddc5d76d9891a26d 100644
--- a/src_colibri2/tests/dune
+++ b/src_colibri2/tests/dune
@@ -10,6 +10,6 @@
(alias runtest)
(deps
(:< tests.exe)
- (source_tree solve/))
+ )
(action
(run %{<})))
diff --git a/src_colibri2/tests/generate_tests/dune b/src_colibri2/tests/generate_tests/dune
new file mode 100644
index 0000000000000000000000000000000000000000..1d7c405ab1f2488562b00be79164024fce522079
--- /dev/null
+++ b/src_colibri2/tests/generate_tests/dune
@@ -0,0 +1,3 @@
+(executable
+ (name generate_dune_tests)
+)
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..59da80597db18f56350d1dde44e73c4e9f41dcbf
--- /dev/null
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -0,0 +1,22 @@
+let dir = Sys.argv.(1)
+let result = Sys.argv.(2)
+
+let print_test cout file =
+ Printf.fprintf cout
+ "(rule (action (with-stdout-to %s.res (run colibri2 --max-step 1000 %s))))\n"
+ file file;
+ Printf.fprintf cout
+ "(rule (alias runtest) (action (diff oracle %s.res)))\n"
+ file
+
+let () =
+ let files = Sys.readdir dir in
+ Array.sort String.compare files;
+ let files = Array.to_list files in
+ let files = List.filter (fun f -> Filename.check_suffix f "cnf" || Filename.check_suffix f ".smt2") files in
+ let cout = open_out (Filename.concat dir "dune.inc") in
+ Printf.fprintf cout
+ "(rule (action (with-stdout-to oracle (echo %S))))\n"
+ (result^"\n");
+ List.iter (print_test cout) files;
+ close_out cout
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune b/src_colibri2/tests/solve/dimacs/sat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..74e69b2c52ff290765701e5e65358570a665fafc
--- /dev/null
+++ b/src_colibri2/tests/solve/dimacs/sat/dune
@@ -0,0 +1,7 @@
+(include dune.inc)
+
+(rule
+ (deps (glob_files *.cnf) (glob_files *.smt2))
+ (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote)
+)
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..e534f7ee2fec92a81db1775ce7d085d66d374241
--- /dev/null
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -0,0 +1,23 @@
+(rule (action (with-stdout-to oracle (echo "sat\n"))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold.cnf))))
+(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
+(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold2.cnf))))
+(rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res)))
+(rule (action (with-stdout-to assertion_fail.cnf.res (run colibri2 --max-step 1000 assertion_fail.cnf))))
+(rule (alias runtest) (action (diff oracle assertion_fail.cnf.res)))
+(rule (action (with-stdout-to fuzzing1.cnf.res (run colibri2 --max-step 1000 fuzzing1.cnf))))
+(rule (alias runtest) (action (diff oracle fuzzing1.cnf.res)))
+(rule (action (with-stdout-to fuzzing2.cnf.res (run colibri2 --max-step 1000 fuzzing2.cnf))))
+(rule (alias runtest) (action (diff oracle fuzzing2.cnf.res)))
+(rule (action (with-stdout-to par8-1-c.cnf.res (run colibri2 --max-step 1000 par8-1-c.cnf))))
+(rule (alias runtest) (action (diff oracle par8-1-c.cnf.res)))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run colibri2 --max-step 1000 pigeon-2.cnf))))
+(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run colibri2 --max-step 1000 pigeon-3.cnf))))
+(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run colibri2 --max-step 1000 pigeon-4.cnf))))
+(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
+(rule (action (with-stdout-to quinn.cnf.res (run colibri2 --max-step 1000 quinn.cnf))))
+(rule (alias runtest) (action (diff oracle quinn.cnf.res)))
+(rule (action (with-stdout-to simple_v3_c2.cnf.res (run colibri2 --max-step 1000 simple_v3_c2.cnf))))
+(rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res)))
diff --git a/src_colibri2/tests/tests.ml b/src_colibri2/tests/tests.ml
index 9a3751374b7e0b32ab513ce4e420f3ca8a2d95b1..ef4d208e1d2d772299fabe39799866cf6304795c 100644
--- a/src_colibri2/tests/tests.ml
+++ b/src_colibri2/tests/tests.ml
@@ -44,13 +44,15 @@ let tests () =
(!opt_seed + 1) (!opt_seed + 9)in
make_tests l None
+let debug = OUnit2.Conf.make_bool "debug" false " activate debugging"
+
let tests () =
(* if Printexc.backtrace_status ()
* then
- * (test_decorate
+ * (OUnitTest.test_decorate
* (fun f ->
- * fun () ->
- * try f ()
+ * fun ctx ->
+ * try f ctx
* with
* | exn ->
* Format.fprintf (Colibri2_popop_lib.Debug.get_debug_formatter ()) "%s"
@@ -58,6 +60,15 @@ let tests () =
* raise exn
* )) (test_list (tests ()))
* else *)
+ OUnitTest.test_decorate
+ (fun f ->
+ fun ctx ->
+ let debug = debug ctx in
+ if debug then
+ Colibri2_popop_lib.Debug.(
+ List.iter (fun (_,f,_,_) -> set_flag f) (list_flags ()));
+ f ctx
+ )
(test_list (tests ()))
(** From oUnit.ml v 1.2.2 *)
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index afbfacf8e7d06428a992826f0953d824626f4aec..d0363923d25a10874da9f727005159c7ee44ce3c 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -79,6 +79,7 @@ module SE = ThTermKind.Register(S)
module D = Interval.Convexe
let dom = DomKind.create_key (module struct type t = D.t let name = "ARITH" end)
+let dom_poly = DomKind.create_key (module struct type t = Polynome.t let name = "ARITH_POLY" end)
let set_dom d node v =
match D.is_singleton v with
@@ -89,6 +90,140 @@ let set_dom d node v =
(** the pexp must be in the dom *)
Egraph.set_dom d dom node v
+(** Polynome *)
+let propa_dem = Demon.Key.create "Arith.DaemonPropa"
+
+let print_bag_cl = Colibri2_popop_lib.Bag.pp Pp.comma Node.pp
+
+let used_in_poly : Node.t Bag.t Node.HC.t = Node.HC.create (Bag.pp Pp.semi Node.pp) "used_in_poly"
+
+module T = struct
+ include Polynome
+ let key = ThTermKind.create_key (module struct type nonrec t = t let name = "SARITH_POLY" end)
+end
+
+module ThE = ThTermKind.Register(T)
+
+let set_poly d cl p =
+ Egraph.set_dom d dom_poly cl p;
+ match Polynome.is_one_node p with
+ | None -> Egraph.set_thterm d cl (ThE.thterm (ThE.index p))
+ | Some cl' -> Egraph.merge d cl cl'
+
+let add_used d cl' new_cl =
+ Node.M.iter (fun used _ ->
+ Node.HC.change (function
+ | Some b -> Some (Bag.append b cl')
+ | None -> Some (Bag.elt cl')
+ ) used_in_poly d used
+ ) new_cl
+
+let subst_doms d cl (p:Polynome.t) =
+ let b = match Node.HC.find used_in_poly d cl with
+ | exception Not_found -> Bag.empty
+ | b -> b
+ in
+ Bag.iter (fun cl' ->
+ match Egraph.get_dom d dom_poly cl' with
+ | None -> assert false (** absurd: can't be used and absent *)
+ | Some q ->
+ let new_cl = Node.M.set_diff p.poly q.poly in
+ let q, _ = Polynome.subst q cl p in
+ add_used d cl' new_cl;
+ set_poly d cl' q
+ ) b;
+ add_used d cl p.poly;
+ set_poly d cl p
+
+module Th = struct
+ include Polynome
+
+ let merged v1 v2 =
+ match v1,v2 with
+ | None, None -> true
+ | Some v', Some v -> equal v' v
+ | _ -> false
+
+ let norm_dom cl = function
+ | None ->
+ let r = monome Q.one cl in
+ r
+ | Some p ->
+ p
+
+ let add_itself d cl norm =
+ add_used d cl norm.poly;
+ Egraph.set_dom d dom_poly cl norm
+
+ let merge d ((p1o,cl1) as a1) ((p2o,cl2) as a2) inv =
+ assert (not (Egraph.is_equal d cl1 cl2));
+ assert (not (CCOpt.is_none p1o && CCOpt.is_none p2o));
+ let (pother, other), (prepr, repr) = if inv then a2,a1 else a1,a2 in
+ let other = Egraph.find d other in
+ let repr = Egraph.find d repr in
+ let p1 = norm_dom other pother in
+ let p2 = norm_dom repr prepr in
+ let diff = sub p1 p2 in
+ (* 0 = other - repr = p1 - p2 = diff *)
+ Debug.dprintf2 debug "[Arith] @[solve 0=%a@]" pp diff;
+ begin match Polynome.extract diff with
+ | Zero -> (** no new equality already equal *)
+ begin
+ match pother, prepr with
+ | Some _, Some _ | None, None ->
+ assert false (** absurd: no need of merge *)
+ | Some p, None ->
+ (** p = repr *)
+ add_itself d repr p
+ | None, Some p ->
+ (** p = other *)
+ add_itself d other p
+ end
+ | Cst _ ->
+ (* 0 = cst <> 0 *)
+ Egraph.contradiction d
+ | Var(q,x,p') ->
+ (** diff = qx + p' *)
+ assert ( not (Q.equal Q.zero q) );
+ Debug.dprintf2 debug "[Arith] @[pivot %a@]" Node.pp x;
+ let add_if_default n norm = function
+ | Some _ -> ()
+ | None ->
+ add_itself d n norm
+ in
+ add_if_default other p1 pother;
+ add_if_default repr p2 prepr;
+ subst_doms d x (Polynome.mult_cst (Q.div Q.one (Q.neg q)) p')
+ end;
+ assert (CCOpt.compare Polynome.compare
+ (Egraph.get_dom d dom_poly repr)
+ (Egraph.get_dom d dom_poly other) = 0)
+
+ let solve_one d cl p1 =
+ match Egraph.get_dom d dom_poly cl with
+ | None ->
+ subst_doms d cl p1
+ | Some p2 ->
+ let diff = Polynome.sub p1 p2 in
+ (* 0 = p1 - p2 = diff *)
+ Debug.dprintf2 debug "[Arith] @[solve in init 0=%a@]" Polynome.pp diff;
+ begin match Polynome.extract diff with
+ | Zero -> ()
+ | Cst _ ->
+ (* 0 = cst <> 0 *)
+ Egraph.contradiction d
+ | Var(q,x,p') ->
+ (** diff = qx + p' *)
+ assert ( not (Q.equal Q.zero q) );
+ Debug.dprintf2 debug "[Arith] @[pivot %a@]" Node.pp x;
+ subst_doms d x (Polynome.mult_cst (Q.div Q.one (Q.neg q)) p')
+ end
+
+ let key = dom_poly
+end
+
+let () = Egraph.register_dom(module Th)
+
let minus_or_one inv =
if inv then Q.minus_one else Q.one
@@ -199,23 +334,25 @@ module DaemonPropa = struct
propagate del s
| _ -> raise UnwaitedEvent
- let init del s =
+ let init d s =
begin match SE.sem s with
- | S.Add (_,cl1,_,cl2) ->
- Debug.dprintf2 debug "TOTO: %a" SE.pp s;
- Egraph.register del cl1; Egraph.register del cl2;
- Demon.Fast.attach del key
+ | S.Add (c1,cl1,c2,cl2) ->
+ Egraph.register d cl1; Egraph.register d cl2;
+ Demon.Fast.attach d key
[Demon.Create.EventValue(SE.node s, real, s);
Demon.Create.EventValue(cl1, real, s);
Demon.Create.EventValue(cl2, real, s);
- ]
+ ];
+ let cl = (SE.node s) in
+ let p1 = Polynome.of_list Q.zero [cl1,c1;cl2,c2] in
+ Th.solve_one d cl p1
| GZero (node,_) ->
- Egraph.register del node;
- Demon.Fast.attach del key
+ Egraph.register d node;
+ Demon.Fast.attach d key
[Demon.Create.EventValue(SE.node s, Boolean.dom, s);
Demon.Create.EventValue(node, real, s)]
end;
- propagate del s;
+ propagate d s;
end
module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
@@ -259,240 +396,6 @@ let to_poly = function
| S.Add(q1,cl1,q2,cl2) -> Polynome.of_list Q.one [cl1,q1;cl2,q2]
| GZero _ -> raise Impossible
-(** Choice *)
-(*
-(** Conflict *)
-(** Reason of equalities between arithmetical terms
- exp: with all the decisions and propagation applied
- imp: without any decision and propagation applied
-*)
-type conpoly = {imp : Polynome.t; exp : Polynome.t; bound: bound;
- deps: Deps.t [@printer (fun _ _ -> ())]}
-let pp_conpoly fmt x =
- Format.fprintf fmt "0 %s@ %a@ (%a)"
- (match x.bound with | Strict -> "<" | Large -> "<=")
- Polynome.pp x.imp
- Polynome.pp x.exp
-let pp_conpoly' fmt x =
- Format.fprintf fmt "%a@ (%a)@ %s 0"
- Polynome.pp x.imp
- Polynome.pp x.exp
- (match x.bound with | Strict -> "<" | Large -> "<=")
-
-type conpair = {mi: conpoly option; ma:conpoly option}
-(** used as [0 <= x + P = mi /\ x + P = ma <= 0] *)
-let pp_conpair fmt = function
- | {mi=None; ma=None} -> Format.fprintf fmt "None"
- | {mi=Some mi;ma=None} -> pp_conpoly fmt mi
- | {mi=None;ma=Some ma} -> pp_conpoly' fmt ma
- | {mi=Some mi;ma=Some ma} ->
- Format.fprintf fmt "%a@,â‹€ %a" pp_conpoly mi pp_conpoly' ma
-
-let interp_conpoly d p =
- let acc = Node.M.fold_left (fun acc node q ->
- let v = Opt.get_def D.reals (Egraph.get_dom d dom node) in
- D.add (D.mult_cst q v) acc
- ) D.zero p.imp.Polynome.poly in
- let acc = D.add_cst p.imp.cst acc in
- let good =
- if p.bound = Strict then DaemonPropa.gt_zero
- else DaemonPropa.ge_zero
- in
- match D.inter acc good with
- | None -> Conflict.False
- | Some i when D.equal i acc -> Conflict.True
- | Some _ -> Conflict.ToDecide
-
-let condom : conpair Trail.con = Trail.Con.create_key "LRA.dom"
-
-(** Return the corresponding bound *)
-let get_exp_conpoly {exp={Polynome.cst}} = Q.neg cst
-
-let mk_conpoly p = {imp = p; exp = p; bound=Large; deps = Deps.empty}
-let mk_conpair p = let p = mk_conpoly p in {mi = Some p; ma = Some p}
-let zero_conpoly = mk_conpoly Polynome.zero
-let zero_conpair = mk_conpair Polynome.zero
-
-let add_bound b1 b2 =
- match b1, b2 with
- | Large, Large -> Large
- | Strict, _ | _, Strict -> Strict
-
-let switch q b1 b2 =
- if Q.leq Q.zero q then b1 else b2
-
-let inv_bound = function
- | Large -> Strict
- | Strict -> Large
-
-let add_conpoly p1 p2 =
- if p2 == zero_conpoly then p1
- else if p1 == zero_conpoly then p2
- else
- { imp = Polynome.add p1.imp p2.imp;
- exp = Polynome.add p1.exp p2.exp;
- bound = add_bound p1.bound p2.bound;
- deps = Deps.concat p1.deps p2.deps}
-
-let add_conpair p1 p2 =
- {mi = Opt.map2 add_conpoly p1.mi p2.mi;
- ma = Opt.map2 add_conpoly p1.ma p2.ma}
-
-let conpair_is_an_equality p1 =
- match p1.mi, p1.ma with
- | Some mi, Some ma ->
- Polynome.equal mi.exp ma.exp &&
- Q.equal mi.exp.cst Q.zero
- | _ -> false
-
-let x_p_cy_conpoly p1 q p2 =
- if p2 == zero_conpoly then p1
- else
- {imp = Polynome.x_p_cy p1.imp q p2.imp;
- exp = Polynome.x_p_cy p1.exp q p2.exp;
- bound = add_bound p1.bound p2.bound;
- deps = Deps.concat p1.deps p2.deps
- }
-
-let cx_p_cy_conpoly q1 p1 q2 p2 =
- {imp = Polynome.cx_p_cy q1 p1.imp q2 p2.imp;
- exp = Polynome.cx_p_cy q1 p1.exp q2 p2.exp;
- bound = add_bound p1.bound p2.bound;
- deps = Deps.concat p1.deps p2.deps;
- }
-
-let cst_mult_conpoly q p =
- {imp = Polynome.mult_cst q p.imp;
- exp = Polynome.mult_cst q p.exp;
- bound = p.bound;
- deps = p.deps;
- }
-
-let cst_mult_conpair q p =
- {mi = Opt.map (cst_mult_conpoly q) (switch q p.mi p.ma);
- ma = Opt.map (cst_mult_conpoly q) (switch q p.ma p.mi);
- }
-
-let x_p_cy_conpair p1 q p2 =
- {mi = Opt.map2 (fun x y -> x_p_cy_conpoly x q y)
- p1.mi (switch q p2.mi p2.ma);
- ma = Opt.map2 (fun x y -> x_p_cy_conpoly x q y)
- p1.ma (switch q p2.ma p2.mi);
- }
-
-let cx_p_cy_conpair q1 p1 q2 p2 =
- {mi = Opt.map2 (fun x y -> cx_p_cy_conpoly q1 x q2 y)
- (switch q1 p1.mi p1.ma)
- (switch q2 p2.mi p2.ma);
- ma = Opt.map2 (fun x y -> cx_p_cy_conpoly q1 x q2 y)
- (switch q1 p1.ma p1.mi)
- (switch q2 p2.ma p2.mi);
- }
-
-let implies q p =
- begin match q.mi, p.mi with
- | _, None -> true
- | None, _ -> false
- | Some q, Some p ->
- match Polynome.is_cst (Polynome.sub p.exp q.exp) with
- | None -> false
- | Some cst ->
- let c = Q.compare Q.zero cst in
- if c = 0 then
- not (p.bound = Strict) || q.bound = Strict
- else c < 0
- end
- &&
- begin match q.ma, p.ma with
- | _, None -> true
- | None, _ -> false
- | Some q, Some p ->
- match Polynome.is_cst (Polynome.sub p.exp q.exp) with
- | None -> false
- | Some cst ->
- let c = Q.compare Q.zero cst in
- if c = 0 then
- not (p.bound = Strict) || q.bound = Strict
- else c > 0
- end
-
-(** cl1 -> cl2 *)
-let dist cl1 cl2 =
- (* contrary of vectors: here AB = OA - OB
- It is more instuitive for the distance with a constant:
- 0 <= node - c node - d <= 0
- *)
- Polynome.of_list Q.zero [cl1,Q.one;cl2,Q.minus_one]
-
-let dist_conpoly cl1 cl2 =
- mk_conpoly (dist cl1 cl2)
-
-let dist_conpair cl1 cl2 =
- mk_conpair (dist cl1 cl2)
-
-let print_conpoly fmt t =
- Format.fprintf fmt "{imp=%a;exp=%a}" Polynome.pp t.imp Polynome.pp t.exp
-
-let get_rlist_conpair_deps t cl1 cl2 deps =
- let r,deps =
- Conflict.ComputeConflict.Equal.one_equal
- t ~from:cl1 ~to_:cl2 condom zero_conpair deps
- in
- (* Debug.dprintf8 debug "cl1=%a cl2=%a r=%a dist=%a" *)
- (* Node.pp cl1 Node.pp cl2 pp_conpair r Polynome.pp (dist cl1 cl2); *)
- assert (conpair_is_an_equality r);
- assert (Polynome.equal (Opt.get r.mi).exp (dist cl1 cl2));
- r,deps
-
-let get_rlist_conpair t cl1 cl2 =
- let r, deps = get_rlist_conpair_deps t cl1 cl2 Trail.Deps.empty in
- Conflict.ComputeConflict.add_deps t deps;
- r
-
-(** Gen Equality and disequality *)
-module GenEquality = struct
- open Conflict
-
- let equality t cl1 cl2 =
- (** cl1 -> cl2 *)
- let p = get_rlist_conpair t cl1 cl2 in
- assert (conpair_is_an_equality p);
- (* Debug.dprintf6 debug "cl1=%a cl2=%a p=%a" *)
- (* Node.pp cl1 Node.pp cl2 pp_conpair p; *)
- (** cl2 -> cl1 *)
- let p = add_conpair p (dist_conpair cl2 cl1) in
- (** cl1 -> cl2 -> cl1 = 0 *)
- assert (conpair_is_an_equality p);
- assert (Polynome.is_zero (Opt.get p.mi).exp);
- Debug.dprintf6 debug "[LRA] %a=%a: %a" Node.pp cl1 Node.pp cl2 pp_conpair p;
- ComputeConflict.unknown_con t condom p
-
- let expspecial =
- { Equality.equality = equality;
- disequality = (fun t _age ~hyp:_ cl1d cl1e cl2e cl2d ->
- equality t cl1d cl1e;
- equality t cl2d cl2e);
- merged = (fun t deps _age cl1d cl1 pexp cl2 cl2d ->
- let eq_t = ComputeConflict.Equal.init condom
- zero_conpair deps ~from:cl1d in
- let eq_t = ComputeConflict.Equal.add_equal t eq_t ~to_:cl1 in
- let eq_t = ComputeConflict.Equal.add_pexp t eq_t ~to_:cl2 pexp in
- let eq_t = ComputeConflict.Equal.add_equal t eq_t ~to_:cl2d in
- let p,deps = ComputeConflict.Equal.close eq_t in
- (** cl2d -> cl1d *)
- let pd = dist_conpair cl2d cl1d in
- let p = add_conpair p pd in
- (* Debug.dprintf2 debug "sum: %a" pp_conpair p; *)
- Trail.Deps.add_unknown_con deps condom p);
- dodec = true (** TODO *);
- new_true_disequality = (fun _ _ _ -> ());
- }
-
- let () = Equality.register_sort Term._Real expspecial
-
-end
-*)
-
type hypbound =
| Eq
| Le
@@ -519,16 +422,19 @@ let pp_hyppoly fmt c =
Polynome.pp c.poly
module ChoLRA = struct
- let make_decision node b env =
+ let make_decision node v env =
Debug.dprintf4 Egraph.print_decision
- "[LRA] decide %a on %a" Q.pp b Node.pp node;
- set_dom env node (D.singleton b)
+ "[LRA] decide %a on %a" D.pp v Node.pp node;
+ set_dom env node v
let choose_decision node env =
let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
- match D.is_singleton v with
- | Some _ -> Egraph.DecNo
- | None -> DecTodo (make_decision node (D.choose v))
+ match D.split_heuristic v with
+ | `Singleton _ -> Egraph.DecNo
+ | `Splitted (v1,v2) ->
+ DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
+ | `NotSplitted ->
+ DecTodo [make_decision node (D.singleton (D.choose v))]
let choice n = {
Egraph.prio = 1;
@@ -555,7 +461,7 @@ let sub cl1 cl2 =
let neg cl2 =
index (S.Add(Q.one,zero,Q.minus_one,cl2))
-let mult _cl1 _cl2 = raise (TODO "mult without constant")
+let mult _node1 _node2 = raise (TODO "mult without constant")
let mult_cst cst node =
add' cst node Q.one zero
@@ -589,7 +495,7 @@ let converter d (f:Expr.Term.t) =
Some (add (of_term a) (of_term b))
| { descr = Expr.App({builtin = Expr.Sub},[],[a;b]); _ } ->
Some (sub (of_term a) (of_term b))
- | { descr = Expr.App({builtin = Expr.Neg},[],[a]); _ } ->
+ | { descr = Expr.App({builtin = Expr.Minus},[],[a]); _ } ->
Some (neg (of_term a))
| { descr = Expr.App({builtin = Expr.Mul},[],args); _ } -> begin
let mult_cst c t = Some (mult_cst c (of_term t)) in
@@ -640,7 +546,10 @@ let th_register env =
(fun d value ->
let v = RealValue.value value in
let s = D.singleton v in
- Egraph.set_dom d dom (RealValue.node value) s
+ Egraph.set_dom d dom (RealValue.node value) s;
+ let cl = RealValue.node value in
+ let p1 = Polynome.of_list v [] in
+ Th.solve_one d cl p1
) env;
()
@@ -686,7 +595,7 @@ let () =
!< (Q.add !>a !>b)
| { descr = Expr.App({builtin = Expr.Sub},[],[a;b]); _ } ->
!< (Q.sub !>a !>b)
- | { descr = Expr.App({builtin = Expr.Neg},[],[a]); _ } ->
+ | { descr = Expr.App({builtin = Expr.Minus},[],[a]); _ } ->
!< (Q.neg !>a)
| { descr = Expr.App({builtin = Expr.Mul},[],[a;b]); _ } ->
!< (Q.mul !>a !>b)
diff --git a/src_colibri2/theories/LRA/interval.ml b/src_colibri2/theories/LRA/interval.ml
index 3713d6c89073e9770e97a8c212c1c2cca7f6f376..f512a3cc2aca5d58ab239f3b25dfc4433da502e1 100644
--- a/src_colibri2/theories/LRA/interval.ml
+++ b/src_colibri2/theories/LRA/interval.ml
@@ -281,6 +281,27 @@ module Convexe = struct
if Q.lt q maxv then q
else Q.add maxv (Q.div_2exp (Q.sub minv maxv) 1)
+ let split_heuristic c =
+ match is_singleton c with
+ | Some s -> `Singleton s
+ | None ->
+ let split_at mid =
+ let left,right =
+ if Q.equal mid c.maxv
+ then inter (lt mid) c, inter (ge mid) c
+ else inter (le mid) c, inter (gt mid) c
+ in
+ match left, right with
+ | Some left, Some right ->
+ `Splitted(left,right)
+ | _ -> assert false
+ in
+ if Q.equal Q.minus_inf c.minv || Q.equal Q.inf c.maxv then
+ if mem Q.zero c then split_at Q.zero
+ else `NotSplitted
+ else
+ let mid = Q.div_2exp (Q.add c.minv c.maxv) (-1) in
+ split_at mid
let nb_incr = 100
let z_nb_incr = Z.of_int nb_incr
@@ -307,6 +328,28 @@ module Convexe = struct
| Q.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 Q.equal Q.minus_inf t.minv then Large else Strict;
+ minv =
+ if is_Large t.minb && Q.is_integer t.minv
+ then Q.add t.minv Q.one
+ else Q.ceil t.minv;
+ maxb = if Q.equal Q.inf t.maxv then Large else Strict;
+ maxv =
+ if is_Large t.maxb && Q.is_integer t.maxv
+ then Q.sub t.maxv Q.one
+ else Q.floor t.maxv;
+ } in
+ if Q.lt t.maxv t.minv then None else begin
+ assert (invariant t);
+ Some t
+ end
+
end
module ConvexeWithExceptions = struct
diff --git a/src_colibri2/theories/LRA/interval.mli b/src_colibri2/theories/LRA/interval.mli
index b6ca6b7b76b82ecb3e05916f32e209dd08a4e694..c6daa364c2470b3d064bdde60e56ad1f6b8e0816 100644
--- a/src_colibri2/theories/LRA/interval.mli
+++ b/src_colibri2/theories/LRA/interval.mli
@@ -28,7 +28,15 @@ val compare_bounds_inf: Q.t * bound -> Q.t * bound -> int
val compare_bounds_sup: Q.t * bound -> Q.t * bound -> int
val compare_bounds_inf_sup: Q.t * bound -> Q.t * bound -> int
-module Convexe: Interval_sig.S
+module Convexe: sig
+ include Interval_sig.S
+ val split_heuristic: t ->
+ [ `Singleton of Q.t
+ | `Splitted of t * t
+ | `NotSplitted ]
+
+ val inter_with_integer: t -> t option
+end
module ConvexeWithExceptions: Interval_sig.S
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 51cc5d5798bcf13e854f5934140f80e7b5de06e4..cfe2b0ead5e2481ab62897541c00da604fad3e87 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -442,7 +442,9 @@ module ChoBool = struct
let choose_decision node env =
match Egraph.get_value env dom node with
| Some _ -> Egraph.DecNo
- | None -> DecTodo (fun env -> make_decision env node true) (** why not true? *)
+ | None -> DecTodo
+ (List.map (fun v env -> make_decision env node v)
+ (Shuffle.shufflel [true;false]))
end
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 925afc195e2c8a48f00224fdfcb8b458aa194d32..e0158476b18dec9b33ce53b357183a4a9eb4526e 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -248,7 +248,7 @@ let norm_set d the =
true
module ChoEquals = struct
- let make_decision the (cl1,cl2) d =
+ let make_equal the (cl1,cl2) d =
Debug.dprintf6 Egraph.print_decision
"[Equality] @[decide on merge of %a and %a in %a@]"
Node.pp cl1 Node.pp cl2 ThE.pp the;
@@ -256,12 +256,23 @@ module ChoEquals = struct
Egraph.register d cl2;
Egraph.merge d cl1 cl2
+ let make_disequal the (cl1,cl2) d =
+ Debug.dprintf6 Egraph.print_decision
+ "[Equality] @[decide on merge of %a and %a in %a@]"
+ Node.pp cl1 Node.pp cl2 ThE.pp the;
+ Egraph.register d cl1;
+ Egraph.register d cl2;
+ let _dis, stag = new_tag the in
+ List.iter (fun cl -> set_dom d cl (stag ())) [cl1;cl2]
+
let choose_decision the d =
let v = ThE.sem the in
let own = ThE.node the in
Debug.dprintf4 debug "[Equality] @[dec on %a for %a@]"
Node.pp own ThE.pp the;
- if norm_set d the
+ if Boolean.is_false d own
+ then Egraph.DecNo
+ else if norm_set d the
then Egraph.DecNo
else
match find_not_disequal d v with
@@ -269,7 +280,7 @@ module ChoEquals = struct
Boolean.set_false d own;
DecNo
| `Found (cl1,cl2) ->
- DecTodo (make_decision the (cl1,cl2))
+ DecTodo [make_equal the (cl1,cl2);make_disequal the (cl1,cl2)]
let mk_choice the = {
Egraph.choice = choose_decision the;