mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

additional API per #977

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-04-16 12:13:30 +09:00
parent 9933c36050
commit 8b5627e361
1 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/api/java/Context.java
View file

@ -2057,7 +2057,17 @@ public class Context implements AutoCloseable {
checkContextMatch(re); checkContextMatch(re);
return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject())); 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. * Create the concatenation of regular languages.
*/ */
@ -2075,7 +2085,15 @@ public class Context implements AutoCloseable {
checkContextMatch(t); checkContextMatch(t);
return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(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. * Create a range expression.