From f6f6a51ffed53b30d38d5767770cba11bc8c2c37 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 19 Oct 2023 14:40:04 +0200 Subject: [PATCH] Document `Th_util.lit_origin` As promised in #886. --- src/lib/reasoners/th_util.mli | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli index e57cb7cf2..a55e5ff88 100644 --- a/src/lib/reasoners/th_util.mli +++ b/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. *)