Partial documentation of SatML

src/lib/reasoners/satml.ml

@@ -78,8 +78,15 @@ exception Stopped
 
 type conflict_origin =
   | C_none
+  (* No conflict. *)
+
   | C_bool of Atom.clause
+  (* Conflict found during the bool constraint propagation with
+     its conflict clause. *)
+
   | C_theory of Ex.t
+  (* Conflict found during the theory constraint propagation.
+     The explanation is returned by the theory reasoner. *)
 
 (* not even the final one *)
 let vraie_form = E.vrai
@@ -182,32 +189,76 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       (* un vecteur des variables du probleme *)
       mutable vars : Atom.var Vec.t;
 
-      (* la pile de decisions avec les faits impliques *)
       mutable trail : Atom.atom Vec.t;
+      (** Stack of the assigned atoms. An atom [a] is assigned if [a.is_true]
+          is [true].
+
+          An assigned atom [a] is decided or propagated:
+          - [a] is decided if we choose it but there is no constraint which
+              forces it to be [true].
+          - [a] is propaged if we discover that [a] as to be [true] because
+              of boolean/theory constraints.
+
+          Both have a decision level stored in [a.var.level]. The decision level
+          of an atom [a] is set as follows:
+          - if [a] is the only atom of a learnt clause, its decision level
+              is [0];
+
+          - if [a] is propagated during the BCP, its decision level is:
+              * The current decision level if [Options.get_minimal_bj ()] is
+                [false].
+              * Otherwise, its decision level is the maximal decision level of
+                the atoms of the unit clause that constraints [a] to be [true];
+
+          - if [a] is an atom of maximal decision level among the atoms of
+              a conflict clause [C] discovered during BCP and all the other
+              atoms of [C] have a lower decision level than [a], we revert
+              the assignation of [a] and [a.neg] is propagated with the
+              decision level given by the second maximal decision level in the
+              clause [C];
+
+          - if [a] is the first atom of a new learnt clause [C]
+              (of size at least 2), we immediatly propagate this atom with the
+              decision level equals to:
+              * The current decision level if [Options.get_minimal_bj ()] is
+                [false].
+              * Otherwise, its decision level is the maximal decision level of
+                the atoms of [C].
+
+          Note: in this trail, atoms aren't ordered in increasing decision
+          level but decided atoms are in order. *)
 
-      (* une pile qui pointe vers les niveaux de decision dans trail *)
       mutable trail_lim : int Vec.t;
+      (* Stack of decision's indexes in trail. *)
 
       (* Tete de la File des faits unitaires a propager.
          C'est un index vers le trail *)
       mutable qhead : int;
 
-      (* Nombre des assignements top-level depuis la derniere
-         execution de 'simplify()' *)
       mutable simpDB_assigns : int;
+      (** Size of the trail at decision level 0 since the last call of
+          [simplify]. *)
 
       (* Nombre restant de propagations a faire avant la prochaine
          execution de 'simplify()' *)
       mutable simpDB_props : int;
 
-      (* Un tas ordone en fonction de l'activite des variables *)
       mutable order : Vheap.t;
+      (* Priority queue used to choose the next variable to decide in
+         [search]. The priorities of variables are given by a heuristic
+         based on the activities of clauses using these variables.
+
+         Notice that the underlying variables of guards aren't present in
+         this queue. Instead these variables are decided first. *)
 
       (* estimation de progressions, mis a jour par 'search()' *)
       mutable progress_estimate : float;
 
-      (* *)
       remove_satisfied : bool;
+      (** If this flag is set to [true], assumed clauses at decision level
+          [0] are removed. *
+
+          Currently, this flag is always [true]. *)
 
       (* inverse du facteur d'acitivte des variables, vaut 1/0.999 par defaut *)
       var_decay : float;
@@ -237,27 +288,31 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
       mutable starts : int;
 
-      mutable decisions : int;
-
-      mutable propagations : int;
-
       mutable conflicts : int;
+      (** Number of conflicts found. This field is unread. *)
 
       mutable clauses_literals : int;
+      (** Sum of the size of all the assumed clauses.
+          The size of a clause is given by its number of literals. *)
 
       mutable learnts_literals : int;
+      (** Sum of the size of all the learnt clauses.
+          The size of a clause is given by its number of literals. *)
 
       mutable max_literals : int;
 
       mutable tot_literals : int;
 
       mutable nb_init_clauses : int;
+      (** Number of assumed clauses. *)
 
       mutable tenv : Th.t;
 
       mutable unit_tenv : Th.t;
 
+      (* TODO: rename to tenv_stack. *)
       mutable tenv_queue : Th.t Vec.t;
+      (** Stack of the environments of Theory. *)
 
       mutable tatoms_queue : Atom.atom Queue.t;
       (** Queue of atoms that have been added to the [trail] through either
@@ -384,8 +439,12 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
           solver. *)
 
       mutable increm_guards : Atom.atom Vec.t;
+      (** Stack of incremental guards. *)
 
       mutable next_dec_guard : int;
+      (** Index in the trail of the next unassigned guard.
+          This index is used to ensure that we decide all the guards before
+          choosing other variables in [search]. *)
     }
 
   exception Conflict of Atom.clause
@@ -444,10 +503,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
       starts = 0;
 
-      decisions = 0;
-
-      propagations = 0;
-
       conflicts = 0;
 
       clauses_literals = 0;
@@ -522,15 +577,14 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       env.clause_inc <- env.clause_inc *. 1e-20
     end
 
-  let decision_level env = Vec.size env.trail_lim
+  let[@inline always] decision_level env = Vec.size env.trail_lim
 
-  let nb_assigns env = Vec.size env.trail
-  let nb_clauses env = Vec.size env.clauses
+  let[@inline always] nb_assigns env = Vec.size env.trail
+  let[@inline always] nb_clauses env = Vec.size env.clauses
   (* unused -- let nb_learnts env = Vec.size env.learnts *)
-  let nb_vars    env = Vec.size env.vars
+  let[@inline always] nb_vars    env = Vec.size env.vars
 
   let new_decision_level env =
-    env.decisions <- env.decisions + 1;
     Vec.push env.trail_lim (Vec.size env.trail);
     if Options.get_profiling() then
       Profiling.decision (decision_level env) "<none>";
@@ -659,6 +713,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     assert (Options.get_minimal_bj () || (!repush == []));
     List.iter (enqueue_assigned env) !repush
 
+  (* Select the next unassigned variable with the highest priority.
+
+     @raise Sat if there is no more unassigned atom. *)
   let rec pick_branch_var env =
     if Vheap.size env.order = 0 then raise Sat;
     let v = Vheap.remove_min env.order in
@@ -671,6 +728,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
   let pick_branch_lit env =
     if env.next_dec_guard < Vec.size env.increm_guards then
       begin
+        (* Guards are always choosen first. *)
         let a = Vec.get env.increm_guards env.next_dec_guard in
         (assert (not (a.neg.is_guard || a.neg.is_true)));
         env.next_dec_guard <- env.next_dec_guard + 1;
@@ -698,16 +756,21 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         max_lvl := max !max_lvl a.var.level) c.atoms;
     !max_lvl
 
+  (* Push in the trail the atom [a] with decision level [lvl] and reason
+     [reason].
+
+     Requires: the atoms [a] and [a.neg] are unassigned.
+     Ensures: the atom [a] is assigned to [true]. *)
   let enqueue env (a : Atom.atom) lvl reason =
     assert (not a.is_true && not a.neg.is_true &&
             a.var.level < 0 && a.var.reason == None && lvl >= 0);
     if a.neg.is_guard then begin
-      (* if the negation of a is (still) a guard, it should be forced to true
+      (* If the negation of [a] is (still) a guard, it should be forced to true
          during the first decisions.
-         If the SAT tries to deduce that a.neg is true (ie. a is false),
+         If the SAT tries to deduce that [a.neg] is true (ie. [a] is false),
          then we have detected an inconsistency. *)
       assert (a.var.level <= env.next_dec_guard);
-      (* guards are necessarily decided/propagated before all other atoms *)
+      (* Guards are necessarily decided/propagated before all other atoms. *)
       raise (Unsat None);
     end;
     (* Garder la reason car elle est utile pour les unsat-core *)
@@ -795,6 +858,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         end
       with Exit -> ()
 
+  (* Propagate the boolean constraints implied by assuming [a].
+     If a contradiction is discovered, its reason is stored in [res]. *)
   let propagate_atom env (a : Atom.atom) res =
     let watched = a.watched in
     let new_sz_w = ref 0 in
@@ -1058,6 +1123,16 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
           if Options.get_profiling() then Profiling.theory_conflict();
           C_theory dep
 
+  (* Perform all the boolean constraint propagations implied by assuming
+     atoms in the queue stored at the top of [env.trail] (the head of
+     this queue is given by [env.qhead]).
+
+     If we found a contradiction, the BCP stops and a conflict clause is
+     returned.
+
+     The theory constraint propagation isn't perfom here. Instead, these
+     atoms are stored in the queue [env.tatoms_queue], which is processed
+     in [theory_propagate]. *)
   let propagate env =
     let num_props = ref 0 in
     let res = ref C_none in
@@ -1071,7 +1146,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       propagate_atom env a res;
       Queue.push a env.tatoms_queue;
     done;
-    env.propagations <- env.propagations + !num_props;
     env.simpDB_props <- env.simpDB_props - !num_props;
     !res
 
@@ -1122,6 +1196,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
   Vec.shrink env.learnts (lim2 - !j) true
 *)
 
+  (* Helper function that removes all the clauses of [vec] that
+     are sastified at the decision level [0] in the environment [env]. *)
   let remove_satisfied env vec =
     let j = ref 0 in
     let k = Vec.size vec - 1 in
@@ -1280,6 +1356,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     | C_bool c -> C_bool c
     | C_theory _ -> assert false
     | C_none ->
+      (* We don't find contradiction during the BCP, thus we
+         can perform the TCP. *)
       if Options.get_tableaux_cdcl () then
         C_none
       else
@@ -1392,6 +1470,16 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     in
     bj_level, learnt, !history
 
+  (* Search in [confl] an atom of maximal decision level [lvl] such that there
+     is no other atom in [confl] whose the decision level is [lvl].
+
+     If such an atom [a] exists, the function returns the tuple
+     [(a, blvl, snd_max)] where:
+     - [blvl] is a backjump level (equal to [lvl - 1] here);
+     - [snd_max] is the second maximal decision level in [confl].
+
+     @requires all the atom of [confl] are assigned to [false]
+               (it's a conflict clause!). *)
   let fixable_with_simple_backjump (confl : Atom.clause) max_lvl lv =
     if not (Options.get_minimal_bj ()) then None
     else
@@ -1469,6 +1557,13 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         cancel_until env blevel;
         record_learnt_clause env ~is_T_learn:false blevel learnt history
       | Some (a, blevel, propag_lvl) ->
+        (* We found an atom [a] in the conflict clause [c] whose the
+           decision level is bigger than all the other atoms of this clause.
+
+           In this case, we backjump just before the decision of [a.neg]
+           (given by the backjump level [blevel]) and we propagate the atom [a]
+           with the decision level given by the second maximum decision level
+           of [c]. *)
         assert (a.neg.is_true);
         cancel_until env blevel;
         assert (not a.neg.is_true);
@@ -1491,10 +1586,17 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 *)
 
 
+  (* Strategies to choose the next decision. *)
   type strat =
     | Auto
+    (* In this mode, we use the activity-based heuristic to choose
+       the next decision. *)
+
     | Stop
+    (* We stop the search process. *)
+
     | Interactive of Atom.atom
+    (* We force the decision of this atom. *)
 
   let find_uip_reason q =
     let res = ref SA.empty in
@@ -1556,6 +1658,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         end
         else raise e
 
+  (* Produce a clause of the form [fuip \/ ~a1 \/ ... \/ ~an] where
+     the [ai] are all the literals assigned by the SAT solver and involved
+     in the explanation [d]. *)
   let clause_of_dep d fuip =
     let cpt = ref 0 in
     let l =
@@ -1570,6 +1675,18 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     in
     fuip :: l, !cpt + 1
 
+  (* Check if the underlying literal [l] of the atom [a] or its negation
+     isn't inconsistent in the current theory environment [tenv].
+
+     if it's the case, the function returns a new clause (with its size)
+     of the form:
+       l \/ ~a1 \/ ... \/ ~an
+     where [ai] are all the literals assigned by the SAT solver and involved in
+     the explanation of the contradiction produced by the theory reasoner.
+
+     In other words, the formula [a1 /\ ... /\ an ==> l] is first-order
+     tautological (it's [true] in any first-order model of the current problem
+     but the underlying proposition formula isn't necessary a tautology). *)
   let th_entailed tenv a =
     if Options.get_no_tcp () || not (Options.get_minimal_bj ()) then None
     else
@@ -1607,6 +1724,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
          Vec.size env.learnts - nb_assigns env >= n_of_learnts then
         reduce_db();
 
+      (* We get an appropriate candidate for the next decision. *)
       let next =
         match !strat with
         | Auto -> pick_branch_lit env
@@ -1615,18 +1733,28 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
           strat := Stop; f
       in
 
+      (* We first check if the [next] literal has to be [true] according to
+         the theory in the current trail. *)
       match th_entailed env.tenv next with
       | None ->
         new_decision_level env;
         let current_level = decision_level env in
         env.cpt_current_propagations <- 0;
+        (* The variable [next.var] aren't already decided or propagated
+           as [pick_branch_lit] guarantees. *)
         assert (next.var.level < 0);
         if Options.get_debug_sat () then
           Printer.print_dbg "[satml] decide: %a" Atom.pr_atom next;
         enqueue env next current_level None
       | Some(c, _) ->
+        (* We discover a first-order tautology [c => next]. In this case,
+           we learn the clause [c] thanks to the theory reasoner.
+
+           We don't need to decide [next] as it's entailed by the theories.
+
+           The right decision level will be set inside
+           [record_learnt_clause]. *)
         record_learnt_clause env ~is_T_learn:true (decision_level env) c []
-        (* right decision level will be set inside record_learnt_clause *)
     done
 
   (* unused --