diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 9c42a326c..0ea4230f6 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -7,6 +7,15 @@ Version 4.next - CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. - add global incremental pre-processing for the legacy core. +Version 4.15.3 +============== +- Add UserPropagator callback option for quantifier instantiations. It allows the user propagator to + intercept quantifier instantiations. It can then inspect these in the callback. By returning false, + the callback signals that the instantiation should be discarded by the solver. The user propagator + is then able to apply finer control over instantiations. It can also use this mechanism to delay + instantiations. + + Version 4.15.2 ============== - #7690, #7691 - fix leak introduced in arithmetic solver. diff --git a/scripts/update_api.py b/scripts/update_api.py index 13bccf832..5c28bcd3e 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -641,6 +641,7 @@ def mk_java(java_src, java_dir, package_name): public static native void propagateRegisterEq(Object o, long ctx, long solver); public static native void propagateRegisterDecide(Object o, long ctx, long solver); public static native void propagateRegisterFinal(Object o, long ctx, long solver); + public static native void propagateRegisterOnBinding(Object o, long ctx, long solver); public static native void propagateAdd(Object o, long ctx, long solver, long javainfo, long e); public static native boolean propagateConsequence(Object o, long ctx, long solver, long javainfo, int num_fixed, long[] fixed, long num_eqs, long[] eq_lhs, long[] eq_rhs, long conseq); public static native boolean propagateNextSplit(Object o, long ctx, long solver, long javainfo, long e, long idx, int phase); @@ -684,6 +685,10 @@ def mk_java(java_src, java_dir, package_name): protected final void registerFinal() { Native.propagateRegisterFinal(this, ctx, solver); } + + protected final void registerOnBinding() { + Native.propagateRegisterOnBinding(this, ctx, solver); + } protected abstract void pushWrapper(); @@ -700,6 +705,8 @@ def mk_java(java_src, java_dir, package_name): protected abstract void fixedWrapper(long lvar, long lvalue); protected abstract void decideWrapper(long lvar, int bit, boolean is_pos); + + protected abstract boolean onBindingWrapper(long q, long inst); } """) java_native.write('\n') diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 02fbe311b..0a1e359da 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -4295,12 +4295,14 @@ namespace z3 { typedef std::function eq_eh_t; typedef std::function created_eh_t; typedef std::function decide_eh_t; + typedef std::function on_binding_eh_t; final_eh_t m_final_eh; eq_eh_t m_eq_eh; fixed_eh_t m_fixed_eh; created_eh_t m_created_eh; decide_eh_t m_decide_eh; + on_binding_eh_t m_on_binding_eh; solver* s; context* c; std::vector subcontexts; @@ -4372,6 +4374,13 @@ namespace z3 { expr val(p->ctx(), _val); p->m_decide_eh(val, bit, is_pos); } + + static bool on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) { + user_propagator_base* p = static_cast(_p); + scoped_cb _cb(p, cb); + expr q(p->ctx(), _q), inst(p->ctx(), _inst); + return p->m_on_binding_eh(q, inst); + } public: user_propagator_base(context& c) : s(nullptr), c(&c) {} @@ -4498,6 +4507,14 @@ namespace z3 { } } + void register_on_binding() { + m_on_binding_eh = [this](expr const& q, expr const& inst) { + return on_binding(q, inst); + }; + if (s) + Z3_solver_propagate_on_binding(ctx(), *s, on_binding_eh); + } + virtual void fixed(expr const& /*id*/, expr const& /*e*/) { } virtual void eq(expr const& /*x*/, expr const& /*y*/) { } @@ -4508,6 +4525,8 @@ namespace z3 { virtual void decide(expr const& /*val*/, unsigned /*bit*/, bool /*is_pos*/) {} + virtual bool on_binding(expr const& /*q*/, expr const& /*inst*/) { return true; } + bool next_split(expr const& e, unsigned idx, Z3_lbool phase) { assert(cb); return Z3_solver_next_split(ctx(), cb, e, idx, phase); diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs index b1a2d3df5..74c5774e8 100644 --- a/src/api/dotnet/UserPropagator.cs +++ b/src/api/dotnet/UserPropagator.cs @@ -64,7 +64,15 @@ namespace Microsoft.Z3 /// If the term is a bit-vector, then an index into the bit-vector being branched on /// The tentative truth-value public delegate void DecideEh(Expr term, uint idx, bool phase); - + + /// + /// Delegate type for callback when a quantifier is bound to an instance. + /// + /// Quantifier + /// Instance + /// true if binding is allowed to take effect in the solver, false if blocked by callback + public delegate bool OnBindingEh(Expr q, Expr inst); + // access managed objects through a static array. // thread safety is ignored for now. GCHandle gch; @@ -78,6 +86,7 @@ namespace Microsoft.Z3 EqEh diseq_eh; CreatedEh created_eh; DecideEh decide_eh; + OnBindingEh on_binding_eh; Native.Z3_push_eh push_eh; Native.Z3_pop_eh pop_eh; @@ -89,6 +98,7 @@ namespace Microsoft.Z3 Native.Z3_eq_eh diseq_wrapper; Native.Z3_decide_eh decide_wrapper; Native.Z3_created_eh created_wrapper; + Native.Z3_on_binding_eh on_binding_wrapper; void Callback(Action fn, Z3_solver_callback cb) { @@ -175,6 +185,19 @@ namespace Microsoft.Z3 prop.Callback(() => prop.decide_eh(t, idx, phase), cb); } + static bool _on_binding(voidp _ctx, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) + { + var prop = (UserPropagator)GCHandle.FromIntPtr(_ctx).Target; + using var q = Expr.Create(prop.ctx, _q); + using var inst = Expr.Create(prop.ctx, _inst); + bool result = true; + prop.Callback(() => { + if (prop.on_binding_wrapper != null) + result = prop.on_binding_eh(q, inst); + }, cb); + return result; + } + /// /// Propagator constructor from a solver class. /// @@ -362,6 +385,20 @@ namespace Microsoft.Z3 } } + /// + /// Set binding callback + /// + public OnBindingEh OnBinding + { + set + { + this.on_binding_wrapper = _on_binding; + this.on_binding_eh = value; + if (solver != null) + Native.Z3_solver_propagate_on_binding(ctx.nCtx, solver.NativeObject, on_binding_wrapper); + } + } + /// /// Set the next decision @@ -378,6 +415,8 @@ namespace Microsoft.Z3 return Native.Z3_solver_next_split(ctx.nCtx, this.callback, e?.NativeObject ?? IntPtr.Zero, idx, phase) != 0; } + + /// /// Track assignments to a term /// diff --git a/src/api/java/NativeStatic.txt b/src/api/java/NativeStatic.txt index 21d6ba075..f98357fde 100644 --- a/src/api/java/NativeStatic.txt +++ b/src/api/java/NativeStatic.txt @@ -153,6 +153,12 @@ static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val, bit, is_pos); } +static boolean on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) { + JavaInfo *info = static_cast(_p); + ScopedCB scoped(info, cb); + return info->jenv->CallVoidMethod(info->jobj, info->on_binding, (jlong)_q, (jlong)_inst); +} + DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEnv *jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) { JavaInfo *info = new JavaInfo; diff --git a/src/api/java/UserPropagatorBase.java b/src/api/java/UserPropagatorBase.java index 46a61400d..1dd26e7e4 100644 --- a/src/api/java/UserPropagatorBase.java +++ b/src/api/java/UserPropagatorBase.java @@ -43,6 +43,13 @@ public abstract class UserPropagatorBase extends Native.UserPropagatorBase { eq(x, y); } + @Override + protected final boolean onBindingWrapper(long lq, long linst) { + Expr q = new Expr(ctx, lq); + Expr inst = new Expr(ctx, linst); + return on_binding(q, inst); + } + @Override protected final UserPropagatorBase freshWrapper(long lctx) { return fresh(new Context(lctx)); @@ -77,6 +84,8 @@ public abstract class UserPropagatorBase extends Native.UserPropagatorBase { public void fixed(Expr var, Expr value) {} public void eq(Expr x, Expr y) {} + + public boolean on_binding(Expr q, Expr inst) { return true; } public void decide(Expr var, int bit, boolean is_pos) {}