mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Revert "Change ASTVector to Expr[] in interpolation result"

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-05-22 08:24:45 -07:00
parent 034a9387ee
commit b4f72c8145
1 changed files with 2 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -90,7 +90,7 @@ public class InterpolationContext extends Context
public class ComputeInterpolantResult public class ComputeInterpolantResult
{ {
public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
public Expr[] interp = null; public ASTVector interp = null;
public Model model = null; public Model model = null;
}; };
@ -110,14 +110,7 @@ public class InterpolationContext extends Context
Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_i = new Native.LongPtr();
Native.LongPtr n_m = 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)); res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
if (res.status == Z3_lbool.Z3_L_FALSE) if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value);
{
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); if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
return res; return res;
} }