mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add empty/full to java #1944
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
141cd687ff
commit
1603075189
|
@ -2173,6 +2173,22 @@ public class Context implements AutoCloseable {
|
|||
{
|
||||
checkContextMatch(t);
|
||||
return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create the empty regular expression.
|
||||
*/
|
||||
public ReExpr mkEmptyRe(Sort s)
|
||||
{
|
||||
return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create the full regular expression.
|
||||
*/
|
||||
public ReExpr mkFullRe(Sort s)
|
||||
{
|
||||
return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
Loading…
Reference in a new issue