From 8b5627e361e2e19ff26dac18d920e01906590ad4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 Apr 2017 12:13:30 +0900
Subject: [PATCH] additional API per #977

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/java/Context.java | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 790ffdca7..db7a08711 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2057,7 +2057,17 @@ public class Context implements AutoCloseable {
 	checkContextMatch(re);
 	return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));            
     }
+
     
+    /**
+     * Create the complement regular expression.
+     */
+    public ReExpr mkComplement(ReExpr re)
+    {
+	checkContextMatch(re);
+	return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));            
+    }    
+
     /**
      * Create the concatenation of regular languages.
      */
@@ -2075,7 +2085,15 @@ public class Context implements AutoCloseable {
 	checkContextMatch(t);
 	return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
     }
-    
+
+    /**
+     * Create the intersection of regular languages.
+     */
+    public ReExpr mkIntersect(ReExpr... t)
+    {
+	checkContextMatch(t);
+	return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
+    }    
     
     /**
      * Create a range expression.