mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix examples and C++ API - build failure

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-15 15:44:13 +01:00
parent 0e32c87dc3 1702a55018
commit 93f55605a8
2 changed files with 49 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/api/c++/z3++.h
View file

@ -1111,10 +1111,10 @@ namespace z3 {
}
inline expr concat(expr const& a, expr const& b) {
context& ctx = a.ctx();
Z3_ast r = Z3_mk_concat(ctx, (Z3_ast) a, (Z3_ast) b);
ctx.check_error();
return expr(ctx, r);
check_context(a, b);
Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
a.ctx().check_error();
return expr(a.ctx(), r);
}
class func_entry : public object {

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

@ -87,6 +87,13 @@ public class InterpolationContext extends Context
return res;
}
public class ComputeInterpolantResult
{
public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
public ASTVector interp = null;
public Model model = null;
};
/**
* Computes an interpolant.
* Remarks: For more information on interpolation please refer
@ -94,17 +101,18 @@ public class InterpolationContext extends Context
* well documented.
* @throws Z3Exception
**/
public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model)
public ComputeInterpolantResult ComputeInterpolant(Expr pat, Params p)
{
checkContextMatch(pat);
checkContextMatch(p);
ComputeInterpolantResult res = new ComputeInterpolantResult();
Native.LongPtr n_i = new Native.LongPtr();
Native.LongPtr n_m = new Native.LongPtr();
int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
interp = new ASTVector(this, n_i.value);
model = new Model(this, n_m.value);
return Z3_lbool.fromInt(r);
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_TRUE) res.model = new Model(this, n_m.value);
return res;
}
///
@ -118,16 +126,23 @@ public class InterpolationContext extends Context
return Native.interpolationProfile(nCtx());
}
public class CheckInterpolantResult
{
public int return_value = 0;
public String error = null;
}
///
/// Checks the correctness of an interpolant.
///
/// Remarks: 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, int[] parents, Expr[] interps, String error, Expr[] theory)
public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
{
CheckInterpolantResult res = new CheckInterpolantResult();
Native.StringPtr n_err_str = new Native.StringPtr();
int r = Native.checkInterpolant(nCtx(),
res.return_value = Native.checkInterpolant(nCtx(),
cnsts.length,
Expr.arrayToNative(cnsts),
parents,
@ -135,41 +150,52 @@ public class InterpolationContext extends Context
n_err_str,
theory.length,
Expr.arrayToNative(theory));
error = n_err_str.value;
return r;
res.error = n_err_str.value;
return res;
}
public class ReadInterpolationProblemResult
{
public int return_value = 0;
public Expr[] cnsts;
public int[] parents;
public String error;
public Expr[] theory;
};
///
/// Reads an interpolation problem from a file.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// well documented.
public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
public ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
{
ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
Native.IntPtr n_num = new Native.IntPtr();
Native.IntPtr n_num_theory = new Native.IntPtr();
Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
Native.StringPtr n_err_str = new Native.StringPtr();
int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
res.return_value = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
int num = n_num.value;
int num_theory = n_num_theory.value;
error = n_err_str.value;
cnsts = new Expr[num];
parents = new int[num];
res.error = n_err_str.value;
res.cnsts = new Expr[num];
res.parents = new int[num];
theory = new Expr[num_theory];
for (int i = 0; i < num; i++)
{
cnsts[i] = Expr.create(this, n_cnsts.value[i]);
parents[i] = n_parents.value[i];
res.cnsts[i] = Expr.create(this, n_cnsts.value[i]);
res.parents[i] = n_parents.value[i];
}
for (int i = 0; i < num_theory; i++)
theory[i] = Expr.create(this, n_theory.value[i]);
return r;
res.theory[i] = Expr.create(this, n_theory.value[i]);
return res;
}
///
/// Writes an interpolation problem to a file.
///