Implement Solver Interrupt and SMT2 Log in Java

[baierd]

In Issues #867 and #1006 the ability to interrupt single solvers as well as the ability to log in SMT-LIB2 format was added.
However this is not possible in Java at the moment. (As far as i am not mistaken)
It would be great if you could add this to the Java wrapper.

[NikolajBjorner]

You can set interrupt on a context, this cancels the solver based on the context.
The method is called "interrupt" and defined on the Context object.

The "toString" method on the Solver object prints the solver state in SMTLIB2 format.

[baierd]

I am aware of both proposed workarounds but they are not useful for our project.
I am an colleague of @PhilippWendler and work on the same project as he does, hence why i mentioned the 2 issues in particular.

[NikolajBjorner]

Regarding logging to an SMT2 file: It is an option on the solver object.
You should set this option (smtlib2_log) before invoking calls on the solver.
There is no specific Java support required for this feature.

z3 /pm:solver
[module] solver, description: solver parameters
cancel_backup_file (symbol) file to save partial search state if search is canceled (default: )
enforce_model_conversion (bool) apply model transformation on new assertions (default: false)
smtlib2_log (symbol) file to save solver interaction (default: )
timeout (unsigned int) timeout on the solver object; overwrites a global timeout (default: 4294967295)

[NikolajBjorner]

regarding the missing call to interrupt the solver object selectively. This was indeed implemented, but absent from the Java API. It has now been added.