From d30797c1c1e120e16ceeab6c95f41aa0f17230ce Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 26 Jul 2016 20:19:13 +0200
Subject: [PATCH] expose a way for theories to bump literal activity
 (heuristics)

---
 src/core/internal.ml    | 15 +++++++++++----
 src/core/plugin_intf.ml |  4 +++-
 src/core/theory_intf.ml |  4 +++-
 src/solver/solver.ml    |  1 +
 4 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 75d0ef3f..fbfde443 100644
--- a/src/core/internal.ml
+++ b/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.get env.clauses_learnt i).activity <-
-          (Vec.get env.clauses_learnt i).activity *. 1e-20;
-      done;
+      Vec.iter
+        (fun c -> c.activity <- c.activity *. 1e-20)
+        env.clauses_learnt;
       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
diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml
index afe5c526..e83dab36 100644
--- a/src/core/plugin_intf.ml
+++ b/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. *)
diff --git a/src/core/theory_intf.ml b/src/core/theory_intf.ml
index 2cdd121f..02f29b8a 100644
--- a/src/core/theory_intf.ml
+++ b/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. *)
diff --git a/src/solver/solver.ml b/src/solver/solver.ml
index 274d3962..2f1356d3 100644
--- a/src/solver/solver.ml
+++ b/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)