Add many comments in CoAlgReasoner.ml

src/lib/CoAlgReasoner.ml

@@ -119,15 +119,30 @@ let isConstraintUnsat cset =
   | Some UnsatC -> true
   | _ -> false
 
-let fhtMustFind fht f =
+(* look up the formula f in the hash-table fht, while knowing that it
+   must be found *)
+let mustWork (f: 'a -> 'b option): 'a -> 'b =
+    fun x -> match (f x) with
+             | Some l -> l
+             | None -> assert false
+
+let mustWork2 (f: 'a -> 'b -> 'c option): 'a -> 'b -> 'c =
+    fun x -> mustWork (f x)
+
+let fhtMustFind : fht -> localFormula -> M.lit =
+    mustWork2 fhtFind
+    (* fun fht f ->
   match fhtFind fht f with
   | Some l -> l
   | None -> assert false
+  *)
 
-let lhtMustFind lht l =
-  match lhtFind lht l with
+let lhtMustFind : lht -> M.lit -> localFormula = mustWork2 lhtFind
+  (*match lhtFind lht l with
   | Some f -> f
   | None -> assert false
+  *)
+
 
 let rec propagateUnsat = function
   | [] -> ()
@@ -390,7 +405,8 @@ let propagateNominals () =
 (*                           Node Expansions                                 *)
 (*****************************************************************************)
 
-let getLit sort fht solver f =
+(* get the literal representing the formula f, possibly expanding the formula hash table fht *)
+let getLit sort (fht: fht) (solver:M.solver) (f: localFormula) : M.lit =
   match fhtFind fht f with
   | Some lit -> lit
   | None ->
@@ -406,11 +422,18 @@ let getLit sort fht solver f =
       in
       lit
 
-let newCore sort bs =
+(* creates a new core of specified sort, representing the set of formulas bs (conjunctively) *)
+let newCore sort (bs: bset) : core =
   let fht = fhtInit () in
   let solver = M.new_solver () in
-  let rec addClauses f =
-    let lf = getLit sort fht solver f in
+  let rec addClauses f : unit =
+    (* "internalize" the formula f, by
+        a. creating a literal for f
+        b. "internalizing" the components of f
+        c. encode the relationship between f and
+           its components
+    *)
+    let lf = getLit sort fht solver f in (* a. *)
     match lfGetType sort f with
     | OrF ->
         let f1 = lfGetDest1 sort f in
@@ -419,6 +442,11 @@ let newCore sort bs =
         addClauses f2;
         let lf1 = fhtMustFind fht f1 in
         let lf2 = fhtMustFind fht f2 in
+        (* c.:
+            if "f = f1 v f2", then it is
+                f -> f1 v f2, i.e.
+                ¬f v f1 v f2
+        *)
         let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
         assert (okay)
     | AndF ->
@@ -428,6 +456,11 @@ let newCore sort bs =
         addClauses f2;
         let lf1 = fhtMustFind fht f1 in
         let lf2 = fhtMustFind fht f2 in
+        (* c.:
+            if "f = f1 ∧ f2" then it is
+                f -> f1 as well as f -> f2, i.e.
+                ¬f v f1 and ¬f v f2.
+        *)
         let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
         assert (okay1);
         let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
@@ -437,7 +470,9 @@ let newCore sort bs =
   bsetIter addClauses bs;
   coreMake sort bs solver fht
 
-let getNextState core =
+(* get another set of formulas whose satisfiability would prove the
+   satisfiability of the core *)
+let getNextState (core:core) : (sort*bset) option =
   let bs = coreGetBs core in
   let fht = coreGetFht core in
   let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
@@ -449,9 +484,9 @@ let getNextState core =
     let newbs = bsetMake () in
     let rec mkExclClause f acc =
       match lfGetType sort f with
-      | OrF ->
+      | OrF -> (* OrF f1 f2 := f *)
           let f1 = lfGetDest1 sort f in
-          let lf1 = fhtMustFind fht f1 in
+          let lf1 = fhtMustFind fht f1 in (* the corresponding literal *)
           if M.literal_status solver lf1 = M.LTRUE then mkExclClause f1 acc
           else
             let f2 = lfGetDest2 sort f in
@@ -482,6 +517,8 @@ let newState sort bs =
   let exp = producer sort bs sl in
   stateMake sort bs exp
 
+(* creates -- if needed -- a new state representing formulas in the bitset bs *)
+(* parent specifies the parent "core" for the new state *)
 let insertState parent sort bs =
   let child =
     match graphFindState sort bs with
@@ -506,6 +543,7 @@ let expandCore core =
       else coreSetStatus core Open
 
 
+(* creates a new core -- if needed -- *)
 let insertCore sort bs =
   match graphFindCore sort bs with
   | None ->