Add support for model minimization and maximization #171

mbovel · 2021-11-28T18:10:16Z

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 · 2021-11-28T18:10:20Z

All committers have signed the CLA.

samarion · 2021-12-02T14:55:57Z

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

mbovel · 2021-12-13T13:28:46Z

src/it/scala/inox/solvers/OptimizerSuite.scala

+      optimizer.assertCnstr(softClause, 1)
+      optimizer.check(Model) match {
+        case SatWithModel(model) =>
+          assert(getIntegerValue(model, v) > 10)


I relaxed the tests so that they work with all valid results.

mbovel · 2021-12-13T21:36:07Z

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

mario-bucev · 2021-12-14T07:27:59Z

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

samarion · 2021-12-17T13:34:23Z

src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala

@@ -25,7 +25,7 @@ trait SMTLIBDebugger extends SMTLIBTarget {
  /* Printing VCs */
  protected lazy val debugOut: Option[java.io.FileWriter] = {
    implicit val debugSection = DebugSectionSMT
-    if (reporter.isDebugEnabled) {
+    if (true) {


Please revert.

samarion · 2021-12-17T13:37:53Z

src/it/scala/inox/solvers/OptimizerSuite.scala

+      optimizer.minimize(x)
+      optimizer.check(Model) match {
+        case SatWithModel(model) =>
+          println(model)


I don't think it's good practice to have println in tests. (Same remark for the binary trees test below.)

samarion · 2021-12-17T13:40:18Z

src/it/scala/inox/solvers/OptimizerSuite.scala

+    val optimizer = factory.getNewSolver()
+    try {
+      optimizer.assertCnstr(clause)
+      optimizer.minimize(E(sizeId)(IntegerType())(aTree))


Optional: could you replace minimize(x) by maximize(-x) to test that function as well?

Done (added a new test).

mbovel · 2022-01-05T10:44:03Z

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 · 2022-01-05T11:24:27Z

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 (epfl-lara/ScalaZ3#80) will help with these crashes.

mbovel · 2022-01-05T11:31:01Z

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 · 2022-01-05T13:35:58Z

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 · 2022-01-06T12:58:07Z

src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala

@@ -17,7 +17,7 @@ trait NativeZ3Optimizer extends AbstractUnrollingOptimizer with Z3Unrolling { se

  override val name = "native-z3-opt"

-  protected object underlying extends {
+  protected val underlying = NativeZ3Solver.synchronized(new {


you should probably share the object on which synchronization is performed between NativeZ3Solver and NativeZ3Optimizer.

So would it make sense to just use NativeZ3Solver.synchronized in both classes?

mbovel · 2022-01-06T13:49:40Z

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 · 2022-01-06T15:09:26Z

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 · 2022-01-06T16:35:11Z

Ok, thanks for taking a look!

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

samarion · 2022-01-07T08:40:27Z

Yep, LGTM. Thanks for addressing all the comments!

mbovel force-pushed the mb/optimizer-suite branch from 7944f76 to 243190c Compare December 13, 2021 13:26

mbovel marked this pull request as ready for review December 13, 2021 13:27

mbovel commented Dec 13, 2021

View reviewed changes

mbovel changed the title ~~Add OptimizerSuite~~ Add support for model minimization and maximization Dec 17, 2021

samarion reviewed Dec 17, 2021

View reviewed changes

mbovel marked this pull request as draft December 17, 2021 14:01

mbovel force-pushed the mb/optimizer-suite branch from 676272f to b482847 Compare January 3, 2022 13:57

Add support for minimize/maximize in Optimizers

eb8329b

mbovel force-pushed the mb/optimizer-suite branch from b482847 to eb8329b Compare January 3, 2022 14:01

mbovel marked this pull request as ready for review January 5, 2022 10:44

Synchronize native optimizer creation and destruction

c97ee31

mbovel commented Jan 6, 2022

View reviewed changes

samarion merged commit 2f402f9 into epfl-lara:master Jan 7, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for model minimization and maximization #171

Add support for model minimization and maximization #171

mbovel commented Nov 28, 2021 •

edited

Loading

CLAassistant commented Nov 28, 2021 •

edited

Loading

samarion commented Dec 2, 2021

mbovel Dec 13, 2021

mbovel commented Dec 13, 2021

mario-bucev commented Dec 14, 2021

samarion Dec 17, 2021

mbovel Jan 5, 2022

samarion Dec 17, 2021

mbovel Jan 5, 2022

samarion Dec 17, 2021

mbovel Jan 5, 2022

mbovel commented Jan 5, 2022

samarion commented Jan 5, 2022

mbovel commented Jan 5, 2022

samarion commented Jan 5, 2022

mbovel Jan 6, 2022 •

edited

Loading

mbovel commented Jan 6, 2022 •

edited

Loading

samarion commented Jan 6, 2022

mbovel commented Jan 6, 2022

samarion commented Jan 7, 2022

Add support for model minimization and maximization #171

Add support for model minimization and maximization #171

Conversation

mbovel commented Nov 28, 2021 • edited Loading

CLAassistant commented Nov 28, 2021 • edited Loading

samarion commented Dec 2, 2021

mbovel Dec 13, 2021

Choose a reason for hiding this comment

mbovel commented Dec 13, 2021

mario-bucev commented Dec 14, 2021

samarion Dec 17, 2021

Choose a reason for hiding this comment

mbovel Jan 5, 2022

Choose a reason for hiding this comment

samarion Dec 17, 2021

Choose a reason for hiding this comment

mbovel Jan 5, 2022

Choose a reason for hiding this comment

samarion Dec 17, 2021

Choose a reason for hiding this comment

mbovel Jan 5, 2022

Choose a reason for hiding this comment

mbovel commented Jan 5, 2022

samarion commented Jan 5, 2022

mbovel commented Jan 5, 2022

samarion commented Jan 5, 2022

mbovel Jan 6, 2022 • edited Loading

Choose a reason for hiding this comment

mbovel commented Jan 6, 2022 • edited Loading

samarion commented Jan 6, 2022

mbovel commented Jan 6, 2022

samarion commented Jan 7, 2022

mbovel commented Nov 28, 2021 •

edited

Loading

CLAassistant commented Nov 28, 2021 •

edited

Loading

mbovel Jan 6, 2022 •

edited

Loading

mbovel commented Jan 6, 2022 •

edited

Loading