From 91352369a979d90abb7143c327329cc3c8d433cc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 26 May 2015 11:20:19 +0100 Subject: [PATCH] Added conversion functions to ASTVectors in .NET and Java. Fixes #108 --- src/api/dotnet/ASTVector.cs | 110 ++++++++++++++++++++++++- src/api/dotnet/Fixedpoint.cs | 8 +- src/api/dotnet/InterpolationContext.cs | 10 +-- src/api/dotnet/Solver.cs | 4 +- src/api/java/ASTVector.java | 110 ++++++++++++++++++++++++- src/api/java/Fixedpoint.java | 8 +- src/api/java/InterpolationContext.java | 8 +- src/api/java/Solver.java | 4 +- 8 files changed, 239 insertions(+), 23 deletions(-) diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index f858c7862..8b599ca48 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -112,7 +112,7 @@ namespace Microsoft.Z3 } /// - /// Translates an AST vector into an Expr[] + /// Translates an ASTVector into an Expr[] /// public Expr[] ToExprArray() { @@ -123,6 +123,114 @@ namespace Microsoft.Z3 return res; } + /// + /// Translates an ASTVector into a BoolExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a BitVecExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a ArithExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a ArrayExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a DatatypeExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a FPExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a FPRMExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a IntExpr[] + /// + 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; + } + + /// + /// Translates an ASTVector into a RealExpr[] + /// + 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); } diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 54dbcd3c1..66449ddbb 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -279,7 +279,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != 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() != 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(); } /// @@ -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(); } diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 9fbdf456e..e6e258b9a 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -47,7 +47,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_get_interpolant in the C/C++ API, which is /// well documented. - 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(); } /// @@ -68,7 +68,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_compute_interpolant in the C/C++ API, which is /// well documented. - 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 /// For more information on interpolation please refer /// too the function Z3_check_interpolant in the C/C++ API, which is /// well documented. - 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); diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index c5227d18f..80ca7a0cd 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -193,7 +193,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != 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() != null); ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject)); - return (BoolExpr[])core.ToExprArray(); + return core.ToBoolExprArray(); } } diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 7011eeb50..5b57db9d9 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -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; + } +} \ No newline at end of file diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index b59a9700a..e1fccdf4f 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -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(); } diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 5af2a6af8..ddce9ee33 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -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(); diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index eb8e81aa5..4d2d9b641 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -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(); } /**