mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Added conversion functions to ASTVectors in .NET and Java.

Browse source 
Fixes #108
This commit is contained in:
Christoph M. Wintersteiger 2015-05-26 11:20:19 +01:00
parent 9912b2cd67
commit 91352369a9
8 changed files with 239 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

110
src/api/dotnet/ASTVector.cs
View file

@ -112,7 +112,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Translates an AST vector into an Expr[]
/// Translates an ASTVector into an Expr[]
/// </summary>
public Expr[] ToExprArray()
{
@ -123,6 +123,114 @@ namespace Microsoft.Z3
return res;
}
/// <summary>
/// Translates an ASTVector into a BoolExpr[]
/// </summary>
public BoolExpr[] ToBoolExprArray()
{
uint n = Size;
BoolExpr[] res = new BoolExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a BitVecExpr[]
/// </summary>
public BitVecExpr[] ToBitVecExprArray()
{
uint n = Size;
BitVecExpr[] res = new BitVecExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a ArithExpr[]
/// </summary>
public ArithExpr[] ToArithExprArray()
{
uint n = Size;
ArithExpr[] res = new ArithExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a ArrayExpr[]
/// </summary>
public ArrayExpr[] ToArrayExprArray()
{
uint n = Size;
ArrayExpr[] res = new ArrayExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a DatatypeExpr[]
/// </summary>
public DatatypeExpr[] ToDatatypeExprArray()
{
uint n = Size;
DatatypeExpr[] res = new DatatypeExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a FPExpr[]
/// </summary>
public FPExpr[] ToFPExprArray()
{
uint n = Size;
FPExpr[] res = new FPExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a FPRMExpr[]
/// </summary>
public FPRMExpr[] ToFPRMExprArray()
{
uint n = Size;
FPRMExpr[] res = new FPRMExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a IntExpr[]
/// </summary>
public IntExpr[] ToIntExprArray()
{
uint n = Size;
IntExpr[] res = new IntExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
/// <summary>
/// Translates an ASTVector into a RealExpr[]
/// </summary>
public RealExpr[] ToRealExprArray()
{
uint n = Size;
RealExpr[] res = new RealExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
return res;
}
#region Internal
internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }

8
src/api/dotnet/Fixedpoint.cs
View file

@ -279,7 +279,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
return (BoolExpr[])av.ToExprArray();
return av.ToBoolExprArray();
}
}
@ -293,7 +293,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
return (BoolExpr[])av.ToExprArray();
return av.ToBoolExprArray();
}
}
@ -318,7 +318,7 @@ namespace Microsoft.Z3
public BoolExpr[] ParseFile(string file)
{
ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
return (BoolExpr[])av.ToExprArray();
return av.ToBoolExprArray();
}
/// <summary>
@ -327,7 +327,7 @@ namespace Microsoft.Z3
public BoolExpr[] ParseString(string s)
{
ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
return (BoolExpr[])av.ToExprArray();
return av.ToBoolExprArray();
}

10
src/api/dotnet/InterpolationContext.cs
View file

@ -47,7 +47,7 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_get_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
{
Contract.Requires(pf != null);
Contract.Requires(pat != null);
@ -59,7 +59,7 @@ namespace Microsoft.Z3
CheckContextMatch(p);
ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
return seq.ToExprArray();
return seq.ToBoolExprArray();
}
/// <summary>
@ -68,7 +68,7 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_compute_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public Z3_lbool ComputeInterpolant(Expr pat, Params p, out Expr[] interp, out Model model)
public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
{
Contract.Requires(pat != null);
Contract.Requires(p != null);
@ -80,7 +80,7 @@ namespace Microsoft.Z3
IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
interp = new ASTVector(this, i).ToExprArray();
interp = new ASTVector(this, i).ToBoolExprArray();
model = new Model(this, m);
return (Z3_lbool)r;
}
@ -102,7 +102,7 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
{
Contract.Requires(cnsts.Length == parents.Length);
Contract.Requires(cnsts.Length == interps.Length + 1);

4
src/api/dotnet/Solver.cs
View file

@ -193,7 +193,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
return (BoolExpr[])assertions.ToExprArray();
return assertions.ToBoolExprArray();
}
}
@ -273,7 +273,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<Expr[]>() != null);
ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
return (BoolExpr[])core.ToExprArray();
return core.ToBoolExprArray();
}
}

110
src/api/java/ASTVector.java
View file

@ -142,4 +142,112 @@ public class ASTVector extends Z3Object
res[i] = Expr.create(getContext(), get(i).getNativeObject());
return res;
}
}
/**
* Translates the AST vector into an BoolExpr[]
* */
public BoolExpr[] ToBoolExprArray()
{
int n = size();
BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++)
res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an BitVecExpr[]
* */
public BitVecExpr[] ToBitVecExprArray()
{
int n = size();
BitVecExpr[] res = new BitVecExpr[n];
for (int i = 0; i < n; i++)
res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an ArithExpr[]
* */
public ArithExpr[] ToArithExprExprArray()
{
int n = size();
ArithExpr[] res = new ArithExpr[n];
for (int i = 0; i < n; i++)
res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an ArrayExpr[]
* */
public ArrayExpr[] ToArrayExprArray()
{
int n = size();
ArrayExpr[] res = new ArrayExpr[n];
for (int i = 0; i < n; i++)
res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an DatatypeExpr[]
* */
public DatatypeExpr[] ToDatatypeExprArray()
{
int n = size();
DatatypeExpr[] res = new DatatypeExpr[n];
for (int i = 0; i < n; i++)
res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an FPExpr[]
* */
public FPExpr[] ToFPExprArray()
{
int n = size();
FPExpr[] res = new FPExpr[n];
for (int i = 0; i < n; i++)
res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an FPRMExpr[]
* */
public FPRMExpr[] ToFPRMExprArray()
{
int n = size();
FPRMExpr[] res = new FPRMExpr[n];
for (int i = 0; i < n; i++)
res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an IntExpr[]
* */
public IntExpr[] ToIntExprArray()
{
int n = size();
IntExpr[] res = new IntExpr[n];
for (int i = 0; i < n; i++)
res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
/**
* Translates the AST vector into an RealExpr[]
* */
public RealExpr[] ToRealExprArray()
{
int n = size();
RealExpr[] res = new RealExpr[n];
for (int i = 0; i < n; i++)
res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
return res;
}
}

8
src/api/java/Fixedpoint.java
View file

@ -296,7 +296,7 @@ public class Fixedpoint extends Z3Object
public BoolExpr[] getRules()
{
ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
return (BoolExpr[]) v.ToExprArray();
return v.ToBoolExprArray();
}
/**
@ -307,7 +307,7 @@ public class Fixedpoint extends Z3Object
public BoolExpr[] getAssertions()
{
ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
return (BoolExpr[]) v.ToExprArray();
return v.ToBoolExprArray();
}
/**
@ -329,7 +329,7 @@ public class Fixedpoint extends Z3Object
public BoolExpr[] ParseFile(String file)
{
ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
return (BoolExpr[])av.ToExprArray();
return av.ToBoolExprArray();
}
/**
@ -340,7 +340,7 @@ public class Fixedpoint extends Z3Object
public BoolExpr[] ParseString(String s)
{
ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
return (BoolExpr[])av.ToExprArray();
return av.ToBoolExprArray();
}

8
src/api/java/InterpolationContext.java
View file

@ -73,14 +73,14 @@ public class InterpolationContext extends Context
* well documented.
* @throws Z3Exception
**/
public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
{
checkContextMatch(pf);
checkContextMatch(pat);
checkContextMatch(p);
ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
return seq.ToExprArray();
return seq.ToBoolExprArray();
}
public class ComputeInterpolantResult
@ -107,7 +107,7 @@ public class InterpolationContext extends Context
Native.LongPtr n_m = new Native.LongPtr();
res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
if (res.status == Z3_lbool.Z3_L_FALSE)
res.interp = (BoolExpr[]) (new ASTVector(this, n_i.value)).ToExprArray();
res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
return res;
}
@ -135,7 +135,7 @@ public class InterpolationContext extends Context
/// Remarks: For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.
public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
{
CheckInterpolantResult res = new CheckInterpolantResult();
Native.StringPtr n_err_str = new Native.StringPtr();

4
src/api/java/Solver.java
View file

@ -188,7 +188,7 @@ public class Solver extends Z3Object
public BoolExpr[] getAssertions()
{
ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
return (BoolExpr[]) assrts.ToExprArray();
return assrts.ToBoolExprArray();
}
/**
@ -280,7 +280,7 @@ public class Solver extends Z3Object
{
ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
return (BoolExpr[])core.ToExprArray();
return core.ToBoolExprArray();
}
/**