expose a way for theories to bump literal activity (heuristics)

src/core/internal.ml

@@ -256,10 +256,9 @@ module Make
   let clause_bump_activity (c:clause) : unit =
     c.activity <- c.activity +. env.clause_incr;
     if c.activity > 1e20 then begin
-      for i = 0 to (Vec.size env.clauses_learnt) - 1 do
+      Vec.iter
-        (Vec.get env.clauses_learnt i).activity <-
+        (fun c -> c.activity <- c.activity *. 1e-20)
-          (Vec.get env.clauses_learnt i).activity *. 1e-20;
+        env.clauses_learnt;
-      done;
       env.clause_incr <- env.clause_incr *. 1e-20
     end
 
@@ -895,12 +894,19 @@ module Make
     Iheap.grow_to_by_double env.order (St.nb_elt ());
     enqueue_bool a lvl (Semantic lvl)
 
+  let slice_bump_lit f n =
+    let a = atom f in
+    for _ = 1 to n do
+      var_bump_activity a.var
+    done
+
   let current_slice (): (_,_,_) Plugin_intf.slice = {
     Plugin_intf.start = env.th_head;
     length = (Vec.size env.elt_queue) - env.th_head;
     get = slice_get;
     push = slice_push;
     propagate = slice_propagate;
+    bump_lit=slice_bump_lit;
   }
 
   (* full slice, for [if_sat] final check *)
@@ -910,6 +916,7 @@ module Make
     get = slice_get;
     push = slice_push;
     propagate = (fun _ -> assert false);
+    bump_lit = (fun _ -> assert false);
   }
 
   (* some boolean literals were decided/propagated within Msat. Now we

src/core/plugin_intf.ml

@@ -40,10 +40,12 @@ type ('term, 'formula, 'proof) slice = {
   get : int -> ('term, 'formula) assumption;
   push : 'formula list -> 'proof -> unit;
   propagate : 'formula -> int -> unit;
+  bump_lit: 'formula -> int -> unit;
 }
 (** The type for a slice of litterals to assume/propagate in the theory.
     [get] operations should only be used for integers [ start <= i < start + length].
-    [push clause proof] allows to add a tautological clause to the sat solver. *)
+    [push clause proof] allows to add a tautological clause to the sat solver.
+    [bump_lit] is useful to heuristically favor this literal for decisions *)
 
 module type S = sig
   (** Signature for theories to be given to the Model Constructing Solver. *)

src/core/theory_intf.ml

@@ -25,10 +25,12 @@ type ('form, 'proof) slice = {
   length : int;
   get : int -> 'form;
   push : 'form list -> 'proof -> unit;
+  bump_lit: 'form -> int -> unit;
 }
 (** The type for a slice of literals to assume/propagate in the theory.
     [get] operations should only be used for integers [ start <= i < start + length].
-    [push clause proof] allows to add a tautological clause to the sat solver. *)
+    [push clause proof] allows to add a tautological clause to the sat solver.
+    [bump_lit] is useful to heuristically favor this literal for decisions *)
 
 module type S = sig
   (** Signature for theories to be given to the Solver. *)

src/solver/solver.ml

@@ -49,6 +49,7 @@ module Plugin(E : Formula_intf.S)
       length = s.Plugin_intf.length;
       get = assume_get s;
       push = s.Plugin_intf.push;
+      bump_lit = s.Plugin_intf.bump_lit;
     }
 
   let assume s = Th.assume (mk_slice s)