Fix issue 737

[Halbaroth]

This PR fix the issue #737.

[bclement-ocp]

Can we actually reach this point? I think that if the SAT solver is not Tableaux, we will already fail when set-option :produce-models is encountered, and if set-option :produce-models is not encountered, we will fail as well.

(Actually, do we? We probably should just error out with "model generation is disabled" here, independenty of the solver, no?)

[Halbaroth]

Yes, we can reach this point. This is the very purpose of this PR to add an appropriate error message in this case.
This error occurs when we call Alt-Ergo without specifying the sat solver but using get-model in the input file. Another solution would be to change automatically the SAT solver to Tableaux when we see a set-option :produce-models.

[bclement-ocp]

We cannot do that because set-option :produce-models happens after we have chosen the SAT solver.

But what I don't understand is if we call Alt-Ergo without a solver but use get-model without setting --interpretation we should have an error that the interpretation is INone, so I don't understand why we proceed past that part. Maybe we don't have that error.

To clarify:

• If we see a get-model and the interpretation is INone, we must error out because we are not in model-generation mode. This is independent of the solver used. I am not sure we actually do this currently but we must do it.
• To reach get-model with a non-INone interpretation, we must either have a (set-option :produce-models), or set the --interpretation or --produce-model command line flags.
• (set-option :produce-models) errors out if the solver is not Tableaux (I think it does, but am not actually sure)
• The flags --interpretation and --produce-model forces the solver to Tableaux, or error out if another solver is explicitly provided (I believe I wrote that code)

So I don't understand when we reach the point where the solver is relevant here -- either we have the interpretation set, and the solver is necessarily Tableaux, or we don't, and that's an error independent of the solver. If we can have a non-INone interpretation with a non-Tableaux solver somehow, that's the bug we need to fix.

[Halbaroth]

Oh yes, you are right. I tried to do it last month, I forgot this issue.

• Currently, if we use (set-option :produce-models), AE actives the generation of models but you have to choose the SAT-solver.
  

  alt-ergo/src/bin/common/solving_loop.ml

  Lines 354 to 363 in 88ea461

  	| ":produce-models", Symbol { name = Simple "true"; _ } ->
  	(* TODO: The generation of models is supported only with the SAT
  	solver Tableaux. Remove this line after merging the OptimAE
  	PR. See https://github.com/OCamlPro/alt-ergo/pull/553 *)
  	if Stdlib.(Options.get_sat_solver () = Tableaux) then
  	Options.set_interpretation ILast
  	else Printer.print_wrn "%a The generation of models is not supported \
  	for the current SAT solver. Please choose the \
  	SAT solver Tableaux."
  	Loc.report st_loc

  
  It doesn't produce an error if you use the flag --interpretation none.
  If you reach a get-model without using set-option :produce-models or the flags --interpretation, --produce-model, --dump-models, AE displays a smtlib error.
• It is the case.
• (set-option :produce-models) produces an error if we don't choose an appropriate SAT solver.
• I confirm that AE prints an error if we try to use another SAT solver with the flags --produce-model and --interpretation forces the SAT-solver to Tableaux.

[bclement-ocp]

Thanks for confirming! Then it seems to me that this new error is redundant with the existing one below (which should mention --produce-models in addition to :produce-models, I guess), no?

[bclement-ocp]

Ah, then that's the actual issue. We should fail if we see (set-option :produce-models true) but can't produce models due to a wrong solver being selected.

(I said "we should ignore" but no -- we really should error I think)

[Halbaroth]

I removed the warning message and now AE fails properly when we forget to set the right sat solver.

[bclement-ocp]

Actually after re-reading the smtlib spec I believe we should "fail" in the sense of returning an smtlib error but then continue as if the set-option was not encountered.

I think this PR should also update the message when we see a get-model but we are not in model-production mode; currently it says to use (set-option :produce-models true) but it should say to use --produce-models instead, because otherwise there will immediately be another error due to Tableaux not being selected.

(And maybe add tests for the combinations of --produce-models / set-option / get-model?)

[Halbaroth]

Ok, we can add some cram tests but we should fix the issue with Mac OS first.

I will print a smtlib error but we don't print anything if there is (get-model) after a failed set-option?

[bclement-ocp]

We do I think? It's the message that currently says "please use set-option :produce-models"

[bclement-ocp]

What is meta about that option?

[Halbaroth]

I thought this option turns some other options on. I can remove it.

[bclement-ocp]

Ah, right -- it is roughly equivalent to --sat-solver Tableaux --interpretation last indeed (but not exactly; --interpretation can still be overwritten separately) but that is an implementation detail, from the user point of view it is just an option.