diff --git a/src/api/java/Context.java b/src/api/java/Context.java index b22bedef79..c6d928de29 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -4038,6 +4038,37 @@ public BitVecExpr mkFPToFP(Expr rm, Expr exp, Expr 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 FuncDecl mkLinearOrder(R sort, int index) { + return (FuncDecl) 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 FuncDecl mkPartialOrder(R sort, int index) { + return (FuncDecl) FuncDecl.create( + this, + Native.mkPartialOrder( + nCtx(), + sort.getNativeObject(), + index + ) + ); + } /** * Wraps an AST.