diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index 780a21f70ba6b0054dcb010c667e44200eccbfbd..afc77d49c535fe795bb9d15ce7f3797c5dc027cf 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -194,9 +194,9 @@ module Events = struct
type delay = Events.delay =
| Immediate
- | Delayed_by of int (** Must be strictly positive *)
+ | Delayed_by of int
| LastEffort of int
- (** Should try to ensure that a model exists, must be strictly positive *)
+ | LastEffortUncontextual of int
| FixingModel
type enqueue = Events.enqueue =
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index 974c065fd8aae1f400d24630e8cab171ce65d2e9..c377ed961540086a860a92bc7faa8363da063cde 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -1111,7 +1111,10 @@ and Events : sig
| Immediate
| Delayed_by of int (** Must be strictly positive *)
| LastEffort of int
- (** Should try to ensure that a model exists, must be strictly positive *)
+ (** After no propagation and decisions remains to be done *)
+ | LastEffortUncontextual of int
+ (** Same as before but could be moved as propagation before the time it is
+ added *)
| FixingModel
type enqueue =
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 2641ad0178b3526dfc033edb3aa440d08cc0a15e..15f84bdcbe7b843e395d97cdeea3a2d7c779f8f7 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -34,7 +34,12 @@ module Print = struct
{ pdem_runable = (fun _ _ _ -> assert false) }
end
-type delay = Immediate | Delayed_by of int | LastEffort of int | FixingModel
+type delay =
+ | Immediate
+ | Delayed_by of int
+ | LastEffort of int
+ | LastEffortUncontextual of int
+ | FixingModel
type enqueue =
| EnqRun : 'r Dem.t * 'r * Nodes.ThTerm.t option -> enqueue
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index 2f744c27eb2d1501bdd8a4083fbe73b6e31059a7..ebf78a13b5f29f566c71da3bc3e82e846938aa70 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -24,7 +24,10 @@ type delay =
| Immediate
| Delayed_by of int (** Must be strictly positive *)
| LastEffort of int
- (** Should try to ensure that a model exists, must be strictly positive *)
+ (** After no propagation and decisions remains to be done *)
+ | LastEffortUncontextual of int
+ (** Same as before but could be moved as propagation before the time it is
+ added *)
| FixingModel
type enqueue =
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 0641b25554ae51edde2b12e3d8586e4a94a5c316..53127a77b53725fe29d14bea9ce574f05f82efcc 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -69,7 +69,7 @@ module PrioMake (S : sig
end) =
struct
module Att = struct
- type t = { id : int; v : S.t }
+ type t = { id : int; v : S.t; added_at : int }
type prio = float
@@ -109,9 +109,11 @@ struct
(function None -> Some coef | Some v -> Some (coef *. v))
t.db x.Att.id
- let insert t v =
+ let get_prio t x = Popop_stdlib.DInt.H.find_def t.db 1. x.Att.id
+
+ let insert t ~added_at v =
Context.Ref.set t.size (Context.Ref.get t.size + 1);
- let x = { Att.v; id = t.next } in
+ let x = { Att.v; id = t.next; added_at } in
t.next <- t.next + 1;
Context.Ref.set t.prio (P.insert t.db x (Context.Ref.get t.prio))
@@ -123,15 +125,15 @@ struct
Some x
| exception Leftistheap.Empty -> None
- let get_min_and_skew t =
- match P.min (Context.Ref.get t.prio) with
- | Some v -> Some (v, Popop_stdlib.DInt.H.find_def t.db 1. v.id)
- | None -> None
-
- let pop t =
- match P.extract_min (Context.Ref.get t.prio) with
- | _, prio -> Context.Ref.set t.prio prio
- | exception Leftistheap.Empty -> ()
+ (* let get_min_and_skew t =
+ * match P.min (Context.Ref.get t.prio) with
+ * | Some v -> Some (v, Popop_stdlib.DInt.H.find_def t.db 1. v.id)
+ * | None -> None
+ *
+ * let pop t =
+ * match P.extract_min (Context.Ref.get t.prio) with
+ * | _, prio -> Context.Ref.set t.prio prio
+ * | exception Leftistheap.Empty -> () *)
let size t = Context.Ref.get t.size
@@ -159,6 +161,7 @@ module PrioLastEffort = PrioMake (struct
| Events.Immediate -> 1
| Events.Delayed_by offset -> offset
| Events.LastEffort offset -> offset
+ | Events.LastEffortUncontextual offset -> offset
| Events.FixingModel -> 1)
end)
@@ -181,7 +184,8 @@ type bp = {
type solve_step =
| Propagate
| FixModel
- | BacktrackChoice of (Egraph.wt -> unit) * (Egraph.wt -> unit) Base.Sequence.t
+ | BacktrackChoice of
+ (Egraph.wt -> unit) * (Egraph.wt -> unit) Base.Sequence.t * solve_step
type t = {
choices : Prio.t;
@@ -198,7 +202,8 @@ type t = {
mutable steps : int;
mutable stepsl : int;
mutable last_todo : (Egraph.wt -> unit) * bp_kind;
- allow_learning : bool;
+ last_effort_learnt : Events.daemon_key Context.Clicket.t;
+ allow_learning : bool; (** Learning *)
mutable learning : bool;
mutable learning_htbl : int ThTerm.H.t;
mutable learning_tbl : int array;
@@ -227,23 +232,25 @@ let get_steps t = t.steps
let new_solver ~learning () =
let context = Context.create () in
+ let creator = Context.creator context in
let daemon_count = ref (-1) in
let dec_count = ref (-1) in
let t =
{
- choices = Prio.create (Context.creator context);
- daemons = Context.TimeWheel.create (Context.creator context);
- lasteffort = PrioLastEffort.create (Context.creator context);
- fixing_model = Context.Ref.create (Context.creator context) [];
+ choices = Prio.create creator;
+ daemons = Context.TimeWheel.create creator;
+ lasteffort = PrioLastEffort.create creator;
+ fixing_model = Context.Ref.create creator [];
prev_scheduler_state = None;
- solver_state = Backtrackable.new_t (Context.creator context);
+ solver_state = Backtrackable.new_t creator;
context;
var_inc = ref 1.;
level = 0;
- solve_step = Context.Ref.create (Context.creator context) Propagate;
+ solve_step = Context.Ref.create creator Propagate;
steps = 0;
stepsl = 0;
last_todo = ((fun _ -> ()), External);
+ last_effort_learnt = Context.Clicket.create creator;
allow_learning = learning;
learning = false;
learning_htbl = ThTerm.H.create 32;
@@ -258,13 +265,15 @@ let new_solver ~learning () =
match get_event_priority att with
| Immediate -> assert false (* absurd *)
| Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
- | LastEffort _ -> PrioLastEffort.insert t.lasteffort att
+ | LastEffort _ -> PrioLastEffort.insert t.lasteffort att ~added_at:(-1)
+ | LastEffortUncontextual _ ->
+ PrioLastEffort.insert t.lasteffort att ~added_at:t.level
| FixingModel ->
Context.Ref.set t.fixing_model (att :: Context.Ref.get t.fixing_model)
and sched_decision dec =
incr dec_count;
(* Debug.dprintf1 debug "[Scheduler] New possible decisions prio:%i" !dec_count; *)
- Prio.insert t.choices dec
+ Prio.insert t.choices dec ~added_at:(-1)
in
Backtrackable.set_sched ~sched_daemon ~sched_decision t.solver_state;
t
@@ -516,7 +525,9 @@ let rec conflict_analysis t =
(fun v ->
Debug.dprintf3 debug_learn "[Learnt|%i] %a is useful"
v.PrioLastEffort.Att.id Events.pp_daemon_key v.PrioLastEffort.Att.v;
- PrioLastEffort.change t.lasteffort v 2.)
+ PrioLastEffort.change t.lasteffort v 2.;
+ if PrioLastEffort.get_prio t.lasteffort v = 16. then
+ Context.Clicket.push t.last_effort_learnt v.v)
t.last_effort_made;
Option.iter
(fun v ->
@@ -540,17 +551,19 @@ let rec conflict_analysis t =
| Some prev -> (
pop_to t prev;
Prio.reprio t.choices;
- let has_learnt = PrioLastEffort.reprio_is_changed t.lasteffort in
+ PrioLastEffort.reprio t.lasteffort;
match prev.kind with
| Choices seq -> (
match Base.Sequence.next seq with
| None -> rewind ()
| Some (choice, choices) ->
- if has_learnt && false then (
- assert (Context.Ref.get t.solve_step = Propagate);
- Context.Ref.set t.solve_step
- (BacktrackChoice (choice, choices)))
- else make_choice t choice choices)
+ Context.Clicket.iter t.last_effort_learnt ~f:(fun v ->
+ Debug.incr stats_lasteffort_propa;
+ let d = Backtrackable.get_delayed t.solver_state in
+ Backtrackable.run_daemon d v);
+ Context.Ref.set t.solve_step
+ (BacktrackChoice
+ (choice, choices, Context.Ref.get t.solve_step)))
| External -> raise Contradiction)
in
rewind ()
@@ -614,47 +627,34 @@ let run_one_step_propagation ~nodec t =
let d = Backtrackable.get_delayed t.solver_state in
Backtrackable.run_daemon d att)
(fun () -> true)
+ | None when nodec -> false
| None -> (
- match PrioLastEffort.get_min_and_skew t.lasteffort with
- | Some (att, skew) when skew > 16. ->
- PrioLastEffort.pop t.lasteffort;
- Debug.dprintf3 debug_learn "[Learnt|%i] %a is directly propagated"
- att.PrioLastEffort.Att.id Events.pp_daemon_key
- att.PrioLastEffort.Att.v;
- Debug.incr stats_lasteffort_propa;
- protect_against_contradiction t
- (fun () ->
- let d = Backtrackable.get_delayed t.solver_state in
- Backtrackable.run_daemon d att.v)
- (fun () -> true)
- | _ when nodec -> false
- | _ -> (
- match Prio.extract_min t.choices with
- | Some chogen as o ->
- t.last_decision_made <- o;
- Debug.dprintf0 debug_queue "[Scheduler] Decision mode";
- try_run_dec t chogen.v;
- true
- | None -> (
- t.last_decision_made <- None;
- Debug.dprintf1 debug_queue "[Scheduler] LastEffort: %i"
- (PrioLastEffort.size t.lasteffort);
- (* if Context.TimeWheel.current_time t.lasteffort < max_last_effort then *)
- match PrioLastEffort.extract_min t.lasteffort with
- | Some att as o ->
- Debug.incr stats_lasteffort;
- t.last_effort_made <- o;
- protect_against_contradiction t
- (fun () ->
- let d = Backtrackable.get_delayed t.solver_state in
- Backtrackable.run_daemon d att.v)
- (fun () -> true)
- | None ->
- t.last_effort_made <- None;
- false
- (* else false *))))
-
-let run_one_step_fix_model t =
+ match Prio.extract_min t.choices with
+ | Some chogen as o ->
+ t.last_decision_made <- o;
+ Debug.dprintf0 debug_queue "[Scheduler] Decision mode";
+ try_run_dec t chogen.v;
+ true
+ | None -> (
+ t.last_decision_made <- None;
+ Debug.dprintf1 debug_queue "[Scheduler] LastEffort: %i"
+ (PrioLastEffort.size t.lasteffort);
+ (* if Context.TimeWheel.current_time t.lasteffort < max_last_effort then *)
+ match PrioLastEffort.extract_min t.lasteffort with
+ | Some att as o ->
+ Debug.incr stats_lasteffort;
+ t.last_effort_made <- o;
+ protect_against_contradiction t
+ (fun () ->
+ let d = Backtrackable.get_delayed t.solver_state in
+ Backtrackable.run_daemon d att.v)
+ (fun () -> true)
+ | None ->
+ t.last_effort_made <- None;
+ false
+ (* else false *)))
+
+let run_one_step_fix_model ~nodec t =
Debug.incr stats_fix_model;
match Context.Ref.get t.fixing_model with
| att :: l ->
@@ -664,6 +664,7 @@ let run_one_step_fix_model t =
let d = Backtrackable.get_delayed t.solver_state in
Backtrackable.run_daemon d att)
(fun () -> true)
+ | [] when nodec -> false
| [] ->
protect_against_contradiction t
(fun () ->
@@ -689,14 +690,20 @@ let run_one_step ~nodec t =
Debug.dprintf0 debug "[Scheduler] FixModel";
Context.Ref.set t.solve_step FixModel;
true)
- | BacktrackChoice (choice, choices) -> (
- match run_one_step_propagation ~nodec:true t with
+ | BacktrackChoice (choice, choices, step) -> (
+ let res =
+ match step with
+ | BacktrackChoice _ -> assert false
+ | Propagate -> run_one_step_propagation ~nodec:true t
+ | FixModel -> run_one_step_fix_model ~nodec:true t
+ in
+ match res with
| true -> true
| false ->
- Context.Ref.set t.solve_step Propagate;
+ Context.Ref.set t.solve_step step;
make_choice t choice choices;
true)
- | FixModel -> run_one_step_fix_model t
+ | FixModel -> run_one_step_fix_model ~nodec t
let rec flush t =
try Backtrackable.flush t.solver_state
diff --git a/src_colibri2/stdlib/context.ml b/src_colibri2/stdlib/context.ml
index 920f2face0b15a0226976d97cc3fd0c8cb28c503..5739853803e6301c201a04c28a56471e0b4c5947 100644
--- a/src_colibri2/stdlib/context.ml
+++ b/src_colibri2/stdlib/context.ml
@@ -556,3 +556,59 @@ module Memo(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key :=
let fold f t =
S.H.fold f t.h
end
+
+module type Clicket = sig
+
+ type 'a t
+
+ val create: creator -> 'a t
+
+ val push: 'a t -> 'a -> unit
+
+ val iter: f:('a -> unit) -> 'a t -> unit
+
+ val todo: 'a t -> bool
+
+ val pp: ?sep:unit Fmt.t -> 'a Fmt.t -> 'a t Fmt.t
+
+end
+
+module Clicket = struct
+ type 'a t = {
+ v : 'a Vector.vector;
+ h : int history;
+ mutable first_not_done : int;
+ }
+
+ let restore t saved = t.first_not_done <- saved
+ let save t () = t.first_not_done
+
+ let refresh t =
+ Expert.refresh
+ ~restore:(restore t)
+ t.h
+
+ let save t =
+ Expert.save
+ ~restore:(restore t)
+ ~save:(save t)
+ t.h
+
+ let clear t =
+ Vector.clear t.v;
+ t.first_not_done <- 0
+
+ let create creator = { v = Vector.create (); h = Expert.create creator; first_not_done = 0 }
+ let iter ~f t = refresh t;
+ for i=t.first_not_done to (Vector.length t.v) - 1 do
+ f (Vector.get t.v i)
+ done;
+ t.first_not_done <- Vector.length t.v;
+ if List.is_empty t.h.context.bps then
+ clear t
+ let todo t = t.first_not_done < Vector.length t.v
+
+ let push t v = save t; Vector.push t.v v
+
+ let pp ?sep pp fmt v = Vector.pp ?pp_sep:sep pp fmt v.v
+end
diff --git a/src_colibri2/stdlib/context.mli b/src_colibri2/stdlib/context.mli
index ffb64fd06e2b1b8d5415ef1654bacffa12e90662..c6337a0a46252a21f72b1d2e7662dc4d4e32bf84 100644
--- a/src_colibri2/stdlib/context.mli
+++ b/src_colibri2/stdlib/context.mli
@@ -253,3 +253,25 @@ module type Memo = sig
end
module Memo (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := S.t
+
+(** Clicket *)
+(** The added element are given back after each pop *)
+
+module type Clicket = sig
+
+ type 'a t
+
+ val create: creator -> 'a t
+
+ val push: 'a t -> 'a -> unit
+
+ val iter: f:('a -> unit) -> 'a t -> unit
+ (** iter on the one that have been added inside sub-branch *)
+
+ val todo: 'a t -> bool
+
+ val pp: ?sep:unit Fmt.t -> 'a Fmt.t -> 'a t Fmt.t
+
+end
+
+module Clicket : Clicket
diff --git a/src_colibri2/tests/solve/models/function.smt2 b/src_colibri2/tests/solve/models/function.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..3ce36e2acae9a0b5cad0fd034525c0c5d386adcf
--- /dev/null
+++ b/src_colibri2/tests/solve/models/function.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+(set-info :status-colibri2 sat)
+
+(declare-fun f (Int) Int)
+
+(assert (< (f 1) (f 2)))
+
+(check-sat)
+;(get-model)
+(get-value ((f 1)))
+(get-value ((f 2)))
+(get-value ((f 3)))
+(get-value ((f 4)))
+;(get-value (f))
diff --git a/src_colibri2/tests/solve/models/function.smt2.oracle b/src_colibri2/tests/solve/models/function.smt2.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ceb501abbbf79de11798f122f59e0730329b88d3
--- /dev/null
+++ b/src_colibri2/tests/solve/models/function.smt2.oracle
@@ -0,0 +1,5 @@
+sat
+((f 1 0))
+((f 2 1))
+((f 3 0))
+((f 4 0))
diff --git a/src_colibri2/theories/FP/interval32.ml b/src_colibri2/theories/FP/interval32.ml
index f0684baed16da75506f0cceff33b08199e8e1c3f..a23adc11371f513e416325fc5e3ea5c81ecb2d13 100644
--- a/src_colibri2/theories/FP/interval32.ml
+++ b/src_colibri2/theories/FP/interval32.ml
@@ -51,4 +51,4 @@ let is_singleton d =
| Some x ->
if Farith2.B32.B32.eq x (Farith2.B32.B32.of_q NE Q.zero) then
None
- else failwith "assert false" (* failSome (float32_to_B32 x) *)
\ No newline at end of file
+ else None (** todo *)
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index bb49bbe7eb03519c45a56e83a74900f3475d4a4c..3f9a5cb7885c32bfad1d195716e44ba46011c729 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -329,21 +329,30 @@ module Delayed_instantiation = struct
let name = "delayed_instantiation"
end)
- let delay = Events.LastEffort 1
+ let delay = Events.LastEffortUncontextual 1
type runable = t * Ground.Subst.t [@@deriving show]
let print_runable = pp_runable
let run d (tri, subst) =
- Debug.dprintf8 debug
- "[Quant] %a delayed instantiation %a, pat %a, checks:%a" Ground.Subst.pp
- subst Ground.ClosedQuantifier.pp tri.form
- Fmt.(list ~sep:comma Pattern.pp)
- tri.pats
- Fmt.(list ~sep:comma Pattern.pp)
- tri.checks;
- instantiate_aux d tri subst
+ let instantiate d =
+ Debug.dprintf8 debug
+ "[Quant] %a delayed instantiation %a, pat %a, checks:%a" Ground.Subst.pp
+ subst Ground.ClosedQuantifier.pp tri.form
+ Fmt.(list ~sep:comma Pattern.pp)
+ tri.pats
+ Fmt.(list ~sep:comma Pattern.pp)
+ tri.checks;
+ instantiate_aux d tri subst
+ in
+ let n = Ground.ClosedQuantifier.node tri.form in
+ match Boolean.is d n with
+ | Some true -> instantiate d
+ | Some false -> ()
+ | None ->
+ Daemon.attach_value d n Boolean.dom (fun d _ v ->
+ if Boolean.BoolValue.equal v Boolean.value_true then instantiate d)
end
let () = Events.register (module Delayed_instantiation)