Fix 1023 by Halbaroth · Pull Request #1291 · OCamlPro/alt-ergo

Halbaroth · 2025-02-11T13:30:01Z

This PR addresses the issue #1023 about inconsistent SAT environments after optimization.

The basic idea is simple. Before optimizing the model in Satml_frontend, we push an additional assertion level.
The first-order model, the boolean model and the objectives are saved before asserting any new formula during the
optimization. The latest consistent models are restored after popping the assertion level.

This PR also includes a refactoring of the optimization implementation in Satml_frontend which improves the readability.

Halbaroth · 2025-02-11T15:19:40Z

It seems that it does not solve #1023 ...
The script:

open AltErgoLib

module Container = (val Sat_solver.get_current ())
module SAT = Container.Make (Theory.Main_Default)

let mk_gf ff =
  Expr.{
    ff;
    origin_name = "";
    gdist = 1;
    hdist = 1;
    trigger_depth = max_int;
    nb_reductions = 0;
    age = 0;
    lem = None;
    mf = false;
    gf = false;
    from_terms = [];
    theory_elim = true
  }

let () =
  let x = Expr.mk_term (Symbols.name ~ns:User "x") [] Ty.Tint in
  let gf = mk_gf Expr.Ints.(x <= ~$10) in
  let env = SAT.empty () in
  SAT.declare env (Hstring.make "x", [], Ty.Tint);
  SAT.assume env gf Explanation.empty;
  let _ : unit =
    try
      let _ : Explanation.t = SAT.unsat env (mk_gf Expr.faux) in
      ()
    with _ -> ()
  in
  SAT.assume env gf Explanation.empty

still raises Unsat at the last command :/

Halbaroth · 2025-02-11T17:33:46Z

I made some progress. The previous script failed because I used Expr.faux instead of Expr.vrai ... now the following script works as expected:

open AltErgoLib

module SAT = Satml_frontend.Make (Theory.Main_Default)

let mk_gf ff =
  Expr.{
    ff;
    origin_name = "";
    gdist = 1;
    hdist = 1;
    trigger_depth = max_int;
    nb_reductions = 0;
    age = 0;
    lem = None;
    mf = false;
    gf = false;
    from_terms = [];
    theory_elim = true
  }

let check_sat =
  let vrai =
    Expr.{ff = vrai;
       origin_name = "vrai";
       hdist = -1;
       gdist = 0;
       trigger_depth = max_int;
       nb_reductions = 0;
       age = 0;
       lem= None;
       mf= false;
       gf=true;
       from_terms = [];
       theory_elim = true;
    }
  in fun env ->
  match SAT.unsat env vrai with
  | _ex -> Fmt.pr "unsat@."
  | exception SAT.I_dont_know ->
      let mdl = Option.get (SAT.get_model env) in
      Fmt.pr "unknown:@ %a@." Models.pp mdl
  | exception SAT.Sat -> Fmt.pr "sat@."

let () =
  Options.set_interpretation ILast;
  Options.set_debug_optimize true;
  let x = Expr.mk_term (Symbols.name ~ns:User "x") [] Ty.Tint in
  let gf = mk_gf Expr.Ints.(x <= ~$10) in
  let env = SAT.empty () in
  SAT.declare env (Hstring.make "x", [], Ty.Tint);
  SAT.assume env gf Explanation.empty;
  SAT.optimize env (Objective.Function.mk ~is_max:true x);
  check_sat env;
  assert (not @@ SAT.is_unsat env);
  SAT.assume env gf Explanation.empty;
  check_sat env

I temporary added a function is_unsat in the SAT solver API in order to check that the underlying SatML solver of Satml_frontend is not unsat after optimization.

Strangely, this script also works on next... but SAT.is_unsat env is true! So it seems that there is another bug on next, and this PR could mask it...

Halbaroth · 2025-02-12T15:06:22Z

#1294 should fix the bug on next. I didn't rebase this PR on #1294 to keep the smaller diff.

bclement-ocp

The approach looks OK overall but I'd like to make sure we are dealing with some corner cases properly.

I think that this made me realize that optimization is currently broken when Options.get_first_interpretation () is set (because we will only ever compute one model in this case), we should probably have an error if those two are used in combination (maybe we already do actually).

We might also want to consider dropping Options.get_first_interpretation () and Options.get_every_interpretation () entirely — they are unlikely to be used since they are not available in SMT-LIB format (I believe) and I think this would allow to return the models in the payload of the Unsat / I_dont_know exceptions and get rid of the last_saved_XXX fields entirely.

bclement-ocp · 2025-02-18T09:26:26Z

src/lib/reasoners/satml_frontend.ml

+  type 'a atom = {
+    lit: 'a;
+    neg: 'a atom;
+  }


Does this really need to be recursive in this way? It seems to me that we don't need to look into neg.neg etc; a simple pair (i.e. type 'a atom = { pos : 'a ; neg : 'a }) would be sufficient.

bclement-ocp · 2025-02-18T09:30:07Z

src/lib/reasoners/satml_frontend.ml

    end

  let update_model_and_return_unknown env compute_model ~unknown_reason =
+    env.last_saved_bmodel <- Some (capture_bmodel env);


Shouldn't this be computed within may_update_last_saved_model? I think the call to SAT.compute_concrete_model within may_update_last_saved_model might change the boolean model, in which case we would have an inconsistency between last_saved_bmodel and last_saved_model.

This also makes me think it would be more future-proof to store the boolean model alongside the theory model as a pair rather than having two independent fields.

You're right. SAT.compute_concrete_model can modify the boolean model too, so I should write:

let update_model_and_return_unknown env compute_model ~unknown_reason = may_update_last_saved_model env compute_model; env.last_saved_bmodel <- Some (capture_bmodel env); Options.Time.unset_timeout (); i_dont_know env unknown_reason

I didn't put it in update_model_and_return_unknown because this function is supposed to update the first order model if Options.get_last_interpretation () is true. If you only use (set-option :produce-assignments true), the compute variable is not true. I can refactor this function to have single place where we update the models.

bclement-ocp · 2025-02-18T09:33:49Z

src/lib/reasoners/satml_frontend.ml

+       - [env.last_saved_model] needs to be forced, as the closure that
+         computes it depends on the current theory environment in [env.satml],
+         which may changed after popping an assertion level.


This should be OK since the theory environment is immutable?

It was my first intuition and the first version of this comment but I misread the function:

let rec compute_concrete_model ~declared_ids env = let acts = theory_slice env in match Th.compute_concrete_model ~acts env.tenv with | () -> ( if is_sat env then Th.extract_concrete_model ~declared_ids env.tenv else try solve env; assert false with Sat -> compute_concrete_model ~declared_ids env ) | exception Ex.Inconsistent (ex, _) -> conflict_analyze_and_fix env (C_theory ex); compute_concrete_model ~declared_ids env

The lazy value is returned by this function, so the right env.tenv value is captured by the closure. I fixed the comment.

src/lib/reasoners/satml_frontend.ml

bclement-ocp · 2025-02-18T09:42:34Z

src/lib/reasoners/satml_frontend.ml

+        | IUnsat (env, _ex) ->
+          (* The explanation [_ex] associated with [env] in [IUnsat] can be
+             discared, as we revert the assertion of formulas that led to this
+             contradiction in [unsat_then_optimize]. *)
+          env, fmdl, omdl, bmdl


In this case the unsat comes from us proving that there is no possible better objective than the one we have currently; this probably should be added to the comment.

(Also the env here is guaranteed to be the same env as we had before — we should probably ignore it, and even better just remove that parameter from IUnsat. It makes sense in FunSAT since the solver is immutable, but in SatML where we update the solver through mutability it just causes confusion)

I added the comment, removed env in IUnsat and removed env in the returned value of optimize_models.

bclement-ocp · 2025-02-18T09:49:45Z

src/lib/reasoners/satml_frontend.ml

+      (* It is more reliable to verify the presence of objectives at
+         the current assertion level by referring to the objective model
+         stored in the current theory environment, rather than checking
+         the emptiness of [env.last_saved_objectives]. *)


I'm not sure it is more reliable — if we find objectives with Th.get_objectives here but there is no last_saved_objectives, we trigger an assertion failure in optimize_models.

What do you think of capturing the model prior to calling optimize_models and passing fmdl/omdl/bmdl as arguments to optimize_models? We would also need to capture the models for the recursive call in optimize_models but I find the mental model easier to follow — we always would capture the models immediately after catching an I_dont_know exception.

The comment is outdated. It was relevant in a previous version of the PR.

Halbaroth · 2025-02-19T14:00:36Z

Ready for a second review. I removed get_first_interpretation and get_every_interpretation in #1299.

bclement-ocp

LGTM but I'm having a hard time following whether we need to force the theory model or not, can you clarify that point?

bclement-ocp · 2025-02-19T14:14:58Z

src/lib/reasoners/satml_frontend.ml

+       - There is no need to force [env.last_saved_model], as this closure
+         has captured the correct theory environment in
+         [SAT.compute_concrete_model].


I'm confused — you previously explained that we did need to force env.last_saved_model because the environment was captured within. Was that incorrect?

(This lazy function for computing the model is really a pain though, it's hard to be sure we are doing things correctly…)

I have been confused too because of this mix of pure/imperative/lazy features. I believe that we do not need to force the model before the optimization phase. When we update the field env.last_saved_model, we call these functions in Satml:

let rec compute_concrete_model ~declared_ids env = let acts = theory_slice env in match Th.compute_concrete_model ~acts env.tenv with | () -> ( if is_sat env then Th.extract_concrete_model ~declared_ids env.tenv else try solve env; assert false with Sat -> compute_concrete_model ~declared_ids env ) | exception Ex.Inconsistent (ex, _) -> conflict_analyze_and_fix env (C_theory ex); compute_concrete_model ~declared_ids env let compute_concrete_model ~declared_ids env = assert (is_sat env); (* Make sure all objectives are optimized before starting model generation. This can cause us to backtrack some of the splits done at the theory level, which is fine, because we don't care about these at the SAT level. *) let rec loop env = let acts = theory_slice env in Th.do_optimize ~acts env.tenv; if not (is_sat env) then try solve env; assert false with Sat -> loop env else compute_concrete_model ~declared_ids env in loop env

The lazy value is returned by Th.extract_concrete_model, which means that env.tenv is captured when we change env.last_saved_model. It is important because this field is altered by Satml.pop. Now the code of extract_concrete_model:

let extract_concrete_model ~declared_ids env = let { gamma_finite; assumed_set; objectives; _ }, _ = do_case_split_aux env ~for_model:true in lazy ( CC_X.extract_concrete_model ~prop_model:assumed_set ~declared_ids gamma_finite ), objectives

I believe that gamma_finite is immutable.

The safer solution consists in forcing the model as I did before the first review. We can also remove the lazy value.

Yeah, I'm not entirely sure why we need a lazy value at all since we only compute the model when model generation is enabled. Not only gamma_finite but the whole theory environment should be immutable, so even if we capture the whole of env.tenv (as long as we don't capture env) it should be fine. OK, as long as CC_X.extract_concrete_model cannot raise, I think that I'm convinced it is OK not to force.

That said, there is something fishy going on here — I think that do_case_split_aux can raise Inconsistent but we don't catch it in Satml.compute_concrete_model; I'm not sure what will happen here.

do_case_split_aux is not in the lazy value. If Option.get_last_interpretation is true, we only call compute_concrete_model here:

do_case_split env Util.AfterMatching; let updated = if not updated && strat != Auto then instantiation env Auto dec_lvl else updated in let dec_lvl' = SAT.decision_level env.satml in let () = if strat == Auto && dec_lvl' = dec_lvl then (* increase chances of forcing Normal each time Auto instantiation doesn't allow to backjump *) env.last_forced_normal <- env.last_forced_normal - 1 in if not updated then update_model_and_return_unknown env (Options.get_last_interpretation ()) ~unknown_reason:Incomplete; (* may becomes ModelGen *) unsat_rec env

The updated value is computed in pre_assume. If pending.updated is false in cdcl_assume then seen_f is empty, so we do not change env.satml. It means that if updated is false in unsat_rec, env.satml did not changed since the last call to do_case_split and this call did not raise an exception.

I believe that it very unlikely to raise Inconsistent in do_case_split_aux in this situation.

The best patch is to remove the lazy value. I can do it in a separated PR.

I am talking about this snippet of code, which is unrelated to the use of lazy:

let rec compute_concrete_model ~declared_ids env = let acts = theory_slice env in match Th.compute_concrete_model ~acts env.tenv with | () -> ( if is_sat env then Th.extract_concrete_model ~declared_ids env.tenv else try solve env; assert false with Sat -> compute_concrete_model ~declared_ids env ) | exception Ex.Inconsistent (ex, _) -> conflict_analyze_and_fix env (C_theory ex); compute_concrete_model ~declared_ids env

We catch Ex.Inconsistent if it comes from Th.compute_concrete_model but not from Th.extract_concrete_model. I am pretty sure that for bit-vectors at least, and probably also for FPA functions, we can raise Inconsistent from extract_concrete_model — or rather from do_case_split_aux.

I was talking about this snippet too. My explanation is not relevant because do_case_split behaves differently during the model generation phase. If we merge #1300 and Ex.Inconsistent raises in Th.extract_concrete_model, it should be caught in unsat_rec.

unsat Fix a bug found while working on PR OCamlPro#1291. More precisely, the following script: ```ocaml Options.set_interpretation ILast; Options.set_debug_optimize true; let x = Expr.mk_term (Symbols.name ~ns:User "x") [] Ty.Tint in let gf = mk_gf Expr.Ints.(x <= ~$10) in let env = SAT.empty () in SAT.declare env (Hstring.make "x", [], Ty.Tint); SAT.assume env gf Explanation.empty; SAT.optimize env (Objective.Function.mk ~is_max:true x); check_sat env; SAT.assume env gf Explanation.empty; (* Should raise Unsat *) check_sat env ``` did not raise unsat at the last `SAT.assume`.

…1301) Fix a bug found while working on PR #1291. More precisely, the following script: ```ocaml Options.set_interpretation ILast; Options.set_debug_optimize true; let x = Expr.mk_term (Symbols.name ~ns:User "x") [] Ty.Tint in let gf = mk_gf Expr.Ints.(x <= ~$10) in let env = SAT.empty () in SAT.declare env (Hstring.make "x", [], Ty.Tint); SAT.assume env gf Explanation.empty; SAT.optimize env (Objective.Function.mk ~is_max:true x); check_sat env; SAT.assume env gf Explanation.empty; (* Should raise Unsat *) check_sat env ``` did not raise unsat at the last `SAT.assume` but it should do it before merging #1291.

Halbaroth · 2025-02-20T11:03:35Z

I closed #1300 and put the commit at the end of this PR.
During the last dev meeting, you suggested to remove env.last_saved_model and compute models only when the user invokes
SAT.get_model. It produce a lot of regressions, which is not a surprise because Satml.compute_concrete_model does some work even if Options.get_produce_models is not true.

Halbaroth · 2025-02-20T13:03:58Z

Good news, I got +1-0 on ae-format and the solver is not slower. I think that we should merge this PR and I will refactor the way we generate models in Satml_frontend in a new PR.

Halbaroth added bug optimization This issue is related to optimization in models. labels Feb 11, 2025

Halbaroth force-pushed the fix-1023 branch from 074530f to 5fb13ae Compare February 11, 2025 13:33

Halbaroth marked this pull request as draft February 11, 2025 15:19

Halbaroth force-pushed the fix-1023 branch from 5fb13ae to 5cde86b Compare February 11, 2025 17:28

Halbaroth mentioned this pull request Feb 12, 2025

Obvious inconsistency ignored after optimization in CDCL-Tableaux #1293

Closed

Halbaroth marked this pull request as ready for review February 12, 2025 15:06

Halbaroth force-pushed the fix-1023 branch 2 times, most recently from 7331200 to b8b9e4f Compare February 18, 2025 09:10

Halbaroth requested a review from bclement-ocp February 18, 2025 09:10

bclement-ocp reviewed Feb 18, 2025

View reviewed changes

Halbaroth requested a review from bclement-ocp February 19, 2025 14:00

bclement-ocp reviewed Feb 19, 2025

View reviewed changes

Halbaroth force-pushed the fix-1023 branch from 36f16fa to b25bfab Compare February 20, 2025 10:02

Fix issue 1023

f83c60e

Halbaroth mentioned this pull request Feb 20, 2025

Remove the lazy value in extract_concrete_model #1300

Closed

Halbaroth force-pushed the fix-1023 branch from b25bfab to 457e43f Compare February 20, 2025 10:58

Remove lazy models

457e43f

Halbaroth requested a review from bclement-ocp February 25, 2025 09:46

Conversation

Halbaroth commented Feb 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Halbaroth commented Feb 11, 2025

Uh oh!

Halbaroth commented Feb 11, 2025

Uh oh!

Halbaroth commented Feb 12, 2025

Uh oh!

bclement-ocp left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Halbaroth Feb 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Halbaroth commented Feb 19, 2025

Uh oh!

bclement-ocp left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Halbaroth commented Feb 20, 2025

Uh oh!

Halbaroth commented Feb 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Halbaroth commented Feb 11, 2025 •

edited

Loading

Halbaroth Feb 18, 2025 •

edited

Loading