mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Allow different parsing strategies (#4205)
* modifiers * modifiers and function * revert * .
This commit is contained in:
parent
39fb44fe09
commit
be998c308c
|
@ -91,12 +91,12 @@ public class ASTVector extends Z3Object {
|
||||||
return Native.astVectorToString(getContext().nCtx(), getNativeObject());
|
return Native.astVectorToString(getContext().nCtx(), getNativeObject());
|
||||||
}
|
}
|
||||||
|
|
||||||
ASTVector(Context ctx, long obj)
|
public ASTVector(Context ctx, long obj)
|
||||||
{
|
{
|
||||||
super(ctx, obj);
|
super(ctx, obj);
|
||||||
}
|
}
|
||||||
|
|
||||||
ASTVector(Context ctx)
|
public ASTVector(Context ctx)
|
||||||
{
|
{
|
||||||
super(ctx, Native.mkAstVector(ctx.nCtx()));
|
super(ctx, Native.mkAstVector(ctx.nCtx()));
|
||||||
}
|
}
|
||||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -70,7 +70,7 @@ public abstract class Z3Object {
|
||||||
return m_ctx;
|
return m_ctx;
|
||||||
}
|
}
|
||||||
|
|
||||||
static long[] arrayToNative(Z3Object[] a)
|
public static long[] arrayToNative(Z3Object[] a)
|
||||||
{
|
{
|
||||||
if (a == null)
|
if (a == null)
|
||||||
return null;
|
return null;
|
||||||
|
@ -80,7 +80,7 @@ public abstract class Z3Object {
|
||||||
return an;
|
return an;
|
||||||
}
|
}
|
||||||
|
|
||||||
static int arrayLength(Z3Object[] a)
|
public static int arrayLength(Z3Object[] a)
|
||||||
{
|
{
|
||||||
return (a == null) ? 0 : a.length;
|
return (a == null) ? 0 : a.length;
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue