From 182039eb44c392078000002f31e8da2ca924b97a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 9 Apr 2019 22:58:43 +0200
Subject: [PATCH] add tc and trc functionals for binary relations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/c++/z3++.h      |  8 ++++++++
 src/api/python/z3/z3.py | 18 ++++++++++++------
 src/api/z3_api.h        | 12 ++++++++++--
 3 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 8df43d477..fd7cb3a90 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -633,6 +633,14 @@ namespace z3 {
         symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
         Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
 
+        func_decl transitive_closure(func_decl const& f) {
+            Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc); 
+        }
+
+        func_decl transitive_reflexive_closure(func_decl const& f) {
+            Z3_func_decl tc = Z3_mk_transitive_reflexive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc); 
+        }
+
         bool is_const() const { return arity() == 0; }
 
         expr operator()() const;
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 9276c3502..242c73e67 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -10379,10 +10379,16 @@ def Range(lo, hi, ctx = None):
 
 # Special Relations
 
-def PartialOrder(n, s):
-    ctx = s.ctx
-    return FuncDeclRef(Z3_mk_partial_order(ctx, n, s.ast), ctx)
+def TransitiveClosure(f):
+    """Given a binary relation R, such that the two arguments have the same sort
+    create the transitive closure relation R+.
+    The transitive closure R+ is a new relation.
+    """
+    return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)
 
-def TreeOrder(n, s):
-    ctx = s.ctx
-    return FuncDeclRef(Z3_mk_tree_order(ctx, n, s.ast), ctx)
+def TransitiveReflexiveClosure(f):
+    """Given a binary relation R, such that the two arguments have the same sort
+    create the transitive reflexive closure relation R*.
+    The transitive reflexive closure R* is a new relation.
+    """
+    return FuncDeclRef(Z3_mk_transitive_reflexive_closure(f.ctx_ref(), f.ast), f.ctx)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 78a6247ed..e154eaf50 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3661,16 +3661,24 @@ extern "C" {
     /**
        \brief create transitive closure of binary relation.
 
+       \pre f is a binary relation, such that the two arguments have the same sorts.
+
+       The resulting relation f+ represents the transitive closure of f.
+
        def_API('Z3_mk_transitive_closure', FUNC_DECL ,(_in(CONTEXT), _in(FUNC_DECL)))
      */
-    Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c,Z3_func_decl f);
+    Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);
 
     /**
        \brief create transitive reflexive closure of binary relation.
 
+       \pre f is a binary relation, such that the two arguments have the same sorts.
+
+       The resulting relation f* represents the transitive-reflexive closure of f.
+
        def_API('Z3_mk_transitive_reflexive_closure', FUNC_DECL ,(_in(CONTEXT), _in(FUNC_DECL)))
      */
-    Z3_func_decl Z3_API Z3_mk_transitive_reflexive_closure(Z3_context c,Z3_func_decl f);
+    Z3_func_decl Z3_API Z3_mk_transitive_reflexive_closure(Z3_context c, Z3_func_decl f);
 
     /*@}*/