Add support for model minimization and maximization

[mbovel]

This PR adds support for model minimization and maximization by adding minimize and maximize methods to the Optimizer trait.

The new tests can be run from the sbt shell using it:testOnly *OptimizerSuite*.

[CLAassistant]

All committers have signed the CLA.

[samarion]

This LGTM. You'll need to add yourself to .larabot.conf in a separate PR for the larabot presubmit to run though.

[mbovel]

I added myself to the trust list, but the CI still hasn't run. Should I just open a new PR?

[mario-bucev]

Due to the log4j vulnerability, EPFL restricted internet access to some of its servers, which seems to include larabot.

[mbovel]

When running the tests twice with "nativez3-opt", I get a fatal error:

# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x000000014448321d, pid=5775, tid=0x0000000000015107
#
# JRE version: OpenJDK Runtime Environment (8.0_312) (build 1.8.0_312-bre_2021_10_20_23_15-b00)
# Java VM: OpenJDK 64-Bit Server VM (25.312-b00 mixed mode bsd-amd64 compressed oops)
# Problematic frame:
# C  [libz3.dylib+0x4e21d]  Z3_optimize_check+0x6e

Stack: [0x00007000b644e000,0x00007000ba44e000],  sp=0x00007000ba44a4e0,  free space=65521k
Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
C  [libz3.dylib+0x4e21d]  Z3_optimize_check+0x6e
j  com.microsoft.z3.Native.INTERNALoptimizeCheck(JJ)I+0
j  com.microsoft.z3.Native.optimizeCheck(JJ)I+2
j  z3.scala.Z3Optimizer.check()Lscala/Option;+14
j  inox.solvers.z3.NativeZ3Optimizer$underlying$.$anonfun$checkAssumptions$2(Linox/solvers/z3/NativeZ3Optimizer$underlying$;Linox/solvers/SolverResponses$Configuration;)Linox/solvers/SolverResponses$SolverResponse;+9
j  inox.solvers.z3.NativeZ3Optimizer$underlying$$$Lambda$7266.apply()Ljava/lang/Object;+8
j  inox.solvers.z3.NativeZ3Optimizer$underlying$.tryZ3(Lscala/Function0;)Lscala/Option;+5
j  inox.solvers.z3.NativeZ3Optimizer$underlying$.checkAssumptions(Linox/solvers/SolverResponses$Configuration;Lscala/collection/immutable/Set;)Linox/solvers/SolverResponses$SolverResponse;+28

Could this problem have been introduced with this PR, or is it an existing issue with Inox, Scala Z3 or Z3 Java API?

[samarion]

There are some issues with the native Z3 implementation which cause it to segfault once in a while (rarely and non-deterministically). Is the crash reproducible in your case?

With some luck, updating to a newer Z3 version (https://github.com/epfl-lara/ScalaZ3/pull/80) will help with these crashes.

[mbovel]

Is the crash reproducible in your case?

Yes; it always crashes on the second run ofOptimizerSuite from the sbt shell.

Log

``` $ sbt ... sbt:inox> it:testOnly *OptimizerSuite* ... [info] OptimizerSuite: [info] - 1: unsatisfiable soft constraint solvr=nativez3-opt (338 milliseconds) [info] - 2: unsatisfiable soft constraint solvr=smt-z3-opt (176 milliseconds) [info] - 3: n times n, minimize solvr=nativez3-opt (104 milliseconds) [info] - 4: n times n, minimize solvr=smt-z3-opt (128 milliseconds) [info] - 5: n times n, maximize solvr=nativez3-opt (30 milliseconds) [info] - 6: n times n, maximize solvr=smt-z3-opt (58 milliseconds) [info] Run completed in 1 second, 499 milliseconds. [info] Total number of tests run: 6 [info] Suites: completed 1, aborted 0 [info] Tests: succeeded 6, failed 0, canceled 0, ignored 0, pending 0 [info] All tests passed. [success] Total time: 8 s, completed Jan 5, 2022 12:26:45 PM sbt:inox> it:testOnly *OptimizerSuite* ... # A fatal error has been detected by the Java Runtime Environment: # # SIGSEGV (0xb) at pc=0x00000001372c221d, pid=8925, tid=0x0000000000014807 # # JRE version: OpenJDK Runtime Environment (8.0_312) (build 1.8.0_312-bre_2021_10_20_23_15-b00) # Java VM: OpenJDK 64-Bit Server VM (25.312-b00 mixed mode bsd-amd64 compressed oops) # Problematic frame: # C [libz3.dylib+0x4e21d] Z3_optimize_check+0x6e ... ```

[samarion]

Hmm, well looking at the NativeZ3Solver implementation I see we have some additional synchronization around the creation and destruction of the underlying Z3 instance. Maybe we need something similar for the optimizer, and to be safe, you should probably share the object on which synchronization is performed between NativeZ3Solver and NativeZ3Optimizer.

[mbovel]

Maybe we need something similar for the optimizer [...]

I tried it (see above). It does not fix the problem.

Actually I see that I get errors with other tests as well, also in master. For example (failing at the first run):

$ sbt
sbt:inox> it:testOnly *BagSuite*
...
[info] -  24: Finite model finding 3 solvr=smt-cvc4 lucky=true (104 milliseconds)
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x00000001424fefcb, pid=11923, tid=0x0000000000014703
#
# JRE version: OpenJDK Runtime Environment (8.0_312) (build 1.8.0_312-bre_2021_10_20_23_15-b00)
# Java VM: OpenJDK 64-Bit Server VM (25.312-b00 mixed mode bsd-amd64 compressed oops)
# Problematic frame:
# C  [libz3.dylib+0x43ffcb]  _ZN3smt17theory_array_full28instantiate_select_map_axiomEPNS_5enodeES2_+0x2b

Or (failing on second run):

$ sbt
sbt:inox> it:testOnly *StringSuite*
...
[info] StringSuite:
[info] -   1: Empty string model solvr=nativez3 (453 milliseconds)
...
sbt:inox> it:testOnly *StringSuite*
...
[info] StringSuite:
[info] -   1: Empty string model solvr=nativez3 *** FAILED *** (296 milliseconds)
[info]   com.microsoft.z3.Z3Exception: Sort mismatch at argument #1 for function (declare-fun String$3 ((Seq (_ BitVec 8))) String$2) supplied sort is String
[info]   at com.microsoft.z3.Native.mkApp(Native.java:1093)
[info]   at z3.scala.Z3Context.mkApp(Z3Context.scala:252)
[info]   at z3.scala.Z3FuncDecl.apply(Z3FuncDecl.scala:5)
[info]   at inox.solvers.z3.Z3Native.rec$1(Z3Native.scala:382)
[info]   at inox.solvers.z3.Z3Native.rec$1(Z3Native.scala:255)
[info]   at inox.solvers.z3.Z3Native.rec$1(Z3Native.scala:246)
[info]   at inox.solvers.z3.Z3Native.toZ3Formula(Z3Native.scala:520)
...

So this is probably unrelated to this PR. Probably best investigated in a separate issue or PR.

[samarion]

The instantiate_select_map_axiom is the error we usually see.

I've never seen the error you're getting in the StringSuite, but that looks more like an Inox bug. I'm not sure anybody else every tried running the test-suite(s) multiple times in a single sbt session, so stuff could be broken (but I can't really imagine why the behavior would change).

[mbovel]

Ok, thanks for taking a look!

So could we merge this PR or are other changes required?

[samarion]

Yep, LGTM. Thanks for addressing all the comments!