From 3557e0b0c52691c08836dfbc2bd37c2def221646 Mon Sep 17 00:00:00 2001
From: CEisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Tue, 19 Oct 2021 16:48:31 +0200
Subject: [PATCH] Added eq/fixed/final functions in C++ user propagator as
 methods (#5607)

---
 src/api/c++/z3++.h | 41 ++++++++++++++++++++++++++++++++++++-----
 1 file changed, 36 insertions(+), 5 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index f0c0cc3aa..b855b30cc 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1516,7 +1516,7 @@ namespace z3 {
         expr substitute(expr_vector const& dst);
 
 
-	class iterator {
+    class iterator {
             expr& e;
             unsigned i;
         public:
@@ -1912,14 +1912,14 @@ namespace z3 {
         Z3_ast r;
         if (a.is_int()) {
             expr zero = a.ctx().int_val(0);
-	    expr ge = a >= zero;
-	    expr na = -a;
+        expr ge = a >= zero;
+        expr na = -a;
             r = Z3_mk_ite(a.ctx(), ge, a, na);	    
         }
         else if (a.is_real()) {
             expr zero = a.ctx().real_val(0);
-	    expr ge = a >= zero;
-	    expr na = -a;
+        expr ge = a >= zero;
+        expr na = -a;
             r = Z3_mk_ite(a.ctx(), ge, a, na);
         }
         else {
@@ -3954,12 +3954,28 @@ namespace z3 {
             Z3_solver_propagate_fixed(ctx(), *s, fixed_eh); 
         }
 
+        void register_fixed() {
+            assert(s);
+            m_fixed_eh = [this](unsigned id, expr const& e) {
+                fixed(id, e);
+            };
+            Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
+        }
+
         void register_eq(eq_eh_t& f) { 
             assert(s);
             m_eq_eh = f; 
             Z3_solver_propagate_eq(ctx(), *s, eq_eh); 
         }
 
+        void register_eq() {
+            assert(s);
+            m_eq_eh = [this](unsigned x, unsigned y) {
+                eq(x, y);
+            };
+            Z3_solver_propagate_eq(ctx(), *s, eq_eh);
+        }
+
         /**
            \brief register a callback on final-check.
            During the final check stage, all propagations have been processed.
@@ -3973,6 +3989,21 @@ namespace z3 {
             m_final_eh = f; 
             Z3_solver_propagate_final(ctx(), *s, final_eh); 
         }
+        
+        void register_final() { 
+            assert(s);
+            m_final_eh = [this]() {
+                final();
+            };
+            Z3_solver_propagate_final(ctx(), *s, final_eh); 
+        }
+
+
+        virtual void fixed(unsigned id, expr const& e) { }
+
+        virtual void eq(unsigned x, unsigned y) { }
+
+        virtual void final() { }
 
         /**
            \brief tracks \c e by a unique identifier that is returned by the call.