fix(BV): Fix unsoundness in BV model generation (#968)

The BV model generation was using an incorrect understanding of the
[is_cs] flag that lead to unsoundness because it assumed that it was
fine to set this flag to [false] when the value is forced *in the
current context* whereas it is only valid to do so when the value is
forced *in all contexts*.

This PR fixes that, and adds copious amounts of documentation to explain
the [is_cs] flag so that we don't make the same mistake again.

Unfortunately the fix leads to a test that no longer passes, but for
good reason as the reasoning used for it was unsound. Hopefully this
should be fixed in a follow-up to
#944

I have also added a new test that is actually satisfiable but would
previously return [unsat]. It times out for now, but is solved properly
in #944

src/lib/reasoners/bitv.ml

@@ -1473,8 +1473,8 @@ module Shostak(X : ALIEN) = struct
 
      Currently a fairly naive backtracking search. *)
   let rec search buf pos sz abstracts =
-    (* [t] are the values we must be distinct from that starts with a '1' *)
-    (* [f] are the values we must be distinct from that starts with a '0' *)
+    (* [t] : values (a) we must be distinct from and (b) start with a '1' *)
+    (* [f] : values (a) we must be distinct from and (b) start with a '0' *)
     let t, nt, f, nf = List.fold_left (fun (t, nt, f, nf) ab ->
         let b, bv = pop_bit ab in
         match b with
@@ -1520,25 +1520,11 @@ module Shostak(X : ALIEN) = struct
       let buf = Bytes.create sz in
       match search buf 0 sz distincts with
       | () ->
-        (* If there are exactly [2^n - 1] constant values we must be distinct
-           from, this is not a case split: the choice is forced. *)
-        let nb =
-          List.fold_left (fun nb a ->
-              if is_cte_abstract a then nb + 1 else nb) 1 distincts
-        in
-        let is_cs = not (Z.equal (Z.of_int nb) (Z.pow (Z.of_int 2) sz)) in
         let bv = Bytes.unsafe_to_string buf in
-        Some (E.bitv bv (Ty.Tbitv sz), is_cs)
+        Some (E.bitv bv (Ty.Tbitv sz), true)
       | exception Not_found ->
-        (* This is not solvable: we are forced to be distinct from all possible
-           values. We signal that by returning an arbitrary bitvector and
-           setting the "case-split" flag to [false], which means that the
-           choice was "forced".
-
-           Since a forced choice is actually inconsistent, this will cause
-           backtracking (and possibly unsat-ness). *)
         let bv = String.make sz '0' in
-        Some (E.bitv bv (Ty.Tbitv sz), false)
+        Some (E.bitv bv (Ty.Tbitv sz), true)
 
   let choose_adequate_model t r l =
     if Options.get_debug_interpretation () then

src/lib/reasoners/sig.mli

@@ -87,12 +87,46 @@ module type SHOSTAK = sig
 
   val abstract_selectors : t -> (r * r) list -> r * (r * r) list
 
-  (* the returned bool is true when the returned term in a constant of the
-     theory. Otherwise, the term contains aliens that should be assigned
-     (eg. records). In this case, it's a unit fact, not a decision
-  *)
   val assign_value :
     r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
+  (**[assign_value r distincts eq] selects the value to assign to [r] in the
+     model as a term [t], and returns [Some (t, is_cs)]. [is_cs] is described
+     below.
+
+     If no appropriate value can be chosen here, return [None] (only do this if
+     either [r] is already a value, or there is a mechanism somewhere else in
+     the code, such as the [case_split] function of a relation module, that
+     ensures completeness of the generated model).
+
+     [r] is the current class representative that a value should be chosen for.
+     No assumptions should be made on the shape of [r], but do return [None] if
+     it is already a value.
+
+     [distincts] is a list of term representatives that the returned value must
+     be distinct from (choosing a value that is present in [distincts] will
+     cause the solver to loop infinitely).
+
+     [eq] is a list of pairs [(t, r)] of terms and their initial representative
+     (i.e., [r] is [fst (X.make t)] for each pair) that encode the equivalence
+     class of [r].
+
+     The returned bool serves a similar purpose as the [is_cs] flag in
+     [Th_util.case_split].
+
+     It should usually be [true], which indicates that the returned term is not
+     forced.
+
+     Use [false] only when the returned term contains aliens that should be
+     assigned (e.g. records).
+
+     **When returning [false], you must ensure that the equality between the
+     first argument and the return value always hold (i.e. is a *unit* fact).
+     In particular, the equality *must not* depend on [distincts] -- doing so
+     would be unsound.**
+
+     In other words, if [assign_value r distincts eq] returns
+     [Some (t, false)], then there must be no context in which
+     [solve r (fst X.make t)] raises [Unsolvable]. You have been warned! *)
 
   (* choose the value to print and how to print it for the given term.
      The second term is its representative. The list is its equivalence class

src/lib/reasoners/sig_rel.mli

@@ -60,7 +60,17 @@ module type RELATION = sig
 
   val case_split :
     t -> Uf.t -> for_model:bool -> Th_util.case_split list
-  (** case_split env returns a list of equalities *)
+  (** case_split env returns a list of equalities
+
+      The returned case splits *must* have a [CS] origin; see the doc of
+      [Th_util.case_split].
+
+      The [for_model] flag is [true] when we are splitting for the purpose of
+      generating a model; the case split may need to be more aggressive in this
+      case to ensure completeness.
+
+      Note: not always equalities (e.g. the arrays theory returns
+      disequalities) *)
 
   val optimizing_split :
     t -> Uf.t -> Th_util.optimized_split -> Th_util.optimized_split option

src/lib/reasoners/th_util.mli

@@ -96,6 +96,24 @@ type lit_origin =
       propagations and theory propagations all have the {!Other} origin. *)
 
 type case_split = Shostak.Combine.r Xliteral.view * bool * lit_origin
+(** A case split is a triple [(a, is_cs, origin)].
+
+    The literal [a] is simply the literal that is the source of the split, or
+    its negation (depending on [origin]).
+
+    The [origin] should be either [CS] or [NCS]. Case splits returned by
+    relations have an origin of [CS], which is then flipped to [NCS] if a
+    contradiction is found involving [a].
+
+    The [is_cs] flag should *always* be [true], unless the literal [a] is a
+    *unit fact*, i.e. a fact that is true in all possible environments, not
+    merely the current one. Note that it is acceptable for unit facts to be
+    returned with [is_cs = true]; but if the [is_cs] flag is [false], the
+    solver *will* assume that the literal can't take part in any conflict.
+    Returning [is_cs = false] if the literal is not an unit fact **is
+    unsound**.
+
+    TL;DR: When in doubt, just set [is_cs] to [true]. *)
 
 type optimized_split = {
   r : Shostak.Combine.r;