CDCL produces model values for popped symbols

[Halbaroth]

The SAT solver CDCL still produces model values for symbols that have been popped of the context. For instance this input file:

(set-option :produce-models true)
(set-logic ALL)
(declare-const x Int)
(push 1)
(declare-fun f (Int) Int)
(assert (= (f 0) 1))
(pop 1)
; The function `f` isn't declared anymore in the current context and we must
; not produce a model value for it.
(check-sat)
(get-model)

produces a value for f with CDCL but does not it with CDCL-Tableaux.

[Halbaroth]

After a quick investigation, I have an almost correct patch to apply on uf.ml:

diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 4049634c..391c3746 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1122,14 +1122,19 @@ let is_suspicious_symbol = function
   | Symbols.Name { hs; _ } when is_suspicious_name hs -> true
   | _ -> false
 
-let terms env =
+let terms ~declared_ids env =
+  let set =
+    List.fold_left
+      (fun acc (hs, _, _) -> Hstring.Set.add hs acc)
+      Hstring.Set.empty declared_ids
+  in
   ME.fold
     (fun t r ((terms, suspicious) as acc) ->
        let Expr.{ f; _ } = Expr.term_view t in
        match f with
-       | Name { defined = true; _ } ->
-         (* We don't store names defined by the user. *)
-         acc
+       | Name { hs; _ } when
+        not @@ Hstring.Set.mem (Hstring.make @@ Id.show hs) set ->
+        acc
        | _ ->
          let suspicious = is_suspicious_symbol f || suspicious in
          MED.add t r terms, suspicious
@@ -1251,7 +1256,7 @@ let extract_concrete_model cache =
   let compute_concrete_model_of_val = compute_concrete_model_of_val cache in
   let get_abstract_for = Cache.get_abstract_for cache.abstracts
   in fun ~prop_model ~declared_ids env ->
-    let terms, suspicious = terms env in
+    let terms, suspicious = terms ~declared_ids env in
     let model, mrepr =
       MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc)
         terms (ModelMap.empty ~suspicious declared_ids, ME.empty)

But this patch is not correct for two reasons:

1. It fails with quoted identifiers because it relies on string identifiers instead of unique identifiers of Dolmen. This will be fixed after merging Get rid of the legacy frontend finally! #1251.
2. The second issue is more serious. It will hide a bug in CDCL. The symbol f should not be in the union-find after (pop 1), but it still appears in the term (f 0) in the field make of Uf.

[bclement-ocp]

The second issue is more serious. It will hide a bug in CDCL. The symbol f should not be in the union-find after (pop 1), but it still appears in the term (f 0) in the field make of Uf.

Ah yes of course because we will still decide on (= (f 0) 0) after popping… I think there is no actual risk (including soundness) here because we are either protected by types ((f 0) and (f 0) for two different fs are only the same terms if the types of the two fs match), or we will just end up making unnecessary decisions.

I'm not sure there is an easy fix possible for that 2nd issue, we probably just should have a proper scoping mechanism for push/pop, not just the SAT-level guards — I'd say it is fine to have the fix for models adapted for #1251 and live with the extra symbols in the union-find for now (keeping this issue open of course). To be fair, I also think it is fine to leave things as is; realistically, nobody is using the (non-Tableaux) CDCL solver for model generation.

Edit: I accidentally a sentence.

[Halbaroth]

I caught the bug because I ran model tests with both CDCL-Tableaux and CDCL. I didn't intend to test the feature with CDCL but it happened when I modified gentest. As we do not plan to support model generation with CDCL, I suggest this solution:

• Only test models with CDCL-Tableaux (basically I restore gentest and keep the tag model in the tests directory).
• After merging Get rid of the legacy frontend finally! #1251, add the above patch with the Dolmen identifiers and emit a warning if such a term appears in the union-find.
• Add a line in the documentation that explains we support model generations only with CDCL-Tableaux. We can also add a warning if someone try to use it with CDCL.

Ah yes of course because we will still decide on (= (f 0) 0) after popping… I think there is no actual risk (including soundness) here because we are either protected by types ((f 0) and (f 0) for two different fs are only the same terms if the types of the two fs match), or we will just end up making unnecessary decisions.

I am not sure to understand why we still decide on this propositional variable after popping. I thought that the guard mechanism will introduce a fresh variable X and consider the implication X => (= (f 0) 1). After popping, CDCL should have backtrack the decisions on both X and (= (f 0) 1) and decide not X. My intuition is that CDCL sees X => (= (f 0) 1) as the disjunction (not X) or (= (f 0) 1). For me, the main difference between CDCL and CDCL-Tableaux is that CDCL-Tableaux will not decide irrelevant parts of disjunctions. As not X has been decided already, it will not decide (= (f 0) 1) and (f 0) won't appear in the union-find. So I tried to disable this feature in CDCL-Tableaux in order to reproduce the bug with it, but I didn't manage to force it to decide (= (f 0) 1) again. Is it wrong?

[bclement-ocp]

Yes I understand you were not looking for this specifically — all I am saying is that I don't think it is worth expending too much effort fixing it in full, because I don't think a "proper" fix is possible without reworking the push/pop mechanism itself. The patch proposed above should be sufficient for the time being IMO (edit: IOW I think your proposed plan above looks good; I'm not sure the 3rd point is necessary because if we do the 2nd point model generation should work as expected with CDCL).

Your reasoning is correct, except that CDCL-Tableaux has two relevant differences with CDCL here: it does not make irrelevant decisions (so here we would not decide on f(0) = 1), and also it does not propagate irrelevant atoms (which may have been decided or propagated) to the theory module. The first feature is gated behind the --no-tableaux-cdcl-in-instantiation flag, the second one is behind the --no-tableaux-cdcl-in-theories flag, and using both flags disables CDCL-Tableaux entirely.

(If you use --no-tableaux-cdcl-in-instantiation you should be able to observe (with -d sat) that CDCL-Tableaux does decide on f(0) = 1, but that information is then not propagated to the theory module, so it never reaches the Uf module)