Clean up OptimAE

[Halbaroth]

This PR refactors the way we manage optimization constraints in
Alt-Ergo.

• Optimization constraints aren't tag on subformulas anymore. Instead
  we use the MaxSMT syntaxes.
• We don't support optimization in Alt-Ergo native format. As this
  feature haven't been published, we don't need to deprecated it.
• We support maximize, minimize and get-objectives. There is no
  support for assert-soft. I think it's out of the scope of this PR.
  Besides, it seems that get-objectives can take arguments in our current implementation of Solving_loop but I didn't find
  any examples using this syntax, thus I silently ignore these arguments.
• The SAT solver API exposes two new functions: optimize and
  get_objectives which, respectively, register objective function and
  return the current objective model.

[Halbaroth]

Uhm, I thought it was a good idea to hide completely the priority order in the objective model but in fact, users could feed AE with a file like this one:

(set-logic ALL)
(set-option :produce-models true)
(declare-const x Int)
(declare-const y Int)
(assert (<= x 10))
(assert (< y 5))
(maximize x)
(maximize y)
(maximize x)
(check-sat)
(get-model)
(get-objectives)

With the current implementation, the second maximize will be completely ignored and output:

unknown
(
  (define-fun x () Int 10)
  (define-fun y () Real 0.0)
)
(objectives 
  (x 10)
  (y (- 5.0 epsilon))
)

Another tricky example is if we use both maximize and minimize on the same expression. The second one is ignored. Should we print a warning?

[bclement-ocp]

Uhm, I thought it was a good idea to hide completely the priority order in the objective model but in fact, users could feed AE with a file like this one:
[..]
Another tricky example is if we use both maximize and minimize on the same expression. The second one is ignored. Should we print a warning?

Yeah, I was going to make a remark on that. We shouldn't print a warning, we should print all the objectives requested by the user in the correct order!

(We might want to also print a warning when we perform optimization under an unbounded/strict objective, which should only occur during model generation if I understand correctly)

Not sure how that's tricky — wouldn't removing the test for an existing function in Objective.Model.add just do The Right Thing™?

[bclement-ocp]

This needs to be wrap_f, not handle_sat_exn to avoid using an invalid satML environment (see #946 and related issues).

[bclement-ocp]

Suggested change

	Printer.print_fmt fmt "@]@,)";
	Printer.print_fmt fmt "@]@,)"

[bclement-ocp]

This does not seem right; we don't return the uf so the added repr is lost.

[Halbaroth]

Uhm, I don't think we need to keep the representative element here. The expression e here isn't a part of our problem but the expression we try to optimize modulo our constraints. Now, I remember why I add this line before

let repr, _ = Uf.find uf e in

The reason is because the function Uf.find fails if the expression have never been added to the union-find before. As the expression can be something completely new, this can happen. Consider for instance the input file:

(set-logic ALL)
(set-option :produce-models true)
(declare-const x Int)
(assert (<= x 10))
(maximize (+ x 5))
(check-sat)
(get-model)
(get-objectives)

The expression (+ x 5) is completely new and the union-find will raise Not_found exception here.

Now if the expression is already knew, we want to get both its representative in the union-find (in the code it's repr) and the semantic values returned by X.make for this expression (in the code it's r1).

Another solution would be add the expression e in the union-find when we call the function optimize of the SAT solver.

[bclement-ocp]

If we want to get the representative if there is one or the result of X.make otherwise then the right code is probably along the lines of:

let repr, r1 =
  match Uf.find uf e with
  | repr, _ -> repr, Uf.make uf e
  | exception Not_found -> let r, _ = X.make e in r, r

That said, I didn't think about it, but you are right — we should add e in the call to optimize (this is what was done before when Optimize was a symbol). Note that this needs to use Theory.add_term to make sure that all sub-terms are properly added (Uf.add only adds the term itself but not the subterms).

The real reason to do this is that if we do (maximize (bv2nat x)) for instance, and the problem does not otherwise contain (bv2nat x), not adding bv2nat to the theory would lose some reasoning power (because it would not be seen by the relations, and knowledge about it would not be properly propagated).

[bclement-ocp]

Suggested change

	for the polynomial [p] in its interval. We used this function in the case
	for the polynomial [p] in its interval. We use this function in the case

[bclement-ocp]

Why is this no longer needed? What happens if an assertion renders an existing objective invalid?

[Halbaroth]

The purpose of update_objectives function was to ensure we add new optimization discovered while exploring a term. At this time, we could have optimization everywhere in formulae. In particular, it means the theory module could ignore an optimization constraint before the underlying formula was involved in a formula of the current trail of the SAT solver. I didn't check, but I guess we could even forget an optimization constraint by backtracking.

If we discover a new constraint, we have to throw away all the case splits. A flag in update_objectives was used to remember that and we call reset_case_split_env if the flag is up.

Now, we feed the SAT solver with all the optimization constraints at once. I thought it was fine but in fact we perform case splits after each assume. Thus we have to reset casesplits after each optimize in Theory.

[Halbaroth]

Actually I did! I just forget to remove the dead code commented. :) Thanks for the remark. I will add a comment in optimize.

[bclement-ocp]

Ah, right, update_objectives is for adding new objectives — I mixed it up in my head with partial_objectives_reset which is used when an objective becomes invalid, thanks for the clarification!

I thought it was fine but in fact we perform case splits after each assume.

Yeah, either after each assume or before matching or after matching depending on the split policy. After each assume is the most aggressive version tho, so I think if we deal with that properly we are good.

I didn't check, but I guess we could even forget an optimization constraint by backtracking.
Now, we feed the SAT solver with all the optimization constraints at once. I thought it was fine but in fact we perform case splits after each assume. Thus we have to reset casesplits after each optimize in Theory.

This remark makes me wonder: previously, we had optimizations in assertions, which are obviously stored in the assertion stack (and so would be normally affected by push and pop), but I am not sure that is still the case in this PR (I didn't see any mechanism that would take care of it, but also was not aware it could be an issue prior to your comment). Might be worth checking -- for instance the following should output 0, not 10.

(set-option :produce-models true)
(set-logic ALL)
(declare-const x Int)
(assert (<= 0 x 10))
(push 1)
(maximize x)
(pop 1)
(minimize x)
(check-sat)
(get-model)

[Halbaroth]

Uhm I thought it was fine because I use the same semantic as the assert but I probably miss something in solving_loop. Thanks for the test.

[bclement-ocp]

Ah dang, I take it that means it does not work then :/ I think it is probably an issue in the Satml_frontend / Satml rather than solving_loop. The way push and pop work in the Satml solver is that we create guards, and assertions within a push/pop assertions are, well, guarded: if the guard is false, the assertion is just ignored.

So for instance the following:

(push 1)
(assert f1)
(check-sat)

is treated as if we had:

(declare-const guard Bool)
(assert (=> guard f1))
(assert guard) ; Generated for all assertions levels that were not popped on (check-sat)
(check-sat)

and the following:

(push 1)
(assert f1)
(pop 1)
(check-sat)

is treated as if we had:

(declare-const guard Bool)
(assert (=> guard f1))
(assert (not guard)) ; Generated on (pop 1)
(check-sat)

and so Th.assume (which is called during propagation) will never be called on f1. But I believe that with the current implementation (from my recollection of it, I did not check in detail) we will always call optimize without taking the guards into account.

In the previous implementation this "just worked" because optimization markers were expressions inside assertions that were not assumed when the guards are false, but now that optimization markers are declarations there is a little bit more work that needs to be duplicated. In fact there is probably a bit of overlap with #901, now that I think about it.

Given that optimization is still experimental (and that you've said you're sick of working on it for so long, which is understandable :) ), I think dropping support for optimization within push/pop in this PR is acceptable. We can then either deal with that as part of #901 (which I think is on track for inclusion in the next release, since postponing #904 freed up quite some time for me) or otherwise in a separate PR; your call.

[Halbaroth]

I think I'll take it after we solve #901. I'll print a warning if we try to optimize with push and pop. An error isn't necessary here as we still got a correct model but we don't respect the optimization constraint.

[Halbaroth]

I open an issue #933 and add a warning when we process files involving both optimization constraints and pop and push.

[bclement-ocp]

Is starting at order 0 here really correct? What if some objectives have been optimized already?

[bclement-ocp]

Hm actually it looks like we are optimizing all objectives again at each case split, that looks wasteful (possibly incorrect, but I don't think so since we use equalities for the splits).

[Halbaroth]

Let's clarify a bit the previous behaviour and the current one.

• Before this PR, the function look_for_sat proceeds choices in this order when for_model = false:
  • First, it propagates new choices in the pending queue.
  • Then it try to optimize as much as it can objectives for which we didn't get a best value yet (in the current SAT branch of course). If it see an objective whose the previous value is a limit (+oo, -oo or a strict bound), it tries to optimize it again.
  • If we fail to optimize a bound, we stop in optimizing_objective.
  • Otherwise, it asks theories to generate new case splits and it goes back to the first point.

Now, if we're generating model (so for_model = true), the previous code ignore objectives whose the value is a limit and we keep optimize next objectives (with a lower priority).

This is not what we want. If we got a limit for some objective o, it doesn't make sense to try to optimize objectives with lower priority than o. But in model generation, we want to keep generating model, even if we can fulfill some objectives.

Let's pick an example:

(set-option :produce-models true)
(set-logic ALL)
(declare-const x Int)
(declare-const y Int)
(maximize x)
(minimize y)
(assert (>= y (- 10)))
(assert (>= x 0))
(check-sat)
(get-model)
(assert (<= x 10))
(check-sat)
(get-model)

If you run AE next on it with the command

dune exec -- alt-ergo test.smt2 --optimize --objctives-in-interpretation --frontend legacy --dump-models

AE outputs:

unknown
Returned unknown reason = Incomplete
(
  (define-fun x () Int +oo)
  (define-fun y () Int (- 10))
)

unknown
Returned unknown reason = Incomplete
(
  (define-fun x () Int 10)
  (define-fun y () Int (- 10))
)

We don't expect that AE keep optimizing objectives after x before the first check-sat, but we keep doing it...

Now, if we don't the same on this PR with the command

dune exec -- alt-ergo test2.smt2 --optimize --objectives-in-interpretation

AE outputs:

unknown
(
  (define-fun x () Int 1)
  (define-fun y () Int 0)
)

; File "test2.smt2", line 12, characters 1-12: I don't know (0.0009) (6 steps) (goal g_2)

unknown
(
  (define-fun x () Int 10)
  (define-fun y () Int (- 10))
)

The new code does the right thing... by chance! It's because during each case split phase, we do again all the optimizations, even if we got an infinity value before and we stop optimization if we got an infinity value in optimizing_objective. If the flag for_model is true, we stop also optimization but we keep generate new casesplits.

I add a new function next_unknown in Objective.Model whose the semantic is closed to the old next_optimization:

  exception Found of Function.t * int

  let next_unknown mdl =
    try
      M.iter (fun { f; order } v ->
        match (v : Value.t) with
        | Value _ -> ()
        | Pinfinity | Minfinity | Limit _ -> raise Exit
        | _ -> raise (Found (f, order))
      ) mdl;
      None
    with
    | Found (f, order) -> Some (f, order)
    | Exit -> None

Notice this function isn't very efficient because we keep visiting Value node in the map again and again. The behaviour of Objective.Model is basically a queue with some printers. I guess I will rewrite it with a functional queue but let's keep map now, early optimization is risky.

[Halbaroth]

Ok, it's still incorrect for this test:

; This test checks if the optimization doesn't stop after trying to
; optimize a strict bound.
(set-option :produce-models true)
(set-logic ALL)
(declare-const x Real)
(declare-const y Real)
; If the SAT solver explores first the right branch of the following OR gate, it
; shouldn't conclude that x cannot be optimized.
(assert (or (<= x 4.0) (< x 1.5)))
(maximize x)
; The current implementation of SatML explores the right branch of OR gates
; first. We add the following line to be sure the optimization feature still
; works after changing the order of branches.
(assert (or (< y 1.5) (<= y 4.0)))
(maximize y)
(check-sat)
(get-model)
(get-objectives)

During the first assert we don't know that y will be bound and we get infinity here. Thus, we have to treat infinity value again after the second assert, otherwise we will print +oo for y. This was explained in a comment of the original OptimAE PR.

[Gbury]

We don't expect that AE keeps optimize value after x after the first check-sat, but we keep doing it...

I disagree: in that case I fully expect alt-ergo to re-optimize the model because of the new get-sat and the new constraints added by assert since the last check-sat !

[Halbaroth]

Ok my example is ambiguous. I was talking of the first check-sat only. I totally agree we have to keep optimize if new constraints are involved.

[bclement-ocp]

I believe this is a behavior change — previously we would keep optimizing further objectives while doing model generation, but now we no longer does (this call to aux goes immediately to generate_choices). Is that intentional?

[bclement-ocp]

Also as far as I can tell, this means that the case splits in the middle of intervals and the such that we create for infinite/limit cases are never used.

[bclement-ocp]

Same remark as above; are standard model generation mechanisms failing somehow?

[Halbaroth]

Before this PR, we use a wrapped case-split as input for this function and we have access to the last computed value for the first-order model through this wrapped case-split.

An alternative implementation would be to give this value as an argument of optimizing_objective.

Notice that my middle_value gives a value in the last interval (for the to_max = true case) of the domain of the polynomial p. You told me other solvers try to give a bigger value when we maximize strict bound.

[bclement-ocp]

Ah, right this is for that! Makes sense. What I was thinking for that case (and what other solvers do I believe) is add an inequality constraint rather than an equality in case that specific value end up not being feasible. For instance, with a nonlinear objective x * x with x in 1 .. 2range, the range forx * xis1 .. 4(AFAIK Alt-Ergo know this) but if we pick2or3as a value there is no model whereas if we just constrain< 3or> 2` it is.

(I think in this specific case we might go into an infinite loop in the current PR if we actually used this split in look_for_sat, not sure)

[Halbaroth]

So I suggest to keep the code as it's now. We could make better change later.

[bclement-ocp]

Sure I am fine with keeping that code as is for now, but the code in look_for_sat needs to be fixed to actually use the split during model generation!

[Stevendeo]

This should happen before (set-logic ...)

[Stevendeo]

As y cannot be optimized, I believe we should warn the user when he invokes (get-objectives)

[bclement-ocp]

I think we are good with a couple minor omissions noted inline; please fix these before merging!

[bclement-ocp]

If it's an int, it should not be called has_incremental. I guess two of my comments in the previous round somewhat contradicted each other. Maybe incremental_depth?

[bclement-ocp]

Should have a link back to #993