Merge pull request #506 from sosy-lab/update_z3-4.15.3

Update Z3 to v4.15.4

Author: kfriedberger

README.md

@@ -60,19 +60,19 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,
 
 JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
 
-| SMT Solver |       Linux x64       |     Linux arm64     | Windows x64 | Windows arm64 |                       MacOS x64                        | MacOS arm64 | Description |
-| --- |:---------------------:|:-------------------:|:---:|:---:|:------------------------------------------------------:|:---:|:--- |
-| [Bitwuzla](https://bitwuzla.github.io/) |  :heavy_check_mark:²  | :heavy_check_mark:² | :heavy_check_mark: |  |                                                        |  | a fast solver for bitvector logic |
-| [Boolector](https://boolector.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | a fast solver for bitvector logic, misses formula introspection, deprecated |
-| [CVC4](https://cvc4.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  |  |
-| [CVC5](https://cvc5.github.io/) |  :heavy_check_mark:  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |
-| [MathSAT5](http://mathsat.fbk.eu/) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/430)³ |  |  |
-| [OpenSMT](https://verify.inf.usi.ch/opensmt) |  :heavy_check_mark:²  | :heavy_check_mark:² |  |  |                                                        |  |  |
-| [OptiMathSAT](http://optimathsat.disi.unitn.it/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | based on MathSAT5, with support for optimization queries |
-| [Princess](http://www.philipp.ruemmer.org/princess.shtml) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | Java-based SMT solver |
-| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | Java-based SMT solver |
-| [Yices2](https://yices.csl.sri.com/) |  :heavy_check_mark:   |                     | [maybe](https://github.com/sosy-lab/java-smt/pull/215) |  | [maybe](https://github.com/sosy-lab/java-smt/pull/400)³ |  |  |
-| [Z3](https://github.com/Z3Prover/z3) |  :heavy_check_mark:²  | :heavy_check_mark:² | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | mature and well-known solver |
+| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description |
+| --- |:---:|:---:|:---:|:---:|:---:|:---:|:--- |
+| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: |  |  |  | a fast solver for bitvector logic |
+| [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |  |  |  |  | a fast solver for bitvector logic, misses formula introspection, deprecated |
+| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: |  |  |  |  |  |  |
+| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |  | :heavy_check_mark: | :heavy_check_mark: |  |
+| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ |  |  |
+| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² |  |  |  |  |  |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: |  |  |  |  |  | based on MathSAT5, with support for optimization queries |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/215) |  | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ |  |  |
+| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
 
 We support a reasonable list of operating systems and versions.
 - Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
@@ -88,7 +88,9 @@ available with Ubuntu 18.04 or later.
 
 ² Solver requires at least `GLIBC_2.29`/`GLIBCXX_3.4.26` or `GLIBC_2.34`/`GLIBCXX_3.4.29`,
 available with Ubuntu 22.04 or later.  
-³ We do not provide a signed solver library for macOS. The user needs to compile and sign it.
+³ Solver requires at least `GLIBC_2.38`/`GLIBCXX_3.4.31`,
+available with Ubuntu 24.04 or later.  
+⁴ We do not provide a signed solver library for macOS. The user needs to compile and sign it.
 
 #### Solver Features
 
@@ -109,7 +111,7 @@ If something specific is missing, please [look for or file an issue](https://git
 
 #### Multithreading Support
 
-| SMT Solver | Concurrent context usage⁴ | Concurrent prover usage⁵ |
+| SMT Solver | Concurrent context usage⁵ | Concurrent prover usage⁶ |
 | --- |:---:|:---:|
 | [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: |  |
 | [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |
@@ -126,13 +128,13 @@ If something specific is missing, please [look for or file an issue](https://git
 Interruption using a [ShutdownNotifier][] may be used to interrupt a solver from any thread.
 Formulas are translatable in between contexts/provers/threads using _FormulaManager.translateFrom()_.
 
-⁴ Multiple contexts, but all operations on each context only from a single thread.  
-⁵ Multiple provers on one or more contexts, with each prover using its own thread.
+⁵ Multiple contexts, but all operations on each context only from a single thread.  
+⁶ Multiple provers on one or more contexts, with each prover using its own thread.
 
 #### Garbage Collection in Native Solvers
 
 JavaSMT exposes an API for performing garbage collection on solvers implemented in a native language.
-As a native solver has no way of knowing whether the created formula object is still referenced 
+As a native solver has no way of knowing whether the created formula object is still referenced
 by the client application, this API is necessary to avoid leaking memory.
 Note that several solvers already support _hash consing_ and thus,
 there is never more than one copy of an identical formula object in memory.
@@ -141,9 +143,9 @@ in the application, it is not necessary to perform any garbage collection at all
 Additionally, the memory for formulas created on user-side (i.e., via JavaSMT) is negligible
 compared to solver-internal memory-consumption when solving a hard SMT query.
 
-- **Z3**: The parameter `solver.z3.usePhantomReferences` may be used to control 
-  whether JavaSMT will attempt to decrease references on Z3 formula 
-  objects once they are no longer referenced.
+- **Z3**: The parameter `solver.z3.usePhantomReferences` may be used to control
+  whether JavaSMT will attempt to decrease references on Z3 formula objects
+  once they are no longer referenced.
 - **MathSAT5**: Currently we do not support performing garbage collection for MathSAT5.
 - **CVC4, CVC5, Bitwuzla, OpenSMT**: Solvers using SWIG bindings do perform garbage collection.
 - **Other native SMT solvers**: we do not perform garbage collection.

lib/ivy.xml

@@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.12" conf="runtime-mathsat-x64->solver-mathsat-x64; runtime-mathsat-arm64->solver-mathsat-arm64" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.15.2" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.15.4" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.9.0-gef441e1c" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />

src/org/sosy_lab/java_smt/api/UserPropagator.java

@@ -110,4 +110,25 @@ public interface UserPropagator {
    * @param theoryExpr The expression to observe.
    */
   void registerExpression(BooleanFormula theoryExpr);
+
+  /**
+   * The on_binding method allows custom user-defined propagators to intercept and control
+   * quantifier instantiations during solving. This callback is invoked whenever the solver performs
+   * a quantifier instantiation (i.e., binds a quantifier to a specific instance). It provides a
+   * hook for the user propagator to inspect the quantifier and its instantiation.
+   *
+   * <p>The default implementation does nothing and accepts all instantiations. It serves for
+   * backward compatibility in the API.
+   *
+   * @param quantifiedVar The quantified variable being instantiated. This is a BooleanFormula
+   *     representing the variable in the quantifier.
+   * @param instantiation The specific instantiation being applied to the quantified variable. It
+   *     has the same formula type as the quantified variable.
+   * @since Z3 release 4.15.3
+   * @return By returning false, the callback signals that the instantiation should be discarded by
+   *     the solver.
+   */
+  default <T extends Formula> boolean onBinding(T quantifiedVar, T instantiation) {
+    return true;
+  }
 }

src/org/sosy_lab/java_smt/solvers/z3/Z3UserPropagator.java

@@ -15,6 +15,7 @@
 import java.util.Map;
 import java.util.Optional;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.PropagatorBackend;
 import org.sosy_lab.java_smt.api.UserPropagator;
 
@@ -28,7 +29,7 @@ final class Z3UserPropagator extends UserPropagatorBase implements PropagatorBac
   /* We use this map to reuse existing formula wrappers and avoid creating unnecessary phantom
   references (if enabled). This is particularly useful, because the user propagator frequently
   reports the same formulas. */
-  private final Map<Long, BooleanFormula> canonicalizer = new HashMap<>();
+  private final Map<Long, Formula> canonicalizer = new HashMap<>();
 
   Z3UserPropagator(
       long ctx,
@@ -70,7 +71,7 @@ protected void eqWrapper(long pL, long pL1) {}
   @Override
   protected void fixedWrapper(long lvar, long lvalue) {
     assert lvalue == z3True || lvalue == z3False;
-    userPropagator.onKnownValue(encapsulate(lvar), lvalue == z3True);
+    userPropagator.onKnownValue(encapsulateBoolean(lvar), lvalue == z3True);
   }
 
   // TODO: This method is called if Z3 re-instantiates a user propagator for a sub-problem
@@ -91,7 +92,12 @@ protected void createdWrapper(long le) {}
   protected void decideWrapper(long lvar, int bit, boolean isPositive) {
     // We currently only allow tracking of decision on boolean formulas,
     // so we ignore the <bit> parameter
-    userPropagator.onDecision(encapsulate(lvar), isPositive);
+    userPropagator.onDecision(encapsulateBoolean(lvar), isPositive);
+  }
+
+  @Override
+  protected boolean onBindingWrapper(long quantifiedVar, long instantiation) {
+    return userPropagator.onBinding(encapsulate(quantifiedVar), encapsulate(instantiation));
   }
 
   // ===========================================================================
@@ -160,12 +166,16 @@ private long[] extractInfoFromArray(BooleanFormula[] formulaArray) {
     return formulaInfos;
   }
 
-  private BooleanFormula encapsulate(final long z3Expr) {
+  private BooleanFormula encapsulateBoolean(final long z3Expr) {
+    return (BooleanFormula) encapsulate(z3Expr);
+  }
+
+  private Formula encapsulate(final long z3Expr) {
     // Due to pointer alignment, the lowest 2-3 bits are always 0 which can lead to
     // more collisions in the hashmap. To counteract, we fill the lowest bits by rotating the
     // value. The rotation guarantees a bijective transformation.
     return canonicalizer.computeIfAbsent(
-        Long.rotateRight(z3Expr, 3), key -> creator.encapsulateBoolean(z3Expr));
+        Long.rotateRight(z3Expr, 3), key -> creator.encapsulateWithTypeOf(z3Expr));
   }
 
   @Override

src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java

@@ -469,9 +469,6 @@ public void bvRotateByBV() throws SolverException, InterruptedException {
       case PRINCESS:
         bitsizes = new int[] {2, 3}; // Princess is too slow for larger bitvectors
         break;
-      case Z3:
-        bitsizes = new int[] {2, 3, 4, 8}; // Z3 is too slow for larger bitvectors since v4.15.0
-        break;
       default:
         bitsizes = new int[] {2, 3, 4, 8, 13, 25, 31};
         break;