Simpler representation of solver types

solver/internal.ml

@@ -43,7 +43,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     mutable var_inc : float;
     (* increment for variables' activity *)
 
-    trail : (semantic var, atom) Either.t Vec.t;
+    trail : (lit, atom) Either.t Vec.t;
     (* decision stack + propagated atoms *)
 
     trail_lim : int Vec.t;
@@ -152,16 +152,22 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
   let get_var_id v = v.vid
   let get_var_level v = v.level
   let get_var_weight v = v.weight
-
   let set_var_weight v w = v.weight <- w
   let set_var_level v l = v.level <- l
 
-  let get_elt_id e = Either.destruct e get_var_id get_var_id
+  (* Accessors for litterals *)
-  let get_elt_weight e = Either.destruct e get_var_weight get_var_weight
+  let get_lit_id v = v.lid
-  let get_elt_level e = Either.destruct e get_var_level get_var_level
+  let get_lit_level (v : lit) = v.level
+  let get_lit_weight (v : lit) = v.weight
+  let set_lit_weight (v : lit) w = v.weight <- w
+  let set_lit_level (v : lit) l = v.level <- l
 
-  let set_elt_weight e = Either.destruct e set_var_weight set_var_weight
+  let get_elt_id e = Either.destruct e get_lit_id get_var_id
-  let set_elt_level e = Either.destruct e set_var_level set_var_level
+  let get_elt_weight e = Either.destruct e get_lit_weight get_var_weight
+  let get_elt_level e = Either.destruct e get_lit_level get_var_level
+
+  let set_elt_weight e = Either.destruct e set_lit_weight set_var_weight
+  let set_elt_level e = Either.destruct e set_lit_level set_var_level
 
   let f_weight i j =
     get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i)
@@ -171,10 +177,10 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
 
   (* Var/clause activity *)
   let insert_var_order e = Either.destruct e
-      (fun v -> Iheap.insert f_weight env.order v.vid)
+      (fun v -> Iheap.insert f_weight env.order v.lid)
       (fun v ->
           Iheap.insert f_weight env.order v.vid;
-          iter_sub (fun t -> Iheap.insert f_weight env.order t.vid) v
+          iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v
       )
 
   let var_decay_activity () =
@@ -194,9 +200,20 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     if Iheap.in_heap env.order v.vid then
       Iheap.decrease f_weight env.order v.vid
 
+  let lit_bump_activity_aux (v : lit) =
+    v.weight <- v.weight +. env.var_inc;
+    if v.weight > 1e100 then begin
+      for i = 0 to (St.nb_vars ()) - 1 do
+        set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100)
+      done;
+      env.var_inc <- env.var_inc *. 1e-100;
+    end;
+    if Iheap.in_heap env.order v.lid then
+      Iheap.decrease f_weight env.order v.lid
+
   let var_bump_activity v =
     var_bump_activity_aux v;
-      iter_sub (fun t -> var_bump_activity_aux t) v
+    iter_sub lit_bump_activity_aux v
 
   let clause_bump_activity c =
     c.activity <- c.activity +. env.clause_inc;
@@ -258,7 +275,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       for c = env.qhead to Vec.size env.trail - 1 do
         Either.destruct (Vec.get env.trail c)
         (fun v ->
-            v.tag.assigned <- None;
+            v.assigned <- None;
             v.level <- -1;
             insert_var_order (Either.mk_left v)
         )
@@ -270,7 +287,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
               a.is_true <- false;
               a.neg.is_true <- false;
               a.var.level <- -1;
-              a.var.tag.reason <- Bcp None;
+              a.var.reason <- Bcp None;
               insert_var_order (Either.mk_right a.var)
             end)
       done;
@@ -292,19 +309,19 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     if a.is_true then
       L.debug 10 "Litteral %a already in queue" pp_atom a
     else begin
-      assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0);
+      assert (a.var.level < 0 && a.var.reason = Bcp None && lvl >= 0);
       a.is_true <- true;
       a.var.level <- lvl;
-      a.var.tag.reason <- reason;
+      a.var.reason <- reason;
       Vec.push env.trail (Either.mk_right a);
       L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom a
     end
 
-  let enqueue_assign (v: semantic var) value lvl =
+  let enqueue_assign v value lvl =
-    v.tag.assigned <- Some value;
+    v.assigned <- Some value;
     v.level <- lvl;
     Vec.push env.trail (Either.mk_left v);
-    L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_semantic_var v
+    L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_lit v
 
   let th_eval a =
     if a.is_true || a.neg.is_true then None
@@ -334,7 +351,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     let c       = ref (Proof.to_list c_clause) in
     let history = ref [c_clause] in
     clause_bump_activity c_clause;
-    let is_semantic a = match a.var.tag.reason with
+    let is_semantic a = match a.var.reason with
         | Semantic _ -> true
         | _ -> false
     in
@@ -355,15 +372,15 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
                 decr tr_ind;
                 L.debug 20 "Looking at trail element %d" !tr_ind;
                 Either.destruct (Vec.get env.trail !tr_ind)
-                (fun v -> L.debug 15 "%a" St.pp_semantic_var v)
+                (fun v -> L.debug 15 "%a" St.pp_lit v)
-                (fun a -> match a.var.tag.reason with
+                (fun a -> match a.var.reason with
                     | Bcp (Some d) ->
                             L.debug 15 "Propagation : %a" St.pp_atom a;
                             L.debug 15 " |- %a" St.pp_clause d;
                             let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in
                             begin match tmp with
                             | [] -> L.debug 15 "No lit to resolve over."
-                            | [b] when b == a.var.tag.pa ->
+                            | [b] when b == a.var.pa ->
                                     clause_bump_activity d;
                                     var_bump_activity a.var;
                                     history := d :: !history;
@@ -419,7 +436,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       decr pathC;
       let p = get_atom !tr_ind in
       decr tr_ind;
-      match !pathC, p.var.tag.reason with
+      match !pathC, p.var.reason with
       | 0, _ ->
         cond := false;
         learnt := p.neg :: (List.rev !learnt)
@@ -429,7 +446,11 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     List.iter (fun q -> q.var.seen <- false) !seen;
     !blevel, !learnt, !history, true
 
-  let analyze c_clause = if St.mcsat then analyze_mcsat c_clause else analyze_sat c_clause
+  let analyze c_clause =
+    if St.mcsat then
+      analyze_mcsat c_clause
+    else
+      analyze_sat c_clause
 
   let record_learnt_clause confl blevel learnt history is_uip =
     begin match learnt with
@@ -627,7 +648,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     a
 
   let slice_get i = Either.destruct (Vec.get env.trail i)
-      (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false)
+      (function {level; term; assigned = Some v} -> Th.Assign (term, v), level | _ -> assert false)
       (fun a -> Th.Lit a.lit, a.var.level)
 
   let slice_push l lemma =
@@ -702,7 +723,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     if sz1 > 2 && (sz2 = 2 || c < 0) then -1
     else 1
 
-(* returns true if the clause is used as a reason for a propagation,
+  (* returns true if the clause is used as a reason for a propagation,
         and therefore can be needed in case of conflict. In this case
         the clause can't be forgotten *)
   let locked c = false (*
@@ -771,26 +792,26 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
          if v.level >= 0 then
            pick_branch_lit ()
          else begin
-            let value = Th.assign v.tag.term in
+           let value = Th.assign v.term in
            env.decisions <- env.decisions + 1;
            new_decision_level();
            let current_level = decision_level () in
-            L.debug 5 "Deciding on %a" St.pp_semantic_var v;
+           L.debug 5 "Deciding on %a" St.pp_lit v;
            enqueue_assign v value current_level
          end)
       (fun v ->
          if v.level >= 0 then begin
-          assert (v.tag.pa.is_true || v.tag.na.is_true);
+           assert (v.pa.is_true || v.na.is_true);
            pick_branch_lit ()
-      end else match Th.eval v.tag.pa.lit with
+         end else match Th.eval v.pa.lit with
            | Th.Unknown ->
              env.decisions <- env.decisions + 1;
              new_decision_level();
              let current_level = decision_level () in
-          L.debug 5 "Deciding on %a" St.pp_atom v.tag.pa;
+             L.debug 5 "Deciding on %a" St.pp_atom v.pa;
-          enqueue_bool v.tag.pa current_level (Bcp None)
+             enqueue_bool v.pa current_level (Bcp None)
            | Th.Valued (b, lvl) ->
-          let a = if b then v.tag.pa else v.tag.na in
+             let a = if b then v.pa else v.na in
              enqueue_bool a lvl (Semantic lvl))
 
   let search n_of_conflicts n_of_learnts =
@@ -872,8 +893,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     Vec.grow_to_by_double env.learnts nbc;
     env.nb_init_clauses <- nbc;
     St.iter_vars (fun e -> Either.destruct e
-        (fun v -> L.debug 50 " -- %a" St.pp_semantic_var v)
+                     (fun v -> L.debug 50 " -- %a" St.pp_lit v)
-        (fun a -> L.debug 50 " -- %a" St.pp_atom a.tag.pa)
+                     (fun a -> L.debug 50 " -- %a" St.pp_atom a.pa)
                  );
     add_clauses ?tag cnf
 
@@ -883,8 +904,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
 
   let eval lit =
     let var, negated = make_boolean_var lit in
-    assert (var.tag.pa.is_true || var.tag.na.is_true);
+    assert (var.pa.is_true || var.na.is_true);
-    let truth = var.tag.pa.is_true in
+    let truth = var.pa.is_true in
     if negated then not truth else truth
 
   let hyps () = env.clauses
@@ -896,7 +917,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
   let model () =
     let opt = function Some a -> a | None -> assert false in
     Vec.fold (fun acc e -> Either.destruct e
-      (fun (v: semantic var) -> (v.tag.term, opt v.tag.assigned)  :: acc)
+                 (fun v -> (v.term, opt v.assigned)  :: acc)
                  (fun _ -> acc)
              ) [] env.trail
 

solver/res.ml

@@ -64,7 +64,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
         if equal_atoms a b then
           aux resolved (a :: acc) r
         else if equal_atoms St.(a.neg) b then
-          aux (St.(a.var.tag.pa) :: resolved) acc r
+          aux (St.(a.var.pa) :: resolved) acc r
         else
           aux resolved (a :: acc) (b :: r)
     in
@@ -133,7 +133,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
         diff_learnt (b :: acc) l r'
     | _ -> raise (Resolution_error "Impossible to derive correct clause")
 
-  let clause_unit a = match St.(a.var.level, a.var.tag.reason) with
+  let clause_unit a = match St.(a.var.level, a.var.reason) with
     | 0, St.Bcp Some c -> c, to_list c
     | _ ->
       raise (Resolution_error "Could not find a reason needed to resolve")
@@ -189,7 +189,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     | [] -> true
     | a :: r ->
       L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
-      let d = match St.(a.var.level, a.var.tag.reason) with
+      let d = match St.(a.var.level, a.var.reason) with
         | 0, St.Bcp Some d -> d
         | _ -> raise Exit
       in
@@ -334,10 +334,10 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
           if f_args <> [] then
               Format.fprintf fmt "<TD>%a</TD></TR>%a%a" St.print_atom (List.hd f_args)
                 (fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_atom a)) (List.tl f_args)
-                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) t_args
+                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_lit v)) t_args
           else if t_args <> [] then
-          Format.fprintf fmt "<TD>%a</TD></TR>%a" St.print_semantic_var (List.hd t_args)
+          Format.fprintf fmt "<TD>%a</TD></TR>%a" St.print_lit (List.hd t_args)
-                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) (List.tl t_args)
+                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_lit v)) (List.tl t_args)
           else
               Format.fprintf fmt "<TD></TD></TR>"
         in

solver/solver_types.ml

@@ -27,40 +27,42 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
   type formula = E.Formula.t
   type proof = Th.proof
 
-  type 'a var =
+  type lit = {
-    { vid : int;
+    lid : int;
-      tag : 'a;
+    term : term;
-      mutable weight : float;
     mutable level : int;
-      mutable seen : bool;
+    mutable weight : float;
+    mutable assigned : term option;
   }
 
-  type semantic =
+  type var = {
-    { term : term;
+    vid : int;
-      mutable assigned : term option; }
-
-  type boolean = {
     pa : atom;
     na : atom;
+    mutable seen : bool;
+    mutable level : int;
+    mutable weight : float;
     mutable reason : reason;
   }
 
-  and atom =
+  and atom = {
-    { var : boolean var;
+    aid : int;
-      lit : formula;
+    var : var;
     neg : atom;
-      mutable watched : clause Vec.t;
+    lit : formula;
     mutable is_true : bool;
-      aid : int }
+    mutable watched : clause Vec.t;
+  }
 
-  and clause =
+  and clause = {
-    { name : string;
+    name : string;
     tag : int option;
-      atoms : atom Vec.t ;
+    atoms : atom Vec.t;
+    learnt : bool;
+    cpremise : premise;
     mutable activity : float;
     mutable removed : bool;
-      learnt : bool;
+  }
-      cpremise : premise }
 
   and reason =
     | Semantic of int
@@ -70,20 +72,19 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     | History of clause list
     | Lemma of proof
 
-  type elt = (semantic var, boolean var) Either.t
+  type elt = (lit, var) Either.t
 
   (* Dummy values *)
   let dummy_lit = E.dummy
 
   let rec dummy_var =
     { vid = -101;
-      level = -1;
-      weight = -1.;
-      seen = false;
-      tag = {
       pa = dummy_atom;
       na = dummy_atom;
-        reason = Bcp None; };
+      seen = false;
+      level = -1;
+      weight = -1.;
+      reason = Bcp None;
     }
   and dummy_atom =
     { var = dummy_var;
@@ -124,13 +125,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     try MT.find t_map t
     with Not_found ->
       let res = {
-          vid = !cpt_mk_var;
+        lid = !cpt_mk_var;
+        term = t;
         weight = 1.;
         level = -1;
-          seen = false;
+        assigned = None;
-          tag = {
-            term = t;
-            assigned = None; };
       } in
       incr cpt_mk_var;
       MT.add t_map t res;
@@ -145,13 +144,12 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
         let cpt_fois_2 = !cpt_mk_var lsl 1 in
         let rec var  =
           { vid = !cpt_mk_var;
-            level = -1;
-            weight = 0.;
-            seen = false;
-            tag = {
             pa = pa;
             na = na;
-              reason = Bcp None;};
+            seen = false;
+            level = -1;
+            weight = 0.;
+            reason = Bcp None;
           }
         and pa =
           { var = var;
@@ -177,7 +175,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
 
   let add_atom lit =
     let var, negated = make_boolean_var lit in
-    if negated then var.tag.na else var.tag.pa
+    if negated then var.na else var.pa
 
   let make_clause ?tag name ali sz_ali is_learnt premise =
     let atoms = Vec.from_list ali sz_ali dummy_atom in
@@ -217,7 +215,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
       List.iter f (Mi.find v.vid !iter_map)
     with Not_found ->
       let l = ref [] in
-          Th.iter_assignable (fun t -> l := add_term t :: !l) v.tag.pa.lit;
+      Th.iter_assignable (fun t -> l := add_term t :: !l) v.pa.lit;
       iter_map := Mi.add v.vid !l !iter_map;
       List.iter f !l
 
@@ -227,7 +225,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     name, (List.map add_atom l), (List.map add_term l'), color
 
   (* Pretty printing for atoms and clauses *)
-  let print_semantic_var fmt (v: semantic var) = E.Term.print fmt v.tag.term
+  let print_lit fmt v = E.Term.print fmt v.term
 
   let print_atom fmt a = E.Formula.print fmt a.lit
 
@@ -243,10 +241,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
 
   (* Complete debug printing *)
-  let sign a = if a==a.var.tag.pa then "" else "-"
+  let sign a = if a == a.var.pa then "" else "-"
 
   let level a =
-    match a.var.level, a.var.tag.reason with
+    match a.var.level, a.var.reason with
     | n, _ when n < 0 -> assert false
     | 0, Bcp (Some c) -> sprintf "->0/%s" c.name
     | 0, Bcp None   -> "@0"
@@ -267,9 +265,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     | None -> ()
     | Some t -> bprintf b "[assignment: %s]" (Log.on_fmt E.Term.print t)
 
-  let pp_semantic_var b v =
+  let pp_lit b v =
     bprintf b "%d [lit:%s]%a"
-      (v.vid+1) (Log.on_fmt E.Term.print v.tag.term) pp_assign v.tag.assigned
+      (v.lid+1) (Log.on_fmt E.Term.print v.term) pp_assign v.assigned
 
   let pp_atom b a =
     bprintf b "%s%d%s[lit:%s]"

solver/solver_types_intf.ml

@@ -20,53 +20,55 @@ module type S = sig
   type formula
   type proof
 
-  type 'a var =
+  type lit = {
-    { vid : int;
+    lid : int;
-      tag : 'a;
+    term : term;
-      mutable weight : float;
     mutable level : int;
-      mutable seen : bool; }
+    mutable weight : float;
+    mutable assigned : term option;
+  }
 
-  type semantic =
+  type var = {
-    { term : term;
+    vid : int;
-      mutable assigned : term option; }
-
-  type boolean = {
     pa : atom;
     na : atom;
+    mutable seen : bool;
+    mutable level : int;
+    mutable weight : float;
     mutable reason : reason;
   }
 
   and atom = {
-    var : boolean var;
+    aid : int;
-    lit : formula;
+    var : var;
     neg : atom;
-    mutable watched : clause Vec.t;
+    lit : formula;
     mutable is_true : bool;
-    aid : int
+    mutable watched : clause Vec.t;
   }
 
   and clause = {
     name : string;
     tag : int option;
     atoms : atom Vec.t;
+    learnt : bool;
+    cpremise : premise;
     mutable activity : float;
     mutable removed : bool;
-    learnt : bool;
-    cpremise : premise
   }
 
   and reason =
     | Semantic of int
     | Bcp of clause option
+
   and premise =
     | History of clause list
     | Lemma of proof
 
-  type elt = (semantic var, boolean var) Either.t
+  type elt = (lit, var) Either.t
   (** Recursive types for literals (atoms) and clauses *)
 
-  val dummy_var : boolean var
+  val dummy_var : var
   val dummy_atom : atom
   val dummy_clause : clause
   (** Dummy values for use in vector dummys *)
@@ -78,13 +80,13 @@ module type S = sig
 
   val add_atom : formula -> atom
   (** Returns the atom associated with the given formula *)
-  val add_term : term -> semantic var
+  val add_term : term -> lit
   (** Returns the variable associated with the term *)
-  val make_boolean_var : formula -> boolean var * bool
+  val make_boolean_var : formula -> var * bool
   (** Returns the variable linked with the given formula, and wether the atom associated with the formula
       is [var.pa] or [var.na] *)
 
-  val iter_sub : (semantic var -> unit) -> boolean var -> unit
+  val iter_sub : (lit -> unit) -> var -> unit
   (** Iterates over the semantic var corresponding to subterms of the fiven literal, according
       to Th.iter_assignable *)
 
@@ -99,16 +101,16 @@ module type S = sig
   val fresh_hname : unit -> string
   (** Fresh names for clauses *)
 
-  val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option)
+  val proof_debug : proof -> string * (atom list) * (lit list) * (string option)
   (** Debugging info for proofs (see Plugin_intf). *)
 
+  val print_lit : Format.formatter -> lit -> unit
   val print_atom : Format.formatter -> atom -> unit
-  val print_semantic_var : Format.formatter -> semantic var -> unit
   val print_clause : Format.formatter -> clause -> unit
   (** Pretty printing functions for atoms and clauses *)
 
+  val pp_lit : Buffer.t -> lit -> unit
   val pp_atom : Buffer.t -> atom -> unit
-  val pp_semantic_var : Buffer.t -> semantic var -> unit
   val pp_clause : Buffer.t -> clause -> unit
   (** Debug function for atoms and clauses (very verbose) *)