diff --git a/README.md b/README.md index 695a7f3c15..251a00f1ea 100644 --- a/README.md +++ b/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. diff --git a/lib/ivy.xml b/lib/ivy.xml index 0b37f16cfe..40df84844d 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/src/org/sosy_lab/java_smt/api/UserPropagator.java b/src/org/sosy_lab/java_smt/api/UserPropagator.java index 9765658d7d..3f9d4ff46f 100644 --- a/src/org/sosy_lab/java_smt/api/UserPropagator.java +++ b/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. + * + *

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 boolean onBinding(T quantifiedVar, T instantiation) { + return true; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3UserPropagator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3UserPropagator.java index 591c346b61..2457b382eb 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3UserPropagator.java +++ b/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 canonicalizer = new HashMap<>(); + private final Map 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 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