Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CDCL produces model values for popped symbols #1243

Open
Halbaroth opened this issue Sep 30, 2024 · 4 comments
Open

CDCL produces model values for popped symbols #1243

Halbaroth opened this issue Sep 30, 2024 · 4 comments
Labels
bug models This issue is related to model generation.

Comments

@Halbaroth
Copy link
Collaborator

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 Halbaroth added bug models This issue is related to model generation. labels Sep 30, 2024
@Halbaroth Halbaroth changed the title CDCL produces model values CDCL produces model values for popped symbols Sep 30, 2024
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Sep 30, 2024
This PR removes:
- the deprecated legacy frontend (parser and typechecker),
- the deprecated AB-Why3 plugin which depends on the legacy parser,
- the associated opam packages and dependencies (including `shell.nix`
  and our Makefile),
- all the reference in the documentation to these bastards,
- simplify `gentest` and rename the tag `dolmen` into `cdcl` in `tests/`,
- the option `frontend` in `Options`.

I also update the `Lib_usage` example because we now use the Dolmen.

We keep the `--frontend` option but now it is a no op command and we
output an appropriate message if users still use it.

This PR cannot be merged before fixing OCamlPro#1243.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Sep 30, 2024
This PR removes:
- the deprecated legacy frontend (parser and typechecker),
- the deprecated AB-Why3 plugin which depends on the legacy parser,
- the associated opam packages and dependencies (including `shell.nix`
  and our Makefile),
- all the reference in the documentation to these bastards,
- simplify `gentest` and rename the tag `dolmen` into `cdcl` in `tests/`,
- the option `frontend` in `Options`.

I also update the `Lib_usage` example because we now use the Dolmen.

We keep the `--frontend` option but now it is a no op command and we
output an appropriate message if users still use it.

This PR cannot be merged before fixing OCamlPro#1243.
@Halbaroth
Copy link
Collaborator Author

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
Copy link
Collaborator

bclement-ocp commented Oct 8, 2024

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
Copy link
Collaborator Author

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
Copy link
Collaborator

bclement-ocp commented Oct 8, 2024

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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug models This issue is related to model generation.
Projects
None yet
Development

No branches or pull requests

2 participants