From cd7ef11593d7c641abb4c4de9c7c1a49338cab27 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Jul 2022 11:00:58 +0200
Subject: [PATCH] add decide callbacks to propagator API

this is an intermediary state. The decide_eh is only partially implemented.
---
 scripts/update_api.py   |  1 +
 src/api/python/z3/z3.py | 29 ++++++++++++++++++++++++++++-
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index 8c6275c56..a468a6885 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1854,6 +1854,7 @@ _lib.Z3_solver_propagate_final.restype = None
 _lib.Z3_solver_propagate_fixed.restype = None
 _lib.Z3_solver_propagate_eq.restype = None
 _lib.Z3_solver_propagate_diseq.restype = None
+_lib.Z3_solver_propagate_decide.restype = None
 
 on_model_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
 _lib.Z3_optimize_register_model_eh.restype = None
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 724980339..8f227649c 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -11419,6 +11419,18 @@ def user_prop_diseq(ctx, cb, x, y):
     prop.diseq(x, y)
     prop.cb = None
 
+# TODO The decision callback is not fully implemented.
+# It needs to handle the ast*, unsigned* idx, and Z3_lbool* 
+def user_prop_decide(ctx, cb, t_ref, idx_ref, phase_ref):
+    prop = _prop_closures.get(ctx)
+    prop.cb = cb
+    t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
+    t, idx, phase = prop.decide(t, idx, phase)
+    t_ref = t
+    idx_ref = idx
+    phase_ref = phase
+    prop.cb = None
+    
 
 _user_prop_push = Z3_push_eh(user_prop_push)
 _user_prop_pop = Z3_pop_eh(user_prop_pop)
@@ -11428,6 +11440,7 @@ _user_prop_created = Z3_created_eh(user_prop_created)
 _user_prop_final = Z3_final_eh(user_prop_final)
 _user_prop_eq = Z3_eq_eh(user_prop_eq)
 _user_prop_diseq = Z3_eq_eh(user_prop_diseq)
+_user_prop_decide = Z3_decide_eh(user_prop_decide)
 
 def PropagateFunction(name, *sig):
     """Create a function that gets tracked by user propagator.
@@ -11531,6 +11544,13 @@ class UserPropagateBase:
             Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
         self.diseq = diseq
 
+    def add_decide(self, decide):
+        assert not self.decide
+        assert not self._ctx
+        if self.solver:
+            Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
+        self.decide = decide        
+
     def push(self):
         raise Z3Exception("push needs to be overwritten")
 
@@ -11547,7 +11567,14 @@ class UserPropagateBase:
         else:
             Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast)
         
-
+    #
+    # Tell the solver to perform the next split on a given term
+    # If the term is a bit-vector the index idx specifies the index of the Boolean variable being
+    # split on. A phase of true = 1/false = -1/undef = 0 = let solver decide is the last argument.
+    #
+    def next_split(self, t, idx, phase):
+        Z3_solver_next_split(self.ctx_ref(), ctypes.c_void_p(self.cb), t.ast, idx, phase)
+        
     #
     # Propagation can only be invoked as during a fixed or final callback.
     #