From f2567bfb04a749ebea84db8e53b9e82c15454203 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 19 Apr 2021 22:36:43 +0200
Subject: [PATCH] Allows to attach event with Egraph.Ro
allows to do the twowatchliteral during enqueue
---
src_colibri2/core/egraph.ml | 117 ++--
src_colibri2/core/egraph.mli | 49 +-
src_colibri2/core/events.ml | 31 +-
src_colibri2/core/events.mli | 12 +-
src_colibri2/core/ground.ml | 2 +-
src_colibri2/popop_lib/bag.ml | 31 ++
src_colibri2/popop_lib/bag.mli | 3 +
src_colibri2/popop_lib/lists.ml | 11 +
src_colibri2/popop_lib/lists.mli | 2 +
.../generate_tests/generate_dune_tests.ml | 2 +-
src_colibri2/tests/solve/dimacs/sat/dune.inc | 22 +-
.../tests/solve/dimacs/unsat/dune.inc | 12 +-
src_colibri2/tests/solve/smt_adt/sat/dune.inc | 12 +-
.../tests/solve/smt_adt/unsat/dune.inc | 14 +-
src_colibri2/tests/solve/smt_lra/sat/dune.inc | 66 +--
.../tests/solve/smt_lra/unsat/dune.inc | 22 +-
src_colibri2/tests/solve/smt_nra/sat/dune.inc | 14 +-
.../tests/solve/smt_nra/unsat/dune.inc | 20 +-
.../tests/solve/smt_quant/sat/dune.inc | 8 +-
.../tests/solve/smt_quant/unsat/dune.inc | 22 +-
src_colibri2/tests/solve/smt_uf/sat/dune.inc | 42 +-
.../tests/solve/smt_uf/unsat/dune.inc | 26 +-
src_colibri2/theories/LRA/realValue.ml | 4 +-
src_colibri2/theories/bool/boolean.ml | 518 +++++++-----------
src_colibri2/theories/bool/boolean.mli | 6 -
25 files changed, 501 insertions(+), 567 deletions(-)
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 6c6152be9..a16452301 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -488,10 +488,12 @@ module Delayed = struct
let* events = ValueKind.M.find_opt valuekind valuetable.events in
Node.M.find_opt node events
in
- Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)
+ (* deletion of events are not taken into account for that kind *)
+ ignore (Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v))
);
let events = Node.M.find_opt node t.env.event_value in
- Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)
+ (* deletion of events are not taken into account for that kind *)
+ ignore (Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v))
let add_pending_merge (t : t) node node' =
Debug.dprintf4 debug "[Egraph] @[add_pending_merge for %a and %a@]"
@@ -526,26 +528,30 @@ module Delayed = struct
(** reg_node *)
let new_events, node_events = Node.M.find_remove node t.env.event_reg in
t.env.event_reg <- new_events;
- Wait.wakeup_events_list Events.Wait.translate_regnode t node_events node;
+ (* deletion of events are not taken into account for that kind *)
+ ignore (Wait.wakeup_events_list Events.Wait.translate_regnode t node_events node);
(** reg *)
- Wait.wakeup_events_list Events.Wait.translate_reg
- t (Some t.env.event_any_reg) node;
+ (* deletion of events are not taken into account for that kind *)
+ ignore (Wait.wakeup_events_list Events.Wait.translate_reg
+ t (Some t.env.event_any_reg) node);
(** reg_sem *)
match Only_for_solver.open_node node with
| Only_for_solver.ThTerm thterm ->
begin match Only_for_solver.sem_of_node thterm with
| Only_for_solver.ThTerm(sem,_) ->
let reg_events = get_table_sem t.env sem in
- Wait.wakeup_events_list Events.Wait.translate_regsem
- t (Some reg_events) (thterm)
+ (* deletion of events are not taken into account for that kind *)
+ ignore (Wait.wakeup_events_list Events.Wait.translate_regsem
+ t (Some reg_events) (thterm))
end
| Only_for_solver.Value nodevalue ->
begin match Value.kind nodevalue with
| Value(value,_) ->
let valuetable = t.env.value in
let reg_events = ValueKind.M.find_opt value valuetable.reg_events in
- Wait.wakeup_events_list Events.Wait.translate_regvalue
- t reg_events (nodevalue);
+ (* deletion of events are not taken into account for that kind *)
+ ignore (Wait.wakeup_events_list Events.Wait.translate_regvalue
+ t reg_events (nodevalue));
set_value_direct t node nodevalue
end
end
@@ -563,9 +569,11 @@ module Delayed = struct
t.env.repr <- Node.M.add node0' node t.env.repr;
(** wakeup the daemons register_node *)
let event, other_event = Node.M.find_remove node0' t.env.event_repr in
- Wait.wakeup_events_bag Events.Wait.translate_change t other_event node0';
+ (* can be always removed *)
+ ignore (Wait.wakeup_events_bag Events.Wait.translate_change t other_event node0');
t.env.event_repr <- event;
- Wait.wakeup_events_list Events.Wait.translate_change t (Some t.env.event_any_repr) node0';
+ (* deletion of events are not taken into account for that kind *)
+ ignore (Wait.wakeup_events_list Events.Wait.translate_change t (Some t.env.event_any_repr) node0');
(** set the value if node0' is one *)
match Nodes.Only_for_solver.nodevalue node0' with
| None -> ()
@@ -594,22 +602,23 @@ module Delayed = struct
let node = find_def t node0 in
let domtable = (get_table_dom t.env dom) in
let new_table = Node.M.add_opt node new_v domtable.table in
- let domtable = { domtable with table = new_table } in
+ let other_events, woken_events = Node.M.find_remove node domtable.events in
+ let domtable = { domtable with table = new_table; events = other_events } in
VDomTable.set t.env.dom dom domtable;
- let events = Node.M.find_opt node domtable.events in
- Wait.wakeup_events_bag Events.Wait.translate_dom t events (node,dom);
- Wait.wakeup_events_list Events.Wait.translate_dom t (Some domtable.reg_events) (node,dom)
-
-
- let set_dom_premerge_pending (type a) t (dom : a DomKind.t) ~from:_ node0 (new_v:a) =
- Debug.incr stats_set_dom;
- let node = find t node0 in
- let domtable = (get_table_dom t.env dom) in
- let new_table = Node.M.add node new_v domtable.table in
- let domtable = { domtable with table = new_table } in
- VDomTable.set t.env.dom dom domtable;
- let events = Node.M.find_opt node domtable.events in
- Wait.wakeup_events_bag Events.Wait.translate_dom t events (node0,dom)
+ let woken_events = Wait.wakeup_events_bag Events.Wait.translate_dom t woken_events (node,dom) in
+ begin match woken_events with
+ | None -> ()
+ | Some woken_events ->
+ let domtable = (get_table_dom t.env dom) in
+ let events =
+ Node.M.add_change (fun events -> events) (fun events b -> Bag.concat events b)
+ node woken_events
+ domtable.events in
+ let domtable = { domtable with events } in
+ VDomTable.set t.env.dom dom domtable;
+ end;
+ (* deletion of events are not taken into account *)
+ ignore (Wait.wakeup_events_list Events.Wait.translate_dom t (Some domtable.reg_events) (node,dom))
let flag_choose_repr_no_value =
Debug.register_flag
@@ -738,6 +747,10 @@ module Delayed = struct
Node.pp repr_node Node.pp repr_node0;
let event, other_event = Node.M.find_remove other_node t.env.event_repr in
+ let other_event = Wait.wakeup_events_bag
+ Events.Wait.translate_change t other_event other_node
+ in
+
(** move node events *)
begin match other_event with
| None -> ()
@@ -786,10 +799,10 @@ module Delayed = struct
(** wakeup the daemons *)
- Wait.wakeup_events_bag
- Events.Wait.translate_change t other_event other_node;
- Wait.wakeup_events_list
- Events.Wait.translate_change t (Some t.env.event_any_repr) other_node
+ t.env.event_any_repr <-
+ Option.value ~default:[] @@
+ Wait.wakeup_events_list
+ Events.Wait.translate_change t (Some t.env.event_any_repr) other_node
let continue_merge t node1_0 node2_0 inv =
let dom_not_done = merge_dom t node1_0 node2_0 inv in
@@ -934,19 +947,6 @@ module Delayed = struct
check d node;
set_dom_pending d dom node (Some v)
- let set_dom_premerge d dom node v =
- Debug.dprintf4 debug
- "[Egraph] @[set_dom_premerge for %a with %a@]"
- Node.pp node (print_dom dom) v;
- check d node;
- let node' = match d.todo_delayed_merge with
- | Some(node1,node2,_) when Node.equal node1 node -> node2
- | Some(node1,node2,_) when Node.equal node2 node -> node1
- | _ -> raise (BrokenInvariant(
- "set_dom_premerge should be used only on the \
- nodeasses currently merged")) in
- set_dom_premerge_pending d dom ~from:node' node v
-
let unset_dom d dom node =
Debug.dprintf2 debug
"[Egraph] @[unset_dom for %a@]"
@@ -1009,10 +1009,11 @@ module Delayed = struct
let event = Events.Wait.Event (dem,event) in
match find t node with
| node -> (** already registered *)
- Wait.wakeup_events_list Events.Wait.translate_regnode t (Some [event]) node
+ ignore (Wait.wakeup_events_list Events.Wait.translate_regnode t (Some [event]) node)
| exception NotRegistered ->
- t.env.event_reg <-
- Node.M.add_change Lists.singleton Lists.add node event t.env.event_reg
+ (* deletion of events are not taken into account *)
+ ignore (t.env.event_reg <-
+ Node.M.add_change Lists.singleton Lists.add node event t.env.event_reg)
let attach_reg_any t dem event =
let event = Events.Wait.Event (dem,event) in
@@ -1245,6 +1246,30 @@ module type Ro = sig
val is_current_env: t -> bool
+ (** {3 Attach Event} *)
+ (** todo rename events and attachment *)
+
+ val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when the dom of the node change *)
+ val attach_any_dom: t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when the dom of any node change *)
+ val attach_value: t -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a value is attached to this equivalence class *)
+ val attach_any_value: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when any kind of value is attached to this equivalence class *)
+ val attach_reg_any: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when any node is registered *)
+ val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when this node is registered *)
+ val attach_reg_sem: t -> 'a ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a new semantical class is registered *)
+ val attach_reg_value: t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a new value is registered *)
+ val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when it is not anymore the representative class *)
+ val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a node is not its representative class anymore *)
+
end
module Ro : Ro with type t = Delayed.t = Delayed
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index a964f1b73..6cf8108ce 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -68,6 +68,30 @@ module type Ro = sig
val is_current_env: t -> bool
+ (** {3 Attach Event} *)
+ (** todo rename events and attachment *)
+
+ val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when the dom of the node change *)
+ val attach_any_dom: t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when the dom of any node change *)
+ val attach_value: t -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a value is attached to this equivalence class *)
+ val attach_any_value: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when any kind of value is attached to this equivalence class *)
+ val attach_reg_any: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when any node is registered *)
+ val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when this node is registered *)
+ val attach_reg_sem: t -> 'a ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a new semantical class is registered *)
+ val attach_reg_value: t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a new value is registered *)
+ val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when it is not anymore the representative class *)
+ val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+ (** wakeup when a node is not its representative class anymore *)
+
end
module Ro : Ro
@@ -92,31 +116,6 @@ val set_value: t -> Node.t -> Value.t -> unit
val merge : t -> Node.t -> Node.t -> unit
-
-(** {3 Attach Event} *)
-(** todo rename events and attachment *)
-
-val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when the dom of the node change *)
-val attach_any_dom: t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when the dom of any node change *)
-val attach_value: t -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a value is attached to this equivalence class *)
-val attach_any_value: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when any kind of value is attached to this equivalence class *)
-val attach_reg_any: t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when any node is registered *)
-val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when this node is registered *)
-val attach_reg_sem: t -> 'a ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a new semantical class is registered *)
-val attach_reg_value: t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a new value is registered *)
-val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when it is not anymore the representative class *)
-val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a node is not its representative class anymore *)
-
type choice_state =
| DecNo
| DecTodo of (t -> unit) list
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index d6182f65a..0398fdf73 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -128,6 +128,7 @@ module Wait = struct
type _ enqueue =
| EnqRun: 'r -> 'r enqueue
+ | EnqLast: 'r -> 'r enqueue
| EnqAlready: _ enqueue
| EnqRedirected: ('e,'r) Dem.t * 'e -> _ enqueue
| EnqStopped: _ enqueue
@@ -184,13 +185,13 @@ module Wait = struct
val new_pending_daemon : delayed -> ('a, 'b) Dem.t -> 'b -> unit
- val wakeup_event : 'a translate -> delayed -> 'a -> t -> unit
+ val wakeup_event : 'a translate -> delayed -> 'a -> t -> t option
val wakeup_events_list :
- 'a translate -> delayed -> t list option -> 'a -> unit
+ 'a translate -> delayed -> t list option -> 'a -> t list option
val wakeup_events_bag :
- 'a translate -> delayed -> t Bag.t option -> 'a -> unit
+ 'a translate -> delayed -> t Bag.t option -> 'a -> t Bag.t option
val is_well_initialized : unit -> bool
end
@@ -261,31 +262,33 @@ module Wait = struct
let wakeup_event translate t info wevent =
match wevent with
| Event (dem,event) ->
- let rec f : type event r. S.delayed -> (event,r) Dem.t -> event -> unit =
- fun t dem event ->
+ let rec f : type event r. S.delayed -> (event,r) Dem.t -> event -> _ -> _ =
+ fun t dem event wevent ->
let module Dem = (val get_dem dem) in
let event = translate.translate info event in
match Dem.enqueue (S.readonly t) event with
- | EnqStopped -> () (** todo remove from the list of event *)
- | EnqAlready -> ()
- | EnqRedirected(dem,event) -> f t dem event
- | EnqRun runable -> new_pending_daemon t dem runable
+ | EnqStopped -> None
+ | EnqAlready -> Some wevent
+ | EnqRedirected(dem,event) -> f t dem event (Event(dem,event))
+ | EnqRun runable -> new_pending_daemon t dem runable; Some wevent
+ | EnqLast runable -> new_pending_daemon t dem runable; None
in
- f t dem event
+ f t dem event wevent
let wakeup_events_list translate t events info =
match events with
| None | Some [] ->
- Debug.dprintf0 debug "[Egraph] @[No scheduling@]"
+ Debug.dprintf0 debug "[Egraph] @[No scheduling@]";
+ None
| Some events ->
- List.iter (wakeup_event translate t info) events
+ Some (Lists.filter_map_homo (wakeup_event translate t info) events)
let wakeup_events_bag translate t events info =
let is_empty = match events with
| None -> true
| Some events -> Bag.is_empty events in
- if is_empty then Debug.dprintf0 debug "[Egraph] @[No scheduling@]"
- else Bag.iter (wakeup_event translate t info) (Opt.get events)
+ if is_empty then (Debug.dprintf0 debug "[Egraph] @[No scheduling@]"; None)
+ else Some (Bag.filter_map_homo (wakeup_event translate t info) (Opt.get events))
end
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index df4af5f05..a0f82a433 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -64,9 +64,15 @@ module Wait : sig
type _ enqueue =
| EnqRun: 'r -> 'r enqueue
+ (** Schedule a daemon run *)
+ | EnqLast: 'r -> 'r enqueue
+ (** Same as EnqRun but remove the waiting event *)
| EnqAlready: _ enqueue
+ (** Don't run but keep the waiting event *)
| EnqRedirected: ('e,'r) Dem.t * 'e -> _ enqueue
+ (** Run another daemon *)
| EnqStopped: _ enqueue
+ (** Stop and don't run *)
type daemon_key =
| DaemonKey: ('k,'runable) Dem.t * 'runable -> daemon_key
@@ -114,13 +120,13 @@ module Wait : sig
val new_pending_daemon : delayed -> ('a, 'b) Dem.t -> 'b -> unit
- val wakeup_event : 'a translate -> delayed -> 'a -> t -> unit
+ val wakeup_event : 'a translate -> delayed -> 'a -> t -> t option
val wakeup_events_list :
- 'a translate -> delayed -> t list option -> 'a -> unit
+ 'a translate -> delayed -> t list option -> 'a -> t list option
val wakeup_events_bag :
- 'a translate -> delayed -> t Bag.t option -> 'a -> unit
+ 'a translate -> delayed -> t Bag.t option -> 'a -> t Bag.t option
val is_well_initialized : unit -> bool
end
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index f6998ec99..62762e173 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -105,7 +105,7 @@ module Term = struct
let pp fmt t =
let infix sep =
- Fmt.(array_paren ~sep:(fun fmt () -> Fmt.pf fmt "@ %s" sep) ~paren:parens Node.pp) fmt t.args
+ Fmt.(array_paren ~sep:(fun fmt () -> Fmt.pf fmt "@ %s " sep) ~paren:parens Node.pp) fmt t.args
in
match t.app.builtin with
| Expr.Equal
diff --git a/src_colibri2/popop_lib/bag.ml b/src_colibri2/popop_lib/bag.ml
index 6b0c87eaf..4f3ff8024 100644
--- a/src_colibri2/popop_lib/bag.ml
+++ b/src_colibri2/popop_lib/bag.ml
@@ -137,6 +137,37 @@ let rec filter f = function
| List xs -> list (List.filter f xs)
| Concat(a,b) -> concat (filter f a) (filter f b)
+let rec filter_map_homo f = function
+ | Empty -> Empty
+ | Elt x as e -> (match f x with | Some x' -> if x == x' then e else Elt x'
+ | None -> Empty)
+ | Add(x,ts) as e -> (match f x with
+ | Some x' when x == x' ->
+ let ts' = filter_map_homo f ts in
+ if ts == ts' then e else add x' ts'
+ | Some x' -> add x' (filter_map_homo f ts)
+ | None -> filter_map_homo f ts)
+ | App(ts,x) as e -> (match f x with
+ | Some x' when x == x' ->
+ let ts' = filter_map_homo f ts in
+ if ts == ts' then e else append ts' x'
+ | Some x' -> append (filter_map_homo f ts) x'
+ | None -> filter_map_homo f ts)
+ | List xs as e ->
+ let rec aux f same old accu = function
+ | [] -> if same then old else list (List.rev accu)
+ | x :: l ->
+ match f x with
+ | None -> aux f false old accu l
+ | Some v when v == x -> aux f same old (v :: accu) l
+ | Some v -> aux f false old (v :: accu) l
+ in
+ aux f true e [] xs
+ | Concat(a,b) as e ->
+ let a' = (filter_map_homo f a) in
+ let b' = (filter_map_homo f b) in
+ if a == a' && b == b' then e else concat a' b'
+
let rec partition f = function
| Empty -> Empty , Empty
| Elt x as e -> if f x then e,Empty else Empty,e
diff --git a/src_colibri2/popop_lib/bag.mli b/src_colibri2/popop_lib/bag.mli
index 36ed27e03..20a788d2b 100644
--- a/src_colibri2/popop_lib/bag.mli
+++ b/src_colibri2/popop_lib/bag.mli
@@ -44,6 +44,9 @@ val for_all : ('a -> bool) -> 'a t -> bool
val exists : ('a -> bool) -> 'a t -> bool
val filter : ('a -> bool) -> 'a t -> 'a t
+val filter_map_homo : ('a -> 'a option) -> 'a t -> 'a t
+(** homogeneous, physical identity kept for identity *)
+
val partition : ('a -> bool) -> 'a t -> 'a t * 'a t
val length : 'a t -> int
diff --git a/src_colibri2/popop_lib/lists.ml b/src_colibri2/popop_lib/lists.ml
index b71605127..f16a4477f 100644
--- a/src_colibri2/popop_lib/lists.ml
+++ b/src_colibri2/popop_lib/lists.ml
@@ -141,3 +141,14 @@ let rec last_rev n = function
else rev,a::rem, n
let hash f = List.fold_left (fun acc x -> (f x) * 65599 + acc)
+
+let filter_map_homo f l =
+ let rec aux f same old accu = function
+ | [] -> if same then old else List.rev accu
+ | x :: l ->
+ match f x with
+ | None -> aux f false old accu l
+ | Some v when v == x -> aux f same old (v :: accu) l
+ | Some v -> aux f false old (v :: accu) l
+ in
+ aux f true l [] l
diff --git a/src_colibri2/popop_lib/lists.mli b/src_colibri2/popop_lib/lists.mli
index 8d593933f..d0c772b6c 100644
--- a/src_colibri2/popop_lib/lists.mli
+++ b/src_colibri2/popop_lib/lists.mli
@@ -88,3 +88,5 @@ val last_rev : int -> 'a list -> 'a list * 'a list * int
*)
val hash: ('a -> int) -> int -> 'a list -> int
+
+val filter_map_homo: ('a -> 'a option) -> 'a list -> 'a list
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index c4b59b529..7155d1b70 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -3,7 +3,7 @@ let result = Sys.argv.(2)
let print_test cout file =
Printf.fprintf cout
- "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 1300 %%{dep:%s}))))\n"
+ "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 3000 %%{dep:%s}))))\n"
file file;
Printf.fprintf cout
"(rule (alias runtest) (action (diff oracle %s.res)))\n"
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
index 321eff408..a3f62fc4b 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -1,23 +1,23 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:anomaly_agetooold.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:anomaly_agetooold2.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold2.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res)))
-(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:assertion_fail.cnf}))))
+(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:assertion_fail.cnf}))))
(rule (alias runtest) (action (diff oracle assertion_fail.cnf.res)))
-(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:fuzzing1.cnf}))))
+(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing1.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing1.cnf.res)))
-(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:fuzzing2.cnf}))))
+(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing2.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing2.cnf.res)))
-(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:par8-1-c.cnf}))))
+(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep: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 %{bin:colibri2} --max-step 1300 %{dep:pigeon-2.cnf}))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-3.cnf}))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-4.cnf}))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
-(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:quinn.cnf}))))
+(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:quinn.cnf}))))
(rule (alias runtest) (action (diff oracle quinn.cnf.res)))
-(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:simple_v3_c2.cnf}))))
+(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:simple_v3_c2.cnf}))))
(rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res)))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
index 6d83227b4..5766ddefe 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -1,13 +1,13 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:anomaly_agetooold.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:modus_ponens.cnf}))))
+(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:modus_ponens.cnf}))))
(rule (alias runtest) (action (diff oracle modus_ponens.cnf.res)))
-(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-1.cnf}))))
+(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-1.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-1.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-2.cnf}))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-3.cnf}))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-4.cnf}))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/sat/dune.inc b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
index 5c9df097e..38973a521 100644
--- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
@@ -1,13 +1,13 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum.smt2}))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
(rule (alias runtest) (action (diff oracle enum.smt2.res)))
-(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list0.smt2}))))
+(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
-(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list1.smt2}))))
+(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
(rule (alias runtest) (action (diff oracle list1.smt2.res)))
-(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:tree1.smt2}))))
+(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree1.smt2}))))
(rule (alias runtest) (action (diff oracle tree1.smt2.res)))
-(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:tree2.smt2}))))
+(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree2.smt2}))))
(rule (alias runtest) (action (diff oracle tree2.smt2.res)))
-(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:tree3.smt2}))))
+(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree3.smt2}))))
(rule (alias runtest) (action (diff oracle tree3.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index b72105b22..9c4a2ebd5 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -1,15 +1,15 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum.smt2}))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
(rule (alias runtest) (action (diff oracle enum.smt2.res)))
-(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum2.smt2}))))
+(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum2.smt2}))))
(rule (alias runtest) (action (diff oracle enum2.smt2.res)))
-(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list0.smt2}))))
+(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
-(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list1.smt2}))))
+(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
(rule (alias runtest) (action (diff oracle list1.smt2.res)))
-(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list2.smt2}))))
+(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list2.smt2}))))
(rule (alias runtest) (action (diff oracle list2.smt2.res)))
-(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list3.smt2}))))
+(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list3.smt2}))))
(rule (alias runtest) (action (diff oracle list3.smt2.res)))
-(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list4.smt2}))))
+(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list4.smt2}))))
(rule (alias runtest) (action (diff oracle list4.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
index d5fd2eeb1..b5a74a06e 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -1,67 +1,67 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_CombiRepr_normalize.smt2}))))
+(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_CombiRepr_normalize.smt2}))))
(rule (alias runtest) (action (diff oracle arith_CombiRepr_normalize.smt2.res)))
-(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_conflict_add_disequality.smt2}))))
+(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conflict_add_disequality.smt2}))))
(rule (alias runtest) (action (diff oracle arith_conflict_add_disequality.smt2.res)))
-(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_conpoly.smt2}))))
+(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conpoly.smt2}))))
(rule (alias runtest) (action (diff oracle arith_conpoly.smt2.res)))
-(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
+(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
(rule (alias runtest) (action (diff oracle arith_decide_must_test_is_dis_equal.smt2.res)))
-(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_init_always_merge_itself.smt2}))))
+(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_always_merge_itself.smt2}))))
(rule (alias runtest) (action (diff oracle arith_init_always_merge_itself.smt2.res)))
-(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
+(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
(rule (alias runtest) (action (diff oracle arith_init_and_propa_must_be_ordered.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case1.smt2}))))
+(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case1.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case1.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case_4.smt2}))))
+(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case_4.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case_4_bis.smt2}))))
+(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4_bis.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case_4_bis.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_coef_of_repr_is_one.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_itself_last_case.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_last_case.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_last_case.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_pivot_not_in_p12.smt2.res)))
-(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_must_use_find.smt2}))))
+(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_must_use_find.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_must_use_find.smt2.res)))
-(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_mult_explication.smt2}))))
+(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_explication.smt2}))))
(rule (alias runtest) (action (diff oracle arith_mult_explication.smt2.res)))
-(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
+(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
(rule (alias runtest) (action (diff oracle arith_mult_not_linear_in_conflict.smt2.res)))
-(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_normalize_use_find_def.smt2}))))
+(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_normalize_use_find_def.smt2}))))
(rule (alias runtest) (action (diff oracle arith_normalize_use_find_def.smt2.res)))
-(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_own_repr.smt2}))))
+(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_own_repr.smt2}))))
(rule (alias runtest) (action (diff oracle arith_own_repr.smt2.res)))
-(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_propacl.smt2}))))
+(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_propacl.smt2}))))
(rule (alias runtest) (action (diff oracle arith_propacl.smt2.res)))
-(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_subst_and_conflict_add.smt2}))))
+(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_subst_and_conflict_add.smt2}))))
(rule (alias runtest) (action (diff oracle arith_subst_and_conflict_add.smt2.res)))
-(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_zero_dom.smt2}))))
+(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_zero_dom.smt2}))))
(rule (alias runtest) (action (diff oracle arith_zero_dom.smt2.res)))
-(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:attach_only_when_dom_present.smt2}))))
+(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:attach_only_when_dom_present.smt2}))))
(rule (alias runtest) (action (diff oracle attach_only_when_dom_present.smt2.res)))
-(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:init_not_repr.smt2}))))
+(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:init_not_repr.smt2}))))
(rule (alias runtest) (action (diff oracle init_not_repr.smt2.res)))
-(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le.smt2}))))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
(rule (alias runtest) (action (diff oracle le.smt2.res)))
-(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le2.smt2}))))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
(rule (alias runtest) (action (diff oracle le2.smt2.res)))
-(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul.smt2}))))
+(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
(rule (alias runtest) (action (diff oracle mul.smt2.res)))
-(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:sem_invariant_in_learnt_dec.smt2}))))
+(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:sem_invariant_in_learnt_dec.smt2}))))
(rule (alias runtest) (action (diff oracle sem_invariant_in_learnt_dec.smt2.res)))
-(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_add_pexp_cl.smt2}))))
+(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_add_pexp_cl.smt2}))))
(rule (alias runtest) (action (diff oracle solver_add_pexp_cl.smt2.res)))
-(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
+(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
(rule (alias runtest) (action (diff oracle solver_arith_homogeneous_dist_sign.smt2.res)))
-(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_merge_itself_repr_inside.smt2}))))
+(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_inside.smt2}))))
(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_inside.smt2.res)))
-(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
+(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
(rule (alias runtest) (action (diff oracle solver_set_pending_merge_expsameexp.smt2.res)))
-(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_subst_eventdom_find.smt2}))))
+(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_subst_eventdom_find.smt2}))))
(rule (alias runtest) (action (diff oracle solver_subst_eventdom_find.smt2.res)))
-(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real.smt2}))))
+(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
(rule (alias runtest) (action (diff oracle to_real.smt2.res)))
-(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real2.smt2}))))
+(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
(rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 533c77d3f..7247c5c7a 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -1,23 +1,23 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_ExpMult_by_zero.smt2}))))
+(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_ExpMult_by_zero.smt2}))))
(rule (alias runtest) (action (diff oracle arith_ExpMult_by_zero.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case2.smt2}))))
+(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case2.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case2.smt2.res)))
-(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le.smt2}))))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
(rule (alias runtest) (action (diff oracle le.smt2.res)))
-(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le2.smt2}))))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
(rule (alias runtest) (action (diff oracle le2.smt2.res)))
-(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul.smt2}))))
+(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
(rule (alias runtest) (action (diff oracle mul.smt2.res)))
-(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:repr_and_poly.smt2}))))
+(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_and_poly.smt2}))))
(rule (alias runtest) (action (diff oracle repr_and_poly.smt2.res)))
-(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:repr_fourier.smt2}))))
+(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_fourier.smt2}))))
(rule (alias runtest) (action (diff oracle repr_fourier.smt2.res)))
-(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_merge_itself_repr_empty.smt2}))))
+(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_empty.smt2}))))
(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res)))
-(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_set_sem_merge_sign.smt2}))))
+(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_sem_merge_sign.smt2}))))
(rule (alias runtest) (action (diff oracle solver_set_sem_merge_sign.smt2.res)))
-(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real.smt2}))))
+(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
(rule (alias runtest) (action (diff oracle to_real.smt2.res)))
-(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real2.smt2}))))
+(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
(rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_nra/sat/dune.inc b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
index 7fd6061c9..4933b571d 100644
--- a/src_colibri2/tests/solve/smt_nra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
@@ -1,15 +1,15 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:ceil.smt2}))))
+(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
(rule (alias runtest) (action (diff oracle ceil.smt2.res)))
-(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos.smt2}))))
+(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos_lt.smt2}))))
+(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
-(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut.smt2}))))
+(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
-(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut2.smt2}))))
+(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
-(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos.smt2}))))
+(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
-(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos_lt.smt2}))))
+(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
index 3ea098f59..3910cff2d 100644
--- a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -1,21 +1,21 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:ceil.smt2}))))
+(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
(rule (alias runtest) (action (diff oracle ceil.smt2.res)))
-(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos.smt2}))))
+(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos_lt.smt2}))))
+(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos_lt_to_real.smt2}))))
+(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt_to_real.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt_to_real.smt2.res)))
-(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:floor.smt2}))))
+(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:floor.smt2}))))
(rule (alias runtest) (action (diff oracle floor.smt2.res)))
-(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut.smt2}))))
+(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
-(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut2.smt2}))))
+(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
-(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos.smt2}))))
+(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
-(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos_lt.smt2}))))
+(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
-(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos_zero_le.smt2}))))
+(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_zero_le.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_zero_le.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune.inc b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
index d88d5660a..cc94dac97 100644
--- a/src_colibri2/tests/solve/smt_quant/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
@@ -1,9 +1,9 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists.smt2}))))
+(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
(rule (alias runtest) (action (diff oracle exists.smt2.res)))
-(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall0.smt2}))))
+(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
(rule (alias runtest) (action (diff oracle forall0.smt2.res)))
-(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall3.smt2}))))
+(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
(rule (alias runtest) (action (diff oracle forall3.smt2.res)))
-(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall4.smt2}))))
+(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
(rule (alias runtest) (action (diff oracle forall4.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index 63371f6c6..b5b0d9392 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -1,23 +1,23 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists.smt2}))))
+(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
(rule (alias runtest) (action (diff oracle exists.smt2.res)))
-(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists2.smt2}))))
+(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists2.smt2}))))
(rule (alias runtest) (action (diff oracle exists2.smt2.res)))
-(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall0.smt2}))))
+(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
(rule (alias runtest) (action (diff oracle forall0.smt2.res)))
-(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall1.smt2}))))
+(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall1.smt2}))))
(rule (alias runtest) (action (diff oracle forall1.smt2.res)))
-(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall2.smt2}))))
+(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall2.smt2}))))
(rule (alias runtest) (action (diff oracle forall2.smt2.res)))
-(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall3.smt2}))))
+(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
(rule (alias runtest) (action (diff oracle forall3.smt2.res)))
-(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall4.smt2}))))
+(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
(rule (alias runtest) (action (diff oracle forall4.smt2.res)))
-(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall5.smt2}))))
+(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall5.smt2}))))
(rule (alias runtest) (action (diff oracle forall5.smt2.res)))
-(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall6.smt2}))))
+(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall6.smt2}))))
(rule (alias runtest) (action (diff oracle forall6.smt2.res)))
-(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall7.smt2}))))
+(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall7.smt2}))))
(rule (alias runtest) (action (diff oracle forall7.smt2.res)))
-(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall8.smt2}))))
+(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall8.smt2}))))
(rule (alias runtest) (action (diff oracle forall8.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
index 6b3b16500..d9082d43c 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -1,43 +1,43 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:bad_conflict.smt2}))))
+(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bad_conflict.smt2}))))
(rule (alias runtest) (action (diff oracle bad_conflict.smt2.res)))
-(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:bcp_dont_like_duplicate.smt2}))))
+(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bcp_dont_like_duplicate.smt2}))))
(rule (alias runtest) (action (diff oracle bcp_dont_like_duplicate.smt2.res)))
-(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:bool_not_propa.smt2}))))
+(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bool_not_propa.smt2}))))
(rule (alias runtest) (action (diff oracle bool_not_propa.smt2.res)))
-(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:boolexpup.smt2}))))
+(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:boolexpup.smt2}))))
(rule (alias runtest) (action (diff oracle boolexpup.smt2.res)))
-(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:clause_normalization.smt2}))))
+(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clause_normalization.smt2}))))
(rule (alias runtest) (action (diff oracle clause_normalization.smt2.res)))
-(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:clmerge.smt2}))))
+(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clmerge.smt2}))))
(rule (alias runtest) (action (diff oracle clmerge.smt2.res)))
-(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:conflict_complete_needed_cl.smt2}))))
+(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:conflict_complete_needed_cl.smt2}))))
(rule (alias runtest) (action (diff oracle conflict_complete_needed_cl.smt2.res)))
-(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:directdom_not.smt2}))))
+(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:directdom_not.smt2}))))
(rule (alias runtest) (action (diff oracle directdom_not.smt2.res)))
-(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:dis_dom_before_first_age.smt2}))))
+(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dis_dom_before_first_age.smt2}))))
(rule (alias runtest) (action (diff oracle dis_dom_before_first_age.smt2.res)))
-(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:dom_merge_equality.smt2}))))
+(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dom_merge_equality.smt2}))))
(rule (alias runtest) (action (diff oracle dom_merge_equality.smt2.res)))
-(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality.smt2}))))
+(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality.smt2}))))
(rule (alias runtest) (action (diff oracle equality.smt2.res)))
-(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality_condis.smt2}))))
+(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_condis.smt2}))))
(rule (alias runtest) (action (diff oracle equality_condis.smt2.res)))
-(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality_get_sem.smt2}))))
+(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_get_sem.smt2}))))
(rule (alias runtest) (action (diff oracle equality_get_sem.smt2.res)))
-(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exp_sem_equality.smt2}))))
+(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exp_sem_equality.smt2}))))
(rule (alias runtest) (action (diff oracle exp_sem_equality.smt2.res)))
-(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:explimit_cl_equality.smt2}))))
+(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:explimit_cl_equality.smt2}))))
(rule (alias runtest) (action (diff oracle explimit_cl_equality.smt2.res)))
-(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:implication.smt2}))))
+(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:implication.smt2}))))
(rule (alias runtest) (action (diff oracle implication.smt2.res)))
-(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:intmap_set_disjoint.smt2}))))
+(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:intmap_set_disjoint.smt2}))))
(rule (alias runtest) (action (diff oracle intmap_set_disjoint.smt2.res)))
-(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:is_equal_not_propagated.smt2}))))
+(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:is_equal_not_propagated.smt2}))))
(rule (alias runtest) (action (diff oracle is_equal_not_propagated.smt2.res)))
-(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:ite_sem_bool.smt2}))))
+(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ite_sem_bool.smt2}))))
(rule (alias runtest) (action (diff oracle ite_sem_bool.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:polyeq_genequality.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
-(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:substupfalse_equality.smt2}))))
+(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:substupfalse_equality.smt2}))))
(rule (alias runtest) (action (diff oracle substupfalse_equality.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index 0195ec1bf..137b8afa1 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -1,27 +1,27 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
+(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
(rule (alias runtest) (action (diff oracle NEQ004_size4__decide_eq_us.smt2.res)))
-(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:deltaed0.smt2}))))
+(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:deltaed0.smt2}))))
(rule (alias runtest) (action (diff oracle deltaed0.smt2.res)))
-(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:diff_to_value_for_bool.smt2}))))
+(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_to_value_for_bool.smt2}))))
(rule (alias runtest) (action (diff oracle diff_to_value_for_bool.smt2.res)))
-(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:diff_value_substupfalse.smt2}))))
+(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_value_substupfalse.smt2}))))
(rule (alias runtest) (action (diff oracle diff_value_substupfalse.smt2.res)))
-(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:distinct.smt2}))))
+(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:distinct.smt2}))))
(rule (alias runtest) (action (diff oracle distinct.smt2.res)))
-(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:eq_diamond2.smt2}))))
+(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:eq_diamond2.smt2}))))
(rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res)))
-(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality_norm_set.smt2}))))
+(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_norm_set.smt2}))))
(rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res)))
-(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:fundef.smt2}))))
+(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:fundef.smt2}))))
(rule (alias runtest) (action (diff oracle fundef.smt2.res)))
-(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
+(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
(rule (alias runtest) (action (diff oracle get_repr_at__instead_of__equal_CRepr.smt2.res)))
-(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:many_distinct.smt2}))))
+(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:many_distinct.smt2}))))
(rule (alias runtest) (action (diff oracle many_distinct.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:polyeq_genequality.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:polyeq_genequality_deltaed.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality_deltaed.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality_deltaed.smt2.res)))
-(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:xor.smt2}))))
+(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:xor.smt2}))))
(rule (alias runtest) (action (diff oracle xor.smt2.res)))
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index a99103e3d..4410b095a 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -231,7 +231,7 @@ assert ( IArray.is_empty args);
assert ( IArray.is_empty args);
merge (cst (Q.of_string_decimal s))
| { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
-let a,b = IArray.extract2_exn args in
+ let a,b = IArray.extract2_exn args in
reg a; reg b; Check.attach d f;
let wait =
set r (let+ va = get a and+ vb = get b in Q.add va vb) &&
@@ -240,7 +240,7 @@ let a,b = IArray.extract2_exn args in
in
List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
| { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
-let a,b = IArray.extract2_exn args in
+ let a,b = IArray.extract2_exn args in
reg a; reg b; Check.attach d f;
let wait =
set r (let+ va = get a and+ vb = get b in Q.sub va vb) &&
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 7278dc237..b3ee59315 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -70,355 +70,206 @@ let set_bool env node b =
let mulbool b1 b2 = not(Equal.bool b1 b2)
-module T = struct
- open Base
- type t =
- { topnot: bool;
- lits: (Node.t * bool) IArray.t;
- }
- [@@deriving eq,ord,hash]
-
-
- let print_cl fmt node b =
- if b
- then Fmt.pf fmt "¬ %a" Node.pp node
- else Node.pp fmt node
-
- let isnot v =
- if IArray.length v.lits = 1 then
- let node,sign = IArray.get v.lits 0 in
- assert (v.topnot && not sign);
- Some node
- else
- None
-
- let pp fmt x =
- match isnot x with
- | Some node ->
- print_cl fmt node true
- | None ->
- let print_cl topnot fmt (node,b) = print_cl fmt node (mulbool topnot b) in
- let aux b fmt' m = IArray.fold ~f:(fun sofar e -> e::sofar) ~init:[] m
- |> List.rev
- |> Fmt.(list ~sep:(const char ',') (print_cl b) fmt')
- in
- if x.topnot
- then Fmt.pf fmt "â‹€(%a)" (aux true) x.lits
- else Fmt.pf fmt "â‹(%a)" (aux false) x.lits
-
-end
-
-let sem = ThTermKind.create_key (module struct type t = T.t let name = "Prop" end)
-
-(* let iter f x = IArray.iter f x.lits *)
-
-let fold f acc x = IArray.fold ~f ~init:acc x.T.lits
-
-let find x n =
- fold (fun acc (n1,b) -> if Node.equal n1 n then Some b else acc) None x
-
-let node_of_bool b =
- if b then node_true else node_false
-
-module Th = struct
- include T
- include MkDatatype(T)
-
- let key = sem
+let _true = node_true
+let _false = node_false
- exception TopKnown of bool
+let set_true env node = set_bool env node true
+let set_false env node = set_bool env node false
- exception Found of Node.t * bool
- let find_not_known d l =
- IArray.iter ~f:(fun (node,b) ->
- match Egraph.get_value d node with
- | Some _ -> ()
- | None -> raise (Found (node,b))
- ) l
+let a = Expr.Term.Var.mk "a" Expr.Ty.bool
+let ta = Expr.Term.of_var a
- let _bcp d l absorbent =
- try
- let res = IArray.fold ~f:(fun acc node ->
- match is d node, acc with
- | Some b, _ when Bool.equal b absorbent -> raise (TopKnown absorbent)
- | Some _, _ -> acc
- | None, Some _ -> raise Exit
- | None, None -> Some node)
- ~init:None l in
- match res with
- | None -> raise (TopKnown (not absorbent))
- | _ -> res
- with Exit -> None
+let _not =
+ let e = Expr.Term.neg ta in
+ fun na ->
+ let subst = { Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [a,na] } in
+ Ground.convert ~subst e
-end
+let _gen mk l =
+ let v = List.map (fun _ -> Expr.Term.Var.mk "b" Expr.Ty.bool) l in
+ let t = List.map Expr.Term.of_var v in
+ let subst = { Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list (List.combine v l) } in
+ Ground.convert ~subst (mk t)
-module ThE = ThTermKind.Register(Th)
+let _and = _gen Expr.Term._and
+let _or = _gen Expr.Term._or
-module DaemonPropaNot = struct
+(** {2 Choice on bool} *)
- module Data = struct
- type t = Th.t * Node.t * Node.t
- let pp fmt (v,cl1,cl2) =
- Format.fprintf fmt "%a,%a -> %a" Th.pp v Node.pp cl1 Node.pp cl2
- end
+module ChoBool = struct
+ let make_decision env node b =
+ Debug.dprintf3 Egraph.print_decision "[Bool] decide %b on %a" b Node.pp node;
+ set_bool env node b
- let delay = Events.Delayed_by 1
- let key = Demon.Fast.create "Bool.DaemonPropaNot"
- let throttle = 100
- let wakeup d =
- function
- | Events.Fired.EventValue(_,_,((_,node,ncl))) ->
- begin match is d node with
- | None -> raise Impossible
- | Some b ->
- set_bool d ncl (not b)
- end;
- | _ -> raise UnwaitedEvent
-
- let init d thterm node =
- let v = ThE.sem thterm in
- let own = ThE.node thterm in
- match is d own with
- | Some b ->
- set_bool d node (not b)
- | None ->
- match is d node with
- | Some b ->
- set_bool d own (not b)
- | None ->
- let events = [Demon.Create.EventValue(own,dom,(v,own,node));
- Demon.Create.EventValue(node,dom,(v,node,own))] in
- Demon.Fast.attach d key events
+ let choose_decision node env =
+ match is env node with
+ | Some _ ->
+ Debug.dprintf2 Egraph.print_decision "[Bool] No decision for %a" Node.pp node;
+ Egraph.DecNo
+ | None -> DecTodo
+ (List.map (fun v env -> make_decision env node v)
+ (Shuffle.shufflel [true;false]))
end
-module RDaemonPropaNot = Demon.Fast.Register(DaemonPropaNot)
+let chobool n = {
+ Egraph.prio = 1;
+ choice = ChoBool.choose_decision n;
+}
-module DaemonPropa = struct
- type watcher = (int,int) Context.Ref2.t
+module TwoWatchLiteral = struct
+ (** todo move the check to enqueue; but it requires to be able to attach event
+ in delayed_ro *)
- type d =
- | Lit of ThE.t (* prop *) * int (* watched *) * watcher
- | All of ThE.t
+ module Daemon = struct
+ type t = {
+ absorbent: Value.t;
+ ground : Ground.t; (** perhaps ground should have an array for args *)
+ from_start : int Context.Ref.t; (** already set before *)
+ from_end : int Context.Ref.t; (** already set after *)
+ }
- let key = Demon.Fast.create "Bool.DaemonPropa"
+ type runable = (Egraph.t -> unit)
- module Data = struct
- type t = d
- let pp fmt = function
- | Lit (thterm,i,w) ->
- let w,n = Context.Ref2.get w in
- Format.fprintf fmt "Lit(%a,%i(%i,%i),%a)" ThE.pp thterm i w n
- Node.pp (ThE.node thterm)
- | All thterm -> Format.fprintf fmt "All(%a)" ThE.pp thterm
- end
+ let print_runable = Fmt.nop
- let delay = Events.Delayed_by 1
- let throttle = 100
-
- let wakeup_lit d thterm watched watcher =
- let v = ThE.sem thterm in
- let own = ThE.node thterm in
- let set_dom_up_true d own _ _ =
- let b = (not v.topnot) in
- match is d own with
- | Some b' when Equal.bool b' b -> ()
- | _ -> set_bool d own b in
- let merge_bcp node sign =
- Debug.dprintf2 debug "[Bool] @[merge_bcp %a@]" Node.pp node;
- match is d own with
- | Some b' ->
- let b = mulbool sign (mulbool b' v.topnot) in
- set_bool d node b
- | None -> (** merge *)
- match is d node with
- | Some b' ->
- let b = mulbool sign (mulbool b' v.topnot) in
- set_bool d own b
- | None -> (** merge *)
- if mulbool v.topnot sign
- then DaemonPropaNot.init d thterm node
- else Egraph.merge d own node in
- let rec find_watch dir pos bound =
- assert (dir = 1 || dir = -1);
- if pos = bound
- then
- let node,sign = IArray.get v.lits pos in
- (merge_bcp node sign; raise Exit)
- else
- let node,sign = IArray.get v.lits pos in
- match is d node with
- | None -> node,pos
- | Some b when mulbool b sign (** true absorbent of or *) ->
- set_dom_up_true d own node b; raise Exit
- | Some _ (** false *) -> find_watch dir (dir+pos) bound
- in
- try
- let w1, w2 = Context.Ref2.get watcher in
- if w1 = -1 (** already done *)
- then false
- else begin
- assert (watched = w1 || watched = w2);
- assert (w1 < w2);
- let dir,bound = if watched = w1 then 1,w2 else -1,w1 in
- let clwatched, watched = find_watch dir watched bound in
- if dir = 1
- then Context.Ref2.set1 watcher watched
- else Context.Ref2.set2 watcher watched;
- Demon.Fast.attach d key
- [Demon.Create.EventValue(clwatched,dom,
- Lit(thterm,watched,watcher))] ;
- true
- end
- with Exit ->
- Context.Ref2.set watcher (-1) (-1);
- false
-
- let wakeup_own d thterm =
- let v = ThE.sem thterm in
- let own = ThE.node thterm in
- begin match is d own with
- | None -> (* only during init *)
- Demon.Fast.attach d key
- [Demon.Create.EventValue(own, dom, All thterm)];
- true
- (** \/ c1 c2 = false ==> c1 = false /\ c2 = false *)
- | Some b when not (mulbool v.topnot b) ->
- let set_dom_down_false (node,sign) = set_bool d node sign in
- IArray.iter ~f:set_dom_down_false v.lits;
- false
- | Some _ -> true
- end
-
- (** return true if things should be propagated *)
- let init d thterm =
- let v = ThE.sem thterm in
- wakeup_own d thterm &&
- let last = IArray.length v.lits - 1 in
- assert (last <> 0);
- let watcher = Context.Ref2.create (Egraph.context d) 0 last in
- wakeup_lit d thterm 0 watcher &&
- wakeup_lit d thterm last watcher
-
- let wakeup d = function
- | Events.Fired.EventValue(_,_,Lit(thterm,watched,next)) ->
- ignore (wakeup_lit d thterm watched next)
- | Events.Fired.EventValue(_ownr,_,All thterm) ->
- (** use this own because the other is the representant *)
- ignore (wakeup_own d thterm)
- | _ -> raise UnwaitedEvent
+ type event = t
+ let print_event fmt r = Ground.pp fmt r.ground
-end
+ let key =
+ Events.Dem.create_key
+ (module struct
+ type d = runable
-module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
-
-module DaemonInit = struct
- let key = Demon.Fast.create "Bool.DaemonInit"
-
- module Data = DUnit
-
- let delay = Events.Delayed_by 1
- let throttle = 100
- let wakeup d = function
- | Events.Fired.EventRegSem(thterm,()) ->
- begin try
- let thterm = ThE.coerce_thterm thterm in
- let v = ThE.sem thterm in
- match T.isnot v with
- | Some node ->
- Egraph.register d node;
- DaemonPropaNot.init d thterm node
- | None ->
- assert (not lazy_propagation);
- IArray.iter ~f:(fun (node,_) -> Egraph.register d node) v.lits;
- if DaemonPropa.init d thterm then ()
- (** we could register a decision here, if we want to do
- decision on any boolean operations not only variable *)
- with Exit -> ()
- end
- | _ -> raise UnwaitedEvent
+ type t = event
-end
+ let name = "Interp.TwoWatchLiteral"
+ end)
-module RDaemonInit = Demon.Fast.Register(DaemonInit)
+ let delay = Events.Delayed_by 1
+ type res_scan =
+ | LimitReached
+ | Absorbent
+ | ToWatch of int
-let _true = node_true
-let _not node =
- index sem {topnot = true; lits = IArray.of_list [node,false]}
-
-
-let filter fold_left =
- let m = fold_left (fun acc (e,b) ->
- Node.M.add_change (fun b -> b)
- (fun b1 b2 -> if Equal.bool b1 b2 then b1 else raise Exit) e b acc)
- Node.M.empty in
- Node.M.bindings m
-
-let gen topnot l =
- try
- let l = filter (fun f acc -> List.fold_left f acc l) in
- match l with
- | [] -> if topnot then node_true else node_false
- | [node,b] when mulbool topnot b -> _not node
- | [node,_] -> node
- | l ->
- index sem {topnot; lits = IArray.of_list l}
- with Exit -> if topnot then node_false else node_true
-
-let _or_and b l =
- try
- let l = filter (fun f acc ->
- List.fold_left (fun acc e -> f acc (e,b)) acc l) in
- match l with
- | [] -> if b then node_true else node_false
- | [a,b'] -> assert (Equal.bool b b'); a
- | l ->
- index sem {topnot = b; lits = IArray.of_list l}
- with Exit -> if b then node_false else node_true
-
-let _or = _or_and false
-let _and = _or_and true
-
-let mk_clause m =
- if Node.M.is_empty m then node_false
- else let len = Node.M.cardinal m in
- if len = 1 then
- let node,b = Node.M.choose m in
- if b then _not node else node
- else
- index sem {topnot=false;
- lits = IArray.of_iter len
- (fun iter -> Node.M.iter (fun node b -> iter (node,b)) m)}
+ let rec check_if_set d args absorbent incr stop i =
+ match Egraph.Ro.get_value d (IArray.get args i) with
+ | None -> ToWatch i
+ | Some b when Value.equal b absorbent ->
+ Absorbent
+ | Some _ -> (* neutral *)
+ let i = incr + i in
+ if i = stop then LimitReached else
+ check_if_set d args absorbent incr stop i
-let _false = node_false
+ let rec check_if_equal_or_set d args absorbent incr stop i n =
+ match check_if_set d args absorbent incr stop i with
+ | LimitReached | Absorbent as r -> r
+ | ToWatch i as r ->
+ if not (Egraph.Ro.is_equal d n (IArray.get args i)) then r
+ else
+ let i = incr + i in
+ if i = stop then LimitReached else
+ check_if_equal_or_set d args absorbent incr stop i n
-let set_true env node = set_bool env node true
-let set_false env node = set_bool env node false
+ let attach d r i =
+ Egraph.Ro.attach_value d
+ (IArray.get (Ground.sem r.ground).args i) BoolValue.key key r;
+ Egraph.Ro.attach_node d (IArray.get (Ground.sem r.ground).args i) key r
-(** {2 Choice on bool} *)
+ let run d r = r d; None
-module ChoBool = struct
- let make_decision env node b =
- Debug.dprintf3 Egraph.print_decision "[Bool] decide %b on %a" b Node.pp node;
- set_bool env node b
+ let enqueue d r =
+ let o_from_start = Context.Ref.get r.from_start in
+ let o_from_end = Context.Ref.get r.from_end in
+ let args = (Ground.sem r.ground).args in
+ if o_from_start = o_from_end then Events.Wait.EnqStopped
+ else
+ let n_end = IArray.get args o_from_end in
+ match check_if_equal_or_set d args r.absorbent (+1) o_from_end o_from_start
+ n_end with
+ | LimitReached ->
+ Context.Ref.set r.from_start o_from_end;
+ Events.Wait.EnqLast(fun d -> Egraph.merge d n_end (Ground.node r.ground))
+ | Absorbent ->
+ Events.Wait.EnqLast(fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+ | ToWatch from_start ->
+ if from_start <> o_from_start then (
+ Context.Ref.set r.from_start from_start;
+ attach d r from_start;
+ );
+ let n_start = IArray.get args from_start in
+ match check_if_equal_or_set d args r.absorbent (-1) from_start o_from_end n_start with
+ | LimitReached ->
+ Context.Ref.set r.from_end from_start;
+ Events.Wait.EnqLast (fun d -> Egraph.merge d n_start (Ground.node r.ground))
+ | Absorbent ->
+ Events.Wait.EnqLast (fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+ | ToWatch from_end when from_end = o_from_end ->
+ Events.Wait.EnqAlready
+ | ToWatch from_end ->
+ Context.Ref.set r.from_end from_end;
+ attach d r from_end;
+ Events.Wait.EnqAlready
+
+ let enqueue d event =
+ match event with
+ | Events.Fired.EventValue (_, _, r)
+ | Events.Fired.EventChange (_, r) ->
+ enqueue d r
+ | _ -> raise Impossible
+
+ let create d absorbent ground =
+ let args = (Ground.sem ground).args in
+ assert (IArray.not_empty args);
+ if IArray.length args = 1 then
+ Egraph.merge d (IArray.get args 0) (Ground.node ground)
+ else
+ let r from_start from_end =
+ assert (from_start < from_end);
+ Debug.dprintf4 debug "Bool create %a (%i-%i)" Ground.pp ground
+ from_start from_end;
+ {
+ ground; absorbent;
+ from_start = Context.Ref.create (Egraph.context d) from_start;
+ from_end = Context.Ref.create (Egraph.context d) from_end;
+ }
+ in
+ match check_if_set (d :> Egraph.Ro.t) args absorbent 1 (IArray.length args - 1) 0 with
+ | LimitReached ->
+ Egraph.merge d (IArray.get args (IArray.length args - 1)) (Ground.node ground)
+ | Absorbent ->
+ Egraph.set_value d (Ground.node ground) absorbent
+ | ToWatch from_start ->
+ let n_start = IArray.get args from_start in
+ match
+ check_if_equal_or_set (d :> Egraph.Ro.t) args absorbent (-1) from_start (IArray.length args - 1) n_start
+ with
+ | LimitReached ->
+ Egraph.merge d n_start (Ground.node ground)
+ | Absorbent ->
+ Egraph.set_value d (Ground.node ground) absorbent
+ | ToWatch from_end ->
+ let r = r from_start from_end in
+ attach (d :> Egraph.Ro.t) r from_start;
+ attach (d :> Egraph.Ro.t) r from_end
+ end
- let choose_decision node env =
- match is env node with
- | Some _ ->
- Debug.dprintf2 Egraph.print_decision "[Bool] No decision for %a" Node.pp node;
- Egraph.DecNo
- | None -> DecTodo
- (List.map (fun v env -> make_decision env node v)
- (Shuffle.shufflel [true;false]))
+ let () = Egraph.Wait.register_dem (module Daemon)
+ let create = Daemon.create
end
-let chobool n = {
- Egraph.prio = 1;
- choice = ChoBool.choose_decision n;
-}
+let init_got_value_bool,wait_for_this_node_get_a_value =
+ Demon.Fast.register_get_value_daemon
+ ~name:"GotBoolValue.bool"
+ ~pp:Fmt.nop
+ (module BoolValue)
+ (fun d n v f -> f d n v)
let converter d (f:Ground.t) =
@@ -433,15 +284,30 @@ let converter d (f:Ground.t) =
when Ground.Ty.equal ty Ground.Ty.bool ->
Egraph.register_decision d (chobool res)
| { app = {builtin = Expr.Or}; tyargs = []; args; _ } ->
- reg_args args; reg (_or (IArray.to_list args))
+ reg_args args;
+ TwoWatchLiteral.create d values_true f
| { app = {builtin = Expr.And}; tyargs = []; args; _ } ->
- reg_args args; reg (_and (IArray.to_list args))
+ reg_args args;
+ TwoWatchLiteral.create d values_false f
| { app = {builtin = Expr.Imply}; tyargs = []; args; _ } ->
let a,b = IArray.extract2_exn args in
- reg_args args; reg (gen false [a,true;b,false])
+ reg_args args;
+ let wait d n v =
+ if Node.equal n res then
+ if not v then (set_bool d a true; set_bool d b false);
+ if Node.equal n a then
+ (if v then (if is_true d res then set_bool d b true)
+ else set_bool d res true);
+ if Node.equal n b then
+ if v then set_bool d res true
+ else if is_true d res then set_bool d a false
+ in
+ List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;res]
| { app = {builtin = Expr.Neg}; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
- reg_args args; reg (_not a)
+ reg_args args;
+ wait_for_this_node_get_a_value d a (fun d _ v -> set_bool d res (not v));
+ wait_for_this_node_get_a_value d res (fun d _ v -> set_bool d a (not v))
| { app = {builtin = Expr.True}; tyargs = []; args; _ } ->
assert ( IArray.is_empty args);
reg _true
@@ -486,15 +352,11 @@ let init_check d =
)
let th_register env =
- RDaemonPropaNot.init env;
- RDaemonPropa.init env;
- RDaemonInit.init env;
- Demon.Fast.attach env
- DaemonInit.key [Demon.Create.EventRegSem(sem,())];
Egraph.register env node_true;
Egraph.register env node_false;
Ground.register_converter env converter;
init_check env;
+ init_got_value_bool env;
()
let () = Egraph.add_default_theory th_register
@@ -525,5 +387,3 @@ let default_value = true
-
-type t = T.t
diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli
index e605b717a..c170d909a 100644
--- a/src_colibri2/theories/bool/boolean.mli
+++ b/src_colibri2/theories/bool/boolean.mli
@@ -18,8 +18,6 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-type t
-val sem: t ThTermKind.t
val dom: bool ValueKind.t
val _true : Node.t
@@ -27,10 +25,6 @@ val _false : Node.t
val _and : Node.t list -> Node.t
val _or : Node.t list -> Node.t
val _not : Node.t -> Node.t
-val gen : bool -> (Node.t * bool) list -> Node.t
-(** [gen d b0 [cl1,b1;cl2,c2]] is
- not_b0 (or (not_b1 cl1,not_b2 cl2)) with not_x f = if x then not f else f
-*)
val set_true : Egraph.t -> Node.t -> unit
val set_false : Egraph.t -> Node.t -> unit
--
GitLab