From 69e2f33ecf1ae574366a6242cb0e42e2e3bd6040 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 11 Nov 2018 09:50:52 -0800
Subject: [PATCH] undefine min/max #1927

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/c++/z3++.h | 51 +++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 48 insertions(+), 3 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index edc724160..dcb929385 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -28,6 +28,9 @@ Notes:
 #include<z3.h>
 #include<limits.h>
 
+#undef min
+#undef max
+
 /**
    \defgroup cppapi C++ API
 
@@ -1478,9 +1481,51 @@ namespace z3 {
     inline expr nand(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
     inline expr nor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
     inline expr xnor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
-    inline expr min(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_fpa_min(a.ctx(), a, b); return expr(a.ctx(), r); }
-    inline expr max(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_fpa_max(a.ctx(), a, b); return expr(a.ctx(), r); }
-    inline expr abs(expr const & a) { Z3_ast r = Z3_mk_fpa_abs(a.ctx(), a); return expr(a.ctx(), r); }
+    inline expr min(expr const& a, expr const& b) { 
+        check_context(a, b); 
+        Z3_ast r;
+        if (a.is_arith()) {
+            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
+        }
+        else if (a.is_bv()) {
+            r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
+        }
+        else {
+            assert(a.is_fpa());
+            r = Z3_mk_fpa_min(a.ctx(), a, b); 
+        }
+        return expr(a.ctx(), r); 
+    }
+    inline expr max(expr const& a, expr const& b) { 
+        check_context(a, b); 
+        Z3_ast r;
+        if (a.is_arith()) {
+            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
+        }
+        else if (a.is_bv()) {
+            r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
+        }
+        else {
+            assert(a.is_fpa());
+            r = Z3_mk_fpa_max(a.ctx(), a, b); 
+        }
+        return expr(a.ctx(), r); 
+    }
+    inline expr abs(expr const & a) { 
+        Z3_ast r;
+        if (a.is_int()) {
+            expr zero = a.ctx().int_val(0);
+            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
+        }
+        else if (a.is_real()) {
+            expr zero = a.ctx().real_val(0);
+            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
+        }
+        else {
+            r = Z3_mk_fpa_abs(a.ctx(), a); 
+        }
+        return expr(a.ctx(), r); 
+    }
     inline expr sqrt(expr const & a, expr const& rm) {
         check_context(a, rm);
         assert(a.is_fpa());