From 8218f25222d343952eca306d1a906a5d6b617c2c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 May 2022 15:30:03 -0700
Subject: [PATCH] add decide callback

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/update_api.py            |  4 +++-
 src/api/dotnet/UserPropagator.cs | 36 ++++++++++++++++++++++++++++++++
 src/api/z3_api.h                 |  1 +
 3 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index b0b795b23..0553843cb 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -414,6 +414,7 @@ def mk_dotnet(dotnet):
 
     for name, ret, sig in Closures:
         sig = sig.replace("void*","voidp").replace("unsigned","uint")
+        sig = sig.replace("Z3_ast*","ref IntPtr").replace("uint*","ref uint").replace("Z3_lbool*","ref int")
         ret = ret.replace("void*","voidp").replace("unsigned","uint")
         if "*" in sig or "*" in ret:
             continue
@@ -1349,7 +1350,8 @@ z3_ml_callbacks = frozenset([
     'Z3_solver_propagate_final',
     'Z3_solver_propagate_eq',
     'Z3_solver_propagate_diseq',
-    'Z3_solver_propagate_created'
+    'Z3_solver_propagate_created',
+    'Z3_solver_propagate_decide'
     ])
 
 def mk_ml(ml_src_dir, ml_output_dir):
diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs
index 13532fdf4..4f604b4cb 100644
--- a/src/api/dotnet/UserPropagator.cs
+++ b/src/api/dotnet/UserPropagator.cs
@@ -55,6 +55,14 @@ namespace Microsoft.Z3
         /// </summary>                
 	public delegate void CreatedEh(Expr term);
 
+        /// <summary>
+        /// Delegate type for callback into solver's branching
+	/// <param name="term">A bit-vector or Boolean used for branching</param>
+	/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
+	/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
+	/// </summary>                
+	public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
+
 	Solver solver;
 	Context  ctx;
 	GCHandle gch;
@@ -64,6 +72,7 @@ namespace Microsoft.Z3
 	EqEh    eq_eh;
 	EqEh    diseq_eh;
 	CreatedEh created_eh;
+	DecideEh  decide_eh;
 
 
 	static void _push(voidp ctx, Z3_solver_callback cb) {
@@ -137,6 +146,20 @@ namespace Microsoft.Z3
            prop.callback = IntPtr.Zero;
 	}
 
+	static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) {
+	   var gch = GCHandle.FromIntPtr(ctx);
+           var prop = (UserPropagator)gch.Target;
+	   var t = Expr.Create(prop.ctx, a);
+	   var u = t;
+	   prop.callback = cb;
+	   prop.decide_eh(ref t, ref idx, ref phase);
+           prop.callback = IntPtr.Zero;
+	   if (u != t) {
+	       a = t.NativeObject;
+	   }
+	   t.Dispose();
+	}
+
         /// <summary>
         /// Propagator constructor from a solver class.
         /// </summary>        
@@ -266,6 +289,19 @@ namespace Microsoft.Z3
 	   }
         }
 
+        /// <summary>
+        /// Set decision callback
+	/// </summary>
+	public DecideEh Decide
+	{
+           set
+	   {
+ 	      this.decide_eh = value;
+              if (solver != null)
+                  Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
+	   }
+        }
+
         /// <summary>
         /// Track assignments to a term
 	/// </summary>
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index e7528da55..4e5f5f5b5 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6801,6 +6801,7 @@ extern "C" {
        In case the expression is a bitvector the bit to split on is determined by the bit argument and the 
        truth-value to try first is given by is_pos. In case the truth value is undefined the solver will decide.
 
+       def_API('Z3_solver_propagate_decide', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_decide_eh)))
     */
     void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);