Add more comments to CoAlgReasoner.ml

src/lib/CoAlgReasoner.ml

@@ -144,7 +144,7 @@ let lhtMustFind : lht -> M.lit -> localFormula = mustWork2 lhtFind
   *)
 
 
-let rec propagateUnsat = function
+let rec propagateUnsat : propagateElement list -> unit = function
   | [] -> ()
   | propElem::tl ->
       let tl1 =
@@ -482,6 +482,26 @@ let getNextState (core:core) : (sort*bset) option =
   else
     let sort = coreGetSort core in
     let newbs = bsetMake () in
+    (* mkExclClause does two things:
+        a. get all formulas which have to be satisfiable in order to prove core
+           being satisfiable
+        b. collect the literals corresponding to the formulas in a. and ensure
+           that a different set of literals is returned on the next call of
+           getNextState.
+           This part b. is done as follows: Assume the list of literals is l_1
+           to l_n. Then we want to prevent minisat from giving us l_1..l_n
+           again by adding a clause
+
+                ¬ (l_1 ∧ ... ∧ l_n)
+
+          So equivalently the clause (¬ l_1 v ... v ¬ l_n) is added to the
+          solver.
+
+          This also has the effect of putting as much knowledge as possible
+          into the solver: getNextState is only called another time, if we are
+          not able to prove (l_1 ∧ ... ∧ l_n), so we know that at least one of
+          the l_i does not hold.
+    *)
     let rec mkExclClause f acc =
       match lfGetType sort f with
       | OrF -> (* OrF f1 f2 := f *)
@@ -503,14 +523,16 @@ let getNextState (core:core) : (sort*bset) option =
           assert (M.literal_status solver lf2 = M.LTRUE);
           mkExclClause f2 acc1
       | _ ->
-          bsetAdd newbs f;
-          (M.neg_lit (fhtMustFind fht f))::acc
+          bsetAdd newbs f; (* for a. *)
+          (M.neg_lit (fhtMustFind fht f))::acc (* for b. *)
     in
+    (* actually compute a. and b. for the formula set bs *)
     let clause = bsetFold mkExclClause bs [] in
-    let okay = M.add_clause solver clause in
+    let okay = M.add_clause solver clause in (* for b. *)
     assert (okay);
     Some (sort, newbs)
 
+(* enforce creating a raw state node. Just a helper for insertState *)
 let newState sort bs =
   let (func, sl) = !sortTable.(sort) in
   let producer = CoAlgLogics.getExpandingFunctionProducer func in
@@ -533,8 +555,10 @@ let insertState parent sort bs =
   stateAddParent child parent
 
 let expandCore core =
+  (* this encodes the disjunctive behaviour of core nodes: *)
   match getNextState core with
   | Some (sort, bs) ->
+      (* proving bs would make the node core satisfiable *)
       insertState core sort bs;
       queueInsertCore core
   | None ->