Document Th_util.lit_origin

src/lib/reasoners/th_util.mli

@@ -38,8 +38,42 @@ type theory =
   | Th_arrays
   | Th_UF
 
+(** Indicates where asserted literals come from.
+
+    Note that literals are deduplicated before being propagated to the
+    relations. {!Subst} literals are preserved, but other kinds of literals may
+    be subsumed. *)
 type lit_origin =
   | Subst
+  (** Only equalities can be {!Subst} literals, and they are oriented: the
+      left-hand side is always an uninterpreted term or AC symbol application.
+      Effectively, {!Subst} literals are the substitutions generated by calls
+      to [X.solve] and propagated through the CC(X) and AC(X) algorithms.
+
+      In practice, a {!Subst} equality [r = rr] is generated when the
+      corresponding substitution is performed by CC(X), i.e. when [rr] becomes
+      the class representative for [r]. *)
   | CS of theory * Numbers.Q.t
+  (** Literals of {!CS} origin come from the case splits performed by a
+      specific theory. Usually, they are equalities of the shape [x = v] where
+      [x] is an uninterpreted term and [v] a value; however, this is not
+      necessarily the case (e.g. {!CS} literals from the theory of arrays are
+      often disequalities).
+
+      Depending on the theory, the shape of {!CS} literals can be restricted.
+      In particular, {!CS} literals of the {!Th_UF} theory: those come from
+      model generation in the union-find, and are assignments, i.e.  equalities
+      [x = v] where [x] is uninterpreted and [v] is a value.
+
+      The rational argument estimates the size of the split -- usually, the
+      number of possible values the theory could choose for this specific
+      uninterpreted term. *)
   | NCS of theory * Numbers.Q.t
+  (** Literals of {!NCS} origin are created from a literal of {!CS} origin when
+      the choice made in a case split turns out to be unsatisfiable. The
+      literal is a negation of a {!CS} literal that was built by the
+      corresponding theory, with the restrictions that this implies. *)
   | Other
+  (** Literals of {!Other} are those that are not covered by any of the cases
+      described above. In particular, user assertions, SAT decisions, SAT
+      propagations and theory propagations all have the {!Other} origin. *)