the meaning of unknown in an optimization problem, and intermediate (nonoptimal) solutions.

[oferst]

1. If I stop Z3 before termination and get
   unknown
   (objectives
   ( (66 1039))
   )
   (model
   ...

does this mean that it found a feasible solution (i.e., satisfies all the hard constraints), but not the optimum ? it makes more sense to me that the status should be 'sat' rather than 'unknown'. Perhaps there should be a new status 'sat but not known if optimal'.

2. could be great to give it the option to print non-optimal solution during run-time. Having the ctrl^c option is not always good enough when it is a long run-time: you do not know whether the solution is good enough to stop the engine or whether it even found a first solution. So while pressing ctrl^c tells you this, it also stops the process.
   A nice interface to this is e.g., the one in cplex. There you can give it a parameter CPX_PARAM_INTSOLFILEPREFIX with the prefix of the solution files that it will emit during the run.

[NikolajBjorner]

Makes sense.

[oferst]

Thanks for implementing this! Two comments:

1. It is better (i.e., consistent with other tools) if it will also emit the optimal (final) solution as a file with that prefix. So I fixed it by adding
   model_ref mdl;
   s().get_model(mdl);
   m_c.model_updated(mdl.get());

in opt/maxres.cpp line 327, in case you want to add it too.
2. Ideally this feature should be global so it works with other supported formats, e.g., opb and wcnf (by the way currently in those formats ctrl-c does not produce the current solution).

[oferst]

My apology for item #2 in the previous post: the solution_prefix is already supported globally.

[NikolajBjorner]

Ah, I thought you wanted the output format to follow opb/wcnf format rules when the input is in this format. That is a valid ask, but something I would not like to do. The other optimization modules don't call into the model_updated functionality yet, but I take you only use maxsat at this point.