add on_binding callbacks across APIs

update release notes,
add to Java, .Net, C++

Author: NikolajBjorner

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.

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')

src/api/c++/z3++.h

@@ -4295,12 +4295,14 @@ namespace z3 {
         typedef std::function<void(expr const&, expr const&)> eq_eh_t;
         typedef std::function<void(expr const&)> created_eh_t;
         typedef std::function<void(expr, unsigned, bool)> decide_eh_t;
+        typedef std::function<bool(expr const&, expr const&)> 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<z3::context*> 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<user_propagator_base*>(_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);

src/api/dotnet/UserPropagator.cs

@@ -64,7 +64,15 @@ public class UserPropagator : IDisposable
         /// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
         /// <param name="phase">The tentative truth-value</param>
         public delegate void DecideEh(Expr term, uint idx, bool phase);
-        
+
+        /// <summary>
+        /// Delegate type for callback when a quantifier is bound to an instance.
+        /// </summary>
+        /// <param name="q">Quantifier</param>
+        /// <param name="inst">Instance</param>
+        /// <returns>true if binding is allowed to take effect in the solver, false if blocked by callback</returns>
+        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 @@ public class UserPropagator : IDisposable
         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 @@ public class UserPropagator : IDisposable
         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 @@ static void _decide(voidp ctx, Z3_solver_callback cb, Z3_ast a, uint idx, bool p
             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;
+        }
+
         /// <summary>
         /// Propagator constructor from a solver class.
         /// </summary>        
@@ -362,6 +385,20 @@ public DecideEh Decide
             }
         }
 
+        /// <summary>
+        /// Set binding callback
+        /// </summary>
+        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);
+            }
+        }
+
 
         /// <summary>
         /// Set the next decision
@@ -378,6 +415,8 @@ public bool NextSplit(Expr e, uint idx, int phase)
             return Native.Z3_solver_next_split(ctx.nCtx, this.callback, e?.NativeObject ?? IntPtr.Zero, idx, phase) != 0;
         }
 
+        
+
         /// <summary>
         /// Track assignments to a term
         /// </summary>

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<JavaInfo*>(_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;
 

src/api/java/UserPropagatorBase.java

@@ -43,6 +43,13 @@ protected final void eqWrapper(long lx, long ly) {
         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 void created(Expr<?> ast) {}
     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) {}