From 279ef05713462237e427dc96192d911a9cb18dbc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 May 2015 08:57:05 -0700 Subject: [PATCH] expose BoolExpr[] for ASTVector and merge common functionality Signed-off-by: Nikolaj Bjorner --- src/api/java/ASTVector.java | 8 ++++++++ src/api/java/Fixedpoint.java | 12 ++---------- src/api/java/InterpolationContext.java | 8 +++++--- src/api/java/Solver.java | 6 +----- 4 files changed, 16 insertions(+), 18 deletions(-) diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 9c6504493..e08a75e7f 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -119,4 +119,12 @@ public class ASTVector extends Z3Object getContext().getASTVectorDRQ().add(o); super.decRef(o); } + + BoolExpr[] ToBoolArray() { + int n = size(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(getContext(), get(i).getNativeObject()); + return res; + } } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index c9d14288b..daa0f4e3f 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -298,11 +298,7 @@ public class Fixedpoint extends Z3Object ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules( getContext().nCtx(), getNativeObject())); - int n = v.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); - return res; + return v.ToBoolArray(); } /** @@ -315,11 +311,7 @@ public class Fixedpoint extends Z3Object ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions( getContext().nCtx(), getNativeObject())); - int n = v.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); - return res; + return v.ToBoolArray(); } /** diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 667c91a53..50c6a223a 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -90,7 +90,7 @@ public class InterpolationContext extends Context public class ComputeInterpolantResult { public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; - public ASTVector interp = null; + public BoolExpr[] interp = null; public Model model = null; }; @@ -109,8 +109,10 @@ public class InterpolationContext extends Context ComputeInterpolantResult res = new ComputeInterpolantResult(); Native.LongPtr n_i = new Native.LongPtr(); 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 = new ASTVector(this, n_i.value); + 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 = (new ASTVector(this, n_i.value)).ToBoolArray(); + } if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index e4ba9de42..7c4c1f4b9 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -190,11 +190,7 @@ public class Solver extends Z3Object { ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); - int n = assrts.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject()); - return res; + return assrts.ToBoolArray(); } /**