From a229416a2bd12ec4beb9b638d8da65aecc9af645 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcus=20V=C3=B6lker?= Date: Fri, 22 May 2015 15:55:09 +0200 Subject: [PATCH 1/5] Change ASTVector to Expr[] in interpolation result --- src/api/java/InterpolationContext.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 667c91a53..25f132fa7 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 Expr[] interp = null; public Model model = null; }; @@ -110,7 +110,14 @@ public class InterpolationContext extends Context 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); + if (res.status == Z3_lbool.Z3_L_FALSE) + { + ASTVector seq = new ASTVector(this, n_i.value); + int n = seq.size(); + res.interp = new Expr[n]; + for (int i = 0; i < n; i++) + res.interp[i] = Expr.create(this, seq.get(i).getNativeObject()); + } if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } From b4f72c81457712929405f397b89c02bd8ca264c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 May 2015 08:24:45 -0700 Subject: [PATCH 2/5] Revert "Change ASTVector to Expr[] in interpolation result" --- src/api/java/InterpolationContext.java | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 25f132fa7..667c91a53 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 Expr[] interp = null; + public ASTVector interp = null; public Model model = null; }; @@ -110,14 +110,7 @@ public class InterpolationContext extends Context 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) - { - ASTVector seq = new ASTVector(this, n_i.value); - int n = seq.size(); - res.interp = new Expr[n]; - for (int i = 0; i < n; i++) - res.interp[i] = Expr.create(this, seq.get(i).getNativeObject()); - } + if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value); if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } From 279ef05713462237e427dc96192d911a9cb18dbc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 May 2015 08:57:05 -0700 Subject: [PATCH 3/5] 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(); } /** From 13a3bdd7a3589c0a7e8b622acfba20e542c2f2b8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 22 May 2015 10:28:19 -0700 Subject: [PATCH 4/5] fix proof for extended GCD rule --- src/smt/theory_arith_int.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index b600dd3c0..7c9e67da6 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -777,8 +777,8 @@ namespace smt { // u += ncoeff * lower_bound(v).get_rational(); u.addmul(ncoeff, lower_bound(v).get_rational()); } - lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); - upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); + lower(v)->push_justification(ante, it->m_coeff, coeffs_enabled()); + upper(v)->push_justification(ante, it->m_coeff, coeffs_enabled()); } else if (gcds.is_zero()) { gcds = abs_ncoeff; From e438143abce11f3217b275c916307a9cb14ca51e Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 22 May 2015 11:02:26 -0700 Subject: [PATCH 5/5] fix for github issue #105 --- src/interp/iz3translate.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index f510f4070..2debdaf42 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -966,7 +966,7 @@ public: get_linear_coefficients(t,coeffs); if(coeffs.size() == 0) return make_int("1"); // arbitrary - rational d = coeffs[0]; + rational d = abs(coeffs[0]); for(unsigned i = 1; i < coeffs.size(); i++){ d = gcd(d,coeffs[i]); }