From 2e15e2aa4d01357223404ab4f9ab9d201a8fe9ab Mon Sep 17 00:00:00 2001
From: mbergen <mbergent@uni-bremen.de>
Date: Wed, 16 Feb 2022 22:37:20 +0100
Subject: [PATCH] Add access to builtin special relations
 (`Context::mkLinearOrder` and `Context::mkPartialOrder` ) to Java API (#5832)

* Add mkLinearOrder

* reorder arguments to match definition, add short comment

* add partial order

* add comments
---
 src/api/java/Context.java | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index b22bedef7..c6d928de2 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -4038,6 +4038,37 @@ public class Context implements AutoCloseable {
         return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
     }
 
+    /**
+     * Creates or a linear order.
+     * @param index The index of the order.
+     * @param sort The sort of the order.
+     */
+    public <R extends Sort> FuncDecl<BoolSort> mkLinearOrder(R sort, int index) {
+        return (FuncDecl<BoolSort>) FuncDecl.create(
+                this,
+                Native.mkLinearOrder(
+                        nCtx(),
+                        sort.getNativeObject(),
+                        index
+                )
+        );
+    }
+
+    /**
+     * Creates or a partial order.
+     * @param index The index of the order.
+     * @param sort The sort of the order.
+     */
+    public <R extends Sort> FuncDecl<BoolSort> mkPartialOrder(R sort, int index) {
+        return (FuncDecl<BoolSort>) FuncDecl.create(
+                this,
+                Native.mkPartialOrder(
+                    nCtx(),
+                    sort.getNativeObject(),
+                    index
+                )
+        );
+    }
 
     /**
      * Wraps an AST.